awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
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
⊢ f = 𝟙 0

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroObject.{v, u} C
⊢ HasInitial.{v, u} C

Tactic:
hasInitial_of_unique 0

Premises used: CategoryTheory.Limits.hasInitial_of_unique, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroObject.{v, u} C
⊢ HasTerminal.{v, u} C

Tactic:
hasTerminal_of_unique 0

Premises used: CategoryTheory.Limits.hasTerminal_of_unique, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroObject.{v, u} C
X : C
⊢ Mono.{v, u} (X := 0) (IsInitial.to zeroIsInitial X)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
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
⊢ IsZero F ↔ ∀ (X : C), IsZero.{v', u'} (F.obj X)

Tactic:
⟨fun hF X => hF.obj X, Functor.isZero _⟩

Premises used: CategoryTheory.Functor.isZero, CategoryTheory.Limits.IsZero.obj, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
D : Type u'
inst_1 : Category.{v', u'} D
C : Type u_1
inst_2 : Category.{v_1, u_1} C
A : C
inst_3 : HasZeroObject.{v_1, u_1} C
⊢ Epi.{v_1, u_1} (Y := terminal.{v_1, u_1} C) (IsTerminal.from terminalIsTerminal A)

Tactic:
(((isZero_zero C).of_iso HasZeroObject.zeroIsoTerminal.symm).epi _)

Premises used: CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal, CategoryTheory.Limits.isZero_zero, CategoryTheory.Limits.IsZero.epi, CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Limits.Sifted
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
dsimp : (e.functor.obj (e.inverse.obj c), e.functor.obj (e.inverse.obj c)) ≅ (c, c)
⊢ (e.inverse ⋙ Functor.diag D ⋙ this.functor).obj c ≅ obj.{v, v, u, u} (Functor.diag C) c

Tactic:
dsimp [this]
-- Module: Mathlib.CategoryTheory.Limits.Sifted
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.functor.obj (e.inverse.obj c), e.functor.obj (e.inverse.obj c)) ≅ (c, c)

Tactic:
exact Iso.prod (e.counitIso.app c) (e.counitIso.app c)

Premises used: CategoryTheory.Iso.prod, CategoryTheory.Iso.app, CategoryTheory.Equivalence.counitIso
-- Module: Mathlib.CategoryTheory.Limits.Sifted
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
have : ∀ (sq : e.inverse ⋙ Functor.diag D ⋙ this.functor ≅ Functor.diag C), Final.{v₁, v₁, u₁, u₁} (Functor.diag D)
⊢ 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))
-- Module: Mathlib.CategoryTheory.Limits.Sifted
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
sq : e.inverse ⋙ Functor.diag D ⋙ this.functor ≅ Functor.diag C
⊢ Final.{v₁, v₁, u₁, u₁} (Functor.diag D)

Tactic:
apply_rules [final_iff_comp_equivalence _ this.functor |>.mpr,
      final_iff_final_comp e.inverse _ |>.mpr, final_of_natIso sq.symm]

Premises used: Iff.mpr, CategoryTheory.Functor.final_iff_comp_equivalence, CategoryTheory.Functor.final_of_natIso, CategoryTheory.Equivalence.functor, CategoryTheory.Functor.final_iff_final_comp, CategoryTheory.Iso.symm, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsSifted.{v, u} C
c₁ c₂ : C
⊢ Final.{v, v, u, u} (Functor.diag C)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsSifted.{v, u} C
c₁ c₂ : C
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 ⋯ = c₂
⊢ ∃ (l : List C), List.IsChain Zag.{v, u} (c₁ :: l) ∧ (c₁ :: l).getLast ⋯ = 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
-- Module: Mathlib.CategoryTheory.Limits.Sifted
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₂] ∧ [c₁, X.right, c₂].getLast ⋯ = c₂
⊢ ∃ (l : List C), List.IsChain Zag.{v, u} (c₁ :: l) ∧ (c₁ :: l).getLast ⋯ = c₂

Tactic:
use [X.right, c₂]

Premises used: CategoryTheory.StructuredArrow.right
-- Module: Mathlib.CategoryTheory.Limits.Sifted
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₂]
h₁ : [c₁, X.right, c₂].getLast ⋯ = c₂
⊢ List.IsChain Zag.{v, u} [c₁, X.right, c₂] ∧ [c₁, X.right, c₂].getLast ⋯ = c₂

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Sifted
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
h₁ : List.IsChain Zag.{v, u} [X.right, c₂]
⊢ List.IsChain Zag.{v, u} [c₁, X.right, c₂]

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Sifted
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)
⊢ Zag.{v, u} c₁ X.right

Tactic:
Zag.of_hom X.hom.fst

Premises used: CategoryTheory.StructuredArrow.hom, Prod.fst, CategoryTheory.Zag.of_hom
-- Module: Mathlib.CategoryTheory.Limits.Sifted
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)
⊢ Zag.{v, u} c₁ X.right

Tactic:
exact Zag.of_hom X.hom.fst

Premises used: CategoryTheory.StructuredArrow.hom, Prod.fst, CategoryTheory.Zag.of_hom
-- Module: Mathlib.CategoryTheory.Limits.Sifted
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} [X.right, c₂]

Tactic:
simpa using Zag.of_inv X.hom.snd

Premises used: CategoryTheory.StructuredArrow.hom, Prod.snd, CategoryTheory.Zag.of_inv
-- Module: Mathlib.CategoryTheory.Limits.Sifted
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)
⊢ [c₁, X.right, c₂].getLast ⋯ = c₂

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryCoproducts.{v, u} C
out : ∀ (d : C × C), IsConnected (StructuredArrow.{v, v, u, u} d (Functor.diag C))
⊢ IsSiftedOrEmpty.{v, u} C

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryCoproducts.{v, u} C
c₁ c₂ : C
⊢ 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₂))⟩
-- Module: Mathlib.CategoryTheory.Limits.Sifted
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))
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 ⋯ = j₂
⊢ IsConnected (StructuredArrow.{v, v, u, u} (c₁, c₂) (Functor.diag C))

Tactic:
apply isConnected_of_zigzag

Premises used: CategoryTheory.isConnected_of_zigzag
-- Module: Mathlib.CategoryTheory.Limits.Sifted
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')
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)]
        ⋯)
      { left := left_1, right := c', hom := g }
⊢ ∃ (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 }

Tactic:
use [.mk ((coprod.inl : c₁ ⟶ c₁ ⨿ c₂), (coprod.inr : c₂ ⟶ c₁ ⨿ c₂)), .mk (g.fst, g.snd)]
-- Module: Mathlib.CategoryTheory.Limits.Sifted
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')
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 }
⊢ 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 }

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]

Premises used: reduceCtorEq, List.isChain_singleton, and_true, List.cons_ne_self, ne_eq, List.isChain_cons_cons, List.getLast_cons, Prod.mk.eta, CategoryTheory.Limits.colimit.cocone_x, CategoryTheory.Functor.diag_obj, List.getLast_singleton, not_false_eq_true
-- Module: Mathlib.CategoryTheory.Limits.Sifted
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')
⊢ (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:
⟨⟨Zag.of_inv <| StructuredArrow.homMk <| coprod.desc f.fst f.snd,
      Zag.of_hom <| StructuredArrow.homMk <| coprod.desc g.fst g.snd⟩, rfl⟩

Premises used: CategoryTheory.StructuredArrow.homMk, CategoryTheory.Limits.coprod.desc, Prod.fst, And.intro, Prod.snd, CategoryTheory.Zag.of_hom, CategoryTheory.Zag.of_inv, rfl
-- Module: Mathlib.CategoryTheory.Limits.Sifted
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')
⊢ (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:
exact ⟨⟨Zag.of_inv <| StructuredArrow.homMk <| coprod.desc f.fst f.snd,
      Zag.of_hom <| StructuredArrow.homMk <| coprod.desc g.fst g.snd⟩, rfl⟩
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
inst_2 : IsSiftedOrEmpty.{v, u} C
inst_3 : IsSiftedOrEmpty.{v₁, u₁} D
⊢ IsSiftedOrEmpty (C × D)

Tactic:
let e : (C × C) × (D × D) ≌ (C × D) × (C × D) := prod.prodμ ..
  final_of_natIso (Iso.refl ((Functor.diag C).prod (Functor.diag D) ⋙ e.functor))

Premises used: CategoryTheory.Functor.diag, CategoryTheory.Functor.final_of_natIso, CategoryTheory.Functor.comp, CategoryTheory.Iso.refl, CategoryTheory.Equivalence.functor, CategoryTheory.Functor.prod, CategoryTheory.prod.prodμ
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsSiftedOrEmpty.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
D' : Type u₂
inst_3 : Category.{v₂, u₂} D'
F : Functor.{v, v₁, u, u₁} C D
G : Functor.{v, v₂, u, u₂} C D'
inst_4 : F.Final
inst_5 : G.Final
⊢ (F.prod' G).Final

Tactic:
show (diag C ⋙ F.prod G).Final from final_comp _ _

Premises used: CategoryTheory.Functor.diag, CategoryTheory.Functor.comp, CategoryTheory.Functor.prod, CategoryTheory.Functor.prod', CategoryTheory.Functor.final_comp
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
X Y : C ⥤ Type u
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))
⊢ 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)

Tactic:
apply colimit.hom_ext

Premises used: CategoryTheory.Limits.colimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
X Y : C ⥤ Type u
j : C
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))))
⊢ 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:
dsimp [externalProductBifunctor, CartesianMonoidalCategory.prodComparison,
    externalProductBifunctorCurried, externalProduct]

Premises used: CategoryTheory.MonoidalCategory.externalProductBifunctor, CategoryTheory.MonoidalCategory.externalProductBifunctorCurried, CategoryTheory.MonoidalCategory.externalProduct, CategoryTheory.CartesianMonoidalCategory.prodComparison
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
X Y : C ⥤ Type u
inst_1 : IsSifted C
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))))
⊢ IsIso (X := obj colim (tensorObj (𝒞 := category) X Y)) (Y := tensorObj (𝒞 := types) (obj colim X) (obj colim Y))
    (CartesianMonoidalCategory.prodComparison colim X Y)

Tactic:
rw [← factorization_prodComparison_colim]

Premises used: CategoryTheory.IsSifted.factorization_prodComparison_colim
-- Module: Mathlib.CategoryTheory.Limits.Sifted
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))
    (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:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
X_1 Y_1 : C ⥤ Type u
inst_1 : IsSifted C
X Y : C ⥤ Type u
⊢ PreservesLimit (pair X Y) colim

Tactic:
preservesLimit_pair_of_isIso_prodComparison _ _ _

Premises used: CategoryTheory.CartesianMonoidalCategory.preservesLimit_pair_of_isIso_prodComparison
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
X Y : C ⥤ Type u
inst_1 : IsSifted C
preservesLimit :
  autoParam (∀ {K : Discrete WalkingPair ⥤ C ⥤ Type u}, PreservesLimit K colim)
    PreservesLimitsOfShape.preservesLimit._autoParam
⊢ PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete WalkingPair) colim

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
X Y : C ⥤ Type u
inst_1 : IsSifted C
F : Discrete WalkingPair ⥤ C ⥤ Type u
⊢ PreservesLimit F colim

Tactic:
apply preservesLimit_of_iso_diagram colim (diagramIsoPair F).symm

Premises used: CategoryTheory.Limits.colim, CategoryTheory.Limits.preservesLimit_of_iso_diagram, CategoryTheory.Iso.symm, CategoryTheory.Limits.diagramIsoPair