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
X Y : C
f : X ⟶ Y
i j : A
erw :
  Eq (α :=
    obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) Y))
    (map (shiftFunctor C j) (map (shiftFunctor C i) f))
    (map (shiftFunctor C i ⋙ shiftFunctor C j) f ≫
      NatTrans.app (Iso.hom (shiftFunctorComm C i j)) Y ≫ Iso.hom (Iso.symm (shiftComm Y i j)))
⊢ Eq (α :=
    obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) Y))
    (map (shiftFunctor C j) (map (shiftFunctor C i) f))
    (Iso.hom (shiftComm X i j) ≫ map (shiftFunctor C i) (map (shiftFunctor C j) f) ≫ Iso.hom (shiftComm Y j i))

Tactic:
erw [← shiftComm_symm Y i j, ← ((shiftFunctorComm C i j).hom.naturality_assoc f)]

Premises used: CategoryTheory.shiftFunctorComm, CategoryTheory.shiftComm_symm, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.naturality_assoc
-- 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 Y : C
f : X ⟶ Y
i j : A
dsimp :
  Eq (α :=
    obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) Y))
    (map (shiftFunctor C j) (map (shiftFunctor C i) f))
    (map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫
      NatTrans.app (Iso.hom (shiftFunctorComm C i j)) Y ≫ NatTrans.app (Iso.inv (shiftFunctorComm C i j)) Y)
⊢ Eq (α :=
    obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) Y))
    (map (shiftFunctor C j) (map (shiftFunctor C i) f))
    (map (shiftFunctor C i ⋙ shiftFunctor C j) f ≫
      NatTrans.app (Iso.hom (shiftFunctorComm C i j)) Y ≫ Iso.hom (Iso.symm (shiftComm Y i j)))

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
X Y : C
f : X ⟶ Y
i j : A
⊢ Eq (α :=
    obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) Y))
    (map (shiftFunctor C j) (map (shiftFunctor C i) f))
    (map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫
      NatTrans.app (Iso.hom (shiftFunctorComm C i j)) Y ≫ NatTrans.app (Iso.inv (shiftFunctorComm C i j)) Y)

Tactic:
simp only [Iso.hom_inv_id_app, Functor.comp_obj, Category.comp_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Category.comp_id
-- 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 Y : C
f : X ⟶ Y
i j : A
rw :
  Eq (α :=
    obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C i) (obj.{v, v, u, u} (shiftFunctor C j) Y))
    (Iso.hom (shiftComm X i j) ≫
      Iso.hom (shiftComm X j i) ≫ map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
    (map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
rw₁ :
  Eq (α :=
    obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C i) (obj.{v, v, u, u} (shiftFunctor C j) Y))
    (Iso.hom (Iso.symm (shiftComm X j i)) ≫
      Iso.hom (shiftComm X j i) ≫ map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
    (map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
rw₂ :
  Eq (α :=
    obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C i) (obj.{v, v, u, u} (shiftFunctor C j) Y))
    (Iso.inv (shiftComm X j i) ≫
      Iso.hom (shiftComm X j i) ≫ map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
    (map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
rw₃ rw₄ :
  Eq (α :=
    obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C i) (obj.{v, v, u, u} (shiftFunctor C j) Y))
    (map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
    (map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))
⊢ Eq (α :=
    obj.{v, v, u, u} (shiftFunctor C j) (obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C i) (obj.{v, v, u, u} (shiftFunctor C j) Y))
    (Iso.hom (shiftComm X i j) ≫ map (shiftFunctor C i) (map (shiftFunctor C j) f))
    (map (shiftFunctor C j) (map (shiftFunctor C i) f) ≫ Iso.hom (shiftComm Y i j))

Tactic:
rw [shiftComm', ← shiftComm_symm, Iso.symm_hom, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Iso.symm_hom, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.shiftComm', CategoryTheory.shiftComm_symm
-- 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
n : A
rw :
  Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) (obj.{v, v, u, u} (shiftFunctor C n) X) ⟶
      obj.{v, v, u, u} (𝟭 C) (obj.{v, v, u, u} (shiftFunctor C n) X))
    (NatTrans.app (Iso.hom (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n) X))
    (CategoryStruct.comp (Y := obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0 ⋙ shiftFunctor C n) X)
      (NatTrans.app (Iso.hom (Iso.symm (shiftFunctorAdd' C n 0 n ⋯) ≪≫ shiftFunctorAdd' C 0 n n ⋯)) X)
      (NatTrans.app (Iso.inv (shiftFunctorAdd' C 0 n n ⋯)) X))
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) (obj.{v, v, u, u} (shiftFunctor C n) X) ⟶
      obj.{v, v, u, u} (𝟭 C) (obj.{v, v, u, u} (shiftFunctor C n) X))
    (NatTrans.app (Iso.hom (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n) X))
    (NatTrans.app (Iso.hom (shiftFunctorComm C n 0)) X ≫
      map (shiftFunctor C n) (NatTrans.app (Iso.hom (shiftFunctorZero C A)) X))

Tactic:
rw [← shiftFunctorAdd'_zero_add_inv_app n X, shiftFunctorComm_eq C n 0 n (add_zero n)]

Premises used: CategoryTheory.shiftFunctorAdd'_zero_add_inv_app, CategoryTheory.shiftFunctorComm_eq, add_zero, 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
X : C
n : A
dsimp :
  Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) (obj.{v, v, u, u} (shiftFunctor C n) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C n) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n) X))
    (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) X))
      (NatTrans.app (Iso.inv (shiftFunctorAdd' C n 0 n ⋯)) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd' C 0 n n ⋯)) X)
      (NatTrans.app (Iso.inv (shiftFunctorAdd' C 0 n n ⋯)) X))
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) (obj.{v, v, u, u} (shiftFunctor C n) X) ⟶
      obj.{v, v, u, u} (𝟭 C) (obj.{v, v, u, u} (shiftFunctor C n) X))
    (NatTrans.app (Iso.hom (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n) X))
    (CategoryStruct.comp (Y := obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0 ⋙ shiftFunctor C n) X)
      (NatTrans.app (Iso.hom (Iso.symm (shiftFunctorAdd' C n 0 n ⋯) ≪≫ shiftFunctorAdd' C 0 n n ⋯)) X)
      (NatTrans.app (Iso.inv (shiftFunctorAdd' C 0 n n ⋯)) 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
X : C
n : A
rw :
  Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) (obj.{v, v, u, u} (shiftFunctor C n) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C n) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n) X))
    (NatTrans.app (Iso.inv (shiftFunctorAdd' C n 0 n ⋯)) 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) X))
        (NatTrans.app (Iso.hom (shiftFunctorAdd' C 0 n n ⋯)) X) (NatTrans.app (Iso.inv (shiftFunctorAdd' C 0 n n ⋯)) X))
rw₁ :
  NatTrans.app (Iso.hom (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n) X) =
    NatTrans.app (Iso.inv (shiftFunctorAdd' C n 0 n ⋯)) X ≫ 𝟙 (obj.{v, v, u, u} (shiftFunctor C n) X)
rw₂ :
  Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) (obj.{v, v, u, u} (shiftFunctor C n) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C n) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n) X))
    (NatTrans.app (Iso.inv (shiftFunctorAdd' C n 0 n ⋯)) X)
rw₃ rw₄ :
  Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) (obj.{v, v, u, u} (shiftFunctor C n) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C n) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n) X))
    (NatTrans.app (Iso.hom (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n) X))
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) (obj.{v, v, u, u} (shiftFunctor C n) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C n) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n) X))
    (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) X))
      (NatTrans.app (Iso.inv (shiftFunctorAdd' C n 0 n ⋯)) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd' C 0 n n ⋯)) X)
      (NatTrans.app (Iso.inv (shiftFunctorAdd' C 0 n n ⋯)) X))

Tactic:
rw [Category.assoc, Iso.hom_inv_id_app, Category.comp_id, shiftFunctorAdd'_add_zero_inv_app]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.shiftFunctorAdd'_add_zero_inv_app, CategoryTheory.Category.comp_id
-- 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
n : A
rw :
  𝟙 (obj.{v, v, u, u} (𝟭 C) (obj.{v, v, u, u} (shiftFunctor C n) X)) =
    map (shiftFunctor C n) (𝟙 (obj.{v, v, u, u} (𝟭 C) X))
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (𝟭 C) (obj.{v, v, u, u} (shiftFunctor C n) X) ⟶
      obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) (obj.{v, v, u, u} (shiftFunctor C n) X))
    (NatTrans.app (Iso.inv (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n) X))
    (map (shiftFunctor C n) (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X) ≫
      NatTrans.app (Iso.inv (shiftFunctorComm C n 0)) X)

Tactic:
rw [← cancel_mono ((shiftFunctorZero C A).hom.app (X⟦n⟧)), Category.assoc, Iso.inv_hom_id_app,
    shiftFunctorZero_hom_app_shift, Iso.inv_hom_id_app_assoc, ← Functor.map_comp,
    Iso.inv_hom_id_app]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.shiftFunctor, CategoryTheory.shiftFunctorZero, CategoryTheory.cancel_mono, CategoryTheory.shiftFunctorZero_hom_app_shift, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv_hom_id_app_assoc, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.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 : C
n : A
dsimp : 𝟙 (obj.{v, v, u, u} (shiftFunctor C n) X) = map (shiftFunctor C n) (𝟙 X)
⊢ 𝟙 (obj.{v, v, u, u} (𝟭 C) (obj.{v, v, u, u} (shiftFunctor C n) X)) =
    map (shiftFunctor C n) (𝟙 (obj.{v, v, u, u} (𝟭 C) 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
X : C
n : A
rw rw₁ :
  Eq.{v + 1} (α := obj.{v, v, u, u} (shiftFunctor C n) X ⟶ obj.{v, v, u, u} (shiftFunctor C n) X)
    (𝟙 (obj.{v, v, u, u} (shiftFunctor C n) X)) (𝟙 (obj.{v, v, u, u} (shiftFunctor C n) X))
⊢ 𝟙 (obj.{v, v, u, u} (shiftFunctor C n) X) = map (shiftFunctor C n) (𝟙 X)

Tactic:
rw [Functor.map_id]

Premises used: CategoryTheory.Functor.map_id
-- 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
a : A
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C a ⋙ shiftFunctor.{v, u, u_1} C (A := A) 0) X ⟶
      obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0 ⋙ shiftFunctor C a) X)
    (NatTrans.app (Iso.hom (shiftFunctorComm C a 0)) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C a) X) ≫
      map (shiftFunctor C a) (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X))

Tactic:
simp only [shiftFunctorZero_hom_app_shift, Category.assoc, ← Functor.map_comp,
    Iso.hom_inv_id_app, Functor.map_id, Functor.comp_obj, Category.comp_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Category.comp_id, CategoryTheory.shiftFunctorZero_hom_app_shift, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp
-- 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 :
  Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C m₁ ⋙ shiftFunctor C (m₂ + m₃)) X ⟶
      obj.{v, v, u, u} (shiftFunctor C m₃) (obj.{v, v, u, u} (shiftFunctor C m₁ ⋙ 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))
    (CategoryStruct.comp (Y :=
      obj.{v, v, u, u} (shiftFunctor C m₃) (obj.{v, v, u, u} (shiftFunctor C m₂ ⋙ shiftFunctor C m₁) X))
      ((NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v, v, u, u} (shiftFunctor C m₁) X) ≫
          map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorComm C m₁ m₂)) X) ≫
            NatTrans.app (Iso.hom (shiftFunctorComm C m₁ m₃)) (obj.{v, v, u, u} (shiftFunctor C 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)))
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C m₁ ⋙ shiftFunctor C (m₂ + m₃)) X ⟶
      obj.{v, v, u, u} (shiftFunctor C m₁) (obj.{v, v, u, u} (shiftFunctor C m₂ ⋙ 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.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v, v, u, u} (shiftFunctor C m₁) X) ≫
      map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorComm C m₁ m₂)) X) ≫
        NatTrans.app (Iso.hom (shiftFunctorComm C m₁ m₃)) (obj.{v, v, u, u} (shiftFunctor C m₂) X))

Tactic:
rw [← cancel_mono ((shiftFunctorComm C m₁ m₃).inv.app (X⟦m₂⟧)),
    ← cancel_mono (((shiftFunctorComm C m₁ m₂).inv.app X)⟦m₃⟧')]

Premises used: CategoryTheory.shiftFunctorComm, CategoryTheory.shiftFunctor, CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.Iso.inv, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.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
m₁ m₂ m₃ : A
X : C
simp :
  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₃) (NatTrans.app (Iso.hom (shiftFunctorComm C m₁ m₂)) X) ≫
        𝟙 (obj.{v, v, u, u} (shiftFunctor C m₁ ⋙ shiftFunctor C m₃) (obj.{v, v, u, u} (shiftFunctor C m₂) X)) ≫
          map (shiftFunctor C m₃) (NatTrans.app (Iso.inv (shiftFunctorComm C m₁ m₂)) X)
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C m₁ ⋙ shiftFunctor C (m₂ + m₃)) X ⟶
      obj.{v, v, u, u} (shiftFunctor C m₃) (obj.{v, v, u, u} (shiftFunctor C m₁ ⋙ 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))
    (CategoryStruct.comp (Y :=
      obj.{v, v, u, u} (shiftFunctor C m₃) (obj.{v, v, u, u} (shiftFunctor C m₂ ⋙ shiftFunctor C m₁) X))
      ((NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v, v, u, u} (shiftFunctor C m₁) X) ≫
          map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorComm C m₁ m₂)) X) ≫
            NatTrans.app (Iso.hom (shiftFunctorComm C m₁ m₃)) (obj.{v, v, u, u} (shiftFunctor C 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)))

Tactic:
simp only [Category.assoc, Iso.hom_inv_id_app]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id_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
m₁ m₂ m₃ : A
X : C
dsimp :
  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₃) (NatTrans.app (Iso.hom (shiftFunctorComm C m₁ 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))) ≫
          map (shiftFunctor C m₃) (NatTrans.app (Iso.inv (shiftFunctorComm C m₁ 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₃) (NatTrans.app (Iso.hom (shiftFunctorComm C m₁ m₂)) X) ≫
        𝟙 (obj.{v, v, u, u} (shiftFunctor C m₁ ⋙ shiftFunctor C m₃) (obj.{v, v, u, u} (shiftFunctor C m₂) X)) ≫
          map (shiftFunctor C m₃) (NatTrans.app (Iso.inv (shiftFunctorComm C m₁ 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
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 (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₁ ⋙ 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₃) (NatTrans.app (Iso.hom (shiftFunctorComm C m₁ 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))) ≫
          map (shiftFunctor C m₃) (NatTrans.app (Iso.inv (shiftFunctorComm C m₁ m₂)) X)

Tactic:
simp only [Category.id_comp, ← Functor.map_comp, Iso.hom_inv_id_app]

Premises used: CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_comp
-- 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.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))))
⊢ 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₁ ⋙ shiftFunctor C m₂) X)))

Tactic:
dsimp