awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c_1 c : Cocone (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
hc : IsColimit c
⊢ IsColimit (coconeOfCoconeForget c)
have refine : ∀ (s : Cocone F),
  Continuous (X := coconePtOfCoconeForget c) (Y := (↑s.1 : Type u))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (hc.desc
            (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
              s))) :
      (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) (forget.mapCocone s).pt)
Tactic: refine IsColimit.ofFaithful forget (ht := hc)
    (fun s ↦ ofHom (ContinuousMap.mk (hc.desc ((forget).mapCocone s)) ?_)) (fun _ ↦ rfl)
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c_1 c : Cocone (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
hc : IsColimit c
s : Cocone F
⊢ Continuous (X := coconePtOfCoconeForget c) (Y := (↑s.1 : Type u))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (hc.desc
            (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
              s))) :
      (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) (forget.mapCocone s).pt)
have rw : topologicalSpaceCoconePtOfCoconeForget c ≤
  induced (Y := (↑s.1 : Type u))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (hc.desc
            (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
              s))) :
      (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) (forget.mapCocone s).pt)
    (str s.1)
Tactic: rw [continuous_iff_le_induced]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c_1 c : Cocone (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
hc : IsColimit c
s : Cocone F
⊢ topologicalSpaceCoconePtOfCoconeForget c ≤
    induced (Y := (↑s.1 : Type u))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (hc.desc
              (Functor.mapCocone
                (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) s))) :
        (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) (forget.mapCocone s).pt)
      (str s.1)
have dsimp : LE.le (α := TopologicalSpace (coconePtOfCoconeForget c))
  (⨆ (j : J),
    coinduced (X := ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) : (a : ToType (F.obj j)) → c.pt) (F.obj j).str)
  (induced (Y := (↑s.1 : Type u))
    (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          (hc.desc
            (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
              s))) :
      (a : c.pt) → ToType s.pt)
    (str s.1))
Tactic: dsimp [topologicalSpaceCoconePtOfCoconeForget]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c_1 c : Cocone (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
hc : IsColimit c
s : Cocone F
⊢ LE.le (α := TopologicalSpace (coconePtOfCoconeForget c))
    (⨆ (j : J),
      coinduced (X := ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) : (a : ToType (F.obj j)) → c.pt) (F.obj j).str)
    (induced (Y := (↑s.1 : Type u))
      (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (hc.desc
              (Functor.mapCocone
                (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) s))) :
        (a : c.pt) → ToType s.pt)
      (str s.1))
have rw : ∀ (i : J),
  LE.le (α := TopologicalSpace (coconePtOfCoconeForget c))
    (coinduced (X := ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj i))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app i)) : (a : ToType (F.obj i)) → c.pt) (F.obj i).str)
    (induced (Y := (↑s.1 : Type u))
      (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (hc.desc
              (Functor.mapCocone
                (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) s))) :
        (a : c.pt) → ToType s.pt)
      (str s.1))
Tactic: rw [iSup_le_iff]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c_1 c : Cocone (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
hc : IsColimit c
s : Cocone F
j : J
⊢ LE.le (α := TopologicalSpace (coconePtOfCoconeForget c))
    (coinduced (X := ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) : (a : ToType (F.obj j)) → c.pt) (F.obj j).str)
    (induced (Y := (↑s.1 : Type u))
      (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (hc.desc
              (Functor.mapCocone
                (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) s))) :
        (a : c.pt) → ToType s.pt)
      (str s.1))
have rw : LE.le (α :=
  TopologicalSpace (ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j)))
  (F.obj j).str
  (induced (Y := (↑s.1 : Type u))
    (Function.comp (β := coconePtOfCoconeForget c)
      (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (hc.desc
              (Functor.mapCocone
                (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) s))) :
        (a : c.pt) → ToType s.pt)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) : (a : ToType (F.obj j)) → c.pt))
    (str s.1))
Tactic: rw [coinduced_le_iff_le_induced, induced_compose]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c_1 c : Cocone (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
hc : IsColimit c
s : Cocone F
j : J
⊢ LE.le (α :=
    TopologicalSpace
      (ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j)))
    (F.obj j).str
    (induced (Y := (↑s.1 : Type u))
      (Function.comp (β := coconePtOfCoconeForget c)
        (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (hc.desc
                (Functor.mapCocone
                  (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) s))) :
          (a : c.pt) → ToType s.pt)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) : (a : ToType (F.obj j)) → c.pt))
      (str s.1))
have h : (↑s.1 : Type u) = (↑(Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) s.pt) j) : Type u) →
  Eq (α :=
    ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j) → (↑s.1 : Type u))
    (Function.comp (β := coconePtOfCoconeForget c)
      (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (hc.desc
              (Functor.mapCocone
                (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) s))) :
        (a : c.pt) → ToType s.pt)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) : (a : ToType (F.obj j)) → c.pt))
    (⇑(Hom.hom (s.ι.app j)) : (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj s.pt).obj j) : Type u))
Tactic: convert! continuous_iff_le_induced.1 (s.ι.app j).hom.continuous
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c_1 c : Cocone (F ⋙ forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
hc : IsColimit c
s : Cocone F
j : J
e_2 : (↑s.1 : Type u) = (↑(Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) s.pt) j) : Type u)
⊢ Eq (α :=
    ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j) → (↑s.1 : Type u))
    (Function.comp (β := coconePtOfCoconeForget c)
      (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (hc.desc
              (Functor.mapCocone
                (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) s))) :
        (a : c.pt) → ToType s.pt)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) : (a : ToType (F.obj j)) → c.pt))
    (⇑(Hom.hom (s.ι.app j)) : (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj s.pt).obj j) : Type u))
have h : ∀ (x : ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j)),
  Eq (α := (↑s.1 : Type u))
    (Function.comp (β := coconePtOfCoconeForget c)
        (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (hc.desc
                (Functor.mapCocone
                  (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) s))) :
          (a : c.pt) → ToType s.pt)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) : (a : ToType (F.obj j)) → c.pt) x :
      (↑s.1 : Type u))
    ((Hom.hom (s.ι.app j) : (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj s.pt).obj j) : Type u)) x :
      (↑(Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) s.pt) j) : Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (hypothesis)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c : Cocone F
hc : IsColimit c
c' : Cocone F :=
  coconeOfCoconeForget
    (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
hc' : IsColimit c' :=
  isColimitCoconeOfForget
    (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
    (isColimitOfPreserves (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) hc)
e : c'.pt ≅ c.pt := hc'.coconePointUniqueUpToIso hc
⊢ Eq.{u + 1} (α := TopologicalSpace (↑c.pt : Type u)) c.pt.str
    (⨆ (j : J),
      coinduced (X := (↑(F.obj j) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (c.ι.app j)) :
          (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u))
        (F.obj j).str)
have he : ∀ (j : J), c'.ι.app j ≫ e.hom = c.ι.app j
Tactic: have he (j : J) : c'.ι.app j ≫ e.hom = c.ι.app j :=
    IsColimit.comp_coconePointUniqueUpToIso_hom hc' hc j
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c : Cocone F
hc : IsColimit c
c' : Cocone F :=
  coconeOfCoconeForget
    (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
hc' : IsColimit c' :=
  isColimitCoconeOfForget
    (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
    (isColimitOfPreserves (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) hc)
e : c'.pt ≅ c.pt := hc'.coconePointUniqueUpToIso hc
he : ∀ (j : J), c'.ι.app j ≫ e.hom = c.ι.app j
⊢ Eq.{u + 1} (α := TopologicalSpace (↑c.pt : Type u)) c.pt.str
    (⨆ (j : J),
      coinduced (X := (↑(F.obj j) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (c.ι.app j)) :
          (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u))
        (F.obj j).str)
have apply : Eq (α := TopologicalSpace (↑c.pt : Type u))
  (coinduced (X := (↑c'.pt : Type u)) (⇑(homeoOfIso e) : (a : (↑c'.pt : Type u)) → (↑c.pt : Type u)) c'.pt.str)
  (⨆ (j : J),
    coinduced (X := (↑(F.obj j) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (c.ι.app j)) :
        (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u))
      (F.obj j).str)
Tactic: apply (homeoOfIso e).coinduced_eq.symm.trans
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c : Cocone F
hc : IsColimit c
c' : Cocone F :=
  coconeOfCoconeForget
    (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
hc' : IsColimit c' :=
  isColimitCoconeOfForget
    (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
    (isColimitOfPreserves (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) hc)
e : c'.pt ≅ c.pt := hc'.coconePointUniqueUpToIso hc
he : ∀ (j : J), c'.ι.app j ≫ e.hom = c.ι.app j
⊢ Eq (α := TopologicalSpace (↑c.pt : Type u))
    (coinduced (X := (↑c'.pt : Type u)) (⇑(homeoOfIso e) : (a : (↑c'.pt : Type u)) → (↑c.pt : Type u)) c'.pt.str)
    (⨆ (j : J),
      coinduced (X := (↑(F.obj j) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (c.ι.app j)) :
          (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u))
        (F.obj j).str)
have dsimp : Eq (α := TopologicalSpace (↑c.pt : Type u))
  (coinduced (X :=
    coconePtOfCoconeForget
      (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c))
    (⇑(homeoOfIso e) : (a : coconePtOfCoconeForget (forget.mapCocone c)) → (↑c.pt : Type u))
    (⨆ (j : J),
      coinduced (X := ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j))
        (⇑{
              toFun :=
                (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      (c.ι.app j)) :
                  (a : (↑(F.obj j) : Type u)) → (↑c.pt : Type u)) } :
          (a : ToType (F.obj j)) → ToType c.pt)
        (F.obj j).str))
  (⨆ (j : J),
    coinduced (X := (↑(F.obj j) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (c.ι.app j)) :
        (a : (↑(F.obj j) : Type u)) → (↑c.pt : Type u))
      (F.obj j).str)
Tactic: dsimp [coconeOfCoconeForget_pt, c', topologicalSpaceCoconePtOfCoconeForget]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c : Cocone F
hc : IsColimit c
c' : Cocone F :=
  coconeOfCoconeForget
    (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
hc' : IsColimit c' :=
  isColimitCoconeOfForget
    (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
    (isColimitOfPreserves (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) hc)
e : c'.pt ≅ c.pt := hc'.coconePointUniqueUpToIso hc
he : ∀ (j : J), c'.ι.app j ≫ e.hom = c.ι.app j
⊢ Eq (α := TopologicalSpace (↑c.pt : Type u))
    (coinduced (X :=
      coconePtOfCoconeForget
        (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c))
      (⇑(homeoOfIso e) : (a : coconePtOfCoconeForget (forget.mapCocone c)) → (↑c.pt : Type u))
      (⨆ (j : J),
        coinduced (X :=
          ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj j))
          (⇑{
                toFun :=
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        carrier) (c.ι.app j)) :
                    (a : (↑(F.obj j) : Type u)) → (↑c.pt : Type u)) } :
            (a : ToType (F.obj j)) → ToType c.pt)
          (F.obj j).str))
    (⨆ (j : J),
      coinduced (X := (↑(F.obj j) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (c.ι.app j)) :
          (a : (↑(F.obj j) : Type u)) → (↑c.pt : Type u))
        (F.obj j).str)
have simp : Eq.{u + 1} (α := TopologicalSpace (↑c.pt : Type u))
  (⨆ (i : J),
    coinduced (X :=
      coconePtOfCoconeForget
        (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c))
      (⇑(homeoOfIso e) : (a : coconePtOfCoconeForget (forget.mapCocone c)) → (↑c.pt : Type u))
      (coinduced (X :=
        ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj i))
        (⇑{
              toFun :=
                (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      (c.ι.app i)) :
                  (a : (↑(F.obj i) : Type u)) → (↑c.pt : Type u)) } :
          (a : ToType (F.obj i)) → ToType c.pt)
        (F.obj i).str))
  (⨆ (j : J),
    coinduced (X := (↑(F.obj j) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (c.ι.app j)) :
        (a : (↑(F.obj j) : Type u)) → (↑c.pt : Type u))
      (F.obj j).str)
Tactic: simp only [coinduced_iSup]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c : Cocone F
hc : IsColimit c
c' : Cocone F :=
  coconeOfCoconeForget
    (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
hc' : IsColimit c' :=
  isColimitCoconeOfForget
    (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
    (isColimitOfPreserves (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) hc)
e : c'.pt ≅ c.pt := hc'.coconePointUniqueUpToIso hc
he : ∀ (j : J), c'.ι.app j ≫ e.hom = c.ι.app j
| ⨆ (j : J),
    coinduced (X := (↑(F.obj j) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (c.ι.app j)) :
        (a : (↑(F.obj j) : Type u)) → (↑c.pt : Type u))
      (F.obj j).str
have simp : ⨆ (j : J),
  coinduced (X := (↑(F.obj j) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
          (c'.ι.app j ≫ e.hom)) :
      (a : (↑(F.obj j) : Type u)) → (↑c.pt : Type u))
    (F.obj j).str
Tactic: simp only [← he]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c : Cocone F
hc : IsColimit c
c' : Cocone F :=
  coconeOfCoconeForget
    (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
hc' : IsColimit c' :=
  isColimitCoconeOfForget
    (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c)
    (isColimitOfPreserves (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) hc)
e : c'.pt ≅ c.pt := hc'.coconePointUniqueUpToIso hc
he : ∀ (j : J), c'.ι.app j ≫ e.hom = c.ι.app j
⊢ Eq.{u + 1} (α := TopologicalSpace (↑c.pt : Type u))
    (⨆ (i : J),
      coinduced (X :=
        coconePtOfCoconeForget
          (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
            c))
        (⇑(homeoOfIso e) : (a : coconePtOfCoconeForget (forget.mapCocone c)) → (↑c.pt : Type u))
        (coinduced (X :=
          ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj i))
          (⇑{
                toFun :=
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        carrier) (c.ι.app i)) :
                    (a : (↑(F.obj i) : Type u)) → (↑c.pt : Type u)) } :
            (a : ToType (F.obj i)) → ToType c.pt)
          (F.obj i).str))
    (⨆ (j : J),
      coinduced (X := (↑(F.obj j) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (c.ι.app j)) :
          (a : (↑(F.obj j) : Type u)) → (↑c.pt : Type u))
        (F.obj j).str)
have conv_rhs : Eq.{u + 1} (α := TopologicalSpace (↑c.pt : Type u))
  (⨆ (i : J),
    coinduced (X :=
      coconePtOfCoconeForget
        (Functor.mapCocone (forget (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) c))
      (⇑(homeoOfIso e) : (a : coconePtOfCoconeForget (forget.mapCocone c)) → (↑c.pt : Type u))
      (coinduced (X :=
        ToType (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (F.obj i))
        (⇑{
              toFun :=
                (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      (c.ι.app i)) :
                  (a : (↑(F.obj i) : Type u)) → (↑c.pt : Type u)) } :
          (a : ToType (F.obj i)) → ToType c.pt)
        (F.obj i).str))
  (⨆ (j : J),
    coinduced (X := (↑(F.obj j) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (c'.ι.app j ≫ e.hom)) :
        (a : (↑(F.obj j) : Type u)) → (↑c.pt : Type u))
      (F.obj j).str)
Tactic: conv_rhs => simp only [← he]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c : Cocone F
hc : IsColimit c
X : Set (↑c.pt : Type u)
⊢ IsOpen X ↔
    ∀ (j : J),
      IsOpen (X := (↑(F.obj j) : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (c.ι.app j)) :
            (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
          X)
have trans : IsOpen X ↔ TopologicalSpace.IsOpen X
Tactic: trans (⨆ (j : J), (F.obj j).str.coinduced (c.ι.app j)).IsOpen X
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Basic (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J TopCat
c : Cocone F
hc : IsColimit c
X : Set (↑c.pt : Type u)
trans : IsOpen X ↔ TopologicalSpace.IsOpen X
⊢ IsOpen X ↔
    ∀ (j : J),
      IsOpen (X := (↑(F.obj j) : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (c.ι.app j)) :
            (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
          X)
have trans₁ : TopologicalSpace.IsOpen X ↔
  ∀ (j : J),
    IsOpen (X := (↑(F.obj j) : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (c.ι.app j)) :
          (a : (↑(F.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u)) ⁻¹'
        X)
Tactic: trans (⨆ (j : J), (F.obj j).str.coinduced (c.ι.app j)).IsOpen X