awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
hr : ∀ (f : X ⟶ Y), Eq (α := X ⟶ biprod.{v, u} Y Y) (biprod.lift 0 f) (f ≫ biprod.inr)
f : X ⟶ Y
h₀ :
  CategoryStruct.comp (Y := biprod.{v, u} Y Y) (biprod.lift f 0) biprod.fst =
    CategoryStruct.comp (Y := biprod.{v, u} Y Y) (f ≫ biprod.inl) biprod.fst
⊢ Eq (α := X ⟶ biprod.{v, u} Y Y) (biprod.lift f 0) (f ≫ biprod.inl)
have h₁ : Eq (α := X ⟶ Y) (CategoryStruct.comp (Y := biprod.{v, u} Y Y) (biprod.lift f 0) biprod.snd)
  (CategoryStruct.comp (Y := biprod.{v, u} Y Y) (f ≫ biprod.inl) biprod.snd)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
hr : ∀ (f : X ⟶ Y), Eq (α := X ⟶ biprod.{v, u} Y Y) (biprod.lift 0 f) (f ≫ biprod.inr)
⊢ EckmannHilton.IsUnital (fun (x1 x2 : X ⟶ Y) ↦ leftAdd X Y x1 x2) 0
have hl : ∀ (f : X ⟶ Y), Eq (α := X ⟶ biprod.{v, u} Y Y) (biprod.lift f 0) (f ≫ biprod.inl)
Tactic: have hl : ∀ f : X ⟶ Y, biprod.lift f (0 : X ⟶ Y) = f ≫ biprod.inl := by
    intro f
    ext
    · simp
    · simp [biprod.lift_snd, Category.assoc, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
f : X ⟶ Y
⊢ Eq (α := biprod.{v, u} X X ⟶ Y) (biprod.desc 0 f) (biprod.snd ≫ f)
have h₀ : Eq (α := X ⟶ Y) (CategoryStruct.comp (Y := biprod.{v, u} X X) biprod.inl (biprod.desc 0 f))
  (CategoryStruct.comp (Y := biprod.{v, u} X X) biprod.inl (biprod.snd ≫ f))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
f : X ⟶ Y
h₀ :
  Eq (α := X ⟶ Y) (CategoryStruct.comp (Y := biprod.{v, u} X X) biprod.inl (biprod.desc 0 f))
    (CategoryStruct.comp (Y := biprod.{v, u} X X) biprod.inl (biprod.snd ≫ f))
⊢ Eq (α := biprod.{v, u} X X ⟶ Y) (biprod.desc 0 f) (biprod.snd ≫ f)
have h₁ : CategoryStruct.comp (Y := biprod.{v, u} X X) biprod.inr (biprod.desc 0 f) =
  CategoryStruct.comp (Y := biprod.{v, u} X X) biprod.inr (biprod.snd ≫ f)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
⊢ EckmannHilton.IsUnital (fun (x1 x2 : X ⟶ Y) ↦ rightAdd X Y x1 x2) 0
have h₂ : ∀ (f : X ⟶ Y), Eq (α := biprod.{v, u} X X ⟶ Y) (biprod.desc 0 f) (biprod.snd ≫ f)
Tactic: have h₂ : ∀ f : X ⟶ Y, biprod.desc (0 : X ⟶ Y) f = biprod.snd ≫ f := by
    intro f
    ext
    · simp
    · simp only [biprod.inr_desc, BinaryBicone.inr_snd_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
h₂ : ∀ (f : X ⟶ Y), Eq (α := biprod.{v, u} X X ⟶ Y) (biprod.desc 0 f) (biprod.snd ≫ f)
f : X ⟶ Y
⊢ Eq (α := biprod.{v, u} X X ⟶ Y) (biprod.desc f 0) (biprod.fst ≫ f)
have h₀ : CategoryStruct.comp (Y := biprod.{v, u} X X) biprod.inl (biprod.desc f 0) =
  CategoryStruct.comp (Y := biprod.{v, u} X X) biprod.inl (biprod.fst ≫ f)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
h₂ : ∀ (f : X ⟶ Y), Eq (α := biprod.{v, u} X X ⟶ Y) (biprod.desc 0 f) (biprod.snd ≫ f)
f : X ⟶ Y
h₀ :
  CategoryStruct.comp (Y := biprod.{v, u} X X) biprod.inl (biprod.desc f 0) =
    CategoryStruct.comp (Y := biprod.{v, u} X X) biprod.inl (biprod.fst ≫ f)
⊢ Eq (α := biprod.{v, u} X X ⟶ Y) (biprod.desc f 0) (biprod.fst ≫ f)
have h₁ : Eq (α := X ⟶ Y) (CategoryStruct.comp (Y := biprod.{v, u} X X) biprod.inr (biprod.desc f 0))
  (CategoryStruct.comp (Y := biprod.{v, u} X X) biprod.inr (biprod.fst ≫ f))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
h₂ : ∀ (f : X ⟶ Y), Eq (α := biprod.{v, u} X X ⟶ Y) (biprod.desc 0 f) (biprod.snd ≫ f)
⊢ EckmannHilton.IsUnital (fun (x1 x2 : X ⟶ Y) ↦ rightAdd X Y x1 x2) 0
have h₁ : ∀ (f : X ⟶ Y), Eq (α := biprod.{v, u} X X ⟶ Y) (biprod.desc f 0) (biprod.fst ≫ f)
Tactic: have h₁ : ∀ f : X ⟶ Y, biprod.desc f (0 : X ⟶ Y) = biprod.fst ≫ f := by
    intro f
    ext
    · simp
    · simp only [biprod.inr_desc, BinaryBicone.inr_fst_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
f g h k : X ⟶ Y
diag : biprod.{v, u} X X ⟶ biprod.{v, u} Y Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
⊢ biprod.inl ≫ diag = biprod.lift f h
have h₀ : (biprod.inl ≫ diag) ≫ biprod.fst = CategoryStruct.comp (Y := biprod.{v, u} Y Y) (biprod.lift f h) biprod.fst
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
f g h k : X ⟶ Y
diag : biprod.{v, u} X X ⟶ biprod.{v, u} Y Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
h₀ : (biprod.inl ≫ diag) ≫ biprod.fst = CategoryStruct.comp (Y := biprod.{v, u} Y Y) (biprod.lift f h) biprod.fst
⊢ biprod.inl ≫ diag = biprod.lift f h
have h₁ : (biprod.inl ≫ diag) ≫ biprod.snd = CategoryStruct.comp (Y := biprod.{v, u} Y Y) (biprod.lift f h) biprod.snd
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
f g h k : X ⟶ Y
diag : biprod.{v, u} X X ⟶ biprod.{v, u} Y Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
⊢ leftAdd X Y (rightAdd X Y f g) (rightAdd X Y h k) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
have hd₁ : biprod.inl ≫ diag = biprod.lift f h
Tactic: have hd₁ : biprod.inl ≫ diag = biprod.lift f h := by ext <;> simp [diag]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
f g h k : X ⟶ Y
diag : biprod.{v, u} X X ⟶ biprod.{v, u} Y Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
⊢ biprod.inr ≫ diag = biprod.lift g k
have h₀ : (biprod.inr ≫ diag) ≫ biprod.fst = CategoryStruct.comp (Y := biprod.{v, u} Y Y) (biprod.lift g k) biprod.fst
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
f g h k : X ⟶ Y
diag : biprod.{v, u} X X ⟶ biprod.{v, u} Y Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
h₀ : (biprod.inr ≫ diag) ≫ biprod.fst = CategoryStruct.comp (Y := biprod.{v, u} Y Y) (biprod.lift g k) biprod.fst
⊢ biprod.inr ≫ diag = biprod.lift g k
have h₁ : (biprod.inr ≫ diag) ≫ biprod.snd = CategoryStruct.comp (Y := biprod.{v, u} Y Y) (biprod.lift g k) biprod.snd
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
f g h k : X ⟶ Y
diag : biprod.{v, u} X X ⟶ biprod.{v, u} Y Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
⊢ leftAdd X Y (rightAdd X Y f g) (rightAdd X Y h k) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
have hd₂ : biprod.inr ≫ diag = biprod.lift g k
Tactic: have hd₂ : biprod.inr ≫ diag = biprod.lift g k := by ext <;> simp [diag]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
f g h k : X ⟶ Y
diag : biprod.{v, u} X X ⟶ biprod.{v, u} Y Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
hd₂ : biprod.inr ≫ diag = biprod.lift g k
⊢ biprod.lift (rightAdd X Y f g) (rightAdd X Y h k) = biprod.lift (𝟙 X) (𝟙 X) ≫ diag
have h₀ : CategoryStruct.comp (Y := biprod.{v, u} Y Y) (biprod.lift (rightAdd X Y f g) (rightAdd X Y h k)) biprod.fst =
  (biprod.lift (𝟙 X) (𝟙 X) ≫ diag) ≫ biprod.fst
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
f g h k : X ⟶ Y
diag : biprod.{v, u} X X ⟶ biprod.{v, u} Y Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
hd₂ : biprod.inr ≫ diag = biprod.lift g k
h₀ :
  CategoryStruct.comp (Y := biprod.{v, u} Y Y) (biprod.lift (rightAdd X Y f g) (rightAdd X Y h k)) biprod.fst =
    (biprod.lift (𝟙 X) (𝟙 X) ≫ diag) ≫ biprod.fst
⊢ biprod.lift (rightAdd X Y f g) (rightAdd X Y h k) = biprod.lift (𝟙 X) (𝟙 X) ≫ diag
have h₁ : CategoryStruct.comp (Y := biprod.{v, u} Y Y) (biprod.lift (rightAdd X Y f g) (rightAdd X Y h k)) biprod.snd =
  (biprod.lift (𝟙 X) (𝟙 X) ≫ diag) ≫ biprod.snd
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
f g h k : X ⟶ Y
diag : biprod.{v, u} X X ⟶ biprod.{v, u} Y Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
hd₂ : biprod.inr ≫ diag = biprod.lift g k
⊢ leftAdd X Y (rightAdd X Y f g) (rightAdd X Y h k) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
have h₁ : biprod.lift (rightAdd X Y f g) (rightAdd X Y h k) = biprod.lift (𝟙 X) (𝟙 X) ≫ diag
Tactic: have h₁ : biprod.lift (f +ᵣ g) (h +ᵣ k) = biprod.lift (𝟙 X) (𝟙 X) ≫ diag := by
    ext <;> cat_disch
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
f g h k : X ⟶ Y
diag : biprod.{v, u} X X ⟶ biprod.{v, u} Y Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
hd₂ : biprod.inr ≫ diag = biprod.lift g k
h₁ : biprod.lift (rightAdd X Y f g) (rightAdd X Y h k) = biprod.lift (𝟙 X) (𝟙 X) ≫ diag
⊢ diag ≫ biprod.desc (𝟙 Y) (𝟙 Y) = biprod.desc (leftAdd X Y f h) (leftAdd X Y g k)
have h₀ : biprod.inl ≫ diag ≫ biprod.desc (𝟙 Y) (𝟙 Y) =
  CategoryStruct.comp (Y := biprod.{v, u} X X) biprod.inl (biprod.desc (leftAdd X Y f h) (leftAdd X Y g k))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
f g h k : X ⟶ Y
diag : biprod.{v, u} X X ⟶ biprod.{v, u} Y Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
hd₂ : biprod.inr ≫ diag = biprod.lift g k
h₁ : biprod.lift (rightAdd X Y f g) (rightAdd X Y h k) = biprod.lift (𝟙 X) (𝟙 X) ≫ diag
h₀ :
  biprod.inl ≫ diag ≫ biprod.desc (𝟙 Y) (𝟙 Y) =
    CategoryStruct.comp (Y := biprod.{v, u} X X) biprod.inl (biprod.desc (leftAdd X Y f h) (leftAdd X Y g k))
⊢ diag ≫ biprod.desc (𝟙 Y) (𝟙 Y) = biprod.desc (leftAdd X Y f h) (leftAdd X Y g k)
have h₂ : biprod.inr ≫ diag ≫ biprod.desc (𝟙 Y) (𝟙 Y) =
  CategoryStruct.comp (Y := biprod.{v, u} X X) biprod.inr (biprod.desc (leftAdd X Y f h) (leftAdd X Y g k))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
f g h k : X ⟶ Y
diag : biprod.{v, u} X X ⟶ biprod.{v, u} Y Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
hd₂ : biprod.inr ≫ diag = biprod.lift g k
h₁ : biprod.lift (rightAdd X Y f g) (rightAdd X Y h k) = biprod.lift (𝟙 X) (𝟙 X) ≫ diag
⊢ leftAdd X Y (rightAdd X Y f g) (rightAdd X Y h k) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
have h₂ : diag ≫ biprod.desc (𝟙 Y) (𝟙 Y) = biprod.desc (leftAdd X Y f h) (leftAdd X Y g k)
Tactic: have h₂ : diag ≫ biprod.desc (𝟙 Y) (𝟙 Y) = biprod.desc (f +ₗ h) (g +ₗ k) := by
    ext <;> simp [reassoc_of% hd₁, reassoc_of% hd₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
f g h k : X ⟶ Y
diag : biprod.{v, u} X X ⟶ biprod.{v, u} Y Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
hd₂ : biprod.inr ≫ diag = biprod.lift g k
h₁ : biprod.lift (rightAdd X Y f g) (rightAdd X Y h k) = biprod.lift (𝟙 X) (𝟙 X) ≫ diag
h₂ : diag ≫ biprod.desc (𝟙 Y) (𝟙 Y) = biprod.desc (leftAdd X Y f h) (leftAdd X Y g k)
⊢ leftAdd X Y (rightAdd X Y f g) (rightAdd X Y h k) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
have rw : CategoryStruct.comp (Y := biprod.{v, u} Y Y) (biprod.lift (rightAdd X Y f g) (rightAdd X Y h k))
    (biprod.desc (𝟙 Y) (𝟙 Y)) =
  rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
Tactic: rw [leftAdd, h₁, Category.assoc, h₂, rightAdd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
f g h k : X ⟶ Y
diag : biprod.{v, u} X X ⟶ biprod.{v, u} Y Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
hd₂ : biprod.inr ≫ diag = biprod.lift g k
h₁ : biprod.lift (rightAdd X Y f g) (rightAdd X Y h k) = biprod.lift (𝟙 X) (𝟙 X) ≫ diag
h₂ : diag ≫ biprod.desc (𝟙 Y) (𝟙 Y) = biprod.desc (leftAdd X Y f h) (leftAdd X Y g k)
rw :
  CategoryStruct.comp (Y := biprod.{v, u} Y Y) (biprod.lift (rightAdd X Y f g) (rightAdd X Y h k))
      (biprod.desc (𝟙 Y) (𝟙 Y)) =
    rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
⊢ leftAdd X Y (rightAdd X Y f g) (rightAdd X Y h k) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
have rw₁ : (biprod.lift (𝟙 X) (𝟙 X) ≫ diag) ≫ biprod.desc (𝟙 Y) (𝟙 Y) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
Tactic: rw [leftAdd, h₁, Category.assoc, h₂, rightAdd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
f g h k : X ⟶ Y
diag : biprod.{v, u} X X ⟶ biprod.{v, u} Y Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
hd₂ : biprod.inr ≫ diag = biprod.lift g k
h₁ : biprod.lift (rightAdd X Y f g) (rightAdd X Y h k) = biprod.lift (𝟙 X) (𝟙 X) ≫ diag
h₂ : diag ≫ biprod.desc (𝟙 Y) (𝟙 Y) = biprod.desc (leftAdd X Y f h) (leftAdd X Y g k)
rw :
  CategoryStruct.comp (Y := biprod.{v, u} Y Y) (biprod.lift (rightAdd X Y f g) (rightAdd X Y h k))
      (biprod.desc (𝟙 Y) (𝟙 Y)) =
    rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
rw₁ : (biprod.lift (𝟙 X) (𝟙 X) ≫ diag) ≫ biprod.desc (𝟙 Y) (𝟙 Y) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
⊢ leftAdd X Y (rightAdd X Y f g) (rightAdd X Y h k) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
have rw₂ : biprod.lift (𝟙 X) (𝟙 X) ≫ diag ≫ biprod.desc (𝟙 Y) (𝟙 Y) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
Tactic: rw [leftAdd, h₁, Category.assoc, h₂, rightAdd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
f g h k : X ⟶ Y
diag : biprod.{v, u} X X ⟶ biprod.{v, u} Y Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
hd₂ : biprod.inr ≫ diag = biprod.lift g k
h₁ : biprod.lift (rightAdd X Y f g) (rightAdd X Y h k) = biprod.lift (𝟙 X) (𝟙 X) ≫ diag
h₂ : diag ≫ biprod.desc (𝟙 Y) (𝟙 Y) = biprod.desc (leftAdd X Y f h) (leftAdd X Y g k)
rw :
  CategoryStruct.comp (Y := biprod.{v, u} Y Y) (biprod.lift (rightAdd X Y f g) (rightAdd X Y h k))
      (biprod.desc (𝟙 Y) (𝟙 Y)) =
    rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
rw₁ : (biprod.lift (𝟙 X) (𝟙 X) ≫ diag) ≫ biprod.desc (𝟙 Y) (𝟙 Y) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
rw₂ : biprod.lift (𝟙 X) (𝟙 X) ≫ diag ≫ biprod.desc (𝟙 Y) (𝟙 Y) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
⊢ leftAdd X Y (rightAdd X Y f g) (rightAdd X Y h k) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
have rw₃ : CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X))
    (biprod.desc (leftAdd X Y f h) (leftAdd X Y g k)) =
  rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
Tactic: rw [leftAdd, h₁, Category.assoc, h₂, rightAdd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
f g h k : X ⟶ Y
diag : biprod.{v, u} X X ⟶ biprod.{v, u} Y Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
hd₂ : biprod.inr ≫ diag = biprod.lift g k
h₁ : biprod.lift (rightAdd X Y f g) (rightAdd X Y h k) = biprod.lift (𝟙 X) (𝟙 X) ≫ diag
h₂ : diag ≫ biprod.desc (𝟙 Y) (𝟙 Y) = biprod.desc (leftAdd X Y f h) (leftAdd X Y g k)
rw :
  CategoryStruct.comp (Y := biprod.{v, u} Y Y) (biprod.lift (rightAdd X Y f g) (rightAdd X Y h k))
      (biprod.desc (𝟙 Y) (𝟙 Y)) =
    rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
rw₁ : (biprod.lift (𝟙 X) (𝟙 X) ≫ diag) ≫ biprod.desc (𝟙 Y) (𝟙 Y) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
rw₂ : biprod.lift (𝟙 X) (𝟙 X) ≫ diag ≫ biprod.desc (𝟙 Y) (𝟙 Y) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
rw₃ :
  CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X))
      (biprod.desc (leftAdd X Y f h) (leftAdd X Y g k)) =
    rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
⊢ leftAdd X Y (rightAdd X Y f g) (rightAdd X Y h k) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
have rw₄ : CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X))
    (biprod.desc (leftAdd X Y f h) (leftAdd X Y g k)) =
  CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X))
    (biprod.desc (leftAdd X Y f h) (leftAdd X Y g k))
Tactic: rw [leftAdd, h₁, Category.assoc, h₂, rightAdd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ (f + g) ≫ h = f ≫ h + g ≫ h
have simp : CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g ≫ h) =
  CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc (f ≫ h) (g ≫ h))
Tactic: simp only [add_eq_right_addition, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g ≫ h) =
    CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc (f ≫ h) (g ≫ h))
have e_a : Eq (α := biprod.{v, u} X X ⟶ Z) (biprod.desc f g ≫ h) (biprod.desc (f ≫ h) (g ≫ h))
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ Eq (α := biprod.{v, u} X X ⟶ Z) (biprod.desc f g ≫ h) (biprod.desc (f ≫ h) (g ≫ h))
have e_a : CategoryStruct.comp (Y := biprod.{v, u} X X) biprod.inl (biprod.desc f g ≫ h) =
  CategoryStruct.comp (Y := biprod.{v, u} X X) biprod.inl (biprod.desc (f ≫ h) (g ≫ h))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
e_a :
  CategoryStruct.comp (Y := biprod.{v, u} X X) biprod.inl (biprod.desc f g ≫ h) =
    CategoryStruct.comp (Y := biprod.{v, u} X X) biprod.inl (biprod.desc (f ≫ h) (g ≫ h))
⊢ Eq (α := biprod.{v, u} X X ⟶ Z) (biprod.desc f g ≫ h) (biprod.desc (f ≫ h) (g ≫ h))
have e_a₁ : CategoryStruct.comp (Y := biprod.{v, u} X X) biprod.inr (biprod.desc f g ≫ h) =
  CategoryStruct.comp (Y := biprod.{v, u} X X) biprod.inr (biprod.desc (f ≫ h) (g ≫ h))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y Z : C
f : X ⟶ Y
g h : Y ⟶ Z
⊢ f ≫ (g + h) = f ≫ g + f ≫ h
have simp : CategoryStruct.comp (Y := biprod.{v, u} Z Z) (f ≫ biprod.lift g h) (biprod.desc (𝟙 Z) (𝟙 Z)) =
  CategoryStruct.comp (Y := biprod.{v, u} Z Z) (biprod.lift (f ≫ g) (f ≫ h)) (biprod.desc (𝟙 Z) (𝟙 Z))
Tactic: simp only [add_eq_left_addition, ← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y Z : C
f : X ⟶ Y
g h : Y ⟶ Z
⊢ CategoryStruct.comp (Y := biprod.{v, u} Z Z) (f ≫ biprod.lift g h) (biprod.desc (𝟙 Z) (𝟙 Z)) =
    CategoryStruct.comp (Y := biprod.{v, u} Z Z) (biprod.lift (f ≫ g) (f ≫ h)) (biprod.desc (𝟙 Z) (𝟙 Z))
have e_a : Eq (α := X ⟶ biprod.{v, u} Z Z) (f ≫ biprod.lift g h) (biprod.lift (f ≫ g) (f ≫ h))
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y Z : C
f : X ⟶ Y
g h : Y ⟶ Z
⊢ Eq (α := X ⟶ biprod.{v, u} Z Z) (f ≫ biprod.lift g h) (biprod.lift (f ≫ g) (f ≫ h))
have e_a : CategoryStruct.comp (Y := biprod.{v, u} Z Z) (f ≫ biprod.lift g h) biprod.fst =
  CategoryStruct.comp (Y := biprod.{v, u} Z Z) (biprod.lift (f ≫ g) (f ≫ h)) biprod.fst
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.OfBiproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y Z : C
f : X ⟶ Y
g h : Y ⟶ Z
e_a :
  CategoryStruct.comp (Y := biprod.{v, u} Z Z) (f ≫ biprod.lift g h) biprod.fst =
    CategoryStruct.comp (Y := biprod.{v, u} Z Z) (biprod.lift (f ≫ g) (f ≫ h)) biprod.fst
⊢ Eq (α := X ⟶ biprod.{v, u} Z Z) (f ≫ biprod.lift g h) (biprod.lift (f ≫ g) (f ≫ h))
have e_a₁ : CategoryStruct.comp (Y := biprod.{v, u} Z Z) (f ≫ biprod.lift g h) biprod.snd =
  CategoryStruct.comp (Y := biprod.{v, u} Z Z) (biprod.lift (f ≫ g) (f ≫ h)) biprod.snd
Tactic: ext