-- Mathlib/CategoryTheory/Shift/Pullback.lean
lemma pullbackShiftFunctorAdd'_inv_app :
    (shiftFunctorAdd' _ a₁ a₂ a₃ h).inv.app X =
      (shiftFunctor (PullbackShift C φ) a₂).map ((pullbackShiftIso C φ a₁ b₁ h₁).hom.app X) ≫
        (pullbackShiftIso C φ a₂ b₂ h₂).hom.app _ ≫
        (shiftFunctorAdd' C b₁ b₂ b₃ (by rw [h₁, h₂, h₃, ← h, φ.map_add])).inv.app X ≫
        (pullbackShiftIso C φ a₃ b₃ h₃).inv.app X

Proof state:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C 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₃
⊢ (shiftFunctorAdd' (PullbackShift C φ) a₁ a₂ a₃ h).inv.app X =
    (shiftFunctor (PullbackShift C φ) a₂).map ((pullbackShiftIso C φ a₁ b₁ h₁).hom.app X) ≫
      (pullbackShiftIso C φ a₂ b₂ h₂).hom.app ((shiftFunctor C b₁).obj X) ≫
        (shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app X ≫ (pullbackShiftIso C φ a₃ b₃ h₃).inv.app X

Tactic:
subst h₁ h₂ h

Result:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
a₁ a₂ : A
b₃ : B
h₃ : b₃ = φ (a₁ + a₂)
⊢ (shiftFunctorAdd' (PullbackShift C φ) a₁ a₂ (a₁ + a₂) ⋯).inv.app X =
    (shiftFunctor (PullbackShift C φ) a₂).map ((pullbackShiftIso C φ a₁ (φ a₁) ⋯).hom.app X) ≫
      (pullbackShiftIso C φ a₂ (φ a₂) ⋯).hom.app ((shiftFunctor C (φ a₁)).obj X) ≫
        (shiftFunctorAdd' C (φ a₁) (φ a₂) b₃ ⋯).inv.app X ≫ (pullbackShiftIso C φ (a₁ + a₂) b₃ h₃).inv.app X

Proof state:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
a₁ a₂ : A
b₃ : B
h₃ : b₃ = φ (a₁ + a₂)
⊢ (shiftFunctorAdd' (PullbackShift C φ) a₁ a₂ (a₁ + a₂) ⋯).inv.app X =
    (shiftFunctor (PullbackShift C φ) a₂).map ((pullbackShiftIso C φ a₁ (φ a₁) ⋯).hom.app X) ≫
      (pullbackShiftIso C φ a₂ (φ a₂) ⋯).hom.app ((shiftFunctor C (φ a₁)).obj X) ≫
        (shiftFunctorAdd' C (φ a₁) (φ a₂) b₃ ⋯).inv.app X ≫ (pullbackShiftIso C φ (a₁ + a₂) b₃ h₃).inv.app X

Tactic:
obtain rfl : b₃ = φ a₁ + φ a₂ := by rw [h₃, φ.map_add]

Result:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
a₁ a₂ : A
h₃ : φ a₁ + φ a₂ = φ (a₁ + a₂)
⊢ (shiftFunctorAdd' (PullbackShift C φ) a₁ a₂ (a₁ + a₂) ⋯).inv.app X =
    (shiftFunctor (PullbackShift C φ) a₂).map ((pullbackShiftIso C φ a₁ (φ a₁) ⋯).hom.app X) ≫
      (pullbackShiftIso C φ a₂ (φ a₂) ⋯).hom.app ((shiftFunctor C (φ a₁)).obj X) ≫
        (shiftFunctorAdd' C (φ a₁) (φ a₂) (φ a₁ + φ a₂) ⋯).inv.app X ≫
          (pullbackShiftIso C φ (a₁ + a₂) (φ a₁ + φ a₂) h₃).inv.app X

Proof state:
case e_a
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
a₁ a₂ : A
h₃ : φ a₁ + φ a₂ = φ (a₁ + a₂)
⊢ ((shiftMonoidalFunctor C B).map (eqToHom ⋯)).app X = (pullbackShiftIso C φ (a₁ + a₂) (φ a₁ + φ a₂) h₃).inv.app X

Tactic:
congr 2

Result:
case e_a.e_self
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
a₁ a₂ : A
h₃ : φ a₁ + φ a₂ = φ (a₁ + a₂)
⊢ (shiftMonoidalFunctor C B).map (eqToHom ⋯) = (pullbackShiftIso C φ (a₁ + a₂) (φ a₁ + φ a₂) h₃).inv