[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
⊢ ↟(Submodule.subtype (LinearMap.ker f)) ≫ f = 0
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
x : ↑(of R { x // x ∈ LinearMap.ker f })
⊢ ↑(↟(Submodule.subtype (LinearMap.ker f)) ≫ f) x = ↑0 x
[PROOFSTEP]
cases x
[GOAL]
case h.mk
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
val✝ : ↑M
property✝ : val✝ ∈ LinearMap.ker f
⊢ ↑(↟(Submodule.subtype (LinearMap.ker f)) ≫ f) { val := val✝, property := property✝ } =
    ↑0 { val := val✝, property := property✝ }
[PROOFSTEP]
assumption
[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
s : Fork f 0
c : ↑s.pt
⊢ ↑f (↑(Fork.ι s) c) = 0
[PROOFSTEP]
rw [← @Function.comp_apply _ _ _ f (Fork.ι s) c, ← coe_comp, Fork.condition, HasZeroMorphisms.comp_zero (Fork.ι s) N]
[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
s : Fork f 0
c : ↑s.pt
⊢ ↑0 c = 0
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
s : Fork f 0
m : s.pt ⟶ (kernelCone f).pt
h : m ≫ Fork.ι (kernelCone f) = Fork.ι s
x : ↑s.pt
⊢ ↑(↑m x) =
    ↑(↑((fun s =>
              LinearMap.codRestrict (LinearMap.ker f) (Fork.ι s) (_ : ∀ (c : ↑s.pt), ↑(Fork.ι s) c ∈ LinearMap.ker f))
            s)
        x)
[PROOFSTEP]
simp [← h]
[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
s : Fork f 0
m : s.pt ⟶ (kernelCone f).pt
h : m ≫ Fork.ι (kernelCone f) = Fork.ι s
x : ↑s.pt
⊢ ↑m x =
    ↑(LinearMap.codRestrict (LinearMap.ker f) (m ≫ Fork.ι (kernelCone f))
          (_ : ∀ (c : ↑s.pt), ↑(m ≫ Fork.ι (kernelCone f)) c ∈ LinearMap.ker f))
      x
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
s : Cofork f 0
m : (cokernelCocone f).pt ⟶ s.pt
h : Cofork.π (cokernelCocone f) ≫ m = Cofork.π s
⊢ m = (fun s => Submodule.liftQ (LinearMap.range f) (Cofork.π s) (_ : LinearMap.range f ≤ LinearMap.ker (Cofork.π s))) s
[PROOFSTEP]
haveI : Epi (asHom (LinearMap.range f).mkQ) :=
  (epi_iff_range_eq_top _).mpr
    (Submodule.range_mkQ _)
      -- Porting note: broken dot notation
[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
s : Cofork f 0
m : (cokernelCocone f).pt ⟶ s.pt
h : Cofork.π (cokernelCocone f) ≫ m = Cofork.π s
this : Epi (↟(Submodule.mkQ (LinearMap.range f)))
⊢ m = (fun s => Submodule.liftQ (LinearMap.range f) (Cofork.π s) (_ : LinearMap.range f ≤ LinearMap.ker (Cofork.π s))) s
[PROOFSTEP]
apply (cancel_epi (asHom (LinearMap.range f).mkQ)).1
[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
s : Cofork f 0
m : (cokernelCocone f).pt ⟶ s.pt
h : Cofork.π (cokernelCocone f) ≫ m = Cofork.π s
this : Epi (↟(Submodule.mkQ (LinearMap.range f)))
⊢ ↟(Submodule.mkQ (LinearMap.range f)) ≫ m =
    ↟(Submodule.mkQ (LinearMap.range f)) ≫
      (fun s => Submodule.liftQ (LinearMap.range f) (Cofork.π s) (_ : LinearMap.range f ≤ LinearMap.ker (Cofork.π s))) s
[PROOFSTEP]
convert h
[GOAL]
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
⊢ cokernel.π f ≫ (cokernelIsoRangeQuotient f).hom = Submodule.mkQ (LinearMap.range f)
[PROOFSTEP]
convert colimit.isoColimitCocone_ι_hom (F := parallelPair f 0) _ _
[GOAL]
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f✝ : G ⟶ H
M N : ModuleCat R
f : M ⟶ N
x y : ↑N
m : ↑M
w : x = y + ↑f m
⊢ ↑(cokernel.π f) x = ↑(cokernel.π f) y
[PROOFSTEP]
subst w
[GOAL]
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f✝ : G ⟶ H
M N : ModuleCat R
f : M ⟶ N
y : ↑N
m : ↑M
⊢ ↑(cokernel.π f) (y + ↑f m) = ↑(cokernel.π f) y
[PROOFSTEP]
simpa only [map_add, add_right_eq_self] using cokernel.condition_apply f m
