awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
inst_2 : HasBinaryProducts.{v, u} C
X Y : C
⊢ Eq.{v + 1} (α := prod.{v, u} (prod.{v, u} X (terminal.{v, u} C)) Y ⟶ X)
    (CategoryStruct.comp (Y := prod.{v, u} X Y)
        (CategoryStruct.comp (Y := prod.{v, u} X (prod.{v, u} (terminal.{v, u} C) Y))
          (Iso.hom (associator X (terminal.{v, u} C) Y) :
            prod.{v, u} (prod.{v, u} X (terminal.{v, u} C)) Y ⟶ prod.{v, u} X (prod.{v, u} (terminal.{v, u} C) Y))
          (map (𝟙 X) (Iso.hom (leftUnitor Y)) : prod.{v, u} X (prod.{v, u} (terminal.{v, u} C) Y) ⟶ prod.{v, u} X Y))
        fst :
      prod.{v, u} (prod.{v, u} X (terminal.{v, u} C)) Y ⟶ X)
    (CategoryStruct.comp (Y := prod.{v, u} X Y) (map (Iso.hom (rightUnitor X)) (𝟙 Y)) fst :
      prod.{v, u} (prod.{v, u} X (terminal.{v, u} C)) Y ⟶ X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
inst_2 : HasBinaryProducts.{v, u} C
X Y : C
⊢ Eq.{v + 1} (α := prod.{v, u} (prod.{v, u} X (terminal.{v, u} C)) Y ⟶ Y)
    (CategoryStruct.comp (Y := prod.{v, u} X Y)
        (CategoryStruct.comp (Y := prod.{v, u} X (prod.{v, u} (terminal.{v, u} C) Y))
          (Iso.hom (associator X (terminal.{v, u} C) Y) :
            prod.{v, u} (prod.{v, u} X (terminal.{v, u} C)) Y ⟶ prod.{v, u} X (prod.{v, u} (terminal.{v, u} C) Y))
          (map (𝟙 X) (Iso.hom (leftUnitor Y)) : prod.{v, u} X (prod.{v, u} (terminal.{v, u} C) Y) ⟶ prod.{v, u} X Y))
        snd :
      prod.{v, u} (prod.{v, u} X (terminal.{v, u} C)) Y ⟶ Y)
    (CategoryStruct.comp (Y := prod.{v, u} X Y) (map (Iso.hom (rightUnitor X)) (𝟙 Y)) snd :
      prod.{v, u} (prod.{v, u} X (terminal.{v, u} C)) Y ⟶ Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryCoproducts.{v, u} C
P Q : C
⊢ CategoryStruct.comp (Y := coprod.{v, u} Q P) (desc inr inl) (desc inr inl) = 𝟙 (coprod.{v, u} P Q)

Tactic:
(coprod.braiding _ _).hom_inv_id

Premises used: CategoryTheory.Limits.coprod.braiding, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Limits.colimit.desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryCoproducts.{v, u} C
P Q : C
⊢ Eq (α := coprod.{v, u} P Q ⟶ coprod.{v, u} P Q)
    (CategoryStruct.comp (Y := coprod.{v, u} Q P) (Iso.hom (braiding P Q) : coprod.{v, u} P Q ⟶ coprod.{v, u} Q P)
        (Iso.hom (braiding Q P) : coprod.{v, u} Q P ⟶ coprod.{v, u} P Q) :
      coprod.{v, u} P Q ⟶ coprod.{v, u} P Q)
    (𝟙 (coprod.{v, u} P Q) : coprod.{v, u} P Q ⟶ coprod.{v, u} P Q)

Tactic:
coprod.symmetry' _ _

Premises used: CategoryTheory.Limits.colimit.desc, CategoryTheory.Limits.coprod.symmetry'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryCoproducts.{v, u} C
W X Y Z : C
⊢ Eq (α :=
    coprod.{v, u} (coprod.{v, u} (coprod.{v, u} W X) Y) Z ⟶ coprod.{v, u} W (coprod.{v, u} X (coprod.{v, u} Y Z)))
    (CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} W (coprod.{v, u} X Y)) Z)
        (map (Iso.hom (associator W X Y)) (𝟙 Z) :
          coprod.{v, u} (coprod.{v, u} (coprod.{v, u} W X) Y) Z ⟶ coprod.{v, u} (coprod.{v, u} W (coprod.{v, u} X Y)) Z)
        (CategoryStruct.comp (Y := coprod.{v, u} W (coprod.{v, u} (coprod.{v, u} X Y) Z))
            (Iso.hom (associator W (coprod.{v, u} X Y) Z) :
              coprod.{v, u} (coprod.{v, u} W (coprod.{v, u} X Y)) Z ⟶
                coprod.{v, u} W (coprod.{v, u} (coprod.{v, u} X Y) Z))
            (map (𝟙 W) (Iso.hom (associator X Y Z)) :
              coprod.{v, u} W (coprod.{v, u} (coprod.{v, u} X Y) Z) ⟶
                coprod.{v, u} W (coprod.{v, u} X (coprod.{v, u} Y Z))) :
          coprod.{v, u} (coprod.{v, u} W (coprod.{v, u} X Y)) Z ⟶
            coprod.{v, u} W (coprod.{v, u} X (coprod.{v, u} Y Z))) :
      coprod.{v, u} (coprod.{v, u} (coprod.{v, u} W X) Y) Z ⟶ coprod.{v, u} W (coprod.{v, u} X (coprod.{v, u} Y Z)))
    (CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} W X) (coprod.{v, u} Y Z))
        (Iso.hom (associator (coprod.{v, u} W X) Y Z) :
          coprod.{v, u} (coprod.{v, u} (coprod.{v, u} W X) Y) Z ⟶ coprod.{v, u} (coprod.{v, u} W X) (coprod.{v, u} Y Z))
        (Iso.hom (associator W X (coprod.{v, u} Y Z)) :
          coprod.{v, u} (coprod.{v, u} W X) (coprod.{v, u} Y Z) ⟶
            coprod.{v, u} W (coprod.{v, u} X (coprod.{v, u} Y Z))) :
      coprod.{v, u} (coprod.{v, u} (coprod.{v, u} W X) Y) Z ⟶ coprod.{v, u} W (coprod.{v, u} X (coprod.{v, u} Y Z)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryCoproducts.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ Eq (α := coprod.{v, u} (coprod.{v, u} X₁ X₂) X₃ ⟶ coprod.{v, u} Y₁ (coprod.{v, u} Y₂ Y₃))
    (CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} Y₁ Y₂) Y₃)
        (map (map f₁ f₂) f₃ : coprod.{v, u} (coprod.{v, u} X₁ X₂) X₃ ⟶ coprod.{v, u} (coprod.{v, u} Y₁ Y₂) Y₃)
        (Iso.hom (associator Y₁ Y₂ Y₃) :
          coprod.{v, u} (coprod.{v, u} Y₁ Y₂) Y₃ ⟶ coprod.{v, u} Y₁ (coprod.{v, u} Y₂ Y₃)) :
      coprod.{v, u} (coprod.{v, u} X₁ X₂) X₃ ⟶ coprod.{v, u} Y₁ (coprod.{v, u} Y₂ Y₃))
    (CategoryStruct.comp (Y := coprod.{v, u} X₁ (coprod.{v, u} X₂ X₃))
        (Iso.hom (associator X₁ X₂ X₃) :
          coprod.{v, u} (coprod.{v, u} X₁ X₂) X₃ ⟶ coprod.{v, u} X₁ (coprod.{v, u} X₂ X₃))
        (map f₁ (map f₂ f₃) : coprod.{v, u} X₁ (coprod.{v, u} X₂ X₃) ⟶ coprod.{v, u} Y₁ (coprod.{v, u} Y₂ Y₃)) :
      coprod.{v, u} (coprod.{v, u} X₁ X₂) X₃ ⟶ coprod.{v, u} Y₁ (coprod.{v, u} Y₂ Y₃))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryCoproducts.{v, u} C
inst_2 : HasInitial.{v, u} C
P : C
h₁ :
  CategoryStruct.comp (Y := coprod.{v, u} (initial.{v, u} C) P) inl (desc (initial.to P) (𝟙 P) ≫ inr) =
    inl ≫ 𝟙 (coprod.{v, u} (initial.{v, u} C) P)
h₂ :
  CategoryStruct.comp (Y := coprod.{v, u} (initial.{v, u} C) P) inr (desc (initial.to P) (𝟙 P) ≫ inr) =
    inr ≫ 𝟙 (coprod.{v, u} (initial.{v, u} C) P)
⊢ desc (initial.to P) (𝟙 P) ≫ inr = 𝟙 (coprod.{v, u} (initial.{v, u} C) P)

Tactic:
apply coprod.hom_ext

Premises used: CategoryTheory.Limits.coprod.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryCoproducts.{v, u} C
inst_2 : HasInitial.{v, u} C
P : C
⊢ CategoryStruct.comp (Y := coprod.{v, u} (initial.{v, u} C) P) inl (desc (initial.to P) (𝟙 P) ≫ inr) =
    inl ≫ 𝟙 (coprod.{v, u} (initial.{v, u} C) P)

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryCoproducts.{v, u} C
inst_2 : HasInitial.{v, u} C
P : C
⊢ CategoryStruct.comp (Y := coprod.{v, u} (initial.{v, u} C) P) inr (desc (initial.to P) (𝟙 P) ≫ inr) =
    inr ≫ 𝟙 (coprod.{v, u} (initial.{v, u} C) P)

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryCoproducts.{v, u} C
inst_2 : HasInitial.{v, u} C
P : C
⊢ Eq.{v + 1} (α := P ⟶ P)
    (CategoryStruct.comp (Y := coprod.{v, u} (initial.{v, u} C) P) inr (desc (initial.to P) (𝟙 P))) (𝟙 P)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryCoproducts.{v, u} C
inst_2 : HasInitial.{v, u} C
f : X ⟶ Y
⊢ Eq (α := coprod.{v, u} (initial.{v, u} C) X ⟶ Y)
    (CategoryStruct.comp (Y := coprod.{v, u} (initial.{v, u} C) Y)
        (map (𝟙 (initial.{v, u} C)) f : coprod.{v, u} (initial.{v, u} C) X ⟶ coprod.{v, u} (initial.{v, u} C) Y)
        (Iso.hom (leftUnitor Y) : coprod.{v, u} (initial.{v, u} C) Y ⟶ Y) :
      coprod.{v, u} (initial.{v, u} C) X ⟶ Y)
    (Iso.hom (leftUnitor X) ≫ f : coprod.{v, u} (initial.{v, u} C) X ⟶ Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryCoproducts.{v, u} C
inst_2 : HasInitial.{v, u} C
P : C
h₁ :
  CategoryStruct.comp (Y := coprod.{v, u} P (initial.{v, u} C)) inl (desc (𝟙 P) (initial.to P) ≫ inl) =
    inl ≫ 𝟙 (coprod.{v, u} P (initial.{v, u} C))
h₂ :
  CategoryStruct.comp (Y := coprod.{v, u} P (initial.{v, u} C)) inr (desc (𝟙 P) (initial.to P) ≫ inl) =
    inr ≫ 𝟙 (coprod.{v, u} P (initial.{v, u} C))
⊢ desc (𝟙 P) (initial.to P) ≫ inl = 𝟙 (coprod.{v, u} P (initial.{v, u} C))

Tactic:
apply coprod.hom_ext

Premises used: CategoryTheory.Limits.coprod.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryCoproducts.{v, u} C
inst_2 : HasInitial.{v, u} C
P : C
⊢ CategoryStruct.comp (Y := coprod.{v, u} P (initial.{v, u} C)) inl (desc (𝟙 P) (initial.to P) ≫ inl) =
    inl ≫ 𝟙 (coprod.{v, u} P (initial.{v, u} C))

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryCoproducts.{v, u} C
inst_2 : HasInitial.{v, u} C
P : C
⊢ CategoryStruct.comp (Y := coprod.{v, u} P (initial.{v, u} C)) inr (desc (𝟙 P) (initial.to P) ≫ inl) =
    inr ≫ 𝟙 (coprod.{v, u} P (initial.{v, u} C))

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryCoproducts.{v, u} C
inst_2 : HasInitial.{v, u} C
P : C
⊢ Eq.{v + 1} (α := P ⟶ P)
    (CategoryStruct.comp (Y := coprod.{v, u} P (initial.{v, u} C)) inl (desc (𝟙 P) (initial.to P))) (𝟙 P)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryCoproducts.{v, u} C
inst_2 : HasInitial.{v, u} C
f : X ⟶ Y
⊢ Eq (α := coprod.{v, u} X (initial.{v, u} C) ⟶ Y)
    (CategoryStruct.comp (Y := coprod.{v, u} Y (initial.{v, u} C))
        (map f (𝟙 (initial.{v, u} C)) : coprod.{v, u} X (initial.{v, u} C) ⟶ coprod.{v, u} Y (initial.{v, u} C))
        (Iso.hom (rightUnitor Y) : coprod.{v, u} Y (initial.{v, u} C) ⟶ Y) :
      coprod.{v, u} X (initial.{v, u} C) ⟶ Y)
    (Iso.hom (rightUnitor X) ≫ f : coprod.{v, u} X (initial.{v, u} C) ⟶ Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryCoproducts.{v, u} C
inst_2 : HasInitial.{v, u} C
X Y : C
h₁ :
  Eq.{v + 1} (α := X ⟶ coprod.{v, u} X Y)
    (CategoryStruct.comp (Y := coprod.{v, u} X (initial.{v, u} C)) (inl : X ⟶ coprod.{v, u} X (initial.{v, u} C))
      (CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y)
          (inl : coprod.{v, u} X (initial.{v, u} C) ⟶ coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y)
          (CategoryStruct.comp (Y := coprod.{v, u} X (coprod.{v, u} (initial.{v, u} C) Y))
              (Iso.hom (associator X (initial.{v, u} C) Y) :
                coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y ⟶
                  coprod.{v, u} X (coprod.{v, u} (initial.{v, u} C) Y))
              (map (𝟙 X) (Iso.hom (leftUnitor Y)) :
                coprod.{v, u} X (coprod.{v, u} (initial.{v, u} C) Y) ⟶ coprod.{v, u} X Y) :
            coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y ⟶ coprod.{v, u} X Y) :
        coprod.{v, u} X (initial.{v, u} C) ⟶ coprod.{v, u} X Y))
    (CategoryStruct.comp (Y := coprod.{v, u} X (initial.{v, u} C)) (inl : X ⟶ coprod.{v, u} X (initial.{v, u} C))
      (CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y) inl
          (map (Iso.hom (rightUnitor X)) (𝟙 Y)) :
        coprod.{v, u} X (initial.{v, u} C) ⟶ coprod.{v, u} X Y))
h₂ :
  Eq.{v + 1} (α := Y ⟶ coprod.{v, u} X Y)
    (CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y)
      (inr : Y ⟶ coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y)
      (CategoryStruct.comp (Y := coprod.{v, u} X (coprod.{v, u} (initial.{v, u} C) Y))
          (Iso.hom (associator X (initial.{v, u} C) Y) :
            coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y ⟶ coprod.{v, u} X (coprod.{v, u} (initial.{v, u} C) Y))
          (map (𝟙 X) (Iso.hom (leftUnitor Y)) :
            coprod.{v, u} X (coprod.{v, u} (initial.{v, u} C) Y) ⟶ coprod.{v, u} X Y) :
        coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y ⟶ coprod.{v, u} X Y))
    (CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y)
      (inr : Y ⟶ coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y)
      (map (Iso.hom (rightUnitor X)) (𝟙 Y) : coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y ⟶ coprod.{v, u} X Y))
⊢ Eq.{v + 1} (α := coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y ⟶ coprod.{v, u} X Y)
    (CategoryStruct.comp (Y := coprod.{v, u} X (coprod.{v, u} (initial.{v, u} C) Y))
        (Iso.hom (associator X (initial.{v, u} C) Y) :
          coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y ⟶ coprod.{v, u} X (coprod.{v, u} (initial.{v, u} C) Y))
        (map (𝟙 X) (Iso.hom (leftUnitor Y)) :
          coprod.{v, u} X (coprod.{v, u} (initial.{v, u} C) Y) ⟶ coprod.{v, u} X Y) :
      coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y ⟶ coprod.{v, u} X Y)
    (map (Iso.hom (rightUnitor X)) (𝟙 Y) : coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y ⟶ coprod.{v, u} X Y)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryCoproducts.{v, u} C
inst_2 : HasInitial.{v, u} C
X Y : C
⊢ Eq.{v + 1} (α := X ⟶ coprod.{v, u} X Y)
    (CategoryStruct.comp (Y := coprod.{v, u} X (initial.{v, u} C)) (inl : X ⟶ coprod.{v, u} X (initial.{v, u} C))
      (CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y)
          (inl : coprod.{v, u} X (initial.{v, u} C) ⟶ coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y)
          (CategoryStruct.comp (Y := coprod.{v, u} X (coprod.{v, u} (initial.{v, u} C) Y))
              (Iso.hom (associator X (initial.{v, u} C) Y) :
                coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y ⟶
                  coprod.{v, u} X (coprod.{v, u} (initial.{v, u} C) Y))
              (map (𝟙 X) (Iso.hom (leftUnitor Y)) :
                coprod.{v, u} X (coprod.{v, u} (initial.{v, u} C) Y) ⟶ coprod.{v, u} X Y) :
            coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y ⟶ coprod.{v, u} X Y) :
        coprod.{v, u} X (initial.{v, u} C) ⟶ coprod.{v, u} X Y))
    (CategoryStruct.comp (Y := coprod.{v, u} X (initial.{v, u} C)) (inl : X ⟶ coprod.{v, u} X (initial.{v, u} C))
      (CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y) inl
          (map (Iso.hom (rightUnitor X)) (𝟙 Y)) :
        coprod.{v, u} X (initial.{v, u} C) ⟶ coprod.{v, u} X Y))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryCoproducts.{v, u} C
inst_2 : HasInitial.{v, u} C
X Y : C
⊢ Eq.{v + 1} (α := Y ⟶ coprod.{v, u} X Y)
    (CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y)
      (inr : Y ⟶ coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y)
      (CategoryStruct.comp (Y := coprod.{v, u} X (coprod.{v, u} (initial.{v, u} C) Y))
          (Iso.hom (associator X (initial.{v, u} C) Y) :
            coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y ⟶ coprod.{v, u} X (coprod.{v, u} (initial.{v, u} C) Y))
          (map (𝟙 X) (Iso.hom (leftUnitor Y)) :
            coprod.{v, u} X (coprod.{v, u} (initial.{v, u} C) Y) ⟶ coprod.{v, u} X Y) :
        coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y ⟶ coprod.{v, u} X Y))
    (CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y)
      (inr : Y ⟶ coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y)
      (map (Iso.hom (rightUnitor X)) (𝟙 Y) : coprod.{v, u} (coprod.{v, u} X (initial.{v, u} C)) Y ⟶ coprod.{v, u} X Y))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X Y : C
s : BinaryFan.{v, u} X Y
⊢ (map F s).fst = F.map s.fst

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X Y : C
s : BinaryFan.{v, u} X Y
⊢ (map F s).snd = F.map s.snd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X Y : C
s : BinaryCofan.{v, u} X Y
⊢ (map F s).inl = F.map s.inl

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X Y : C
s : BinaryCofan.{v, u} X Y
⊢ (map F s).inr = F.map s.inr

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X Y : C
s : BinaryFan.{v, u} X Y
⊢ fst ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone s)) =
    Iso.hom (Iso.refl ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone s)).pt) ≫ (map F s).fst

Tactic:
simp [fst]

Premises used: CategoryTheory.Limits.BinaryFan.fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X Y : C
s : BinaryFan.{v, u} X Y
⊢ snd ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone s)) =
    Iso.hom (Iso.refl ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone s)).pt) ≫ (map F s).snd

Tactic:
simp [snd]

Premises used: CategoryTheory.Limits.BinaryFan.snd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X Y : C
s : BinaryCofan.{v, u} X Y
⊢ inl ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone s)) ≫
      Iso.hom (Iso.refl ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone s)).pt) =
    (map F s).inl

Tactic:
simp [inl]

Premises used: CategoryTheory.Limits.BinaryCofan.inl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X Y : C
s : BinaryCofan.{v, u} X Y
⊢ inr ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone s)) ≫
      Iso.hom (Iso.refl ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone s)).pt) =
    (map F s).inr

Tactic:
simp [inr]

Premises used: CategoryTheory.Limits.BinaryCofan.inr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{w, u₂} D
F : Functor.{v, w, u, u₂} C D
A B : C
inst_2 : HasBinaryProduct.{v, u} A B
inst_3 : HasBinaryProduct.{w, u₂} (F.obj A) (F.obj B)
⊢ Eq (α := F.obj (prod.{v, u} A B) ⟶ F.obj A)
    (CategoryStruct.comp (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prodComparison F A B) prod.fst) (F.map prod.fst)

Tactic:
prod.lift_fst _ _

Premises used: CategoryTheory.Limits.prod.lift_fst, CategoryTheory.Limits.limit.lift, CategoryTheory.Limits.prodComparison
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{w, u₂} D
F : Functor.{v, w, u, u₂} C D
A B : C
inst_2 : HasBinaryProduct.{v, u} A B
inst_3 : HasBinaryProduct.{w, u₂} (F.obj A) (F.obj B)
⊢ Eq (α := F.obj (prod.{v, u} A B) ⟶ F.obj B)
    (CategoryStruct.comp (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prodComparison F A B) prod.snd) (F.map prod.snd)

Tactic:
prod.lift_snd _ _

Premises used: CategoryTheory.Limits.prod.lift_snd, CategoryTheory.Limits.limit.lift, CategoryTheory.Limits.prodComparison
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{w, u₂} D
F : Functor.{v, w, u, u₂} C D
A B : C
inst_2 : HasBinaryProduct.{v, u} A B
inst_3 : HasBinaryProduct.{w, u₂} (F.obj A) (F.obj B)
H : Functor.{v, w, u, u₂} C D
inst_4 : HasBinaryProduct.{w, u₂} (H.obj A) (H.obj B)
α : F ⟶ H
rw :
  Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (H.obj A) (H.obj B))
    (α.app (prod.{v, u} A B) ≫ prod.lift (H.map prod.fst) (H.map prod.snd))
    (CategoryStruct.comp (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prodComparison F A B) (prod.map (α.app A) (α.app B)))
rw₁ :
  Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (H.obj A) (H.obj B))
    (α.app (prod.{v, u} A B) ≫ prod.lift (H.map prod.fst) (H.map prod.snd))
    (CategoryStruct.comp (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prod.lift (F.map prod.fst) (F.map prod.snd))
      (prod.map (α.app A) (α.app B)))
rw₂ :
  Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (H.obj A) (H.obj B))
    (α.app (prod.{v, u} A B) ≫ prod.lift (H.map prod.fst) (H.map prod.snd))
    (prod.lift (F.map prod.fst ≫ α.app A) (F.map prod.snd ≫ α.app B))
rw₃ :
  Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (H.obj A) (H.obj B))
    (prod.lift (α.app (prod.{v, u} A B) ≫ H.map prod.fst) (α.app (prod.{v, u} A B) ≫ H.map prod.snd))
    (prod.lift (F.map prod.fst ≫ α.app A) (F.map prod.snd ≫ α.app B))
rw₄ :
  Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (H.obj A) (H.obj B))
    (prod.lift (α.app (prod.{v, u} A B) ≫ H.map prod.fst) (α.app (prod.{v, u} A B) ≫ H.map prod.snd))
    (prod.lift (α.app (prod.{v, u} A B) ≫ H.map prod.fst) (F.map prod.snd ≫ α.app B))
rw₅ rw₆ :
  Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (H.obj A) (H.obj B))
    (prod.lift (α.app (prod.{v, u} A B) ≫ H.map prod.fst) (α.app (prod.{v, u} A B) ≫ H.map prod.snd))
    (prod.lift (α.app (prod.{v, u} A B) ≫ H.map prod.fst) (α.app (prod.{v, u} A B) ≫ H.map prod.snd))
⊢ Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (H.obj A) (H.obj B)) (α.app (prod.{v, u} A B) ≫ prodComparison H A B)
    (CategoryStruct.comp (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prodComparison F A B) (prod.map (α.app A) (α.app B)))

Tactic:
rw [prodComparison, prodComparison, prod.lift_map, prod.comp_lift, α.naturality, α.naturality]

Premises used: CategoryTheory.Limits.prod.lift_map, CategoryTheory.NatTrans.naturality, CategoryTheory.Limits.prod.comp_lift, CategoryTheory.Limits.prodComparison
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
D : Type u₂
inst_1 : Category.{w, u₂} D
E : Type u₃
inst_2 : Category.{w', u₃} E
F_1 : Functor.{v, w, u, u₂} C D
G : Functor.{w, w', u₂, u₃} D E
A_1 A' B B' : C
inst_3 : HasBinaryProduct.{v, u} A_1 B
inst_4 : HasBinaryProduct.{v, u} A' B'
inst_5 : HasBinaryProduct.{w, u₂} (F_1.obj A_1) (F_1.obj B)
inst_6 : HasBinaryProduct.{w, u₂} (F_1.obj A') (F_1.obj B')
inst_7 : HasBinaryProduct.{w', u₃} (G.obj (F_1.obj A_1)) (G.obj (F_1.obj B))
inst_8 : HasBinaryProduct.{w', u₃} ((F_1 ⋙ G).obj A_1) ((F_1 ⋙ G).obj B)
inst_9 : HasBinaryProducts.{v, u} C
inst_10 : HasBinaryProducts.{w, u₂} D
F : Functor.{v, w, u, u₂} C D
A f : C
⊢ ∀ ⦃Y : C⦄ (f_1 : f ⟶ Y),
    (Functor.obj prod.functor A ⋙ F).map f_1 ≫ prodComparison F A Y =
      prodComparison F A f ≫ (F ⋙ Functor.obj prod.functor (F.obj A)).map f_1

Tactic:
simp [prodComparison_natural]

Premises used: CategoryTheory.Limits.prodComparison_natural