-- Mathlib/CategoryTheory/Shift/Adjunction.lean
@[reassoc]
lemma iso_inv_app (Y : C) :
    (iso adj a).inv.app Y = (F.map ((shiftFunctorCompIsoId C a b h).inv.app Y))⟦a⟧' ≫
      (F.map ((adj.unit.app (Y⟦a⟧))⟦b⟧'))⟦a⟧' ≫ (F.map ((G.commShiftIso b).inv.app
        (F.obj (Y⟦a⟧))))⟦a⟧' ≫ (adj.counit.app ((F.obj (Y⟦a⟧))⟦b⟧))⟦a⟧' ≫
          (shiftFunctorCompIsoId D b a (by simp [eq_neg_of_add_eq_zero_left h])).hom.app
            (F.obj (Y⟦a⟧))

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Category.{u_4, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
a b : A
h : a + b = 0
inst✝ : G.CommShift A
Y : C
⊢ (iso adj a).inv.app Y =
    (shiftFunctor D a).map (F.map ((shiftFunctorCompIsoId C a b h).inv.app Y)) ≫
      (shiftFunctor D a).map (F.map ((shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj Y)))) ≫
        (shiftFunctor D a).map (F.map ((G.commShiftIso b).inv.app (F.obj ((shiftFunctor C a).obj Y)))) ≫
          (shiftFunctor D a).map (adj.counit.app ((shiftFunctor D b).obj (F.obj ((shiftFunctor C a).obj Y)))) ≫
            (shiftFunctorCompIsoId D b a ⋯).hom.app (F.obj ((shiftFunctor C a).obj Y))

Tactic:
obtain rfl : b = -a := eq_neg_of_add_eq_zero_right h

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Category.{u_4, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
a : A
inst✝ : G.CommShift A
Y : C
h : a + -a = 0
⊢ (iso adj a).inv.app Y =
    (shiftFunctor D a).map (F.map ((shiftFunctorCompIsoId C a (-a) h).inv.app Y)) ≫
      (shiftFunctor D a).map (F.map ((shiftFunctor C (-a)).map (adj.unit.app ((shiftFunctor C a).obj Y)))) ≫
        (shiftFunctor D a).map (F.map ((G.commShiftIso (-a)).inv.app (F.obj ((shiftFunctor C a).obj Y)))) ≫
          (shiftFunctor D a).map (adj.counit.app ((shiftFunctor D (-a)).obj (F.obj ((shiftFunctor C a).obj Y)))) ≫
            (shiftFunctorCompIsoId D (-a) a ⋯).hom.app (F.obj ((shiftFunctor C a).obj Y))

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Category.{u_4, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
a : A
inst✝ : G.CommShift A
Y : C
h : a + -a = 0
⊢ (iso adj a).inv.app Y =
    (shiftFunctor D a).map (F.map ((shiftFunctorCompIsoId C a (-a) h).inv.app Y)) ≫
      (shiftFunctor D a).map (F.map ((shiftFunctor C (-a)).map (adj.unit.app ((shiftFunctor C a).obj Y)))) ≫
        (shiftFunctor D a).map (F.map ((G.commShiftIso (-a)).inv.app (F.obj ((shiftFunctor C a).obj Y)))) ≫
          (shiftFunctor D a).map (adj.counit.app ((shiftFunctor D (-a)).obj (F.obj ((shiftFunctor C a).obj Y)))) ≫
            (shiftFunctorCompIsoId D (-a) a ⋯).hom.app (F.obj ((shiftFunctor C a).obj Y))

Tactic:
simp [iso, iso', shiftEquiv']

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{?u.239122, u_1} C
inst✝⁴ : Category.{?u.239126, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
a b : A
h : a + b = 0
inst✝ : G.CommShift A
Y : C
⊢ b + a = 0

Tactic:
simp [eq_neg_of_add_eq_zero_left h]

Result:
no goals