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 : AddGroup 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 : G.CommShift A
a b : A
⊢ CommShift.CompatibilityUnit adj (Functor.CommShift.isoAdd (iso adj a) (iso adj b))
    (Functor.CommShift.isoAdd (Functor.commShiftIso G a) (Functor.commShiftIso G b))

Tactic:
exact CommShift.compatibilityUnit_isoAdd adj _ _ _ _
      (compatibilityUnit_iso adj a) (compatibilityUnit_iso adj b)

Premises used: CategoryTheory.Adjunction.LeftAdjointCommShift.compatibilityUnit_iso, CategoryTheory.Adjunction.CommShift.compatibilityUnit_isoAdd
-- 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 : AddGroup 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 : G.CommShift A
this : F.CommShift A := adj.leftAdjointCommShift A
⊢ adj.CommShift A

Tactic:
CommShift.mk' _ _ ⟨fun a ↦ ?_⟩

Premises used: CategoryTheory.Adjunction.CommShift.mk', CategoryTheory.NatTrans.CommShift.mk
-- 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 : AddGroup 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 : G.CommShift A
this : F.CommShift A := adj.leftAdjointCommShift A
refine :
  ∀ (a : A),
    Eq (α := shiftFunctor C a ⋙ 𝟭 C ⟶ (F ⋙ G) ⋙ shiftFunctor C a)
      (Iso.hom (Functor.commShiftIso (𝟭 C) a) ≫ Functor.whiskerRight adj.unit (shiftFunctor C a))
      (Functor.whiskerLeft (shiftFunctor C a) adj.unit ≫ Iso.hom (Functor.commShiftIso (F ⋙ G) a))
⊢ adj.CommShift A

Tactic:
refine CommShift.mk' _ _ ⟨fun a ↦ ?_⟩

Premises used: CategoryTheory.Adjunction.CommShift.mk', CategoryTheory.NatTrans.CommShift.mk
-- 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 : AddGroup 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 : G.CommShift A
this : F.CommShift A := adj.leftAdjointCommShift A
a : A
w :
  ∀ (X : C),
    Eq (α := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a ⋙ 𝟭 C) X ⟶ ((F ⋙ G) ⋙ shiftFunctor C a).obj X)
      (NatTrans.app (Iso.hom (Functor.commShiftIso (𝟭 C) a) ≫ Functor.whiskerRight adj.unit (shiftFunctor C a)) X)
      (NatTrans.app (Functor.whiskerLeft (shiftFunctor C a) adj.unit ≫ Iso.hom (Functor.commShiftIso (F ⋙ G) a)) X)
⊢ Eq (α := shiftFunctor C a ⋙ 𝟭 C ⟶ (F ⋙ G) ⋙ shiftFunctor C a)
    (Iso.hom (Functor.commShiftIso (𝟭 C) a) ≫ Functor.whiskerRight adj.unit (shiftFunctor C a))
    (Functor.whiskerLeft (shiftFunctor C a) adj.unit ≫ Iso.hom (Functor.commShiftIso (F ⋙ G) a))

Tactic:
ext X
-- 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 : AddGroup 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 : G.CommShift A
this : F.CommShift A := adj.leftAdjointCommShift A
a : A
X : C
w :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X)))
    (NatTrans.app (Iso.hom (Functor.commShiftIso (𝟭 C) a)) X ≫ Functor.map (shiftFunctor C a) (adj.unit.app X) :
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.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.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X)))
⊢ Eq (α := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a ⋙ 𝟭 C) X ⟶ ((F ⋙ G) ⋙ shiftFunctor C a).obj X)
    (NatTrans.app (Iso.hom (Functor.commShiftIso (𝟭 C) a) ≫ Functor.whiskerRight adj.unit (shiftFunctor C a)) X)
    (NatTrans.app (Functor.whiskerLeft (shiftFunctor C a) adj.unit ≫ Iso.hom (Functor.commShiftIso (F ⋙ G) a)) 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 : AddGroup 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 : G.CommShift A
this : F.CommShift A := adj.leftAdjointCommShift A
a : A
X : C
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X)))
    (NatTrans.app (Iso.hom (Functor.commShiftIso (𝟭 C) a)) X ≫ Functor.map (shiftFunctor C a) (adj.unit.app X) :
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.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.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X)))

Tactic:
simpa only [Functor.commShiftIso_id_hom_app, Functor.comp_obj, Functor.id_obj, id_comp,
    Functor.commShiftIso_comp_hom_app] using LeftAdjointCommShift.compatibilityUnit_iso adj a X

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.commShiftIso_comp_hom_app, CategoryTheory.Adjunction.LeftAdjointCommShift.compatibilityUnit_iso, CategoryTheory.Functor.commShiftIso_id_hom_app, CategoryTheory.Functor.id_obj, 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
E : Equivalence.{v_1, v_2, u_1, u_2} C D
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 : E.functor.CommShift A
inst_6 : E.inverse.CommShift A
inst_7 : E.CommShift A
⊢ NatTrans.CommShift E.unitIso.hom A

Tactic:
inferInstanceAs (NatTrans.CommShift E.toAdjunction.unit A)

Premises used: _private.0.CategoryTheory.Equivalence.CommShift.instCommShiftHomFunctorUnitIso._proof_1
-- 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
E : Equivalence.{v_1, v_2, u_1, u_2} C D
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 : E.functor.CommShift A
inst_6 : E.inverse.CommShift A
inst_7 : E.CommShift A
⊢ NatTrans.CommShift E.counitIso.hom A

Tactic:
inferInstanceAs (NatTrans.CommShift E.toAdjunction.counit A)

Premises used: _private.0.CategoryTheory.Equivalence.CommShift.instCommShiftHomFunctorCounitIso._proof_1
-- 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
E : Equivalence.{v_1, v_2, u_1, u_2} C D
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 : E.functor.CommShift A
inst_6 : E.inverse.CommShift A
⊢ CommShift.{v_1, u_1, v_1, u_1, u_3} (C := C) refl A

Tactic:
inferInstanceAs <| Adjunction.id.CommShift A

Premises used: _private.0.CategoryTheory.Equivalence.CommShift.instRefl._proof_1
-- 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
E : Equivalence.{v_1, v_2, u_1, u_2} C D
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 : E.functor.CommShift A
inst_6 : E.inverse.CommShift A
inst_7 : E.CommShift A
⊢ E.symm.CommShift A

Tactic:
mk' E.symm A (inferInstanceAs (NatTrans.CommShift E.counitIso.inv A))

Premises used: CategoryTheory.Equivalence.CommShift.mk', CategoryTheory.Equivalence.symm, _private.0.CategoryTheory.Equivalence.CommShift.instSymm._proof_1
-- 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
E : Equivalence.{v_1, v_2, u_1, u_2} C D
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 : E.functor.CommShift A
inst_6 : E.inverse.CommShift A
h : NatTrans.CommShift E.counitIso.hom A
⊢ E.CommShift A

Tactic:
have := mk' E.symm A (inferInstanceAs (NatTrans.CommShift E.counitIso.inv A))
  inferInstanceAs (E.symm.symm.CommShift A)

Premises used: CategoryTheory.Equivalence.CommShift.mk', _private.0.CategoryTheory.Equivalence.CommShift.mk''._proof_1, _private.0.CategoryTheory.Equivalence.CommShift.mk''._proof_2, CategoryTheory.Equivalence.symm
-- 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
E : Equivalence.{v_1, v_2, u_1, u_2} C D
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 : E.functor.CommShift A
inst_6 : E.inverse.CommShift A
F : Type u_4
inst_7 : Category.{v_3, u_4} F
inst_8 : HasShift.{v_3, u_4, u_3} F A
E' : Equivalence.{v_2, v_3, u_2, u_4} D F
inst_9 : E.CommShift A
inst_10 : E'.functor.CommShift A
inst_11 : E'.inverse.CommShift A
inst_12 : E'.CommShift A
⊢ (E.functor ⋙ E'.functor).CommShift A

Tactic:
infer_instance
-- 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
E : Equivalence.{v_1, v_2, u_1, u_2} C D
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 : E.functor.CommShift A
inst_6 : E.inverse.CommShift A
F : Type u_4
inst_7 : Category.{v_3, u_4} F
inst_8 : HasShift.{v_3, u_4, u_3} F A
E' : Equivalence.{v_2, v_3, u_2, u_4} D F
inst_9 : E.CommShift A
inst_10 : E'.functor.CommShift A
inst_11 : E'.inverse.CommShift A
inst_12 : E'.CommShift A
⊢ (E'.inverse ⋙ E.inverse).CommShift A

Tactic:
infer_instance
-- 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
E : Equivalence.{v_1, v_2, u_1, u_2} C D
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 : E.functor.CommShift A
inst_6 : E.inverse.CommShift A
F : Type u_4
inst_7 : Category.{v_3, u_4} F
inst_8 : HasShift.{v_3, u_4, u_3} F A
E' : Equivalence.{v_2, v_3, u_2, u_4} D F
inst_9 : E.CommShift A
inst_10 : E'.functor.CommShift A
inst_11 : E'.inverse.CommShift A
inst_12 : E'.CommShift A
⊢ (E.trans E').CommShift A

Tactic:
inferInstanceAs ((E.toAdjunction.comp E'.toAdjunction).CommShift A)

Premises used: _private.0.CategoryTheory.Equivalence.CommShift.instTrans._proof_1
-- 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
E : Equivalence.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddGroup 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 : E.functor.CommShift A
this : E.inverse.CommShift A := E.commShiftInverse A
⊢ E.CommShift A

Tactic:
CommShift.mk' _ _ (E.toAdjunction.commShift_of_leftAdjoint A).commShift_unit

Premises used: CategoryTheory.Equivalence.CommShift.mk', CategoryTheory.Adjunction.CommShift.commShift_unit
-- 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
E : Equivalence.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddGroup 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 : E.functor.CommShift A
this : E.inverse.CommShift A := E.commShiftInverse A
⊢ E.CommShift A

Tactic:
exact CommShift.mk' _ _ (E.toAdjunction.commShift_of_leftAdjoint A).commShift_unit

Premises used: CategoryTheory.Equivalence.CommShift.mk', CategoryTheory.Adjunction.CommShift.commShift_unit
-- 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
E : Equivalence.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddGroup 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 : E.inverse.CommShift A
this : E.functor.CommShift A := E.commShiftFunctor A
⊢ E.symm.CommShift A

Tactic:
have := E.symm.commShift_of_functor A
-- 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
E : Equivalence.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddGroup 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 : E.inverse.CommShift A
this_1 : E.functor.CommShift A := E.commShiftFunctor A
this : E.symm.CommShift A
⊢ E.CommShift A

Tactic:
inferInstanceAs (E.symm.symm.CommShift A)

Premises used: _private.0.CategoryTheory.Equivalence.commShift_of_inverse._proof_1
-- 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
E : Equivalence.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddGroup 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 : E.inverse.CommShift A
this_1 : E.functor.CommShift A := E.commShiftFunctor A
this : E.symm.CommShift A
⊢ E.CommShift A

Tactic:
exact inferInstanceAs (E.symm.symm.CommShift A)
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
F : A → Functor.{v, v, u, u} C C
zero : F 0 ≅ 𝟭 C
add : (n m : A) → F (n + m) ≅ F n ⋙ F m
m₁ m₂ m₃ : A
X : C
rw rw₁ : (F (m₁ + (m₂ + m₃))).obj X = (F (m₁ + (m₂ + m₃))).obj X
⊢ (F (m₁ + m₂ + m₃)).obj X = (F (m₁ + (m₂ + m₃))).obj X

Tactic:
rw [add_assoc]

Premises used: add_assoc
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
F : A → Functor.{v, v, u, u} C C
zero : F 0 ≅ 𝟭 C
add : (n m : A) → F (n + m) ≅ F n ⋙ F m
assoc_hom_app :
  ∀ (m₁ m₂ m₃ : A) (X : C),
    NatTrans.app (Iso.hom (add (m₁ + m₂) m₃)) X ≫ (F m₃).map ((add m₁ m₂).hom.app X) =
      eqToHom ⋯ ≫ NatTrans.app (Iso.hom (add m₁ (m₂ + m₃))) X ≫ (add m₂ m₃).hom.app ((F m₁).obj X)
n : A
X : C
dsimp : (F (0 + n)).obj X = (F n).obj X
⊢ (F (0 + n)).obj X = (F n).obj (obj.{v, v, u, u} (𝟭 C) X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
F : A → Functor.{v, v, u, u} C C
zero : F 0 ≅ 𝟭 C
add : (n m : A) → F (n + m) ≅ F n ⋙ F m
assoc_hom_app :
  ∀ (m₁ m₂ m₃ : A) (X : C),
    NatTrans.app (Iso.hom (add (m₁ + m₂) m₃)) X ≫ (F m₃).map ((add m₁ m₂).hom.app X) =
      eqToHom ⋯ ≫ NatTrans.app (Iso.hom (add m₁ (m₂ + m₃))) X ≫ (add m₂ m₃).hom.app ((F m₁).obj X)
n : A
X : C
rw rw₁ : (F n).obj X = (F n).obj X
⊢ (F (0 + n)).obj X = (F n).obj X

Tactic:
rw [zero_add]

Premises used: zero_add
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
F : A → Functor.{v, v, u, u} C C
zero : F 0 ≅ 𝟭 C
add : (n m : A) → F (n + m) ≅ F n ⋙ F m
assoc_hom_app :
  ∀ (m₁ m₂ m₃ : A) (X : C),
    NatTrans.app (Iso.hom (add (m₁ + m₂) m₃)) X ≫ (F m₃).map ((add m₁ m₂).hom.app X) =
      eqToHom ⋯ ≫ NatTrans.app (Iso.hom (add m₁ (m₂ + m₃))) X ≫ (add m₂ m₃).hom.app ((F m₁).obj X)
zero_add_hom_app : ∀ (n : A) (X : C), NatTrans.app (Iso.hom (add 0 n)) X = eqToHom ⋯ ≫ (F n).map (zero.inv.app X)
n : A
X : C
dsimp : (F (n + 0)).obj X = (F n).obj X
⊢ (F (n + 0)).obj X = obj.{v, v, u, u} (𝟭 C) ((F n).obj X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
F : A → Functor.{v, v, u, u} C C
zero : F 0 ≅ 𝟭 C
add : (n m : A) → F (n + m) ≅ F n ⋙ F m
assoc_hom_app :
  ∀ (m₁ m₂ m₃ : A) (X : C),
    NatTrans.app (Iso.hom (add (m₁ + m₂) m₃)) X ≫ (F m₃).map ((add m₁ m₂).hom.app X) =
      eqToHom ⋯ ≫ NatTrans.app (Iso.hom (add m₁ (m₂ + m₃))) X ≫ (add m₂ m₃).hom.app ((F m₁).obj X)
zero_add_hom_app : ∀ (n : A) (X : C), NatTrans.app (Iso.hom (add 0 n)) X = eqToHom ⋯ ≫ (F n).map (zero.inv.app X)
n : A
X : C
rw rw₁ : (F n).obj X = (F n).obj X
⊢ (F (n + 0)).obj X = (F n).obj X

Tactic:
rw [add_zero]

Premises used: add_zero
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
m₁ m₂ m₃ : A
X : C
rw rw₁ : (h.F (m₁ + (m₂ + m₃))).obj X = (h.F (m₁ + (m₂ + m₃))).obj X
⊢ (h.F (m₁ + (m₂ + m₃))).obj X = (h.F (m₁ + m₂ + m₃)).obj X

Tactic:
rw [add_assoc]

Premises used: add_assoc
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
m₁ m₂ m₃ : A
X : C
rw :
  Eq.{v + 1} (α := (h.F m₃).obj ((h.F m₁ ⋙ h.F m₂).obj X) ⟶ (h.F m₃).obj ((h.F m₁ ⋙ h.F m₂).obj X))
    (𝟙 ((h.F m₃).obj ((h.F m₁ ⋙ h.F m₂).obj X))) (𝟙 ((h.F m₂ ⋙ h.F m₃).obj ((h.F m₁).obj X)))
⊢ (h.F m₃).map ((h.add m₁ m₂).inv.app X) ≫ NatTrans.app (Iso.inv (h.add (m₁ + m₂) m₃)) X =
    (h.add m₂ m₃).inv.app ((h.F m₁).obj X) ≫ NatTrans.app (Iso.inv (h.add m₁ (m₂ + m₃))) X ≫ eqToHom ⋯

Tactic:
rw [← cancel_mono ((h.add (m₁ + m₂) m₃).hom.app X ≫ (h.F m₃).map ((h.add m₁ m₂).hom.app X)),
    Category.assoc, Category.assoc, Category.assoc, Iso.inv_hom_id_app_assoc, ← Functor.map_comp,
    Iso.inv_hom_id_app, Functor.map_id, h.assoc_hom_app, eqToHom_trans_assoc, eqToHom_refl,
    Category.id_comp, Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShiftMkCore.F, CategoryTheory.eqToHom_refl, CategoryTheory.cancel_mono, CategoryTheory.Functor.map, HAdd.hAdd, CategoryTheory.Functor.map_id, CategoryTheory.ShiftMkCore.add, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.map_comp, CategoryTheory.ShiftMkCore.assoc_hom_app, CategoryTheory.eqToHom_trans_assoc, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv_hom_id_app_assoc, CategoryTheory.NatTrans.app, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
m₁ m₂ m₃ : A
X : C
⊢ Eq.{v + 1} (α := (h.F m₃).obj ((h.F m₁ ⋙ h.F m₂).obj X) ⟶ (h.F m₃).obj ((h.F m₁ ⋙ h.F m₂).obj X))
    (𝟙 ((h.F m₃).obj ((h.F m₁ ⋙ h.F m₂).obj X))) (𝟙 ((h.F m₂ ⋙ h.F m₃).obj ((h.F m₁).obj X)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
n : A
X : C
dsimp : (h.F n).obj X = (h.F (0 + n)).obj X
⊢ (h.F n).obj (obj.{v, v, u, u} (𝟭 C) X) = (h.F (0 + n)).obj X

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
n : A
X : C
rw rw₁ : (h.F n).obj X = (h.F n).obj X
⊢ (h.F n).obj X = (h.F (0 + n)).obj X

Tactic:
rw [zero_add]

Premises used: zero_add
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
n : A
X : C
rw :
  NatTrans.app (Iso.hom (h.add 0 n)) X ≫ NatTrans.app (Iso.inv (h.add 0 n)) X =
    NatTrans.app (Iso.hom (h.add 0 n)) X ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
rw₁ : 𝟙 ((h.F (0 + n)).obj X) = NatTrans.app (Iso.hom (h.add 0 n)) X ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
rw₂ :
  𝟙 ((h.F (0 + n)).obj X) = (eqToHom ⋯ ≫ (h.F n).map (h.zero.inv.app X)) ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
rw₃ : 𝟙 ((h.F (0 + n)).obj X) = eqToHom ⋯ ≫ (h.F n).map (h.zero.inv.app X) ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
rw₄ : 𝟙 ((h.F (0 + n)).obj X) = eqToHom ⋯ ≫ (h.F n).map (h.zero.inv.app X ≫ h.zero.hom.app X) ≫ eqToHom ⋯
rw₅ : 𝟙 ((h.F (0 + n)).obj X) = eqToHom ⋯ ≫ (h.F n).map (𝟙 (obj.{v, v, u, u} (𝟭 C) X)) ≫ eqToHom ⋯
rw₆ :
  Eq.{v + 1} (α := (h.F (0 + n)).obj X ⟶ (h.F (0 + n)).obj X) (𝟙 ((h.F (0 + n)).obj X))
    (eqToHom ⋯ ≫ 𝟙 ((h.F n).obj (obj.{v, v, u, u} (𝟭 C) X)) ≫ eqToHom ⋯)
rw₇ : Eq.{v + 1} (α := (h.F (0 + n)).obj X ⟶ (h.F (0 + n)).obj X) (𝟙 ((h.F (0 + n)).obj X)) (eqToHom ⋯ ≫ eqToHom ⋯)
rw₈ : Eq.{v + 1} (α := (h.F (0 + n)).obj X ⟶ (h.F (0 + n)).obj X) (𝟙 ((h.F (0 + n)).obj X)) (eqToHom ⋯)
rw₉ rw₁₀ :
  Eq.{v + 1} (α := (h.F (0 + n)).obj X ⟶ (h.F (0 + n)).obj X) (𝟙 ((h.F (0 + n)).obj X)) (𝟙 ((h.F (0 + n)).obj X))
⊢ NatTrans.app (Iso.inv (h.add 0 n)) X = (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯

Tactic:
rw [← cancel_epi ((h.add 0 n).hom.app X), Iso.hom_inv_id_app, h.zero_add_hom_app,
    Category.assoc, ← Functor.map_comp_assoc, Iso.inv_hom_id_app, Functor.map_id,
    Category.id_comp, eqToHom_trans, eqToHom_refl]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.eqToHom_refl, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_id, CategoryTheory.ShiftMkCore.add, CategoryTheory.ShiftMkCore.zero_add_hom_app, CategoryTheory.Iso.inv_hom_id_app, OfNat.ofNat, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app, CategoryTheory.eqToHom_trans, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
n : A
X : C
dsimp : (h.F n).obj X = (h.F (n + 0)).obj X
⊢ obj.{v, v, u, u} (𝟭 C) ((h.F n).obj X) = (h.F (n + 0)).obj X

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
n : A
X : C
rw rw₁ : (h.F n).obj X = (h.F n).obj X
⊢ (h.F n).obj X = (h.F (n + 0)).obj X

Tactic:
rw [add_zero]

Premises used: add_zero
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
n : A
X : C
rw :
  NatTrans.app (Iso.hom (h.add n 0)) X ≫ NatTrans.app (Iso.inv (h.add n 0)) X =
    NatTrans.app (Iso.hom (h.add n 0)) X ≫ h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
rw₁ : 𝟙 ((h.F (n + 0)).obj X) = NatTrans.app (Iso.hom (h.add n 0)) X ≫ h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
rw₂ :
  𝟙 ((h.F (n + 0)).obj X) = (eqToHom ⋯ ≫ h.zero.inv.app ((h.F n).obj X)) ≫ h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
rw₃ : 𝟙 ((h.F (n + 0)).obj X) = eqToHom ⋯ ≫ h.zero.inv.app ((h.F n).obj X) ≫ h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
rw₄ : Eq.{v + 1} (α := (h.F (n + 0)).obj X ⟶ (h.F (n + 0)).obj X) (𝟙 ((h.F (n + 0)).obj X)) (eqToHom ⋯ ≫ eqToHom ⋯)
rw₅ : Eq.{v + 1} (α := (h.F (n + 0)).obj X ⟶ (h.F (n + 0)).obj X) (𝟙 ((h.F (n + 0)).obj X)) (eqToHom ⋯)
rw₆ rw₇ :
  Eq.{v + 1} (α := (h.F (n + 0)).obj X ⟶ (h.F (n + 0)).obj X) (𝟙 ((h.F (n + 0)).obj X)) (𝟙 ((h.F (n + 0)).obj X))
⊢ NatTrans.app (Iso.inv (h.add n 0)) X = h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯

Tactic:
rw [← cancel_epi ((h.add n 0).hom.app X), Iso.hom_inv_id_app, h.add_zero_hom_app,
    Category.assoc, Iso.inv_hom_id_app_assoc, eqToHom_trans, eqToHom_refl]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShiftMkCore.add_zero_hom_app, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.eqToHom_refl, CategoryTheory.ShiftMkCore.add, OfNat.ofNat, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv_hom_id_app_assoc, CategoryTheory.NatTrans.app, CategoryTheory.eqToHom_trans