awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X Y Z : C
n m : ℤ
f : ShiftedHom X Y n
g : ShiftedHom Y Z m
q : ℤ
hq : n + m = q
rw :
  CategoryStruct.comp (Y :=
        Opposite.unop
          (Functor.obj.{v_1, v_1, u_1, u_1}
            (Equivalence.functor (opShiftFunctorEquivalence C n) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C n))
            (Opposite.op X)))
        (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C n))) (Opposite.op X)))
        (Functor.map (shiftFunctor C n)
          (Quiver.Hom.unop
            (Quiver.Hom.op g ≫
              CategoryStruct.comp (Y :=
                Functor.obj.{v_1, v_1, u_1, u_1}
                  (Equivalence.inverse (opShiftFunctorEquivalence C n) ⋙
                    Equivalence.functor (opShiftFunctorEquivalence C n))
                  (Opposite.op Y))
                (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C n))) (Opposite.op Y))
                (Functor.map (shiftFunctor Cᵒᵖ n) (Quiver.Hom.op f))))) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C m n q ⋯)) Z =
    f.comp g ⋯
⊢ (Equiv.symm (opEquiv' n m q hq) :
        (a : Opposite.op ((shiftFunctor C m).obj Z) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) → ShiftedHom X Z q)
      (Quiver.Hom.op g ≫
          CategoryStruct.comp (Y :=
            Functor.obj.{v_1, v_1, u_1, u_1}
              (Equivalence.inverse (opShiftFunctorEquivalence C n) ⋙
                Equivalence.functor (opShiftFunctorEquivalence C n))
              (Opposite.op Y))
            (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C n))) (Opposite.op Y))
            (Functor.map (shiftFunctor Cᵒᵖ n) (Quiver.Hom.op f)) :
        Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) Z) ⟶
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) (Opposite.op X)) =
    f.comp g ⋯

Tactic:
rw [opEquiv'_symm_apply, opEquiv_symm_apply]

Premises used: CategoryTheory.ShiftedHom.opEquiv'_symm_apply, CategoryTheory.ShiftedHom.opEquiv_symm_apply
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X Y Z : C
n m : ℤ
f : ShiftedHom X Y n
g : ShiftedHom Y Z m
q : ℤ
hq : n + m = q
a a₁ :
  Eq.{v_1 + 1} (α := Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C q) Z) ⟶ Opposite.op X)
    (Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n q ⋯)) Z) ≫
        Quiver.Hom.op (Functor.map (shiftFunctor C n) g) ≫ Quiver.Hom.op f :
      Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C q) Z) ⟶ Opposite.op X)
    (Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n q ⋯)) Z) ≫
      Quiver.Hom.op (Functor.map (shiftFunctor C n) g) ≫ Quiver.Hom.op f)
⊢ Eq (α := Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C q) Z) ⟶ Opposite.op X)
    (Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n q ⋯)) Z) ≫
      Quiver.Hom.op (Functor.map (shiftFunctor C n) g) ≫
        CategoryStruct.comp (Y :=
          Opposite.op
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
              (Opposite.unop
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n)
                  (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y))))))
          (Quiver.Hom.op
              (Functor.map (shiftFunctor C n)
                (Quiver.Hom.unop
                  (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C n))) (Opposite.op Y)))) :
            Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y) ⟶
              Opposite.op
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
                  (Opposite.unop
                    (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n)
                      (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y))))))
          (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C n)))
                (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y)) ≫
              Quiver.Hom.op f :
            Functor.obj.{v_1, v_1, u_1, u_1}
                (Equivalence.functor (opShiftFunctorEquivalence C n) ⋙
                  Equivalence.inverse (opShiftFunctorEquivalence C n))
                (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y)) ⟶
              Opposite.op X))
    (Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n q ⋯)) Z) ≫
      Quiver.Hom.op (Functor.map (shiftFunctor C n) g) ≫ Quiver.Hom.op f)

Tactic:
erw [(opShiftFunctorEquivalence C n).inverse_counitInv_comp_assoc (Opposite.op Y)]

Premises used: CategoryTheory.Equivalence.inverse_counitInv_comp_assoc, Opposite.op, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X Y Z : C
f : Y ⟶ X
n a : ℤ
x :
  Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Z) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) (Opposite.op X)
a' : ℤ
h : n + a = a'
⊢ Eq.{v_1 + 1} (α := Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') Z) ⟶ Opposite.op Y)
    (Quiver.Hom.op
        ((Equiv.symm (opEquiv' n a a' h) :
            (a : Opposite.op ((shiftFunctor C a).obj Z) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op Y)) → ShiftedHom Y Z a')
          (x ≫ Functor.map (shiftFunctor Cᵒᵖ n) f.op)) :
      Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') Z) ⟶ Opposite.op Y)
    (Quiver.Hom.op
        (f ≫
          (Equiv.symm (opEquiv' n a a' h) :
              (a : Opposite.op ((shiftFunctor C a).obj Z) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) →
                ShiftedHom X Z a')
            x) :
      Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') Z) ⟶ Opposite.op Y)

Tactic:
simp [opEquiv'_symm_apply, opEquiv_symm_apply]

Premises used: CategoryTheory.ShiftedHom.opEquiv'_symm_apply, CategoryTheory.ShiftedHom.opEquiv_symm_apply
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X Y : C
a : ℤ
f :
  Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) (Opposite.op X)
⊢ Eq (α := ShiftedHom X Y a)
    ((Equiv.symm (opEquiv' 0 a a ⋯) :
          (a_1 : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ 0).obj (Opposite.op X)) → ShiftedHom X Y a)
        f :
      ShiftedHom X Y a)
    (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) (Opposite.op X)) ≫ f.unop :
      Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) (Opposite.op X)) ⟶
        Opposite.unop (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y)))

Tactic:
simp [opEquiv'_symm_apply, opEquiv_symm_apply, shiftFunctorAdd'_add_zero,
    opShiftFunctorEquivalence_zero_unitIso_inv_app]

Premises used: CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_zero_unitIso_inv_app, CategoryTheory.shiftFunctorAdd'_add_zero, CategoryTheory.ShiftedHom.opEquiv'_symm_apply, CategoryTheory.ShiftedHom.opEquiv_symm_apply
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X Y Z : C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
x :
  Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (m + n)) (Opposite.op X)
⊢ m + n + a = a''

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X Y : C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
x :
  Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (m + n)) (Opposite.op X)
⊢ a + n = a'

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X Y : C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
x :
  Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (m + n)) (Opposite.op X)
⊢ n + m = m + n

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X Y : C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
x :
  Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (m + n)) (Opposite.op X)
⊢ a + n + m = a''

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X Y : C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
n a : ℤ
x y :
  Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) (Opposite.op X)
a' : ℤ
h : n + a = a'
dsimp :
  (Equiv.symm (opEquiv n) :
          (a_1 : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) →
            X ⟶ (shiftFunctor C n).obj ((shiftFunctor C a).obj Y))
        (x + y) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C a n a' ⋯)) Y =
    HAdd.hAdd (α := ShiftedHom X Y a') (β := ShiftedHom X Y a')
      ((Equiv.symm (opEquiv n) :
              (a_1 : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) →
                X ⟶ (shiftFunctor C n).obj ((shiftFunctor C a).obj Y))
            x ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C a n a' ⋯)) Y :
        X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') Y)
      ((Equiv.symm (opEquiv n) :
              (a_1 : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) →
                X ⟶ (shiftFunctor C n).obj ((shiftFunctor C a).obj Y))
            y ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C a n a' ⋯)) Y :
        X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') Y)
⊢ (Equiv.symm (opEquiv' n a a' h) :
        (a : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) → ShiftedHom X Y a')
      (x + y) =
    HAdd.hAdd (α := ShiftedHom X Y a') (β := ShiftedHom X Y a')
      ((Equiv.symm (opEquiv' n a a' h) :
            (a : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) → ShiftedHom X Y a')
          x :
        ShiftedHom X Y a')
      ((Equiv.symm (opEquiv' n a a' h) :
            (a : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) → ShiftedHom X Y a')
          y :
        ShiftedHom X Y a')

Tactic:
dsimp [opEquiv']

Premises used: CategoryTheory.ShiftedHom.opEquiv'
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctors
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
functor : (a : A) → Functor.{v_1, v_2, u_1, u_2} C D
shiftIso : (n a a' : A) → (ha' : n + a = a') → functor a' ⋙ shiftFunctor D n ≅ functor a
shiftIso_zero : ∀ (a : A), shiftIso 0 a a ⋯ = (functor a).isoWhiskerLeft (shiftFunctorZero D A)
n m a a' a'' : A
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.SingleFunctors
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
n m a a' a'' : A
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.SingleFunctors
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_2, u_2, u_5} D A
F : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ (F.shiftIso (m + n) a a'' ⋯).hom.app X =
    NatTrans.app (Iso.hom (shiftFunctorAdd D m n)) ((F.functor a'').obj X) ≫
      Functor.map (shiftFunctor D n) ((F.shiftIso m a' a'' ha'').hom.app X) ≫ (F.shiftIso n a a' ha').hom.app X

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

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

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

Premises used: CategoryTheory.SingleFunctors.shiftIso_add
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctors
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
n m mn : A
hnm : m + n = mn
a a' a'' : A
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.SingleFunctors
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_2, u_2, u_5} D A
F : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
n m mn : A
hnm : m + n = mn
a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
subst :
  F.shiftIso (m + n) a a'' ⋯ =
    (F.functor a'').isoWhiskerLeft (shiftFunctorAdd' D m n (m + n) ⋯) ≪≫
      ((F.functor a'').associator (shiftFunctor D m) (shiftFunctor D n)).symm ≪≫
        isoWhiskerRight (F.shiftIso m a' a'' ha'') (shiftFunctor D n) ≪≫ F.shiftIso n a a' ha'
⊢ F.shiftIso mn a a'' ⋯ =
    (F.functor a'').isoWhiskerLeft (shiftFunctorAdd' D m n mn hnm) ≪≫
      ((F.functor a'').associator (shiftFunctor D m) (shiftFunctor D n)).symm ≪≫
        isoWhiskerRight (F.shiftIso m a' a'' ha'') (shiftFunctor D n) ≪≫ F.shiftIso n a a' ha'

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

Tactic:
rw [shiftFunctorAdd'_eq_shiftFunctorAdd, shiftIso_add]

Premises used: CategoryTheory.SingleFunctors.shiftIso_add, CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctors
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
n m mn : A
hnm : m + n = mn
a a' a'' : A
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.SingleFunctors
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_2, u_2, u_5} D A
F : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
n m mn : A
hnm : m + n = mn
a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ (F.shiftIso mn a a'' ⋯).hom.app X =
    NatTrans.app (Iso.hom (shiftFunctorAdd' D m n mn hnm)) ((F.functor a'').obj X) ≫
      Functor.map (shiftFunctor D n) ((F.shiftIso m a' a'' ha'').hom.app X) ≫ (F.shiftIso n a a' ha').hom.app X

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

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

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

Premises used: CategoryTheory.SingleFunctors.shiftIso_add'
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctors
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_2, u_2, u_5} D A
F : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
a : A
X : C
rw :
  Eq (α := (F.functor a ⋙ shiftFunctor.{v_2, u_2, u_5} D (A := A) 0).obj X ⟶ (F.functor a).obj X)
    (NatTrans.app (Iso.hom ((F.functor a).isoWhiskerLeft (shiftFunctorZero D A))) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero D A)) ((F.functor a).obj X))
⊢ NatTrans.app (Iso.hom (F.shiftIso 0 a a ⋯)) X = NatTrans.app (Iso.hom (shiftFunctorZero D A)) ((F.functor a).obj X)

Tactic:
rw [shiftIso_zero]

Premises used: CategoryTheory.SingleFunctors.shiftIso_zero
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctors
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_2, u_2, u_5} D A
F : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
a : A
X : C
⊢ Eq (α := (F.functor a ⋙ shiftFunctor.{v_2, u_2, u_5} D (A := A) 0).obj X ⟶ (F.functor a).obj X)
    (NatTrans.app (Iso.hom ((F.functor a).isoWhiskerLeft (shiftFunctorZero D A))) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero D A)) ((F.functor a).obj X))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctors
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_2, u_2, u_5} D A
F : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
a : A
X : C
rw :
  Eq (α := (F.functor a).obj X ⟶ (F.functor a ⋙ shiftFunctor.{v_2, u_2, u_5} D (A := A) 0).obj X)
    (NatTrans.app (Iso.inv ((F.functor a).isoWhiskerLeft (shiftFunctorZero D A))) X)
    (NatTrans.app (Iso.inv (shiftFunctorZero D A)) ((F.functor a).1 X))
⊢ NatTrans.app (Iso.inv (F.shiftIso 0 a a ⋯)) X = NatTrans.app (Iso.inv (shiftFunctorZero D A)) ((F.functor a).1 X)

Tactic:
rw [shiftIso_zero]

Premises used: CategoryTheory.SingleFunctors.shiftIso_zero
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctors
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_2, u_2, u_5} D A
F : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
a : A
X : C
⊢ Eq (α := (F.functor a).obj X ⟶ (F.functor a ⋙ shiftFunctor.{v_2, u_2, u_5} D (A := A) 0).obj X)
    (NatTrans.app (Iso.inv ((F.functor a).isoWhiskerLeft (shiftFunctorZero D A))) X)
    (NatTrans.app (Iso.inv (shiftFunctorZero D A)) ((F.functor a).1 X))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctors
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_2, u_2, u_5} D A
F : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
a : A
⊢ Hom.hom (𝟙 F) a = 𝟙 (F.functor a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctors
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_2, u_2, u_5} D A
F G H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
f : F ⟶ G
g : G ⟶ H
a : A
⊢ (f ≫ g).hom a = f.hom a ≫ g.hom a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctors
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_2, u_2, u_5} D A
F G : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
f g : F ⟶ G
h : f.hom = g.hom
⊢ f = g

Tactic:
Hom.ext h

Premises used: CategoryTheory.SingleFunctors.Hom.ext