awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
rw 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)
⊢ 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:
rw [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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) (0 ≫ CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) biprod.snd) 0

Tactic:
zero_comp

Premises used: CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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₄ :
  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)
⊢ e = 0

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

Premises used: CategoryTheory.Limits.biprod.snd, CategoryTheory.Limits.biprod.lift, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.zero_comp, OfNat.ofNat, Neg.neg
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
⊢ Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)

Tactic:
simpa [u]
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
⊢ 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]
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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)
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)) ⋯)),
    e = 0
⊢ e = 0

Tactic:
have :=
      monoIsKernelOfCokernel _
        (BiproductToPushoutIsCokernel.isColimitBiproductToPushout f g)
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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)) ⋯)
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)) ⋯))
    (hd : d ≫ Fork.ι (KernelFork.ofι (biprod.lift f (-g)) ⋯) = u), e = 0
⊢ e = 0

Tactic:
obtain ⟨d, hd⟩ := KernelFork.IsLimit.lift' this u hu

Premises used: CategoryTheory.Limits.KernelFork.IsLimit.lift'
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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 rw₁ : d ≫ (-g) = d ≫ (-g)
⊢ d ≫ (-g) = d ≫ CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) biprod.snd

Tactic:
rw [biprod.lift_snd]

Premises used: CategoryTheory.Limits.biprod.lift_snd
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
rw₁ 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)
⊢ 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

Tactic:
rw [← Category.assoc, hd]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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) = 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 _ _
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
⊢ d ≫ (-g) = 0 ≫ (-g)

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
⊢ d = 0

Tactic:
have : d = 0 := (cancel_mono (-g)).1 (by simpa)
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
rw rw₁ : e = e
⊢ e = CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift e 0) biprod.fst

Tactic:
rw [biprod.lift_fst]

Premises used: CategoryTheory.Limits.biprod.lift_fst
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
rw 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
⊢ 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:
rw [← hd]
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
rw 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)
⊢ 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:
rw [this]
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
rw 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)
⊢ 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:
rw [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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) (0 ≫ CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) biprod.fst) 0

Tactic:
zero_comp

Premises used: CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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₄ :
  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)
⊢ e = 0

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

Premises used: CategoryTheory.Limits.biprod.lift, CategoryTheory.Limits.biprod.fst, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.zero_comp, OfNat.ofNat, Neg.neg
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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 ((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
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
this : Mono ((colimit.cocone (span f g)).ι.app WalkingCospan.right)
⊢ Mono s.inr

Tactic:
apply
    mono_of_mono_fac (IsColimit.comp_coconePointUniqueUpToIso_hom hs (colimit.isColimit _) _)

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.mono_of_mono_fac
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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 ((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
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
this : Mono ((colimit.cocone (span f g)).ι.app WalkingCospan.left)
⊢ Mono s.inl

Tactic:
apply
    mono_of_mono_fac (IsColimit.comp_coconePointUniqueUpToIso_hom hs (colimit.isColimit _) _)

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.mono_of_mono_fac
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
g₁ : X ⟶ W
inst_3 : Epi g₁
g₂ : W ⟶ Z
inst_4 : Mono g₂
hg : g₁ ≫ g₂ = g
f' : W ⟶ Y
hf : g₁ ≫ f' = f
t : PushoutCocone f g
ht : IsColimit t
⊢ Mono t.inl

Tactic:
apply mono_inl_of_isColimit _ _ (PushoutCocone.isColimitOfFactors _ _ _ _ _ hf hg t ht)

Premises used: CategoryTheory.Limits.PushoutCocone.isColimitOfFactors, CategoryTheory.Abelian.mono_inl_of_isColimit