[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
s : Fork f 0
⊢ ↑s.pt →+ ↑G
[PROOFSTEP]
exact Fork.ι s
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
s : Fork f 0
c : ↑s.pt
⊢ ↑f (↑(Fork.ι s) c) = 0
[PROOFSTEP]
exact FunLike.congr_fun s.condition c
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
x✝ : Fork f 0
⊢ (fun s => codRestrict (Fork.ι s) (ker f) (_ : ∀ (c : ↑s.pt), ↑(Fork.ι s) c ∈ ker f)) x✝ ≫ Fork.ι (kernelCone f) =
    Fork.ι x✝
[PROOFSTEP]
rfl
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
x✝¹ : Fork f 0
x✝ : x✝¹.pt ⟶ (kernelCone f).pt
h : x✝ ≫ Fork.ι (kernelCone f) = Fork.ι x✝¹
x : ↑x✝¹.pt
⊢ ↑(↑x✝ x) = ↑(↑((fun s => codRestrict (Fork.ι s) (ker f) (_ : ∀ (c : ↑s.pt), ↑(Fork.ι s) c ∈ ker f)) x✝¹) x)
[PROOFSTEP]
exact FunLike.congr_fun h x
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
x✝¹ : Cofork f 0
x✝ : (cokernelCocone f).pt ⟶ x✝¹.pt
h : Cofork.π (cokernelCocone f) ≫ x✝ = Cofork.π x✝¹
this : Epi (Cofork.π (cokernelCocone f))
⊢ ?m.55829 x✝¹ x✝ h this ≫ x✝ =
    ?m.55829 x✝¹ x✝ h this ≫ (fun s => lift (range f) (Cofork.π s) (_ : range f ≤ ker (Cofork.π s))) x✝¹
[PROOFSTEP]
simpa only [parallelPair_obj_one] using h
