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 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
dsimp :
  Eq.{v + 1} (α := X ⟶ obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X))
    (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd' C p' p 0 hp)) X)
    ((NatTrans.app (Iso.inv (shiftFunctorZero C A)) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd' C n' n 0 hn)) X) ≫
      map (shiftFunctor C n)
          (NatTrans.app (Iso.inv (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n') X) ≫
            NatTrans.app (Iso.hom (shiftFunctorAdd' C m' m 0 hm)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
            (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
          map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X))
⊢ Eq.{v + 1} (α := obj.{v, v, u, u} (𝟭 C) X ⟶ obj.{v, v, u, u} (shiftFunctor C p' ⋙ shiftFunctor C p) X)
    (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C p' p hp)) X)
    (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C n' n hn)) X ≫
      CategoryStruct.comp (Y :=
        obj.{v, v, u, u} (shiftFunctor C n)
          (obj.{v, v, u, u} (shiftFunctor C m' ⋙ shiftFunctor C m) (obj.{v, v, u, u} (shiftFunctor C n') X)))
        (map (shiftFunctor C n)
            (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C m' m hm)) (obj.{v, v, u, u} (shiftFunctor C n') X)) :
          obj.{v, v, u, u} (shiftFunctor C n) (obj.{v, v, u, u} (shiftFunctor C n') X) ⟶
            obj.{v, v, u, u} (shiftFunctor C n)
              (obj.{v, v, u, u} (shiftFunctor C m' ⋙ shiftFunctor C m) (obj.{v, v, u, u} (shiftFunctor C n') X)))
        (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
              (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
            map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X) :
          obj.{v, v, u, u} (shiftFunctor C n)
              (obj.{v, v, u, u} (shiftFunctor C m' ⋙ shiftFunctor C m) (obj.{v, v, u, u} (shiftFunctor C n') X)) ⟶
            obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') 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
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
simp :
  Eq.{v + 1} (α := X ⟶ obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X))
    (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd' C p' p 0 hp)) X)
    (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C n' n 0 hn)) X ≫
        map (shiftFunctor C n)
            (NatTrans.app (Iso.inv (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
          map (shiftFunctor C n)
              (NatTrans.app (Iso.hom (shiftFunctorAdd' C m' m 0 hm)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
                (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
              map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X))
⊢ Eq.{v + 1} (α := X ⟶ obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X))
    (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd' C p' p 0 hp)) X)
    ((NatTrans.app (Iso.inv (shiftFunctorZero C A)) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd' C n' n 0 hn)) X) ≫
      map (shiftFunctor C n)
          (NatTrans.app (Iso.inv (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n') X) ≫
            NatTrans.app (Iso.hom (shiftFunctorAdd' C m' m 0 hm)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
            (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
          map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X))

Tactic:
simp only [Functor.map_comp, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_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 : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
e_a :
  Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) X ⟶
      obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C p' p 0 hp)) X)
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' n 0 hn)) X ≫
      map (shiftFunctor C n) (NatTrans.app (Iso.inv (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        map (shiftFunctor C n)
            (NatTrans.app (Iso.hom (shiftFunctorAdd' C m' m 0 hm)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
              (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
            map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X))
⊢ Eq.{v + 1} (α := X ⟶ obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X))
    (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd' C p' p 0 hp)) X)
    (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C n' n 0 hn)) X ≫
        map (shiftFunctor C n)
            (NatTrans.app (Iso.inv (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
          map (shiftFunctor C n)
              (NatTrans.app (Iso.hom (shiftFunctorAdd' C m' m 0 hm)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
                (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
              map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X))

Tactic:
congr 1
-- 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
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
e_a :
  Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) X ⟶
      obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C p' p 0 hp)) X)
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' n 0 hn)) X ≫
      map (shiftFunctor C n) (NatTrans.app (Iso.inv (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        map (shiftFunctor C n)
            (NatTrans.app (Iso.hom (shiftFunctorAdd' C m' m 0 hm)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
          map (shiftFunctor C m ⋙ shiftFunctor C n) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h)) (obj.{v, v, u, u} (shiftFunctor C p') X))
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) X ⟶
      obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C p' p 0 hp)) X)
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' n 0 hn)) X ≫
      map (shiftFunctor C n) (NatTrans.app (Iso.inv (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        map (shiftFunctor C n)
            (NatTrans.app (Iso.hom (shiftFunctorAdd' C m' m 0 hm)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
              (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
            map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X))

Tactic:
rw [← NatTrans.naturality]

Premises used: CategoryTheory.NatTrans.naturality
-- 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
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
e_a :
  Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) X ⟶
      obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C p' p 0 hp)) X)
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' n 0 hn)) X ≫
      CategoryStruct.comp (Y :=
        obj.{v, v, u, u} (shiftFunctor C n)
          (obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) (obj.{v, v, u, u} (shiftFunctor C n') X)))
        (map (shiftFunctor C n)
          (NatTrans.app (Iso.inv (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n') X)))
        (map (shiftFunctor C n)
            (NatTrans.app (Iso.hom (shiftFunctorAdd' C m' m 0 hm)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
          map (shiftFunctor C n) (map (shiftFunctor C m) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X)) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h)) (obj.{v, v, u, u} (shiftFunctor C p') X)))
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) X ⟶
      obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C p' p 0 hp)) X)
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' n 0 hn)) X ≫
      map (shiftFunctor C n) (NatTrans.app (Iso.inv (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        map (shiftFunctor C n)
            (NatTrans.app (Iso.hom (shiftFunctorAdd' C m' m 0 hm)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
          map (shiftFunctor C m ⋙ shiftFunctor C n) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h)) (obj.{v, v, u, u} (shiftFunctor C p') X))

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
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
rw : p' + m + n = n' + n
rw₁ : p' + m + n = 0
rw₂ : p' + (m + n) = 0
rw₃ : p' + p = 0
rw₄ rw₅ : Eq.{u_1 + 1} (α := A) 0 0
⊢ p' + m = n'

Tactic:
rw [← add_left_inj n, hn, add_assoc, h, hp]

Premises used: add_assoc, add_left_inj
-- 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
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
rw : p' + (m + n) = 0
rw₁ : p' + p = 0
rw₂ rw₃ : Eq.{u_1 + 1} (α := A) 0 0
⊢ p' + m + n = 0

Tactic:
rw [add_assoc, h, hp]

Premises used: add_assoc
-- 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
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' + m) = n'
rw₁ : n' + 0 = n'
rw₂ rw₃ : n' = n'
⊢ n' + m' + m = n'

Tactic:
rw [add_assoc, hm, add_zero]

Premises used: add_assoc, 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
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
-- 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
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
rw :
  𝟙 (obj.{v, v, u, u} (shiftFunctor C p' ⋙ shiftFunctor C p) X) =
    map (shiftFunctor C p) (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' m' p' ⋯)) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C m n p h))
          (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        map (shiftFunctor C n)
            (𝟙 (obj.{v, v, u, u} (shiftFunctor C m' ⋙ shiftFunctor C m) (obj.{v, v, u, u} (shiftFunctor C n') X))) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
              (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
            map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X)
⊢ Eq.{v + 1} (α := obj.{v, v, u, u} (shiftFunctor C p' ⋙ shiftFunctor C p) X ⟶ obj.{v, v, u, u} (𝟭 C) X)
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C p' p hp)) X)
    (map (shiftFunctor C p) (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' m' p' ⋯)) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C m n p h))
          (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        map (shiftFunctor C n)
            (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C m' m hm)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C n' n hn)) X)

Tactic:
rw [← cancel_mono ((shiftFunctorCompIsoId C p' p hp).inv.app X), Iso.hom_inv_id_app,
    shiftFunctorCompIsoId_add'_inv_app m n p m' n' p' hm hn hp h,
    Category.assoc, Category.assoc, Category.assoc, Iso.hom_inv_id_app_assoc,
    ← Functor.map_comp_assoc, Iso.hom_inv_id_app]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.shiftFunctorCompIsoId_add'_inv_app, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.cancel_mono, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Iso.hom_inv_id_app_assoc, CategoryTheory.shiftFunctorCompIsoId, CategoryTheory.Iso.inv, 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
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
dsimp :
  𝟙 (obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X)) =
    map (shiftFunctor C p) (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' m' p' ⋯)) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C m n p h))
          (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        map (shiftFunctor C n)
            (𝟙
              (obj.{v, v, u, u} (shiftFunctor C m)
                (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)))) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
              (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
            map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X)
⊢ 𝟙 (obj.{v, v, u, u} (shiftFunctor C p' ⋙ shiftFunctor C p) X) =
    map (shiftFunctor C p) (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' m' p' ⋯)) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C m n p h))
          (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        map (shiftFunctor C n)
            (𝟙 (obj.{v, v, u, u} (shiftFunctor C m' ⋙ shiftFunctor C m) (obj.{v, v, u, u} (shiftFunctor C n') X))) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
              (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
            map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X)

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
inst_3 : HasZeroMorphisms.{v, u} C
X Y : C
n : A
⊢ Eq.{v + 1} (α := obj.{v, v, u, u} (shiftFunctor C n) X ⟶ obj.{v, v, u, u} (shiftFunctor C n) Y)
    (map (shiftFunctor C n) 0) 0

Tactic:
CategoryTheory.Functor.map_zero _ _ _

Premises used: CategoryTheory.Functor.map_zero
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddCommMonoid A
inst_2 : HasShift.{v, u, u_1} C A
i j k : A
h rw : i + j = k
rw₁ rw₂ : k = k
⊢ j + i = k

Tactic:
rw [add_comm j i, h]

Premises used: add_comm
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddCommMonoid A
inst_2 : HasShift.{v, u, u_1} C A
i j k : A
h : i + j = k
subst :
  Eq (α :=
    Iso (C := Functor.{v, v, u, u} C C) (shiftFunctor C i ⋙ shiftFunctor C j) (shiftFunctor C j ⋙ shiftFunctor C i))
    (shiftFunctorComm C i j) (Iso.symm (shiftFunctorAdd' C i j (i + j) ⋯) ≪≫ shiftFunctorAdd' C j i (i + j) ⋯)
⊢ Eq (α :=
    Iso (C := Functor.{v, v, u, u} C C) (shiftFunctor C i ⋙ shiftFunctor C j) (shiftFunctor C j ⋙ shiftFunctor C i))
    (shiftFunctorComm C i j) (Iso.symm (shiftFunctorAdd' C i j k h) ≪≫ shiftFunctorAdd' C j i k ⋯)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddCommMonoid A
inst_2 : HasShift.{v, u, u_1} C A
i j : A
rw :
  Eq (α :=
    Iso (C := Functor.{v, v, u, u} C C) (shiftFunctor C i ⋙ shiftFunctor C j) (shiftFunctor C j ⋙ shiftFunctor C i))
    (shiftFunctorComm C i j) (Iso.symm (shiftFunctorAdd C i j) ≪≫ shiftFunctorAdd' C j i (i + j) ⋯)
⊢ Eq (α :=
    Iso (C := Functor.{v, v, u, u} C C) (shiftFunctor C i ⋙ shiftFunctor C j) (shiftFunctor C j ⋙ shiftFunctor C i))
    (shiftFunctorComm C i j) (Iso.symm (shiftFunctorAdd' C i j (i + j) ⋯) ≪≫ shiftFunctorAdd' C j i (i + j) ⋯)

Tactic:
rw [shiftFunctorAdd'_eq_shiftFunctorAdd]

Premises used: CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddCommMonoid A
inst_2 : HasShift.{v, u, u_1} C A
i j : A
⊢ Eq (α :=
    Iso (C := Functor.{v, v, u, u} C C) (shiftFunctor C i ⋙ shiftFunctor C j) (shiftFunctor C j ⋙ shiftFunctor C i))
    (shiftFunctorComm C i j) (Iso.symm (shiftFunctorAdd C i j) ≪≫ shiftFunctorAdd' C j i (i + j) ⋯)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddCommMonoid A
inst_2 : HasShift.{v, u, u_1} C A
i : A
rw :
  Eq (α :=
    Iso (C := Functor.{v, v, u, u} C C) (shiftFunctor C i ⋙ shiftFunctor C i) (shiftFunctor C i ⋙ shiftFunctor C i))
    (Iso.symm (shiftFunctorAdd' C i i (i + i) ⋯) ≪≫ shiftFunctorAdd' C i i (i + i) ⋯)
    (Iso.refl (shiftFunctor C i ⋙ shiftFunctor C i))
rw₁ rw₂ :
  Eq (α :=
    Iso (C := Functor.{v, v, u, u} C C) (shiftFunctor C i ⋙ shiftFunctor C i) (shiftFunctor C i ⋙ shiftFunctor C i))
    (Iso.refl (shiftFunctor C i ⋙ shiftFunctor C i)) (Iso.refl (shiftFunctor C i ⋙ shiftFunctor C i))
⊢ Eq (α :=
    Iso (C := Functor.{v, v, u, u} C C) (shiftFunctor C i ⋙ shiftFunctor C i) (shiftFunctor C i ⋙ shiftFunctor C i))
    (shiftFunctorComm C i i) (Iso.refl (shiftFunctor C i ⋙ shiftFunctor C i))

Tactic:
rw [shiftFunctorComm_eq C i i (i + i) rfl, Iso.symm_self_id]

Premises used: CategoryTheory.Iso.symm_self_id, HAdd.hAdd, CategoryTheory.shiftFunctorComm_eq, rfl
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddCommMonoid A
inst_2 : HasShift.{v, u, u_1} C A
i j : A
w :
  Eq (α :=
    Quiver.Hom (V := Functor.{v, v, u, u} C C) (shiftFunctor C j ⋙ shiftFunctor C i)
      (shiftFunctor C i ⋙ shiftFunctor C j))
    (Iso.hom (Iso.symm (shiftFunctorComm C i j))) (Iso.hom (shiftFunctorComm C j i))
⊢ Eq (α :=
    Iso (C := Functor.{v, v, u, u} C C) (shiftFunctor C j ⋙ shiftFunctor C i) (shiftFunctor C i ⋙ shiftFunctor C j))
    (Iso.symm (shiftFunctorComm C i j)) (shiftFunctorComm C j i)

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddCommMonoid A
inst_2 : HasShift.{v, u, u_1} C A
i j : A
w :
  Eq (α :=
    Quiver.Hom (V := Functor.{v, v, u, u} C C) (shiftFunctor C j ⋙ shiftFunctor C i)
      (shiftFunctor C i ⋙ shiftFunctor C j))
    (Iso.inv (Iso.symm (shiftFunctorAdd' C i j (i + j) ⋯) ≪≫ shiftFunctorAdd' C j i (i + j) ⋯))
    (Iso.hom (Iso.symm (shiftFunctorAdd' C j i (i + j) ⋯) ≪≫ shiftFunctorAdd' C i j (i + j) ⋯))
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v, v, u, u} C C) (shiftFunctor C j ⋙ shiftFunctor C i)
      (shiftFunctor C i ⋙ shiftFunctor C j))
    (Iso.inv (shiftFunctorComm C i j)) (Iso.hom (shiftFunctorComm C j i))

Tactic:
rw [shiftFunctorComm_eq C i j (i + j) rfl, shiftFunctorComm_eq C j i (i + j) (add_comm j i)]

Premises used: add_comm, HAdd.hAdd, CategoryTheory.shiftFunctorComm_eq, rfl
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddCommMonoid A
inst_2 : HasShift.{v, u, u_1} C A
i j : A
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v, v, u, u} C C) (shiftFunctor C j ⋙ shiftFunctor C i)
      (shiftFunctor C i ⋙ shiftFunctor C j))
    (Iso.inv (Iso.symm (shiftFunctorAdd' C i j (i + j) ⋯) ≪≫ shiftFunctorAdd' C j i (i + j) ⋯))
    (Iso.hom (Iso.symm (shiftFunctorAdd' C j i (i + j) ⋯) ≪≫ shiftFunctorAdd' C i j (i + j) ⋯))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddCommMonoid A
inst_2 : HasShift.{v, u, u_1} C A
X : C
i j : A
w :
  Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C i) (obj.{v, v, u, u} (shiftFunctor C j) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X))
    (Iso.hom (Iso.symm (shiftComm X i j))) (Iso.hom (shiftComm X j i))
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C i) (obj.{v, v, u, u} (shiftFunctor C j) X) ≅
      obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X))
    (Iso.symm (shiftComm X i j)) (shiftComm X j i)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddCommMonoid A
inst_2 : HasShift.{v, u, u_1} C A
X : C
i j : A
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C i) (obj.{v, v, u, u} (shiftFunctor C j) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X))
    (Iso.hom (Iso.symm (shiftComm X i j))) (Iso.hom (shiftComm X j i))

Tactic:
NatTrans.congr_app (congr_arg Iso.hom (shiftFunctorComm_symm C i j)) X

Premises used: CategoryTheory.NatTrans.congr_app, congr_arg, CategoryTheory.shiftFunctorComm_symm, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddCommMonoid A
inst_2 : HasShift.{v, u, u_1} C A
X : C
i j : A
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C i) (obj.{v, v, u, u} (shiftFunctor C j) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X))
    (Iso.hom (Iso.symm (shiftComm X i j))) (Iso.hom (shiftComm X j i))

Tactic:
exact NatTrans.congr_app (congr_arg Iso.hom (shiftFunctorComm_symm C i j)) X

Premises used: CategoryTheory.NatTrans.congr_app, congr_arg, CategoryTheory.shiftFunctorComm_symm, CategoryTheory.Iso.hom