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

Tactic:
simp only [Functor.map_id, Category.comp_id,
    shiftFunctorComm_eq C _ _ _ rfl, ← shiftFunctorAdd'_eq_shiftFunctorAdd]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.shiftFunctorComm_eq, rfl, 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
m₁ m₂ m₃ : A
X : C
dsimp :
  Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C (m₂ + m₃)) (obj.{v, v, u, u} (shiftFunctor C m₁) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C m₃)
        (obj.{v, v, u, u} (shiftFunctor C m₂) (obj.{v, v, u, u} (shiftFunctor C m₁) X)))
    ((NatTrans.app (Iso.inv (shiftFunctorAdd' C m₁ (m₂ + m₃) (m₁ + (m₂ + m₃)) ⋯)) X ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C (m₂ + m₃) m₁ (m₁ + (m₂ + m₃)) ⋯)) X) ≫
      map (shiftFunctor C m₁) (NatTrans.app (Iso.hom (shiftFunctorAdd' C m₂ m₃ (m₂ + m₃) ⋯)) X) ≫
        (NatTrans.app (Iso.inv (shiftFunctorAdd' C m₃ m₁ (m₁ + m₃) ⋯)) (obj.{v, v, u, u} (shiftFunctor C m₂) X) ≫
            NatTrans.app (Iso.hom (shiftFunctorAdd' C m₁ m₃ (m₁ + m₃) ⋯)) (obj.{v, v, u, u} (shiftFunctor C m₂) X)) ≫
          map (shiftFunctor C m₃)
            (NatTrans.app (Iso.inv (shiftFunctorAdd' C m₂ m₁ (m₁ + m₂) ⋯)) X ≫
              NatTrans.app (Iso.hom (shiftFunctorAdd' C m₁ m₂ (m₁ + m₂) ⋯)) X))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C m₂ m₃ (m₂ + m₃) ⋯)) (obj.{v, v, u, u} (shiftFunctor C m₁) X))
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C (m₂ + m₃)) (obj.{v, v, u, u} (shiftFunctor C m₁) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C m₃)
        (obj.{v, v, u, u} (shiftFunctor C m₂) (obj.{v, v, u, u} (shiftFunctor C m₁) X)))
    (NatTrans.app
        (Iso.hom
          (Iso.symm (shiftFunctorAdd' C m₁ (m₂ + m₃) (m₁ + (m₂ + m₃)) ⋯) ≪≫
            shiftFunctorAdd' C (m₂ + m₃) m₁ (m₁ + (m₂ + m₃)) ⋯))
        X ≫
      map (shiftFunctor C m₁) (NatTrans.app (Iso.hom (shiftFunctorAdd' C m₂ m₃ (m₂ + m₃) ⋯)) X) ≫
        NatTrans.app (Iso.inv (Iso.symm (shiftFunctorAdd' C m₁ m₃ (m₁ + m₃) ⋯) ≪≫ shiftFunctorAdd' C m₃ m₁ (m₁ + m₃) ⋯))
            (obj.{v, v, u, u} (shiftFunctor C m₂) X) ≫
          map (shiftFunctor C m₃)
            (NatTrans.app
              (Iso.inv (Iso.symm (shiftFunctorAdd' C m₁ m₂ (m₁ + m₂) ⋯) ≪≫ shiftFunctorAdd' C m₂ m₁ (m₁ + m₂) ⋯)) X))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C m₂ m₃ (m₂ + m₃) ⋯)) (obj.{v, v, u, u} (shiftFunctor C m₁) X))

Tactic:
dsimp
-- 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
m₁ m₂ m₃ : A
X : C
rw : m₁ + m₂ + m₃ = m₁ + (m₂ + m₃)
rw₁ rw₂ : m₁ + (m₂ + m₃) = m₁ + (m₂ + m₃)
⊢ m₂ + m₁ + m₃ = m₁ + (m₂ + m₃)

Tactic:
rw [add_comm m₂ m₁, add_assoc]

Premises used: add_assoc, 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
m₁ m₂ m₃ : A
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C (m₂ + m₃)) (obj.{v, v, u, u} (shiftFunctor C m₁) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C m₃)
        (obj.{v, v, u, u} (shiftFunctor C m₂) (obj.{v, v, u, u} (shiftFunctor C m₁) X)))
    ((NatTrans.app (Iso.inv (shiftFunctorAdd' C m₁ (m₂ + m₃) (m₁ + (m₂ + m₃)) ⋯)) X ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C (m₂ + m₃) m₁ (m₁ + (m₂ + m₃)) ⋯)) X) ≫
      map (shiftFunctor C m₁) (NatTrans.app (Iso.hom (shiftFunctorAdd' C m₂ m₃ (m₂ + m₃) ⋯)) X) ≫
        (NatTrans.app (Iso.inv (shiftFunctorAdd' C m₃ m₁ (m₁ + m₃) ⋯)) (obj.{v, v, u, u} (shiftFunctor C m₂) X) ≫
            NatTrans.app (Iso.hom (shiftFunctorAdd' C m₁ m₃ (m₁ + m₃) ⋯)) (obj.{v, v, u, u} (shiftFunctor C m₂) X)) ≫
          map (shiftFunctor C m₃)
            (NatTrans.app (Iso.inv (shiftFunctorAdd' C m₂ m₁ (m₁ + m₂) ⋯)) X ≫
              NatTrans.app (Iso.hom (shiftFunctorAdd' C m₁ m₂ (m₁ + m₂) ⋯)) X))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C m₂ m₃ (m₂ + m₃) ⋯)) (obj.{v, v, u, u} (shiftFunctor C m₁) X))

Tactic:
simp only [Category.assoc, Iso.hom_inv_id_app_assoc, Iso.inv_hom_id_app_assoc,
    ← Functor.map_comp,
    shiftFunctorAdd'_assoc_hom_app_assoc m₂ m₃ m₁ (m₂ + m₃) (m₁ + m₃) (m₁ + (m₂ + m₃)) rfl
      (add_comm m₃ m₁) (add_comm _ m₁) X,
    ← shiftFunctorAdd'_assoc_hom_app_assoc m₂ m₁ m₃ (m₁ + m₂) (m₁ + m₃)
      (m₁ + (m₂ + m₃)) (add_comm _ _) rfl (by rw [add_comm m₂ m₁, add_assoc]) X,
    shiftFunctorAdd'_assoc_hom_app m₁ m₂ m₃
      (m₁ + m₂) (m₂ + m₃) (m₁ + (m₂ + m₃)) rfl rfl (add_assoc _ _ _) X]

Premises used: CategoryTheory.Category.assoc, add_assoc, add_comm, CategoryTheory.Iso.hom_inv_id_app_assoc, HAdd.hAdd, CategoryTheory.Functor.map_comp, CategoryTheory.shiftFunctorAdd'_assoc_hom_app_assoc, CategoryTheory.Iso.inv_hom_id_app_assoc, rfl, CategoryTheory.shiftFunctorAdd'_assoc_hom_app
-- 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_1 Y : C
f : X_1 ⟶ Y
m n : A
hmn : m + n = 0
X : C
rw : m + n = 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := A) 0 0
⊢ n + m = 0

Tactic:
rw [add_comm, hmn]

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
m n : A
hmn : m + n = 0
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C m ⋙ shiftFunctor C n) X ⟶ obj.{v, v, u, u} (shiftFunctor C n ⋙ shiftFunctor C m) X)
    (NatTrans.app (Iso.hom (shiftFunctorComm C m n)) X)
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C m n hmn)) X ≫
      NatTrans.app (Iso.inv (shiftFunctorCompIsoId C n m ⋯)) X)

Tactic:
simp [shiftFunctorCompIsoId, shiftFunctorComm_eq C m n 0 hmn]

Premises used: CategoryTheory.shiftFunctorCompIsoId, CategoryTheory.shiftFunctorComm_eq, OfNat.ofNat
-- 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
m n : A
hmn : m + n = 0
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C n ⋙ shiftFunctor C m) X ⟶ obj.{v, v, u, u} (shiftFunctor C m ⋙ shiftFunctor C n) X)
    (NatTrans.app (Iso.inv (shiftFunctorComm C m n)) X)
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C n m ⋯)) X ≫
      NatTrans.app (Iso.inv (shiftFunctorCompIsoId C m n hmn)) X)

Tactic:
simp [shiftFunctorCompIsoId, shiftFunctorComm_eq C m n 0 hmn]

Premises used: CategoryTheory.shiftFunctorCompIsoId, CategoryTheory.shiftFunctorComm_eq, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
D : Type u_2
inst_1 : Category.{v_1, u_2} D
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_1} D A
F : Functor.{v, v_1, u, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v, v, u, u} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
X : C
⊢ F.map ((zero hF s i).hom.app X) =
    NatTrans.app (Iso.hom (i 0)) X ≫ NatTrans.app (Iso.hom (shiftFunctorZero D A)) (F.obj X)

Tactic:
simp [zero]

Premises used: CategoryTheory.Functor.FullyFaithful.hasShift.zero
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
D : Type u_2
inst_1 : Category.{v_1, u_2} D
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_1} D A
F : Functor.{v, v_1, u, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v, v, u, u} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
X : C
⊢ F.map ((zero hF s i).inv.app X) =
    NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X) ≫ NatTrans.app (Iso.inv (i 0)) X

Tactic:
simp [zero]

Premises used: CategoryTheory.Functor.FullyFaithful.hasShift.zero
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
D : Type u_2
inst_1 : Category.{v_1, u_2} D
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_1} D A
F : Functor.{v, v_1, u, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v, v, u, u} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
a b : A
X : C
dsimp :
  F.map
      (hF.preimage
        (NatTrans.app (Iso.hom (i (a + b))) X ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd D a b)) (F.obj X) ≫
            𝟙 (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D b) (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D a) (F.obj X))) ≫
              map (shiftFunctor D b) ((i a).inv.app X) ≫
                𝟙 (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D b) (F.obj ((s a).obj X))) ≫
                  (i b).inv.app ((s a).obj X) ≫ 𝟙 (F.obj ((s b).obj ((s a).obj X))))) =
    NatTrans.app (Iso.hom (i (a + b))) X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd D a b)) (F.obj X) ≫
        map (shiftFunctor D b) ((i a).inv.app X) ≫ (i b).inv.app ((s a).obj X)
⊢ F.map ((add hF s i a b).hom.app X) =
    NatTrans.app (Iso.hom (i (a + b))) X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd D a b)) (F.obj X) ≫
        map (shiftFunctor D b) ((i a).inv.app X) ≫ (i b).inv.app ((s a).obj X)

Tactic:
dsimp [add]

Premises used: CategoryTheory.Functor.FullyFaithful.hasShift.add
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
D : Type u_2
inst_1 : Category.{v_1, u_2} D
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_1} D A
F : Functor.{v, v_1, u, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v, v, u, u} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
a b : A
X : C
⊢ F.map
      (hF.preimage
        (NatTrans.app (Iso.hom (i (a + b))) X ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd D a b)) (F.obj X) ≫
            𝟙 (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D b) (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D a) (F.obj X))) ≫
              map (shiftFunctor D b) ((i a).inv.app X) ≫
                𝟙 (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D b) (F.obj ((s a).obj X))) ≫
                  (i b).inv.app ((s a).obj X) ≫ 𝟙 (F.obj ((s b).obj ((s a).obj X))))) =
    NatTrans.app (Iso.hom (i (a + b))) X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd D a b)) (F.obj X) ≫
        map (shiftFunctor D b) ((i a).inv.app X) ≫ (i b).inv.app ((s a).obj X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
D : Type u_2
inst_1 : Category.{v_1, u_2} D
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_1} D A
F : Functor.{v, v_1, u, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v, v, u, u} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
a b : A
X : C
dsimp :
  F.map
      (hF.preimage
        ((((((𝟙 (F.obj ((s b).obj ((s a).obj X))) ≫ (i b).hom.app ((s a).obj X)) ≫
                  𝟙 (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D b) (F.obj ((s a).obj X)))) ≫
                map (shiftFunctor D b) ((i a).hom.app X)) ≫
              𝟙 (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D b) (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D a) (F.obj X)))) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X)) ≫
          NatTrans.app (Iso.inv (i (a + b))) X)) =
    (i b).hom.app ((s a).obj X) ≫
      map (shiftFunctor D b) ((i a).hom.app X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
⊢ F.map ((add hF s i a b).inv.app X) =
    (i b).hom.app ((s a).obj X) ≫
      map (shiftFunctor D b) ((i a).hom.app X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X) ≫ NatTrans.app (Iso.inv (i (a + b))) X

Tactic:
dsimp [add]

Premises used: CategoryTheory.Functor.FullyFaithful.hasShift.add
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
D : Type u_2
inst_1 : Category.{v_1, u_2} D
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_1} D A
F : Functor.{v, v_1, u, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v, v, u, u} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
a b : A
X : C
⊢ F.map
      (hF.preimage
        ((((((𝟙 (F.obj ((s b).obj ((s a).obj X))) ≫ (i b).hom.app ((s a).obj X)) ≫
                  𝟙 (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D b) (F.obj ((s a).obj X)))) ≫
                map (shiftFunctor D b) ((i a).hom.app X)) ≫
              𝟙 (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D b) (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D a) (F.obj X)))) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X)) ≫
          NatTrans.app (Iso.inv (i (a + b))) X)) =
    (i b).hom.app ((s a).obj X) ≫
      map (shiftFunctor D b) ((i a).hom.app X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X) ≫ NatTrans.app (Iso.inv (i (a + b))) X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
D : Type u_2
inst_1 : Category.{v_1, u_2} D
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_1} D A
F : Functor.{v, v_1, u, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v, v, u, u} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
m₁ m₂ m₃ : A
X : C
⊢ Eq.{v_1 + 1} (α :=
    obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₃)
        (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁ ⋙ shiftFunctor D m₂) (F.obj X)))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' D (m₁ + m₂) m₃ (m₁ + m₂ + m₃) ⋯)) (F.obj X) ≫
        map (shiftFunctor D m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd' D m₁ m₂ (m₁ + m₂) ⋯)) (F.obj X)) :
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
        obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₃)
          (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁ ⋙ shiftFunctor D m₂) (F.obj X)))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯)) (F.obj X) ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' D m₂ m₃ (m₂ + m₃) ⋯))
          (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)) :
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
        obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₂ ⋙ shiftFunctor D m₃)
          (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)))

Tactic:
have h := shiftFunctorAdd'_assoc_hom_app m₁ m₂ m₃ _ _ (m₁ + m₂ + m₃) rfl rfl rfl (F.obj X)
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
D : Type u_2
inst_1 : Category.{v_1, u_2} D
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_1} D A
F : Functor.{v, v_1, u, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v, v, u, u} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
m₁ m₂ m₃ : A
X : C
h :
  Eq.{v_1 + 1} (α :=
    obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₃)
        (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁ ⋙ shiftFunctor D m₂) (F.obj X)))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' D (m₁ + m₂) m₃ (m₁ + m₂ + m₃) ⋯)) (F.obj X) ≫
        map (shiftFunctor D m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd' D m₁ m₂ (m₁ + m₂) ⋯)) (F.obj X)) :
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
        obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₃)
          (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁ ⋙ shiftFunctor D m₂) (F.obj X)))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯)) (F.obj X) ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' D m₂ m₃ (m₂ + m₃) ⋯))
          (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)) :
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
        obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₂ ⋙ shiftFunctor D m₃)
          (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)))
⊢ Eq.{v_1 + 1} (α :=
    obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₃)
        (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁ ⋙ shiftFunctor D m₂) (F.obj X)))
    (NatTrans.app (Iso.hom (shiftFunctorAdd D (m₁ + m₂) m₃)) (F.obj X) ≫
        map (shiftFunctor D m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd D m₁ m₂)) (F.obj X)) :
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
        obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₃)
          (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁ ⋙ shiftFunctor D m₂) (F.obj X)))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯)) (F.obj X) ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd D m₂ m₃)) (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)) :
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
        obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₂ ⋙ shiftFunctor D m₃)
          (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)))

Tactic:
simp only [shiftFunctorAdd'_eq_shiftFunctorAdd] at h

Premises used: CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
D : Type u_2
inst_1 : Category.{v_1, u_2} D
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_1} D A
F : Functor.{v, v_1, u, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v, v, u, u} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
m₁ m₂ m₃ : A
X : C
h :
  Eq.{v_1 + 1} (α :=
    obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₃)
        (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁ ⋙ shiftFunctor D m₂) (F.obj X)))
    (NatTrans.app (Iso.hom (shiftFunctorAdd D (m₁ + m₂) m₃)) (F.obj X) ≫
        map (shiftFunctor D m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd D m₁ m₂)) (F.obj X)) :
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
        obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₃)
          (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁ ⋙ shiftFunctor D m₂) (F.obj X)))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯)) (F.obj X) ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd D m₂ m₃)) (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)) :
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
        obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₂ ⋙ shiftFunctor D m₃)
          (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)))
rw :
  F.map (NatTrans.app (Iso.hom (add hF s i (m₁ + m₂) m₃)) X ≫ (s m₃).map ((add hF s i m₁ m₂).hom.app X)) ≫
      (i m₃).hom.app ((s m₂).obj ((s m₁).obj X)) =
    F.map (eqToHom ⋯ ≫ NatTrans.app (Iso.hom (add hF s i m₁ (m₂ + m₃))) X ≫ (add hF s i m₂ m₃).hom.app ((s m₁).obj X)) ≫
      (i m₃).hom.app ((s m₂).obj ((s m₁).obj X))
⊢ F.map (NatTrans.app (Iso.hom (add hF s i (m₁ + m₂) m₃)) X ≫ (s m₃).map ((add hF s i m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯ ≫ NatTrans.app (Iso.hom (add hF s i m₁ (m₂ + m₃))) X ≫ (add hF s i m₂ m₃).hom.app ((s m₁).obj X))

Tactic:
rw [← cancel_mono ((i m₃).hom.app ((s m₂).obj ((s m₁).obj X)))]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Iso.hom, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Shift.Basic
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
D : Type u_2
inst_1 : Category.{v_1, u_2} D
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_1} D A
F : Functor.{v, v_1, u, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v, v, u, u} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
m₁ m₂ m₃ : A
X : C
h :
  Eq.{v_1 + 1} (α :=
    obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₃)
        (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁ ⋙ shiftFunctor D m₂) (F.obj X)))
    (NatTrans.app (Iso.hom (shiftFunctorAdd D (m₁ + m₂) m₃)) (F.obj X) ≫
        map (shiftFunctor D m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd D m₁ m₂)) (F.obj X)) :
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
        obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₃)
          (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁ ⋙ shiftFunctor D m₂) (F.obj X)))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯)) (F.obj X) ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd D m₂ m₃)) (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)) :
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
        obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₂ ⋙ shiftFunctor D m₃)
          (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)))
simp :
  NatTrans.app (Iso.hom (i (m₁ + m₂ + m₃))) X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd D (m₁ + m₂) m₃)) (F.obj X) ≫
        map (shiftFunctor D m₃) (NatTrans.app (Iso.inv (i (m₁ + m₂))) X) ≫
          (i m₃).inv.app ((s (m₁ + m₂)).obj X) ≫
            F.map ((s m₃).map ((add hF s i m₁ m₂).hom.app X)) ≫ (i m₃).hom.app ((s m₂).obj ((s m₁).obj X)) =
    F.map (eqToHom ⋯) ≫
      NatTrans.app (Iso.hom (i (m₁ + (m₂ + m₃)))) X ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd D m₁ (m₂ + m₃))) (F.obj X) ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd D m₂ m₃)) (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)) ≫
            map (shiftFunctor D m₃) (map (shiftFunctor D m₂) ((i m₁).inv.app X)) ≫
              map (shiftFunctor D m₃) ((i m₂).inv.app ((s m₁).obj X))
⊢ F.map (NatTrans.app (Iso.hom (add hF s i (m₁ + m₂) m₃)) X ≫ (s m₃).map ((add hF s i m₁ m₂).hom.app X)) ≫
      (i m₃).hom.app ((s m₂).obj ((s m₁).obj X)) =
    F.map (eqToHom ⋯ ≫ NatTrans.app (Iso.hom (add hF s i m₁ (m₂ + m₃))) X ≫ (add hF s i m₂ m₃).hom.app ((s m₁).obj X)) ≫
      (i m₃).hom.app ((s m₂).obj ((s m₁).obj X))

Tactic:
simp only [Functor.comp_obj, Functor.map_comp, map_add_hom_app,
          Category.assoc, Iso.inv_hom_id_app_assoc, NatTrans.naturality_assoc, Functor.comp_map,
          Iso.inv_hom_id_app, Category.comp_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Functor.FullyFaithful.hasShift.map_add_hom_app, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Iso.inv_hom_id_app_assoc, CategoryTheory.Functor.comp_map, CategoryTheory.NatTrans.naturality_assoc