awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (hypothesis)
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
⊢ m = (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g
have h₂' : 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₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ m = (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g
have 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
Tactic: obtain ⟨q : X ⟶ T, hq : b.fst ≫ q = m - (b.fst ≫ f + b.snd ≫ g)⟩ :=
        CokernelCofork.IsColimit.desc' hb _ h₂'
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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)
⊢ m = (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g
have rw : m - (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g = 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.id_comp q, ← b.inl_fst, Category.assoc, hq, h₁',
        comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ m = (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g
have rw₁ : b.fst ≫ q = 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.id_comp q, ← b.inl_fst, Category.assoc, hq, h₁',
        comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ m = (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g
have rw₂ : b.fst ≫ 𝟙 X ≫ q = 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.id_comp q, ← b.inl_fst, Category.assoc, hq, h₁',
        comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ m = (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g
have rw₃ : b.fst ≫ (b.inl ≫ b.fst) ≫ q = 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.id_comp q, ← b.inl_fst, Category.assoc, hq, h₁',
        comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ m = (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g
have rw₄ : b.fst ≫ b.inl ≫ b.fst ≫ q = 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.id_comp q, ← b.inl_fst, Category.assoc, hq, h₁',
        comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ m = (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g
have rw₅ : b.fst ≫ b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.id_comp q, ← b.inl_fst, Category.assoc, hq, h₁',
        comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ m = (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g
have rw₆ : Eq (α := b.toCocone.pt ⟶ T) (b.fst ≫ 0) 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.id_comp q, ← b.inl_fst, Category.assoc, hq, h₁',
        comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ m = (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g
have rw₇ : Eq.{v + 1} (α := b.toCocone.pt ⟶ T) 0 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.id_comp q, ← b.inl_fst, Category.assoc, hq, h₁',
        comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (hypothesis)
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
⊢ m = (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g
have h₁' : 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₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (hypothesis)
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
⊢ m = (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g
have h₂' : 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₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ m = (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g
have 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
Tactic: obtain ⟨q : Y ⟶ T, hq : b.snd ≫ q = m - (b.fst ≫ f + b.snd ≫ g)⟩ :=
        CokernelCofork.IsColimit.desc' hb _ h₁'
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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)
⊢ m = (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g
have rw : m - (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g = 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.id_comp q, ← b.inr_snd, Category.assoc, hq, h₂',
        comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ m = (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g
have rw₁ : b.snd ≫ q = 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.id_comp q, ← b.inr_snd, Category.assoc, hq, h₂',
        comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ m = (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g
have rw₂ : b.snd ≫ 𝟙 Y ≫ q = 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.id_comp q, ← b.inr_snd, Category.assoc, hq, h₂',
        comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ m = (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g
have rw₃ : b.snd ≫ (b.inr ≫ b.snd) ≫ q = 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.id_comp q, ← b.inr_snd, Category.assoc, hq, h₂',
        comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ m = (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g
have rw₄ : b.snd ≫ b.inr ≫ b.snd ≫ q = 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.id_comp q, ← b.inr_snd, Category.assoc, hq, h₂',
        comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ m = (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g
have rw₅ : b.snd ≫ b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.id_comp q, ← b.inr_snd, Category.assoc, hq, h₂',
        comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ m = (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g
have rw₆ : Eq (α := b.toCocone.pt ⟶ T) (b.snd ≫ 0) 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.id_comp q, ← b.inr_snd, Category.assoc, hq, h₂',
        comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ m = (fun {T : C} (f : X ⟶ T) (g : Y ⟶ T) ↦ b.fst ≫ f + b.snd ≫ g) f g
have rw₇ : Eq.{v + 1} (α := b.toCocone.pt ⟶ T) 0 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.id_comp q, ← b.inr_snd, Category.assoc, hq, h₂',
        comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ 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)
have rw : Eq (α := Y ⟶ c.pt) (section_ f ≫ i.lift (Fork.ofι (Fork.ι (kernelForkOfFork (Fork.ofι (𝟙 X - f ≫ section_ f) sorry))) sorry)) 0
Tactic: rw [splitMonoOfIdempotentOfIsLimitFork_retraction, isLimitForkOfKernelFork_lift,
        isKernelCompMono_lift]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ Eq (α := Y ⟶ c.pt) (section_ f ≫ i.lift (Fork.ofι (Fork.ι (kernelForkOfFork (Fork.ofι (𝟙 X - f ≫ section_ f) ⋯))) ⋯))
    0
have dsimp : Eq (α := Y ⟶ c.pt) (section_ f ≫ i.lift (Fork.ofι (Fork.ofι (𝟙 X - f ≫ section_ f) sorry).ι sorry)) 0
Tactic: dsimp only [kernelForkOfFork_ι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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) := ⋯
⊢ Eq (α := Y ⟶ c.pt) (section_ f ≫ i.lift (Fork.ofι (Fork.ofι (𝟙 X - f ≫ section_ f) ⋯).ι ⋯)) 0
have apply : (section_ f ≫ i.lift (Fork.ofι (Fork.ofι (𝟙 X - f ≫ section_ f) sorry).ι sorry)) ≫ Fork.ι c = 0
Tactic: apply zero_of_comp_mono c.ι
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ a = b
have homGroup : Eq (α := (P Q : C) → AddCommGroup (P ⟶ Q)) homGroup homGroup
Tactic: apply Preadditive.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ Eq (α := (P Q : C) → AddCommGroup (P ⟶ Q)) homGroup homGroup
have homGroup : ∀ (X Y : C), Eq.{v + 1} (α := AddCommGroup (X ⟶ Y)) (homGroup X Y) (homGroup X Y)
Tactic: funext X Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ Eq.{v + 1} (α := AddCommGroup (X ⟶ Y)) (homGroup X Y) (homGroup X Y)
have homGroup : Eq (α := (X ⟶ Y) → (X ⟶ Y) → (X ⟶ Y)) HAdd.hAdd HAdd.hAdd
Tactic: apply AddCommGroup.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ Eq (α := (X ⟶ Y) → (X ⟶ Y) → (X ⟶ Y)) HAdd.hAdd HAdd.hAdd
have homGroup : ∀ (f g : X ⟶ Y), f + g = f + g
Tactic: funext f g
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
have h : preadditiveHasZeroMorphisms = inst_3
Tactic: convert! (inferInstance : HasBinaryBiproduct X X)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (hypothesis)
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
⊢ f + g = f + g
have h₁ : f + g = CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)
Tactic: have h₁ := @biprod.add_eq_lift_id_desc _ _ a _ _ f g
      (by convert! (inferInstance : HasBinaryBiproduct X X); subsingleton)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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₁ : f + g = CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)
⊢ HasBinaryBiproduct.{v, u} X X
have h : preadditiveHasZeroMorphisms = inst_3
Tactic: convert! (inferInstance : HasBinaryBiproduct X X)