awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
this : Epi (Cofork.π c) := ⋯
⊢ Eq (α := Y ⟶ X)
    (Cofork.π c ≫ i.desc (Cofork.ofπ (Cofork.π (CokernelCofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯)) ⋯) ≫ retraction f) 0
have simp : 𝟙 Y ≫ retraction f - retraction f = 0
Tactic: simp only [sub_comp, comp_sub, Category.comp_id, Category.assoc, IsSplitMono.id, sub_self,
      Cofork.IsColimit.π_desc_assoc, CokernelCofork.π_ofπ, IsSplitMono.id_assoc]
-- 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 : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
this : Epi (Cofork.π c) := ⋯
⊢ 𝟙 Y ≫ retraction f - retraction f = 0
have a : 𝟙 Y ≫ retraction f = retraction f
Tactic: apply sub_eq_zero_of_eq
-- 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 : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ (binaryBiconeOfIsSplitMonoOfCokernel i).fst ≫ (binaryBiconeOfIsSplitMonoOfCokernel i).inl +
      (binaryBiconeOfIsSplitMonoOfCokernel i).snd ≫ (binaryBiconeOfIsSplitMonoOfCokernel i).inr =
    𝟙 (binaryBiconeOfIsSplitMonoOfCokernel i).pt
have simp : HAdd.hAdd (β := (binaryBiconeOfIsSplitMonoOfCokernel i).pt ⟶ (binaryBiconeOfIsSplitMonoOfCokernel i).pt)
    (retraction f ≫ (binaryBiconeOfIsSplitMonoOfCokernel i).inl)
    (Cofork.π c ≫
        IsColimit.desc (isColimitCoforkOfCokernelCofork (isCokernelEpiComp i (retraction f) sorry))
          (Cofork.ofπ (𝟙 Y - retraction f ≫ f) sorry) :
      (binaryBiconeOfIsSplitMonoOfCokernel i).pt ⟶ (binaryBiconeOfIsSplitMonoOfCokernel i).pt) =
  𝟙 (binaryBiconeOfIsSplitMonoOfCokernel i).pt
Tactic: simp only [binaryBiconeOfIsSplitMonoOfCokernel_fst,
        binaryBiconeOfIsSplitMonoOfCokernel_inr,
        binaryBiconeOfIsSplitMonoOfCokernel_snd,
        splitEpiOfIdempotentOfIsColimitCofork_section_]
-- 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 : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ HAdd.hAdd (β := (binaryBiconeOfIsSplitMonoOfCokernel i).pt ⟶ (binaryBiconeOfIsSplitMonoOfCokernel i).pt)
      (retraction f ≫ (binaryBiconeOfIsSplitMonoOfCokernel i).inl)
      (Cofork.π c ≫
          IsColimit.desc (isColimitCoforkOfCokernelCofork (isCokernelEpiComp i (retraction f) ⋯))
            (Cofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯) :
        (binaryBiconeOfIsSplitMonoOfCokernel i).pt ⟶ (binaryBiconeOfIsSplitMonoOfCokernel i).pt) =
    𝟙 (binaryBiconeOfIsSplitMonoOfCokernel i).pt
have dsimp : HAdd.hAdd (β := Y ⟶ Y) (retraction f ≫ (binaryBiconeOfIsSplitMonoOfCokernel i).inl)
    (Cofork.π c ≫
        IsColimit.desc (isColimitCoforkOfCokernelCofork (isCokernelEpiComp i (retraction f) sorry))
          (Cofork.ofπ (𝟙 Y - retraction f ≫ f) sorry) :
      Y ⟶ Y) =
  𝟙 Y
Tactic: dsimp only [binaryBiconeOfIsSplitMonoOfCokernel_pt]
-- 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 : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ HAdd.hAdd (β := Y ⟶ Y) (retraction f ≫ (binaryBiconeOfIsSplitMonoOfCokernel i).inl)
      (Cofork.π c ≫
          IsColimit.desc (isColimitCoforkOfCokernelCofork (isCokernelEpiComp i (retraction f) ⋯))
            (Cofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯) :
        Y ⟶ Y) =
    𝟙 Y
have rw : HAdd.hAdd (β := Y ⟶ Y) (retraction f ≫ (binaryBiconeOfIsSplitMonoOfCokernel i).inl)
    (Cofork.π c ≫ i.desc (Cofork.ofπ (Cofork.π (cokernelCoforkOfCofork (Cofork.ofπ (𝟙 Y - retraction f ≫ f) sorry))) sorry) :
      Y ⟶ Y) =
  𝟙 Y
Tactic: rw [isColimitCoforkOfCokernelCofork_desc, isCokernelEpiComp_desc]
-- 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 : IsLimit b.sndKernelFork
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 = (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g
have h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
Tactic: have h₁' : ((m : T ⟶ b.pt) - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 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 : IsLimit b.sndKernelFork
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 = (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g
have h₂' : (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₂
-- 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 : IsLimit b.sndKernelFork
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
⊢ m = (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g
have obtain : ∀ (q : T ⟶ X) (hq : q ≫ b.inl = 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
Tactic: obtain ⟨q : T ⟶ X, hq : q ≫ b.inl = m - (f ≫ b.inl + g ≫ b.inr)⟩ :=
        KernelFork.IsLimit.lift' 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 : IsLimit b.sndKernelFork
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 ⟶ X
hq : q ≫ b.inl = 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
have rw : m - (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g = 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.comp_id q, ← b.inl_fst, ← Category.assoc, hq, h₁',
        zero_comp]
-- 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 : IsLimit b.sndKernelFork
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 ⟶ X
hq : q ≫ b.inl = 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
⊢ m = (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g
have rw₁ : q ≫ b.inl = 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.comp_id q, ← b.inl_fst, ← Category.assoc, hq, h₁',
        zero_comp]
-- 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 : IsLimit b.sndKernelFork
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 ⟶ X
hq : q ≫ b.inl = 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.inl = 0
⊢ m = (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g
have rw₂ : (q ≫ 𝟙 X) ≫ b.inl = 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.comp_id q, ← b.inl_fst, ← Category.assoc, hq, h₁',
        zero_comp]
-- 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 : IsLimit b.sndKernelFork
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 ⟶ X
hq : q ≫ b.inl = 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.inl = 0
rw₂ : (q ≫ 𝟙 X) ≫ b.inl = 0
⊢ m = (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g
have rw₃ : (q ≫ b.inl ≫ b.fst) ≫ b.inl = 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.comp_id q, ← b.inl_fst, ← Category.assoc, hq, h₁',
        zero_comp]
-- 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 : IsLimit b.sndKernelFork
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 ⟶ X
hq : q ≫ b.inl = 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.inl = 0
rw₂ : (q ≫ 𝟙 X) ≫ b.inl = 0
rw₃ : (q ≫ b.inl ≫ b.fst) ≫ b.inl = 0
⊢ m = (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g
have rw₄ : ((q ≫ b.inl) ≫ b.fst) ≫ b.inl = 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.comp_id q, ← b.inl_fst, ← Category.assoc, hq, h₁',
        zero_comp]
-- 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 : IsLimit b.sndKernelFork
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 ⟶ X
hq : q ≫ b.inl = 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.inl = 0
rw₂ : (q ≫ 𝟙 X) ≫ b.inl = 0
rw₃ : (q ≫ b.inl ≫ b.fst) ≫ b.inl = 0
rw₄ : ((q ≫ b.inl) ≫ b.fst) ≫ b.inl = 0
⊢ m = (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g
have rw₅ : ((m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst) ≫ b.inl = 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.comp_id q, ← b.inl_fst, ← Category.assoc, hq, h₁',
        zero_comp]
-- 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 : IsLimit b.sndKernelFork
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 ⟶ X
hq : q ≫ b.inl = 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.inl = 0
rw₂ : (q ≫ 𝟙 X) ≫ b.inl = 0
rw₃ : (q ≫ b.inl ≫ b.fst) ≫ b.inl = 0
rw₄ : ((q ≫ b.inl) ≫ b.fst) ≫ b.inl = 0
rw₅ : ((m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst) ≫ b.inl = 0
⊢ m = (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g
have rw₆ : Eq (α := T ⟶ b.toCone.pt) (0 ≫ b.inl) 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.comp_id q, ← b.inl_fst, ← Category.assoc, hq, h₁',
        zero_comp]
-- 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 : IsLimit b.sndKernelFork
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 ⟶ X
hq : q ≫ b.inl = 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.inl = 0
rw₂ : (q ≫ 𝟙 X) ≫ b.inl = 0
rw₃ : (q ≫ b.inl ≫ b.fst) ≫ b.inl = 0
rw₄ : ((q ≫ b.inl) ≫ b.fst) ≫ b.inl = 0
rw₅ : ((m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst) ≫ b.inl = 0
rw₆ : Eq (α := T ⟶ b.toCone.pt) (0 ≫ b.inl) 0
⊢ m = (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g
have rw₇ : Eq.{v + 1} (α := T ⟶ b.toCone.pt) 0 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.comp_id q, ← b.inl_fst, ← Category.assoc, hq, h₁',
        zero_comp]
-- 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 : 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 = (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g
have h₁' : (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₁
-- 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 : 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 = (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g
have h₂' : (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₂
-- 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 : 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
⊢ m = (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g
have 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
Tactic: obtain ⟨q : T ⟶ Y, hq : q ≫ b.inr = m - (f ≫ b.inl + g ≫ b.inr)⟩ :=
        KernelFork.IsLimit.lift' 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 : 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)
⊢ m = (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g
have rw : m - (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g = 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.comp_id q, ← b.inr_snd, ← Category.assoc, hq, h₂',
        zero_comp]
-- 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 : 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
⊢ m = (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g
have rw₁ : q ≫ b.inr = 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.comp_id q, ← b.inr_snd, ← Category.assoc, hq, h₂',
        zero_comp]
-- 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 : 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
⊢ m = (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g
have rw₂ : (q ≫ 𝟙 Y) ≫ b.inr = 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.comp_id q, ← b.inr_snd, ← Category.assoc, hq, h₂',
        zero_comp]
-- 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 : 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
⊢ m = (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g
have rw₃ : (q ≫ b.inr ≫ b.snd) ≫ b.inr = 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.comp_id q, ← b.inr_snd, ← Category.assoc, hq, h₂',
        zero_comp]
-- 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 : 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
⊢ m = (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g
have rw₄ : ((q ≫ b.inr) ≫ b.snd) ≫ b.inr = 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.comp_id q, ← b.inr_snd, ← Category.assoc, hq, h₂',
        zero_comp]
-- 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 : 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
⊢ m = (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g
have rw₅ : ((m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd) ≫ b.inr = 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.comp_id q, ← b.inr_snd, ← Category.assoc, hq, h₂',
        zero_comp]
-- 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 : 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
⊢ m = (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g
have rw₆ : Eq (α := T ⟶ b.toCone.pt) (0 ≫ b.inr) 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.comp_id q, ← b.inr_snd, ← Category.assoc, hq, h₂',
        zero_comp]
-- 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 : 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
⊢ m = (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g
have rw₇ : Eq.{v + 1} (α := T ⟶ b.toCone.pt) 0 0
Tactic: rw [← sub_eq_zero, ← hq, ← Category.comp_id q, ← b.inr_snd, ← Category.assoc, hq, h₂',
        zero_comp]
-- 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
⊢ 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₁