-- Mathlib/Topology/Category/TopCat/Limits/Basic.lean
theorem coinduced_of_isColimit :
    c.pt.str = ⨆ j, (F.obj j).str.coinduced (c.ι.app j)

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
c' : Cocone F := coconeOfCoconeForget (forget.mapCocone c)
hc' : IsColimit c' := isColimitCoconeOfForget (forget.mapCocone c) (isColimitOfPreserves forget hc)
e : c'.pt ≅ c.pt := hc'.coconePointUniqueUpToIso hc
⊢ c.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str

Tactic:
have he (j : J) : c'.ι.app j ≫ e.hom = c.ι.app j :=
  IsColimit.comp_coconePointUniqueUpToIso_hom hc' hc j

Result:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
c' : Cocone F := coconeOfCoconeForget (forget.mapCocone c)
hc' : IsColimit c' := isColimitCoconeOfForget (forget.mapCocone c) (isColimitOfPreserves forget hc)
e : c'.pt ≅ c.pt := hc'.coconePointUniqueUpToIso hc
he : ∀ (j : J), c'.ι.app j ≫ e.hom = c.ι.app j
⊢ c.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
c' : Cocone F := coconeOfCoconeForget (forget.mapCocone c)
hc' : IsColimit c' := isColimitCoconeOfForget (forget.mapCocone c) (isColimitOfPreserves forget hc)
e : c'.pt ≅ c.pt := hc'.coconePointUniqueUpToIso hc
he : ∀ (j : J), c'.ι.app j ≫ e.hom = c.ι.app j
⊢ c.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str

Tactic:
apply (homeoOfIso e).coinduced_eq.symm.trans

Result:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
c' : Cocone F := coconeOfCoconeForget (forget.mapCocone c)
hc' : IsColimit c' := isColimitCoconeOfForget (forget.mapCocone c) (isColimitOfPreserves forget hc)
e : c'.pt ≅ c.pt := hc'.coconePointUniqueUpToIso hc
he : ∀ (j : J), c'.ι.app j ≫ e.hom = c.ι.app j
⊢ coinduced (⇑(homeoOfIso e)) c'.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
⊢ c.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str

Tactic:
let c' := coconeOfCoconeForget ((forget).mapCocone c)

Result:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
c' : Cocone F := coconeOfCoconeForget (forget.mapCocone c)
⊢ c.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
c' : Cocone F := coconeOfCoconeForget (forget.mapCocone c)
hc' : IsColimit c' := isColimitCoconeOfForget (forget.mapCocone c) (isColimitOfPreserves forget hc)
e : c'.pt ≅ c.pt := hc'.coconePointUniqueUpToIso hc
he : ∀ (j : J), c'.ι.app j ≫ e.hom = c.ι.app j
⊢ ⨆ i, coinduced (⇑(homeoOfIso e)) (coinduced (⇑(ConcreteCategory.hom (c.ι.app i))) (F.obj i).str) =
    ⨆ j, coinduced (⇑(ConcreteCategory.hom (c'.ι.app j ≫ e.hom))) (F.obj j).str

Tactic:
rfl

Result:
no goals

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
c' : Cocone F := coconeOfCoconeForget (forget.mapCocone c)
hc' : IsColimit c' := isColimitCoconeOfForget (forget.mapCocone c) (isColimitOfPreserves forget hc)
⊢ c.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str

Tactic:
let e := IsColimit.coconePointUniqueUpToIso hc' hc

Result:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
c' : Cocone F := coconeOfCoconeForget (forget.mapCocone c)
hc' : IsColimit c' := isColimitCoconeOfForget (forget.mapCocone c) (isColimitOfPreserves forget hc)
e : c'.pt ≅ c.pt := hc'.coconePointUniqueUpToIso hc
⊢ c.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
c' : Cocone F := coconeOfCoconeForget (forget.mapCocone c)
⊢ c.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str

Tactic:
let hc' : IsColimit c' := isColimitCoconeOfForget _ (isColimitOfPreserves forget hc)

Result:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
c' : Cocone F := coconeOfCoconeForget (forget.mapCocone c)
hc' : IsColimit c' := isColimitCoconeOfForget (forget.mapCocone c) (isColimitOfPreserves forget hc)
⊢ c.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
c' : Cocone F := coconeOfCoconeForget (forget.mapCocone c)
hc' : IsColimit c' := isColimitCoconeOfForget (forget.mapCocone c) (isColimitOfPreserves forget hc)
e : c'.pt ≅ c.pt := hc'.coconePointUniqueUpToIso hc
he : ∀ (j : J), c'.ι.app j ≫ e.hom = c.ι.app j
⊢ coinduced (⇑(homeoOfIso e)) c'.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str

Tactic:
dsimp [coconeOfCoconeForget_pt, c', topologicalSpaceCoconePtOfCoconeForget]

Result:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
c' : Cocone F := coconeOfCoconeForget (forget.mapCocone c)
hc' : IsColimit c' := isColimitCoconeOfForget (forget.mapCocone c) (isColimitOfPreserves forget hc)
e : c'.pt ≅ c.pt := hc'.coconePointUniqueUpToIso hc
he : ∀ (j : J), c'.ι.app j ≫ e.hom = c.ι.app j
⊢ coinduced (⇑(homeoOfIso e)) (⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str) =
    ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
c' : Cocone F := coconeOfCoconeForget (forget.mapCocone c)
hc' : IsColimit c' := isColimitCoconeOfForget (forget.mapCocone c) (isColimitOfPreserves forget hc)
e : c'.pt ≅ c.pt := hc'.coconePointUniqueUpToIso hc
he : ∀ (j : J), c'.ι.app j ≫ e.hom = c.ι.app j
⊢ coinduced (⇑(homeoOfIso e)) (⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str) =
    ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str

Tactic:
simp only [coinduced_iSup, c']

Result:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
c' : Cocone F := coconeOfCoconeForget (forget.mapCocone c)
hc' : IsColimit c' := isColimitCoconeOfForget (forget.mapCocone c) (isColimitOfPreserves forget hc)
e : c'.pt ≅ c.pt := hc'.coconePointUniqueUpToIso hc
he : ∀ (j : J), c'.ι.app j ≫ e.hom = c.ι.app j
⊢ ⨆ i, coinduced (⇑(homeoOfIso e)) (coinduced (⇑(ConcreteCategory.hom (c.ι.app i))) (F.obj i).str) =
    ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
c' : Cocone F := coconeOfCoconeForget (forget.mapCocone c)
hc' : IsColimit c' := isColimitCoconeOfForget (forget.mapCocone c) (isColimitOfPreserves forget hc)
e : c'.pt ≅ c.pt := hc'.coconePointUniqueUpToIso hc
he : ∀ (j : J), c'.ι.app j ≫ e.hom = c.ι.app j
⊢ ⨆ i, coinduced (⇑(homeoOfIso e)) (coinduced (⇑(ConcreteCategory.hom (c.ι.app i))) (F.obj i).str) =
    ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str

Tactic:
conv_rhs => simp only [← he]

Result:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
c' : Cocone F := coconeOfCoconeForget (forget.mapCocone c)
hc' : IsColimit c' := isColimitCoconeOfForget (forget.mapCocone c) (isColimitOfPreserves forget hc)
e : c'.pt ≅ c.pt := hc'.coconePointUniqueUpToIso hc
he : ∀ (j : J), c'.ι.app j ≫ e.hom = c.ι.app j
⊢ ⨆ i, coinduced (⇑(homeoOfIso e)) (coinduced (⇑(ConcreteCategory.hom (c.ι.app i))) (F.obj i).str) =
    ⨆ j, coinduced (⇑(ConcreteCategory.hom (c'.ι.app j ≫ e.hom))) (F.obj j).str