-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory (hypothesis)
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) (pullback.snd D.L₁.g D.v₀₁.τ₃ ≫ 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₁)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.φ₁ ≫ 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₂) :
      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₃
⊢ 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₁) x₁ : CC D.L₃.X₁)
have eq₃ : Eq (α := CC D.L₃.X₁)
  ((ConcreteCategory.hom (FC := FC) (CC := CC) D.δ : (a : CC D.L₀.X₃) → CC D.L₃.X₁)
      ((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₂) :
        CC D.L₀.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₁)
Tactic: rw [ConcreteCategory.comp_apply, ConcreteCategory.comp_apply] at eq
Cleared hypotheses: eq, eq₁, eq₂