-- Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 :
  HasForget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CD := AddCommGrpCat.carrier)
inst_4 : Abelian.{v, u} C
inst_5 :
  Functor.Additive
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
      (CD := AddCommGrpCat.carrier))
inst_6 :
  Functor.PreservesHomology
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
      (CD := AddCommGrpCat.carrier))
D : SnakeInput.{v, u} C
x₃ : ToType (FC := FC) (CC := CC) D.L₀.X₃
x₂ : ToType (FC := FC) (CC := CC) D.L₁.X₂
x₁ : ToType (FC := FC) (CC := CC) D.L₂.X₁
h₂ :
  Eq (α := CC D.L₁.X₃)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.L₁.g : (a : CC D.L₁.X₂) → CC D.L₁.X₃) x₂ : CC D.L₁.X₃)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.v₀₁.τ₃ : (a : CC D.L₀.X₃) → CC D.L₁.X₃) x₃ : CC D.L₁.X₃)
h₁ :
  Eq (α := CC D.L₂.X₂)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.L₂.f : (a : CC D.L₂.X₁) → CC D.L₂.X₂) x₁ : CC D.L₂.X₂)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.v₁₂.τ₂ : (a : CC D.L₁.X₂) → CC D.L₂.X₂) x₂ : CC D.L₂.X₂)
this_1 :
  PreservesFiniteLimits
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
      (CD := AddCommGrpCat.carrier))
this : PreservesFiniteLimits (forget C (FC := FC) (CC := CC))
eq :
  Eq (α := CC D.L₃.X₁)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.δ : (a : CC D.L₀.X₃) → CC D.L₃.X₁) x₃ : CC D.L₃.X₁)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.v₂₃.τ₁ : (a : CC D.L₂.X₁) → CC D.L₃.X₁)
        ((ConcreteCategory.hom (FC := FC) (CC := CC) D.φ₁ : (a : CC (pullback D.L₁.g D.v₀₁.τ₃)) → CC D.L₂.X₁)
            (Concrete.pullbackMk (FC := FC) (CC := CC) D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) :
          CC D.L₂.X₁) :
      CC D.L₃.X₁)
eq₁ :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (pullback.fst D.L₁.g D.v₀₁.τ₃) :
        (a : CC (pullback D.L₁.g D.v₀₁.τ₃)) → CC D.L₁.X₂)
      (Concrete.pullbackMk (FC := FC) (CC := CC) D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) =
    x₂
eq₂ :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (pullback.snd D.L₁.g D.v₀₁.τ₃) :
        (a : CC (pullback D.L₁.g D.v₀₁.τ₃)) → CC D.L₀.X₃)
      (Concrete.pullbackMk (FC := FC) (CC := CC) D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) =
    x₃
a :
  Eq (α := CC D.L₂.X₂)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.L₂.f : (a : CC D.L₂.X₁) → CC D.L₂.X₂)
        ((ConcreteCategory.hom (FC := FC) (CC := CC) D.φ₁ : (a : CC (pullback D.L₁.g D.v₀₁.τ₃)) → CC D.L₂.X₁)
            (Concrete.pullbackMk (FC := FC) (CC := CC) D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) :
          CC D.L₂.X₁) :
      CC D.L₂.X₂)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.L₂.f : (a : CC D.L₂.X₁) → CC D.L₂.X₂) x₁ : CC D.L₂.X₂)
⊢ (ConcreteCategory.hom (FC := FC) (CC := CC) D.φ₁ : (a : CC (pullback D.L₁.g D.v₀₁.τ₃)) → CC D.L₂.X₁)
      (Concrete.pullbackMk (FC := FC) (CC := CC) D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) =
    x₁

Tactic:
apply (Preadditive.mono_iff_injective' D.L₂.f).1 inferInstance

Premises used: CategoryTheory.ShortComplex.SnakeInput.L₂, inferInstance, Iff.mp, CategoryTheory.ShortComplex.f, CategoryTheory.Preadditive.mono_iff_injective'