awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
F : Functor.{v', v, u', u} D C
hF : F.FullyFaithful
x x_1 x_2 : D
f : x_1 ⟶ x_2
⊢ Eq (α := F.obj x ⟶ F.obj x_2) (F.map (0 ≫ f)) (F.map 0)
have change : Eq (α := F.obj x ⟶ F.obj x_2) (F.map (hF.preimage 0 ≫ f)) (F.map (hF.preimage 0))
Tactic: change F.map ((hF.preimage _) ≫ f) = F.map (hF.preimage _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X : C
hX : IsTerminal.{v, u} X
⊢ IsZero.{v, u} X
have rw : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
Tactic: rw [IsZero.iff_id_eq_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X : C
hX : IsInitial.{v, u} X
⊢ IsZero.{v, u} X
have rw : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
Tactic: rw [IsZero.iff_id_eq_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
hY : IsZero.{v, u} Y
e : X ≅ Y
⊢ IsZero.{v, u} X
have refine_1 : ∀ (Z : C) (f : X ⟶ Z), f = default
Tactic: refine ⟨fun Z => ⟨⟨⟨e.hom ≫ hY.to_ Z⟩, fun f => ?_⟩⟩,
    fun Z => ⟨⟨⟨hY.from_ Z ≫ e.inv⟩, fun f => ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
hY : IsZero.{v, u} Y
e : X ≅ Y
refine_1 : ∀ (Z : C) (f : X ⟶ Z), f = default
⊢ IsZero.{v, u} X
have refine_2 : ∀ (Z : C) (f : Z ⟶ X), f = default
Tactic: refine ⟨fun Z => ⟨⟨⟨e.hom ≫ hY.to_ Z⟩, fun f => ?_⟩⟩,
    fun Z => ⟨⟨⟨hY.from_ Z ≫ e.inv⟩, fun f => ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
hY : IsZero.{v, u} Y
e : X ≅ Y
Z : C
f : X ⟶ Z
⊢ f = default
have refine_1 : e.inv ≫ f = e.inv ≫ default
Tactic: rw [← cancel_epi e.inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
hY : IsZero.{v, u} Y
e : X ≅ Y
Z : C
f : Z ⟶ X
⊢ f = default
have refine_2 : f ≫ e.hom = default ≫ e.hom
Tactic: rw [← cancel_mono e.hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
hF : ∀ (X : C), IsZero.{v', u'} (F.obj X)
⊢ IsZero F
have unique_to : ∀ (Y : Functor.{v, v', u, u'} C D), Nonempty (Unique (F ⟶ Y))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
hF : ∀ (X : C), IsZero.{v', u'} (F.obj X)
unique_to : ∀ (Y : Functor.{v, v', u, u'} C D), Nonempty (Unique (F ⟶ Y))
⊢ IsZero F
have unique_from : ∀ (Y : Functor.{v, v', u, u'} C D), Nonempty (Unique (Y ⟶ F))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
hF : ∀ (X : C), IsZero.{v', u'} (F.obj X)
G : Functor.{v, v', u, u'} C D
⊢ Nonempty (Unique (F ⟶ G))
have unique_to : F ⟶ G
Tactic: refine ⟨⟨⟨?_⟩, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
hF : ∀ (X : C), IsZero.{v', u'} (F.obj X)
G : Functor.{v, v', u, u'} C D
unique_to : F ⟶ G
⊢ Nonempty (Unique (F ⟶ G))
have unique_to₁ : ∀ (a : F ⟶ G), a = default
Tactic: refine ⟨⟨⟨?_⟩, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
hF : ∀ (X : C), IsZero.{v', u'} (F.obj X)
G : Functor.{v, v', u, u'} C D
⊢ Nonempty (Unique (G ⟶ F))
have unique_from : G ⟶ F
Tactic: refine ⟨⟨⟨?_⟩, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
hF : ∀ (X : C), IsZero.{v', u'} (F.obj X)
G : Functor.{v, v', u, u'} C D
unique_from : G ⟶ F
⊢ Nonempty (Unique (G ⟶ F))
have unique_from₁ : ∀ (a : G ⟶ F), a = default
Tactic: refine ⟨⟨⟨?_⟩, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
hF : ∀ (X : C), IsZero.{v', u'} (F.obj X)
G : Functor.{v, v', u, u'} C D
⊢ F ⟶ G
have unique_to : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.map f ≫ sorry.to_ (G.obj Y) = sorry.to_ (G.obj X) ≫ G.map f
Tactic: refine
      { app := fun X => (hF _).to_ _
        naturality := ?_ }
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
hF : ∀ (X : C), IsZero.{v', u'} (F.obj X)
G : Functor.{v, v', u, u'} C D
f : F ⟶ G
⊢ f = default
have unique_to : ∀ (x : C), f.app x = NatTrans.app default x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
hF : ∀ (X : C), IsZero.{v', u'} (F.obj X)
G : Functor.{v, v', u, u'} C D
⊢ G ⟶ F
have unique_from : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), G.map f ≫ sorry.from_ (G.obj Y) = sorry.from_ (G.obj X) ≫ F.map f
Tactic: refine
      { app := fun X => (hF _).from_ _
        naturality := ?_ }
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
hF : ∀ (X : C), IsZero.{v', u'} (F.obj X)
G : Functor.{v, v', u, u'} C D
f : G ⟶ F
⊢ f = default
have unique_from : ∀ (x : C), f.app x = NatTrans.app default x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroObject.{v', u'} D
F : Functor.{v, v', u, u'} C D
hF : IsZero F
X : C
G : Functor.{v, v', u, u'} C D := Functor.obj (Functor.const C) 0
⊢ IsZero.{v', u'} (F.obj X)
have hG : IsZero G
Tactic: have hG : IsZero G := Functor.isZero _ fun _ => isZero_zero _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_2 : F.Full
inst_3 : F.Faithful
X : C
hX : IsZero.{v', u'} (F.obj X)
⊢ IsZero.{v, u} X
have have : ∀ (h : F.FullyFaithful), IsZero.{v, u} X
Tactic: have h : F.FullyFaithful := .ofFullyFaithful _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_2 : F.Full
inst_3 : F.Faithful
X : C
hX : IsZero.{v', u'} (F.obj X)
h : F.FullyFaithful
⊢ IsZero.{v, u} X
have have : ∀ (this : (Y : C) → Unique (F.obj X ⟶ F.obj Y)), IsZero.{v, u} X
Tactic: have (Y : C) := (hX.unique_to (F.obj Y)).some
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_2 : F.Full
inst_3 : F.Faithful
X : C
hX : IsZero.{v', u'} (F.obj X)
h : F.FullyFaithful
this : (Y : C) → Unique (F.obj X ⟶ F.obj Y)
⊢ IsZero.{v, u} X
have have : ∀ (this : (Y : C) → Unique (F.obj Y ⟶ F.obj X)), IsZero.{v, u} X
Tactic: have (Y : C) := (hX.unique_from (F.obj Y)).some
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroObject.{v, u} C
f : Quiver.Hom.{v, u} (V := C) 0 0
⊢ IsIso f
have h : f = 𝟙 0
Tactic: convert! show IsIso (𝟙 (0 : C)) by infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsSifted.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
e : Equivalence.{v₁, v, u₁, u} D C
this : Equivalence.{v₁, v, u₁, u} (D × D) (C × C) := e.prod e
c : C
⊢ (e.inverse ⋙ Functor.diag D ⋙ this.functor).obj c ≅ obj.{v, v, u, u} (Functor.diag C) c
have dsimp : (e.functor.obj (e.inverse.obj c), e.functor.obj (e.inverse.obj c)) ≅ (c, c)
Tactic: dsimp [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsSifted.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
e : Equivalence.{v₁, v, u₁, u} D C
this : Equivalence.{v₁, v, u₁, u} (D × D) (C × C) := e.prod e
⊢ Final.{v₁, v₁, u₁, u₁} (Functor.diag D)
have have : ∀ (sq : e.inverse ⋙ Functor.diag D ⋙ this.functor ≅ Functor.diag C), Final.{v₁, v₁, u₁, u₁} (Functor.diag D)
Tactic: have sq : (e.inverse ⋙ diag D ⋙ this.functor ≅ diag C) :=
        NatIso.ofComponents (fun c ↦ by dsimp [this]
                                        exact Iso.prod (e.counitIso.app c) (e.counitIso.app c))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsSifted.{v, u} C
c₁ c₂ : C
⊢ ∃ (l : List C), List.IsChain Zag.{v, u} (c₁ :: l) ∧ (c₁ :: l).getLast ⋯ = c₂
have have : ∀ (X : StructuredArrow.{v, v, u, u} (c₁, c₂) (Functor.diag C)),
  ∃ (l : List C), List.IsChain Zag.{v, u} (c₁ :: l) ∧ (c₁ :: l).getLast sorry = c₂
Tactic: have X : StructuredArrow (c₁, c₂) (diag C) :=
          letI S : Final (diag C) := by infer_instance
          Nonempty.some (S.out (c₁, c₂)).is_nonempty
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsSifted.{v, u} C
c₁ c₂ : C
X : StructuredArrow.{v, v, u, u} (c₁, c₂) (Functor.diag C)
⊢ ∃ (l : List C), List.IsChain Zag.{v, u} (c₁ :: l) ∧ (c₁ :: l).getLast ⋯ = c₂
have h : List.IsChain Zag.{v, u} [c₁, X.right, c₂] ∧ [c₁, X.right, c₂].getLast sorry = c₂
Tactic: use [X.right, c₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsSifted.{v, u} C
c₁ c₂ : C
X : StructuredArrow.{v, v, u, u} (c₁, c₂) (Functor.diag C)
⊢ List.IsChain Zag.{v, u} [c₁, X.right, c₂] ∧ [c₁, X.right, c₂].getLast ⋯ = c₂
have h : List.IsChain Zag.{v, u} [c₁, X.right, c₂]
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsSifted.{v, u} C
c₁ c₂ : C
X : StructuredArrow.{v, v, u, u} (c₁, c₂) (Functor.diag C)
h : List.IsChain Zag.{v, u} [c₁, X.right, c₂]
⊢ List.IsChain Zag.{v, u} [c₁, X.right, c₂] ∧ [c₁, X.right, c₂].getLast ⋯ = c₂
have h₁ : [c₁, X.right, c₂].getLast sorry = c₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsSifted.{v, u} C
c₁ c₂ : C
X : StructuredArrow.{v, v, u, u} (c₁, c₂) (Functor.diag C)
⊢ List.IsChain Zag.{v, u} [c₁, X.right, c₂]
have h : Zag.{v, u} c₁ X.right
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsSifted.{v, u} C
c₁ c₂ : C
X : StructuredArrow.{v, v, u, u} (c₁, c₂) (Functor.diag C)
h : Zag.{v, u} c₁ X.right
⊢ List.IsChain Zag.{v, u} [c₁, X.right, c₂]
have h₁ : List.IsChain Zag.{v, u} [X.right, c₂]
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryCoproducts.{v, u} C
⊢ IsSiftedOrEmpty.{v, u} C
have out : ∀ (d : C × C), IsConnected (StructuredArrow.{v, v, u, u} d (Functor.diag C))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryCoproducts.{v, u} C
c₁ c₂ : C
⊢ IsConnected (StructuredArrow.{v, v, u, u} (c₁, c₂) (Functor.diag C))
have this : Nonempty (StructuredArrow.{v, v, u, u} (c₁, c₂) (Functor.diag C))
Tactic: haveI : _root_.Nonempty <| StructuredArrow (c₁, c₂) (diag C) :=
      ⟨.mk ((coprod.inl : c₁ ⟶ c₁ ⨿ c₂), (coprod.inr : c₂ ⟶ c₁ ⨿ c₂))⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryCoproducts.{v, u} C
c₁ c₂ : C
this : Nonempty (StructuredArrow.{v, v, u, u} (c₁, c₂) (Functor.diag C))
⊢ IsConnected (StructuredArrow.{v, v, u, u} (c₁, c₂) (Functor.diag C))
have out : ∀ (j₁ j₂ : StructuredArrow.{v, v, u, u} (c₁, c₂) (Functor.diag C)),
  ∃ (l : List (StructuredArrow.{v, v, u, u} (c₁, c₂) (Functor.diag C))),
    List.IsChain Zag (j₁ :: l) ∧ (j₁ :: l).getLast sorry = j₂
Tactic: apply isConnected_of_zigzag
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryCoproducts.{v, u} C
c₁ c₂ : C
this : Nonempty (StructuredArrow.{v, v, u, u} (c₁, c₂) (Functor.diag C))
left : Discrete PUnit.{1}
c : C
f : (c₁, c₂) ⟶ (c, c)
left_1 : Discrete PUnit.{1}
c' : C
g : (c₁, c₂) ⟶ (c', c')
⊢ ∃ (l : List (StructuredArrow.{v, v, u, u} (c₁, c₂) (Functor.diag C))),
    List.IsChain Zag
        ({ left := left, right := c, hom := f : Comma.{0, v, v, 0, u, u} (fromPUnit (c₁, c₂)) (Functor.diag C) } :: l) ∧
      ({ left := left, right := c, hom := f : Comma.{0, v, v, 0, u, u} (fromPUnit (c₁, c₂)) (Functor.diag C) } ::
              l).getLast
          ⋯ =
        { left := left_1, right := c', hom := g }
have h : List.IsChain (α := StructuredArrow.{v, v, u, u} (c₁, c₂) (Functor.diag C)) Zag
    [{ left := left, right := c, hom := f },
      StructuredArrow.mk (Y := (colimit.cocone (pair c₁ c₂)).1) (coprod.inl, coprod.inr),
      StructuredArrow.mk (g.1, g.2)] ∧
  Eq (α := StructuredArrow.{v, v, u, u} (c₁, c₂) (Functor.diag C))
    (List.getLast
      [{ left := left, right := c, hom := f },
        StructuredArrow.mk (Y := (colimit.cocone (pair c₁ c₂)).1) (coprod.inl, coprod.inr),
        StructuredArrow.mk (g.1, g.2)]
      sorry)
    { left := left_1, right := c', hom := g }
Tactic: use [.mk ((coprod.inl : c₁ ⟶ c₁ ⨿ c₂), (coprod.inr : c₂ ⟶ c₁ ⨿ c₂)), .mk (g.fst, g.snd)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryCoproducts.{v, u} C
c₁ c₂ : C
this : Nonempty (StructuredArrow.{v, v, u, u} (c₁, c₂) (Functor.diag C))
left : Discrete PUnit.{1}
c : C
f : (c₁, c₂) ⟶ (c, c)
left_1 : Discrete PUnit.{1}
c' : C
g : (c₁, c₂) ⟶ (c', c')
⊢ List.IsChain (α := StructuredArrow.{v, v, u, u} (c₁, c₂) (Functor.diag C)) Zag
      [{ left := left, right := c, hom := f },
        StructuredArrow.mk (Y := (colimit.cocone (pair c₁ c₂)).1) (coprod.inl, coprod.inr),
        StructuredArrow.mk (g.1, g.2)] ∧
    Eq (α := StructuredArrow.{v, v, u, u} (c₁, c₂) (Functor.diag C))
      (List.getLast
        [{ left := left, right := c, hom := f },
          StructuredArrow.mk (Y := (colimit.cocone (pair c₁ c₂)).1) (coprod.inl, coprod.inr),
          StructuredArrow.mk (g.1, g.2)]
        ⋯)
      { left := left_1, right := c', hom := g }
have h : (Zag (J := StructuredArrow.{v, v, u, u} (c₁, c₂) (Functor.diag C)) { left := left, right := c, hom := f }
      (StructuredArrow.mk (Y := colimit.{0, 0, v, u} (pair c₁ c₂)) (coprod.inl, coprod.inr)) ∧
    Zag (J := StructuredArrow.{v, v, u, u} (c₁, c₂) (Functor.diag C))
      (StructuredArrow.mk (Y := colimit.{0, 0, v, u} (pair c₁ c₂)) (coprod.inl, coprod.inr)) (StructuredArrow.mk g)) ∧
  Eq (α := StructuredArrow.{v, v, u, u} (c₁, c₂) (Functor.diag C)) (StructuredArrow.mk g)
    { left := left_1, right := c', hom := g }
Tactic: simp only [colimit.cocone_x, diag_obj, Prod.mk.eta, List.isChain_cons_cons,
      List.isChain_singleton, and_true, ne_eq, reduceCtorEq, not_false_eq_true,
      List.getLast_cons, List.cons_ne_self, List.getLast_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (goal)
Goal:
C : Type u
inst : SmallCategory C
X Y : C ⥤ Type u
⊢ Eq (α := colimit (obj (tensor (C ⥤ Type u)) (X, Y)) ⟶ obj (obj (curriedTensor (Type u)) (colimit X)) (colimit Y))
    (CategoryStruct.comp (Y :=
      colimit
        (obj (externalProductBifunctor C C (Type u) ⋙ obj (whiskeringLeft C (C × C) (Type u)) (Functor.diag C)) (X, Y)))
      (Iso.hom (HasColimit.isoOfNatIso (Iso.symm (Iso.app (externalProductCompDiagIso C (Type u)) (X, Y)))))
      (CategoryStruct.comp (Y := colimit (X ⊠ Y))
        (colimit.pre (X ⊠ Y) (Functor.diag C) : colimit (Functor.diag C ⋙ X ⊠ Y) ⟶ colimit (X ⊠ Y))
        (Iso.hom (PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂ X Y (curriedTensor (Type u))) :
          colimit (obj uncurry (obj (obj (obj (whiskeringLeft₂ (Type u)) X) Y) (curriedTensor (Type u)))) ⟶
            obj (obj (curriedTensor (Type u)) (colimit X)) (colimit Y))))
    (CartesianMonoidalCategory.prodComparison colim X Y)
have w : ∀ (j : C),
  Eq (α := (obj (tensor (C ⥤ Type u)) (X, Y)).obj j ⟶ obj (obj (curriedTensor (Type u)) (colimit X)) (colimit Y))
    (CategoryStruct.comp (Y := colimit (obj (tensor (C ⥤ Type u)) (X, Y)))
      (colimit.ι (obj (tensor (C ⥤ Type u)) (X, Y)) j)
      (CategoryStruct.comp (Y :=
        colimit
          (obj (externalProductBifunctor C C (Type u) ⋙ obj (whiskeringLeft C (C × C) (Type u)) (Functor.diag C))
            (X, Y)))
        (Iso.hom (HasColimit.isoOfNatIso (Iso.symm (Iso.app (externalProductCompDiagIso C (Type u)) (X, Y)))))
        (CategoryStruct.comp (Y := colimit (X ⊠ Y))
          (colimit.pre (X ⊠ Y) (Functor.diag C) : colimit (Functor.diag C ⋙ X ⊠ Y) ⟶ colimit (X ⊠ Y))
          (Iso.hom (PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂ X Y (curriedTensor (Type u))) :
            colimit (obj uncurry (obj (obj (obj (whiskeringLeft₂ (Type u)) X) Y) (curriedTensor (Type u)))) ⟶
              obj (obj (curriedTensor (Type u)) (colimit X)) (colimit Y)))))
    (CategoryStruct.comp (Y := colimit (obj (tensor (C ⥤ Type u)) (X, Y)))
      (colimit.ι (obj (tensor (C ⥤ Type u)) (X, Y)) j) (CartesianMonoidalCategory.prodComparison colim X Y))
Tactic: apply colimit.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (goal)
Goal:
C : Type u
inst : SmallCategory C
X Y : C ⥤ Type u
j : C
⊢ Eq (α := (obj (tensor (C ⥤ Type u)) (X, Y)).obj j ⟶ obj (obj (curriedTensor (Type u)) (colimit X)) (colimit Y))
    (CategoryStruct.comp (Y := colimit (obj (tensor (C ⥤ Type u)) (X, Y)))
      (colimit.ι (obj (tensor (C ⥤ Type u)) (X, Y)) j)
      (CategoryStruct.comp (Y :=
        colimit
          (obj (externalProductBifunctor C C (Type u) ⋙ obj (whiskeringLeft C (C × C) (Type u)) (Functor.diag C))
            (X, Y)))
        (Iso.hom (HasColimit.isoOfNatIso (Iso.symm (Iso.app (externalProductCompDiagIso C (Type u)) (X, Y)))))
        (CategoryStruct.comp (Y := colimit (X ⊠ Y))
          (colimit.pre (X ⊠ Y) (Functor.diag C) : colimit (Functor.diag C ⋙ X ⊠ Y) ⟶ colimit (X ⊠ Y))
          (Iso.hom (PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂ X Y (curriedTensor (Type u))) :
            colimit (obj uncurry (obj (obj (obj (whiskeringLeft₂ (Type u)) X) Y) (curriedTensor (Type u)))) ⟶
              obj (obj (curriedTensor (Type u)) (colimit X)) (colimit Y)))))
    (CategoryStruct.comp (Y := colimit (obj (tensor (C ⥤ Type u)) (X, Y)))
      (colimit.ι (obj (tensor (C ⥤ Type u)) (X, Y)) j) (CartesianMonoidalCategory.prodComparison colim X Y))
have w : Eq (α := tensorObj (𝒞 := types) (X.obj j) (Y.obj j) ⟶ tensorObj (𝒞 := types) (colimit X) (colimit Y))
  (CategoryStruct.comp (Y := colimit (tensorObj (𝒞 := category) X Y)) (colimit.ι (tensorObj (𝒞 := category) X Y) j)
    (CategoryStruct.comp (Y :=
      colimit (Functor.diag C ⋙ obj uncurry (obj (obj (obj (whiskeringLeft₂ (Type u)) X) Y) (curriedTensor (Type u)))))
      (Iso.hom (HasColimit.isoOfNatIso (Iso.symm (Iso.app (externalProductCompDiagIso C (Type u)) (X, Y)))))
      (CategoryStruct.comp (Y :=
        colimit (obj uncurry (obj (obj (obj (whiskeringLeft₂ (Type u)) X) Y) (curriedTensor (Type u)))))
        (colimit.pre (obj uncurry (obj (obj (obj (whiskeringLeft₂ (Type u)) X) Y) (curriedTensor (Type u))))
            (Functor.diag C) :
          colimit
              (Functor.diag C ⋙ obj uncurry (obj (obj (obj (whiskeringLeft₂ (Type u)) X) Y) (curriedTensor (Type u)))) ⟶
            colimit (obj uncurry (obj (obj (obj (whiskeringLeft₂ (Type u)) X) Y) (curriedTensor (Type u)))))
        (Iso.hom (PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂ X Y (curriedTensor (Type u))) :
          colimit (obj uncurry (obj (obj (obj (whiskeringLeft₂ (Type u)) X) Y) (curriedTensor (Type u)))) ⟶
            tensorObj (𝒞 := types) (colimit X) (colimit Y)))))
  (CategoryStruct.comp (Y := colimit (tensorObj (𝒞 := category) X Y)) (colimit.ι (tensorObj (𝒞 := category) X Y) j)
    (lift (colimMap (fst X Y)) (colimMap (snd X Y))))
Tactic: dsimp [externalProductBifunctor, CartesianMonoidalCategory.prodComparison,
    externalProductBifunctorCurried, externalProduct]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (goal)
Goal:
C : Type u
inst : SmallCategory C
X Y : C ⥤ Type u
inst_1 : IsSifted C
⊢ IsIso (X := obj colim (tensorObj (𝒞 := category) X Y)) (Y := tensorObj (𝒞 := types) (obj colim X) (obj colim Y))
    (CartesianMonoidalCategory.prodComparison colim X Y)
have rw : IsIso (X := obj colim (tensorObj (𝒞 := category) X Y)) (Y := tensorObj (𝒞 := types) (obj colim X) (obj colim Y))
  (CategoryStruct.comp (Y :=
    colimit
      (obj (externalProductBifunctor C C (Type u) ⋙ obj (whiskeringLeft C (C × C) (Type u)) (Functor.diag C)) (X, Y)))
    (Iso.hom (HasColimit.isoOfNatIso (Iso.symm (Iso.app (externalProductCompDiagIso C (Type u)) (X, Y)))))
    (CategoryStruct.comp (Y := colimit (X ⊠ Y))
      (colimit.pre (X ⊠ Y) (Functor.diag C) : colimit (Functor.diag C ⋙ X ⊠ Y) ⟶ colimit (X ⊠ Y))
      (Iso.hom (PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂ X Y (curriedTensor (Type u))) :
        colimit (obj uncurry (obj (obj (obj (whiskeringLeft₂ (Type u)) X) Y) (curriedTensor (Type u)))) ⟶
          obj (obj (curriedTensor (Type u)) (colimit X)) (colimit Y))))
Tactic: rw [← factorization_prodComparison_colim]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (goal)
Goal:
C : Type u
inst : SmallCategory C
X Y : C ⥤ Type u
inst_1 : IsSifted C
⊢ PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete WalkingPair) colim
have preservesLimit : autoParam (∀ {K : Discrete WalkingPair ⥤ C ⥤ Type u}, PreservesLimit K colim)
  PreservesLimitsOfShape.preservesLimit._autoParam
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (goal)
Goal:
C : Type u
inst : SmallCategory C
X Y : C ⥤ Type u
inst_1 : IsSifted C
⊢ PreservesLimit.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (empty (C ⥤ Type u)) colim
have f : obj (C := C ⥤ Type u) colim (⊤_ C ⥤ Type u) ≅ ⊤_ Type u
Tactic: apply preservesTerminal_of_iso
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (goal)
Goal:
C : Type u
inst : SmallCategory C
X Y : C ⥤ Type u
inst_1 : IsSifted C
⊢ obj (C := C ⥤ Type u) colim (⊤_ C ⥤ Type u) ≅ ⊤_ Type u
have f : ⊤_ Type u ≅ obj (C := C ⥤ Type u) colim (⊤_ C ⥤ Type u)
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (goal)
Goal:
C : Type u
inst : SmallCategory C
X Y : C ⥤ Type u
inst_1 : IsSifted C
⊢ ⊤_ Type u ≅ obj (C := C ⥤ Type u) colim (⊤_ C ⥤ Type u)
have f : PUnit.{u + 1} ≅ obj (C := C ⥤ Type u) colim (⊤_ C ⥤ Type u)
Tactic: apply (_ : ⊤_ (Type u) ≅ PUnit.{u + 1}).trans
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (goal)
Goal:
C : Type u
inst : SmallCategory C
X Y : C ⥤ Type u
inst_1 : IsSifted C
f : PUnit.{u + 1} ≅ obj (C := C ⥤ Type u) colim (⊤_ C ⥤ Type u)
⊢ ⊤_ Type u ≅ obj (C := C ⥤ Type u) colim (⊤_ C ⥤ Type u)
have apply : ⊤_ Type u ≅ PUnit.{u + 1}
Tactic: apply (_ : ⊤_ (Type u) ≅ PUnit.{u + 1}).trans