[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X : C
⊢ AddCommGroup (End X)
[PROOFSTEP]
dsimp [End]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X : C
⊢ AddCommGroup (X ⟶ X)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
f : P ⟶ Q
g g' : Q ⟶ R
⊢ (fun g => f ≫ g) (g + g') = (fun g => f ≫ g) g + (fun g => f ≫ g) g'
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
g : Q ⟶ R
f f' : P ⟶ Q
⊢ (fun f => f ≫ g) (f + f') = (fun f => f ≫ g) f + (fun f => f ≫ g) f'
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
f f' : P ⟶ Q
g g' : Q ⟶ R
⊢ (-f) ≫ (-g) = f ≫ g
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P✝ Q✝ R : C
f✝ f' : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R
P Q : C
f : P ⟶ Q
inst✝ : Epi f
Z✝ : C
g g' : Q ⟶ Z✝
H : (-f) ≫ g = (-f) ≫ g'
⊢ g = g'
[PROOFSTEP]
rwa [neg_comp, neg_comp, ← comp_neg, ← comp_neg, cancel_epi, neg_inj] at H 
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P✝ Q✝ R : C
f✝ f' : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R
P Q : C
f : P ⟶ Q
inst✝ : Mono f
Z✝ : C
g g' : Z✝ ⟶ P
H : g ≫ (-f) = g' ≫ (-f)
⊢ g = g'
[PROOFSTEP]
rwa [comp_neg, comp_neg, ← neg_comp, ← neg_comp, cancel_mono, neg_inj] at H 
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
f✝ f' : P ⟶ Q
g g' : Q ⟶ R
X : C
src✝ : Monoid (End X) := End.monoid
f : End X
⊢ 0 * f = 0
[PROOFSTEP]
dsimp [mul]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
f✝ f' : P ⟶ Q
g g' : Q ⟶ R
X : C
src✝ : Monoid (End X) := End.monoid
f : End X
⊢ f ≫ 0 = 0
[PROOFSTEP]
exact HasZeroMorphisms.comp_zero f _
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
f✝ f' : P ⟶ Q
g g' : Q ⟶ R
X : C
src✝ : Monoid (End X) := End.monoid
f : End X
⊢ f * 0 = 0
[PROOFSTEP]
dsimp [mul]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
f✝ f' : P ⟶ Q
g g' : Q ⟶ R
X : C
src✝ : Monoid (End X) := End.monoid
f : End X
⊢ 0 ≫ f = 0
[PROOFSTEP]
exact HasZeroMorphisms.zero_comp _ f
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P Q R : C
f✝ f' : P ⟶ Q
g✝ g' : Q ⟶ R
X Y : C
f : X ⟶ Y
inst✝ : HasLimit (parallelPair f 0)
w : kernel.ι f = 0
P✝ : C
g : P✝ ⟶ X
h : g ≫ f = 0
⊢ g = 0
[PROOFSTEP]
rw [← kernel.lift_ι f g h, w, Limits.comp_zero]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P Q R : C
f✝ f' : P ⟶ Q
g✝ g' : Q ⟶ R
X Y : C
f : X ⟶ Y
inst✝ : HasColimit (parallelPair f 0)
w : cokernel.π f = 0
R✝ : C
g : Y ⟶ R✝
h : f ≫ g = 0
⊢ g = 0
[PROOFSTEP]
rw [← cokernel.π_desc f g h, w, Limits.zero_comp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P Q R : C
f f' : P ⟶ Q
g g' : Q ⟶ R
inst✝ : IsIso f
⊢ f ≫ g = 0 ↔ g = 0
[PROOFSTEP]
rw [← IsIso.eq_inv_comp, Limits.comp_zero]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P Q R : C
f f' : P ⟶ Q
g g' : Q ⟶ R
inst✝ : IsIso g
⊢ f ≫ g = 0 ↔ f = 0
[PROOFSTEP]
rw [← IsIso.eq_comp_inv, Limits.zero_comp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : KernelFork (f - g)
⊢ Fork.ι c ≫ f = Fork.ι c ≫ g
[PROOFSTEP]
rw [← sub_eq_zero, ← comp_sub, c.condition]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : Fork f g
⊢ Fork.ι c ≫ (f - g) = Fork.ι c ≫ 0
[PROOFSTEP]
rw [comp_sub, comp_zero, sub_eq_zero, c.condition]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f = ι ≫ g
⊢ ι ≫ (f - g) = 0
[PROOFSTEP]
simp [w]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : KernelFork (f - g)
i : IsLimit c
s : Fork f g
m✝ :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (forkOfKernelFork c).pt).obj WalkingParallelPair.zero
h : m✝ ≫ Fork.ι (forkOfKernelFork c) = Fork.ι s
⊢ m✝ = IsLimit.lift i (kernelForkOfFork s)
[PROOFSTEP]
apply Fork.IsLimit.hom_ext i
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : KernelFork (f - g)
i : IsLimit c
s : Fork f g
m✝ :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (forkOfKernelFork c).pt).obj WalkingParallelPair.zero
h : m✝ ≫ Fork.ι (forkOfKernelFork c) = Fork.ι s
⊢ m✝ ≫ Fork.ι c = IsLimit.lift i (kernelForkOfFork s) ≫ Fork.ι c
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : Fork f g
i : IsLimit c
s : Fork (f - g) 0
m✝ :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (kernelForkOfFork c).pt).obj WalkingParallelPair.zero
h : m✝ ≫ Fork.ι (kernelForkOfFork c) = Fork.ι s
⊢ m✝ = IsLimit.lift i (forkOfKernelFork s)
[PROOFSTEP]
apply Fork.IsLimit.hom_ext i
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : Fork f g
i : IsLimit c
s : Fork (f - g) 0
m✝ :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (kernelForkOfFork c).pt).obj WalkingParallelPair.zero
h : m✝ ≫ Fork.ι (kernelForkOfFork c) = Fork.ι s
⊢ m✝ ≫ Fork.ι c = IsLimit.lift i (forkOfKernelFork s) ≫ Fork.ι c
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : CokernelCofork (f - g)
⊢ f ≫ Cofork.π c = g ≫ Cofork.π c
[PROOFSTEP]
rw [← sub_eq_zero, ← sub_comp, c.condition]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : Cofork f g
⊢ (f - g) ≫ Cofork.π c = 0 ≫ Cofork.π c
[PROOFSTEP]
rw [sub_comp, zero_comp, sub_eq_zero, c.condition]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
P : C
π : Y ⟶ P
w : f ≫ π = g ≫ π
⊢ (f - g) ≫ π = 0
[PROOFSTEP]
simp [w]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : CokernelCofork (f - g)
i : IsColimit c
s : Cofork f g
m✝ :
  ((Functor.const WalkingParallelPair).obj (coforkOfCokernelCofork c).pt).obj WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
h : Cofork.π (coforkOfCokernelCofork c) ≫ m✝ = Cofork.π s
⊢ m✝ = IsColimit.desc i (cokernelCoforkOfCofork s)
[PROOFSTEP]
apply Cofork.IsColimit.hom_ext i
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : CokernelCofork (f - g)
i : IsColimit c
s : Cofork f g
m✝ :
  ((Functor.const WalkingParallelPair).obj (coforkOfCokernelCofork c).pt).obj WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
h : Cofork.π (coforkOfCokernelCofork c) ≫ m✝ = Cofork.π s
⊢ Cofork.π c ≫ m✝ = Cofork.π c ≫ IsColimit.desc i (cokernelCoforkOfCofork s)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : Cofork f g
i : IsColimit c
s : Cofork (f - g) 0
m✝ :
  ((Functor.const WalkingParallelPair).obj (cokernelCoforkOfCofork c).pt).obj WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
h : Cofork.π (cokernelCoforkOfCofork c) ≫ m✝ = Cofork.π s
⊢ m✝ = IsColimit.desc i (coforkOfCokernelCofork s)
[PROOFSTEP]
apply Cofork.IsColimit.hom_ext i
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : Cofork f g
i : IsColimit c
s : Cofork (f - g) 0
m✝ :
  ((Functor.const WalkingParallelPair).obj (cokernelCoforkOfCofork c).pt).obj WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
h : Cofork.π (cokernelCoforkOfCofork c) ≫ m✝ = Cofork.π s
⊢ Cofork.π c ≫ m✝ = Cofork.π c ≫ IsColimit.desc i (coforkOfCokernelCofork s)
[PROOFSTEP]
aesop_cat
