-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Lifting (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B X Y : CochainComplex.{v_1, u_1, 0} C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → CommSq.LiftStruct (A := Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) n) A) ⋯
Q : CochainComplex.{v_1, u_1, 0} C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex.{v_1, u_1, 0} C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
this_1 : Epi π
this_2 : Mono ι
n : ℤ
this :
  CategoryStruct.comp (Y := X.X (n + 1)) ((↑(cocycle₁' sq hsq) : Cochain B X 1).v n (n + 1) ⋯) (X.d (n + 1) (n + 2)) +
      B.d n (n + 1) ≫ (↑(cocycle₁' sq hsq) : Cochain B X 1).v (n + 1) (n + 2) ⋯ =
    0
h :
  HAdd.hAdd (α := Q.X n ⟶ K.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2))
        (Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯) ≫
      ι.f (n + 2) =
    0 ≫ ι.f (n + 2)
h₁ :
  π.f n ≫
      HAdd.hAdd (α := Q.X n ⟶ K.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2))
          (Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯) ≫
        ι.f (n + 2) =
    π.f n ≫ 0 ≫ ι.f (n + 2)
h₂ :
  π.f n ≫
      HAdd.hAdd (α := Q.X n ⟶ X.X (n + 2)) (((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2)) ≫ ι.f (n + 2))
        ((Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯) ≫ ι.f (n + 2)) =
    π.f n ≫ 0 ≫ ι.f (n + 2)
h₃ :
  π.f n ≫
      HAdd.hAdd (α := Q.X n ⟶ X.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2) ≫ ι.f (n + 2))
        ((Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯) ≫ ι.f (n + 2)) =
    π.f n ≫ 0 ≫ ι.f (n + 2)
h₄ :
  π.f n ≫
      HAdd.hAdd (α := Q.X n ⟶ X.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2) ≫ ι.f (n + 2))
        (Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯ ≫ ι.f (n + 2)) =
    π.f n ≫ 0 ≫ ι.f (n + 2)
h₅ :
  HAdd.hAdd (α := B.X n ⟶ X.X (n + 2))
      (π.f n ≫ (cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2) ≫ ι.f (n + 2))
      (π.f n ≫ Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯ ≫ ι.f (n + 2)) =
    π.f n ≫ 0 ≫ ι.f (n + 2)
h₆ :
  HAdd.hAdd (α := B.X n ⟶ X.X (n + 2))
      (π.f n ≫ (cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2) ≫ ι.f (n + 2))
      (B.d n (n + 1) ≫ π.f (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯ ≫ ι.f (n + 2)) =
    π.f n ≫ 0 ≫ ι.f (n + 2)
h₇ :
  HAdd.hAdd (α := B.X n ⟶ X.X (n + 2))
      (π.f n ≫ (cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2) ≫ ι.f (n + 2))
      (B.d n (n + 1) ≫ (↑(cocycle₁' sq hsq) : Cochain B X 1).v (n + 1) (n + 2) ⋯) =
    π.f n ≫ 0 ≫ ι.f (n + 2)
⊢ HAdd.hAdd (α := Q.X n ⟶ K.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2))
      (Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯) =
    0
have h₈ : HAdd.hAdd (α := B.X n ⟶ X.X (n + 2)) (π.f n ≫ (cochain₁ sq hsq hQ hK).v n (n + 1) sorry ≫ K.d (n + 1) (n + 2) ≫ ι.f (n + 2))
    (B.d n (n + 1) ≫ (↑(cocycle₁' sq hsq) : Cochain B X 1).v (n + 1) (n + 2) sorry) =
  π.f n ≫ 0
Tactic: rwa [← cancel_mono (ι.f (n + 2)), ← cancel_epi (π.f n),
      Preadditive.add_comp, Category.assoc, Category.assoc, Preadditive.comp_add,
      HomologicalComplex.Hom.comm_assoc,
      π_f_cochain₁_v_ι_f, zero_comp, comp_zero, ← ι.comm,
      π_f_cochain₁_v_ι_f_assoc]