-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} J
F₁ F₂ F₃ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
τ' : F₂ ⟶ F₃
e : F₁ ≅ F₂
G G' : Functor.{v_2, v_3, u_2, u_3} D E
τ'' : G ⟶ G'
H : Functor.{v_3, v_4, u_3, u_4} E J
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_1, u_1, u_5} C A
inst_6 : HasShift.{v_2, u_2, u_5} D A
inst_7 : HasShift.{v_3, u_3, u_5} E A
inst_8 : HasShift.{v_4, u_4, u_5} J A
inst_9 : F₁.CommShift A
inst_10 : F₂.CommShift A
inst_11 : F₃.CommShift A
inst_12 : G.CommShift A
inst_13 : G'.CommShift A
inst_14 : H.CommShift A
inst_15 : CommShift e.hom A
a : A
X : C
w :
  Eq (α :=
    F₁.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X))
    (e.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      app (Iso.hom (Functor.commShiftIso F₂ a)) X ≫ Functor.map (shiftFunctor D a) (e.inv.app X))
    (e.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      e.inv.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫ app (Iso.hom (Functor.commShiftIso F₁ a)) X)
w₁ :
  Eq (α :=
    F₁.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X))
    (e.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      app (Iso.hom (Functor.commShiftIso F₂ a)) X ≫ Functor.map (shiftFunctor D a) (e.inv.app X))
    (app (Iso.hom (Functor.commShiftIso F₁ a)) X)
w₂ :
  Eq (α :=
    F₁.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X))
    (app (Iso.hom (Functor.commShiftIso F₁ a)) X ≫
      Functor.map (shiftFunctor D a) (e.hom.app X) ≫ Functor.map (shiftFunctor D a) (e.inv.app X))
    (app (Iso.hom (Functor.commShiftIso F₁ a)) X)
w₃ :
  Eq (α :=
    F₁.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X))
    (app (Iso.hom (Functor.commShiftIso F₁ a)) X ≫ Functor.map (shiftFunctor D a) (e.hom.app X ≫ e.inv.app X))
    (app (Iso.hom (Functor.commShiftIso F₁ a)) X)
w₄ :
  Eq (α :=
    F₁.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X))
    (app (Iso.hom (Functor.commShiftIso F₁ a)) X ≫ Functor.map (shiftFunctor D a) (𝟙 (F₁.obj X)))
    (app (Iso.hom (Functor.commShiftIso F₁ a)) X)
⊢ Eq (α :=
    F₂.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X))
    (app (Iso.hom (Functor.commShiftIso F₂ a)) X ≫ Functor.map (shiftFunctor D a) (e.inv.app X))
    (e.inv.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫ app (Iso.hom (Functor.commShiftIso F₁ a)) X)
have w₅ : Eq (α :=
  F₁.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X))
  (app (Iso.hom (Functor.commShiftIso F₁ a)) X ≫ 𝟙 (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X)))
  (app (Iso.hom (Functor.commShiftIso F₁ a)) X)
Tactic: rw [← cancel_epi (e.hom.app (X⟦a⟧)), e.hom_inv_id_app_assoc, ← shift_app_comm_assoc,
    ← Functor.map_comp, e.hom_inv_id_app, Functor.map_id, Category.comp_id]