awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryCoproduct.{v, u} X Y
h₁ : CategoryStruct.comp (Y := coprod.{v, u} X Y) inl (map (𝟙 X) (𝟙 Y)) = inl ≫ 𝟙 (coprod.{v, u} X Y)
⊢ map (𝟙 X) (𝟙 Y) = 𝟙 (coprod.{v, u} X Y)
have h₂ : CategoryStruct.comp (Y := coprod.{v, u} X Y) inr (map (𝟙 X) (𝟙 Y)) = inr ≫ 𝟙 (coprod.{v, u} X Y)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryCoproduct.{v, u} X Y
⊢ desc inl inr = 𝟙 (coprod.{v, u} X Y)
have h₁ : CategoryStruct.comp (Y := coprod.{v, u} X Y) inl (desc inl inr) = inl ≫ 𝟙 (coprod.{v, u} X Y)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasBinaryCoproduct.{v, u} X Y
h₁ : CategoryStruct.comp (Y := coprod.{v, u} X Y) inl (desc inl inr) = inl ≫ 𝟙 (coprod.{v, u} X Y)
⊢ desc inl inr = 𝟙 (coprod.{v, u} X Y)
have h₂ : CategoryStruct.comp (Y := coprod.{v, u} X Y) inr (desc inl inr) = inr ≫ 𝟙 (coprod.{v, u} X Y)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S T U V W : C
inst_1 : HasBinaryCoproduct.{v, u} U W
inst_2 : HasBinaryCoproduct.{v, u} T V
f : U ⟶ S
g : W ⟶ S
h : T ⟶ U
k : V ⟶ W
⊢ Eq (α := coprod.{v, u} T V ⟶ S) (CategoryStruct.comp (Y := coprod.{v, u} U W) (map h k) (desc f g))
    (desc (h ≫ f) (k ≫ g))
have h₁ : CategoryStruct.comp (Y := coprod.{v, u} T V) inl (CategoryStruct.comp (Y := coprod.{v, u} U W) (map h k) (desc f g)) =
  CategoryStruct.comp (Y := coprod.{v, u} T V) inl (desc (h ≫ f) (k ≫ g))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S T U V W : C
inst_1 : HasBinaryCoproduct.{v, u} U W
inst_2 : HasBinaryCoproduct.{v, u} T V
f : U ⟶ S
g : W ⟶ S
h : T ⟶ U
k : V ⟶ W
h₁ :
  CategoryStruct.comp (Y := coprod.{v, u} T V) inl (CategoryStruct.comp (Y := coprod.{v, u} U W) (map h k) (desc f g)) =
    CategoryStruct.comp (Y := coprod.{v, u} T V) inl (desc (h ≫ f) (k ≫ g))
⊢ Eq (α := coprod.{v, u} T V ⟶ S) (CategoryStruct.comp (Y := coprod.{v, u} U W) (map h k) (desc f g))
    (desc (h ≫ f) (k ≫ g))
have h₂ : CategoryStruct.comp (Y := coprod.{v, u} T V) inr (CategoryStruct.comp (Y := coprod.{v, u} U W) (map h k) (desc f g)) =
  CategoryStruct.comp (Y := coprod.{v, u} T V) inr (desc (h ≫ f) (k ≫ g))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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) (desc (g ≫ inl) (g' ≫ inr)) (map g g')
have 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')
Tactic: rw [← coprod.map_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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 (α := 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))
have 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)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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)))
⊢ 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))
have 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)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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₂)
⊢ i₁ = i₂
have h₁ : inl ≫ i₁ = inl ≫ i₂
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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₂
⊢ i₁ = i₂
have h₂ : inr ≫ i₁ = inr ≫ i₂
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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₂)
⊢ inl ≫ i₁ = inl ≫ i₂
have h₁ : f ≫ inl ≫ i₁ = f ≫ inl ≫ i₂
Tactic: rw [← cancel_epi f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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₂)
⊢ inr ≫ i₁ = inr ≫ i₂
have h₂ : g ≫ inr ≫ i₁ = g ≫ inr ≫ i₂
Tactic: rw [← cancel_epi g]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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
⊢ snd ≫ lift (terminal.from P) (𝟙 P) = 𝟙 (prod.{v, u} (terminal.{v, u} C) P)
have 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
Tactic: apply prod.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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
⊢ snd ≫ lift (terminal.from P) (𝟙 P) = 𝟙 (prod.{v, u} (terminal.{v, u} C) P)
have 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
Tactic: apply prod.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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)
⊢ fst ≫ lift (𝟙 P) (terminal.from P) = 𝟙 (prod.{v, u} P (terminal.{v, u} C))
have 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
Tactic: apply prod.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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
⊢ fst ≫ lift (𝟙 P) (terminal.from P) = 𝟙 (prod.{v, u} P (terminal.{v, u} C))
have 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
Tactic: apply prod.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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 (α := 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))
have 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))
Tactic: rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, prod.leftUnitor_hom_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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))
⊢ 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))
have 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))
Tactic: rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, prod.leftUnitor_hom_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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))
⊢ 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))
have 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)
Tactic: rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, prod.leftUnitor_hom_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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)
⊢ 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))
have rw₃ : Eq (α := prod.{v, u} (terminal.{v, u} C) X ⟶ Y) (Iso.hom (leftUnitor X) ≫ f) (Iso.hom (leftUnitor X) ≫ f)
Tactic: rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, prod.leftUnitor_hom_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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 (α := 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))
have 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))
Tactic: rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, prod.rightUnitor_hom_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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))
⊢ 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))
have 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))
Tactic: rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, prod.rightUnitor_hom_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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))
⊢ 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))
have 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)
Tactic: rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, prod.rightUnitor_hom_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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)
⊢ 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))
have rw₃ : Eq (α := prod.{v, u} X (terminal.{v, u} C) ⟶ Y) (Iso.hom (prod.rightUnitor X) ≫ f) (Iso.hom (prod.rightUnitor X) ≫ f)
Tactic: rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, prod.rightUnitor_hom_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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 ⟶ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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)
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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
⊢ desc (initial.to P) (𝟙 P) ≫ inr = 𝟙 (coprod.{v, u} (initial.{v, u} C) P)
have 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)
Tactic: apply coprod.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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)
⊢ desc (initial.to P) (𝟙 P) ≫ inr = 𝟙 (coprod.{v, u} (initial.{v, u} C) P)
have 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)
Tactic: apply coprod.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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
⊢ desc (𝟙 P) (initial.to P) ≫ inl = 𝟙 (coprod.{v, u} P (initial.{v, u} C))
have 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))
Tactic: apply coprod.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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))
⊢ desc (𝟙 P) (initial.to P) ≫ inl = 𝟙 (coprod.{v, u} P (initial.{v, u} C))
have 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))
Tactic: apply coprod.hom_ext