awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
a : A
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C a ⋙ shiftFunctor.{v, u, u_1} C (A := A) 0) X ⟶
      obj.{v, v, u, u} (shiftFunctor C a) X)
    (NatTrans.app (Iso.inv (shiftFunctorAdd' C a 0 a ⋯)) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C a) X))

Tactic:
simpa using NatTrans.congr_app (congr_arg Iso.inv (shiftFunctorAdd'_add_zero C a)) X

Premises used: CategoryTheory.shiftFunctorAdd'_add_zero, CategoryTheory.NatTrans.congr_app, congr_arg, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
a : A
X : C
dsimp : obj.{v, v, u, u} (shiftFunctor C a) X = obj.{v, v, u, u} (shiftFunctor C (a + 0)) X
⊢ obj.{v, v, u, u} (𝟭 C) (obj.{v, v, u, u} (shiftFunctor C a) X) = obj.{v, v, u, u} (shiftFunctor C (a + 0)) 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
inst_2 : HasShift.{v, u, u_1} C A
a : A
X : C
rw rw₁ : obj.{v, v, u, u} (shiftFunctor C a) X = obj.{v, v, u, u} (shiftFunctor C a) X
⊢ obj.{v, v, u, u} (shiftFunctor C a) X = obj.{v, v, u, u} (shiftFunctor C (a + 0)) 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
inst_2 : HasShift.{v, u, u_1} C A
a : A
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C a ⋙ shiftFunctor.{v, u, u_1} C (A := A) 0) X ⟶
      obj.{v, v, u, u} (shiftFunctor C (a + 0)) X)
    (NatTrans.app (Iso.inv (shiftFunctorAdd C a 0)) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C a) X) ≫ eqToHom ⋯)

Tactic:
simp [← shiftFunctorAdd'_add_zero_inv_app, shiftFunctorAdd']

Premises used: CategoryTheory.shiftFunctorAdd', CategoryTheory.shiftFunctorAdd'_add_zero_inv_app
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
X : C
rw : a₁ + a₂ + a₃ = a₁₂₃
rw₁ rw₂ : a₁₂₃ = a₁₂₃
⊢ a₁₂ + a₃ = a₁₂₃

Tactic:
rw [← h₁₂, h₁₂₃]
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
X : C
rw : a₁ + (a₂ + a₃) = a₁₂₃
rw₁ : a₁ + a₂ + a₃ = a₁₂₃
rw₂ rw₃ : a₁₂₃ = a₁₂₃
⊢ a₁ + a₂₃ = a₁₂₃

Tactic:
rw [← h₂₃, ← add_assoc, h₁₂₃]

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
inst_2 : HasShift.{v, u, u_1} C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C a₁₂₃) X ⟶
      obj.{v, v, u, u} (shiftFunctor C a₃) (obj.{v, v, u, u} (shiftFunctor C a₁ ⋙ shiftFunctor C a₂) X))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ ⋯)) X ≫
      map (shiftFunctor C a₃) (NatTrans.app (Iso.hom (shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂)) X))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ⋯)) X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃)) (obj.{v, v, u, u} (shiftFunctor C a₁) X))

Tactic:
simpa using NatTrans.congr_app (congr_arg Iso.hom
    (shiftFunctorAdd'_assoc C _ _ _ _ _ _ h₁₂ h₂₃ h₁₂₃)) X

Premises used: CategoryTheory.shiftFunctorAdd'_assoc, CategoryTheory.NatTrans.congr_app, congr_arg, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C a₃) (obj.{v, v, u, u} (shiftFunctor C a₁ ⋙ shiftFunctor C a₂) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C a₁₂₃) X)
    (map (shiftFunctor C a₃) (NatTrans.app (Iso.inv (shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂)) X) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ ⋯)) X)
    (NatTrans.app (Iso.inv (shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃)) (obj.{v, v, u, u} (shiftFunctor C a₁) X) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ⋯)) X)

Tactic:
simpa using NatTrans.congr_app (congr_arg Iso.inv
    (shiftFunctorAdd'_assoc C _ _ _ _ _ _ h₁₂ h₂₃ h₁₂₃)) X

Premises used: CategoryTheory.shiftFunctorAdd'_assoc, CategoryTheory.NatTrans.congr_app, congr_arg, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
a₁ a₂ a₃ : A
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C (a₁ + a₂ + a₃)) X ⟶
      obj.{v, v, u, u} (shiftFunctor C a₃) (obj.{v, v, u, u} (shiftFunctor C a₁ ⋙ shiftFunctor C a₂) X))
    (NatTrans.app (Iso.hom (shiftFunctorAdd C (a₁ + a₂) a₃)) X ≫
      map (shiftFunctor C a₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C a₁ a₂)) X))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯)) X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd C a₂ a₃)) (obj.{v, v, u, u} (shiftFunctor C a₁) X))

Tactic:
simpa using NatTrans.congr_app (congr_arg Iso.hom (shiftFunctorAdd_assoc C a₁ a₂ a₃)) X

Premises used: CategoryTheory.NatTrans.congr_app, congr_arg, CategoryTheory.shiftFunctorAdd_assoc, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
a₁ a₂ a₃ : A
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C a₃) (obj.{v, v, u, u} (shiftFunctor C a₁ ⋙ shiftFunctor C a₂) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C (a₁ + a₂ + a₃)) X)
    (map (shiftFunctor C a₃) (NatTrans.app (Iso.inv (shiftFunctorAdd C a₁ a₂)) X) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd C (a₁ + a₂) a₃)) X)
    (NatTrans.app (Iso.inv (shiftFunctorAdd C a₂ a₃)) (obj.{v, v, u, u} (shiftFunctor C a₁) X) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯)) X)

Tactic:
simpa using NatTrans.congr_app (congr_arg Iso.inv (shiftFunctorAdd_assoc C a₁ a₂ a₃)) X

Premises used: CategoryTheory.NatTrans.congr_app, congr_arg, CategoryTheory.shiftFunctorAdd_assoc, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
X Y : C
f : X ⟶ Y
i j : A
⊢ Eq (α :=
    obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) Y))
    (map (shiftFunctor C j) (map (shiftFunctor C i) f))
    (Iso.inv (shiftAdd X i j) ≫ map (shiftFunctor C (i + j)) f ≫ Iso.hom (shiftAdd Y i j))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
X Y : C
f : X ⟶ Y
symm :
  Eq (α :=
    obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) X ⟶
      obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) Y)
    (Iso.hom (shiftZero A X) ≫ f ≫ Iso.inv (shiftZero A Y)) (map (shiftFunctor.{v, u, u_1} C (A := A) 0) f)
⊢ Eq (α :=
    obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) X ⟶
      obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) Y)
    (map (shiftFunctor.{v, u, u_1} C (A := A) 0) f) (Iso.hom (shiftZero A X) ≫ f ≫ Iso.inv (shiftZero A Y))

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
X Y : C
f : X ⟶ Y
rw :
  Eq (α :=
    obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) X ⟶
      obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) Y)
    (NatTrans.app (Iso.hom (shiftFunctorZero C A)) X ≫ f ≫ NatTrans.app (Iso.inv (shiftFunctorZero C A)) Y)
    (map (shiftFunctor.{v, u, u_1} C (A := A) 0) f)
⊢ Eq (α :=
    obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) X ⟶
      obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) Y)
    (Iso.hom (shiftZero A X) ≫ f ≫ Iso.inv (shiftZero A Y)) (map (shiftFunctor.{v, u, u_1} C (A := A) 0) f)

Tactic:
rw [Iso.app_inv, Iso.app_hom]

Premises used: CategoryTheory.Iso.app_inv, CategoryTheory.Iso.app_hom
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
X Y : C
f : X ⟶ Y
⊢ Eq (α :=
    obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) X ⟶
      obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) Y)
    (NatTrans.app (Iso.hom (shiftFunctorZero C A)) X ≫ f ≫ NatTrans.app (Iso.inv (shiftFunctorZero C A)) Y)
    (map (shiftFunctor.{v, u, u_1} C (A := A) 0) f)

Tactic:
apply NatIso.naturality_2

Premises used: CategoryTheory.NatIso.naturality_2
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
i j : A
h : i + j = 0
rw : j + i + j = 0 + j
rw₁ : j + (i + j) = 0 + j
rw₂ : j + 0 = 0 + j
rw₃ : j + 0 = j
rw₄ rw₅ : j = j
⊢ j + i = 0

Tactic:
rw [← add_left_inj j, add_assoc, h, zero_add, add_zero]

Premises used: add_assoc, add_left_inj, zero_add, add_zero
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
i j : A
h : i + j = 0
X : C
dsimp : j + i = 0
⊢ (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := j : Discrete A } { as := i : Discrete A }).as =
    Discrete.as (MonoidalCategoryStruct.tensorUnit (Discrete A) (𝒞 := discreteCategory A))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
i j : A
h : i + j = 0
X : C
rw : j + i + j = 0 + j
rw₁ : j + (i + j) = 0 + j
rw₂ : j + 0 = 0 + j
rw₃ : j + 0 = j
rw₄ rw₅ : j = j
⊢ j + i = 0

Tactic:
rw [← add_left_inj j, add_assoc, h, zero_add, add_zero]

Premises used: add_assoc, add_left_inj, zero_add, add_zero
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X Y : C
f : X ⟶ Y
i : A
change : IsEquivalence.{v, v, u, u} (Equivalence.functor (shiftEquiv C i))
⊢ IsEquivalence.{v, v, u, u} (shiftFunctor C i)

Tactic:
change (shiftEquiv C i).functor.IsEquivalence

Premises used: CategoryTheory.Equivalence.functor, CategoryTheory.shiftEquiv, CategoryTheory.Functor.IsEquivalence
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X Y : C
f : X ⟶ Y
i : A
⊢ IsEquivalence.{v, v, u, u} (Equivalence.functor (shiftEquiv C i))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X Y : C
f : X ⟶ Y
i j : A
hij : i + j = 0
⊢ CategoryStruct.comp (Y := obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X)
      (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C i j hij)) X)
      (map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ NatTrans.app (Iso.hom (shiftFunctorCompIsoId C i j hij)) Y) =
    f

Tactic:
NatIso.naturality_1 (shiftFunctorCompIsoId C i j hij) f

Premises used: CategoryTheory.NatIso.naturality_1, CategoryTheory.shiftFunctorCompIsoId
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X Y : C
f : X ⟶ Y
i : A
⊢ Eq (α :=
    obj.{v, v, u, u} (shiftFunctor C (-i)) (obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C (-i)) (obj.{v, v, u, u} (shiftFunctor C i) Y))
    (map (shiftFunctor C (-i)) (map (shiftFunctor C i) f))
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C i (-i) ⋯)) X ≫
      f ≫ NatTrans.app (Iso.inv (shiftFunctorCompIsoId C i (-i) ⋯)) Y)

Tactic:
(NatIso.naturality_2 (shiftFunctorCompIsoId C i (-i) (add_neg_cancel i)) f).symm

Premises used: add_neg_cancel, CategoryTheory.NatIso.naturality_2, CategoryTheory.shiftFunctorCompIsoId, Eq.symm, Neg.neg
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X Y : C
f : X ⟶ Y
i : A
⊢ Eq (α :=
    obj.{v, v, u, u} (shiftFunctor C i) (obj.{v, v, u, u} (shiftFunctor C (-i)) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C i) (obj.{v, v, u, u} (shiftFunctor C (-i)) Y))
    (map (shiftFunctor C i) (map (shiftFunctor C (-i)) f))
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-i) i ⋯)) X ≫
      f ≫ NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-i) i ⋯)) Y)

Tactic:
(NatIso.naturality_2 (shiftFunctorCompIsoId C (-i) i (neg_add_cancel i)) f).symm

Premises used: neg_add_cancel, CategoryTheory.NatIso.naturality_2, CategoryTheory.shiftFunctorCompIsoId, Eq.symm, Neg.neg
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
n : A
X : C
⊢ map (shiftFunctor C n) (Iso.inv (shiftShiftNeg X n)) ≫
      Iso.hom (shiftNegShift (obj.{v, v, u, u} (shiftFunctor C n) X) n) =
    𝟙 (obj.{v, v, u, u} (shiftFunctor C n) X)

Tactic:
(shiftEquiv C n).functor_unitIso_comp X

Premises used: CategoryTheory.shiftFunctor, CategoryTheory.shiftEquiv, CategoryTheory.Equivalence.functor_unitIso_comp
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X_1 Y : C
f : X_1 ⟶ Y
n m : A
h : n + m = 0
X : C
rw : m + -m = 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := A) 0 0
⊢ m + n = 0

Tactic:
rw [← neg_eq_of_add_eq_zero_left h, add_neg_cancel]

Premises used: add_neg_cancel, neg_eq_of_add_eq_zero_left
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
n m : A
h : n + m = 0
X : C
dsimp :
  Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C n) (obj.{v, v, u, u} (shiftFunctor C m) (obj.{v, v, u, u} (shiftFunctor C n) X)) ⟶
      obj.{v, v, u, u} (shiftFunctor C n) X)
    (map (shiftFunctor C n)
      (NatTrans.app (Iso.inv (shiftFunctorAdd' C n m 0 h)) X ≫ NatTrans.app (Iso.hom (shiftFunctorZero C A)) X))
    (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n 0 ⋯)) (obj.{v, v, u, u} (shiftFunctor C n) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n) X))
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C n) (obj.{v, v, u, u} (shiftFunctor C n ⋙ shiftFunctor C m) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C n) (obj.{v, v, u, u} (𝟭 C) X))
    (map (shiftFunctor C n) (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C n m h)) X))
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C m n ⋯)) (obj.{v, v, u, u} (shiftFunctor C n) X))

Tactic:
dsimp [shiftFunctorCompIsoId]

Premises used: CategoryTheory.shiftFunctorCompIsoId
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
n m : A
h : n + m = 0
X : C
rw : m + -m = 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := A) 0 0
⊢ m + n = 0

Tactic:
rw [← neg_eq_of_add_eq_zero_left h, add_neg_cancel]

Premises used: add_neg_cancel, neg_eq_of_add_eq_zero_left
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
n m : A
h : n + m = 0
X : C
rw : 0 + n = n
rw₁ rw₂ : n = n
⊢ n + m + n = n

Tactic:
rw [h, 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 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
n m : A
h : n + m = 0
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C n) (obj.{v, v, u, u} (shiftFunctor C m) (obj.{v, v, u, u} (shiftFunctor C n) X)) ⟶
      obj.{v, v, u, u} (shiftFunctor C n) X)
    (map (shiftFunctor C n)
      (NatTrans.app (Iso.inv (shiftFunctorAdd' C n m 0 h)) X ≫ NatTrans.app (Iso.hom (shiftFunctorZero C A)) X))
    (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n 0 ⋯)) (obj.{v, v, u, u} (shiftFunctor C n) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n) X))

Tactic:
simpa only [Functor.map_comp, ← shiftFunctorAdd'_zero_add_inv_app n X,
    ← shiftFunctorAdd'_add_zero_inv_app n X]
    using shiftFunctorAdd'_assoc_inv_app n m n 0 0 n h
      (by rw [← neg_eq_of_add_eq_zero_left h, add_neg_cancel]) (by rw [h, zero_add]) X

Premises used: CategoryTheory.shiftFunctorAdd'_assoc_inv_app, CategoryTheory.shiftFunctorAdd'_zero_add_inv_app, CategoryTheory.shiftFunctorAdd'_add_zero_inv_app, CategoryTheory.Functor.map_comp, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
n m : A
h : n + m = 0
X : C
rw :
  Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C n) (obj.{v, v, u, u} (𝟭 C) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C n) (obj.{v, v, u, u} (𝟭 C) X))
    (𝟙 (obj.{v, v, u, u} (shiftFunctor C n) (obj.{v, v, u, u} (𝟭 C) X)))
    (𝟙 (obj.{v, v, u, u} (𝟭 C) (obj.{v, v, u, u} (shiftFunctor C n) X)))
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C n) (obj.{v, v, u, u} (𝟭 C) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C n) (obj.{v, v, u, u} (shiftFunctor C n ⋙ shiftFunctor C m) X))
    (map (shiftFunctor C n) (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C n m h)) X))
    (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C m n ⋯)) (obj.{v, v, u, u} (shiftFunctor C n) X))

Tactic:
rw [← cancel_mono (((shiftFunctorCompIsoId C n m h).hom.app X)⟦n⟧'),
    ← Functor.map_comp, Iso.inv_hom_id_app, Functor.map_id,
    shift_shiftFunctorCompIsoId_hom_app, Iso.inv_hom_id_app]

Premises used: CategoryTheory.shift_shiftFunctorCompIsoId_hom_app, CategoryTheory.shiftFunctor, CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.Functor.map_id, CategoryTheory.shiftFunctorCompIsoId, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
n m : A
h : n + m = 0
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C n) (obj.{v, v, u, u} (𝟭 C) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C n) (obj.{v, v, u, u} (𝟭 C) X))
    (𝟙 (obj.{v, v, u, u} (shiftFunctor C n) (obj.{v, v, u, u} (𝟭 C) X)))
    (𝟙 (obj.{v, v, u, u} (𝟭 C) (obj.{v, v, u, u} (shiftFunctor C n) X)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
n : A
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C n) (obj.{v, v, u, u} (shiftFunctor C n ⋙ shiftFunctor C (-n)) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C n) (obj.{v, v, u, u} (𝟭 C) X))
    (map (shiftFunctor C n) (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C n (-n) ⋯)) X))
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-n) n ⋯)) (obj.{v, v, u, u} (shiftFunctor C n) X))

Tactic:
apply shift_shiftFunctorCompIsoId_hom_app

Premises used: CategoryTheory.shift_shiftFunctorCompIsoId_hom_app
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
n : A
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C n) (obj.{v, v, u, u} (𝟭 C) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C n) (obj.{v, v, u, u} (shiftFunctor C n ⋙ shiftFunctor C (-n)) X))
    (map (shiftFunctor C n) (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C n (-n) ⋯)) X))
    (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-n) n ⋯)) (obj.{v, v, u, u} (shiftFunctor C n) X))

Tactic:
apply shift_shiftFunctorCompIsoId_inv_app

Premises used: CategoryTheory.shift_shiftFunctorCompIsoId_inv_app
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
n : A
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C (-n)) (obj.{v, v, u, u} (shiftFunctor C (-n) ⋙ shiftFunctor C n) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C (-n)) (obj.{v, v, u, u} (𝟭 C) X))
    (map (shiftFunctor C (-n)) (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-n) n ⋯)) X))
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C n (-n) ⋯)) (obj.{v, v, u, u} (shiftFunctor C (-n)) X))

Tactic:
apply shift_shiftFunctorCompIsoId_hom_app

Premises used: CategoryTheory.shift_shiftFunctorCompIsoId_hom_app
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
n : A
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C (-n)) (obj.{v, v, u, u} (𝟭 C) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C (-n)) (obj.{v, v, u, u} (shiftFunctor C (-n) ⋙ shiftFunctor C n) X))
    (map (shiftFunctor C (-n)) (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-n) n ⋯)) X))
    (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C n (-n) ⋯)) (obj.{v, v, u, u} (shiftFunctor C (-n)) X))

Tactic:
apply shift_shiftFunctorCompIsoId_inv_app

Premises used: CategoryTheory.shift_shiftFunctorCompIsoId_inv_app
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0 ⋙ shiftFunctor.{v, u, u_1} C (A := A) 0) X ⟶
      obj.{v, v, u, u} (𝟭 C) X)
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 0 0 ⋯)) X)
    (map (shiftFunctor.{v, u, u_1} C (A := A) 0) (NatTrans.app (Iso.hom (shiftFunctorZero C A)) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorZero C A)) X)

Tactic:
simp [shiftFunctorCompIsoId, shiftFunctorAdd'_zero_add_inv_app]

Premises used: CategoryTheory.shiftFunctorAdd'_zero_add_inv_app, CategoryTheory.shiftFunctorCompIsoId
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (𝟭 C) X ⟶
      obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0 ⋙ shiftFunctor.{v, u, u_1} C (A := A) 0) X)
    (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 0 0 ⋯)) X)
    (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X ≫
      map (shiftFunctor.{v, u, u_1} C (A := A) 0) (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X))

Tactic:
simp [shiftFunctorCompIsoId, shiftFunctorAdd'_zero_add_hom_app]

Premises used: CategoryTheory.shiftFunctorAdd'_zero_add_hom_app, CategoryTheory.shiftFunctorCompIsoId
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X Y : C
f : X ⟶ Y
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
rw : n' + m' + p = p' + p
rw₁ : n' + m' + p = 0
rw₂ : n' + m' + (m + n) = 0
rw₃ : n' + (m' + (m + n)) = 0
rw₄ : n' + (m' + m + n) = 0
rw₅ : n' + (0 + n) = 0
rw₆ : n' + n = 0
rw₇ rw₈ : Eq.{u_1 + 1} (α := A) 0 0
⊢ n' + m' = p'

Tactic:
rw [← add_left_inj p, hp, ← h, add_assoc,
          ← add_assoc m', hm, zero_add, hn]

Premises used: add_assoc, add_left_inj, zero_add