-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_5} C A
inst_4 : HasShift.{v_2, u_2, u_5} D A
inst_5 : F₁.CommShift A
inst_6 : F₂.CommShift A
a b : A
ha : CommShiftCore τ a
hb : CommShiftCore τ b
X : C
this :
  Eq (α :=
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
        (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X)) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F₂.obj X))
    (Functor.map (shiftFunctor D b) (Functor.map (shiftFunctor D a) (τ.app X)) ≫
        app (Iso.inv (shiftFunctorAdd D a b)) (F₂.obj X) :
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
          (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X)) ⟶
        Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F₂.obj X))
    (app (Iso.inv (shiftFunctorAdd D a b)) (F₁.obj X) ≫ Functor.map (shiftFunctor D (a + b)) (τ.app X) :
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
          (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X)) ⟶
        Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F₂.obj X))
⊢ Eq (α :=
    F₁.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F₂.obj X))
    (app (Iso.hom (Functor.commShiftIso F₁ (a + b))) X ≫ Functor.map (shiftFunctor D (a + b)) (τ.app X))
    (τ.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X) ≫
      app (Iso.hom (Functor.commShiftIso F₂ (a + b))) X)
have w : Eq (α :=
  F₁.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X) ⟶
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F₂.obj X))
  (F₁.map (app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
    app (Iso.hom (Functor.commShiftIso F₁ b)) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      Functor.map (shiftFunctor D b) (app (Iso.hom (Functor.commShiftIso F₁ a)) X) ≫
        app (Iso.inv (shiftFunctorAdd D a b)) (F₁.obj X) ≫ Functor.map (shiftFunctor D (a + b)) (τ.app X))
  (F₁.map (Iso.hom (Iso.app (shiftFunctorAdd C a b) X)) ≫
    CategoryStruct.comp (Y :=
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
        (F₁.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
      (app (Iso.hom (Functor.commShiftIso F₁ b)) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (CategoryStruct.comp (Y :=
        Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
          (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F₁.obj X)))
        (Functor.map (shiftFunctor D b) (app (Iso.hom (Functor.commShiftIso F₁ a)) X))
        (Functor.map (shiftFunctor D b) (Functor.map (shiftFunctor D a) (τ.app X)) ≫
          CategoryStruct.comp (Y :=
            Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
              (F₂.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
            (Functor.map (shiftFunctor D b) (app (Iso.inv (Functor.commShiftIso F₂ a)) X))
            (app (Iso.inv (Functor.commShiftIso F₂ b)) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
              F₂.map (Iso.inv (Iso.app (shiftFunctorAdd C a b) X)) ≫
                F₂.map (app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
                  CategoryStruct.comp (Y :=
                    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
                      (F₂.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
                    (app (Iso.hom (Functor.commShiftIso F₂ b)) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
                    (Functor.map (shiftFunctor D b) (app (Iso.hom (Functor.commShiftIso F₂ a)) X) ≫
                      app (Iso.inv (shiftFunctorAdd D a b)) (F₂.obj X))))))
Tactic: simp only [Functor.commShiftIso_add, Functor.CommShift.isoAdd_hom_app,
      ← NatTrans.naturality_2 τ ((shiftFunctorAdd C a b).app X),
      Functor.comp_obj, hb.app_shift_assoc, ha.app_shift, assoc,
      (shiftFunctor D b).map_comp_assoc]