Module: Mathlib.CategoryTheory.Shift.Pullback

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
inst✝³ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
D : Type u_4
inst✝² : Category.{v_2, u_4} D
inst✝¹ : HasShift D B
F : C ⥤ D
inst✝ : F.CommShift B
x✝² x✝¹ : A
x✝ : PullbackShift C φ
⊢ F.map ((pullbackShiftIso C φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝) ≫
      (commShiftIso F (φ (x✝² + x✝¹))).hom.app x✝ ≫
        (pullbackShiftIso D φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝) =
    F.map ((shiftFunctorAdd (PullbackShift C φ) x✝² x✝¹).hom.app x✝) ≫
      F.map ((pullbackShiftIso C φ x✝¹ (φ x✝¹) ⋯).hom.app ((shiftFunctor (PullbackShift C φ) x✝²).obj x✝)) ≫
        (commShiftIso F (φ x✝¹)).hom.app ((shiftFunctor (PullbackShift C φ) x✝²).obj x✝) ≫
          (pullbackShiftIso D φ x✝¹ (φ x✝¹) ⋯).inv.app (F.obj ((shiftFunctor (PullbackShift C φ) x✝²).obj x✝)) ≫
            (shiftFunctor (PullbackShift D φ) x✝¹).map (F.map ((pullbackShiftIso C φ x✝² (φ x✝²) ⋯).hom.app x✝)) ≫
              (shiftFunctor (PullbackShift D φ) x✝¹).map ((commShiftIso F (φ x✝²)).hom.app x✝) ≫
                (shiftFunctor (PullbackShift D φ) x✝¹).map ((pullbackShiftIso D φ x✝² (φ x✝²) ⋯).inv.app (F.obj x✝)) ≫
                  (shiftFunctorAdd (PullbackShift D φ) x✝² x✝¹).inv.app (F.obj x✝)

Tactic:
rw [F.commShiftIso_add' (φ.map_add _ _).symm,
      ← shiftFunctorAdd'_eq_shiftFunctorAdd, ← shiftFunctorAdd'_eq_shiftFunctorAdd,
      pullbackShiftFunctorAdd'_hom_app φ _ _ _ _ rfl _ _ _ rfl rfl rfl,
      pullbackShiftFunctorAdd'_inv_app φ _ _ _ _ rfl _ _ _ rfl rfl rfl]

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
inst✝³ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
D : Type u_4
inst✝² : Category.{v_2, u_4} D
inst✝¹ : HasShift D B
F : C ⥤ D
inst✝ : F.CommShift B
x✝² x✝¹ : A
x✝ : PullbackShift C φ
⊢ F.map ((pullbackShiftIso C φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝) ≫
      (CommShift.isoAdd' ⋯ (commShiftIso F (φ x✝²)) (commShiftIso F (φ x✝¹))).hom.app x✝ ≫
        (pullbackShiftIso D φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝) =
    F.map
        ((pullbackShiftIso C φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝ ≫
          (shiftFunctorAdd' C (φ x✝²) (φ x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝ ≫
            (pullbackShiftIso C φ x✝¹ (φ x✝¹) ⋯).inv.app ((shiftFunctor C (φ x✝²)).obj x✝) ≫
              (shiftFunctor (PullbackShift C φ) x✝¹).map ((pullbackShiftIso C φ x✝² (φ x✝²) ⋯).inv.app x✝)) ≫
      F.map ((pullbackShiftIso C φ x✝¹ (φ x✝¹) ⋯).hom.app ((shiftFunctor (PullbackShift C φ) x✝²).obj x✝)) ≫
        (commShiftIso F (φ x✝¹)).hom.app ((shiftFunctor (PullbackShift C φ) x✝²).obj x✝) ≫
          (pullbackShiftIso D φ x✝¹ (φ x✝¹) ⋯).inv.app (F.obj ((shiftFunctor (PullbackShift C φ) x✝²).obj x✝)) ≫
            (shiftFunctor (PullbackShift D φ) x✝¹).map (F.map ((pullbackShiftIso C φ x✝² (φ x✝²) ⋯).hom.app x✝)) ≫
              (shiftFunctor (PullbackShift D φ) x✝¹).map ((commShiftIso F (φ x✝²)).hom.app x✝) ≫
                (shiftFunctor (PullbackShift D φ) x✝¹).map ((pullbackShiftIso D φ x✝² (φ x✝²) ⋯).inv.app (F.obj x✝)) ≫
                  (shiftFunctor (PullbackShift D φ) x✝¹).map ((pullbackShiftIso D φ x✝² (φ x✝²) ⋯).hom.app (F.obj x✝)) ≫
                    (pullbackShiftIso D φ x✝¹ (φ x✝¹) ⋯).hom.app ((shiftFunctor D (φ x✝²)).obj (F.obj x✝)) ≫
                      (shiftFunctorAdd' D (φ x✝²) (φ x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝) ≫
                        (pullbackShiftIso D φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝)