awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.ULift (goal)
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cone K
hc : IsLimit c
⊢ LE.le (α := TopologicalSpace (↑(uliftFunctor.mapCone c).pt : Type (max u v))) (uliftFunctor.mapCone c).pt.str
    (⨅ (j : J),
      TopologicalSpace.induced (Y := (↑((K ⋙ uliftFunctor).obj j) : Type (max u v)))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) ((uliftFunctor.mapCone c).π.app j)) :
          (a : (↑(((Functor.const J).obj (uliftFunctor.mapCone c).pt).obj j) : Type (max u v))) →
            (↑((K ⋙ uliftFunctor).obj j) : Type (max u v)))
        ((K ⋙ uliftFunctor).obj j).str)
have refine_1 : ∀ (i : J),
  LE.le (α := TopologicalSpace (↑(uliftFunctor.mapCone c).pt : Type (max u v))) (uliftFunctor.mapCone c).pt.str
    (TopologicalSpace.induced (Y := (↑((K ⋙ uliftFunctor).obj i) : Type (max u v)))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
            carrier) ((uliftFunctor.mapCone c).π.app i)) :
        (a : (↑(((Functor.const J).obj (uliftFunctor.mapCone c).pt).obj i) : Type (max u v))) →
          (↑((K ⋙ uliftFunctor).obj i) : Type (max u v)))
      ((K ⋙ uliftFunctor).obj i).str)
Tactic: rw [le_iInf_iff]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.ULift (goal)
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cone K
hc : IsLimit c
j : J
t : Set (↑((K ⋙ uliftFunctor).obj j) : Type (max u v))
ht : IsOpen t
⊢ IsOpen (X := (↑(uliftFunctor.mapCone c).pt : Type (max u v)))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
            carrier) ((uliftFunctor.mapCone c).π.app j)) :
        (a : (↑(((Functor.const J).obj (uliftFunctor.mapCone c).pt).obj j) : Type (max u v))) →
          (↑((K ⋙ uliftFunctor).obj j) : Type (max u v))) ⁻¹'
      t)
have refine_1 : IsOpen.{u} (X := (↑c.pt : Type u))
  (Set.preimage (β := ULift.{v, u} (↑c.pt : Type u))
    (⇑(Homeomorph.symm Homeomorph.ulift) : (a : (↑c.pt : Type u)) → ULift.{v, u} (↑c.pt : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
            carrier) (uliftFunctor.map (c.π.app j))) :
        (a : (↑(uliftFunctor.obj (((Functor.const J).obj c.pt).obj j)) : Type (max u v))) →
          (↑(uliftFunctor.obj (K.obj j)) : Type (max u v))) ⁻¹'
      t))
Tactic: refine ⟨Homeomorph.ulift.symm ⁻¹' ((uliftFunctor.map (c.π.app j)) ⁻¹' t), ?_, rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.ULift (goal)
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cone K
hc : IsLimit c
j : J
t : Set (↑((K ⋙ uliftFunctor).obj j) : Type (max u v))
ht : IsOpen t
⊢ IsOpen.{u} (X := (↑c.pt : Type u))
    (Set.preimage (β := ULift.{v, u} (↑c.pt : Type u))
      (⇑(Homeomorph.symm Homeomorph.ulift) : (a : (↑c.pt : Type u)) → ULift.{v, u} (↑c.pt : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) (uliftFunctor.map (c.π.app j))) :
          (a : (↑(uliftFunctor.obj (((Functor.const J).obj c.pt).obj j)) : Type (max u v))) →
            (↑(uliftFunctor.obj (K.obj j)) : Type (max u v))) ⁻¹'
        t))
have refine_1 : IsOpen (X := ULift.{v, u} (↑c.pt : Type u))
  ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
          (uliftFunctor.map (c.π.app j))) :
      (a : (↑(uliftFunctor.obj (((Functor.const J).obj c.pt).obj j)) : Type (max u v))) →
        (↑(uliftFunctor.obj (K.obj j)) : Type (max u v))) ⁻¹'
    t)
Tactic: apply Homeomorph.ulift.continuous_invFun.isOpen_preimage
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.ULift (goal)
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cone K
hc : IsLimit c
⊢ LE.le (α := TopologicalSpace (↑(uliftFunctor.mapCone c).pt : Type (max u v)))
    (⨅ (j : J),
      TopologicalSpace.induced (Y := (↑((K ⋙ uliftFunctor).obj j) : Type (max u v)))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) ((uliftFunctor.mapCone c).π.app j)) :
          (a : (↑(((Functor.const J).obj (uliftFunctor.mapCone c).pt).obj j) : Type (max u v))) →
            (↑((K ⋙ uliftFunctor).obj j) : Type (max u v)))
        ((K ⋙ uliftFunctor).obj j).str)
    (TopologicalSpace.induced ULift.down c.pt.str)
have refine_2 : ∀ (i : J),
  LE.le (α := TopologicalSpace (↑(uliftFunctor.mapCone c).pt : Type (max u v)))
    (TopologicalSpace.generateFrom (⋃ (i : J), {s : Set (↑(uliftFunctor.mapCone c).pt : Type (max u v)) | IsOpen s}))
    (TopologicalSpace.induced ULift.down
      (TopologicalSpace.induced (Y := (↑(K.obj i) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (c.π.app i)) :
          (a : (↑(((Functor.const J).obj c.pt).obj i) : Type u)) → (↑(K.obj i) : Type u))
        (K.obj i).str))
Tactic: rw [← generateFrom_iUnion_isOpen, induced_of_isLimit _ hc, induced_iInf, le_iInf_iff]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.ULift (goal)
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cone K
hc : IsLimit c
i : J
t : Set (↑(K.obj i) : Type u)
ht : IsOpen t
⊢ IsOpen (X := (↑(uliftFunctor.mapCone c).pt : Type (max u v)))
    (ULift.down ⁻¹'
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (c.π.app i)) :
          (a : (↑(((Functor.const J).obj c.pt).obj i) : Type u)) → (↑(K.obj i) : Type u)) ⁻¹'
        t)
have refine_2 : Membership.mem (γ := Set (Set (↑(uliftFunctor.mapCone c).pt : Type (max u v))))
  (⋃ (i : J), {s : Set (↑(uliftFunctor.mapCone c).pt : Type (max u v)) | IsOpen s})
  (ULift.down ⁻¹'
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (c.π.app i)) :
        (a : (↑(((Functor.const J).obj c.pt).obj i) : Type u)) → (↑(K.obj i) : Type u)) ⁻¹'
      t)
Tactic: refine .basic _ ?_
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.ULift (goal)
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cone K
hc : IsLimit c
i : J
t : Set (↑(K.obj i) : Type u)
ht : IsOpen t
⊢ Membership.mem (γ := Set (Set (↑(uliftFunctor.mapCone c).pt : Type (max u v))))
    (⋃ (i : J), {s : Set (↑(uliftFunctor.mapCone c).pt : Type (max u v)) | IsOpen s})
    (ULift.down ⁻¹'
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (c.π.app i)) :
          (a : (↑(((Functor.const J).obj c.pt).obj i) : Type u)) → (↑(K.obj i) : Type u)) ⁻¹'
        t)
have refine_2 : ∃ (i_1 : J),
  Membership.mem (γ := Set (Set (↑(uliftFunctor.mapCone c).pt : Type (max u v))))
    {s : Set (↑(uliftFunctor.mapCone c).pt : Type (max u v)) | IsOpen s}
    (ULift.down ⁻¹'
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (c.π.app i)) :
          (a : (↑(((Functor.const J).obj c.pt).obj i) : Type u)) → (↑(K.obj i) : Type u)) ⁻¹'
        t)
Tactic: rw [Set.mem_iUnion]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.ULift (goal)
Goal:
⊢ PreservesColimitsOfSize.{w', w, u, max u v, u + 1, max (u + 1) (v + 1)} uliftFunctor
have refine : ∀ {J : Type w} [inst : Category.{w', w} J] {K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat} {c : Cocone K}
  (hc : IsColimit c), Nonempty (IsColimit (uliftFunctor.mapCocone c))
Tactic: refine ⟨⟨fun {K} ↦ ⟨fun {c} hc ↦ ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.ULift (goal)
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cocone K
hc : IsColimit c
⊢ Nonempty (IsColimit (uliftFunctor.mapCocone c))
have rw : Eq (α := TopologicalSpace (↑(uliftFunctor.mapCocone c).pt : Type (max u v))) (uliftFunctor.mapCocone c).pt.str
  (⨆ (j : J),
    TopologicalSpace.coinduced (X := (↑((K ⋙ uliftFunctor).obj j) : Type (max u v)))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
            carrier) ((uliftFunctor.mapCocone c).ι.app j)) :
        (a : (↑((K ⋙ uliftFunctor).obj j) : Type (max u v))) →
          (↑(((Functor.const J).obj (uliftFunctor.mapCocone c).pt).obj j) : Type (max u v)))
      ((K ⋙ uliftFunctor).obj j).str)
Tactic: rw [nonempty_isColimit_iff_eq_coinduced]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.ULift (goal)
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cocone K
hc : IsColimit c
rw :
  Eq (α := TopologicalSpace (↑(uliftFunctor.mapCocone c).pt : Type (max u v))) (uliftFunctor.mapCocone c).pt.str
    (⨆ (j : J),
      TopologicalSpace.coinduced (X := (↑((K ⋙ uliftFunctor).obj j) : Type (max u v)))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) ((uliftFunctor.mapCocone c).ι.app j)) :
          (a : (↑((K ⋙ uliftFunctor).obj j) : Type (max u v))) →
            (↑(((Functor.const J).obj (uliftFunctor.mapCocone c).pt).obj j) : Type (max u v)))
        ((K ⋙ uliftFunctor).obj j).str)
⊢ Nonempty (IsColimit (uliftFunctor.mapCocone c))
have hc₁ : IsColimit (F :=
  (K ⋙ uliftFunctor) ⋙
    forget TopCat (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier))
  (Functor.mapCocone
    (forget TopCat (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier))
    (uliftFunctor.mapCocone c))
Tactic: rw [nonempty_isColimit_iff_eq_coinduced]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.ULift (goal)
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cocone K
hc : IsColimit c
⊢ Eq (α := TopologicalSpace (↑(uliftFunctor.mapCocone c).pt : Type (max u v))) (uliftFunctor.mapCocone c).pt.str
    (⨆ (j : J),
      TopologicalSpace.coinduced (X := (↑((K ⋙ uliftFunctor).obj j) : Type (max u v)))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) ((uliftFunctor.mapCocone c).ι.app j)) :
          (a : (↑((K ⋙ uliftFunctor).obj j) : Type (max u v))) →
            (↑(((Functor.const J).obj (uliftFunctor.mapCocone c).pt).obj j) : Type (max u v)))
        ((K ⋙ uliftFunctor).obj j).str)
have a : ∀ (s : Set (↑(uliftFunctor.mapCocone c).pt : Type (max u v))), IsOpen s ↔ IsOpen s
Tactic: ext s
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.ULift (goal)
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cocone K
hc : IsColimit c
s : Set (↑(uliftFunctor.mapCocone c).pt : Type (max u v))
⊢ IsOpen s ↔ IsOpen s
have a : (∀ (j : J),
    IsOpen (X := (↑(K.obj j) : Type u))
      (Set.preimage (β := (↑(Functor.obj.{w', u, w, u + 1} (Functor.obj (Functor.const J) c.pt) j) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (c.ι.app j)) :
          (a : (↑(K.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u))
        ((⇑(Homeomorph.symm Homeomorph.ulift) : (a : (↑c.pt : Type u)) → ULift.{v, u} (↑c.pt : Type u)) ⁻¹' s))) ↔
  ∀ (i : J), IsOpen s
Tactic: rw [Homeomorph.ulift.symm.isOpenEmbedding.isOpen_iff_preimage_isOpen (by simp),
      isOpen_iff_of_isColimit _ hc, isOpen_iSup_iff]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.ULift (goal)
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cocone K
hc : IsColimit c
s : Set (↑(uliftFunctor.mapCocone c).pt : Type (max u v))
⊢ (∀ (j : J),
      IsOpen (X := (↑(K.obj j) : Type u))
        (Set.preimage (β := (↑(Functor.obj.{w', u, w, u + 1} (Functor.obj (Functor.const J) c.pt) j) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (c.ι.app j)) :
            (a : (↑(K.obj j) : Type u)) → (↑(((Functor.const J).obj c.pt).obj j) : Type u))
          ((⇑(Homeomorph.symm Homeomorph.ulift) : (a : (↑c.pt : Type u)) → ULift.{v, u} (↑c.pt : Type u)) ⁻¹' s))) ↔
    ∀ (i : J), IsOpen s
have a : ∀ (a : J),
  IsOpen (X := (↑(K.obj a) : Type u))
      (Set.preimage (β := (↑(Functor.obj.{w', u, w, u + 1} (Functor.obj (Functor.const J) c.pt) a) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (c.ι.app a)) :
          (a_1 : (↑(K.obj a) : Type u)) → (↑(((Functor.const J).obj c.pt).obj a) : Type u))
        ((⇑(Homeomorph.symm Homeomorph.ulift) : (a : (↑c.pt : Type u)) → ULift.{v, u} (↑c.pt : Type u)) ⁻¹' s)) ↔
    IsOpen s
Tactic: congr!
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.ULift (goal)
Goal:
J : Type w
inst : Category.{w', w} J
K : CategoryTheory.Functor.{w', u, w, u + 1} J TopCat
c : Cocone K
hc : IsColimit c
s : Set (↑(uliftFunctor.mapCocone c).pt : Type (max u v))
a : J
⊢ IsOpen (X := (↑(K.obj a) : Type u))
      (Set.preimage (β := (↑(Functor.obj.{w', u, w, u + 1} (Functor.obj (Functor.const J) c.pt) a) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (c.ι.app a)) :
          (a_1 : (↑(K.obj a) : Type u)) → (↑(((Functor.const J).obj c.pt).obj a) : Type u))
        ((⇑(Homeomorph.symm Homeomorph.ulift) : (a : (↑c.pt : Type u)) → ULift.{v, u} (↑c.pt : Type u)) ⁻¹' s)) ↔
    IsOpen s
have a : IsOpen (X := ULift.{v, u} (↑(K.obj a) : Type u))
    (Set.preimage (β := (↑(K.obj a) : Type u))
      (⇑Homeomorph.ulift : (a_1 : ULift.{v, u} (↑(K.obj a) : Type u)) → (↑(K.obj a) : Type u))
      (Set.preimage (β := (↑(Functor.obj.{w', u, w, u + 1} (Functor.obj (Functor.const J) c.pt) a) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (c.ι.app a)) :
          (a_1 : (↑(K.obj a) : Type u)) → (↑(((Functor.const J).obj c.pt).obj a) : Type u))
        ((⇑(Homeomorph.symm Homeomorph.ulift) : (a : (↑c.pt : Type u)) → ULift.{v, u} (↑c.pt : Type u)) ⁻¹' s))) ↔
  IsOpen s
Tactic: rw [Homeomorph.ulift.isOpenEmbedding.isOpen_iff_preimage_isOpen (by simp)]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Yoneda (goal)
Goal:
Y : Type w'
inst : TopologicalSpace Y
α : Type
X : α → TopCat
⊢ Eq (α := (yonedaPresheaf' Y).obj (∏ᶜ fun (x : α) ↦ op (X x)) ⟶ ∏ᶜ fun (b : α) ↦ (yonedaPresheaf' Y).obj (op (X b)))
    (piComparison (yonedaPresheaf' Y) fun (x : α) ↦ op (X x))
    ((yonedaPresheaf' Y).map (Iso.inv (opCoproductIsoProduct X) ≫ (TopCat.sigmaIsoSigma X).inv.op) ≫
      Iso.inv
          ((equivEquivIso :
              (a : ((i : α) → C((↑(X i) : Type w), Y)) ≃ C((i : α) × (↑(X i) : Type w), Y)) →
                ((i : α) → C((↑(X i) : Type w), Y)) ≅ C((i : α) × (↑(X i) : Type w), Y))
            (sigmaEquiv Y fun (x : α) ↦ (↑(X x) : Type w))) ≫
        Iso.inv (Types.productIso fun (i : α) ↦ ContinuousMap.{w, w'} (↑(X i) : Type w) Y))
have rw : (piComparison (yonedaPresheaf' Y) fun (x : α) ↦ op (X x)) ≫
    Iso.hom (Types.productIso fun (i : α) ↦ ContinuousMap.{w, w'} (↑(X i) : Type w) Y) =
  (yonedaPresheaf' Y).map (Iso.inv (opCoproductIsoProduct X) ≫ (TopCat.sigmaIsoSigma X).inv.op) ≫
    Iso.inv
      ((equivEquivIso :
          (a : ((i : α) → C((↑(X i) : Type w), Y)) ≃ C((i : α) × (↑(X i) : Type w), Y)) →
            ((i : α) → C((↑(X i) : Type w), Y)) ≅ C((i : α) × (↑(X i) : Type w), Y))
        (sigmaEquiv Y fun (x : α) ↦ (↑(X x) : Type w)))
Tactic: rw [← Category.assoc, Iso.eq_comp_inv]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Yoneda (goal)
Goal:
Y : Type w'
inst : TopologicalSpace Y
α : Type
X : α → TopCat
⊢ (piComparison (yonedaPresheaf' Y) fun (x : α) ↦ op (X x)) ≫
      Iso.hom (Types.productIso fun (i : α) ↦ ContinuousMap.{w, w'} (↑(X i) : Type w) Y) =
    (yonedaPresheaf' Y).map (Iso.inv (opCoproductIsoProduct X) ≫ (TopCat.sigmaIsoSigma X).inv.op) ≫
      Iso.inv
        ((equivEquivIso :
            (a : ((i : α) → C((↑(X i) : Type w), Y)) ≃ C((i : α) × (↑(X i) : Type w), Y)) →
              ((i : α) → C((↑(X i) : Type w), Y)) ≅ C((i : α) × (↑(X i) : Type w), Y))
          (sigmaEquiv Y fun (x : α) ↦ (↑(X x) : Type w)))
have h : ∀ (x : (yonedaPresheaf' Y).obj (∏ᶜ fun (x : α) ↦ op (X x))) (x_1 : α) (a : (↑(X x_1) : Type w)),
  Eq.{w' + 1} (α := Y)
    ((TypeCat.Fun.toFun
            (ConcreteCategory.hom (FC := TypeCat.Fun)
              ((piComparison (yonedaPresheaf' Y) fun (x : α) ↦ op (X x)) ≫
                Iso.hom (Types.productIso fun (i : α) ↦ ContinuousMap.{w, w'} (↑(X i) : Type w) Y)))
            x x_1 :
          (a : (↑(X x_1) : Type w)) → Y)
        a :
      Y)
    ((TypeCat.Fun.toFun
            (ConcreteCategory.hom (FC := TypeCat.Fun)
              ((yonedaPresheaf' Y).map (Iso.inv (opCoproductIsoProduct X) ≫ (TopCat.sigmaIsoSigma X).inv.op) ≫
                Iso.inv
                  ((equivEquivIso :
                      (a : ((i : α) → C((↑(X i) : Type w), Y)) ≃ C((i : α) × (↑(X i) : Type w), Y)) →
                        ((i : α) → C((↑(X i) : Type w), Y)) ≅ C((i : α) × (↑(X i) : Type w), Y))
                    (sigmaEquiv Y fun (x : α) ↦ (↑(X x) : Type w)))))
            x x_1 :
          (a : (↑(X x_1) : Type w)) → Y)
        a :
      Y)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Yoneda (goal)
Goal:
Y : Type w'
inst : TopologicalSpace Y
α : Type
X : α → TopCat
x : (yonedaPresheaf' Y).obj (∏ᶜ fun (x : α) ↦ op (X x))
x_1 : α
a : (↑(X x_1) : Type w)
⊢ Eq.{w' + 1} (α := Y)
    ((TypeCat.Fun.toFun
            (ConcreteCategory.hom (FC := TypeCat.Fun)
              ((piComparison (yonedaPresheaf' Y) fun (x : α) ↦ op (X x)) ≫
                Iso.hom (Types.productIso fun (i : α) ↦ ContinuousMap.{w, w'} (↑(X i) : Type w) Y)))
            x x_1 :
          (a : (↑(X x_1) : Type w)) → Y)
        a :
      Y)
    ((TypeCat.Fun.toFun
            (ConcreteCategory.hom (FC := TypeCat.Fun)
              ((yonedaPresheaf' Y).map (Iso.inv (opCoproductIsoProduct X) ≫ (TopCat.sigmaIsoSigma X).inv.op) ≫
                Iso.inv
                  ((equivEquivIso :
                      (a : ((i : α) → C((↑(X i) : Type w), Y)) ≃ C((i : α) × (↑(X i) : Type w), Y)) →
                        ((i : α) → C((↑(X i) : Type w), Y)) ≅ C((i : α) × (↑(X i) : Type w), Y))
                    (sigmaEquiv Y fun (x : α) ↦ (↑(X x) : Type w)))))
            x x_1 :
          (a : (↑(X x_1) : Type w)) → Y)
        a :
      Y)
have h : Eq.{w' + 1} (α := Y)
  ((x : (a : (↑(unop (∏ᶜ fun (x : α) ↦ op (X x))) : Type w)) → Y)
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
              (X := ∐ X) (Quiver.Hom.unop (Iso.inv (opCoproductIsoProduct X))) :
            (a : (↑(∐ X) : Type w)) → (↑(unop (∏ᶜ fun (x : α) ↦ op (X x))) : Type w))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
                  (Y := ∐ X) (Sigma.ι X x_1) :
                (a : (↑(X x_1) : Type w)) → (↑(∐ X) : Type w))
              a :
            (↑(∐ X) : Type w)) :
        (↑(unop (∏ᶜ fun (x : α) ↦ op (X x))) : Type w)) :
    Y)
  ((x : (a : (↑(unop (∏ᶜ fun (x : α) ↦ op (X x))) : Type w)) → Y)
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
              (X := ∐ X) (Quiver.Hom.unop (Iso.inv (opCoproductIsoProduct X))) :
            (a : (↑(∐ X) : Type w)) → (↑(unop (∏ᶜ fun (x : α) ↦ op (X x))) : Type w))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
                  (TopCat.sigmaIsoSigma X).inv :
                (a : (i : α) × (↑(X i) : Type w)) → (↑(∐ X) : Type w))
              (Sigma.mk (β := fun (x : α) ↦ (↑(X x) : Type w)) x_1 a) :
            (↑(∐ X) : Type w)) :
        (↑(unop (∏ᶜ fun (x : α) ↦ op (X x))) : Type w)) :
    Y)
Tactic: simp [yonedaPresheaf', piComparison, ← opCoproductIsoProduct_inv_comp_ι]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : CategoryTheory.Functor.{v, w, u, w + 1} C TopCat
Y : Type w'
inst_1 : TopologicalSpace Y
x : ℕ
K : Discrete (Fin x) ⥤ TopCatᵒᵖ
α : Type
X : α → TopCat
⊢ IsIso (X := (yonedaPresheaf' Y).obj (∏ᶜ fun (x : α) ↦ op (X x))) (Y :=
    ∏ᶜ fun (b : α) ↦ (yonedaPresheaf' Y).obj ((fun (x : α) ↦ op (X x)) b))
    (piComparison (yonedaPresheaf' Y) fun (x : α) ↦ op (X x))
have rw : IsIso (Y := ∏ᶜ fun (b : α) ↦ (yonedaPresheaf' Y).obj ((fun (x : α) ↦ op (X x)) b))
  ((yonedaPresheaf' Y).map (Iso.inv (opCoproductIsoProduct X) ≫ (TopCat.sigmaIsoSigma X).inv.op) ≫
    Iso.inv
        ((equivEquivIso :
            (a : ((i : α) → C((↑(X i) : Type w), Y)) ≃ C((i : α) × (↑(X i) : Type w), Y)) →
              ((i : α) → C((↑(X i) : Type w), Y)) ≅ C((i : α) × (↑(X i) : Type w), Y))
          (sigmaEquiv Y fun (x : α) ↦ (↑(X x) : Type w))) ≫
      Iso.inv (Types.productIso fun (i : α) ↦ ContinuousMap.{w, w'} (↑(X i) : Type w) Y))
Tactic: rw [piComparison_fac]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCommRingCat (goal)
Goal:
R : TopCommRingCat
⊢ Continuous.{u, u} (X := R.α) (Y := R.α)
    (⇑{ toFun := fun (x : R.α) ↦ x, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } : (a : R.α) → R.α)
have dsimp : Continuous (Y := R.α) fun (x : R.α) ↦ x
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.Category.TopCommRingCat (goal)
Goal:
X Y Z : TopCommRingCat
f : { f : X.α →+* Y.α // Continuous (X := X.α) (Y := Y.α) (⇑f : (a : X.α) → Y.α) }
g : { f : Y.α →+* Z.α // Continuous (X := Y.α) (Y := Z.α) (⇑f : (a : Y.α) → Z.α) }
⊢ Continuous (X := X.α) (Y := Z.α) (⇑((↑g : Y.α →+* Z.α).comp (↑f : X.α →+* Y.α)) : (a : X.α) → Z.α)
have mk : ∀ (val : X.α →+* Y.α) (property : Continuous (X := X.α) (Y := Y.α) (⇑val : (a : X.α) → Y.α)),
  Continuous (X := X.α) (Y := Z.α)
    (⇑((↑g : Y.α →+* Z.α).comp
          (↑(Subtype.mk (p := fun (f : X.α →+* Y.α) ↦ Continuous (X := X.α) (Y := Y.α) (⇑f : (a : X.α) → Y.α)) val
                property) :
            X.α →+* Y.α)) :
      (a : X.α) → Z.α)
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Topology.Category.TopCommRingCat (goal)
Goal:
X Y Z : TopCommRingCat
g : { f : Y.α →+* Z.α // Continuous (X := Y.α) (Y := Z.α) (⇑f : (a : Y.α) → Z.α) }
val : X.α →+* Y.α
property : Continuous (X := X.α) (Y := Y.α) (⇑val : (a : X.α) → Y.α)
⊢ Continuous (X := X.α) (Y := Z.α)
    (⇑((↑g : Y.α →+* Z.α).comp
          (↑(Subtype.mk (p := fun (f : X.α →+* Y.α) ↦ Continuous (X := X.α) (Y := Y.α) (⇑f : (a : X.α) → Y.α)) val
                property) :
            X.α →+* Y.α)) :
      (a : X.α) → Z.α)
have mk : ∀ (val_1 : Y.α →+* Z.α) (property_1 : Continuous (X := Y.α) (Y := Z.α) (⇑val_1 : (a : Y.α) → Z.α)),
  Continuous (X := X.α) (Y := Z.α)
    (⇑((↑(Subtype.mk (p := fun (f : Y.α →+* Z.α) ↦ Continuous (X := Y.α) (Y := Z.α) (⇑f : (a : Y.α) → Z.α)) val_1
                  property_1) :
              Y.α →+* Z.α).comp
          (↑(Subtype.mk (p := fun (f : X.α →+* Y.α) ↦ Continuous (X := X.α) (Y := Y.α) (⇑f : (a : X.α) → Y.α)) val
                property) :
            X.α →+* Y.α)) :
      (a : X.α) → Z.α)
Tactic: cases g
Cleared hypotheses: g