-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
mp :
  (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker →
    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          ModuleCat.carrier) S.g).ker =
      (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          ModuleCat.carrier) S.f).range
mpr :
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          ModuleCat.carrier) S.g).ker =
      (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          ModuleCat.carrier) S.f).range →
    (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker
mp₁ mp₂ mp₃ :
  (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker →
    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          ModuleCat.carrier) S.g).ker =
      (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          ModuleCat.carrier) S.f).range
mpr₁ mpr₂ mpr₃ :
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          ModuleCat.carrier) S.g).ker =
      (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          ModuleCat.carrier) S.f).range →
    (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker
mp₄ mp₅ mp₆ :
  (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker →
    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          ModuleCat.carrier) S.g).ker =
      (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          ModuleCat.carrier) S.f).range
mpr₄ mpr₅ mpr₆ :
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          ModuleCat.carrier) S.g).ker =
      (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          ModuleCat.carrier) S.f).range →
    (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker
mp₇ mp₈ :
  (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker →
    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          ModuleCat.carrier) S.g).ker =
      (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          ModuleCat.carrier) S.f).range
mpr₇ mpr₈ :
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          ModuleCat.carrier) S.g).ker =
      (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          ModuleCat.carrier) S.f).range →
    (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker
⊢ (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker ↔
    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          ModuleCat.carrier) S.g).ker =
      (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          ModuleCat.carrier) S.f).range

Tactic:
tauto