-- 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
⊢ ↑((Hom.hom P.toLimit) origin) a ∈ fJ a

Tactic:
rw [← (P.toLimit origin).property M_to_Na]

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
⊢ (Hom.hom ((P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).map M_to_Na))
      (↑((Hom.hom P.toLimit) origin) m) ∈
    fJ a

Proof state:
P : ProfiniteGrp.{u}
⊢ ∀ (U : Set ↑(limit (P.toFiniteQuotientFunctor ⋙ forget₂ FiniteGrp.{u} ProfiniteGrp.{u})).toProfinite.toTop),
    IsOpen U → U.Nonempty → (U ∩ Set.range ⇑(Hom.hom P.toLimit)).Nonempty

Tactic:
rintro U ⟨s, hsO, hsv⟩ ⟨⟨spc, hspc⟩, uDefaultSpec⟩

Result:
case intro.intro.intro.mk
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, hspc⟩ ∈ U
⊢ (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
⊢ ↑((Hom.hom P.toLimit) origin) a ∈ fJ a

Tactic:
let M_to_Na : m ⟶ a := (iInf_le (fun (j : J) => j.1.1.1) ⟨a, a_in_J⟩).hom

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
⊢ ↑((Hom.hom P.toLimit) origin) a ∈ fJ a