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

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, 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✝ : F.CommShift A
Y : D
h : -a + a = 0
⊢ adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫
      G.map ((shiftFunctorCompIsoId D (-a) a ⋯).inv.app (F.obj ((shiftFunctor C a).obj (G.obj Y)))) ≫
        G.map ((shiftFunctor D a).map ((F.commShiftIso (-a)).inv.app ((shiftFunctor C a).obj (G.obj Y)))) ≫
          G.map ((shiftFunctor D a).map ((F.commShiftIso (-a)).hom.app ((shiftFunctor C a).obj (G.obj Y)))) ≫
            G.map ((shiftFunctor D a).map ((shiftFunctor D (-a)).map ((F.commShiftIso a).hom.app (G.obj Y)))) ≫
              G.map ((shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj Y)))) ≫
                G.map ((shiftFunctor D a).map (adj.counit.app Y)) =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫
      G.map ((shiftFunctorCompIsoId D (-a) a h).inv.app (F.obj ((shiftFunctor C a).obj (G.obj Y)))) ≫
        G.map ((shiftFunctor D a).map ((shiftFunctor D (-a)).map ((F.commShiftIso a).hom.app (G.obj Y)))) ≫
          G.map ((shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj Y)))) ≫
            G.map ((shiftFunctor D a).map (adj.counit.app Y))

Tactic:
slice_lhs 3 4 => rw [← Functor.map_comp, ← Functor.map_comp, Iso.inv_hom_id_app]

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, 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✝ : F.CommShift A
Y : D
h : -a + a = 0
⊢ adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫
      G.map ((shiftFunctorCompIsoId D (-a) a ⋯).inv.app (F.obj ((shiftFunctor C a).obj (G.obj Y)))) ≫
        ((G.map ((shiftFunctor D a).map (𝟙 ((F ⋙ shiftFunctor D (-a)).obj ((shiftFunctor C a).obj (G.obj Y))))) ≫
              G.map ((shiftFunctor D a).map ((shiftFunctor D (-a)).map ((F.commShiftIso a).hom.app (G.obj Y))))) ≫
            G.map ((shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj Y))))) ≫
          G.map ((shiftFunctor D a).map (adj.counit.app Y)) =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫
      G.map ((shiftFunctorCompIsoId D (-a) a h).inv.app (F.obj ((shiftFunctor C a).obj (G.obj Y)))) ≫
        G.map ((shiftFunctor D a).map ((shiftFunctor D (-a)).map ((F.commShiftIso a).hom.app (G.obj Y)))) ≫
          G.map ((shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj Y)))) ≫
            G.map ((shiftFunctor D a).map (adj.counit.app Y))

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, 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 : b + a = 0
inst✝ : F.CommShift A
Y : D
⊢ b = -a

Tactic:
rw [← add_left_inj a, h, neg_add_cancel]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, 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 : b + a = 0
inst✝ : F.CommShift A
Y : D
⊢ (iso adj a).inv.app Y =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫
      G.map ((shiftFunctorCompIsoId D b a h).inv.app (F.obj ((shiftFunctor C a).obj (G.obj Y)))) ≫
        G.map ((shiftFunctor D a).map ((shiftFunctor D b).map ((F.commShiftIso a).hom.app (G.obj Y)))) ≫
          G.map ((shiftFunctor D a).map ((shiftFunctorCompIsoId D a b ⋯).hom.app (F.obj (G.obj Y)))) ≫
            G.map ((shiftFunctor D a).map (adj.counit.app Y))

Tactic:
obtain rfl : b = -a := by rw [← add_left_inj a, h, neg_add_cancel]

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, 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✝ : F.CommShift A
Y : D
h : -a + a = 0
⊢ (iso adj a).inv.app Y =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫
      G.map ((shiftFunctorCompIsoId D (-a) a h).inv.app (F.obj ((shiftFunctor C a).obj (G.obj Y)))) ≫
        G.map ((shiftFunctor D a).map ((shiftFunctor D (-a)).map ((F.commShiftIso a).hom.app (G.obj Y)))) ≫
          G.map ((shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj Y)))) ≫
            G.map ((shiftFunctor D a).map (adj.counit.app Y))

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, 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✝ : F.CommShift A
Y : D
h : -a + a = 0
⊢ (iso adj a).inv.app Y =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫
      G.map ((shiftFunctorCompIsoId D (-a) a h).inv.app (F.obj ((shiftFunctor C a).obj (G.obj Y)))) ≫
        G.map ((shiftFunctor D a).map ((shiftFunctor D (-a)).map ((F.commShiftIso a).hom.app (G.obj Y)))) ≫
          G.map ((shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj Y)))) ≫
            G.map ((shiftFunctor D a).map (adj.counit.app Y))

Tactic:
simp only [iso, iso', shiftEquiv', Equiv.toFun_as_coe, conjugateIsoEquiv_apply_inv,
  conjugateEquiv_apply_app, Functor.comp_obj, comp_unit_app, Functor.id_obj,
  Equivalence.toAdjunction_unit, Equivalence.Equivalence_mk'_unit, Iso.symm_hom, Functor.comp_map,
  comp_counit_app, Equivalence.toAdjunction_counit, Equivalence.Equivalence_mk'_counit,
  Functor.map_shiftFunctorCompIsoId_hom_app, assoc, Functor.map_comp]

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, 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✝ : F.CommShift A
Y : D
h : -a + a = 0
⊢ adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫
      G.map ((shiftFunctorCompIsoId D (-a) a ⋯).inv.app (F.obj ((shiftFunctor C a).obj (G.obj Y)))) ≫
        G.map ((shiftFunctor D a).map ((F.commShiftIso (-a)).inv.app ((shiftFunctor C a).obj (G.obj Y)))) ≫
          G.map ((shiftFunctor D a).map ((F.commShiftIso (-a)).hom.app ((shiftFunctor C a).obj (G.obj Y)))) ≫
            G.map ((shiftFunctor D a).map ((shiftFunctor D (-a)).map ((F.commShiftIso a).hom.app (G.obj Y)))) ≫
              G.map ((shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj Y)))) ≫
                G.map ((shiftFunctor D a).map (adj.counit.app Y)) =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫
      G.map ((shiftFunctorCompIsoId D (-a) a h).inv.app (F.obj ((shiftFunctor C a).obj (G.obj Y)))) ≫
        G.map ((shiftFunctor D a).map ((shiftFunctor D (-a)).map ((F.commShiftIso a).hom.app (G.obj Y)))) ≫
          G.map ((shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj Y)))) ≫
            G.map ((shiftFunctor D a).map (adj.counit.app Y))