-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexOpposite (hypothesis)
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 : ℤ
⊢ Quiver.Hom.op (f.f (-n)) =
    (HAdd.hAdd (α := K.X (-n) ⟶ L.X (-n)) (β := K.X (-n) ⟶ L.X (-n))
          ((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 :
            K.X (-n) ⟶ L.X (-n))
          ((prevD (-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 :
            K.X (-n) ⟶ L.X (-n)) +
        g.f (-n)).op
have this : HomologicalComplex.Hom.f (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) f.op) n =
  HAdd.hAdd (α :=
      (Functor.obj (Equivalence.functor (opEquivalence C)) (op L)).X n ⟶
        (Functor.obj (Equivalence.functor (opEquivalence C)) (op K)).X n)
      (β :=
      (Functor.obj (Equivalence.functor (opEquivalence C)) (op L)).X n ⟶
        (Functor.obj (Equivalence.functor (opEquivalence C)) (op K)).X n)
      (((dNext.{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)) n :
              ((i j : ℤ) →
                  (Functor.obj (Equivalence.functor (opEquivalence C)) (op L)).X i ⟶
                    (Functor.obj (Equivalence.functor (opEquivalence C)) (op K)).X j) →+
                ((Functor.obj (Equivalence.functor (opEquivalence C)) (op L)).X n ⟶
                  (Functor.obj (Equivalence.functor (opEquivalence C)) (op K)).X n)) :
            (a : (i j : ℤ) → ((opEquivalence C).functor.obj (op L)).X i ⟶ ((opEquivalence C).functor.obj (op K)).X j) →
              ((opEquivalence C).functor.obj (op L)).X n ⟶ ((opEquivalence C).functor.obj (op K)).X n)
          h.hom :
        (Functor.obj (Equivalence.functor (opEquivalence C)) (op L)).X n ⟶
          (Functor.obj (Equivalence.functor (opEquivalence C)) (op K)).X n)
      (((prevD.{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)) n :
              ((i j : ℤ) →
                  (Functor.obj (Equivalence.functor (opEquivalence C)) (op L)).X i ⟶
                    (Functor.obj (Equivalence.functor (opEquivalence C)) (op K)).X j) →+
                ((Functor.obj (Equivalence.functor (opEquivalence C)) (op L)).X n ⟶
                  (Functor.obj (Equivalence.functor (opEquivalence C)) (op K)).X n)) :
            (a : (i j : ℤ) → ((opEquivalence C).functor.obj (op L)).X i ⟶ ((opEquivalence C).functor.obj (op K)).X j) →
              ((opEquivalence C).functor.obj (op L)).X n ⟶ ((opEquivalence C).functor.obj (op K)).X n)
          h.hom :
        (Functor.obj (Equivalence.functor (opEquivalence C)) (op L)).X n ⟶
          (Functor.obj (Equivalence.functor (opEquivalence C)) (op K)).X n) +
    HomologicalComplex.Hom.f (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) g.op) n
Tactic: have := h.comm n