-- 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
M : Subgroup ↑P.toProfinite.toTop := ⨅ j, ↑(↑j).toOpenSubgroup
hM : M.Normal
hMOpen : IsOpen ↑M
m : OpenNormalSubgroup ↑P.toProfinite.toTop := { toSubgroup := M, isOpen' := hMOpen, isNormal' := ⋯ }
⊢ (U ∩ Set.range ⇑(Hom.hom P.toLimit)).Nonempty

Tactic:
rcases QuotientGroup.mk'_surjective M (spc m) with ⟨origin, horigin⟩

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

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

Tactic:
rw [← hsv]

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 ∈ Subtype.val ⁻¹' s

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)) ((QuotientGroup.mk' M) origin) ∈ fJ a

Tactic:
rw [horigin]

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)) (spc m) ∈ fJ a