J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
homeo : ↑C.pt ≃ₜ ↑(limitConeInfi F).pt := homeoOfIso (IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F))
⊢ C.pt.str = ⨅ (j : J), induced ((forget TopCat).map (C.π.app j)) (F.obj j).str
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
⊢ C.pt.str = ⨅ (j : J), induced ((forget TopCat).map (C.π.app j)) (F.obj j).str
let homeo := homeoOfIso (hC.conePointUniqueUpToIso (limitConeInfiIsLimit F))
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
homeo : ↑C.pt ≃ₜ ↑(limitConeInfi F).pt := homeoOfIso (IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F))
⊢ induced (↑homeo) (topologicalSpace_coe (limitConeInfi F).pt) =
    ⨅ (j : J), induced ((forget TopCat).map (C.π.app j)) (F.obj j).str
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
homeo : ↑C.pt ≃ₜ ↑(limitConeInfi F).pt := homeoOfIso (IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F))
⊢ C.pt.str = ⨅ (j : J), induced ((forget TopCat).map (C.π.app j)) (F.obj j).str
refine' homeo.inducing.induced.trans _
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
homeo : ↑C.pt ≃ₜ ↑(limitConeInfi F).pt := homeoOfIso (IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F))
⊢ induced (↑homeo) (⨅ (j : J), induced ((Types.limitCone (F ⋙ forget TopCat)).π.app j) (F.obj j).str) =
    ⨅ (j : J), induced ((forget TopCat).map (C.π.app j)) (F.obj j).str
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
homeo : ↑C.pt ≃ₜ ↑(limitConeInfi F).pt := homeoOfIso (IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F))
⊢ induced (↑homeo) (topologicalSpace_coe (limitConeInfi F).pt) =
    ⨅ (j : J), induced ((forget TopCat).map (C.π.app j)) (F.obj j).str
change induced homeo (⨅ j : J, _) = _
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
homeo : ↑C.pt ≃ₜ ↑(limitConeInfi F).pt := homeoOfIso (IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F))
⊢ (⨅ (i : J),
      induced
        ((Types.limitCone (F ⋙ forget TopCat)).π.app i ∘
          ↑(homeoOfIso (IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F))))
        (F.obj i).str) =
    ⨅ (j : J), induced ((forget TopCat).map (C.π.app j)) (F.obj j).str
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
homeo : ↑C.pt ≃ₜ ↑(limitConeInfi F).pt := homeoOfIso (IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F))
⊢ induced (↑homeo) (⨅ (j : J), induced ((Types.limitCone (F ⋙ forget TopCat)).π.app j) (F.obj j).str) =
    ⨅ (j : J), induced ((forget TopCat).map (C.π.app j)) (F.obj j).str
simp [induced_iInf, induced_compose]
no goals
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TopCatMax
C : Cone F
hC : IsLimit C
homeo : ↑C.pt ≃ₜ ↑(limitConeInfi F).pt := homeoOfIso (IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F))
⊢ (⨅ (i : J),
      induced
        ((Types.limitCone (F ⋙ forget TopCat)).π.app i ∘
          ↑(homeoOfIso (IsLimit.conePointUniqueUpToIso hC (limitConeInfiIsLimit F))))
        (F.obj i).str) =
    ⨅ (j : J), induced ((forget TopCat).map (C.π.app j)) (F.obj j).str
rfl