ExactRightSchreierGeneration.lean

theorem profinite_minimalPower_schreierGenerator_lifts_discrete
    [DecidableEq X]
    (β : FreeGroup X →* P) (K : Subgroup P) (x : X) {N : ℕ}
    (hN : 0 < N)
    (hpow : β ((FreeGroup.of x) ^ N) ∈ K)
    (hmin : ∀ m : ℕ, 0 < m → m < N → β ((FreeGroup.of x) ^ m) ∉ K) :
    ∃ T : Set (FreeGroup X), ∃ hT :
        IsRightSchreierTransversal (X := X) (Subgroup.comap β K) T,
      (FreeGroup.of x) ^ (N - 1) ∈ T ∧
        schreierGenerator (X := X) hT ((FreeGroup.of x) ^ (N - 1)) x =
          ⟨(FreeGroup.of x) ^ N, hpow⟩

theorem map_schreierGenerator_eq_cocycle
    [DecidableEq X]
    {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) (Subgroup.comap (π.comp φ) K) T)
    (hβsurj : Function.Surjective (π.comp φ))
    {t : FreeGroup X} (ht : t ∈ T) (x : X) :
    let τ := rightSchreierSectionOfComap π φ (π.comp φ) K rfl hβsurj hT
    let hτ := rightSchreierSectionOfComap_spec π φ (π.comp φ) K rfl hβsurj hT
    let Hc : Subgroup F := Subgroup.comap π K
    rightQuotientSectionCocycle (H := Hc) τ hτ (φ (FreeGroup.of x))
        (Quotient.mk'' (φ t)) =
      ⟨φ (schreierGenerator (X := X) hT t x), by
        change (π.comp φ) ↑(schreierGenerator (X := X) hT t x) ∈ K
        exact (schreierGenerator (X := X) hT t x).2⟩ := by
  classical
  let τ := rightSchreierSectionOfComap π φ (π.comp φ) K rfl hβsurj hT
  let hτ := rightSchreierSectionOfComap_spec π φ (π.comp φ) K rfl hβsurj hT
  let Hc : Subgroup F := Subgroup.comap π K
  let rep := schreierRepresentative (X := X) hT (t * FreeGroup.of x)
  have hτt :
      τ (Quotient.mk'' (φ t)) = φ t := by
    simpa [τ] using
      (rightSchreierSectionOfComap_eq_of_mem π φ (π.comp φ) K rfl hβsurj hT ht)
  have hrep_rel :
      QuotientGroup.rightRel Hc (φ ((rep : T) : FreeGroup X)) (φ (t * FreeGroup.of x)) := by
    rw [QuotientGroup.rightRel_apply]
    dsimp [Hc]
    change π (φ (t * FreeGroup.of x) * (φ ((rep : T) : FreeGroup X))⁻¹) ∈ K
    have hrel :
        t * FreeGroup.of x * (((rep : T) : FreeGroup X))⁻¹ ∈
          Subgroup.comap (π.comp φ) K := by
      exact hT.1.mul_inv_toRightFun_mem (t * FreeGroup.of x)
    simpa [MonoidHom.comp_apply, MonoidHom.map_mul, MonoidHom.map_inv] using hrel
  have hqnext :
      (φ (FreeGroup.of x))⁻¹ • (Quotient.mk'' (φ t) : Quotient (QuotientGroup.rightRel Hc)) =
        Quotient.mk'' (φ ((rep : T) : FreeGroup X)) := by
    calc
      (φ (FreeGroup.of x))⁻¹ • (Quotient.mk'' (φ t) : Quotient (QuotientGroup.rightRel Hc))
          = Quotient.mk'' (φ t * φ (FreeGroup.of x)) := by
              rw [rightCosetMulAction_inv_mk_smul (H := Hc) (φ (FreeGroup.of x)) (φ t)]
      _ = Quotient.mk'' (φ (t * FreeGroup.of x)) := by
            simp only [MonoidHom.map_mul]
      _ = Quotient.mk'' (φ ((rep : T) : FreeGroup X)) := (Quotient.sound' hrep_rel).symm
  have hτnext :
      τ (Quotient.mk'' (φ t * φ (FreeGroup.of x))) =
        φ ((rep : T) : FreeGroup X) := by
    have hqnext' :
        (Quotient.mk'' (φ t * φ (FreeGroup.of x)) :
            Quotient (QuotientGroup.rightRel Hc)) =
          Quotient.mk'' (φ ((rep : T) : FreeGroup X)) := by
      calc
        (Quotient.mk'' (φ t * φ (FreeGroup.of x)) :
            Quotient (QuotientGroup.rightRel Hc))
            = Quotient.mk'' (φ (t * FreeGroup.of x)) := by
                simp only [MonoidHom.map_mul]
        _ = Quotient.mk'' (φ ((rep : T) : FreeGroup X)) := (Quotient.sound' hrep_rel).symm
    rw [hqnext']
    exact
      rightSchreierSectionOfComap_eq_of_mem π φ (π.comp φ) K rfl hβsurj hT rep.2
  have hτrep :
      τ ((φ (FreeGroup.of x))⁻¹ •
          (Quotient.mk'' (φ t) : Quotient (QuotientGroup.rightRel Hc))) =
        φ ((rep : T) : FreeGroup X) := by
    have hrep_sec :
        τ (Quotient.mk'' (φ ((rep : T) : FreeGroup X))) =
          φ ((rep : T) : FreeGroup X) :=
      rightSchreierSectionOfComap_eq_of_mem π φ (π.comp φ) K rfl hβsurj hT rep.2
    exact hqnext ▸ hrep_sec
  apply Subtype.ext
  change
      τ (Quotient.mk'' (φ t)) * φ (FreeGroup.of x) *
          (τ ((φ (FreeGroup.of x))⁻¹ •
            (Quotient.mk'' (φ t) : Quotient (QuotientGroup.rightRel Hc))))⁻¹ =
        φ ↑(schreierGenerator hT t x)
  dsimp [rightQuotientSectionCocycle]
  have hqnext'' :
      (Quotient.mk'' (φ t * φ (FreeGroup.of x)) :
          Quotient (QuotientGroup.rightRel Hc)) =
        (φ (FreeGroup.of x))⁻¹ •
          (Quotient.mk'' (φ t) : Quotient (QuotientGroup.rightRel Hc)) := by
    simp only [rightCosetMulAction_mk_smul, inv_inv] at hqnext ⊢
  have hqnext''' :
      (Quotient.mk'' (φ t * (φ (FreeGroup.of x))⁻¹⁻¹) :
          Quotient (QuotientGroup.rightRel Hc)) =
        (φ (FreeGroup.of x))⁻¹ •
          (Quotient.mk'' (φ t) : Quotient (QuotientGroup.rightRel Hc)) := by
    simpa only [inv_inv] using hqnext''
  rw [hτt, hqnext''', hτrep]
  simp only [mul_assoc, schreierGenerator, MonoidHom.map_mul, MonoidHom.map_inv, rep]

theorem rightQuotientSectionCocycle_eq_map_schreierGenerator_of_comap
    [DecidableEq X]
    {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) (Subgroup.comap (π.comp φ) K) T)
    (hβsurj : Function.Surjective (π.comp φ))
    {t : FreeGroup X} (ht : t ∈ T) (x : X) :
    let τ := rightSchreierSectionOfComap π φ (π.comp φ) K rfl hβsurj hT
    let hτ := rightSchreierSectionOfComap_spec π φ (π.comp φ) K rfl hβsurj hT
    let Hc : Subgroup F := Subgroup.comap π K
    rightQuotientSectionCocycle (H := Hc) τ hτ (φ (FreeGroup.of x))
        (Quotient.mk'' (φ t)) =
      ⟨φ (schreierGenerator (X := X) hT t x), by
        change (π.comp φ) ↑(schreierGenerator (X := X) hT t x) ∈ K
        exact (schreierGenerator (X := X) hT t x).2⟩ := by
  simpa using map_schreierGenerator_eq_cocycle
    (X := X) (φ := φ) (π := π) (K := K) hT hβsurj ht x

theorem topologicallyGenerates_range_transportedCocycle
    [DecidableEq X]
    {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) (Subgroup.comap (π.comp φ) K) T)
    (hβsurj : Function.Surjective (π.comp φ))
    (hφdense :
      DenseRange
        ({ toFun := fun g : Subgroup.comap (π.comp φ) K => ⟨φ g.1, g.2⟩
           map_one' := by simp only [OneMemClass.coe_one, map_one, Subgroup.mk_eq_one]
           map_mul' := by
             intro a b
             ext
             simp only [Subgroup.coe_mul, map_mul]} :
          Subgroup.comap (π.comp φ) K →* ↥(Subgroup.comap π K))) :
    let τ := rightSchreierSectionOfComap π φ (π.comp φ) K rfl hβsurj hT
    let hτ := rightSchreierSectionOfComap_spec π φ (π.comp φ) K rfl hβsurj hT
    let κ :
        Quotient (QuotientGroup.rightRel (Subgroup.comap π K)) × X →
          ↥(Subgroup.comap π K) :=
      fun p =>
        rightQuotientSectionCocycle (H := Subgroup.comap π K) τ hτ (φ (FreeGroup.of p.2)) p.1
    ProCGroups.Generation.TopologicallyGenerates (G := ↥(Subgroup.comap π K)) (Set.range κ) := by
  classical
  let φL : Subgroup.comap (π.comp φ) K →* ↥(Subgroup.comap π K) :=
    { toFun := fun g => ⟨φ g.1, g.2⟩
      map_one' := by simp only [OneMemClass.coe_one, map_one, Subgroup.mk_eq_one]
      map_mul' := by
        intro a b
        ext
        simp only [Subgroup.coe_mul, map_mul]}
  let τ := rightSchreierSectionOfComap π φ (π.comp φ) K rfl hβsurj hT
  let hτ := rightSchreierSectionOfComap_spec π φ (π.comp φ) K rfl hβsurj hT
  let κ :
      Quotient (QuotientGroup.rightRel (Subgroup.comap π K)) × X →
        ↥(Subgroup.comap π K) :=
    fun p =>
      rightQuotientSectionCocycle (H := Subgroup.comap π K) τ hτ (φ (FreeGroup.of p.2)) p.1
  have hsubset :
      φL '' (schreierGeneratorSet (X := X) hT : Set (Subgroup.comap (π.comp φ) K)) ⊆
        Set.range κ := by
    intro z hz
    rcases hz with ⟨s, hs, rfl⟩
    rcases hs with ⟨t, ht, x, rfl, _⟩
    refine ⟨(Quotient.mk'' (φ t), x), ?_⟩
    simpa [κ, φL] using
      (map_schreierGenerator_eq_cocycle (X := X) (φ := φ) (π := π) (K := K)
        hT hβsurj ht x)
  have hmap :
      Subgroup.closure
          (φL '' (schreierGeneratorSet (X := X) hT :
            Set (Subgroup.comap (π.comp φ) K))) =
        φL.range := by
    calc
      Subgroup.closure
          (φL '' (schreierGeneratorSet (X := X) hT :
            Set (Subgroup.comap (π.comp φ) K)))
          = (Subgroup.closure
              (schreierGeneratorSet (X := X) hT :
                Set (Subgroup.comap (π.comp φ) K))).map φL := by
                  symm
                  exact MonoidHom.map_closure φL _
      _ = (⊤ : Subgroup (Subgroup.comap (π.comp φ) K)).map φL := by
            rw [closure_schreierGeneratorSet_eq_top (X := X) hT]
      _ = φL.range := by
            rw [← MonoidHom.range_eq_map]
  have hgenImg :
      ProCGroups.Generation.TopologicallyGenerates (G := ↥(Subgroup.comap π K))
        (φL '' (schreierGeneratorSet (X := X) hT :
          Set (Subgroup.comap (π.comp φ) K))) := by
    rw [ProCGroups.Generation.topologicallyGenerates_iff_dense]
    rw [hmap]
    change Dense (Set.range φL)
    exact hφdense
  exact ProCGroups.Generation.topologicallyGenerates_mono (G := ↥(Subgroup.comap π K))
    hgenImg hsubset

theorem topologicallyGenerates_topologicalClosure_of_range
    (ξ : Y → G) :
    let W : Subgroup G := (Subgroup.closure (Set.range ξ)).topologicalClosure
    let ξW : Y → W := fun y =>
      ⟨ξ y, Subgroup.le_topologicalClosure _ (Subgroup.subset_closure ⟨y, rfl⟩)⟩
    ProCGroups.Generation.TopologicallyGenerates (G := W) (Set.range ξW) := by
  classical
  let A : Subgroup G := Subgroup.closure (Set.range ξ)
  let W : Subgroup G := A.topologicalClosure
  let ξW : Y → W := fun y =>
    ⟨ξ y, Subgroup.le_topologicalClosure _ (Subgroup.subset_closure ⟨y, rfl⟩)⟩
  rw [ProCGroups.Generation.topologicallyGenerates_iff_dense]
  let B : Subgroup W := Subgroup.closure (Set.range ξW)
  let i : W →* G := W.subtype
  have hrange : i '' Set.range ξW = Set.range ξ := by
    ext g
    constructor
    · rintro ⟨y, ⟨x, rfl⟩, rfl⟩
      exact ⟨x, rfl⟩
    · rintro ⟨y, rfl⟩
      exact ⟨ξW y, ⟨y, rfl⟩, rfl⟩
  have hmap : B.map i = A := by
    calc
      B.map i = Subgroup.closure (i '' Set.range ξW) := by
        simpa [B] using (MonoidHom.map_closure i (Set.range ξW))
      _ = A := by
        simp only [hrange, A]
  have himage : ((↑) : W → G) '' (B : Set W) = (A : Set G) := by
    change i '' (B : Set W) = (A : Set G)
    exact congrArg SetLike.coe hmap
  have hsubset :
      (W : Set G) ⊆ closure (((↑) : W → G) '' (B : Set W)) := by
    rw [himage]
    simp only [Subgroup.topologicalClosure_coe, subset_refl, W, A]
  exact (Subtype.dense_iff).2 hsubset

theorem continuousMonoidHom_eq_of_agrees_on_topologicallyGeneratingSet
    {X : Set G}
    (hX : ProCGroups.Generation.TopologicallyGenerates (G := G) X)
    {f g : G →* A} (hf : Continuous f) (hg : Continuous g)
    (hfg : Set.EqOn f g X) :
    f = g

instance instMulActionRightCosetComap :
    MulAction F (Quotient (QuotientGroup.rightRel (Subgroup.comap π K)))

theorem wreathLeftCoordinate_basepoint_of_transversalWord
    (hT : IsRightSchreierTransversal (X := X) (Subgroup.comap (π.comp φ) K) T)
    (ψ : F →* PermutationalWreathProduct A
      (Quotient (QuotientGroup.rightRel (Subgroup.comap π K))) F)
    (hψ :
      (SemidirectProduct.rightHom :
          PermutationalWreathProduct A
            (Quotient (QuotientGroup.rightRel (Subgroup.comap π K))) F →* F).comp ψ =
        MonoidHom.id F)
    (hone :
      ∀ {t : FreeGroup X}, t ∈ T → ∀ x : X,
        schreierGenerator (X := X) hT t x = 1 →
          wreathLeftCoordinate ψ
            (Quotient.mk'' (φ t) :
              Quotient (QuotientGroup.rightRel (Subgroup.comap π K)))
            (φ (FreeGroup.of x)) = 1)
    (t : FreeGroup X) (ht : t ∈ T) :
    wreathLeftCoordinate ψ
      (Quotient.mk'' (1 : F) :
        Quotient (QuotientGroup.rightRel (Subgroup.comap π K)))
      (φ t) = 1

theorem wreathLeftCoordinate_basepoint_of_rightSchreierSectionOfComap
    (hT : IsRightSchreierTransversal (X := X) (Subgroup.comap (π.comp φ) K) T)
    (hβsurj : Function.Surjective (π.comp φ))
    (ψ : F →* PermutationalWreathProduct A
      (Quotient (QuotientGroup.rightRel (Subgroup.comap π K))) F)
    (hψ :
      (SemidirectProduct.rightHom :
          PermutationalWreathProduct A
            (Quotient (QuotientGroup.rightRel (Subgroup.comap π K))) F →* F).comp ψ =
        MonoidHom.id F)
    (hone :
      ∀ {t : FreeGroup X}, t ∈ T → ∀ x : X,
        schreierGenerator (X := X) hT t x = 1 →
          wreathLeftCoordinate ψ
            (Quotient.mk'' (φ t) :
              Quotient (QuotientGroup.rightRel (Subgroup.comap π K)))
            (φ (FreeGroup.of x)) = 1)
    (q : Quotient (QuotientGroup.rightRel (Subgroup.comap π K))) :
    wreathLeftCoordinate ψ
      (Quotient.mk'' (1 : F) :
        Quotient (QuotientGroup.rightRel (Subgroup.comap π K)))
      (rightSchreierSectionOfComap π φ (π.comp φ) K rfl hβsurj hT q) = 1

theorem exists_continuousFiniteQuotientLift_of_comap_freeGroupLift
    (C : ProCGroups.FiniteGroupClass.{u})
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
    (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
    (hQuot : ProCGroups.FiniteGroupClass.QuotientClosed C)
    (hExt : ProCGroups.FiniteGroupClass.ExtensionClosed C)
    {X : Type u} [Finite X]
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
      [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
    {ι : X → F}
    (hF : IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := C) X F ι)
    (H : OpenSubgroup F)
    {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
    [Finite Q] [DiscreteTopology Q]
    (hQ : C Q)
    (ψ : Subgroup.comap (FreeGroup.lift ι) (H : Subgroup F) →* Q) :
    ∃ ψBar : ↥(H : Subgroup F) →* Q,
      Continuous ψBar ∧
        ψBar.comp
          ({ toFun := fun g : Subgroup.comap (FreeGroup.lift ι) (H : Subgroup F) =>
              ⟨(FreeGroup.lift ι) g.1, g.2⟩
             map_one' := by simp only [OneMemClass.coe_one, map_one, Subgroup.mk_eq_one]
             map_mul' := by
               intro a b
               ext
               simp only [Subgroup.coe_mul, map_mul]} :
            Subgroup.comap (FreeGroup.lift ι) (H : Subgroup F) →* ↥(H : Subgroup F)) = ψ := by
  classical
  let n : ℕ := Nat.card (F ⧸ (H : Subgroup F))
  let P := openSubgroupIndexActionRange (G := F) H
    (show Nat.card (F ⧸ (H : Subgroup F)) = n by rfl)
  let ρ : F →ₜ* P :=
    openSubgroupIndexActionRangeContinuousHom (G := F) H
      (show Nat.card (F ⧸ (H : Subgroup F)) = n by rfl)
  let q0 : F ⧸ (H : Subgroup F) := QuotientGroup.mk (s := (H : Subgroup F)) (1 : F)
  let K : Subgroup P := MulAction.stabilizer P q0
  let βF : FreeGroup X →* F := FreeGroup.lift ι
  let β : FreeGroup X →* P := ρ.toMonoidHom.comp βF
  let Lk : Subgroup (FreeGroup X) := Subgroup.comap β K
  let L : Subgroup (FreeGroup X) := Subgroup.comap βF (H : Subgroup F)
  let : TopologicalSpace (FreeGroup X) := ⊥
  let : DiscreteTopology (FreeGroup X) := ⟨rfl⟩
  have hcomap : Subgroup.comap ρ.toMonoidHom K = (H : Subgroup F) := by
    ext g
    constructor
    · intro hg
      change ρ g • q0 = q0 at hg
      rw [openSubgroupIndexActionRangeContinuousHom_smul_basepoint
        (G := F) H (show Nat.card (F ⧸ (H : Subgroup F)) = n by rfl) g] at hg
      change (QuotientGroup.mk (s := (H : Subgroup F)) g : F ⧸ (H : Subgroup F)) =
          QuotientGroup.mk (s := (H : Subgroup F)) (1 : F) at hg
      simpa [QuotientGroup.eq] using hg
    · intro hg
      change ρ g • q0 = q0
      exact openSubgroupIndexActionRangeContinuousHom_smul_basepoint_of_mem
        (G := F) H (show Nat.card (F ⧸ (H : Subgroup F)) = n by rfl) hg
  have hLk : Lk = L := by
    ext w
    change β w ∈ K ↔ βF w ∈ (H : Subgroup F)
    change βF w ∈ Subgroup.comap ρ.toMonoidHom K ↔ βF w ∈ (H : Subgroup F)
    rw [hcomap]
  let Hc : OpenSubgroup F :=
    { toSubgroup := Subgroup.comap ρ.toMonoidHom K
      isOpen' := by
        rw [hcomap]
        exact H.isOpen' }
  have hHc : Hc = H := by
    ext g
    change g ∈ Subgroup.comap ρ.toMonoidHom K ↔ g ∈ (H : Subgroup F)
    rw [hcomap]
  let toK : L →* Lk :=
    { toFun := fun g => ⟨g.1, by
        have hgL : βF g.1 ∈ (H : Subgroup F) := g.2
        have hgComap : βF g.1 ∈ (Subgroup.comap ρ.toMonoidHom K : Subgroup F) := by
          exact (congrArg (fun S : Subgroup F => βF g.1 ∈ S) hcomap).mpr hgL
        change ρ (βF g.1) ∈ K
        exact hgComap⟩
      map_one' := by simp only [OneMemClass.coe_one, Subgroup.mk_eq_one]
      map_mul' := by
        intro a b
        ext
        simp only [Subgroup.coe_mul, MulMemClass.mk_mul_mk]}
  let fromK : Lk →* L :=
    { toFun := fun g => ⟨g.1, by
        have hgLk : β g.1 ∈ K := g.2
        have hgComap : βF g.1 ∈ (Subgroup.comap ρ.toMonoidHom K : Subgroup F) := by
          change ρ (βF g.1) ∈ K
          simpa [β] using hgLk
        have hgH : βF g.1 ∈ (H : Subgroup F) := by
          exact (congrArg (fun S : Subgroup F => βF g.1 ∈ S) hcomap).mp hgComap
        change βF g.1 ∈ (H : Subgroup F)
        exact hgH⟩
      map_one' := by simp only [OneMemClass.coe_one, Subgroup.mk_eq_one]
      map_mul' := by
        intro a b
        ext
        simp only [Subgroup.coe_mul, MulMemClass.mk_mul_mk]}
  let φOrig : L →* ↥(H : Subgroup F) :=
    { toFun := fun g => ⟨βF g.1, g.2⟩
      map_one' := by simp only [OneMemClass.coe_one, map_one, Subgroup.mk_eq_one]
      map_mul' := by
        intro a b
        ext
        simp only [Subgroup.coe_mul, map_mul]}
  let φK : Lk →* ↥(Hc : Subgroup F) :=
    { toFun := fun g => ⟨βF g.1, by
        have hgLk : β g.1 ∈ K := g.2
        change ρ (βF g.1) ∈ K
        simpa [β] using hgLk⟩
      map_one' := by simp only [OneMemClass.coe_one, map_one, Subgroup.mk_eq_one]
      map_mul' := by
        intro a b
        ext
        simp only [Subgroup.coe_mul, map_mul, MulMemClass.mk_mul_mk]}
  let toHc : ↥(H : Subgroup F) →* ↥(Hc : Subgroup F) :=
    { toFun := fun g => ⟨g.1, by
        have hgH : g.1 ∈ (H : Subgroup F) := g.2
        have hgComap : g.1 ∈ (Subgroup.comap ρ.toMonoidHom K : Subgroup F) := by
          exact (congrArg (fun S : Subgroup F => g.1 ∈ S) hcomap).mpr hgH
        change ρ g.1 ∈ K
        exact hgComap⟩
      map_one' := by simp only [OneMemClass.coe_one, Subgroup.mk_eq_one]
      map_mul' := by
        intro a b
        ext
        simp only [Subgroup.coe_mul, MulMemClass.mk_mul_mk]}
  let ψK : Lk →* Q := ψ.comp fromK
  let : DiscreteTopology (OpenSubgroupRightQuotient Hc) :=
    discreteTopology_openSubgroupRightQuotient (F := F) Hc
  let : ContinuousSMul F (OpenSubgroupRightQuotient Hc) := by
    refine ContinuousSMul.mk ?_
    refine (continuous_prod_of_discrete_right).2 ?_
    intro q
    convert
      (continuous_rightCosetMulAction_inv_smul_of_open
        (G := F) (H := (Hc : Subgroup F)) Hc.isOpen' q).comp continuous_inv using 1
    ext g
    simp only [Function.comp_apply, inv_inv]
  have hβFdense : DenseRange βF :=
    denseRange_freeGroupLift_of_topologicallyGenerates
      (F := F) (X := X) hF.generates_range
  have hρSurj : Function.Surjective ρ := by
    intro p
    rcases p.down.2 with ⟨g, hg⟩
    refine ⟨g, ?_⟩
    apply ULift.ext
    apply Subtype.ext
    exact hg
  have hβDense : DenseRange β := by
    simpa [β, MonoidHom.comp_apply] using
      (Function.Surjective.denseRange hρSurj).comp hβFdense ρ.continuous_toFun
  have hβSurj : Function.Surjective β :=
    surjective_of_denseRange (F := FreeGroup X) (P := P) hβDense
  obtain ⟨T, hTK⟩ := exists_rightSchreierTransversal (X := X) Lk
  let eQuot :
      Quotient (QuotientGroup.rightRel Lk) ≃ OpenSubgroupRightQuotient Hc := by
    simpa [Hc, OpenSubgroupRightQuotient] using
      (rightQuotientEquivOfComap ρ.toMonoidHom βF β K rfl hβSurj)
  let tRep : OpenSubgroupRightQuotient Hc → T := fun q =>
    hTK.1.rightQuotientEquiv (eQuot.symm q)
  have htRep_eq_of_mem {t : FreeGroup X} (ht : t ∈ T) :
      tRep (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc) = ⟨t, ht⟩ := by
    have hmk :
        (rightQuotientEquivOfComap ρ.toMonoidHom βF β K rfl hβSurj)
            (Quotient.mk'' t : Quotient (QuotientGroup.rightRel Lk)) =
          (Quotient.mk'' (βF t) :
            Quotient (QuotientGroup.rightRel (Subgroup.comap ρ.toMonoidHom K))) := by
      exact rightQuotientEquivOfComap_mk ρ.toMonoidHom βF β K rfl hβSurj t
    have hEq :
        eQuot.symm (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc) =
          (Quotient.mk'' t : Quotient (QuotientGroup.rightRel Lk)) := by
      exact eQuot.symm_apply_eq.mpr
        (by simpa [eQuot, Hc, OpenSubgroupRightQuotient] using hmk.symm)
    apply hTK.1.rightQuotientEquiv.symm.injective
    have hqt :
        (Quotient.mk'' t : Quotient (QuotientGroup.rightRel Lk)) =
          hTK.1.rightQuotientEquiv.symm ⟨t, ht⟩ := by
      simpa using
        hTK.1.mk''_rightQuotientEquiv
          (hTK.1.rightQuotientEquiv.symm ⟨t, ht⟩)
    simpa only [tRep, Equiv.symm_apply_apply] using hEq.trans hqt
  let ν :
      X → PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F := fun x =>
    ⟨fun q => ψK (schreierGenerator (X := X) hTK ((tRep q : T) : FreeGroup X) x), ι x⟩
  have hQproC : HasOpenNormalBasisInClass C Q := by
    exact HasOpenNormalBasisInClass.of_finite_discrete (C := C) (G := Q) hQuot hQ
  have hWreath :
      HasOpenNormalBasisInClass C
        (PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F) := by
    exact
      hasOpenNormalBasisInClass_permutationalWreathProduct
        (C := C) hForm hIso hExt hQproC hF.hasOpenNormalBasisInClass
  let W : Subgroup (PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F) :=
    (Subgroup.closure (Set.range ν)).topologicalClosure
  have hWproC : HasOpenNormalBasisInClass C W := by
    exact
      HasOpenNormalBasisInClass.of_isClosed_subgroup
        (C := C) (G := PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F)
        hIso hSub hWreath W (Subgroup.isClosed_topologicalClosure _)
  let hWclosed : IsClosed (W : Set (PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc)
      F)) := by
    simp [W]
  let : CompactSpace W := hWclosed.isClosedEmbedding_subtypeVal.compactSpace
  let νW : X → W := fun x =>
    ⟨ν x, Subgroup.le_topologicalClosure _ (Subgroup.subset_closure ⟨x, rfl⟩)⟩
  have hνWconv : FamilyConvergesToOneAlongOpenSubgroups (G := W) νW := by
    exact FamilyConvergesToOneAlongOpenSubgroups.of_finite_domain (G := W) νW
  have hνWgen :
      ProCGroups.Generation.TopologicallyGenerates (G := W) (Set.range νW) := by
    simpa [W, νW] using topologicallyGenerates_topologicalClosure_of_range ν
  rcases hF.existsUnique_lift hWproC νW hνWconv hνWgen with
    ⟨ηW, hηW, _⟩
  let η : F →* PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F :=
    W.subtype.comp ηW
  have hηCont : Continuous η := by
    simpa [η] using (continuous_subtype_val.comp hηW.1)
  have hηOnGen : ∀ x : X, η (ι x) = ν x := by
    intro x
    simpa [η, νW] using congrArg Subtype.val (hηW.2 x)
  have hηRight :
      (SemidirectProduct.rightHom :
          PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F →* F).comp η =
        MonoidHom.id F := by
    rcases hF.existsUnique_lift hF.hasOpenNormalBasisInClass ι
        hF.convergesToOneAlongOpenSubgroups hF.generates_range with
      ⟨u, hu, huuniq⟩
    have hu_id : MonoidHom.id F = u := by
      exact
        huuniq (MonoidHom.id F)
          ⟨by simpa using (continuous_id : Continuous fun x : F => x), by intro x; rfl⟩
    have hu_η :
        (SemidirectProduct.rightHom :
            PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F →* F).comp η = u := by
      let v : F →* F :=
        (SemidirectProduct.rightHom :
            PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F →* F).comp η
      have hv_on_gen : ∀ x : X, v (ι x) = ι x := by
        intro x
        have hx := congrArg
          (fun z : PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F => z.right)
          (hηOnGen x)
        simpa [v, ν, MonoidHom.comp_apply] using hx
      exact huuniq v ⟨continuous_permutationalWreathProduct_right.comp hηCont, hv_on_gen⟩
    calc
      (SemidirectProduct.rightHom :
          PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F →* F).comp η = u := hu_η
      _ = MonoidHom.id F := hu_id.symm
  have hηCoord :
      ∀ q : OpenSubgroupRightQuotient Hc, ∀ x : X,
        wreathLeftCoordinate η q (βF (FreeGroup.of x)) =
          ψK (schreierGenerator (X := X) hTK ((tRep q : T) : FreeGroup X) x) := by
    intro q x
    simpa [wreathLeftCoordinate, βF, ν] using
      congrArg
        (fun z : PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F => z.left q)
        (hηOnGen x)
  have hηOne :
      ∀ {t : FreeGroup X}, t ∈ T → ∀ x : X,
        schreierGenerator (X := X) hTK t x = 1 →
          wreathLeftCoordinate η
            (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc)
            (βF (FreeGroup.of x)) = 1 := by
    intro t ht x hsg
    rw [hηCoord]
    rw [htRep_eq_of_mem (t := t) ht]
    simp only [hsg, map_one, ψK]
  have htPure :
      ∀ q : OpenSubgroupRightQuotient Hc,
        wreathLeftCoordinate η
          (Quotient.mk'' (1 : F) : OpenSubgroupRightQuotient Hc)
          (rightSchreierSectionOfComap ρ.toMonoidHom βF β K rfl hβSurj hTK q) = 1 := by
    intro q
    simpa [Hc, OpenSubgroupRightQuotient, β] using
      (wreathLeftCoordinate_basepoint_of_rightSchreierSectionOfComap
        (X := X) (φ := βF) (π := ρ.toMonoidHom) (K := K) (T := T)
        hTK hβSurj η hηRight hηOne q)
  let ψBarK : ↥(Hc : Subgroup F) →* Q :=
    rightQuotientBasepointProjectionHom (H := (Hc : Subgroup F)) η hηRight
  have hψBarKCont : Continuous ψBarK := by
    change Continuous
      ((fun z : PermutationalWreathProduct Q (OpenSubgroupRightQuotient Hc) F =>
          z.left (Quotient.mk'' (1 : F))) ∘ η ∘ Subtype.val)
    exact
      (continuous_permutationalWreathProduct_left_apply (A := Q)
        (S := OpenSubgroupRightQuotient Hc) (G := F)
        (Quotient.mk'' (1 : F) : OpenSubgroupRightQuotient Hc)).comp
          (hηCont.comp continuous_subtype_val)
  have hψBarKOnSchreier :
      ∀ s : ↥(schreierGeneratorSet (X := X) hTK),
        ψBarK (φK s) = ψK s := by
    rintro ⟨s, hs⟩
    rcases hs with ⟨t, ht, x, rfl, _hne⟩
    have hmap :
        φK (schreierGenerator (X := X) hTK t x) =
          rightQuotientSectionCocycle
            (H := (Hc : Subgroup F))
            (rightSchreierSectionOfComap ρ.toMonoidHom βF β K rfl hβSurj hTK)
            (rightSchreierSectionOfComap_spec ρ.toMonoidHom βF β K rfl hβSurj hTK)
            (βF (FreeGroup.of x))
            (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc) := by
      apply Subtype.ext
      have hcocycle :=
        congrArg Subtype.val
          (map_schreierGenerator_eq_cocycle
            (X := X) (φ := βF) (π := ρ.toMonoidHom) (K := K) hTK hβSurj ht x).symm
      change βF ↑(schreierGenerator (X := X) hTK t x) =
        ↑(rightQuotientSectionCocycle
          (H := (Hc : Subgroup F))
          (rightSchreierSectionOfComap ρ.toMonoidHom βF β K rfl hβSurj hTK)
          (rightSchreierSectionOfComap_spec
            ρ.toMonoidHom βF β K rfl hβSurj hTK)
          (βF (FreeGroup.of x))
          (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc))
      convert hcocycle using 1
    calc
      ψBarK (φK (schreierGenerator (X := X) hTK t x)) =
          ψBarK
            (rightQuotientSectionCocycle
              (H := (Hc : Subgroup F))
              (rightSchreierSectionOfComap ρ.toMonoidHom βF β K rfl hβSurj hTK)
              (rightSchreierSectionOfComap_spec
                ρ.toMonoidHom βF β K rfl hβSurj hTK)
              (βF (FreeGroup.of x))
              (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc)) := by
            rw [hmap]
      _ =
          wreathLeftCoordinate η
            (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc)
            (βF (FreeGroup.of x)) := by
            simpa [ψBarK, Hc, OpenSubgroupRightQuotient] using
              (rightQuotientBasepointProjectionHom_apply_cocycle
                (H := (Hc : Subgroup F))
                (τ := rightSchreierSectionOfComap ρ.toMonoidHom βF β K rfl hβSurj hTK)
                (hτ := rightSchreierSectionOfComap_spec
                  ρ.toMonoidHom βF β K rfl hβSurj hTK)
                (ψ := η) hηRight htPure
                (βF (FreeGroup.of x))
                (Quotient.mk'' (βF t) : OpenSubgroupRightQuotient Hc))
      _ = ψK (schreierGenerator (X := X) hTK t x) := by
            rw [hηCoord]
            rw [htRep_eq_of_mem (t := t) ht]
  have hψBarKFac : ψBarK.comp φK = ψK := by
    have hSchGen :
        ProCGroups.Generation.TopologicallyGenerates
          (G := Lk) (schreierGeneratorSet (X := X) hTK : Set Lk) := by
      rw [ProCGroups.Generation.topologicallyGenerates_iff_dense]
      rw [closure_schreierGeneratorSet_eq_top (X := X) hTK]
      exact dense_univ
    apply continuousMonoidHom_eq_of_agrees_on_topologicallyGeneratingSet
      (G := Lk) (A := Q) hSchGen
      (continuous_of_discreteTopology : Continuous (ψBarK.comp φK))
      (continuous_of_discreteTopology : Continuous ψK)
    intro h hh
    exact hψBarKOnSchreier ⟨h, hh⟩
  let ψBar : ↥(H : Subgroup F) →* Q := ψBarK.comp toHc
  have htoHcCont : Continuous toHc :=
    Continuous.subtype_mk continuous_subtype_val (by
      intro x
      exact (congrArg (fun S : Subgroup F => x.1 ∈ S) hcomap).mpr x.2)
  have hψBarCont : Continuous ψBar := hψBarKCont.comp htoHcCont
  refine ⟨ψBar, hψBarCont, ?_⟩
  apply MonoidHom.ext
  intro l
  have hto :
      toHc (φOrig l) = φK (toK l) := by
    ext
    rfl
  have hfrom :
      fromK (toK l) = l := by
    ext
    rfl
  have hfacK := congrArg (fun f : Lk →* Q => f (toK l)) hψBarKFac
  calc
    ψBar (φOrig l) = ψBarK (φK (toK l)) := by
      simpa [ψBar, MonoidHom.comp_apply] using congrArg ψBarK hto
    _ = ψK (toK l) := hfacK
    _ = ψ (fromK (toK l)) := rfl
    _ = ψ l := by rw [hfrom]

theorem exists_pointedFreeRightSchreierGeneratorFamily_of_openSubgroup
    {C : ProCGroups.FiniteGroupClass.{u}}
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
    (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
    (hExt : ProCGroups.FiniteGroupClass.ExtensionClosed C)
    {X : Type u} [TopologicalSpace X] [CompactSpace X] {x0 : X}
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
      [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
    {ι : X → F}
    (hF : IsEpimorphicallyPointedFreeProCGroupOn
      (C := C) X x0 F ι)
    (H : OpenSubgroup F) :
    ∃ κ : OpenSubgroupRightQuotient H × X → ↥(H : Subgroup F),
      Continuous κ ∧
      (∀ q : OpenSubgroupRightQuotient H, κ (q, x0) = 1) ∧
      κ (openSubgroupRightCoset H (1 : F), x0) = 1 ∧
      IsCompact (Set.range κ) ∧
      IsClosed (Set.range κ) ∧
      IsEpimorphicallyPointedFreeProCGroupOn
        (C := C)
        (Set.range κ)
        ⟨κ (openSubgroupRightCoset H (1 : F), x0),
          ⟨(openSubgroupRightCoset H (1 : F), x0), rfl⟩⟩
        ↥(H : Subgroup F) Subtype.val

theorem exists_pointedFreeRightSchreierGeneratorFamily_of_openSubgroup_of_minimalGeneratorPower
    {C : ProCGroups.FiniteGroupClass.{u}}
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
    (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
    (hExt : ProCGroups.FiniteGroupClass.ExtensionClosed C)
    {X : Type u} [TopologicalSpace X] [CompactSpace X] {x0 : X}
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
      [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
    {ι : X → F}
    (hF : IsEpimorphicallyPointedFreeProCGroupOn
      (C := C) X x0 F ι)
    (H : OpenSubgroup F) (x : X) {N : ℕ}
    (hN : 0 < N)
    (hpow : (ι x) ^ N ∈ (H : Subgroup F))
    (hmin : ∀ m : ℕ, 0 < m → m < N → (ι x) ^ m ∉ (H : Subgroup F)) :
    ∃ κ : OpenSubgroupRightQuotient H × X → ↥(H : Subgroup F),
      Continuous κ ∧
      (∀ q : OpenSubgroupRightQuotient H, κ (q, x0) = 1) ∧
      κ (openSubgroupRightCoset H (1 : F), x0) = 1 ∧
      (⟨(ι x) ^ N, hpow⟩ : ↥(H : Subgroup F)) ∈ Set.range κ ∧
      IsCompact (Set.range κ) ∧
      IsClosed (Set.range κ) ∧
      IsEpimorphicallyPointedFreeProCGroupOn
        (C := C)
        (Set.range κ)
        ⟨κ (openSubgroupRightCoset H (1 : F), x0),
          ⟨(openSubgroupRightCoset H (1 : F), x0), rfl⟩⟩
        ↥(H : Subgroup F) Subtype.val