-- Mathlib/CategoryTheory/Shift/Adjunction.lean
@[reassoc]
lemma iso_hom_app (X : D) :
    (iso adj a).hom.app X =
      (shiftFunctorCompIsoId C b a h).inv.app (G.obj ((shiftFunctor D a).obj X)) ≫
        (adj.unit.app ((shiftFunctor C b).obj (G.obj ((shiftFunctor D a).obj X))))⟦a⟧' ≫
          (G.map ((F.commShiftIso b).hom.app (G.obj ((shiftFunctor D a).obj X))))⟦a⟧' ≫
            (G.map ((shiftFunctor D b).map (adj.counit.app ((shiftFunctor D a).obj X))))⟦a⟧' ≫
              (G.map ((shiftFunctorCompIsoId D a b
                (by rw [← add_left_inj a, add_assoc, h, zero_add, add_zero])).hom.app X))⟦a⟧'

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{?u.170007, u_1} C
inst✝⁴ : Category.{?u.170011, 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
X : D
⊢ a + b = 0

Tactic:
rw [← add_left_inj a, add_assoc, h, zero_add, add_zero]

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
X : D
⊢ (iso adj a).hom.app X =
    (shiftFunctorCompIsoId C b a h).inv.app (G.obj ((shiftFunctor D a).obj X)) ≫
      (shiftFunctor C a).map (adj.unit.app ((shiftFunctor C b).obj (G.obj ((shiftFunctor D a).obj X)))) ≫
        (shiftFunctor C a).map (G.map ((F.commShiftIso b).hom.app (G.obj ((shiftFunctor D a).obj X)))) ≫
          (shiftFunctor C a).map (G.map ((shiftFunctor D b).map (adj.counit.app ((shiftFunctor D a).obj X)))) ≫
            (shiftFunctor C a).map (G.map ((shiftFunctorCompIsoId D a b ⋯).hom.app X))

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
X : D
h : -a + a = 0
⊢ (iso adj a).hom.app X =
    (shiftFunctorCompIsoId C (-a) a h).inv.app (G.obj ((shiftFunctor D a).obj X)) ≫
      (shiftFunctor C a).map (adj.unit.app ((shiftFunctor C (-a)).obj (G.obj ((shiftFunctor D a).obj X)))) ≫
        (shiftFunctor C a).map (G.map ((F.commShiftIso (-a)).hom.app (G.obj ((shiftFunctor D a).obj X)))) ≫
          (shiftFunctor C a).map (G.map ((shiftFunctor D (-a)).map (adj.counit.app ((shiftFunctor D a).obj X)))) ≫
            (shiftFunctor C a).map (G.map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app X))

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
X : D
h : -a + a = 0
⊢ (iso adj a).hom.app X =
    (shiftFunctorCompIsoId C (-a) a h).inv.app (G.obj ((shiftFunctor D a).obj X)) ≫
      (shiftFunctor C a).map (adj.unit.app ((shiftFunctor C (-a)).obj (G.obj ((shiftFunctor D a).obj X)))) ≫
        (shiftFunctor C a).map (G.map ((F.commShiftIso (-a)).hom.app (G.obj ((shiftFunctor D a).obj X)))) ≫
          (shiftFunctor C a).map (G.map ((shiftFunctor D (-a)).map (adj.counit.app ((shiftFunctor D a).obj X)))) ≫
            (shiftFunctor C a).map (G.map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app X))

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

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
X : D
⊢ b = -a

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

Result:
no goals