-- Mathlib/CategoryTheory/Shift/Adjunction.lean
/--
The commutation isomorphisms of `Adjunction.RightAdjointCommShift.iso` are compatible with
the unit of the adjunction.
-/
lemma compatibilityUnit_iso (a : A) :
    CommShift.CompatibilityUnit adj (F.commShiftIso a) (iso adj a)

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
inst✝ : F.CommShift A
a : A
⊢ CommShift.CompatibilityUnit adj (F.commShiftIso a) (iso adj a)

Tactic:
intro

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
inst✝ : F.CommShift A
a : A
X✝ : C
⊢ (shiftFunctor C a).map (adj.unit.app X✝) =
    adj.unit.app ((shiftFunctor C a).obj X✝) ≫ G.map ((F.commShiftIso a).hom.app X✝) ≫ (iso adj a).hom.app (F.obj X✝)

Proof state:
case a
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
inst✝ : F.CommShift A
a : A
X✝ : C
⊢ (adj.homEquiv ((shiftFunctor C a).obj X✝) ((shiftFunctor D a).obj (F.obj X✝))).symm
      ((shiftFunctor C a).map (adj.unit.app X✝) ≫
        adj.unit.app ((shiftFunctor C a).obj (G.obj (F.obj X✝))) ≫
          G.map ((shiftFunctorCompIsoId D (-a) a ⋯).inv.app (F.obj ((shiftFunctor C a).obj (G.obj (F.obj X✝))))) ≫
            G.map ((shiftFunctor D a).map ((shiftFunctor D (-a)).map ((F.commShiftIso a).hom.app (G.obj (F.obj X✝))))) ≫
              G.map ((shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj (F.obj X✝))))) ≫
                G.map ((shiftFunctor D a).map (adj.counit.app (F.obj X✝)))) =
    (adj.homEquiv ((shiftFunctor C a).obj X✝) ((shiftFunctor D a).obj (F.obj X✝))).symm
      (adj.unit.app ((shiftFunctor C a).obj X✝) ≫
        G.map ((F.commShiftIso a).hom.app X✝) ≫ 𝟙 (G.obj ((shiftFunctor D a).obj (F.obj X✝))))

Tactic:
simp only [comp_id, homEquiv_counit, Functor.map_comp, assoc, counit_naturality,
  counit_naturality_assoc, left_triangle_components_assoc]

Result:
case a
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
inst✝ : F.CommShift A
a : A
X✝ : C
⊢ F.map ((shiftFunctor C a).map (adj.unit.app X✝)) ≫
      (shiftFunctorCompIsoId D (-a) a ⋯).inv.app (F.obj ((shiftFunctor C a).obj (G.obj (F.obj X✝)))) ≫
        (shiftFunctor D a).map ((shiftFunctor D (-a)).map ((F.commShiftIso a).hom.app (G.obj (F.obj X✝)))) ≫
          (shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj (F.obj X✝)))) ≫
            (shiftFunctor D a).map (adj.counit.app (F.obj X✝)) =
    (F.commShiftIso a).hom.app X✝

Proof state:
case a
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
inst✝ : F.CommShift A
a : A
X✝ : C
⊢ F.map ((shiftFunctor C a).map (adj.unit.app X✝)) ≫
      (F.commShiftIso a).hom.app (G.obj (F.obj X✝)) ≫
        (shiftFunctorCompIsoId D (-a) a ⋯).inv.app ((shiftFunctor D a).obj (F.obj (G.obj (F.obj X✝)))) ≫
          (shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj (F.obj X✝)))) ≫
            (shiftFunctor D a).map (adj.counit.app (F.obj X✝)) =
    (F.commShiftIso a).hom.app X✝

Tactic:
rw [shift_shiftFunctorCompIsoId_hom_app, Iso.inv_hom_id_app_assoc,
  Functor.commShiftIso_hom_naturality_assoc, ← Functor.map_comp,
  left_triangle_components, Functor.map_id, comp_id]

Result:
no goals

Proof state:
case a
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
inst✝ : F.CommShift A
a : A
X✝ : C
⊢ F.map ((shiftFunctor C a).map (adj.unit.app X✝)) ≫
      (shiftFunctorCompIsoId D (-a) a ⋯).inv.app (F.obj ((shiftFunctor C a).obj (G.obj (F.obj X✝)))) ≫
        (shiftFunctor D a).map ((shiftFunctor D (-a)).map ((F.commShiftIso a).hom.app (G.obj (F.obj X✝)))) ≫
          (shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj (F.obj X✝)))) ≫
            (shiftFunctor D a).map (adj.counit.app (F.obj X✝)) =
    (F.commShiftIso a).hom.app X✝

Tactic:
erw [← NatTrans.naturality_assoc]

Result:
case a
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
inst✝ : F.CommShift A
a : A
X✝ : C
⊢ F.map ((shiftFunctor C a).map (adj.unit.app X✝)) ≫
      (𝟭 D).map ((F.commShiftIso a).hom.app (G.obj (F.obj X✝))) ≫
        (shiftFunctorCompIsoId D (-a) a ⋯).inv.app ((shiftFunctor D a).obj (F.obj (G.obj (F.obj X✝)))) ≫
          (shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj (F.obj X✝)))) ≫
            (shiftFunctor D a).map (adj.counit.app (F.obj X✝)) =
    (F.commShiftIso 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
inst✝ : F.CommShift A
a : A
X✝ : C
⊢ (shiftFunctor C a).map (adj.unit.app X✝) =
    adj.unit.app ((shiftFunctor C a).obj X✝) ≫ G.map ((F.commShiftIso a).hom.app X✝) ≫ (iso adj a).hom.app (F.obj X✝)

Tactic:
rw [← cancel_mono ((RightAdjointCommShift.iso adj a).inv.app _), assoc, assoc,
  Iso.hom_inv_id_app, RightAdjointCommShift.iso_inv_app adj _ _ (neg_add_cancel a)]

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
inst✝ : F.CommShift A
a : A
X✝ : C
⊢ (shiftFunctor C a).map (adj.unit.app X✝) ≫
      adj.unit.app ((shiftFunctor C a).obj (G.obj (F.obj X✝))) ≫
        G.map ((shiftFunctorCompIsoId D (-a) a ⋯).inv.app (F.obj ((shiftFunctor C a).obj (G.obj (F.obj X✝))))) ≫
          G.map ((shiftFunctor D a).map ((shiftFunctor D (-a)).map ((F.commShiftIso a).hom.app (G.obj (F.obj X✝))))) ≫
            G.map ((shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj (F.obj X✝))))) ≫
              G.map ((shiftFunctor D a).map (adj.counit.app (F.obj X✝))) =
    adj.unit.app ((shiftFunctor C a).obj X✝) ≫
      G.map ((F.commShiftIso a).hom.app X✝) ≫ 𝟙 ((shiftFunctor D a ⋙ G).obj (F.obj X✝))