[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
hf : Mono f
⊢ (LinearEquiv.toModuleIso'
          (LinearEquiv.trans (LinearEquiv.symm (Submodule.quotEquivOfEqBot (LinearMap.ker f) (_ : LinearMap.ker f = ⊥)))
            (LinearEquiv.trans (LinearMap.quotKerEquivRange f)
              (LinearEquiv.ofEq (LinearMap.range f) (LinearMap.ker (Submodule.mkQ (LinearMap.range f)))
                (_ : LinearMap.range f = LinearMap.ker (Submodule.mkQ (LinearMap.range f))))))).hom ≫
      Fork.ι (kernelCone (Submodule.mkQ (LinearMap.range f))) =
    f
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
hf : Mono f
x✝ : ↑M
⊢ ↑((LinearEquiv.toModuleIso'
              (LinearEquiv.trans
                (LinearEquiv.symm (Submodule.quotEquivOfEqBot (LinearMap.ker f) (_ : LinearMap.ker f = ⊥)))
                (LinearEquiv.trans (LinearMap.quotKerEquivRange f)
                  (LinearEquiv.ofEq (LinearMap.range f) (LinearMap.ker (Submodule.mkQ (LinearMap.range f)))
                    (_ : LinearMap.range f = LinearMap.ker (Submodule.mkQ (LinearMap.range f))))))).hom ≫
          Fork.ι (kernelCone (Submodule.mkQ (LinearMap.range f))))
      x✝ =
    ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
hf : Epi f
⊢ Cofork.π (cokernelCocone (Submodule.subtype (LinearMap.ker f))) ≫
      (LinearEquiv.toModuleIso'
          (LinearEquiv.trans
            (LinearEquiv.trans
              (Submodule.quotEquivOfEq (LinearMap.range (Submodule.subtype (LinearMap.ker f))) (LinearMap.ker f)
                (_ : LinearMap.range (Submodule.subtype (LinearMap.ker f)) = LinearMap.ker f))
              (LinearMap.quotKerEquivRange f))
            (LinearEquiv.ofTop (LinearMap.range f) (_ : LinearMap.range f = ⊤)))).hom =
    f
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
hf : Epi f
x✝ : ↑((parallelPair (Submodule.subtype (LinearMap.ker f)) 0).obj WalkingParallelPair.one)
⊢ ↑(Cofork.π (cokernelCocone (Submodule.subtype (LinearMap.ker f))) ≫
          (LinearEquiv.toModuleIso'
              (LinearEquiv.trans
                (LinearEquiv.trans
                  (Submodule.quotEquivOfEq (LinearMap.range (Submodule.subtype (LinearMap.ker f))) (LinearMap.ker f)
                    (_ : LinearMap.range (Submodule.subtype (LinearMap.ker f)) = LinearMap.ker f))
                  (LinearMap.quotKerEquivRange f))
                (LinearEquiv.ofTop (LinearMap.range f) (_ : LinearMap.range f = ⊤)))).hom)
      x✝ =
    ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
O : ModuleCat R
g : N ⟶ O
⊢ Exact f g ↔ range f = ker g
[PROOFSTEP]
rw [abelian.exact_iff' f g (kernelIsLimit _) (cokernelIsColimit _)]
[GOAL]
R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
O : ModuleCat R
g : N ⟶ O
⊢ f ≫ g = 0 ∧ Fork.ι (kernelCone g) ≫ Cofork.π (cokernelCocone f) = 0 ↔ range f = ker g
[PROOFSTEP]
exact
  ⟨fun h => le_antisymm (range_le_ker_iff.2 h.1) (ker_le_range_iff.2 h.2), fun h =>
    ⟨range_le_ker_iff.1 <| le_of_eq h, ker_le_range_iff.1 <| le_of_eq h.symm⟩⟩
