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

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
⊢ (U ∩ Set.range ⇑(Hom.hom P.toLimit)).Nonempty

Tactic:
let M := iInf (fun (j : J) => j.1.1.1)

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
⊢ (U ∩ Set.range ⇑(Hom.hom P.toLimit)).Nonempty

Proof state:
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 ∈ s
⊢ (U ∩ Set.range ⇑(Hom.hom P.toLimit)).Nonempty

Tactic:
rcases (isOpen_pi_iff.mp hsO) _ uDefaultSpec with ⟨J, fJ, hJ1, hJ2⟩

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
⊢ (U ∩ Set.range ⇑(Hom.hom P.toLimit)).Nonempty

Proof state:
case h
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
⊢ (Hom.hom P.toLimit) origin ∈ U ∩ Set.range ⇑(Hom.hom P.toLimit)

Tactic:
refine ⟨?_, origin, rfl⟩

Result:
case h
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
⊢ (Hom.hom P.toLimit) origin ∈ U