awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_3 : Mono f
R : C
e : R ⟶ Z
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inr f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift 0 e
⊢ e = 0
have hu : Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
  (0 : R ⟶ pushout f g)
Tactic: have hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0 := by simpa [u]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_3 : Mono f
R : C
e : R ⟶ Z
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inr f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift 0 e
hu :
  Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)
⊢ e = 0
have have : ∀
  (this :
    IsLimit (F :=
      parallelPair (X := biprod.{v, u} Y Z) (Y :=
        Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
          (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
        (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
      (KernelFork.ofι (biprod.lift f (-g)) sorry)),
  e = 0
Tactic: have :=
      monoIsKernelOfCokernel _
        (BiproductToPushoutIsCokernel.isColimitBiproductToPushout f g)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_3 : Mono f
R : C
e : R ⟶ Z
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inr f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift 0 e
hu :
  Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)
this :
  IsLimit (F :=
    parallelPair (X := biprod.{v, u} Y Z) (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
        (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
      (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
    (KernelFork.ofι (biprod.lift f (-g)) ⋯)
⊢ e = 0
have obtain : ∀
  (d :
    R ⟶
      Cone.pt (F :=
        parallelPair (X := biprod.{v, u} Y Z) (Y :=
          Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
            (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
          (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
        (KernelFork.ofι (biprod.lift f (-g)) sorry))
  (hd : d ≫ Fork.ι (KernelFork.ofι (biprod.lift f (-g)) sorry) = u), e = 0
Tactic: obtain ⟨d, hd⟩ := KernelFork.IsLimit.lift' this u hu
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_3 : Mono f
R : C
e : R ⟶ Z
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inr f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift 0 e
hu :
  Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)
this :
  IsLimit (F :=
    parallelPair (X := biprod.{v, u} Y Z) (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
        (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
      (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
    (KernelFork.ofι (biprod.lift f (-g)) ⋯)
d : R ⟶ X
hd : Eq (α := R ⟶ biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) (biprod.lift 0 e)
⊢ d ≫ f = d ≫ CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) biprod.fst
have rw : d ≫ f = d ≫ f
Tactic: rw [biprod.lift_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_3 : Mono f
R : C
e : R ⟶ Z
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inr f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift 0 e
hu :
  Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)
this :
  IsLimit (F :=
    parallelPair (X := biprod.{v, u} Y Z) (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
        (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
      (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
    (KernelFork.ofι (biprod.lift f (-g)) ⋯)
d : R ⟶ X
hd : Eq (α := R ⟶ biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) (biprod.lift 0 e)
⊢ d ≫ CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) biprod.fst = u ≫ biprod.fst
have rw : CategoryStruct.comp (Y := biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) biprod.fst = u ≫ biprod.fst
Tactic: rw [← Category.assoc, hd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_3 : Mono f
R : C
e : R ⟶ Z
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inr f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift 0 e
hu :
  Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)
this :
  IsLimit (F :=
    parallelPair (X := biprod.{v, u} Y Z) (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
        (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
      (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
    (KernelFork.ofι (biprod.lift f (-g)) ⋯)
d : R ⟶ X
hd : Eq (α := R ⟶ biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) (biprod.lift 0 e)
rw : CategoryStruct.comp (Y := biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) biprod.fst = u ≫ biprod.fst
⊢ d ≫ CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) biprod.fst = u ≫ biprod.fst
have rw₁ : CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift 0 e) biprod.fst = u ≫ biprod.fst
Tactic: rw [← Category.assoc, hd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_3 : Mono f
R : C
e : R ⟶ Z
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inr f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift 0 e
hu :
  Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)
this :
  IsLimit (F :=
    parallelPair (X := biprod.{v, u} Y Z) (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
        (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
      (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
    (KernelFork.ofι (biprod.lift f (-g)) ⋯)
d : R ⟶ X
hd : Eq (α := R ⟶ biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) (biprod.lift 0 e)
⊢ e = 0
have this₁ : d ≫ f = 0
Tactic: have : d ≫ f = 0 := calc
      d ≫ f = d ≫ biprod.lift f (-g) ≫ biprod.fst := by rw [biprod.lift_fst]
      _ = u ≫ biprod.fst := by rw [← Category.assoc, hd]
      _ = 0 := biprod.lift_fst _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_3 : Mono f
R : C
e : R ⟶ Z
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inr f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift 0 e
hu :
  Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)
this_1 :
  IsLimit (F :=
    parallelPair (X := biprod.{v, u} Y Z) (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
        (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
      (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
    (KernelFork.ofι (biprod.lift f (-g)) ⋯)
d : R ⟶ X
hd : Eq (α := R ⟶ biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) (biprod.lift 0 e)
this : d ≫ f = 0
⊢ e = 0
have this₁ : d = 0
Tactic: have : d = 0 := (cancel_mono f).1 (by simpa)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_3 : Mono f
R : C
e : R ⟶ Z
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inr f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift 0 e
hu :
  Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)
this_1 :
  IsLimit (F :=
    parallelPair (X := biprod.{v, u} Y Z) (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
        (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
      (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
    (KernelFork.ofι (biprod.lift f (-g)) ⋯)
d : R ⟶ X
hd : Eq (α := R ⟶ biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) (biprod.lift 0 e)
this_2 : d ≫ f = 0
this : d = 0
⊢ e = CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift 0 e) biprod.snd
have rw : e = e
Tactic: rw [biprod.lift_snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_3 : Mono f
R : C
e : R ⟶ Z
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inr f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift 0 e
hu :
  Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)
this_1 :
  IsLimit (F :=
    parallelPair (X := biprod.{v, u} Y Z) (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
        (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
      (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
    (KernelFork.ofι (biprod.lift f (-g)) ⋯)
d : R ⟶ X
hd : Eq (α := R ⟶ biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) (biprod.lift 0 e)
this_2 : d ≫ f = 0
this : d = 0
⊢ CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift 0 e) biprod.snd =
    CategoryStruct.comp (Y := biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) biprod.snd
have rw : CategoryStruct.comp (Y := biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) biprod.snd =
  CategoryStruct.comp (Y := biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) biprod.snd
Tactic: rw [← hd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_3 : Mono f
R : C
e : R ⟶ Z
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inr f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift 0 e
hu :
  Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)
this_1 :
  IsLimit (F :=
    parallelPair (X := biprod.{v, u} Y Z) (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
        (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
      (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
    (KernelFork.ofι (biprod.lift f (-g)) ⋯)
d : R ⟶ X
hd : Eq (α := R ⟶ biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) (biprod.lift 0 e)
this_2 : d ≫ f = 0
this : d = 0
⊢ CategoryStruct.comp (Y := biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) biprod.snd =
    CategoryStruct.comp (Y := biprod.{v, u} Y Z) (0 ≫ biprod.lift f (-g)) biprod.snd
have rw : Eq (α := R ⟶ Z) (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (0 ≫ biprod.lift f (-g)) biprod.snd)
  (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (0 ≫ biprod.lift f (-g)) biprod.snd)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_3 : Mono f
R : C
e : R ⟶ Z
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inr f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift 0 e
hu :
  Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)
this_1 :
  IsLimit (F :=
    parallelPair (X := biprod.{v, u} Y Z) (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
        (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
      (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
    (KernelFork.ofι (biprod.lift f (-g)) ⋯)
d : R ⟶ X
hd : Eq (α := R ⟶ biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) (biprod.lift 0 e)
this_2 : d ≫ f = 0
this : d = 0
⊢ Eq (α := R ⟶ Z) (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (0 ≫ biprod.lift f (-g)) biprod.snd)
    (0 ≫ CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) biprod.snd)
have rw : Eq (α := R ⟶ Z) (0 ≫ CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) biprod.snd)
  (0 ≫ CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) biprod.snd)
Tactic: rw [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_3 : Mono f
R : C
e : R ⟶ Z
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inr f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift 0 e
hu :
  Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)
this_1 :
  IsLimit (F :=
    parallelPair (X := biprod.{v, u} Y Z) (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
        (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
      (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
    (KernelFork.ofι (biprod.lift f (-g)) ⋯)
d : R ⟶ X
hd : Eq (α := R ⟶ biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) (biprod.lift 0 e)
this_2 : d ≫ f = 0
this : d = 0
⊢ e = 0
have e₁ : e = CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift 0 e) biprod.snd
Tactic: calc
      e = biprod.lift (0 : R ⟶ Y) e ≫ biprod.snd := by rw [biprod.lift_snd]
      _ = (d ≫ biprod.lift f (-g)) ≫ biprod.snd := by rw [← hd]
      _ = (0 ≫ biprod.lift f (-g)) ≫ biprod.snd := by rw [this]
      _ = 0 ≫ biprod.lift f (-g) ≫ biprod.snd := by rw [Category.assoc]
      _ = 0 := zero_comp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_3 : Mono f
R : C
e : R ⟶ Z
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inr f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift 0 e
hu :
  Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)
this_1 :
  IsLimit (F :=
    parallelPair (X := biprod.{v, u} Y Z) (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
        (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
      (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
    (KernelFork.ofι (biprod.lift f (-g)) ⋯)
d : R ⟶ X
hd : Eq (α := R ⟶ biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) (biprod.lift 0 e)
this_2 : d ≫ f = 0
this : d = 0
e₁ : e = CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift 0 e) biprod.snd
⊢ e = 0
have e₂ : CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift 0 e) biprod.snd =
  CategoryStruct.comp (Y := biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) biprod.snd
Tactic: calc
      e = biprod.lift (0 : R ⟶ Y) e ≫ biprod.snd := by rw [biprod.lift_snd]
      _ = (d ≫ biprod.lift f (-g)) ≫ biprod.snd := by rw [← hd]
      _ = (0 ≫ biprod.lift f (-g)) ≫ biprod.snd := by rw [this]
      _ = 0 ≫ biprod.lift f (-g) ≫ biprod.snd := by rw [Category.assoc]
      _ = 0 := zero_comp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_3 : Mono f
R : C
e : R ⟶ Z
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inr f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift 0 e
hu :
  Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)
this_1 :
  IsLimit (F :=
    parallelPair (X := biprod.{v, u} Y Z) (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
        (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
      (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
    (KernelFork.ofι (biprod.lift f (-g)) ⋯)
d : R ⟶ X
hd : Eq (α := R ⟶ biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) (biprod.lift 0 e)
this_2 : d ≫ f = 0
this : d = 0
e₁ : e = CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift 0 e) biprod.snd
e₂ :
  CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift 0 e) biprod.snd =
    CategoryStruct.comp (Y := biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) biprod.snd
⊢ e = 0
have e₃ : CategoryStruct.comp (Y := biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) biprod.snd =
  CategoryStruct.comp (Y := biprod.{v, u} Y Z) (0 ≫ biprod.lift f (-g)) biprod.snd
Tactic: calc
      e = biprod.lift (0 : R ⟶ Y) e ≫ biprod.snd := by rw [biprod.lift_snd]
      _ = (d ≫ biprod.lift f (-g)) ≫ biprod.snd := by rw [← hd]
      _ = (0 ≫ biprod.lift f (-g)) ≫ biprod.snd := by rw [this]
      _ = 0 ≫ biprod.lift f (-g) ≫ biprod.snd := by rw [Category.assoc]
      _ = 0 := zero_comp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_3 : Mono f
R : C
e : R ⟶ Z
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inr f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift 0 e
hu :
  Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)
this_1 :
  IsLimit (F :=
    parallelPair (X := biprod.{v, u} Y Z) (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
        (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
      (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
    (KernelFork.ofι (biprod.lift f (-g)) ⋯)
d : R ⟶ X
hd : Eq (α := R ⟶ biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) (biprod.lift 0 e)
this_2 : d ≫ f = 0
this : d = 0
e₁ : e = CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift 0 e) biprod.snd
e₂ :
  CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift 0 e) biprod.snd =
    CategoryStruct.comp (Y := biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) biprod.snd
e₃ :
  CategoryStruct.comp (Y := biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) biprod.snd =
    CategoryStruct.comp (Y := biprod.{v, u} Y Z) (0 ≫ biprod.lift f (-g)) biprod.snd
⊢ e = 0
have e₄ : Eq (α := R ⟶ Z) (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (0 ≫ biprod.lift f (-g)) biprod.snd)
  (0 ≫ CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) biprod.snd)
Tactic: calc
      e = biprod.lift (0 : R ⟶ Y) e ≫ biprod.snd := by rw [biprod.lift_snd]
      _ = (d ≫ biprod.lift f (-g)) ≫ biprod.snd := by rw [← hd]
      _ = (0 ≫ biprod.lift f (-g)) ≫ biprod.snd := by rw [this]
      _ = 0 ≫ biprod.lift f (-g) ≫ biprod.snd := by rw [Category.assoc]
      _ = 0 := zero_comp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_3 : Mono g
R : C
e : R ⟶ Y
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inl f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift e 0
⊢ e = 0
have hu : Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
  (0 : R ⟶ pushout f g)
Tactic: have hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0 := by simpa [u]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_3 : Mono g
R : C
e : R ⟶ Y
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inl f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift e 0
hu :
  Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)
⊢ e = 0
have have : ∀
  (this :
    IsLimit (F :=
      parallelPair (X := biprod.{v, u} Y Z) (Y :=
        Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
          (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
        (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
      (KernelFork.ofι (biprod.lift f (-g)) sorry)),
  e = 0
Tactic: have :=
      monoIsKernelOfCokernel _
        (BiproductToPushoutIsCokernel.isColimitBiproductToPushout f g)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_3 : Mono g
R : C
e : R ⟶ Y
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inl f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift e 0
hu :
  Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)
this :
  IsLimit (F :=
    parallelPair (X := biprod.{v, u} Y Z) (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
        (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
      (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
    (KernelFork.ofι (biprod.lift f (-g)) ⋯)
⊢ e = 0
have obtain : ∀
  (d :
    R ⟶
      Cone.pt (F :=
        parallelPair (X := biprod.{v, u} Y Z) (Y :=
          Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
            (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
          (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
        (KernelFork.ofι (biprod.lift f (-g)) sorry))
  (hd : d ≫ Fork.ι (KernelFork.ofι (biprod.lift f (-g)) sorry) = u), e = 0
Tactic: obtain ⟨d, hd⟩ := KernelFork.IsLimit.lift' this u hu
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_3 : Mono g
R : C
e : R ⟶ Y
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inl f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift e 0
hu :
  Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)
this :
  IsLimit (F :=
    parallelPair (X := biprod.{v, u} Y Z) (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
        (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
      (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
    (KernelFork.ofι (biprod.lift f (-g)) ⋯)
d : R ⟶ X
hd : Eq (α := R ⟶ biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) (biprod.lift e 0)
⊢ d ≫ (-g) = d ≫ CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) biprod.snd
have rw : d ≫ (-g) = d ≫ (-g)
Tactic: rw [biprod.lift_snd]