awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsLimit b.fstKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
⊢ (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0

Tactic:
have h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0 := by simpa using sub_eq_zero.2 h₁
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsLimit b.fstKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
⊢ (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0

Tactic:
simpa using sub_eq_zero.2 h₂

Premises used: Iff.mpr, sub_eq_zero
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsLimit b.fstKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
⊢ (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0

Tactic:
have h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0 := by simpa using sub_eq_zero.2 h₂
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsLimit b.fstKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0
obtain :
  ∀ (q : T ⟶ Y) (hq : q ≫ b.inr = m - (f ≫ b.inl + g ≫ b.inr)),
    m = (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g
⊢ m = (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g

Tactic:
obtain ⟨q : T ⟶ Y, hq : q ≫ b.inr = m - (f ≫ b.inl + g ≫ b.inr)⟩ :=
        KernelFork.IsLimit.lift' hb _ h₁'

Premises used: CategoryTheory.Limits.BinaryBicone.inl, CategoryTheory.Limits.KernelFork.IsLimit.lift', CategoryTheory.Limits.BinaryBicone.inr, HAdd.hAdd, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsLimit b.fstKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0
q : T ⟶ Y
hq : q ≫ b.inr = m - (f ≫ b.inl + g ≫ b.inr)
rw : m - (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g = 0
rw₁ : q ≫ b.inr = 0
rw₂ : (q ≫ 𝟙 Y) ≫ b.inr = 0
rw₃ : (q ≫ b.inr ≫ b.snd) ≫ b.inr = 0
rw₄ : ((q ≫ b.inr) ≫ b.snd) ≫ b.inr = 0
rw₅ : ((m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd) ≫ b.inr = 0
rw₆ : Eq (α := T ⟶ b.toCone.pt) (0 ≫ b.inr) 0
rw₇ rw₈ : Eq.{v + 1} (α := T ⟶ b.toCone.pt) 0 0
⊢ m = (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g

Tactic:
rw [← sub_eq_zero, ← hq, ← Category.comp_id q, ← b.inr_snd, ← Category.assoc, hq, h₂',
        zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.BinaryBicone.inr_snd, sub_eq_zero, CategoryTheory.Category.comp_id, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsColimit b.inrCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
⊢ BinaryCofan.inl b.toCocone ≫ (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsColimit b.inrCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
⊢ BinaryCofan.inr b.toCocone ≫ (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g = g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsColimit b.inrCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
⊢ b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0

Tactic:
simpa using sub_eq_zero.2 h₁

Premises used: Iff.mpr, sub_eq_zero
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsColimit b.inrCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
⊢ b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0

Tactic:
have h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0 := by simpa using sub_eq_zero.2 h₁
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsColimit b.inrCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
⊢ b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0

Tactic:
simpa using sub_eq_zero.2 h₂

Premises used: Iff.mpr, sub_eq_zero
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsColimit b.inrCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
⊢ b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0

Tactic:
have h₂' : b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0 := by simpa using sub_eq_zero.2 h₂
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsColimit b.inrCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
h₂' : b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
obtain :
  ∀ (q : X ⟶ T) (hq : b.fst ≫ q = m - (b.fst ≫ f + b.snd ≫ g)),
    m = (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g
⊢ m = (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g

Tactic:
obtain ⟨q : X ⟶ T, hq : b.fst ≫ q = m - (b.fst ≫ f + b.snd ≫ g)⟩ :=
        CokernelCofork.IsColimit.desc' hb _ h₂'

Premises used: CategoryTheory.Limits.BinaryBicone.fst, CategoryTheory.Limits.CokernelCofork.IsColimit.desc', CategoryTheory.Limits.BinaryBicone.snd, HAdd.hAdd, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsColimit b.inrCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
h₂' : b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
q : X ⟶ T
hq : b.fst ≫ q = m - (b.fst ≫ f + b.snd ≫ g)
rw : m - (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g = 0
rw₁ : b.fst ≫ q = 0
rw₂ : b.fst ≫ 𝟙 X ≫ q = 0
rw₃ : b.fst ≫ (b.inl ≫ b.fst) ≫ q = 0
rw₄ : b.fst ≫ b.inl ≫ b.fst ≫ q = 0
rw₅ : b.fst ≫ b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
rw₆ : Eq (α := b.toCocone.pt ⟶ T) (b.fst ≫ 0) 0
rw₇ rw₈ : Eq.{v + 1} (α := b.toCocone.pt ⟶ T) 0 0
⊢ m = (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g

Tactic:
rw [← sub_eq_zero, ← hq, ← Category.id_comp q, ← b.inl_fst, Category.assoc, hq, h₁',
        comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.BinaryBicone.inl_fst, sub_eq_zero, CategoryTheory.Limits.comp_zero, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsColimit b.inlCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
⊢ BinaryCofan.inl b.toCocone ≫ (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsColimit b.inlCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
⊢ BinaryCofan.inr b.toCocone ≫ (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g = g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsColimit b.inlCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
⊢ b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0

Tactic:
simpa using sub_eq_zero.2 h₁

Premises used: Iff.mpr, sub_eq_zero
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsColimit b.inlCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
⊢ b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0

Tactic:
have h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0 := by simpa using sub_eq_zero.2 h₁
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsColimit b.inlCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
⊢ b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0

Tactic:
simpa using sub_eq_zero.2 h₂

Premises used: Iff.mpr, sub_eq_zero
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsColimit b.inlCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
⊢ b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0

Tactic:
have h₂' : b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0 := by simpa using sub_eq_zero.2 h₂
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsColimit b.inlCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
h₂' : b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
obtain :
  ∀ (q : Y ⟶ T) (hq : b.snd ≫ q = m - (b.fst ≫ f + b.snd ≫ g)),
    m = (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g
⊢ m = (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g

Tactic:
obtain ⟨q : Y ⟶ T, hq : b.snd ≫ q = m - (b.fst ≫ f + b.snd ≫ g)⟩ :=
        CokernelCofork.IsColimit.desc' hb _ h₁'

Premises used: CategoryTheory.Limits.BinaryBicone.fst, CategoryTheory.Limits.CokernelCofork.IsColimit.desc', CategoryTheory.Limits.BinaryBicone.snd, HAdd.hAdd, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsColimit b.inlCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
h₂' : b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
q : Y ⟶ T
hq : b.snd ≫ q = m - (b.fst ≫ f + b.snd ≫ g)
rw : m - (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g = 0
rw₁ : b.snd ≫ q = 0
rw₂ : b.snd ≫ 𝟙 Y ≫ q = 0
rw₃ : b.snd ≫ (b.inr ≫ b.snd) ≫ q = 0
rw₄ : b.snd ≫ b.inr ≫ b.snd ≫ q = 0
rw₅ : b.snd ≫ b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
rw₆ : Eq (α := b.toCocone.pt ⟶ T) (b.snd ≫ 0) 0
rw₇ rw₈ : Eq.{v + 1} (α := b.toCocone.pt ⟶ T) 0 0
⊢ m = (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g

Tactic:
rw [← sub_eq_zero, ← hq, ← Category.id_comp q, ← b.inr_snd, Category.assoc, hq, h₂',
        comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.BinaryBicone.inr_snd, sub_eq_zero, CategoryTheory.Limits.comp_zero, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitEpi f
c : KernelFork f
i : IsLimit c
⊢ Fork.ι c ≫ (𝟙 X - (𝟙 X - f ≫ section_ f)) = 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitEpi f
c : KernelFork f
i : IsLimit c
c' : KernelFork (𝟙 X - (𝟙 X - f ≫ section_ f)) := KernelFork.ofι (Fork.ι c) ⋯
⊢ 𝟙 X - (𝟙 X - f ≫ section_ f) = f ≫ section_ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitEpi f
c : KernelFork f
i : IsLimit c
c' : KernelFork (𝟙 X - (𝟙 X - f ≫ section_ f)) := KernelFork.ofι (Fork.ι c) ⋯
i' : IsLimit c' := isKernelCompMono i (section_ f) ⋯
i'' : IsLimit (forkOfKernelFork c') := isLimitForkOfKernelFork i'
⊢ (𝟙 X - f ≫ section_ f) ≫ (𝟙 X - f ≫ section_ f) = 𝟙 X - f ≫ section_ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitEpi f
c : KernelFork f
i : IsLimit c
⊢ (Fork.ι c ≫
      let c' : KernelFork (𝟙 X - (𝟙 X - f ≫ section_ f)) := KernelFork.ofι (Fork.ι c) ⋯;
      let i' : IsLimit c' := isKernelCompMono i (section_ f) ⋯;
      let i'' := isLimitForkOfKernelFork i';
      (splitMonoOfIdempotentOfIsLimitFork C ⋯ i'').retraction) =
    𝟙 c.pt

Tactic:
apply SplitMono.id

Premises used: CategoryTheory.SplitMono.id
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitEpi f
c : KernelFork f
i : IsLimit c
⊢ Fork.ι c ≫ f = 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitEpi f
c : KernelFork f
i : IsLimit c
dsimp :
  Eq (α := Y ⟶ c.pt)
    (section_ f ≫
        SplitMono.retraction (f := Fork.ι (forkOfKernelFork (KernelFork.ofι (Fork.ι c) ⋯)))
          (splitMonoOfIdempotentOfIsLimitFork C ⋯ (isLimitForkOfKernelFork (isKernelCompMono i (section_ f) ⋯)) :
            SplitMono (X :=
              Cone.pt (F := parallelPair (𝟙 X) (𝟙 X - f ≫ section_ f)) (forkOfKernelFork (KernelFork.ofι (Fork.ι c) ⋯)))
              (Fork.ι (forkOfKernelFork (KernelFork.ofι (Fork.ι c) ⋯)))) :
      Y ⟶ c.pt)
    (0 : Y ⟶ c.pt)
⊢ Eq (α := Y ⟶ c.pt)
    (section_ f ≫
      let c' : KernelFork (𝟙 X - (𝟙 X - f ≫ section_ f)) := KernelFork.ofι (Fork.ι c) ⋯;
      let i' : IsLimit c' := isKernelCompMono i (section_ f) ⋯;
      let i'' := isLimitForkOfKernelFork i';
      (splitMonoOfIdempotentOfIsLimitFork C ⋯ i'').retraction)
    0

Tactic:
dsimp only
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitEpi f
c : KernelFork f
i : IsLimit c
rw :
  Eq (α := Y ⟶ c.pt) (section_ f ≫ i.lift (Fork.ofι (Fork.ι (kernelForkOfFork (Fork.ofι (𝟙 X - f ≫ section_ f) ⋯))) ⋯))
    0
⊢ Eq (α := Y ⟶ c.pt)
    (section_ f ≫
        SplitMono.retraction (f := Fork.ι (forkOfKernelFork (KernelFork.ofι (Fork.ι c) ⋯)))
          (splitMonoOfIdempotentOfIsLimitFork C ⋯ (isLimitForkOfKernelFork (isKernelCompMono i (section_ f) ⋯)) :
            SplitMono (X :=
              Cone.pt (F := parallelPair (𝟙 X) (𝟙 X - f ≫ section_ f)) (forkOfKernelFork (KernelFork.ofι (Fork.ι c) ⋯)))
              (Fork.ι (forkOfKernelFork (KernelFork.ofι (Fork.ι c) ⋯)))) :
      Y ⟶ c.pt)
    (0 : Y ⟶ c.pt)

Tactic:
rw [splitMonoOfIdempotentOfIsLimitFork_retraction, isLimitForkOfKernelFork_lift,
        isKernelCompMono_lift]

Premises used: CategoryTheory.Limits.isKernelCompMono_lift, CategoryTheory.Preadditive.isLimitForkOfKernelFork_lift, CategoryTheory.Limits.splitMonoOfIdempotentOfIsLimitFork_retraction
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitEpi f
c : KernelFork f
i : IsLimit c
dsimp : Eq (α := Y ⟶ c.pt) (section_ f ≫ i.lift (Fork.ofι (Fork.ofι (𝟙 X - f ≫ section_ f) ⋯).ι ⋯)) 0
⊢ Eq (α := Y ⟶ c.pt) (section_ f ≫ i.lift (Fork.ofι (Fork.ι (kernelForkOfFork (Fork.ofι (𝟙 X - f ≫ section_ f) ⋯))) ⋯))
    0

Tactic:
dsimp only [kernelForkOfFork_ι]

Premises used: CategoryTheory.Preadditive.kernelForkOfFork_ι
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitEpi f
c : KernelFork f
i : IsLimit c
this : Mono (Fork.ι c) := ⋯
apply : (section_ f ≫ i.lift (Fork.ofι (Fork.ofι (𝟙 X - f ≫ section_ f) ⋯).ι ⋯)) ≫ Fork.ι c = 0
⊢ Eq (α := Y ⟶ c.pt) (section_ f ≫ i.lift (Fork.ofι (Fork.ofι (𝟙 X - f ≫ section_ f) ⋯).ι ⋯)) 0

Tactic:
apply zero_of_comp_mono c.ι

Premises used: CategoryTheory.Limits.zero_of_comp_mono, CategoryTheory.Limits.Fork.ι
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitEpi f
c : KernelFork f
i : IsLimit c
this : Mono (Fork.ι c) := ⋯
⊢ (section_ f ≫ i.lift (Fork.ofι (Fork.ofι (𝟙 X - f ≫ section_ f) ⋯).ι ⋯)) ≫ Fork.ι c = 0

Tactic:
simp only [comp_sub, Category.comp_id, Category.assoc, sub_self, Fork.IsLimit.lift_ι,
        Fork.ι_ofι, IsSplitEpi.id_assoc]

Premises used: CategoryTheory.Category.assoc, sub_self, CategoryTheory.Category.comp_id, CategoryTheory.Limits.Fork.IsLimit.lift_ι, CategoryTheory.IsSplitEpi.id_assoc, CategoryTheory.Preadditive.comp_sub, CategoryTheory.Limits.Fork.ι_ofι
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitEpi f
c : KernelFork f
i : IsLimit c
⊢ section_ f ≫ f = 𝟙 Y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitEpi f
c : KernelFork f
i : IsLimit c
⊢ Iso.hom (Iso.refl c.pt) ≫ Fork.ι (binaryBiconeOfIsSplitEpiOfKernel i).sndKernelFork = Fork.ι c

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
inst_2 : HasBinaryBiproduct.{v, u} X X
⊢ f + g = CategoryStruct.comp (Y := biprod.{v, u} X X) (lift (𝟙 X) (𝟙 X)) (desc f g)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
inst_2 : HasBinaryBiproduct.{v, u} Y Y
⊢ f + g = CategoryStruct.comp (Y := biprod.{v, u} Y Y) (lift f g) (desc (𝟙 Y) (𝟙 Y))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
inst_1 : Preadditive.{v, u} C_1
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasBinaryBiproducts.{v, u} C
a b : Preadditive.{v, u} C
homGroup : Eq (α := (P Q : C) → AddCommGroup (P ⟶ Q)) Preadditive.homGroup Preadditive.homGroup
⊢ a = b

Tactic:
apply Preadditive.ext

Premises used: CategoryTheory.Preadditive.ext
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
inst_1 : Preadditive.{v, u} C_1
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasBinaryBiproducts.{v, u} C
a b : Preadditive.{v, u} C
homGroup : ∀ (X Y : C), Eq.{v + 1} (α := AddCommGroup (X ⟶ Y)) (Preadditive.homGroup X Y) (Preadditive.homGroup X Y)
⊢ Eq (α := (P Q : C) → AddCommGroup (P ⟶ Q)) Preadditive.homGroup Preadditive.homGroup

Tactic:
funext X Y
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
inst_1 : Preadditive.{v, u} C_1
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasBinaryBiproducts.{v, u} C
a b : Preadditive.{v, u} C
X Y : C
homGroup : Eq (α := (X ⟶ Y) → (X ⟶ Y) → (X ⟶ Y)) HAdd.hAdd HAdd.hAdd
⊢ Eq.{v + 1} (α := AddCommGroup (X ⟶ Y)) (Preadditive.homGroup X Y) (Preadditive.homGroup X Y)

Tactic:
apply AddCommGroup.ext

Premises used: AddCommGroup.ext
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
inst_1 : Preadditive.{v, u} C_1
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasBinaryBiproducts.{v, u} C
a b : Preadditive.{v, u} C
X Y : C
homGroup : ∀ (f g : X ⟶ Y), f + g = f + g
⊢ Eq (α := (X ⟶ Y) → (X ⟶ Y) → (X ⟶ Y)) HAdd.hAdd HAdd.hAdd

Tactic:
funext f g
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
inst_1 : Preadditive.{v, u} C_1
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasBinaryBiproducts.{v, u} C
a b : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
⊢ HasBinaryBiproduct.{v, u} X X

Tactic:
(inferInstance : HasBinaryBiproduct X X)

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
inst_1 : Preadditive.{v, u} C_1
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasBinaryBiproducts.{v, u} C
a b : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
h : preadditiveHasZeroMorphisms = inst_3
⊢ HasBinaryBiproduct.{v, u} X X

Tactic:
convert! (inferInstance : HasBinaryBiproduct X X)

Premises used: inferInstance