awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ≫ CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) biprod.snd =
    CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift e 0) 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) (biprod.lift e 0) biprod.snd
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 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)
rw :
  CategoryStruct.comp (Y := biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) biprod.snd =
    CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift e 0) biprod.snd
⊢ d ≫ CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) biprod.snd =
    CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift e 0) biprod.snd
have rw₁ : Eq (α := R ⟶ Z) (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift e 0) biprod.snd)
  (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift e 0) biprod.snd)
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 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)
⊢ e = 0
have this₁ : d ≫ (-g) = 0
Tactic: have : d ≫ (-g) = 0 := calc
      d ≫ (-g) = d ≫ biprod.lift f (-g) ≫ biprod.snd := by rw [biprod.lift_snd]
      _ = biprod.lift e (0 : R ⟶ Z) ≫ biprod.snd := by rw [← Category.assoc, hd]
      _ = 0 := biprod.lift_snd _ _
-- 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
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 e 0)
this : d ≫ (-g) = 0
⊢ e = 0
have this₁ : d = 0
Tactic: have : d = 0 := (cancel_mono (-g)).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 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_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 e 0)
this_2 : d ≫ (-g) = 0
this : d = 0
⊢ e = CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift e 0) biprod.fst
have rw : e = e
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 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_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 e 0)
this_2 : d ≫ (-g) = 0
this : d = 0
⊢ CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift e 0) biprod.fst =
    CategoryStruct.comp (Y := biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) biprod.fst
have rw : CategoryStruct.comp (Y := biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) biprod.fst =
  CategoryStruct.comp (Y := biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) biprod.fst
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 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_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 e 0)
this_2 : d ≫ (-g) = 0
this : d = 0
⊢ CategoryStruct.comp (Y := biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) biprod.fst =
    CategoryStruct.comp (Y := biprod.{v, u} Y Z) (0 ≫ biprod.lift f (-g)) biprod.fst
have rw : Eq (α := R ⟶ Y) (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (0 ≫ biprod.lift f (-g)) biprod.fst)
  (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (0 ≫ biprod.lift f (-g)) biprod.fst)
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 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_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 e 0)
this_2 : d ≫ (-g) = 0
this : d = 0
⊢ Eq (α := R ⟶ Y) (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (0 ≫ biprod.lift f (-g)) biprod.fst)
    (0 ≫ CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) biprod.fst)
have rw : Eq (α := R ⟶ Y) (0 ≫ CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) biprod.fst)
  (0 ≫ CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) biprod.fst)
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 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_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 e 0)
this_2 : d ≫ (-g) = 0
this : d = 0
⊢ e = 0
have e₁ : e = CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift e 0) biprod.fst
Tactic: calc
      e = biprod.lift e (0 : R ⟶ Z) ≫ biprod.fst := by rw [biprod.lift_fst]
      _ = (d ≫ biprod.lift f (-g)) ≫ biprod.fst := by rw [← hd]
      _ = (0 ≫ biprod.lift f (-g)) ≫ biprod.fst := by rw [this]
      _ = 0 ≫ biprod.lift f (-g) ≫ biprod.fst := 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 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_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 e 0)
this_2 : d ≫ (-g) = 0
this : d = 0
e₁ : e = CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift e 0) biprod.fst
⊢ e = 0
have e₂ : CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift e 0) biprod.fst =
  CategoryStruct.comp (Y := biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) biprod.fst
Tactic: calc
      e = biprod.lift e (0 : R ⟶ Z) ≫ biprod.fst := by rw [biprod.lift_fst]
      _ = (d ≫ biprod.lift f (-g)) ≫ biprod.fst := by rw [← hd]
      _ = (0 ≫ biprod.lift f (-g)) ≫ biprod.fst := by rw [this]
      _ = 0 ≫ biprod.lift f (-g) ≫ biprod.fst := 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 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_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 e 0)
this_2 : d ≫ (-g) = 0
this : d = 0
e₁ : e = CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift e 0) biprod.fst
e₂ :
  CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift e 0) biprod.fst =
    CategoryStruct.comp (Y := biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) biprod.fst
⊢ e = 0
have e₃ : CategoryStruct.comp (Y := biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) biprod.fst =
  CategoryStruct.comp (Y := biprod.{v, u} Y Z) (0 ≫ biprod.lift f (-g)) biprod.fst
Tactic: calc
      e = biprod.lift e (0 : R ⟶ Z) ≫ biprod.fst := by rw [biprod.lift_fst]
      _ = (d ≫ biprod.lift f (-g)) ≫ biprod.fst := by rw [← hd]
      _ = (0 ≫ biprod.lift f (-g)) ≫ biprod.fst := by rw [this]
      _ = 0 ≫ biprod.lift f (-g) ≫ biprod.fst := 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 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_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 e 0)
this_2 : d ≫ (-g) = 0
this : d = 0
e₁ : e = CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift e 0) biprod.fst
e₂ :
  CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift e 0) biprod.fst =
    CategoryStruct.comp (Y := biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) biprod.fst
e₃ :
  CategoryStruct.comp (Y := biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) biprod.fst =
    CategoryStruct.comp (Y := biprod.{v, u} Y Z) (0 ≫ biprod.lift f (-g)) biprod.fst
⊢ e = 0
have e₄ : Eq (α := R ⟶ Y) (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (0 ≫ biprod.lift f (-g)) biprod.fst)
  (0 ≫ CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) biprod.fst)
Tactic: calc
      e = biprod.lift e (0 : R ⟶ Z) ≫ biprod.fst := by rw [biprod.lift_fst]
      _ = (d ≫ biprod.lift f (-g)) ≫ biprod.fst := by rw [← hd]
      _ = (0 ≫ biprod.lift f (-g)) ≫ biprod.fst := by rw [this]
      _ = 0 ≫ biprod.lift f (-g) ≫ biprod.fst := 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
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_3 : Mono f
s : PushoutCocone f g
hs : IsColimit s
⊢ Mono s.inr
have this : Mono ((colimit.cocone (span f g)).ι.app WalkingCospan.right)
Tactic: haveI : Mono (NatTrans.app (colimit.cocone (span f g)).ι WalkingCospan.right) :=
    Abelian.mono_pushout_of_mono_f f g
-- 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
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_3 : Mono g
s : PushoutCocone f g
hs : IsColimit s
⊢ Mono s.inl
have this : Mono ((colimit.cocone (span f g)).ι.app WalkingCospan.left)
Tactic: haveI : Mono (NatTrans.app (colimit.cocone (span f g)).ι WalkingCospan.left) :=
    Abelian.mono_pushout_of_mono_g f g
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
inst_2 : HasFiniteProducts.{u_2, u_1} C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), Nonempty (AbelianStruct f)
X Y : C
f : X ⟶ Y
h_1 : Mono f
⊢ Nonempty (NormalMono f)
have obtain : ∀ (hf : AbelianStruct f), Nonempty (NormalMono f)
Tactic: obtain ⟨hf⟩ := h f
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Preadditive.{u_2, u_1} C
inst_2 : HasFiniteProducts.{u_2, u_1} C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), Nonempty (AbelianStruct f)
X Y : C
f : X ⟶ Y
h_1 : Epi f
⊢ Nonempty (NormalEpi f)
have obtain : ∀ (hf : AbelianStruct f), Nonempty (NormalEpi f)
Tactic: obtain ⟨hf⟩ := h f
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h : IsPushout t l r b
T : C
x₄ : T ⟶ X₄
⊢ ∃ (T' : C) (π : T' ⟶ T) (_ : Epi π) (x₂ : T' ⟶ X₂) (x₃ : T' ⟶ X₃), π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
have this : Epi (X := ShortComplex.X₂ sorry.shortComplex) (ShortComplex.g sorry.shortComplex)
Tactic: have := h.epi_shortComplex_g
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h : IsPushout t l r b
T : C
x₄ : T ⟶ X₄
this : Epi (X := ShortComplex.X₂ ⋯.shortComplex) (ShortComplex.g ⋯.shortComplex)
⊢ ∃ (T' : C) (π : T' ⟶ T) (_ : Epi π) (x₂ : T' ⟶ X₂) (x₃ : T' ⟶ X₃), π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
have obtain : ∀ (T' : C) (π : T' ⟶ T),
  Epi π →
    ∀ (u : T' ⟶ ShortComplex.X₂ sorry.shortComplex) (hu : π ≫ x₄ = u ≫ ShortComplex.g sorry.shortComplex),
      ∃ (T' : C) (π : T' ⟶ T) (_ : Epi π) (x₂ : T' ⟶ X₂) (x₃ : T' ⟶ X₃), π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
Tactic: obtain ⟨T', π, _, u, hu⟩ := surjective_up_to_refinements_of_epi h.shortComplex.g x₄
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h : IsPushout t l r b
T : C
x₄ : T ⟶ X₄
this : Epi (X := ShortComplex.X₂ ⋯.shortComplex) (ShortComplex.g ⋯.shortComplex)
T' : C
π : T' ⟶ T
w : Epi π
u : T' ⟶ ShortComplex.X₂ ⋯.shortComplex
hu : π ≫ x₄ = u ≫ ShortComplex.g ⋯.shortComplex
⊢ ∃ (T' : C) (π : T' ⟶ T) (_ : Epi π) (x₂ : T' ⟶ X₂) (x₃ : T' ⟶ X₃), π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
have refine : π ≫ x₄ = (u ≫ biprod.fst) ≫ r + (u ≫ biprod.snd) ≫ b
Tactic: refine ⟨T', π, inferInstance, u ≫ biprod.fst, u ≫ biprod.snd, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h : IsPushout t l r b
T : C
x₄ : T ⟶ X₄
this : Epi (X := ShortComplex.X₂ ⋯.shortComplex) (ShortComplex.g ⋯.shortComplex)
T' : C
π : T' ⟶ T
w : Epi π
u : T' ⟶ ShortComplex.X₂ ⋯.shortComplex
hu : π ≫ x₄ = u ≫ ShortComplex.g ⋯.shortComplex
⊢ π ≫ x₄ = (u ≫ biprod.fst) ≫ r + (u ≫ biprod.snd) ≫ b
have simp : u ≫ ShortComplex.g sorry.shortComplex =
  u ≫ HAdd.hAdd (α := ShortComplex.X₂ sorry.shortComplex ⟶ X₄) (biprod.fst ≫ r) (biprod.snd ≫ b)
Tactic: simp only [hu, assoc, ← Preadditive.comp_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h : IsPushout t l r b
T : C
x₄ : T ⟶ X₄
this : Epi (X := ShortComplex.X₂ ⋯.shortComplex) (ShortComplex.g ⋯.shortComplex)
T' : C
π : T' ⟶ T
w : Epi π
u : T' ⟶ ShortComplex.X₂ ⋯.shortComplex
hu : π ≫ x₄ = u ≫ ShortComplex.g ⋯.shortComplex
⊢ u ≫ ShortComplex.g ⋯.shortComplex =
    u ≫ HAdd.hAdd (α := ShortComplex.X₂ ⋯.shortComplex ⟶ X₄) (biprod.fst ≫ r) (biprod.snd ≫ b)
have e_a : ShortComplex.g sorry.shortComplex = HAdd.hAdd (α := ShortComplex.X₂ sorry.shortComplex ⟶ X₄) (biprod.fst ≫ r) (biprod.snd ≫ b)
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
⊢ x₄ = 0
have obtain : ∀ (T₁ : C) (π : T₁ ⟶ T₀), Epi π → ∀ (x₂ : T₁ ⟶ X₂) (x₃ : T₁ ⟶ X₃) (eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b), x₄ = 0
Tactic: obtain ⟨T₁, π, _, x₂, x₃, eq⟩ := hom_eq_add_up_to_refinements h₁ x₄
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
⊢ (-x₂) ≫ r' = x₃ ≫ b'
have rw : -x₂ ≫ r' = x₃ ≫ b'
Tactic: rw [Preadditive.neg_comp, neg_eq_iff_add_eq_zero, ← fac₂, ← fac₁,
        ← assoc, ← assoc, ← Preadditive.add_comp, ← eq, assoc, hx₄, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
rw : -x₂ ≫ r' = x₃ ≫ b'
⊢ (-x₂) ≫ r' = x₃ ≫ b'
have rw₁ : x₂ ≫ r' + x₃ ≫ b' = 0
Tactic: rw [Preadditive.neg_comp, neg_eq_iff_add_eq_zero, ← fac₂, ← fac₁,
        ← assoc, ← assoc, ← Preadditive.add_comp, ← eq, assoc, hx₄, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.CommSq (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst_2 : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
rw : -x₂ ≫ r' = x₃ ≫ b'
rw₁ : x₂ ≫ r' + x₃ ≫ b' = 0
⊢ (-x₂) ≫ r' = x₃ ≫ b'
have rw₂ : x₂ ≫ r' + x₃ ≫ b ≫ k = 0
Tactic: rw [Preadditive.neg_comp, neg_eq_iff_add_eq_zero, ← fac₂, ← fac₁,
        ← assoc, ← assoc, ← Preadditive.add_comp, ← eq, assoc, hx₄, comp_zero]