-- Mathlib/Topology/Algebra/Category/ProfiniteGrp/Limits.lean
theorem denseRange_toLimit (P : ProfiniteGrp.{u}) : DenseRange (toLimit P)

Proof state:
case h.a
P : ProfiniteGrp.{u}
U : Set ↑(limit (P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp.{u} ProfiniteGrp.{u})).toProfinite.toTop
s :
  Set
    ((j : OpenNormalSubgroup ↑P.toProfinite.toTop) →
      ↑((P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc :
  (j : OpenNormalSubgroup ↑P.toProfinite.toTop) →
    ↑((P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp.{u} ProfiniteGrp.{u})
uDefaultSpec : spc ∈ s
J : Finset (OpenNormalSubgroup ↑P.toProfinite.toTop)
fJ :
  (a : OpenNormalSubgroup ↑P.toProfinite.toTop) →
    Set ↑((P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ spc a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑P.toProfinite.toTop := ⨅ j, ↑(↑j).toOpenSubgroup
hM : M.Normal
hMOpen : IsOpen ↑M
m : OpenNormalSubgroup ↑P.toProfinite.toTop := { toSubgroup := M, isOpen' := hMOpen, isNormal' := ⋯ }
origin : ↑P.toProfinite.toTop
horigin : (QuotientGroup.mk' M) origin = spc m
a : OpenNormalSubgroup ↑P.toProfinite.toTop
a_in_J : a ∈ ↑J
M_to_Na : m ⟶ a := ⋯.hom
⊢ (ConcreteCategory.hom (P.toFiniteQuotientFunctor.map M_to_Na)) (spc m) ∈ fJ a

Tactic:
exact Set.mem_of_eq_of_mem (hspc M_to_Na) (hJ1 a a_in_J).2

Result:
no goals

Proof state:
case intro.intro.intro.mk.intro.intro.intro
P : ProfiniteGrp.{u}
U : Set ↑(limit (P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp.{u} ProfiniteGrp.{u})).toProfinite.toTop
s :
  Set
    ((j : OpenNormalSubgroup ↑P.toProfinite.toTop) →
      ↑((P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc :
  (j : OpenNormalSubgroup ↑P.toProfinite.toTop) →
    ↑((P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp.{u} ProfiniteGrp.{u})
uDefaultSpec : spc ∈ s
J : Finset (OpenNormalSubgroup ↑P.toProfinite.toTop)
fJ :
  (a : OpenNormalSubgroup ↑P.toProfinite.toTop) →
    Set ↑((P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ spc a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑P.toProfinite.toTop := ⨅ j, ↑(↑j).toOpenSubgroup
hM : M.Normal
⊢ (U ∩ Set.range ⇑(Hom.hom P.toLimit)).Nonempty

Tactic:
have hMOpen : IsOpen (M : Set P) := by
  rw [Subgroup.coe_iInf]
  exact isOpen_iInter_of_finite fun i => i.1.1.isOpen'

Result:
case intro.intro.intro.mk.intro.intro.intro
P : ProfiniteGrp.{u}
U : Set ↑(limit (P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp.{u} ProfiniteGrp.{u})).toProfinite.toTop
s :
  Set
    ((j : OpenNormalSubgroup ↑P.toProfinite.toTop) →
      ↑((P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc :
  (j : OpenNormalSubgroup ↑P.toProfinite.toTop) →
    ↑((P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp.{u} ProfiniteGrp.{u})
uDefaultSpec : spc ∈ s
J : Finset (OpenNormalSubgroup ↑P.toProfinite.toTop)
fJ :
  (a : OpenNormalSubgroup ↑P.toProfinite.toTop) →
    Set ↑((P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ spc a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑P.toProfinite.toTop := ⨅ j, ↑(↑j).toOpenSubgroup
hM : M.Normal
hMOpen : IsOpen ↑M
⊢ (U ∩ Set.range ⇑(Hom.hom P.toLimit)).Nonempty

Proof state:
case h.a
P : ProfiniteGrp.{u}
U : Set ↑(limit (P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp.{u} ProfiniteGrp.{u})).toProfinite.toTop
s :
  Set
    ((j : OpenNormalSubgroup ↑P.toProfinite.toTop) →
      ↑((P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc :
  (j : OpenNormalSubgroup ↑P.toProfinite.toTop) →
    ↑((P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp.{u} ProfiniteGrp.{u})
uDefaultSpec : spc ∈ s
J : Finset (OpenNormalSubgroup ↑P.toProfinite.toTop)
fJ :
  (a : OpenNormalSubgroup ↑P.toProfinite.toTop) →
    Set ↑((P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ spc a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑P.toProfinite.toTop := ⨅ j, ↑(↑j).toOpenSubgroup
hM : M.Normal
hMOpen : IsOpen ↑M
m : OpenNormalSubgroup ↑P.toProfinite.toTop := { toSubgroup := M, isOpen' := hMOpen, isNormal' := ⋯ }
origin : ↑P.toProfinite.toTop
horigin : (QuotientGroup.mk' M) origin = spc m
a : OpenNormalSubgroup ↑P.toProfinite.toTop
a_in_J : a ∈ ↑J
M_to_Na : m ⟶ a := ⋯.hom
⊢ (Hom.hom ((P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).map M_to_Na))
      (↑((Hom.hom P.toLimit) origin) m) ∈
    fJ a

Tactic:
show (P.toFiniteQuotientFunctor.map M_to_Na) (QuotientGroup.mk' M origin) ∈ _

Result:
case h.a
P : ProfiniteGrp.{u}
U : Set ↑(limit (P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp.{u} ProfiniteGrp.{u})).toProfinite.toTop
s :
  Set
    ((j : OpenNormalSubgroup ↑P.toProfinite.toTop) →
      ↑((P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc :
  (j : OpenNormalSubgroup ↑P.toProfinite.toTop) →
    ↑((P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp.{u} ProfiniteGrp.{u})
uDefaultSpec : spc ∈ s
J : Finset (OpenNormalSubgroup ↑P.toProfinite.toTop)
fJ :
  (a : OpenNormalSubgroup ↑P.toProfinite.toTop) →
    Set ↑((P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ spc a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑P.toProfinite.toTop := ⨅ j, ↑(↑j).toOpenSubgroup
hM : M.Normal
hMOpen : IsOpen ↑M
m : OpenNormalSubgroup ↑P.toProfinite.toTop := { toSubgroup := M, isOpen' := hMOpen, isNormal' := ⋯ }
origin : ↑P.toProfinite.toTop
horigin : (QuotientGroup.mk' M) origin = spc m
a : OpenNormalSubgroup ↑P.toProfinite.toTop
a_in_J : a ∈ ↑J
M_to_Na : m ⟶ a := ⋯.hom
⊢ (ConcreteCategory.hom (P.toFiniteQuotientFunctor.map M_to_Na)) ((QuotientGroup.mk' M) origin) ∈ fJ a