-- 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.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
m : OpenNormalSubgroup ↑P.toProfinite.toTop := { toSubgroup := M, isOpen' := hMOpen, isNormal' := ⋯ }
origin : ↑P.toProfinite.toTop
horigin : (QuotientGroup.mk' M) origin = spc m
⊢ (U ∩ Set.range ⇑(Hom.hom P.toLimit)).Nonempty

Tactic:
use (toLimit P) origin

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

Proof state:
P : ProfiniteGrp.{u}
⊢ DenseRange ⇑(Hom.hom P.toLimit)

Tactic:
apply dense_iff_inter_open.mpr

Result:
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

Proof state:
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
⊢ IsOpen (⋂ i, ↑↑(↑i).toOpenSubgroup)

Tactic:
exact isOpen_iInter_of_finite fun i => i.1.1.isOpen'

Result:
no goals

Proof state:
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
⊢ IsOpen ↑M

Tactic:
rw [Subgroup.coe_iInf]

Result:
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
⊢ IsOpen (⋂ i, ↑↑(↑i).toOpenSubgroup)