-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexOpposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h :
  Homotopy.{v_1, u_1, 0} (ι := ℤ) (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
    Functor.obj (Equivalence.functor (opEquivalence C)) (op L)) (D :=
    Functor.obj (Equivalence.functor (opEquivalence C)) (op K))
    (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) f.op)
    (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) g.op)
H :
  ∀ (p q p' q' : ℤ) (hp : p = p') (hq : q = q'),
    h.hom p q =
      Quiver.Hom.op (Iso.hom (HomologicalComplex.XIsoOfEq L ⋯)) ≫
        h.hom p' q' ≫ Quiver.Hom.op (Iso.hom (HomologicalComplex.XIsoOfEq K ⋯))
n : ℤ
this :
  Quiver.Hom.op (f.f (-n)) =
    HAdd.hAdd (α := op (L.X (-n)) ⟶ op (K.X (-n))) (β := op (L.X (-n)) ⟶ op (K.X (-n)))
        (((dNext.{v_1, u_1, 0} (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
                  (HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt) (D :=
                  (HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt) n :
                ((i j : ℤ) →
                    ((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X i ⟶
                      ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X j) →+
                  (((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X n ⟶
                    ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X n)) :
              (a : (i j : ℤ) → op (L.X (-i)) ⟶ op (K.X (-j))) → op (L.X (-n)) ⟶ op (K.X (-n)))
            h.hom :
          op (L.X (-n)) ⟶ op (K.X (-n)))
        (((prevD.{v_1, u_1, 0} (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
                  (HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt) (D :=
                  (HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt) n :
                ((i j : ℤ) →
                    ((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X i ⟶
                      ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X j) →+
                  (((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X n ⟶
                    ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X n)) :
              (a : (i j : ℤ) → op (L.X (-i)) ⟶ op (K.X (-j))) → op (L.X (-n)) ⟶ op (K.X (-n)))
            h.hom :
          op (L.X (-n)) ⟶ op (K.X (-n))) +
      Quiver.Hom.op (g.f (-n))
⊢ CategoryStruct.comp (Y := ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X (n - 1))
      (h.hom n (n - 1)) (((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).d (n - 1) n) =
    Quiver.Hom.op
      ((dNext (-n) : (a : (i j : ℤ) → K.X i ⟶ L.X j) → K.X (-n) ⟶ L.X (-n)) fun (p q : ℤ) ↦
        (HomologicalComplex.XIsoOfEq K ⋯).hom ≫
          Quiver.Hom.unop (h.hom (-q) (-p)) ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom)
have e_a : CategoryStruct.comp (Y := ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X (n - 1))
    (h.hom n (n - 1)) (((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).d (n - 1) n) =
  Quiver.Hom.op
    (CategoryStruct.comp (Y := K.X (-(n - 1))) (K.d (-n) (-(n - 1)))
      (Iso.hom (HomologicalComplex.XIsoOfEq K sorry) ≫
        Quiver.Hom.unop (h.hom (- -n) (- -(n - 1))) ≫ Iso.hom (HomologicalComplex.XIsoOfEq L sorry)))
Tactic: rw [dNext_eq _ (i' := - (n - 1)) (by dsimp; lia)]