-- 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 f g
n : ℤ
e_a :
  Eq (α := op (L.X (-n)) ⟶ op (K.X (-n)))
    (Quiver.Hom.op ((prevD (-n) : (a : (i j : ℤ) → K.X i ⟶ L.X j) → K.X (-n) ⟶ L.X (-n)) h.hom) :
      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)))
        fun (p q : ℤ) ↦ Quiver.Hom.op (h.hom (-q) (-p)) :
      op (L.X (-n)) ⟶ op (K.X (-n)))
⊢ HAdd.hAdd (α := op (L.X (-n)) ⟶ op (K.X (-n))) (β := op (L.X (-n)) ⟶ op (K.X (-n)))
      (Quiver.Hom.op ((prevD (-n) : (a : (i j : ℤ) → K.X i ⟶ L.X j) → K.X (-n) ⟶ L.X (-n)) h.hom) :
        op (L.X (-n)) ⟶ op (K.X (-n)))
      (Quiver.Hom.op ((dNext (-n) : (a : (i j : ℤ) → K.X i ⟶ L.X j) → K.X (-n) ⟶ L.X (-n)) h.hom) :
        op (L.X (-n)) ⟶ op (K.X (-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)))
          fun (p q : ℤ) ↦ Quiver.Hom.op (h.hom (-q) (-p)) :
        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)))
          fun (p q : ℤ) ↦ Quiver.Hom.op (h.hom (-q) (-p)) :
        op (L.X (-n)) ⟶ op (K.X (-n)))
have e_a₁ : Eq (α := op (L.X (-n)) ⟶ op (K.X (-n)))
  (Quiver.Hom.op ((dNext (-n) : (a : (i j : ℤ) → K.X i ⟶ L.X j) → K.X (-n) ⟶ L.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)))
      fun (p q : ℤ) ↦ Quiver.Hom.op (h.hom (-q) (-p)) :
    op (L.X (-n)) ⟶ op (K.X (-n)))
Tactic: congr 1