-- Lean 4 proof step from Mathlib.Algebra.Homology.LeftResolution.Basic (goal)
Goal:
A : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} A
ι : Functor.{v_1, v_2, u_2, u_1} C A
Λ : LeftResolution ι
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst_2 : ι.Full
inst_3 : ι.Faithful
inst_4 : HasZeroMorphisms.{v_1, u_2} C
inst_5 : Abelian.{v_2, u_1} A
n : ℕ
p :
  (f : HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex Y) n) ×'
    (f' : HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Y) (n + 1)) ×'
      f' ≫ HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n = HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫ f
rw :
  ι.map
      (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫
        p.fst (β := fun (f : HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex Y) n) ↦
          (f' : HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Y) (n + 1)) ×'
            f' ≫ HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n =
              HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫ f)) =
    ι.map
        (p.snd (β := fun (f : HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex Y) n) ↦
              (f' :
                HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Y) (n + 1)) ×'
                f' ≫ HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n =
                  HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫ f).fst
          (β :=
          fun (f' : HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Y) (n + 1)) ↦
          f' ≫ HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n =
            HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫
              p.fst (β :=
                fun (f : HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex Y) n) ↦
                (f' :
                  HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Y) (n + 1)) ×'
                  f' ≫ HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n =
                    HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫ f))) ≫
      ι.map (HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n)
rw₁ :
  ι.map
      (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫
        p.fst (β := fun (f : HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex Y) n) ↦
          (f' : HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Y) (n + 1)) ×'
            f' ≫ HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n =
              HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫ f)) =
    ι.map
      (p.snd (β := fun (f : HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex Y) n) ↦
              (f' :
                HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Y) (n + 1)) ×'
                f' ≫ HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n =
                  HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫ f).fst
          (β :=
          fun (f' : HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Y) (n + 1)) ↦
          f' ≫ HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n =
            HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫
              p.fst (β :=
                fun (f : HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex Y) n) ↦
                (f' :
                  HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Y) (n + 1)) ×'
                  f' ≫ HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n =
                    HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫ f)) ≫
        HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n)
⊢ ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n) ≫
      ι.map
        (p.fst (β := fun (f : HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex Y) n) ↦
          (f' : HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Y) (n + 1)) ×'
            f' ≫ HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n =
              HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫ f)) =
    ι.map
        (p.snd (β := fun (f : HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex Y) n) ↦
              (f' :
                HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Y) (n + 1)) ×'
                f' ≫ HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n =
                  HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫ f).fst
          (β :=
          fun (f' : HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Y) (n + 1)) ↦
          f' ≫ HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n =
            HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫
              p.fst (β :=
                fun (f : HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex Y) n) ↦
                (f' :
                  HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Y) (n + 1)) ×'
                  f' ≫ HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n =
                    HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫ f))) ≫
      ι.map (HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n)
have rw₂ : Eq (α := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)) ⟶ ι.obj (HomologicalComplex.X (Λ.chainComplex Y) n))
  (ι.map
    (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫
      p.fst (β := fun (f : HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex Y) n) ↦
        (f' : HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Y) (n + 1)) ×'
          f' ≫ HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n =
            HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫ f)))
  (ι.map
    (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫
      p.fst (β := fun (f : HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex Y) n) ↦
        (f' : HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Y) (n + 1)) ×'
          f' ≫ HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n =
            HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫ f)))
Tactic: rw [← ι.map_comp, ← ι.map_comp, p.2.2]