awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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)
hl : ∀ (f : X ⟶ Y), Eq (α := X ⟶ biprod.{v, u} Y Y) (biprod.lift f 0) (f ≫ biprod.inl)
⊢ EckmannHilton.IsUnital (fun (x1 x2 : X ⟶ Y) ↦ leftAdd X Y x1 x2) 0

Tactic:
exact {
    left_id := fun f => by simp [hr f, leftAdd, Category.assoc, Category.comp_id, biprod.inr_desc],
    right_id := fun f => by simp [hl f, leftAdd, Category.assoc, Category.comp_id, biprod.inl_desc]
  }
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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))
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)
⊢ Eq (α := biprod.{v, u} X X ⟶ Y) (biprod.desc 0 f) (biprod.snd ≫ f)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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 (α := 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:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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
⊢ 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:
simp only [biprod.inr_desc, BinaryBicone.inr_snd_assoc]

Premises used: CategoryTheory.Limits.biprod.inr_desc, CategoryTheory.Limits.BinaryBicone.inr_snd_assoc
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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)

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]
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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)
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))
⊢ Eq (α := biprod.{v, u} X X ⟶ Y) (biprod.desc f 0) (biprod.fst ≫ f)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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
⊢ 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:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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 (α := 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:
simp only [biprod.inr_desc, BinaryBicone.inr_fst_assoc, zero_comp]

Premises used: CategoryTheory.Limits.BinaryBicone.inr_fst_assoc, CategoryTheory.Limits.biprod.inr_desc, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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)

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]
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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)
h₁ : ∀ (f : X ⟶ Y), Eq (α := biprod.{v, u} X X ⟶ Y) (biprod.desc f 0) (biprod.fst ≫ f)
f : X ⟶ Y
⊢ rightAdd X Y 0 f = f

Tactic:
simp [h₂ f, rightAdd, biprod.lift_snd_assoc, Category.id_comp]

Premises used: CategoryTheory.SemiadditiveOfBinaryBiproducts.rightAdd, CategoryTheory.Limits.biprod.lift_snd_assoc, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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)
h₁ : ∀ (f : X ⟶ Y), Eq (α := biprod.{v, u} X X ⟶ Y) (biprod.desc f 0) (biprod.fst ≫ f)
f : X ⟶ Y
⊢ rightAdd X Y f 0 = f

Tactic:
simp [h₁ f, rightAdd, biprod.lift_fst_assoc, Category.id_comp]

Premises used: CategoryTheory.Limits.biprod.lift_fst_assoc, CategoryTheory.SemiadditiveOfBinaryBiproducts.rightAdd, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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)
h₁ : ∀ (f : X ⟶ Y), Eq (α := biprod.{v, u} X X ⟶ Y) (biprod.desc f 0) (biprod.fst ≫ f)
⊢ EckmannHilton.IsUnital (fun (x1 x2 : X ⟶ Y) ↦ rightAdd X Y x1 x2) 0

Tactic:
exact {
    left_id := fun f => by simp [h₂ f, rightAdd, biprod.lift_snd_assoc, Category.id_comp],
    right_id := fun f => by simp [h₁ f, rightAdd, biprod.lift_fst_assoc, Category.id_comp]
  }
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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
h₁ : (biprod.inl ≫ diag) ≫ biprod.snd = CategoryStruct.comp (Y := biprod.{v, u} Y Y) (biprod.lift f h) biprod.snd
⊢ biprod.inl ≫ diag = biprod.lift f h

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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.fst = CategoryStruct.comp (Y := biprod.{v, u} Y Y) (biprod.lift f h) biprod.fst

Tactic:
simp [diag]
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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.snd = CategoryStruct.comp (Y := biprod.{v, u} Y Y) (biprod.lift f h) biprod.snd

Tactic:
simp [diag]
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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

Tactic:
have hd₁ : biprod.inl ≫ diag = biprod.lift f h := by ext <;> simp [diag]
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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
h₁ : (biprod.inr ≫ diag) ≫ biprod.snd = CategoryStruct.comp (Y := biprod.{v, u} Y Y) (biprod.lift g k) biprod.snd
⊢ biprod.inr ≫ diag = biprod.lift g k

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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.fst = CategoryStruct.comp (Y := biprod.{v, u} Y Y) (biprod.lift g k) biprod.fst

Tactic:
simp [diag]
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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.snd = CategoryStruct.comp (Y := biprod.{v, u} Y Y) (biprod.lift g k) biprod.snd

Tactic:
simp [diag]
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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

Tactic:
have hd₂ : biprod.inr ≫ diag = biprod.lift g k := by ext <;> simp [diag]
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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
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
⊢ biprod.lift (rightAdd X Y f g) (rightAdd X Y h k) = biprod.lift (𝟙 X) (𝟙 X) ≫ diag

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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

Tactic:
have h₁ : biprod.lift (f +ᵣ g) (h +ᵣ k) = biprod.lift (𝟙 X) (𝟙 X) ≫ diag := by
    ext <;> cat_disch
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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))
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))
⊢ diag ≫ biprod.desc (𝟙 Y) (𝟙 Y) = biprod.desc (leftAdd X Y f h) (leftAdd X Y g k)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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
⊢ 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:
simp [reassoc_of% hd₁, reassoc_of% hd₂]
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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
⊢ 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:
simp [reassoc_of% hd₁, reassoc_of% hd₂]
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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)

Tactic:
have h₂ : diag ≫ biprod.desc (𝟙 Y) (𝟙 Y) = biprod.desc (f +ₗ h) (g +ₗ k) := by
    ext <;> simp [reassoc_of% hd₁, reassoc_of% hd₂]
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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)
rw₄ 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))
⊢ 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)

Tactic:
rw [leftAdd, h₁, Category.assoc, h₂, rightAdd]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.SemiadditiveOfBinaryBiproducts.rightAdd, CategoryTheory.SemiadditiveOfBinaryBiproducts.leftAdd
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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 : X ⟶ Y
⊢ f + g = CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)

Tactic:
rfl

Premises used: CategoryTheory.SemiadditiveOfBinaryBiproducts.rightAdd, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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 : X ⟶ Y
⊢ f + g = CategoryStruct.comp (Y := biprod.{v, u} Y Y) (biprod.lift f g) (biprod.desc (𝟙 Y) (𝟙 Y))

Tactic:
congr_fun₂ (EckmannHilton.mul (isUnital_leftAdd X Y) (isUnital_rightAdd X Y) (distrib X Y)).symm f
    g

Premises used: EckmannHilton.mul, congr_fun₂, CategoryTheory.SemiadditiveOfBinaryBiproducts.isUnital_leftAdd, CategoryTheory.SemiadditiveOfBinaryBiproducts.distrib, CategoryTheory.SemiadditiveOfBinaryBiproducts.leftAdd, CategoryTheory.SemiadditiveOfBinaryBiproducts.isUnital_rightAdd, Eq.symm
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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
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))
⊢ (f + g) ≫ h = f ≫ h + g ≫ h

Tactic:
simp only [add_eq_right_addition, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.SemiadditiveOfBinaryBiproducts.add_eq_right_addition
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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 : Eq (α := biprod.{v, u} X X ⟶ Z) (biprod.desc f g ≫ h) (biprod.desc (f ≫ h) (g ≫ h))
⊢ 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:
congr
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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))
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))
⊢ Eq (α := biprod.{v, u} X X ⟶ Z) (biprod.desc f g ≫ h) (biprod.desc (f ≫ h) (g ≫ h))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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.inl (biprod.desc f g ≫ h) =
    CategoryStruct.comp (Y := biprod.{v, u} X X) biprod.inl (biprod.desc (f ≫ h) (g ≫ h))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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.inr (biprod.desc f g ≫ h) =
    CategoryStruct.comp (Y := biprod.{v, u} X X) biprod.inr (biprod.desc (f ≫ h) (g ≫ h))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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
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))
⊢ f ≫ (g + h) = f ≫ g + f ≫ h

Tactic:
simp only [add_eq_left_addition, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.SemiadditiveOfBinaryBiproducts.add_eq_left_addition
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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 : Eq (α := X ⟶ biprod.{v, u} Z Z) (f ≫ biprod.lift g h) (biprod.lift (f ≫ g) (f ≫ h))
⊢ 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:
congr
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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
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
⊢ Eq (α := X ⟶ biprod.{v, u} Z Z) (f ≫ biprod.lift g h) (biprod.lift (f ≫ g) (f ≫ h))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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.fst =
    CategoryStruct.comp (Y := biprod.{v, u} Z Z) (biprod.lift (f ≫ g) (f ≫ h)) biprod.fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts
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.snd =
    CategoryStruct.comp (Y := biprod.{v, u} Z Z) (biprod.lift (f ≫ g) (f ≫ h)) biprod.snd

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Opposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
⊢ Eq (α := Limits.HasZeroMorphisms.{v_1, u_1} Cᵒᵖ) Preadditive.preadditiveHasZeroMorphisms
    Limits.hasZeroMorphismsOpposite

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Opposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
⊢ Eq (α := Limits.HasZeroMorphisms.{v_1, u_1} Cᵒᵖ) Preadditive.preadditiveHasZeroMorphisms
    Limits.hasZeroMorphismsOpposite

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Opposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ (f + g).unop = f.unop + g.unop

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Opposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ (f - g).unop = f.unop - g.unop

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Opposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : Cᵒᵖ
k : ℤ
f : X ⟶ Y
⊢ (k • f).unop = k • f.unop

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl