-- Mathlib/Topology/Category/TopCat/Limits/Products.lean
theorem induced_of_isLimit {F : J ⥤ TopCat.{max v u}} (C : Cone F) (hC : IsLimit C) :
    C.pt.str = ⨅ j, (F.obj j).str.induced (C.π.app j)

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
homeo : ↑C.pt ≃ₜ ↑(limitConeInfi F).pt := homeoOfIso (hC.conePointUniqueUpToIso (limitConeInfiIsLimit F))
⊢ ⨅ i, induced ((Types.limitCone (F ⋙ forget TopCat)).π.app i ∘ ⇑homeo) (F.obj i).str =
    ⨅ j, induced (⇑(ConcreteCategory.hom (C.π.app j))) (F.obj j).str

Tactic:
rfl

Result:
no goals

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
⊢ C.pt.str = ⨅ j, induced (⇑(ConcreteCategory.hom (C.π.app j))) (F.obj j).str

Tactic:
let homeo := homeoOfIso (hC.conePointUniqueUpToIso (limitConeInfiIsLimit F))

Result:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
homeo : ↑C.pt ≃ₜ ↑(limitConeInfi F).pt := homeoOfIso (hC.conePointUniqueUpToIso (limitConeInfiIsLimit F))
⊢ C.pt.str = ⨅ j, induced (⇑(ConcreteCategory.hom (C.π.app j))) (F.obj j).str

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
homeo : ↑C.pt ≃ₜ ↑(limitConeInfi F).pt := homeoOfIso (hC.conePointUniqueUpToIso (limitConeInfiIsLimit F))
⊢ induced (⇑homeo) (⨅ j, induced ((Types.limitCone (F ⋙ forget TopCat)).π.app j) (F.obj j).str) =
    ⨅ j, induced (⇑(ConcreteCategory.hom (C.π.app j))) (F.obj j).str

Tactic:
simp [induced_iInf, induced_compose]

Result:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
homeo : ↑C.pt ≃ₜ ↑(limitConeInfi F).pt := homeoOfIso (hC.conePointUniqueUpToIso (limitConeInfiIsLimit F))
⊢ ⨅ i, induced ((Types.limitCone (F ⋙ forget TopCat)).π.app i ∘ ⇑homeo) (F.obj i).str =
    ⨅ j, induced (⇑(ConcreteCategory.hom (C.π.app j))) (F.obj j).str

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
homeo : ↑C.pt ≃ₜ ↑(limitConeInfi F).pt := homeoOfIso (hC.conePointUniqueUpToIso (limitConeInfiIsLimit F))
⊢ induced (⇑homeo) (limitConeInfi F).pt.str = ⨅ j, induced (⇑(ConcreteCategory.hom (C.π.app j))) (F.obj j).str

Tactic:
change induced homeo (⨅ j : J, _) = _

Result:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
homeo : ↑C.pt ≃ₜ ↑(limitConeInfi F).pt := homeoOfIso (hC.conePointUniqueUpToIso (limitConeInfiIsLimit F))
⊢ induced (⇑homeo) (⨅ j, induced ((Types.limitCone (F ⋙ forget TopCat)).π.app j) (F.obj j).str) =
    ⨅ j, induced (⇑(ConcreteCategory.hom (C.π.app j))) (F.obj j).str

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
homeo : ↑C.pt ≃ₜ ↑(limitConeInfi F).pt := homeoOfIso (hC.conePointUniqueUpToIso (limitConeInfiIsLimit F))
⊢ C.pt.str = ⨅ j, induced (⇑(ConcreteCategory.hom (C.π.app j))) (F.obj j).str

Tactic:
refine homeo.isInducing.eq_induced.trans ?_

Result:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
homeo : ↑C.pt ≃ₜ ↑(limitConeInfi F).pt := homeoOfIso (hC.conePointUniqueUpToIso (limitConeInfiIsLimit F))
⊢ induced (⇑homeo) (limitConeInfi F).pt.str = ⨅ j, induced (⇑(ConcreteCategory.hom (C.π.app j))) (F.obj j).str