-- 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₃ :
  (↑(Functor.obj
        (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
          (CD := AddCommGrpCat.carrier))
        D.L₀.X₃) :
    Type v)
x₂ :
  (↑(Functor.obj
        (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
          (CD := AddCommGrpCat.carrier))
        D.L₁.X₂) :
    Type v)
x₁ :
  (↑(Functor.obj
        (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
          (CD := AddCommGrpCat.carrier))
        D.L₂.X₁) :
    Type v)
h₂ :
  Eq (α :=
    (↑(Functor.obj
          (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
            (CD := AddCommGrpCat.carrier))
          D.L₁.X₃) :
      Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (X :=
            Functor.obj
              (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
              D.L₁.X₂)
            (Functor.map
              (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
              D.L₁.g) :
          (a : (↑((forget₂ C Ab).obj D.L₁.X₂) : Type v)) → (↑((forget₂ C Ab).obj D.L₁.X₃) : Type v))
        x₂ :
      (↑(Functor.obj
            (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
              (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
            D.L₁.X₃) :
        Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (X :=
            Functor.obj
              (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
              D.L₀.X₃)
            (Functor.map
              (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
              D.v₀₁.τ₃) :
          (a : (↑((forget₂ C Ab).obj D.L₀.X₃) : Type v)) → (↑((forget₂ C Ab).obj D.L₁.X₃) : Type v))
        x₃ :
      (↑(Functor.obj
            (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
              (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
            D.L₁.X₃) :
        Type v))
h₁ :
  Eq (α :=
    (↑(Functor.obj
          (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
            (CD := AddCommGrpCat.carrier))
          D.L₂.X₂) :
      Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (X :=
            Functor.obj
              (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
              D.L₂.X₁)
            (Functor.map
              (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
              D.L₂.f) :
          (a : (↑((forget₂ C Ab).obj D.L₂.X₁) : Type v)) → (↑((forget₂ C Ab).obj D.L₂.X₂) : Type v))
        x₁ :
      (↑(Functor.obj
            (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
              (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
            D.L₂.X₂) :
        Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (X :=
            Functor.obj
              (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
              D.L₁.X₂)
            (Functor.map
              (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
              D.v₁₂.τ₂) :
          (a : (↑((forget₂ C Ab).obj D.L₁.X₂) : Type v)) → (↑((forget₂ C Ab).obj D.L₂.X₂) : Type v))
        x₂ :
      (↑(Functor.obj
            (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
              (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
            D.L₂.X₂) :
        Type v))
e :
  Iso (C := C ⥤ Type v)
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
        (CD := AddCommGrpCat.carrier) ⋙
      forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
        AddCommGrpCat.carrier))
    (forget C (FC := FC) (CC := CC))
⊢ Eq (α := (fun (X : Type v) ↦ X) (Functor.obj (forget C (FC := FC) (CC := CC)) D.L₃.X₁))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app D.L₃.X₁) :
          (a : (fun (X : Type v) ↦ X) ((forget₂ C Ab ⋙ forget Ab).obj D.L₃.X₁)) →
            (fun (X : Type v) ↦ X) ((forget C).obj D.L₃.X₁))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) (X :=
                Functor.obj
                  (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                    (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
                  D.L₀.X₃)
                (Functor.map
                  (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                    (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
                  D.δ) :
              (a : (↑((forget₂ C Ab).obj D.L₀.X₃) : Type v)) → (↑((forget₂ C Ab).obj D.L₃.X₁) : Type v))
            x₃ :
          (↑(Functor.obj
                (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                  (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
                D.L₃.X₁) :
            Type v)) :
      (fun (X : Type v) ↦ X) (Functor.obj (forget C (FC := FC) (CC := CC)) D.L₃.X₁))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app D.L₃.X₁) :
          (a : (fun (X : Type v) ↦ X) ((forget₂ C Ab ⋙ forget Ab).obj D.L₃.X₁)) →
            (fun (X : Type v) ↦ X) ((forget C).obj D.L₃.X₁))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) (X :=
                Functor.obj
                  (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                    (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
                  D.L₂.X₁)
                (Functor.map
                  (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                    (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
                  D.v₂₃.τ₁) :
              (a : (↑((forget₂ C Ab).obj D.L₂.X₁) : Type v)) → (↑((forget₂ C Ab).obj D.L₃.X₁) : Type v))
            x₁ :
          (↑(Functor.obj
                (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                  (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
                D.L₃.X₁) :
            Type v)) :
      (fun (X : Type v) ↦ X) (Functor.obj (forget C (FC := FC) (CC := CC)) D.L₃.X₁))

Tactic:
exact (ConcreteCategory.congr_hom (e.hom.naturality D.δ) x₃).trans ((D.δ_apply _ _ _
    (((ConcreteCategory.congr_hom (e.hom.naturality D.L₁.g) x₂).symm.trans (by simp_all)).trans
      (ConcreteCategory.congr_hom (e.hom.naturality D.v₀₁.τ₃) x₃))
    (((ConcreteCategory.congr_hom (e.hom.naturality D.L₂.f) x₁).symm.trans (by simp_all)).trans
      (ConcreteCategory.congr_hom (e.hom.naturality D.v₁₂.τ₂) x₂))).trans
    (ConcreteCategory.congr_hom (e.hom.naturality D.v₂₃.τ₁).symm x₁))

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Iso.hom, Eq.trans, CategoryTheory.ShortComplex.SnakeInput.δ