-- Lean 4 proof step from Mathlib.Algebra.Homology.ConcreteCategory (goal)
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))
ι : Type u_2
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v, u, u_2} C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
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))
        (S.X₃.X i)) :
    Type v)
hx₃ :
  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))
          (S.X₃.X j)) :
      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))
              (S.X₃.X i))
            (Functor.map
              (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
              (S.X₃.d i j)) :
          (a : (↑((forget₂ C Ab).obj (S.X₃.X i)) : Type v)) → (↑((forget₂ C Ab).obj (S.X₃.X j)) : 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))
            (S.X₃.X j)) :
        Type v))
    (0 :
      (↑(Functor.obj
            (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
              (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
            (S.X₃.X j)) :
        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))
        (S.X₂.X i)) :
    Type v)
hx₂ :
  (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))
            (S.X₂.X i))
          (Functor.map
            (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
              (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
            (S.g.f i)) :
        (a : (↑((forget₂ C Ab).obj (S.X₂.X i)) : Type v)) → (↑((forget₂ C Ab).obj (S.X₃.X i)) : Type v))
      x₂ =
    x₃
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))
        (S.X₁.X j)) :
    Type v)
hx₁ :
  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))
          (S.X₂.X j)) :
      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))
              (S.X₁.X j))
            (Functor.map
              (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
              (S.f.f j)) :
          (a : (↑((forget₂ C Ab).obj (S.X₁.X j)) : Type v)) → (↑((forget₂ C Ab).obj (S.X₂.X j)) : 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))
            (S.X₂.X j)) :
        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))
              (S.X₂.X i))
            (Functor.map
              (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
              (S.X₂.d i j)) :
          (a : (↑((forget₂ C Ab).obj (S.X₂.X i)) : Type v)) → (↑((forget₂ C Ab).obj (S.X₂.X j)) : 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))
            (S.X₂.X j)) :
        Type v))
k : ι
hk : c.next j = k
⊢ 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))
          (S.X₂.X j)) :
      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))
              (S.X₂.X i))
            (Functor.map
              (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
              (S.X₂.d i j)) :
          (a : (↑((forget₂ C Ab).obj (S.X₂.X i)) : Type v)) → (↑((forget₂ C Ab).obj (S.X₂.X j)) : 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))
            (S.X₂.X j)) :
        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))
              (S.X₂.cycles j))
            (Functor.map
              (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
              (S.X₂.iCycles j)) :
          (a : (↑((forget₂ C Ab).obj (S.X₂.cycles j)) : Type v)) → (↑((forget₂ C Ab).obj (S.X₂.X j)) : 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))
                  (S.X₂.opcycles i))
                (Y :=
                Functor.obj
                  (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                    (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
                  (S.X₂.cycles j))
                (Functor.map
                  (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                    (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
                  (S.X₂.opcyclesToCycles i j)) :
              (a : (↑((forget₂ C Ab).obj (S.X₂.opcycles i)) : Type v)) →
                (↑((forget₂ C Ab).obj (S.X₂.cycles j)) : 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))
                      (S.X₂.X i))
                    (Y :=
                    Functor.obj
                      (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                        (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
                      (S.X₂.opcycles i))
                    (Functor.map
                      (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                        (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
                      (S.X₂.pOpcycles i)) :
                  (a : (↑((forget₂ C Ab).obj (S.X₂.X i)) : Type v)) →
                    (↑((forget₂ C Ab).obj (S.X₂.opcycles i)) : 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))
                    (S.X₂.opcycles i)) :
                Type v)) :
          (↑(Functor.obj
                (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                  (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
                (S.X₂.cycles j)) :
            Type v)) :
      (↑(Functor.obj
            (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
              (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
            (S.X₂.X j)) :
        Type v))
have conv_rhs : 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))
        (S.X₂.X j)) :
    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))
            (S.X₂.X i))
          (Functor.map
            (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
              (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
            (S.X₂.d i j)) :
        (a : (↑((forget₂ C Ab).obj (S.X₂.X i)) : Type v)) → (↑((forget₂ C Ab).obj (S.X₂.X j)) : 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))
          (S.X₂.X j)) :
      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))
            (S.X₂.cycles j))
          (Functor.map
            (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
              (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
            (S.X₂.iCycles j)) :
        (a : (↑((forget₂ C Ab).obj (S.X₂.cycles j)) : Type v)) → (↑((forget₂ C Ab).obj (S.X₂.X j)) : 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))
                (S.X₂.opcycles i))
              (Y :=
              Functor.obj
                (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                  (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
                (S.X₂.cycles j))
              (Functor.map
                (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                  (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
                (S.X₂.opcyclesToCycles i j)) :
            (a : (↑((forget₂ C Ab).obj (S.X₂.opcycles i)) : Type v)) → (↑((forget₂ C Ab).obj (S.X₂.cycles j)) : 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))
                    (S.X₂.X i))
                  (Y :=
                  Functor.obj
                    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                      (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
                    (S.X₂.opcycles i))
                  (Functor.map
                    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                      (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
                    (S.X₂.pOpcycles i)) :
                (a : (↑((forget₂ C Ab).obj (S.X₂.X i)) : Type v)) → (↑((forget₂ C Ab).obj (S.X₂.opcycles i)) : 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))
                  (S.X₂.opcycles i)) :
              Type v)) :
        (↑(Functor.obj
              (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
              (S.X₂.cycles j)) :
          Type v)) :
    (↑(Functor.obj
          (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
            (CD := AddCommGrpCat.carrier))
          (S.X₂.X j)) :
      Type v))
Tactic: conv_rhs =>
      rw [← ConcreteCategory.forget₂_comp_apply, ← ConcreteCategory.forget₂_comp_apply,
        HomologicalComplex.pOpcycles_opcyclesToCycles_assoc, HomologicalComplex.toCycles_i]