awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
inst_1 : HasBinaryCoproduct.{v, u} W Y
inst_2 : HasBinaryCoproduct.{v, u} X Z
g : W ⟶ X
g' : Y ⟶ Z
rw :
  Eq (α := coprod.{v, u} W Y ⟶ coprod.{v, u} X Z)
    (CategoryStruct.comp (Y := coprod.{v, u} X Z) (map g g') (desc inl inr)) (map g g')
⊢ Eq (α := coprod.{v, u} W Y ⟶ coprod.{v, u} X Z) (desc (g ≫ inl) (g' ≫ inr)) (map g g')

Tactic:
rw [← coprod.map_desc]

Premises used: CategoryTheory.Limits.coprod.map_desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
inst_1 : HasBinaryCoproduct.{v, u} W Y
inst_2 : HasBinaryCoproduct.{v, u} X Z
g : W ⟶ X
g' : Y ⟶ Z
⊢ Eq (α := coprod.{v, u} W Y ⟶ coprod.{v, u} X Z)
    (CategoryStruct.comp (Y := coprod.{v, u} X Z) (map g g') (desc inl inr)) (map g g')

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
A₁ A₂ A₃ B₁ B₂ B₃ : C
inst_1 : HasBinaryCoproduct.{v, u} A₁ B₁
inst_2 : HasBinaryCoproduct.{v, u} A₂ B₂
inst_3 : HasBinaryCoproduct.{v, u} A₃ B₃
f : A₁ ⟶ A₂
g : B₁ ⟶ B₂
h : A₂ ⟶ A₃
k : B₂ ⟶ B₃
h₁ :
  Eq (α := A₁ ⟶ coprod.{v, u} A₃ B₃)
    (CategoryStruct.comp (Y := coprod.{v, u} A₁ B₁) inl
      (CategoryStruct.comp (Y := coprod.{v, u} A₂ B₂) (map f g) (map h k)))
    (CategoryStruct.comp (Y := coprod.{v, u} A₁ B₁) inl (map (f ≫ h) (g ≫ k)))
h₂ :
  Eq (α := B₁ ⟶ coprod.{v, u} A₃ B₃)
    (CategoryStruct.comp (Y := coprod.{v, u} A₁ B₁) inr
      (CategoryStruct.comp (Y := coprod.{v, u} A₂ B₂) (map f g) (map h k)))
    (CategoryStruct.comp (Y := coprod.{v, u} A₁ B₁) inr (map (f ≫ h) (g ≫ k)))
⊢ Eq (α := coprod.{v, u} A₁ B₁ ⟶ coprod.{v, u} A₃ B₃)
    (CategoryStruct.comp (Y := coprod.{v, u} A₂ B₂) (map f g) (map h k)) (map (f ≫ h) (g ≫ k))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
A₁ A₂ A₃ B₁ B₂ B₃ : C
inst_1 : HasBinaryCoproduct.{v, u} A₁ B₁
inst_2 : HasBinaryCoproduct.{v, u} A₂ B₂
inst_3 : HasBinaryCoproduct.{v, u} A₃ B₃
f : A₁ ⟶ A₂
g : B₁ ⟶ B₂
h : A₂ ⟶ A₃
k : B₂ ⟶ B₃
⊢ Eq (α := A₁ ⟶ coprod.{v, u} A₃ B₃)
    (CategoryStruct.comp (Y := coprod.{v, u} A₁ B₁) inl
      (CategoryStruct.comp (Y := coprod.{v, u} A₂ B₂) (map f g) (map h k)))
    (CategoryStruct.comp (Y := coprod.{v, u} A₁ B₁) inl (map (f ≫ h) (g ≫ k)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
A₁ A₂ A₃ B₁ B₂ B₃ : C
inst_1 : HasBinaryCoproduct.{v, u} A₁ B₁
inst_2 : HasBinaryCoproduct.{v, u} A₂ B₂
inst_3 : HasBinaryCoproduct.{v, u} A₃ B₃
f : A₁ ⟶ A₂
g : B₁ ⟶ B₂
h : A₂ ⟶ A₃
k : B₂ ⟶ B₃
⊢ Eq (α := B₁ ⟶ coprod.{v, u} A₃ B₃)
    (CategoryStruct.comp (Y := coprod.{v, u} A₁ B₁) inr
      (CategoryStruct.comp (Y := coprod.{v, u} A₂ B₂) (map f g) (map h k)))
    (CategoryStruct.comp (Y := coprod.{v, u} A₁ B₁) inr (map (f ≫ h) (g ≫ k)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
A B X Y : C
f : A ⟶ B
g : X ⟶ Y
inst_1 : HasColimitsOfShape.{0, 0, v, u} (Discrete WalkingPair) C
⊢ Eq (α := coprod.{v, u} X A ⟶ coprod.{v, u} Y B)
    (CategoryStruct.comp (Y := coprod.{v, u} X B) (map (𝟙 X) f) (map g (𝟙 B)))
    (CategoryStruct.comp (Y := coprod.{v, u} Y A) (map g (𝟙 A)) (map (𝟙 Y) f))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z W : C
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : HasBinaryCoproduct.{v, u} Z W
inst_2 : HasBinaryCoproduct.{v, u} Y W
inst_3 : HasBinaryCoproduct.{v, u} X W
⊢ Eq (α := coprod.{v, u} X W ⟶ coprod.{v, u} Z W) (map (f ≫ g) (𝟙 W))
    (CategoryStruct.comp (Y := coprod.{v, u} Y W) (map f (𝟙 W)) (map g (𝟙 W)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z W : C
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : HasBinaryCoproduct.{v, u} W X
inst_2 : HasBinaryCoproduct.{v, u} W Y
inst_3 : HasBinaryCoproduct.{v, u} W Z
⊢ Eq (α := coprod.{v, u} W X ⟶ coprod.{v, u} W Z) (map (𝟙 W) (f ≫ g))
    (CategoryStruct.comp (Y := coprod.{v, u} W Y) (map (𝟙 W) f) (map (𝟙 W) g))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 W X Y Z : C
inst_1 : HasBinaryCoproduct.{v, u} W X
inst_2 : HasBinaryCoproduct.{v, u} Y Z
f : W ⟶ Y
g : X ⟶ Z
inst_3 : IsIso f
inst_4 : IsIso g
⊢ IsIso (X := coprod.{v, u} W X) (Y := coprod.{v, u} Y Z) (coprod.map f g)

Tactic:
(coprod.mapIso (asIso f) (asIso g)).isIso_hom

Premises used: CategoryTheory.Limits.coprod.map, CategoryTheory.Limits.coprod.mapIso, CategoryTheory.Iso.isIso_hom, CategoryTheory.Limits.colimMap, CategoryTheory.Limits.IsColimit.map, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
X_1 Y_1 : C_1
C : Type u_1
inst_1 : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_2 : Epi f
inst_3 : Epi g
inst_4 : HasBinaryCoproduct.{v_1, u_1} W X
inst_5 : HasBinaryCoproduct.{v_1, u_1} Y Z
Z_1 : C
i₁ i₂ : coprod.{v_1, u_1} Y Z ⟶ Z_1
h : Eq (α := coprod.{v_1, u_1} W X ⟶ Z_1) (map f g ≫ i₁) (map f g ≫ i₂)
h₁ : inl ≫ i₁ = inl ≫ i₂
h₂ : inr ≫ i₁ = inr ≫ i₂
⊢ i₁ = i₂

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
X_1 Y_1 : C_1
C : Type u_1
inst_1 : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_2 : Epi f
inst_3 : Epi g
inst_4 : HasBinaryCoproduct.{v_1, u_1} W X
inst_5 : HasBinaryCoproduct.{v_1, u_1} Y Z
Z_1 : C
i₁ i₂ : coprod.{v_1, u_1} Y Z ⟶ Z_1
h : Eq (α := coprod.{v_1, u_1} W X ⟶ Z_1) (map f g ≫ i₁) (map f g ≫ i₂)
h₁ : f ≫ inl ≫ i₁ = f ≫ inl ≫ i₂
⊢ inl ≫ i₁ = inl ≫ i₂

Tactic:
rw [← cancel_epi f]

Premises used: CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
X_1 Y_1 : C_1
C : Type u_1
inst_1 : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_2 : Epi f
inst_3 : Epi g
inst_4 : HasBinaryCoproduct.{v_1, u_1} W X
inst_5 : HasBinaryCoproduct.{v_1, u_1} Y Z
Z_1 : C
i₁ i₂ : coprod.{v_1, u_1} Y Z ⟶ Z_1
h : Eq (α := coprod.{v_1, u_1} W X ⟶ Z_1) (map f g ≫ i₁) (map f g ≫ i₂)
⊢ f ≫ inl ≫ i₁ = f ≫ inl ≫ i₂

Tactic:
simpa using congr_arg (fun f => coprod.inl ≫ f) h

Premises used: CategoryTheory.Limits.coprod.inl, congr_arg, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
X_1 Y_1 : C_1
C : Type u_1
inst_1 : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_2 : Epi f
inst_3 : Epi g
inst_4 : HasBinaryCoproduct.{v_1, u_1} W X
inst_5 : HasBinaryCoproduct.{v_1, u_1} Y Z
Z_1 : C
i₁ i₂ : coprod.{v_1, u_1} Y Z ⟶ Z_1
h : Eq (α := coprod.{v_1, u_1} W X ⟶ Z_1) (map f g ≫ i₁) (map f g ≫ i₂)
h₂ : g ≫ inr ≫ i₁ = g ≫ inr ≫ i₂
⊢ inr ≫ i₁ = inr ≫ i₂

Tactic:
rw [← cancel_epi g]

Premises used: CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
X_1 Y_1 : C_1
C : Type u_1
inst_1 : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_2 : Epi f
inst_3 : Epi g
inst_4 : HasBinaryCoproduct.{v_1, u_1} W X
inst_5 : HasBinaryCoproduct.{v_1, u_1} Y Z
Z_1 : C
i₁ i₂ : coprod.{v_1, u_1} Y Z ⟶ Z_1
h : Eq (α := coprod.{v_1, u_1} W X ⟶ Z_1) (map f g ≫ i₁) (map f g ≫ i₂)
⊢ g ≫ inr ≫ i₁ = g ≫ inr ≫ i₂

Tactic:
simpa using congr_arg (fun f => coprod.inr ≫ f) h

Premises used: congr_arg, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.coprod.inr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasBinaryCoproduct.{v, u} X X
inst_2 : HasBinaryCoproduct.{v, u} Y Y
⊢ Eq (α := coprod.{v, u} X X ⟶ Y) (CategoryStruct.comp (Y := coprod.{v, u} Y Y) (map f f) (codiag Y)) (codiag X ≫ f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryCoproduct.{v, u} X Y
inst_2 : HasBinaryCoproduct.{v, u} (coprod.{v, u} X Y) (coprod.{v, u} X Y)
⊢ CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} X Y) (coprod.{v, u} X Y)) (map inl inr)
      (codiag (coprod.{v, u} X Y)) =
    𝟙 (coprod.{v, u} X Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimitsOfShape.{0, 0, v, u} (Discrete WalkingPair) C
X X' Y Y' : C
g : X ⟶ Y
g' : X' ⟶ Y'
⊢ Eq (α := coprod.{v, u} X X' ⟶ coprod.{v, u} Y Y')
    (CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} Y Y') (coprod.{v, u} Y Y')) (map (g ≫ inl) (g' ≫ inr))
      (codiag (coprod.{v, u} Y Y')))
    (map g g')

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ∀ {X Y : C}, HasLimit.{0, 0, v, u} (pair X Y)
⊢ HasBinaryProducts.{v, u} C

Tactic:
{ has_limit := fun F => hasLimit_of_iso (diagramIsoPair F).symm }

Premises used: CategoryTheory.Limits.hasLimit_of_iso, CategoryTheory.Limits.HasLimitsOfShape.mk, CategoryTheory.Iso.symm, CategoryTheory.Limits.diagramIsoPair
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ∀ {X Y : C}, HasColimit.{0, 0, v, u} (pair X Y)
⊢ HasBinaryCoproducts.{v, u} C

Tactic:
{ has_colimit := fun F => hasColimit_of_iso (diagramIsoPair F) }

Premises used: CategoryTheory.Limits.HasColimitsOfShape.mk, CategoryTheory.Limits.hasColimit_of_iso, CategoryTheory.Limits.diagramIsoPair
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryProducts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : Z ⟶ W
⊢ Eq (α := prod.{v, u} X Z ⟶ prod.{v, u} W Y)
    (CategoryStruct.comp (Y := prod.{v, u} Y W) (prod.map f g) (Iso.hom (prod.braiding Y W)))
    (CategoryStruct.comp (Y := prod.{v, u} Z X) (Iso.hom (prod.braiding X Z)) (prod.map g f))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
P Q : C
inst_1 : HasBinaryProduct.{v, u} P Q
inst_2 : HasBinaryProduct.{v, u} Q P
⊢ CategoryStruct.comp (Y := prod.{v, u} Q P) (lift snd fst) (lift snd fst) = 𝟙 (prod.{v, u} P Q)

Tactic:
(prod.braiding _ _).hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Limits.limit.lift, CategoryTheory.Limits.prod.braiding
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
P Q : C
inst_1 : HasBinaryProduct.{v, u} P Q
inst_2 : HasBinaryProduct.{v, u} Q P
⊢ CategoryStruct.comp (Y := prod.{v, u} Q P) (Iso.hom (braiding P Q)) (Iso.hom (braiding Q P)) = 𝟙 (prod.{v, u} P Q)

Tactic:
(prod.braiding _ _).hom_inv_id

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

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryProducts.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ Eq (α := prod.{v, u} (prod.{v, u} X₁ X₂) X₃ ⟶ prod.{v, u} Y₁ (prod.{v, u} Y₂ Y₃))
    (CategoryStruct.comp (Y := prod.{v, u} (prod.{v, u} Y₁ Y₂) Y₃)
        (map (map f₁ f₂) f₃ : prod.{v, u} (prod.{v, u} X₁ X₂) X₃ ⟶ prod.{v, u} (prod.{v, u} Y₁ Y₂) Y₃)
        (Iso.hom (associator Y₁ Y₂ Y₃) : prod.{v, u} (prod.{v, u} Y₁ Y₂) Y₃ ⟶ prod.{v, u} Y₁ (prod.{v, u} Y₂ Y₃)) :
      prod.{v, u} (prod.{v, u} X₁ X₂) X₃ ⟶ prod.{v, u} Y₁ (prod.{v, u} Y₂ Y₃))
    (CategoryStruct.comp (Y := prod.{v, u} X₁ (prod.{v, u} X₂ X₃))
        (Iso.hom (associator X₁ X₂ X₃) : prod.{v, u} (prod.{v, u} X₁ X₂) X₃ ⟶ prod.{v, u} X₁ (prod.{v, u} X₂ X₃))
        (map f₁ (map f₂ f₃) : prod.{v, u} X₁ (prod.{v, u} X₂ X₃) ⟶ prod.{v, u} Y₁ (prod.{v, u} Y₂ Y₃)) :
      prod.{v, u} (prod.{v, u} X₁ X₂) X₃ ⟶ prod.{v, u} Y₁ (prod.{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 : HasTerminal.{v, u} C
P : C
inst_2 : HasBinaryProduct.{v, u} (terminal.{v, u} C) P
h₁ :
  CategoryStruct.comp (Y := prod.{v, u} (terminal.{v, u} C) P) (snd ≫ lift (terminal.from P) (𝟙 P)) fst =
    𝟙 (prod.{v, u} (terminal.{v, u} C) P) ≫ fst
h₂ :
  CategoryStruct.comp (Y := prod.{v, u} (terminal.{v, u} C) P) (snd ≫ lift (terminal.from P) (𝟙 P)) snd =
    𝟙 (prod.{v, u} (terminal.{v, u} C) P) ≫ snd
⊢ snd ≫ lift (terminal.from P) (𝟙 P) = 𝟙 (prod.{v, u} (terminal.{v, u} C) P)

Tactic:
apply prod.hom_ext

Premises used: CategoryTheory.Limits.prod.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasTerminal.{v, u} C
P : C
inst_2 : HasBinaryProduct.{v, u} (terminal.{v, u} C) P
⊢ CategoryStruct.comp (Y := prod.{v, u} (terminal.{v, u} C) P) (snd ≫ lift (terminal.from P) (𝟙 P)) fst =
    𝟙 (prod.{v, u} (terminal.{v, u} C) P) ≫ fst

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 : HasTerminal.{v, u} C
P : C
inst_2 : HasBinaryProduct.{v, u} (terminal.{v, u} C) P
⊢ CategoryStruct.comp (Y := prod.{v, u} (terminal.{v, u} C) P) (snd ≫ lift (terminal.from P) (𝟙 P)) snd =
    𝟙 (prod.{v, u} (terminal.{v, u} C) P) ≫ snd

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 : HasTerminal.{v, u} C
P : C
inst_2 : HasBinaryProduct.{v, u} (terminal.{v, u} C) P
⊢ Eq.{v + 1} (α := P ⟶ P)
    (CategoryStruct.comp (Y := prod.{v, u} (terminal.{v, u} C) P) (lift (terminal.from P) (𝟙 P)) snd) (𝟙 P)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasTerminal.{v, u} C
P : C
inst_2 : HasBinaryProduct.{v, u} P (terminal.{v, u} C)
h₁ :
  CategoryStruct.comp (Y := prod.{v, u} P (terminal.{v, u} C)) (fst ≫ lift (𝟙 P) (terminal.from P)) fst =
    𝟙 (prod.{v, u} P (terminal.{v, u} C)) ≫ fst
h₂ :
  CategoryStruct.comp (Y := prod.{v, u} P (terminal.{v, u} C)) (fst ≫ lift (𝟙 P) (terminal.from P)) snd =
    𝟙 (prod.{v, u} P (terminal.{v, u} C)) ≫ snd
⊢ fst ≫ lift (𝟙 P) (terminal.from P) = 𝟙 (prod.{v, u} P (terminal.{v, u} C))

Tactic:
apply prod.hom_ext

Premises used: CategoryTheory.Limits.prod.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasTerminal.{v, u} C
P : C
inst_2 : HasBinaryProduct.{v, u} P (terminal.{v, u} C)
⊢ CategoryStruct.comp (Y := prod.{v, u} P (terminal.{v, u} C)) (fst ≫ lift (𝟙 P) (terminal.from P)) fst =
    𝟙 (prod.{v, u} P (terminal.{v, u} C)) ≫ fst

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 : HasTerminal.{v, u} C
P : C
inst_2 : HasBinaryProduct.{v, u} P (terminal.{v, u} C)
⊢ CategoryStruct.comp (Y := prod.{v, u} P (terminal.{v, u} C)) (fst ≫ lift (𝟙 P) (terminal.from P)) snd =
    𝟙 (prod.{v, u} P (terminal.{v, u} C)) ≫ snd

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 : HasTerminal.{v, u} C
P : C
inst_2 : HasBinaryProduct.{v, u} P (terminal.{v, u} C)
⊢ Eq.{v + 1} (α := P ⟶ P)
    (CategoryStruct.comp (Y := prod.{v, u} P (terminal.{v, u} C)) (lift (𝟙 P) (terminal.from P)) fst) (𝟙 P)

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

Tactic:
prod.map_snd _ _

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.prod.map_snd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasTerminal.{v, u} C
inst_2 : HasBinaryProducts.{v, u} C
f : X ⟶ Y
rw :
  Eq (α := prod.{v, u} (terminal.{v, u} C) X ⟶ prod.{v, u} (terminal.{v, u} C) Y) (map (𝟙 (terminal.{v, u} C)) f)
    (Iso.hom (leftUnitor X) ≫ f ≫ Iso.inv (leftUnitor Y))
rw₁ :
  Eq (α := prod.{v, u} (terminal.{v, u} C) X ⟶ prod.{v, u} (terminal.{v, u} C) Y) (map (𝟙 (terminal.{v, u} C)) f)
    ((Iso.hom (leftUnitor X) ≫ f) ≫ Iso.inv (leftUnitor Y))
rw₂ :
  Eq (α := prod.{v, u} (terminal.{v, u} C) X ⟶ Y)
    (CategoryStruct.comp (Y := prod.{v, u} (terminal.{v, u} C) Y) (map (𝟙 (terminal.{v, u} C)) f)
      (Iso.hom (leftUnitor Y)))
    (Iso.hom (leftUnitor X) ≫ f)
rw₃ rw₄ : Eq (α := prod.{v, u} (terminal.{v, u} C) X ⟶ Y) (Iso.hom (leftUnitor X) ≫ f) (Iso.hom (leftUnitor X) ≫ f)
⊢ Eq (α := X ⟶ prod.{v, u} (terminal.{v, u} C) Y)
    (CategoryStruct.comp (Y := prod.{v, u} (terminal.{v, u} C) X) (Iso.inv (leftUnitor X))
      (map (𝟙 (terminal.{v, u} C)) f))
    (f ≫ Iso.inv (leftUnitor Y))

Tactic:
rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, prod.leftUnitor_hom_naturality]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.eq_comp_inv, CategoryTheory.Iso.inv_comp_eq, CategoryTheory.Limits.prod.leftUnitor_hom_naturality
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasTerminal.{v, u} C
inst_2 : HasBinaryProducts.{v, u} C
f : X ⟶ Y
⊢ Eq (α := prod.{v, u} X (terminal.{v, u} C) ⟶ Y)
    (CategoryStruct.comp (Y := prod.{v, u} Y (terminal.{v, u} C)) (map f (𝟙 (terminal.{v, u} C)))
      (Iso.hom (rightUnitor Y)))
    (Iso.hom (rightUnitor X) ≫ f)

Tactic:
prod.map_fst _ _

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.prod.map_fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasTerminal.{v, u} C
inst_2 : HasBinaryProducts.{v, u} C
f : X ⟶ Y
rw :
  Eq (α := prod.{v, u} X (terminal.{v, u} C) ⟶ prod.{v, u} Y (terminal.{v, u} C)) (prod.map f (𝟙 (terminal.{v, u} C)))
    (Iso.hom (prod.rightUnitor X) ≫ f ≫ Iso.inv (prod.rightUnitor Y))
rw₁ :
  Eq (α := prod.{v, u} X (terminal.{v, u} C) ⟶ prod.{v, u} Y (terminal.{v, u} C)) (prod.map f (𝟙 (terminal.{v, u} C)))
    ((Iso.hom (prod.rightUnitor X) ≫ f) ≫ Iso.inv (prod.rightUnitor Y))
rw₂ :
  Eq (α := prod.{v, u} X (terminal.{v, u} C) ⟶ Y)
    (CategoryStruct.comp (Y := prod.{v, u} Y (terminal.{v, u} C)) (prod.map f (𝟙 (terminal.{v, u} C)))
      (Iso.hom (prod.rightUnitor Y)))
    (Iso.hom (prod.rightUnitor X) ≫ f)
rw₃ rw₄ :
  Eq (α := prod.{v, u} X (terminal.{v, u} C) ⟶ Y) (Iso.hom (prod.rightUnitor X) ≫ f) (Iso.hom (prod.rightUnitor X) ≫ f)
⊢ Eq (α := X ⟶ prod.{v, u} Y (terminal.{v, u} C))
    (CategoryStruct.comp (Y := prod.{v, u} X (terminal.{v, u} C)) (Iso.inv (prod.rightUnitor X))
      (prod.map f (𝟙 (terminal.{v, u} C))))
    (f ≫ Iso.inv (prod.rightUnitor Y))

Tactic:
rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, prod.rightUnitor_hom_naturality]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.prod.rightUnitor_hom_naturality, CategoryTheory.Iso.eq_comp_inv, CategoryTheory.Iso.inv_comp_eq
-- 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
h₁ :
  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)
h₂ :
  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)
⊢ Eq.{v + 1} (α := prod.{v, u} (prod.{v, u} X (terminal.{v, u} C)) 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) :
      prod.{v, u} (prod.{v, u} X (terminal.{v, u} C)) Y ⟶ prod.{v, u} X Y)
    (map (Iso.hom (rightUnitor X)) (𝟙 Y) : prod.{v, u} (prod.{v, u} X (terminal.{v, u} C)) Y ⟶ prod.{v, u} X Y)

Tactic:
ext