awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
A : Type w
inst_4 : AddMonoid A
inst_5 : HasShift.{v₁, u₁, w} C A
C₁ : Type u_1
C₂ : Type u_2
inst_6 : Category.{v_1, u_1} C₁
inst_7 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
M : Type u_3
inst_8 : AddMonoid M
inst_9 : HasShift.{v_1, u_1, u_3} C₁ M
inst_10 : HasShift.{v_2, u_2, u_3} C₂ M
inst_11 : Φ.functor (W₁ := W₁) (W₂ := W₂).CommShift M
D₁ : Type u_4
D₂ : Type u_5
inst_12 : Category.{v_3, u_4} D₁
inst_13 : Category.{v_4, u_5} D₂
L₁ : Functor.{v_1, v_3, u_1, u_4} C₁ D₁
inst_14 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_5} C₂ D₂
inst_15 : HasShift.{v_3, u_4, u_3} D₁ M
inst_16 : HasShift.{v_4, u_5, u_3} D₂ M
inst_17 : L₁.CommShift M
inst_18 : L₂.CommShift M
G : Functor.{v_3, v_4, u_4, u_5} D₁ D₂
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G
this : Lifting L₁ W₁ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂) G := Lifting.mk (W := W₁) e.symm
⊢ G.CommShift M

Tactic:
exact Functor.commShiftOfLocalization L₁ W₁ M (Φ.functor ⋙ L₂) G

Premises used: CategoryTheory.Functor.comp, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.Functor.commShiftOfLocalization
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C₁ M
inst_4 : HasShift.{v_2, u_2, u_3} C₂ M
inst_5 : Φ.functor (W₁ := W₁) (W₂ := W₂).CommShift M
D₁ : Type u_4
D₂ : Type u_5
inst_6 : Category.{v_3, u_4} D₁
inst_7 : Category.{v_4, u_5} D₂
L₁ : Functor.{v_1, v_3, u_1, u_4} C₁ D₁
inst_8 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_5} C₂ D₂
inst_9 : HasShift.{v_3, u_4, u_3} D₁ M
inst_10 : HasShift.{v_4, u_5, u_3} D₂ M
inst_11 : L₁.CommShift M
inst_12 : L₂.CommShift M
G : Functor.{v_3, v_4, u_4, u_5} D₁ D₂
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G
m : M
X : C₁
⊢ Eq (α := (shiftFunctor D₁ m ⋙ G).obj (L₁.obj X) ⟶ (G ⋙ shiftFunctor D₂ m).obj (L₁.obj X))
    (NatTrans.app (Iso.hom (Functor.commShiftIso G m)) (L₁.obj X))
    (CategoryStruct.comp (Y := G.obj ((shiftFunctor C₁ m ⋙ L₁).obj X))
      (G.map (NatTrans.app (Iso.inv (Functor.commShiftIso L₁ m)) X))
      (e.inv.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) X) ≫
        CategoryStruct.comp (Y := L₂.obj ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ shiftFunctor C₂ m).obj X))
          (L₂.map (NatTrans.app (Iso.hom (Functor.commShiftIso (Φ.functor (W₁ := W₁) (W₂ := W₂)) m)) X))
          (NatTrans.app (Iso.hom (Functor.commShiftIso L₂ m)) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ≫
            Functor.map (shiftFunctor D₂ m) (e.hom.app X))))

Tactic:
simp [Functor.commShiftOfLocalization_iso_hom_app,
    Functor.commShiftIso_comp_hom_app]

Premises used: CategoryTheory.Functor.commShiftIso_comp_hom_app, CategoryTheory.Functor.commShiftOfLocalization_iso_hom_app
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C₁ M
inst_4 : HasShift.{v_2, u_2, u_3} C₂ M
inst_5 : Φ.functor (W₁ := W₁) (W₂ := W₂).CommShift M
D₁ : Type u_4
D₂ : Type u_5
inst_6 : Category.{v_3, u_4} D₁
inst_7 : Category.{v_4, u_5} D₂
L₁ : Functor.{v_1, v_3, u_1, u_4} C₁ D₁
inst_8 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_5} C₂ D₂
inst_9 : HasShift.{v_3, u_4, u_3} D₁ M
inst_10 : HasShift.{v_4, u_5, u_3} D₂ M
inst_11 : L₁.CommShift M
inst_12 : L₂.CommShift M
G : Functor.{v_3, v_4, u_4, u_5} D₁ D₂
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G
m : M
X : C₁
⊢ Eq (α := (G ⋙ shiftFunctor D₂ m).obj (L₁.obj X) ⟶ (shiftFunctor D₁ m ⋙ G).obj (L₁.obj X))
    (NatTrans.app (Iso.inv (Functor.commShiftIso G m)) (L₁.obj X))
    (Functor.map (shiftFunctor D₂ m) (e.inv.app X) ≫
      CategoryStruct.comp (Y := (shiftFunctor C₂ m ⋙ L₂).obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X))
        (NatTrans.app (Iso.inv (Functor.commShiftIso L₂ m)) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X))
        (CategoryStruct.comp (Y := L₂.obj ((shiftFunctor C₁ m ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)).obj X))
          (L₂.map (NatTrans.app (Iso.inv (Functor.commShiftIso (Φ.functor (W₁ := W₁) (W₂ := W₂)) m)) X))
          (e.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) X) ≫
            G.map (NatTrans.app (Iso.hom (Functor.commShiftIso L₁ m)) X))))

Tactic:
simp [Functor.commShiftOfLocalization_iso_inv_app,
    Functor.commShiftIso_comp_inv_app]

Premises used: CategoryTheory.Functor.commShiftOfLocalization_iso_inv_app, CategoryTheory.Functor.commShiftIso_comp_inv_app
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C₁ M
inst_4 : HasShift.{v_2, u_2, u_3} C₂ M
inst_5 : Φ.functor (W₁ := W₁) (W₂ := W₂).CommShift M
D₁ : Type u_4
D₂ : Type u_5
inst_6 : Category.{v_3, u_4} D₁
inst_7 : Category.{v_4, u_5} D₂
L₁ : Functor.{v_1, v_3, u_1, u_4} C₁ D₁
inst_8 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_5} C₂ D₂
inst_9 : HasShift.{v_3, u_4, u_3} D₁ M
inst_10 : HasShift.{v_4, u_5, u_3} D₂ M
inst_11 : L₁.CommShift M
inst_12 : L₂.CommShift M
G : Functor.{v_3, v_4, u_4, u_5} D₁ D₂
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G
this : G.CommShift M := Φ.commShift (W₁ := W₁) (W₂ := W₂) M L₁ L₂ G e
⊢ NatTrans.CommShift e.hom M

Tactic:
⟨fun m ↦ ?_⟩

Premises used: CategoryTheory.NatTrans.CommShift.mk
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C₁ M
inst_4 : HasShift.{v_2, u_2, u_3} C₂ M
inst_5 : Φ.functor (W₁ := W₁) (W₂ := W₂).CommShift M
D₁ : Type u_4
D₂ : Type u_5
inst_6 : Category.{v_3, u_4} D₁
inst_7 : Category.{v_4, u_5} D₂
L₁ : Functor.{v_1, v_3, u_1, u_4} C₁ D₁
inst_8 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_5} C₂ D₂
inst_9 : HasShift.{v_3, u_4, u_3} D₁ M
inst_10 : HasShift.{v_4, u_5, u_3} D₂ M
inst_11 : L₁.CommShift M
inst_12 : L₂.CommShift M
G : Functor.{v_3, v_4, u_4, u_5} D₁ D₂
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G
this : G.CommShift M := Φ.commShift (W₁ := W₁) (W₂ := W₂) M L₁ L₂ G e
refine :
  ∀ (m : M),
    Eq (α := shiftFunctor C₁ m ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ⟶ (L₁ ⋙ G) ⋙ shiftFunctor D₂ m)
      (Iso.hom (Functor.commShiftIso (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂) m) ≫
        Functor.whiskerRight e.hom (shiftFunctor D₂ m))
      (Functor.whiskerLeft (shiftFunctor C₁ m) e.hom ≫ Iso.hom (Functor.commShiftIso (L₁ ⋙ G) m))
⊢ NatTrans.CommShift e.hom M

Tactic:
refine ⟨fun m ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C₁ M
inst_4 : HasShift.{v_2, u_2, u_3} C₂ M
inst_5 : Φ.functor (W₁ := W₁) (W₂ := W₂).CommShift M
D₁ : Type u_4
D₂ : Type u_5
inst_6 : Category.{v_3, u_4} D₁
inst_7 : Category.{v_4, u_5} D₂
L₁ : Functor.{v_1, v_3, u_1, u_4} C₁ D₁
inst_8 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_5} C₂ D₂
inst_9 : HasShift.{v_3, u_4, u_3} D₁ M
inst_10 : HasShift.{v_4, u_5, u_3} D₂ M
inst_11 : L₁.CommShift M
inst_12 : L₂.CommShift M
G : Functor.{v_3, v_4, u_4, u_5} D₁ D₂
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G
this : G.CommShift M := Φ.commShift (W₁ := W₁) (W₂ := W₂) M L₁ L₂ G e
m : M
w :
  ∀ (X : C₁),
    Eq (α := (shiftFunctor C₁ m ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).obj X ⟶ ((L₁ ⋙ G) ⋙ shiftFunctor D₂ m).obj X)
      (NatTrans.app
        (Iso.hom (Functor.commShiftIso (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂) m) ≫
          Functor.whiskerRight e.hom (shiftFunctor D₂ m))
        X)
      (NatTrans.app (Functor.whiskerLeft (shiftFunctor C₁ m) e.hom ≫ Iso.hom (Functor.commShiftIso (L₁ ⋙ G) m)) X)
⊢ Eq (α := shiftFunctor C₁ m ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ⟶ (L₁ ⋙ G) ⋙ shiftFunctor D₂ m)
    (Iso.hom (Functor.commShiftIso (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂) m) ≫
      Functor.whiskerRight e.hom (shiftFunctor D₂ m))
    (Functor.whiskerLeft (shiftFunctor C₁ m) e.hom ≫ Iso.hom (Functor.commShiftIso (L₁ ⋙ G) m))

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C₁ M
inst_4 : HasShift.{v_2, u_2, u_3} C₂ M
inst_5 : Φ.functor (W₁ := W₁) (W₂ := W₂).CommShift M
D₁ : Type u_4
D₂ : Type u_5
inst_6 : Category.{v_3, u_4} D₁
inst_7 : Category.{v_4, u_5} D₂
L₁ : Functor.{v_1, v_3, u_1, u_4} C₁ D₁
inst_8 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_5} C₂ D₂
inst_9 : HasShift.{v_3, u_4, u_3} D₁ M
inst_10 : HasShift.{v_4, u_5, u_3} D₂ M
inst_11 : L₁.CommShift M
inst_12 : L₂.CommShift M
G : Functor.{v_3, v_4, u_4, u_5} D₁ D₂
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G
this : G.CommShift M := Φ.commShift (W₁ := W₁) (W₂ := W₂) M L₁ L₂ G e
m : M
X : C₁
⊢ Eq (α := (shiftFunctor C₁ m ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).obj X ⟶ ((L₁ ⋙ G) ⋙ shiftFunctor D₂ m).obj X)
    (NatTrans.app
      (Iso.hom (Functor.commShiftIso (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂) m) ≫
        Functor.whiskerRight e.hom (shiftFunctor D₂ m))
      X)
    (NatTrans.app (Functor.whiskerLeft (shiftFunctor C₁ m) e.hom ≫ Iso.hom (Functor.commShiftIso (L₁ ⋙ G) m)) X)

Tactic:
simp [Functor.commShiftIso_comp_hom_app, commShift_iso_hom_app, ← Functor.map_comp_assoc]

Premises used: CategoryTheory.LocalizerMorphism.commShift_iso_hom_app, CategoryTheory.Functor.commShiftIso_comp_hom_app, CategoryTheory.Functor.map_comp_assoc
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
A : Type w
inst_4 : AddMonoid A
inst_5 : HasShift.{v₁, u₁, w} C A
C₁ : Type u_1
C₂ : Type u_2
inst_6 : Category.{v_1, u_1} C₁
inst_7 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
M : Type u_3
inst_8 : AddMonoid M
inst_9 : HasShift.{v_1, u_1, u_3} C₁ M
inst_10 : HasShift.{v_2, u_2, u_3} C₂ M
inst_11 : Φ.functor (W₁ := W₁) (W₂ := W₂).CommShift M
D₁ : Type u_4
D₂ : Type u_5
inst_12 : Category.{v_3, u_4} D₁
inst_13 : Category.{v_4, u_5} D₂
L₁ : Functor.{v_1, v_3, u_1, u_4} C₁ D₁
inst_14 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_5} C₂ D₂
inst_15 : HasShift.{v_3, u_4, u_3} D₁ M
inst_16 : HasShift.{v_4, u_5, u_3} D₂ M
inst_17 : L₁.CommShift M
inst_18 : L₂.CommShift M
inst_19 : W₁.IsCompatibleWithShift M
inst_20 : W₂.IsCompatibleWithShift M
inst_21 : L₂.IsLocalization W₂
⊢ NatTrans.CommShift (F₂ := W₁.Q ⋙ Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
    (Iso.hom
      (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))
    M

Tactic:
natTransCommShift_hom ..

Premises used: CategoryTheory.LocalizerMorphism.natTransCommShift_hom
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
m₁ m₂ m₃ : A
X : Cᵒᵖ
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₃)
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁ ⋙ shiftFunctor C m₂) (Opposite.unop X)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m₁ + m₂ + m₃)) (Opposite.unop X))
    (NatTrans.app (Iso.inv (shiftFunctorAdd C m₂ m₃))
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) (Opposite.unop X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯)) (Opposite.unop X))
    (Quiver.Hom.unop
      (eqToHom ⋯ ≫
        NatTrans.app (Iso.hom (Iso.symm (NatIso.op (shiftFunctorAdd C m₁ (m₂ + m₃))))) X ≫
          NatTrans.app (Iso.hom (Iso.symm (NatIso.op (shiftFunctorAdd C m₂ m₃))))
            (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.op (shiftFunctor C m₁)) X)))

Tactic:
simp [shiftFunctorAdd']

Premises used: CategoryTheory.shiftFunctorAdd'
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
n : A
X : Cᵒᵖ
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_2} C (A := A) 0 ⋙ shiftFunctor C n) (Opposite.unop X) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (0 + n)) (Opposite.unop X))
    (Functor.map (shiftFunctor C n) (NatTrans.app (Iso.hom (shiftFunctorZero C A)) (Opposite.unop X)) ≫ eqToHom ⋯)
    (Quiver.Hom.unop
      (eqToHom ⋯ ≫
        Functor.map (Functor.op (shiftFunctor C n))
          (NatTrans.app (Iso.inv (Iso.symm (NatIso.op (shiftFunctorZero C A)))) X)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
n : A
X : Cᵒᵖ
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n ⋙ shiftFunctor.{v_1, u_1, u_2} C (A := A) 0) (Opposite.unop X) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (n + 0)) (Opposite.unop X))
    (NatTrans.app (Iso.hom (shiftFunctorZero C A))
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (Opposite.unop X)) ≫
      eqToHom ⋯)
    (Quiver.Hom.unop
      (eqToHom ⋯ ≫
        NatTrans.app (Iso.inv (Iso.symm (NatIso.op (shiftFunctorZero C A))))
          (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.op (shiftFunctor C n)) X)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
inst_3 : HasZeroObject.{v_1, u_1} C
⊢ HasZeroObject.{v_1, u_1} Cᵒᵖ

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
inst_3 : Preadditive.{v_1, u_1} C
n : A
inst_4 : Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
change : Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.op (shiftFunctor C n))
⊢ Functor.Additive.{v_1, u_1, v_1, u_1} (C := OppositeShift.{v_1, u_1, u_2} C A)
    (shiftFunctor (OppositeShift.{v_1, u_1, u_2} C A) n)

Tactic:
change (shiftFunctor C n).op.Additive

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.Additive, CategoryTheory.shiftFunctor
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
inst_3 : Preadditive.{v_1, u_1} C
n : A
inst_4 : Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
⊢ Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.op (shiftFunctor C n))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
X : OppositeShift.{v_1, u_1, u_2} C A
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 (OppositeShift.{v_1, u_1, u_2} C A)) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_2} (OppositeShift.{v_1, u_1, u_2} C A) (A := A) 0) X)
    (NatTrans.app (Iso.inv (shiftFunctorZero (OppositeShift.{v_1, u_1, u_2} C A) A)) X)
    (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C A)) (Opposite.unop X)))

Tactic:
rfl

Premises used: Quiver.Hom.op, rfl
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
X : OppositeShift.{v_1, u_1, u_2} C A
rw :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_2} (OppositeShift.{v_1, u_1, u_2} C A) (A := A) 0) X) =
    𝟙 (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_2} C (A := A) 0) (Opposite.unop X)))
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_2} (OppositeShift.{v_1, u_1, u_2} C A) (A := A) 0) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 (OppositeShift.{v_1, u_1, u_2} C A)) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero (OppositeShift.{v_1, u_1, u_2} C A) A)) X)
    (Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorZero C A)) (Opposite.unop X)))

Tactic:
rw [← cancel_mono ((shiftFunctorZero (OppositeShift C A) A).inv.app X),
    Iso.hom_inv_id_app, oppositeShiftFunctorZero_inv_app, ← op_comp,
    Iso.hom_inv_id_app, op_id]

Premises used: CategoryTheory.op_comp, CategoryTheory.shiftFunctorZero, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.cancel_mono, CategoryTheory.oppositeShiftFunctorZero_inv_app, CategoryTheory.OppositeShift, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app, CategoryTheory.op_id
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
X : OppositeShift.{v_1, u_1, u_2} C A
⊢ 𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_2} (OppositeShift.{v_1, u_1, u_2} C A) (A := A) 0) X) =
    𝟙 (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_2} C (A := A) 0) (Opposite.unop X)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
X : OppositeShift.{v_1, u_1, u_2} C A
a b : A
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1}
        (shiftFunctor (OppositeShift.{v_1, u_1, u_2} C A) a ⋙ shiftFunctor (OppositeShift.{v_1, u_1, u_2} C A) b) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_2} C A) (a + b)) X)
    (NatTrans.app (Iso.inv (shiftFunctorAdd (OppositeShift.{v_1, u_1, u_2} C A) a b)) X)
    (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) (Opposite.unop X)))

Tactic:
rfl

Premises used: Quiver.Hom.op, rfl
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
X : OppositeShift.{v_1, u_1, u_2} C A
a b : A
rw :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_2} C A) (a + b)) X) =
    𝟙 (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) (Opposite.unop X)))
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_2} C A) (a + b)) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (shiftFunctor (OppositeShift.{v_1, u_1, u_2} C A) a ⋙ shiftFunctor (OppositeShift.{v_1, u_1, u_2} C A) b) X)
    (NatTrans.app (Iso.hom (shiftFunctorAdd (OppositeShift.{v_1, u_1, u_2} C A) a b)) X)
    (Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) (Opposite.unop X)))

Tactic:
rw [← cancel_mono ((shiftFunctorAdd (OppositeShift C A) a b).inv.app X),
    Iso.hom_inv_id_app, oppositeShiftFunctorAdd_inv_app, ← op_comp,
    Iso.hom_inv_id_app, op_id]

Premises used: CategoryTheory.op_comp, CategoryTheory.oppositeShiftFunctorAdd_inv_app, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.shiftFunctorAdd, CategoryTheory.cancel_mono, CategoryTheory.OppositeShift, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app, CategoryTheory.op_id
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
X : OppositeShift.{v_1, u_1, u_2} C A
a b : A
⊢ 𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_2} C A) (a + b)) X) =
    𝟙 (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) (Opposite.unop X)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
X : OppositeShift.{v_1, u_1, u_2} C A
a b c : A
h : a + b = c
subst :
  NatTrans.app (Iso.inv (shiftFunctorAdd' (OppositeShift.{v_1, u_1, u_2} C A) a b (a + b) ⋯)) X =
    Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b (a + b) ⋯)) (Opposite.unop X))
⊢ NatTrans.app (Iso.inv (shiftFunctorAdd' (OppositeShift.{v_1, u_1, u_2} C A) a b c h)) X =
    Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b c h)) (Opposite.unop X))

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
X : OppositeShift.{v_1, u_1, u_2} C A
a b : A
⊢ NatTrans.app (Iso.inv (shiftFunctorAdd' (OppositeShift.{v_1, u_1, u_2} C A) a b (a + b) ⋯)) X =
    Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b (a + b) ⋯)) (Opposite.unop X))

Tactic:
simp only [shiftFunctorAdd'_eq_shiftFunctorAdd, oppositeShiftFunctorAdd_inv_app]

Premises used: CategoryTheory.oppositeShiftFunctorAdd_inv_app, CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
X : OppositeShift.{v_1, u_1, u_2} C A
a b c : A
h : a + b = c
subst :
  NatTrans.app (Iso.hom (shiftFunctorAdd' (OppositeShift.{v_1, u_1, u_2} C A) a b (a + b) ⋯)) X =
    Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C a b (a + b) ⋯)) (Opposite.unop X))
⊢ NatTrans.app (Iso.hom (shiftFunctorAdd' (OppositeShift.{v_1, u_1, u_2} C A) a b c h)) X =
    Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C a b c h)) (Opposite.unop X))

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
X : OppositeShift.{v_1, u_1, u_2} C A
a b : A
⊢ NatTrans.app (Iso.hom (shiftFunctorAdd' (OppositeShift.{v_1, u_1, u_2} C A) a b (a + b) ⋯)) X =
    Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C a b (a + b) ⋯)) (Opposite.unop X))

Tactic:
simp only [shiftFunctorAdd'_eq_shiftFunctorAdd, oppositeShiftFunctorAdd_hom_app]

Premises used: CategoryTheory.oppositeShiftFunctorAdd_hom_app, CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd