-- Mathlib/Topology/Algebra/Category/ProfiniteGrp/Limits.lean
lemma toLimit_fun_continuous (P : ProfiniteGrp.{u}) : Continuous (toLimit_fun P)

Proof state:
case h.e'_3.h
P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
s : Set ↑((forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj (P.toFiniteQuotientFunctor.obj H)).toProfinite.toTop
a✝ : IsOpen s
i : ↑P.toProfinite.toTop ⧸ ↑H.toOpenSubgroup
x✝ : i ∈ s
x : ↑P.toProfinite.toTop
⊢ ↑x = i ↔ x ∈ Quotient.out i • (↑H.toOpenSubgroup).carrier

Tactic:
nth_rw 1 [← QuotientGroup.out_eq' i, eq_comm, QuotientGroup.eq]

Result:
case h.e'_3.h
P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
s : Set ↑((forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj (P.toFiniteQuotientFunctor.obj H)).toProfinite.toTop
a✝ : IsOpen s
i : ↑P.toProfinite.toTop ⧸ ↑H.toOpenSubgroup
x✝ : i ∈ s
x : ↑P.toProfinite.toTop
⊢ (Quotient.out i)⁻¹ * x ∈ ↑H.toOpenSubgroup ↔ x ∈ Quotient.out i • (↑H.toOpenSubgroup).carrier

Proof state:
case h.e'_3.h
P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
s : Set ↑((forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj (P.toFiniteQuotientFunctor.obj H)).toProfinite.toTop
a✝ : IsOpen s
i : ↑P.toProfinite.toTop ⧸ ↑H.toOpenSubgroup
x✝ : i ∈ s
x : ↑P.toProfinite.toTop
⊢ x ∈ QuotientGroup.mk ⁻¹' {i} ↔ x ∈ Quotient.out i • (↑H.toOpenSubgroup).carrier

Tactic:
simp only [Set.mem_preimage, Set.mem_singleton_iff]

Result:
case h.e'_3.h
P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
s : Set ↑((forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj (P.toFiniteQuotientFunctor.obj H)).toProfinite.toTop
a✝ : IsOpen s
i : ↑P.toProfinite.toTop ⧸ ↑H.toOpenSubgroup
x✝ : i ∈ s
x : ↑P.toProfinite.toTop
⊢ ↑x = i ↔ x ∈ Quotient.out i • (↑H.toOpenSubgroup).carrier

Proof state:
case h.e'_3
P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
s : Set ↑((forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj (P.toFiniteQuotientFunctor.obj H)).toProfinite.toTop
a✝ : IsOpen s
i : ↑P.toProfinite.toTop ⧸ ↑H.toOpenSubgroup
x✝ : i ∈ s
⊢ QuotientGroup.mk ⁻¹' {i} = Quotient.out i • (↑H.toOpenSubgroup).carrier

Tactic:
ext x

Result:
case h.e'_3.h
P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
s : Set ↑((forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj (P.toFiniteQuotientFunctor.obj H)).toProfinite.toTop
a✝ : IsOpen s
i : ↑P.toProfinite.toTop ⧸ ↑H.toOpenSubgroup
x✝ : i ∈ s
x : ↑P.toProfinite.toTop
⊢ x ∈ QuotientGroup.mk ⁻¹' {i} ↔ x ∈ Quotient.out i • (↑H.toOpenSubgroup).carrier

Proof state:
P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
⊢ Continuous fun a => ↑a

Tactic:
apply Continuous.mk

Result:
case isOpen_preimage
P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
⊢ ∀ (s : Set ↑((forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj (P.toFiniteQuotientFunctor.obj H)).toProfinite.toTop),
    IsOpen s → IsOpen ((fun a => ↑a) ⁻¹' s)

Proof state:
P : ProfiniteGrp.{u}
⊢ ∀ (i : OpenNormalSubgroup ↑P.toProfinite.toTop), Continuous fun a => (Subtype.val ∘ ⇑P.toLimit_fun) a i

Tactic:
intro H

Result:
P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
⊢ Continuous fun a => (Subtype.val ∘ ⇑P.toLimit_fun) a H

Proof state:
case isOpen_preimage
P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
⊢ ∀ (s : Set ↑((forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj (P.toFiniteQuotientFunctor.obj H)).toProfinite.toTop),
    IsOpen s → IsOpen ((fun a => ↑a) ⁻¹' s)

Tactic:
intro s _

Result:
case isOpen_preimage
P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
s : Set ↑((forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj (P.toFiniteQuotientFunctor.obj H)).toProfinite.toTop
a✝ : IsOpen s
⊢ IsOpen ((fun a => ↑a) ⁻¹' s)

Proof state:
case h.e'_3.h
P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
s : Set ↑((forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj (P.toFiniteQuotientFunctor.obj H)).toProfinite.toTop
a✝ : IsOpen s
i : ↑P.toProfinite.toTop ⧸ ↑H.toOpenSubgroup
x✝ : i ∈ s
x : ↑P.toProfinite.toTop
⊢ (Quotient.out i)⁻¹ * x ∈ ↑H.toOpenSubgroup ↔ x ∈ Quotient.out i • (↑H.toOpenSubgroup).carrier

Tactic:
exact Iff.symm (Set.mem_smul_set_iff_inv_smul_mem)

Result:
no goals

Proof state:
case isOpen_preimage
P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
s : Set ↑((forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj (P.toFiniteQuotientFunctor.obj H)).toProfinite.toTop
a✝ : IsOpen s
⊢ IsOpen ((fun a => ↑a) ⁻¹' s)

Tactic:
rw [← (Set.biUnion_preimage_singleton QuotientGroup.mk s)]

Result:
case isOpen_preimage
P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
s : Set ↑((forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj (P.toFiniteQuotientFunctor.obj H)).toProfinite.toTop
a✝ : IsOpen s
⊢ IsOpen (⋃ y ∈ s, QuotientGroup.mk ⁻¹' {y})

Proof state:
P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
⊢ Continuous fun a => (Subtype.val ∘ ⇑P.toLimit_fun) a H

Tactic:
dsimp only [Functor.comp_obj, CompHausLike.coe_of, Functor.comp_map,
  CompHausLike.toCompHausLike_map, CompHausLike.compHausLikeToTop_map, Set.mem_setOf_eq,
  toLimit_fun, MonoidHom.coe_mk, OneHom.coe_mk, Function.comp_apply]

Result:
P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
⊢ Continuous fun a => ↑a

Proof state:
case isOpen_preimage
P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
s : Set ↑((forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj (P.toFiniteQuotientFunctor.obj H)).toProfinite.toTop
a✝ : IsOpen s
⊢ IsOpen (⋃ y ∈ s, QuotientGroup.mk ⁻¹' {y})

Tactic:
refine isOpen_iUnion (fun i ↦ isOpen_iUnion (fun _ ↦ ?_))

Result:
case isOpen_preimage
P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
s : Set ↑((forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj (P.toFiniteQuotientFunctor.obj H)).toProfinite.toTop
a✝ : IsOpen s
i : ↑P.toProfinite.toTop ⧸ ↑H.toOpenSubgroup
x✝ : i ∈ s
⊢ IsOpen (QuotientGroup.mk ⁻¹' {i})

Proof state:
case isOpen_preimage
P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
s : Set ↑((forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj (P.toFiniteQuotientFunctor.obj H)).toProfinite.toTop
a✝ : IsOpen s
i : ↑P.toProfinite.toTop ⧸ ↑H.toOpenSubgroup
x✝ : i ∈ s
⊢ IsOpen (QuotientGroup.mk ⁻¹' {i})

Tactic:
convert IsOpen.leftCoset H.toOpenSubgroup.isOpen' (Quotient.out i)

Result:
case h.e'_3
P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
s : Set ↑((forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).obj (P.toFiniteQuotientFunctor.obj H)).toProfinite.toTop
a✝ : IsOpen s
i : ↑P.toProfinite.toTop ⧸ ↑H.toOpenSubgroup
x✝ : i ∈ s
⊢ QuotientGroup.mk ⁻¹' {i} = Quotient.out i • (↑H.toOpenSubgroup).carrier

Proof state:
P : ProfiniteGrp.{u}
⊢ Continuous ⇑P.toLimit_fun

Tactic:
apply continuous_induced_rng.mpr (continuous_pi _)

Result:
P : ProfiniteGrp.{u}
⊢ ∀ (i : OpenNormalSubgroup ↑P.toProfinite.toTop), Continuous fun a => (Subtype.val ∘ ⇑P.toLimit_fun) a i