awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
inst_4 : F.ShiftSequence M
X Y : C
n a a' : M
ha' : n + a = a'
f : X ⟶ Y
⊢ (F.shift a).map (map (shiftFunctor C n) f) ≫ NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) Y =
    NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) X ≫ (F.shift a').map f

Tactic:
(F.shiftIso n a a' ha').hom.naturality f

Premises used: CategoryTheory.Functor.shiftIso, CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
inst_4 : F.ShiftSequence M
X Y : C
n a a' : M
ha' : n + a = a'
f : X ⟶ Y
⊢ (F.shift a').map f ≫ NatTrans.app (Iso.inv (F.shiftIso n a a' ha')) Y =
    NatTrans.app (Iso.inv (F.shiftIso n a a' ha')) X ≫ (F.shift a).map (map (shiftFunctor C n) f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
inst_4 : F.ShiftSequence M
n : M
X Y : C
f : X ⟶ Y
⊢ F.map (map (shiftFunctor C n) f) ≫ NatTrans.app (Iso.hom (F.isoShift n)) Y =
    NatTrans.app (Iso.hom (F.isoShift n)) X ≫ (F.shift n).map f

Tactic:
(F.isoShift n).hom.naturality f

Premises used: CategoryTheory.Functor.isoShift, CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
inst_4 : F.ShiftSequence M
n : M
X Y : C
f : X ⟶ Y
⊢ (F.shift n).map f ≫ NatTrans.app (Iso.inv (F.isoShift n)) Y =
    NatTrans.app (Iso.inv (F.isoShift n)) X ≫ F.map (map (shiftFunctor C n) f)

Tactic:
(F.isoShift n).inv.naturality f

Premises used: CategoryTheory.Functor.isoShift, CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
inst_4 : F.ShiftSequence M
a : M
⊢ F.shiftIso 0 a a ⋯ = isoWhiskerRight (shiftFunctorZero C M) (F.shift a) ≪≫ (F.shift a).leftUnitor

Tactic:
ShiftSequence.shiftIso_zero a

Premises used: CategoryTheory.Functor.shiftIso, CategoryTheory.Functor.shift, CategoryTheory.Functor.ShiftSequence.shiftIso_zero
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
inst_4 : F.ShiftSequence M
a : M
X : C
⊢ NatTrans.app (Iso.hom (F.shiftIso 0 a a ⋯)) X = (F.shift a).map (NatTrans.app (Iso.hom (shiftFunctorZero C M)) X)

Tactic:
simp [F.shiftIso_zero a]

Premises used: CategoryTheory.Functor.shiftIso_zero
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
inst_4 : F.ShiftSequence M
a : M
X : C
⊢ NatTrans.app (Iso.inv (F.shiftIso 0 a a ⋯)) X = (F.shift a).map (NatTrans.app (Iso.inv (shiftFunctorZero C M)) X)

Tactic:
simp [F.shiftIso_zero a]

Premises used: CategoryTheory.Functor.shiftIso_zero
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
rw : m + (n + a) = a''
rw₁ : m + a' = a''
rw₂ rw₃ : a'' = a''
⊢ m + n + a = a''

Tactic:
rw [add_assoc, ha', ha'']

Premises used: add_assoc
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
inst_4 : F.ShiftSequence M
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
⊢ F.shiftIso (m + n) a a'' ⋯ =
    isoWhiskerRight (shiftFunctorAdd C m n) (F.shift a) ≪≫
      associator (shiftFunctor C m) (shiftFunctor C n) (F.shift a) ≪≫
        isoWhiskerLeft (shiftFunctor C m) (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha''

Tactic:
ShiftSequence.shiftIso_add _ _ _ _ _ _ _

Premises used: CategoryTheory.Functor.shiftIso, CategoryTheory.Functor.ShiftSequence.shiftIso_add, CategoryTheory.Functor.shift
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
rw : m + (n + a) = a''
rw₁ : m + a' = a''
rw₂ rw₃ : a'' = a''
⊢ m + n + a = a''

Tactic:
rw [add_assoc, ha', ha'']

Premises used: add_assoc
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
inst_4 : F.ShiftSequence M
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ NatTrans.app (Iso.hom (F.shiftIso (m + n) a a'' ⋯)) X =
    (F.shift a).map (NatTrans.app (Iso.hom (shiftFunctorAdd C m n)) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
        NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X

Tactic:
simp [F.shiftIso_add n m a a' a'' ha' ha'']

Premises used: CategoryTheory.Functor.shiftIso_add
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
inst_4 : F.ShiftSequence M
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ NatTrans.app (Iso.inv (F.shiftIso (m + n) a a'' ⋯)) X =
    NatTrans.app (Iso.inv (F.shiftIso m a' a'' ha'')) X ≫
      NatTrans.app (Iso.inv (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
        (F.shift a).map (NatTrans.app (Iso.inv (shiftFunctorAdd C m n)) X)

Tactic:
simp [F.shiftIso_add n m a a' a'' ha' ha'']

Premises used: CategoryTheory.Functor.shiftIso_add
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
rw : m + n + a = a''
rw₁ : m + n + a = m + a'
rw₂ : m + n + a = m + (n + a)
rw₃ rw₄ : m + (n + a) = m + (n + a)
⊢ mn + a = a''

Tactic:
rw [← hnm, ← ha'', ← ha', add_assoc]

Premises used: add_assoc
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
inst_4 : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
subst :
  F.shiftIso (m + n) a a'' ⋯ =
    isoWhiskerRight (shiftFunctorAdd' C m n (m + n) ⋯) (F.shift a) ≪≫
      associator (shiftFunctor C m) (shiftFunctor C n) (F.shift a) ≪≫
        isoWhiskerLeft (shiftFunctor C m) (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha''
⊢ F.shiftIso mn a a'' ⋯ =
    isoWhiskerRight (shiftFunctorAdd' C m n mn hnm) (F.shift a) ≪≫
      associator (shiftFunctor C m) (shiftFunctor C n) (F.shift a) ≪≫
        isoWhiskerLeft (shiftFunctor C m) (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha''

Tactic:
subst hnm
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
inst_4 : F.ShiftSequence M
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
rw :
  F.shiftIso (m + n) a a'' ⋯ =
    isoWhiskerRight (shiftFunctorAdd C m n) (F.shift a) ≪≫
      associator (shiftFunctor C m) (shiftFunctor C n) (F.shift a) ≪≫
        isoWhiskerLeft (shiftFunctor C m) (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha''
rw₁ :
  isoWhiskerRight (shiftFunctorAdd C m n) (F.shift a) ≪≫
      associator (shiftFunctor C m) (shiftFunctor C n) (F.shift a) ≪≫
        isoWhiskerLeft (shiftFunctor C m) (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha'' =
    isoWhiskerRight (shiftFunctorAdd C m n) (F.shift a) ≪≫
      associator (shiftFunctor C m) (shiftFunctor C n) (F.shift a) ≪≫
        isoWhiskerLeft (shiftFunctor C m) (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha''
a'₁ : M
ha'₁ : n + a = a'
ha''₁ : m + a' = a''
rw₂ :
  isoWhiskerRight (shiftFunctorAdd C m n) (F.shift a) ≪≫
      associator (shiftFunctor C m) (shiftFunctor C n) (F.shift a) ≪≫
        isoWhiskerLeft (shiftFunctor C m) (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha'' =
    isoWhiskerRight (shiftFunctorAdd C m n) (F.shift a) ≪≫
      associator (shiftFunctor C m) (shiftFunctor C n) (F.shift a) ≪≫
        isoWhiskerLeft (shiftFunctor C m) (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha''
a'₂ : M
ha'₂ : n + a = a'
ha''₂ : m + a' = a''
⊢ F.shiftIso (m + n) a a'' ⋯ =
    isoWhiskerRight (shiftFunctorAdd' C m n (m + n) ⋯) (F.shift a) ≪≫
      associator (shiftFunctor C m) (shiftFunctor C n) (F.shift a) ≪≫
        isoWhiskerLeft (shiftFunctor C m) (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha''

Tactic:
rw [shiftFunctorAdd'_eq_shiftFunctorAdd, shiftIso_add]

Premises used: CategoryTheory.Functor.shiftIso_add, CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
rw : m + n + a = a''
rw₁ : m + n + a = m + a'
rw₂ : m + n + a = m + (n + a)
rw₃ rw₄ : m + (n + a) = m + (n + a)
⊢ mn + a = a''

Tactic:
rw [← hnm, ← ha'', ← ha', add_assoc]

Premises used: add_assoc
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
inst_4 : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ NatTrans.app (Iso.hom (F.shiftIso mn a a'' ⋯)) X =
    (F.shift a).map (NatTrans.app (Iso.hom (shiftFunctorAdd' C m n mn hnm)) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
        NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X

Tactic:
simp [F.shiftIso_add' n m mn hnm a a' a'' ha' ha'']

Premises used: CategoryTheory.Functor.shiftIso_add'
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
inst_4 : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ NatTrans.app (Iso.inv (F.shiftIso mn a a'' ⋯)) X =
    NatTrans.app (Iso.inv (F.shiftIso m a' a'' ha'')) X ≫
      NatTrans.app (Iso.inv (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
        (F.shift a).map (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n mn hnm)) X)

Tactic:
simp [F.shiftIso_add' n m mn hnm a a' a'' ha' ha'']

Premises used: CategoryTheory.Functor.shiftIso_add'
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
inst_4 : F.ShiftSequence M
X Y Z : C
n : M
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y
g : Y ⟶ Z
a a' : M
ha' : n + a = a'
⊢ F.shiftMap (f ≫ map (shiftFunctor C n) g) a a' ha' = F.shiftMap f a a' ha' ≫ (F.shift a').map g

Tactic:
simp [shiftMap]

Premises used: CategoryTheory.Functor.shiftMap
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
inst_4 : F.ShiftSequence M
X Y Z : C
n : M
f : X ⟶ Y
g : Y ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Z
a a' : M
ha' : n + a = a'
⊢ F.shiftMap (f ≫ g) a a' ha' = (F.shift a).map f ≫ F.shiftMap g a a' ha'

Tactic:
simp [shiftMap]

Premises used: CategoryTheory.Functor.shiftMap
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
X Y : C
m : M
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) Y
n mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
rw : mn + a = m + a'
rw₁ : mn + a = m + (n + a)
rw₂ : m + n + a = m + (n + a)
rw₃ rw₄ : m + (n + a) = m + (n + a)
⊢ mn + a = a''

Tactic:
rw [← ha'', ← ha', ← hnm, add_assoc]

Premises used: add_assoc
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
inst_4 : F.ShiftSequence M
X Y : C
m : M
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) Y
n mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
⊢ NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) X ≫ F.shiftMap f a' a'' ha'' =
    (F.shift a).map (map (shiftFunctor C n) f) ≫
      (F.shift a).map (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n mn hnm)) Y) ≫
        NatTrans.app (Iso.hom (F.shiftIso mn a a'' ⋯)) Y

Tactic:
simp only [F.shiftIso_add'_hom_app n m mn hnm a a' a'' ha' ha'' Y,
    ← Functor.map_comp_assoc, Iso.inv_hom_id_app, Functor.map_id,
    id_comp, comp_obj, shiftIso_hom_naturality_assoc, shiftMap]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.shiftIso_add'_hom_app, CategoryTheory.Functor.shiftMap, CategoryTheory.Functor.shiftIso_hom_naturality_assoc, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
inst_7 : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
rw : n + (m + a) = a
rw₁ : n + m + a = a
rw₂ : 0 + a = a
rw₃ rw₄ : a = a
⊢ n + a' = a

Tactic:
rw [← ha', ← add_assoc, hnm, zero_add]

Premises used: add_assoc, zero_add
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
inst_7 : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
rw : m + n + m = 0 + m
rw₁ : m + (n + m) = 0 + m
rw₂ : m + 0 = 0 + m
rw₃ : m + 0 = m
rw₄ rw₅ : m = m
⊢ m + n = 0

Tactic:
rw [← add_left_inj m, add_assoc, hnm, zero_add, add_zero]

Premises used: add_assoc, add_left_inj, zero_add, add_zero
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
G : Type u_4
inst_2 : AddGroup G
inst_3 : HasShift.{v_1, u_1, u_4} C G
inst_4 : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
rw : m + n + m = 0 + m
rw₁ : m + (n + m) = 0 + m
rw₂ : m + 0 = 0 + m
rw₃ : m + 0 = m
rw₄ rw₅ : m = m
⊢ m + n = 0

Tactic:
rw [← add_left_inj m, add_assoc, hnm, zero_add, add_zero]

Premises used: add_assoc, add_left_inj, zero_add, add_zero
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
G : Type u_4
inst_2 : AddGroup G
inst_3 : HasShift.{v_1, u_1, u_4} C G
inst_4 : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
⊢ m + n = 0

Tactic:
have hnm' : m + n = 0 := by
    rw [← add_left_inj m, add_assoc, hnm, zero_add, add_zero]
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
G : Type u_4
inst_2 : AddGroup G
inst_3 : HasShift.{v_1, u_1, u_4} C G
inst_4 : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
hnm' : m + n = 0
⊢ NatTrans.app (Iso.hom (F.shiftIso n a' a ⋯)) X ≫ F.shiftMap f a a' ha' =
    (F.shift a').map (map (shiftFunctor C n) f ≫ NatTrans.app (Iso.hom (shiftFunctorCompIsoId C m n ⋯)) Y)

Tactic:
simp [F.shiftIso_hom_app_comp_shiftMap f n 0 hnm' a' a, shiftIso_zero_hom_app,
    shiftFunctorCompIsoId]

Premises used: CategoryTheory.Functor.shiftIso_zero_hom_app, CategoryTheory.Functor.shiftIso_hom_app_comp_shiftMap, CategoryTheory.shiftFunctorCompIsoId, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
inst_7 : HasZeroMorphisms.{v_1, u_1} C
inst_8 : HasZeroMorphisms.{v_2, u_2} A
inst_9 : F.PreservesZeroMorphisms
inst_10 : ∀ (n : M), PreservesZeroMorphisms.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
n : M
⊢ (F.shift n).PreservesZeroMorphisms

Tactic:
preservesZeroMorphisms_of_iso (F.isoShift n)

Premises used: CategoryTheory.Functor.isoShift, CategoryTheory.Functor.preservesZeroMorphisms_of_iso
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
inst_4 : F.ShiftSequence M
inst_5 : HasZeroMorphisms.{v_1, u_1} C
inst_6 : HasZeroMorphisms.{v_2, u_2} A
inst_7 : F.PreservesZeroMorphisms
inst_8 : ∀ (n : M), PreservesZeroMorphisms.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
X Y : C
n a a' : M
ha' : n + a = a'
⊢ Eq (α := (F.shift a).obj X ⟶ (F.shift a').obj Y) (F.shiftMap 0 a a' ha') 0

Tactic:
simp [shiftMap]

Premises used: CategoryTheory.Functor.shiftMap
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
inst_7 : Preadditive.{v_1, u_1} C
inst_8 : Preadditive.{v_2, u_2} A
inst_9 : F.Additive
inst_10 : ∀ (n : M), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
n : M
⊢ (F.shift n).Additive

Tactic:
additive_of_iso (F.isoShift n)

Premises used: CategoryTheory.Functor.isoShift, CategoryTheory.Functor.additive_of_iso
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : HasShift.{v_2, u_2, u_4} D M
inst_6 : HasShift.{v_3, u_3, u_4} E M
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
α : ShiftedHom X Y a₁
β : ShiftedHom Y Z a₂
γ : ShiftedHom Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h : a₃ + a₂ + a₁ = a
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.ShiftedHom
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : HasShift.{v_2, u_2, u_4} D M
inst_6 : HasShift.{v_3, u_3, u_4} E M
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
α : ShiftedHom X Y a₁
β : ShiftedHom Y Z a₂
γ : ShiftedHom Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h rw : a₃ + a₂ + a₁ = a
rw₁ rw₂ : a = a
⊢ a₂₃ + a₁ = a

Tactic:
rw [← h₂₃, h]
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
α : ShiftedHom X Y a₁
β : ShiftedHom Y Z a₂
γ : ShiftedHom Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h : a₃ + a₂ + a₁ = a
⊢ (α.comp β h₁₂).comp γ ⋯ = α.comp (β.comp γ h₂₃) ⋯

Tactic:
simp only [comp, assoc, Functor.map_comp,
    shiftFunctorAdd'_assoc_inv_app a₃ a₂ a₁ a₂₃ a₁₂ a h₂₃ h₁₂ h,
    ← NatTrans.naturality_assoc, Functor.comp_map]

Premises used: CategoryTheory.shiftFunctorAdd'_assoc_inv_app, CategoryTheory.Category.assoc, CategoryTheory.ShiftedHom.comp, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.comp_map, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : HasShift.{v_2, u_2, u_4} D M
inst_6 : HasShift.{v_3, u_3, u_4} E M
X Y Z T : C
m₀ : M
hm₀ : m₀ = 0
f : X ⟶ Y
⊢ (fun (g : ShiftedHom X Y m₀) ↦ g ≫ NatTrans.app (Iso.hom (shiftFunctorZero' C m₀ hm₀)) Y)
      ((fun (f : X ⟶ Y) ↦ (mk₀ m₀ hm₀ f : ShiftedHom X Y m₀)) f) =
    f

Tactic:
simp [mk₀]

Premises used: CategoryTheory.ShiftedHom.mk₀