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✝) ≫
      F.map ((shiftFunctorAdd' (PullbackShift C φ) (φ x✝²) (φ x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝) ≫
        (commShiftIso F (φ x✝¹)).hom.app ((shiftFunctor (PullbackShift C φ) (φ x✝²)).obj x✝) ≫
          (shiftFunctor (PullbackShift D φ) (φ x✝¹)).map ((commShiftIso F (φ x✝²)).hom.app x✝) ≫
            (shiftFunctorAdd' (PullbackShift D φ) (φ x✝²) (φ x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝) ≫
              (pullbackShiftIso D φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝) =
    F.map ((pullbackShiftIso C φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝) ≫
      F.map ((shiftFunctorAdd' C (φ x✝²) (φ x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝) ≫
        F.map ((pullbackShiftIso C φ x✝¹ (φ x✝¹) ⋯).inv.app ((shiftFunctor C (φ x✝²)).obj x✝)) ≫
          F.map ((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✝)) ≫
              (shiftFunctor C (φ x✝¹) ⋙ F).map ((pullbackShiftIso C φ x✝² (φ x✝²) ⋯).hom.app x✝) ≫
                (commShiftIso F (φ x✝¹)).hom.app ((shiftFunctor C (φ x✝²)).obj x✝) ≫
                  (shiftFunctor D (φ x✝¹)).map ((commShiftIso F (φ x✝²)).hom.app x✝) ≫
                    (shiftFunctorAdd' D (φ x✝²) (φ x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝) ≫
                      (pullbackShiftIso D φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝)

Tactic:
slice_rhs 4 5 => rw [← map_comp, (pullbackShiftIso C φ _ _ rfl).hom.naturality, map_comp]

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✝) ≫
      F.map ((shiftFunctorAdd' (PullbackShift C φ) (φ x✝²) (φ x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝) ≫
        (commShiftIso F (φ x✝¹)).hom.app ((shiftFunctor (PullbackShift C φ) (φ x✝²)).obj x✝) ≫
          (shiftFunctor (PullbackShift D φ) (φ x✝¹)).map ((commShiftIso F (φ x✝²)).hom.app x✝) ≫
            (shiftFunctorAdd' (PullbackShift D φ) (φ x✝²) (φ x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝) ≫
              (pullbackShiftIso D φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝) =
    F.map ((pullbackShiftIso C φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝) ≫
      F.map ((shiftFunctorAdd' C (φ x✝²) (φ x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝) ≫
        F.map ((pullbackShiftIso C φ x✝¹ (φ x✝¹) ⋯).inv.app ((shiftFunctor C (φ x✝²)).obj x✝)) ≫
          (((((F.map ((pullbackShiftIso C φ x✝¹ (φ x✝¹) ⋯).hom.app ((shiftFunctor C (φ x✝²)).obj x✝)) ≫
                      F.map ((shiftFunctor C (φ x✝¹)).map ((pullbackShiftIso C φ x✝² (φ x✝²) ⋯).inv.app x✝))) ≫
                    (shiftFunctor C (φ x✝¹) ⋙ F).map ((pullbackShiftIso C φ x✝² (φ x✝²) ⋯).hom.app x✝)) ≫
                  (commShiftIso F (φ x✝¹)).hom.app ((shiftFunctor C (φ x✝²)).obj x✝)) ≫
                (shiftFunctor D (φ x✝¹)).map ((commShiftIso F (φ x✝²)).hom.app x✝)) ≫
              (shiftFunctorAdd' D (φ x✝²) (φ x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝)) ≫
            (pullbackShiftIso D φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝)