-- Mathlib/CategoryTheory/Shift/Adjunction.lean
/-- Given an adjunction `adj : F ⊣ G`, `a, b` in `A` and commutation isomorphisms
between shifts by `a` (resp. `b`) and `F` and `G`, if these commutation isomorphisms are
compatible with the unit of `adj`, then so are the commutation isomorphisms between shifts
by `a + b` and `F` and `G` constructed by `Functor.CommShift.isoAdd`.
-/
lemma compatibilityUnit_isoAdd (h : CompatibilityUnit adj e₁ e₂)
    (h' : CompatibilityUnit adj f₁ f₂) :
    CompatibilityUnit adj (Functor.CommShift.isoAdd e₁ f₁) (Functor.CommShift.isoAdd e₂ f₂)

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✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
f₁ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
f₂ : shiftFunctor D b ⋙ G ≅ G ⋙ shiftFunctor C b
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj f₁ f₂
X : C
this :
  (shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj X)) ≫ f₂.inv.app (F.obj ((shiftFunctor C a).obj X)) =
    adj.unit.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫ G.map (f₁.hom.app ((shiftFunctor C a).obj X))
⊢ (shiftFunctor C (a + b)).map (adj.unit.app X) ≫ (shiftFunctorAdd C a b).hom.app (G.obj (F.obj X)) =
    (shiftFunctorAdd C a b).hom.app X ≫
      (shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj X)) ≫
        (G ⋙ shiftFunctor C b).map (e₁.hom.app X) ≫
          (shiftFunctor C b).map (e₂.hom.app (F.obj X)) ≫
            𝟙 ((shiftFunctor C a ⋙ shiftFunctor C b).obj (G.obj (F.obj X)))

Tactic:
dsimp

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✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
f₁ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
f₂ : shiftFunctor D b ⋙ G ≅ G ⋙ shiftFunctor C b
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj f₁ f₂
X : C
this :
  (shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj X)) ≫ f₂.inv.app (F.obj ((shiftFunctor C a).obj X)) =
    adj.unit.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫ G.map (f₁.hom.app ((shiftFunctor C a).obj X))
⊢ (shiftFunctor C (a + b)).map (adj.unit.app X) ≫ (shiftFunctorAdd C a b).hom.app (G.obj (F.obj X)) =
    (shiftFunctorAdd C a b).hom.app X ≫
      (shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj X)) ≫
        (shiftFunctor C b).map (G.map (e₁.hom.app X)) ≫
          (shiftFunctor C b).map (e₂.hom.app (F.obj X)) ≫
            𝟙 ((shiftFunctor C b).obj ((shiftFunctor C a).obj (G.obj (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✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
f₁ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
f₂ : shiftFunctor D b ⋙ G ≅ G ⋙ shiftFunctor C b
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj f₁ f₂
X : C
this :
  (shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj X)) =
    adj.unit.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫
      G.map (f₁.hom.app ((shiftFunctor C a).obj X)) ≫ f₂.hom.app (F.obj ((shiftFunctor C a).obj X))
⊢ (shiftFunctor C (a + b)).map (adj.unit.app X) =
    adj.unit.app ((shiftFunctor C (a + b)).obj X) ≫
      G.map ((Functor.CommShift.isoAdd e₁ f₁).hom.app X) ≫ (Functor.CommShift.isoAdd e₂ f₂).hom.app (F.obj X)

Tactic:
simp only [← cancel_mono (f₂.inv.app _), assoc, Iso.hom_inv_id_app,
  Functor.id_obj, Functor.comp_obj, comp_id] at this

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✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
f₁ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
f₂ : shiftFunctor D b ⋙ G ≅ G ⋙ shiftFunctor C b
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj f₁ f₂
X : C
this :
  (shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj X)) ≫ f₂.inv.app (F.obj ((shiftFunctor C a).obj X)) =
    adj.unit.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫ G.map (f₁.hom.app ((shiftFunctor C a).obj X))
⊢ (shiftFunctor C (a + b)).map (adj.unit.app X) =
    adj.unit.app ((shiftFunctor C (a + b)).obj X) ≫
      G.map ((Functor.CommShift.isoAdd e₁ f₁).hom.app X) ≫ (Functor.CommShift.isoAdd e₂ f₂).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✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
f₁ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
f₂ : shiftFunctor D b ⋙ G ≅ G ⋙ shiftFunctor C b
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj f₁ f₂
X : C
this :
  (shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj X)) ≫ f₂.inv.app (F.obj ((shiftFunctor C a).obj X)) =
    adj.unit.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫ G.map (f₁.hom.app ((shiftFunctor C a).obj X))
⊢ (shiftFunctor C (a + b)).map (adj.unit.app X) ≫ (shiftFunctorAdd C a b).hom.app (G.obj (F.obj X)) =
    (shiftFunctorAdd C a b).hom.app X ≫
      (shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj X)) ≫
        (shiftFunctor C b).map (G.map (e₁.hom.app X)) ≫
          (shiftFunctor C b).map (e₂.hom.app (F.obj X)) ≫
            𝟙 ((shiftFunctor C b).obj ((shiftFunctor C a).obj (G.obj (F.obj X))))

Tactic:
rw [← (shiftFunctor C b).map_comp_assoc, ← (shiftFunctor C b).map_comp_assoc,
  assoc, ← h X, NatTrans.naturality]

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✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
f₁ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
f₂ : shiftFunctor D b ⋙ G ≅ G ⋙ shiftFunctor C b
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj f₁ f₂
X : C
this :
  (shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj X)) ≫ f₂.inv.app (F.obj ((shiftFunctor C a).obj X)) =
    adj.unit.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫ G.map (f₁.hom.app ((shiftFunctor C a).obj X))
⊢ (shiftFunctorAdd C a b).hom.app X ≫ (shiftFunctor C a ⋙ shiftFunctor C b).map (adj.unit.app X) =
    (shiftFunctorAdd C a b).hom.app X ≫
      (shiftFunctor C b).map ((shiftFunctor C a).map (adj.unit.app X)) ≫
        𝟙 ((shiftFunctor C b).obj ((shiftFunctor C a).obj (G.obj (F.obj X))))