QuotientGeneratorConvergingPairs.lean

structure QuotientGeneratorConvergingPair where
  /-- The subgroup used to form the quotient carrying the generator family. -/
  N : Subgroup G
  /-- The quotienting subgroup is normal. -/
  normal_N : N.Normal
  /-- The quotienting subgroup is closed, so the quotient has the intended profinite topology. -/
  closed_N : IsClosed (N : Set G)
  /-- The distinguished generator set in `G ⧸ N`. -/
  Y : Set (G ⧸ N)
  /-- The quotient identity is excluded from the distinguished generator set. -/
  subset_compl : Y ⊆ ({1} : Set (G ⧸ N))ᶜ
  /-- The generator set converges to the quotient identity along open subgroups. -/
  converges : ConvergesToOneAlongOpenSubgroups (G := G ⧸ N) Y
  /-- The distinguished set topologically generates the entire quotient `G ⧸ N`. -/
  generates : TopologicallyGenerates (G := G ⧸ N) Y

def QuotientGeneratorConvergingPair.sourceSet
    (A : QuotientGeneratorConvergingPair (G := G)) :
    Set (G ⧸ A.N)

abbrev QuotientGeneratorConvergingPair.Source
    (A : QuotientGeneratorConvergingPair (G := G))

instance instTopologicalSpaceQuotientGeneratorConvergingPairSource
    (A : QuotientGeneratorConvergingPair (G := G)) :
    TopologicalSpace A.Source

def QuotientGeneratorConvergingPair.sourceOne
    (A : QuotientGeneratorConvergingPair (G := G)) : A.Source

def QuotientGeneratorConvergingPair.sourceOfY
    (A : QuotientGeneratorConvergingPair (G := G)) (y : A.Y) : A.Source

theorem QuotientGeneratorConvergingPair.source_cases
    (A : QuotientGeneratorConvergingPair (G := G)) (x : A.Source) :
    x = A.sourceOne ∨ ∃ y : A.Y, x = A.sourceOfY y

def QuotientGeneratorConvergingPair.yImage
    (A B : QuotientGeneratorConvergingPair (G := G))
    (σ : A.Source → G ⧸ B.N) : Set (G ⧸ B.N)

def QuotientGeneratorConvergingPair.Le
    (A B : QuotientGeneratorConvergingPair (G := G)) : Prop

instance instLEQuotientGeneratorConvergingPair :
    LE (QuotientGeneratorConvergingPair (G := G)) where
  le := QuotientGeneratorConvergingPair.Le

instance instPreorderQuotientGeneratorConvergingPair :
    Preorder (QuotientGeneratorConvergingPair (G := G)) where
  le_refl A := by
    refine ⟨le_rfl, Subtype.val, ?_, ?_, rfl, ?_, ?_⟩
    · change Continuous (fun x : A.Source => (x : G ⧸ A.N))
      exact continuous_subtype_val
    · intro q
      simp only [leftQuotientProjection_id, id_eq]
    · intro y
      simp only [QuotientGeneratorConvergingPair.sourceOfY, Subtype.coe_prop]
    · simp only [QuotientGeneratorConvergingPair.yImage, QuotientGeneratorConvergingPair.sourceOfY,
  Subtype.range_coe_subtype, ofPred_mem_eq, sdiff_self, leftQuotientProjection_id, id_eq,
  ofPred_eq_eq_singleton, subset_singleton_iff, mem_empty_iff_false, IsEmpty.forall_iff,
      implies_true]
  le_trans A B C hAB hBC := by
    classical
    rcases hAB with ⟨hBA, σAB, hσABcont, hσABright, hσABone, hσABmem, hσABdiff⟩
    rcases hBC with ⟨hCB, σBC, hσBCcont, hσBCright, hσBCone, hσBCmem, hσBCdiff⟩
    let τ : A.Source → B.Source := fun x =>
      ⟨σAB x, by
        rcases A.source_cases x with h1 | ⟨y, rfl⟩
        · rw [h1]
          exact Or.inl hσABone
        · exact Or.inr (hσABmem y)⟩
    have hτcont : Continuous τ := by
      exact hσABcont.subtype_mk <| by
        intro x
        rcases A.source_cases x with h1 | ⟨y, rfl⟩
        · rw [h1]
          exact Or.inl hσABone
        · exact Or.inr (hσABmem y)
    have hτone : τ A.sourceOne = B.sourceOne := by
      apply Subtype.ext
      exact hσABone
    have hτofY (y : A.Y) :
        τ (A.sourceOfY y) = B.sourceOfY ⟨σAB (A.sourceOfY y), hσABmem y⟩ := by
      apply Subtype.ext
      rfl
    have hEqBC :
        ∀ (y : B.Y) {q : G ⧸ C.N},
          q ∈ C.Y →
          leftQuotientProjection (C.N) (B.N) hCB q = y.1 →
            q = σBC (B.sourceOfY y) := by
      intro y q hqY hqproj
      by_cases hqim : q ∈ B.yImage C σBC
      · rcases hqim with ⟨y', hy'Eq⟩
        have hproj' :
            leftQuotientProjection (C.N) (B.N) hCB q = y'.1 := by
          calc
            leftQuotientProjection (C.N) (B.N) hCB q =
                leftQuotientProjection (C.N) (B.N) hCB
                  (σBC (B.sourceOfY y')) := congrArg
                    (leftQuotientProjection (C.N) (B.N) hCB) hy'Eq.symm
            _ = y'.1 := by
              exact hσBCright (B.sourceOfY y')
        have hyEq : y' = y := by
          apply Subtype.ext
          exact hproj'.symm.trans hqproj
        simpa [hyEq] using hy'Eq.symm
      · have hker :
          leftQuotientProjection (C.N) (B.N) hCB q = 1 := hσBCdiff ⟨hqY, hqim⟩
        have hyne : y.1 ≠ 1 := by
          simpa using B.subset_compl y.2
        exact False.elim (hyne (hqproj.symm.trans hker))
    refine ⟨hCB.trans hBA, fun x => σBC (τ x), hσBCcont.comp hτcont, ?_, ?_, ?_, ?_⟩
    · intro x
      calc
        leftQuotientProjection (C.N) (A.N) (hCB.trans hBA) (σBC (τ x)) =
            leftQuotientProjection (B.N) (A.N) hBA
              (leftQuotientProjection (C.N) (B.N) hCB (σBC (τ x))) := by
                exact leftQuotientProjection_comp_apply_symm
                  (K := (C.N : Subgroup G)) (H := (B.N : Subgroup G))
                  (L := (A.N : Subgroup G)) hCB hBA (σBC (τ x))
        _ = leftQuotientProjection (B.N) (A.N) hBA ((τ x).1) := by
              rw [hσBCright (τ x)]
        _ = leftQuotientProjection (B.N) (A.N) hBA (σAB x) := by
              rfl
        _ = x.1 := hσABright x
    · simpa [hτone] using hσBCone
    · intro y
      let yB : B.Y := ⟨σAB (A.sourceOfY y), hσABmem y⟩
      simpa [hτofY, yB] using hσBCmem yB
    · intro q hq
      rcases hq with ⟨hqY, hqnotAC⟩
      by_cases hqimB : q ∈ B.yImage C σBC
      · rcases hqimB with ⟨z, hzEq⟩
        have hzNotInA : z.1 ∉ A.yImage B σAB := by
          intro hzInA
          rcases hzInA with ⟨y, hyEq⟩
          let yB : B.Y := ⟨σAB (A.sourceOfY y), hσABmem y⟩
          have hprojqz :
              leftQuotientProjection (C.N) (B.N) hCB q = z.1 := by
            calc
              leftQuotientProjection (C.N) (B.N) hCB q =
                  leftQuotientProjection (C.N) (B.N) hCB
                    (σBC (B.sourceOfY z)) := congrArg
                      (leftQuotientProjection (C.N) (B.N) hCB) hzEq.symm
              _ = z.1 := by
                exact hσBCright (B.sourceOfY z)
          have hprojq :
              leftQuotientProjection (C.N) (B.N) hCB q = yB.1 := by
            calc
              leftQuotientProjection (C.N) (B.N) hCB q = z.1 := hprojqz
              _ = yB.1 := by
                    simpa [yB] using hyEq.symm
          have hqEq : q = σBC (B.sourceOfY yB) := hEqBC yB hqY hprojq
          have hqInAC : q ∈ A.yImage C (fun x => σBC (τ x)) := by
            refine ⟨y, ?_⟩
            simpa [hτofY] using hqEq.symm
          exact hqnotAC hqInAC
        have hzProjA :
            leftQuotientProjection (B.N) (A.N) hBA z.1 = 1 :=
          hσABdiff ⟨z.2, hzNotInA⟩
        have hprojqB :
            leftQuotientProjection (C.N) (B.N) hCB q = z.1 := by
          calc
            leftQuotientProjection (C.N) (B.N) hCB q =
                leftQuotientProjection (C.N) (B.N) hCB
                  (σBC (B.sourceOfY z)) := congrArg
                    (leftQuotientProjection (C.N) (B.N) hCB) hzEq.symm
            _ = z.1 := by
              exact hσBCright (B.sourceOfY z)
        calc
          leftQuotientProjection (C.N) (A.N) (hCB.trans hBA) q =
              leftQuotientProjection (B.N) (A.N) hBA
                (leftQuotientProjection (C.N) (B.N) hCB q) := by
                  exact leftQuotientProjection_comp_apply_symm
                    (K := (C.N : Subgroup G)) (H := (B.N : Subgroup G))
                    (L := (A.N : Subgroup G)) hCB hBA q
          _ = leftQuotientProjection (B.N) (A.N) hBA z.1 := by
                rw [hprojqB]
          _ = 1 := hzProjA
      · have hprojqB :
          leftQuotientProjection (C.N) (B.N) hCB q = 1 := hσBCdiff ⟨hqY, hqimB⟩
        calc
          leftQuotientProjection (C.N) (A.N) (hCB.trans hBA) q =
              leftQuotientProjection (B.N) (A.N) hBA
                (leftQuotientProjection (C.N) (B.N) hCB q) := by
                  exact leftQuotientProjection_comp_apply_symm
                    (K := (C.N : Subgroup G)) (H := (B.N : Subgroup G))
                    (L := (A.N : Subgroup G)) hCB hBA q
          _ = leftQuotientProjection (B.N) (A.N) hBA 1 := by
                rw [hprojqB]
          _ = 1 := by
                rfl

theorem QuotientGeneratorConvergingPair.le_hBA
    {A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B) :
    B.N ≤ A.N

def QuotientGeneratorConvergingPair.le_map
    {A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B) :
    A.Source → G ⧸ B.N

theorem QuotientGeneratorConvergingPair.le_map_continuous
    {A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B) :
    Continuous (A.le_map hAB)

theorem QuotientGeneratorConvergingPair.le_map_right
    {A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B)
    (x : A.Source) :
    leftQuotientProjection (B.N) (A.N) (A.le_hBA hAB) (A.le_map hAB x) = x.1

theorem QuotientGeneratorConvergingPair.le_map_one
    {A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B) :
    A.le_map hAB A.sourceOne = 1

theorem QuotientGeneratorConvergingPair.le_map_mem
    {A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B)
    (y : A.Y) :
    A.le_map hAB (A.sourceOfY y) ∈ B.Y

theorem QuotientGeneratorConvergingPair.le_map_diff
    {A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B) :
    B.Y \ A.yImage B (A.le_map hAB) ⊆
      {q : G ⧸ B.N |
        leftQuotientProjection (B.N) (A.N) (A.le_hBA hAB) q = 1}

theorem QuotientGeneratorConvergingPair.eq_le_map_of_mem_of_proj_eq
    {A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B)
    (y : A.Y) {q : G ⧸ B.N}
    (hqY : q ∈ B.Y)
    (hqproj : leftQuotientProjection (B.N) (A.N) (A.le_hBA hAB) q = y.1) :
    q = A.le_map hAB (A.sourceOfY y)

theorem QuotientGeneratorConvergingPair.le_map_compat
    {A B C : QuotientGeneratorConvergingPair (G := G)}
    (hAB : A ≤ B) (hAC : A ≤ C) (hBC : B ≤ C)
    (y : A.Y) :
    leftQuotientProjection (C.N) (B.N) (B.le_hBA hBC)
      (A.le_map hAC (A.sourceOfY y)) =
      A.le_map hAB (A.sourceOfY y)

theorem ConvergesToOneAlongOpenSubgroups.range_subtype_pointed
    {H : Type v} [Group H] [TopologicalSpace H]
    {X : Set G}
    {f : ↥((({1} : Set G) ∪ X)) → H}
    (hf : Continuous f)
    (hf1 : f ⟨1, Or.inl rfl⟩ = 1)
    (hX : ConvergesToOneAlongOpenSubgroups (G := G) X) :
    ConvergesToOneAlongOpenSubgroups (G := H)
      (Set.range fun x : X => f ⟨x.1, Or.inr x.2⟩) := by
  let S : Set G := ({1} : Set G) ∪ X
  let g : X → H := fun x => f ⟨x.1, Or.inr x.2⟩
  intro U
  have hpre : IsOpen (f ⁻¹' (U : Set H)) :=
    (openSubgroup_isOpen (G := H) U).preimage hf
  have h1pre : (⟨1, Or.inl rfl⟩ : ↥S) ∈ f ⁻¹' (U : Set H) := by
    change f ⟨1, Or.inl rfl⟩ ∈ U
    rw [hf1]
    exact U.one_mem'
  rcases isOpen_induced_iff.mp hpre with ⟨W, hWopen, hWeq⟩
  have h1W : (1 : G) ∈ W := by
    have : (⟨1, Or.inl rfl⟩ : ↥S) ∈ Subtype.val ⁻¹' W := by
      exact hWeq.symm ▸ h1pre
    simpa using this
  rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hWopen h1W with ⟨V, hVW⟩
  have hsubset :
      Set.range g \ (U : Set H) ⊆ g '' {x : X | (x : G) ∉ (V : Set G)} := by
    intro y hy
    rcases hy with ⟨hyY, hyU⟩
    rcases hyY with ⟨x, rfl⟩
    refine ⟨x, ?_, rfl⟩
    intro hxV
    have hxW : (x : G) ∈ W := hVW hxV
    have hxpre : (⟨x.1, Or.inr x.2⟩ : ↥S) ∈ Subtype.val ⁻¹' W := by
      change (x : G) ∈ W
      exact hxW
    have hxpreU : (⟨x.1, Or.inr x.2⟩ : ↥S) ∈ f ⁻¹' (U : Set H) := by
      exact hWeq ▸ hxpre
    have : g x ∈ (U : Set H) := by
      change f ⟨x.1, Or.inr x.2⟩ ∈ U
      exact hxpreU
    exact hyU this
  have hfinite_pre : {x : X | (x : G) ∉ (V : Set G)}.Finite := by
    let e : X ↪ G := ⟨Subtype.val, Subtype.val_injective⟩
    have hfinite : (X \ (V : Set G)).Finite := hX V.toOpenSubgroup
    have hfinite' : {x : X | e x ∈ X ∧ e x ∉ (V : Set G)}.Finite := by
      simpa [Set.preimage] using hfinite.preimage_embedding e
    have hEq : {x : X | e x ∈ X ∧ e x ∉ (V : Set G)} = {x : X | (x : G) ∉ (V : Set G)} := by
      ext x
      simp only [Function.Embedding.coeFn_mk, Subtype.coe_prop, SetLike.mem_coe, true_and,
          mem_ofPred_eq, e]
    exact hEq ▸ hfinite'
  exact hfinite_pre.image g |>.subset hsubset

theorem exists_quotientPair_le_openSubgroup_of_chain_iInf_le
    {c : Set (QuotientGeneratorConvergingPair (G := G))}
    (hc : IsChain (· ≤ ·) c) (hcne : c.Nonempty)
    (U : OpenSubgroup G)
    (hInf : iInf (fun p : c => p.1.N) ≤ (U : Subgroup G)) :
    ∃ p : c, p.1.N ≤ (U : Subgroup G) := by
  classical
  have hInter :
      (⋂ p : c, (((p.1.N : Subgroup G) : Set G))) ⊆ ((U : Subgroup G) : Set G) := by
    intro x hx
    exact hInf (by simpa [Subgroup.mem_iInf] using hx)
  rcases finite_iInter_subgroup_subset_openSubgroup (G := G)
      (H := fun p : c => p.1.N)
      (hclosed := fun p => p.1.closed_N)
      U hInter with ⟨s, hs⟩
  by_cases hsne : s.Nonempty
  · have hc' : IsChain (· ≤ ·) (Set.univ : Set c) := by
      intro a ha b hb hne
      have hne' : (a : QuotientGeneratorConvergingPair (G := G)) ≠ b := by
        intro h
        exact hne (Subtype.ext h)
      simpa using hc a.2 b.2 hne'
    rcases finite_subset_chain_has_upper hc' s (by intro z hz; simp only [mem_univ]) hsne with
        ⟨m, hm, hmax⟩
    refine ⟨m, ?_⟩
    intro x hx
    have hx' :
        x ∈ ⋂ p ∈ s, (((p.1.N : Subgroup G) : Set G)) := by
      refine mem_iInter₂.2 ?_
      intro p hp
      exact (QuotientGeneratorConvergingPair.le_hBA (hmax p hp)) hx
    exact hs hx'
  · rcases hcne with ⟨p, hp⟩
    refine ⟨⟨p, hp⟩, ?_⟩
    have htop : ((⊤ : Subgroup G) : Set G) ⊆ ((U : Subgroup G) : Set G) := by
      have :
          (⋂ p ∈ s, (((p.1.N : Subgroup G) : Set G))) ⊆ ((U : Subgroup G) : Set G) := hs
      simpa [Finset.not_nonempty_iff_eq_empty.mp hsne] using this
    intro x hx
    exact htop (by simp only [Subgroup.coe_top, mem_univ])

theorem quotientGeneratorPair_exists_liftToInf
    {c : Set (QuotientGeneratorConvergingPair (G := G))}
    (hc : IsChain (· ≤ ·) c) (a : c) :
    let K : Subgroup G := iInf fun p : c => p.1.N
    letI : K.Normal := Subgroup.normal_iInf_normal fun p : c => p.1.normal_N
    ∃ σ : a.1.Source → G ⧸ K,
      Continuous σ ∧
      (∀ b : c, ∀ hab : a.1 ≤ b.1,
        leftQuotientProjection K b.1.N
          (iInf_le (fun p : c => p.1.N) b) ∘ σ =
          a.1.le_map hab) ∧
      σ a.1.sourceOne = 1 := by
  classical
  intro K
  have : K.Normal := Subgroup.normal_iInf_normal fun p : c => p.1.normal_N
  let Tail := {b : c // a.1 ≤ b.1}
  have : Nonempty Tail := ⟨⟨a, le_rfl⟩⟩
  let L : Tail → ClosedSubgroup G := fun b =>
    ⟨b.1.1.N, b.1.1.closed_N⟩
  have hL : ∀ {i j : Tail}, i ≤ j → (L j : Subgroup G) ≤ (L i : Subgroup G) := by
    intro i j hij
    exact QuotientGeneratorConvergingPair.le_hBA hij
  have hdir : Directed (· ≤ ·) (id : Tail → Tail) := by
    intro i j
    by_cases hij : i ≤ j
    · exact ⟨j, hij, le_rfl⟩
    · have hji : j ≤ i := by
        by_cases hEq : i = j
        · exact hEq ▸ le_rfl
        · rcases hc i.1.2 j.1.2 (by
            intro h
            exact hEq (Subtype.ext (Subtype.ext h))) with hij' | hji'
          · exact False.elim (hij hij')
          · exact hji'
      exact ⟨i, le_rfl, hji⟩
  let η : ∀ b : Tail, a.1.Source → G ⧸ (L b : Subgroup G) := fun b =>
    a.1.le_map b.2
  have hηcont : ∀ b : Tail, Continuous (η b) := by
    intro b
    exact a.1.le_map_continuous b.2
  have hηcompat : ∀ {i j : Tail} (hij : i ≤ j),
      leftQuotientProjection (L j : Subgroup G) (L i : Subgroup G) (hL hij) ∘ η j = η i := by
    intro i j hij
    funext x
    rcases a.1.source_cases x with rfl | ⟨y, rfl⟩
    · have h1j : η j a.1.sourceOne = 1 := by
        change a.1.le_map j.2 a.1.sourceOne = 1
        exact a.1.le_map_one j.2
      have h1i : η i a.1.sourceOne = 1 := by
        change a.1.le_map i.2 a.1.sourceOne = 1
        exact a.1.le_map_one i.2
      calc
        (leftQuotientProjection (L j : Subgroup G) (L i : Subgroup G) (hL hij) ∘ η j)
            a.1.sourceOne
            = leftQuotientProjection (L j : Subgroup G) (L i : Subgroup G) (hL hij)
                (η j a.1.sourceOne) := by
                    simp only [Function.comp]
        _ = leftQuotientProjection (L j : Subgroup G) (L i : Subgroup G) (hL hij) 1 := by
              rw [h1j]
        _ = 1 := by rfl
        _ = η i a.1.sourceOne := by rw [h1i]
    · simpa [η] using a.1.le_map_compat i.2 j.2 hij y
  have hηone : ∀ b : Tail, η b a.1.sourceOne = 1 := by
    intro b
    change a.1.le_map b.2 a.1.sourceOne = 1
    exact a.1.le_map_one b.2
  obtain ⟨ηinf, hηinf_continuous, hηinf_fac, hηinf_one⟩ :=
    exists_continuous_leftQuotient_lift_of_directed
      (G := G) L hL hdir η hηcont hηcompat a.1.sourceOne hηone
  let H : Subgroup G := ((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G)
  have hKeq : H = K := by
    apply le_antisymm
    · refine le_iInf ?_
      intro p
      by_cases hap : a.1 ≤ p.1
      · exact iInf_le (fun b : Tail => (L b : Subgroup G)) ⟨p, hap⟩
      · have hKa :
          H ≤ a.1.N :=
          iInf_le (fun b : Tail => (L b : Subgroup G)) ⟨a, le_rfl⟩
        by_cases hEq : p = a
        · simpa [K, hEq] using hKa
        · rcases hc p.2 a.2 (by
            intro h
            exact hEq (Subtype.ext h)) with hpa | hap'
          · exact hKa.trans (QuotientGeneratorConvergingPair.le_hBA hpa)
          · exact False.elim (hap hap')
    · refine le_iInf ?_
      intro b
      exact iInf_le (fun p : c => p.1.N) b.1
  have : H.Normal := by
    exact Subgroup.normal_iInf_normal fun b : Tail => b.1.1.normal_N
  have hGoal :
      ∃ σ : a.1.Source → G ⧸ H,
        Continuous σ ∧
        (∀ b : c, ∀ hab : a.1 ≤ b.1,
          leftQuotientProjection H b.1.N
              (closedSubgroup_sInf_le (L := L) ⟨b, hab⟩) ∘ σ =
            a.1.le_map hab) ∧
        σ a.1.sourceOne = 1 := by
    refine ⟨ηinf, hηinf_continuous, ?_, hηinf_one⟩
    intro b hab
    simpa [Tail, L, η] using hηinf_fac ⟨b, hab⟩
  have hGoal' :
      ∃ σ : a.1.Source → G ⧸ H,
        Continuous σ ∧
        (∀ b : c, ∀ hab : a.1 ≤ b.1,
          leftQuotientProjection H b.1.N
              (hKeq.trans_le (iInf_le (fun p : c => p.1.N) b)) ∘ σ =
            a.1.le_map hab) ∧
        σ a.1.sourceOne = 1 := by
    rcases hGoal with ⟨σ, hσcont, hσfac, hσone⟩
    refine ⟨σ, hσcont, ?_, hσone⟩
    intro b hab
    simpa using hσfac b hab
  change
    ∃ σ : a.1.Source → G ⧸ K,
      Continuous σ ∧
      (∀ b : c, ∀ hab : a.1 ≤ b.1,
        leftQuotientProjection K b.1.N
          (iInf_le (fun p : c => p.1.N) b) ∘ σ =
          a.1.le_map hab) ∧
      σ a.1.sourceOne = 1
  let Data : Type _ := { J : Subgroup G // J.Normal ∧ ∀ b : c, J ≤ b.1.N }
  let P : Data → Prop := fun d =>
    letI : d.1.Normal := d.2.1
    ∃ σ : a.1.Source → G ⧸ d.1,
      Continuous σ ∧
      (∀ b : c, ∀ hab : a.1 ≤ b.1,
        leftQuotientProjection d.1 b.1.N (d.2.2 b) ∘ σ =
          a.1.le_map hab) ∧
      σ a.1.sourceOne = 1
  let dH : Data :=
    ⟨H, ⟨inferInstance, fun b => hKeq.trans_le (iInf_le (fun p : c => p.1.N) b)⟩⟩
  let dK : Data :=
    ⟨K, ⟨inferInstance, fun b => iInf_le (fun p : c => p.1.N) b⟩⟩
  have hd : dH = dK := by
    apply Subtype.ext
    exact hKeq
  have hPdH : P dH := by
    simpa [P, dH] using hGoal'
  have hPdK : P dK := by
    exact Eq.mp (congrArg P hd) hPdH
  simpa [P, dK] using hPdK

def quotientGeneratorPairTop :
    QuotientGeneratorConvergingPair (G := G) where
  N := ⊤
  normal_N := by infer_instance
  closed_N := isClosed_univ
  Y := ∅
  subset_compl := by intro q hq; simp only [mem_empty_iff_false] at hq
  converges := by intro U; simp only [empty_sdiff, finite_empty]
  generates := by
    classical
    rw [TopologicallyGenerates]
    apply top_unique
    intro q hq
    rcases Quotient.exists_rep q with ⟨g, rfl⟩
    have hg1 : QuotientGroup.mk' (⊤ : Subgroup G) g = (1 : G ⧸ (⊤ : Subgroup G)) := by
      exact (QuotientGroup.eq_one_iff (N := (⊤ : Subgroup G)) g).2 (by simp only [Subgroup.mem_top])
    have hbot :
        QuotientGroup.mk' (⊤ : Subgroup G) g ∈ (⊥ : Subgroup (G ⧸ (⊤ : Subgroup G))) := by
      change QuotientGroup.mk' (⊤ : Subgroup G) g = (1 : G ⧸ (⊤ : Subgroup G))
      exact hg1
    simpa [Subgroup.closure_eq] using
      (Subgroup.le_topologicalClosure (⊥ : Subgroup (G ⧸ (⊤ : Subgroup G))) hbot)

theorem quotientGeneratorPair_exists_strictExtension
    (p : QuotientGeneratorConvergingPair (G := G))
    (hne : p.N ≠ ⊥) :
    ∃ p' : QuotientGeneratorConvergingPair (G := G), p ≤ p' ∧ ¬ p' ≤ p

theorem closedNormalQuotientSection_bot_eq
    (hbotClosed : IsClosed (((⊥ : Subgroup G) : Set G))) :
    closedNormalQuotientSection (G := G)
      (N := (⊥ : Subgroup G)) hbotClosed =
      (quotientBotContinuousMulEquiv (G := G)).symm

def QuotientGeneratorConvergingPair.toAmbientSet
    (p : QuotientGeneratorConvergingPair (G := G)) : Set G

theorem QuotientGeneratorConvergingPair.toAmbientSet_generatesAndConvergesToOneAlongOpenSubgroups
    (p : QuotientGeneratorConvergingPair (G := G))
    (hbot : p.N = ⊥) :
    GeneratesAndConvergesToOneAlongOpenSubgroups (G := G) p.toAmbientSet

theorem quotientGeneratorPair_exists_upperBound_of_chain
    (c : Set (QuotientGeneratorConvergingPair (G := G)))
    (hc : IsChain (· ≤ ·) c) (hcn : c.Nonempty) :
    ∃ ub : QuotientGeneratorConvergingPair (G := G), ∀ a ∈ c, a ≤ ub

theorem exists_generatorsConvergingToOne :
    ∃ X : Set G, GeneratesAndConvergesToOneAlongOpenSubgroups (G := G) X

theorem GeneratesAndConvergesToOneAlongOpenSubgroups.image_of_continuousSurjective
    {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (f : G →* H) (hf : Continuous f) (hfsurj : Function.Surjective f)
    {X : Set G} (hX : GeneratesAndConvergesToOneAlongOpenSubgroups (G := G) X) :
    GeneratesAndConvergesToOneAlongOpenSubgroups (G := H) (f '' X)

theorem GeneratesAndConvergesToOneAlongOpenSubgroups.image_of_continuousMulEquiv
    {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (e : G ≃ₜ* H) {X : Set G}
    (hX : GeneratesAndConvergesToOneAlongOpenSubgroups (G := G) X) :
    GeneratesAndConvergesToOneAlongOpenSubgroups (G := H) (e '' X)

theorem ConvergesToOneAlongOpenSubgroups.image_of_continuousMulEquiv_iff
    {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
    (e : G ≃ₜ* H) {X : Set G} :
    ConvergesToOneAlongOpenSubgroups (G := H) (e '' X) ↔ ConvergesToOneAlongOpenSubgroups (G :=
        G) X

theorem GeneratesAndConvergesToOneAlongOpenSubgroups.image_of_continuousMulEquiv_iff
    {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
    (e : G ≃ₜ* H) {X : Set G} :
    GeneratesAndConvergesToOneAlongOpenSubgroups (G := H) (e '' X) ↔
        GeneratesAndConvergesToOneAlongOpenSubgroups (G := G) X

theorem topologicalRank_eq_of_continuousMulEquiv
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
    (e : G ≃ₜ* H) :
    topologicalRank G = topologicalRank H