-- Mathlib/CategoryTheory/Shift/Adjunction.lean
/--
The commutation isomorphisms of `Adjunction.LeftAdjointCommShift.iso` are compatible with
the unit of the adjunction.
-/
lemma compatibilityUnit_iso (a : A) :
    CommShift.CompatibilityUnit adj (iso adj a) (G.commShiftIso 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✝ : G.CommShift A
a : A
X✝ : C
⊢ (shiftFunctor C a).map (adj.unit.app X✝) =
    (shiftFunctor C a).map (adj.unit.app X✝) ≫
      (shiftFunctor C a).map ((shiftFunctorCompIsoId C a (-a) ⋯).inv.app (G.obj (F.obj X✝))) ≫
        (shiftFunctor C a).map ((shiftFunctor C (-a)).map ((G.commShiftIso a).inv.app (F.obj X✝))) ≫
          (shiftFunctorCompIsoId C (-a) a ⋯).hom.app (G.obj ((shiftFunctor D a).obj (F.obj X✝))) ≫
            (G.commShiftIso a).hom.app (F.obj X✝)

Tactic:
rw [shift_shiftFunctorCompIsoId_inv_app, ← Functor.comp_map,
  (shiftFunctorCompIsoId C _ _ (neg_add_cancel a)).hom.naturality_assoc]

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

Tactic:
simp

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

Tactic:
simp only [Functor.id_obj, Functor.comp_obj, Functor.map_shiftFunctorCompIsoId_inv_app,
  Functor.map_comp, assoc, unit_naturality_assoc, right_triangle_components_assoc]

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

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

Tactic:
rw [LeftAdjointCommShift.iso_hom_app adj _ _ (add_neg_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✝ : G.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.map ((shiftFunctor C a).map (adj.unit.app X✝)) ≫
            F.map ((shiftFunctor C a).map (G.map ((shiftFunctorCompIsoId D a (-a) ⋯).inv.app (F.obj X✝)))) ≫
              F.map ((shiftFunctor C a).map ((G.commShiftIso (-a)).hom.app ((shiftFunctor D a).obj (F.obj X✝)))) ≫
                F.map ((shiftFunctorCompIsoId C (-a) a ⋯).hom.app (G.obj ((shiftFunctor D a).obj (F.obj X✝)))) ≫
                  adj.counit.app ((shiftFunctor D a).obj (F.obj X✝))) ≫
        (G.commShiftIso a).hom.app (F.obj X✝)