awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} 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 :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      G.obj
        (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
          (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))))
    (Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      f₂.inv.app (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
    (adj.unit.app
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
a₁ : G.map (𝟙 (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a ⋙ shiftFunctor D b) (F.obj X)))
| G.map (NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X)) ≫
    G.map (NatTrans.app (Iso.hom (shiftFunctorAdd D a b)) (F.obj X))

Tactic:
rw [← G.map_comp, Iso.inv_hom_id_app]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} 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 :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      G.obj
        (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
          (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))))
    (Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      f₂.inv.app (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
    (adj.unit.app
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
slice_rhs :
  Functor.map (shiftFunctor C (a + b)) (adj.unit.app X) =
    NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      adj.unit.app
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
          G.map (Functor.map (shiftFunctor D b) (e₁.hom.app X)) ≫
            ((G.map (𝟙 (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a ⋙ shiftFunctor D b) (F.obj X))) ≫
                  f₂.hom.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))) ≫
                Functor.map (shiftFunctor C b) (e₂.hom.app (F.obj X))) ≫
              NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) (G.obj (F.obj X))
⊢ Functor.map (shiftFunctor C (a + b)) (adj.unit.app X) =
    NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      adj.unit.app
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
          G.map (Functor.map (shiftFunctor D b) (e₁.hom.app X)) ≫
            G.map (NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X)) ≫
              G.map (NatTrans.app (Iso.hom (shiftFunctorAdd D a b)) (F.obj X)) ≫
                f₂.hom.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)) ≫
                  Functor.map (shiftFunctor C b) (e₂.hom.app (F.obj X)) ≫
                    NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) (G.obj (F.obj X))

Tactic:
slice_rhs 5 6 => rw [← G.map_comp, Iso.inv_hom_id_app]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} 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 :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      G.obj
        (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
          (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))))
    (Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      f₂.inv.app (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
    (adj.unit.app
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
simp :
  Functor.map (shiftFunctor C (a + b)) (adj.unit.app X) =
    NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      adj.unit.app
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
          G.map (Functor.map (shiftFunctor D b) (e₁.hom.app X)) ≫
            f₂.hom.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)) ≫
              Functor.map (shiftFunctor C b) (e₂.hom.app (F.obj X)) ≫
                NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) (G.obj (F.obj X))
⊢ Functor.map (shiftFunctor C (a + b)) (adj.unit.app X) =
    NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      adj.unit.app
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
          G.map (Functor.map (shiftFunctor D b) (e₁.hom.app X)) ≫
            ((G.map (𝟙 (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a ⋙ shiftFunctor D b) (F.obj X))) ≫
                  f₂.hom.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))) ≫
                Functor.map (shiftFunctor C b) (e₂.hom.app (F.obj X))) ≫
              NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) (G.obj (F.obj X))

Tactic:
simp only [Functor.comp_obj, Functor.map_id, id_comp, assoc]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Functor.map_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} 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 :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      G.obj
        (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
          (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))))
    (Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      f₂.inv.app (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
    (adj.unit.app
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
erw :
  Functor.map (shiftFunctor C (a + b)) (adj.unit.app X) =
    NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      adj.unit.app
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
          f₂.hom.app (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
            (G ⋙ shiftFunctor C b).map (e₁.hom.app X) ≫
              Functor.map (shiftFunctor C b) (e₂.hom.app (F.obj X)) ≫
                NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) (G.obj (F.obj X))
⊢ Functor.map (shiftFunctor C (a + b)) (adj.unit.app X) =
    NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      adj.unit.app
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
          G.map (Functor.map (shiftFunctor D b) (e₁.hom.app X)) ≫
            f₂.hom.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)) ≫
              Functor.map (shiftFunctor C b) (e₂.hom.app (F.obj X)) ≫
                NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) (G.obj (F.obj X))

Tactic:
erw [f₂.hom.naturality_assoc]

Premises used: CategoryTheory.Iso.hom, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} 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 :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      G.obj
        (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
          (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))))
    (Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      f₂.inv.app (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
    (adj.unit.app
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
rw :
  Functor.map (shiftFunctor C (a + b)) (adj.unit.app X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) (G.obj (F.obj X)) =
    NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        (G ⋙ shiftFunctor C b).map (e₁.hom.app X) ≫
          Functor.map (shiftFunctor C b) (e₂.hom.app (F.obj X)) ≫
            𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a ⋙ shiftFunctor C b) (G.obj (F.obj X)))
⊢ Functor.map (shiftFunctor C (a + b)) (adj.unit.app X) =
    NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      adj.unit.app
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
          f₂.hom.app (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
            (G ⋙ shiftFunctor C b).map (e₁.hom.app X) ≫
              Functor.map (shiftFunctor C b) (e₂.hom.app (F.obj X)) ≫
                NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) (G.obj (F.obj X))

Tactic:
rw [← reassoc_of% this, ← cancel_mono ((shiftFunctorAdd C a b).hom.app _),
    assoc, assoc, assoc, assoc, assoc, assoc, Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.shiftFunctorAdd, CategoryTheory.cancel_mono, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv_hom_id_app_assoc, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} 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 :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      G.obj
        (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
          (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))))
    (Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      f₂.inv.app (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
    (adj.unit.app
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
dsimp :
  Functor.map (shiftFunctor C (a + b)) (adj.unit.app X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) (G.obj (F.obj X)) =
    NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        Functor.map (shiftFunctor C b) (G.map (e₁.hom.app X)) ≫
          Functor.map (shiftFunctor C b) (e₂.hom.app (F.obj X)) ≫
            𝟙
              (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X))))
⊢ Functor.map (shiftFunctor C (a + b)) (adj.unit.app X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) (G.obj (F.obj X)) =
    NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        (G ⋙ shiftFunctor C b).map (e₁.hom.app X) ≫
          Functor.map (shiftFunctor C b) (e₂.hom.app (F.obj X)) ≫
            𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a ⋙ shiftFunctor C b) (G.obj (F.obj X)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} 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 :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      G.obj
        (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
          (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))))
    (Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      f₂.inv.app (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
    (adj.unit.app
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
rw :
  NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      Functor.map (shiftFunctor C a ⋙ shiftFunctor C b) (adj.unit.app X) =
    NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      Functor.map (shiftFunctor C b) (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
        𝟙
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X))))
⊢ Functor.map (shiftFunctor C (a + b)) (adj.unit.app X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) (G.obj (F.obj X)) =
    NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        Functor.map (shiftFunctor C b) (G.map (e₁.hom.app X)) ≫
          Functor.map (shiftFunctor C b) (e₂.hom.app (F.obj X)) ≫
            𝟙
              (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X))))

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.shiftFunctor, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} 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 :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      G.obj
        (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
          (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))))
    (Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      f₂.inv.app (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
    (adj.unit.app
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
dsimp :
  NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      Functor.map (shiftFunctor C b) (Functor.map (shiftFunctor C a) (adj.unit.app X)) =
    NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      Functor.map (shiftFunctor C b) (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
        𝟙
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X))))
⊢ NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      Functor.map (shiftFunctor C a ⋙ shiftFunctor C b) (adj.unit.app X) =
    NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      Functor.map (shiftFunctor C b) (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
        𝟙
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X))))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} 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 :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      G.obj
        (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
          (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))))
    (Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      f₂.inv.app (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
    (adj.unit.app
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
rw rw₁ :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X))))
    (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      Functor.map (shiftFunctor C b) (Functor.map (shiftFunctor C a) (adj.unit.app X)))
    (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      Functor.map (shiftFunctor C b) (Functor.map (shiftFunctor C a) (adj.unit.app X)))
⊢ NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      Functor.map (shiftFunctor C b) (Functor.map (shiftFunctor C a) (adj.unit.app X)) =
    NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      Functor.map (shiftFunctor C b) (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
        𝟙
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X))))

Tactic:
rw [comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
inst_6 : G.CommShift A
inst_7 : adj.CommShift A
a : A
X : C
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      ((F ⋙ G) ⋙ shiftFunctor C a).obj X)
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso (F ⋙ G) a)) X)
    (Functor.map (shiftFunctor C a) (adj.unit.app X))

Tactic:
simpa using (NatTrans.shift_app_comm adj.unit a X).symm

Premises used: CategoryTheory.Adjunction.unit, Eq.symm, CategoryTheory.NatTrans.shift_app_comm