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
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)))
erw :
  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) ≫
            (i m₃).hom.app ((s (m₁ + m₂)).obj X) ≫ (F ⋙ shiftFunctor D m₃).map ((add hF s i m₁ m₂).hom.app 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))
⊢ 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))

Tactic:
erw [(i m₃).hom.naturality]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom
-- 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)))
⊢ Eq.{v_1 + 1} (α :=
    F.obj ((s (m₁ + m₂ + m₃)).obj X) ⟶ obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₃) (F.obj ((s m₂).obj ((s m₁).obj X))))
    (CategoryStruct.comp (Y := obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X))
        (CategoryStruct.comp (Y := (s (m₁ + (m₂ + m₃)) ⋙ F).obj X) (eqToHom ⋯)
          (NatTrans.app (Iso.hom (i (m₁ + (m₂ + m₃)))) X ≫ eqToHom ⋯))
        (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)) ≫
            map (shiftFunctor D m₃) (map (shiftFunctor D m₂) ((i m₁).inv.app X) ≫ (i m₂).inv.app ((s m₁).obj X))) :
      F.obj ((s (m₁ + m₂ + m₃)).obj X) ⟶
        obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₃) (F.obj ((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.obj ((s (m₁ + m₂ + m₃)).obj X) ⟶
        obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₃) (F.obj ((s m₂).obj ((s m₁).obj X))))

Tactic:
simp [shiftFunctorAdd', eqToHom_map]

Premises used: CategoryTheory.eqToHom_map, CategoryTheory.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
n : A
X : C
⊢ Eq (α := (s (0 + n) ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D (0 + n)).obj X) (NatTrans.app (Iso.hom (i (0 + n))) X)
    (eqToHom ⋯ ≫ (i n).hom.app X ≫ eqToHom ⋯)

Tactic:
have this := dcongr_arg (fun a => (i a).hom.app X) (zero_add n)
-- 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
n : A
X : C
this :
  Eq (α := (s (0 + n) ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D (0 + n)).obj X) (NatTrans.app (Iso.hom (i (0 + n))) X)
    (eqToHom ⋯ ≫ (i n).hom.app X ≫ eqToHom ⋯)
rw :
  F.map (NatTrans.app (Iso.hom (add hF s i 0 n)) X) ≫ (i n).hom.app ((s 0).obj X) =
    F.map (eqToHom ⋯ ≫ (s n).map ((zero hF s i).inv.app X)) ≫ (i n).hom.app ((s 0).obj X)
⊢ F.map (NatTrans.app (Iso.hom (add hF s i 0 n)) X) = F.map (eqToHom ⋯ ≫ (s n).map ((zero hF s i).inv.app X))

Tactic:
rw [← cancel_mono ((i n).hom.app ((s 0).obj X))]

Premises used: CategoryTheory.cancel_mono, OfNat.ofNat, 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
n : A
X : C
this :
  Eq (α := (s (0 + n) ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D (0 + n)).obj X) (NatTrans.app (Iso.hom (i (0 + n))) X)
    (eqToHom ⋯ ≫ (i n).hom.app X ≫ eqToHom ⋯)
simp :
  Eq.{v_1 + 1} (α := F.obj ((s (0 + n)).obj X) ⟶ obj.{v_1, v_1, u_2, u_2} (shiftFunctor D n) (F.obj ((s 0).obj X)))
    (eqToHom ⋯ ≫
        (i n).hom.app X ≫
          map (shiftFunctor D n) (NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X)) ≫
            map (shiftFunctor D n) (NatTrans.app (Iso.inv (i 0)) X) :
      F.obj ((s (0 + n)).obj X) ⟶ obj.{v_1, v_1, u_2, u_2} (shiftFunctor D n) (F.obj ((s 0).obj X)))
    (eqToHom ⋯ ≫ F.map ((s n).map ((zero hF s i).inv.app X)) ≫ (i n).hom.app ((s 0).obj X) :
      F.obj ((s (0 + n)).obj X) ⟶ obj.{v_1, v_1, u_2, u_2} (shiftFunctor D n) (F.obj ((s 0).obj X)))
⊢ F.map (NatTrans.app (Iso.hom (add hF s i 0 n)) X) ≫ (i n).hom.app ((s 0).obj X) =
    F.map (eqToHom ⋯ ≫ (s n).map ((zero hF s i).inv.app X)) ≫ (i n).hom.app ((s 0).obj X)

Tactic:
simp only [comp_obj, map_add_hom_app, this, shiftFunctorAdd_zero_add_hom_app, id_obj,
          Category.assoc, eqToHom_trans_assoc, eqToHom_refl, Category.id_comp, Iso.inv_hom_id_app,
          Category.comp_id, map_comp, eqToHom_map]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.eqToHom_map, CategoryTheory.shiftFunctorAdd_zero_add_hom_app, CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, CategoryTheory.Functor.FullyFaithful.hasShift.map_add_hom_app, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.map_comp, CategoryTheory.eqToHom_trans_assoc, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Category.id_comp
-- 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
n : A
X : C
this :
  Eq (α := (s (0 + n) ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D (0 + n)).obj X) (NatTrans.app (Iso.hom (i (0 + n))) X)
    (eqToHom ⋯ ≫ (i n).hom.app X ≫ eqToHom ⋯)
e_a :
  (i n).hom.app X ≫
      map (shiftFunctor D n) (NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X)) ≫
        map (shiftFunctor D n) (NatTrans.app (Iso.inv (i 0)) X) =
    F.map ((s n).map ((zero hF s i).inv.app X)) ≫ (i n).hom.app ((s 0).obj X)
⊢ Eq.{v_1 + 1} (α := F.obj ((s (0 + n)).obj X) ⟶ obj.{v_1, v_1, u_2, u_2} (shiftFunctor D n) (F.obj ((s 0).obj X)))
    (eqToHom ⋯ ≫
        (i n).hom.app X ≫
          map (shiftFunctor D n) (NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X)) ≫
            map (shiftFunctor D n) (NatTrans.app (Iso.inv (i 0)) X) :
      F.obj ((s (0 + n)).obj X) ⟶ obj.{v_1, v_1, u_2, u_2} (shiftFunctor D n) (F.obj ((s 0).obj X)))
    (eqToHom ⋯ ≫ F.map ((s n).map ((zero hF s i).inv.app X)) ≫ (i n).hom.app ((s 0).obj X) :
      F.obj ((s (0 + n)).obj X) ⟶ obj.{v_1, v_1, u_2, u_2} (shiftFunctor D n) (F.obj ((s 0).obj X)))

Tactic:
congr 1
-- 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
n : A
X : C
this :
  Eq (α := (s (0 + n) ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D (0 + n)).obj X) (NatTrans.app (Iso.hom (i (0 + n))) X)
    (eqToHom ⋯ ≫ (i n).hom.app X ≫ eqToHom ⋯)
e_a :
  (i n).hom.app X ≫
      map (shiftFunctor D n) (NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X)) ≫
        map (shiftFunctor D n) (NatTrans.app (Iso.inv (i 0)) X) =
    (i n).hom.app X ≫ (F ⋙ shiftFunctor D n).map ((zero hF s i).inv.app X)
⊢ (i n).hom.app X ≫
      map (shiftFunctor D n) (NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X)) ≫
        map (shiftFunctor D n) (NatTrans.app (Iso.inv (i 0)) X) =
    F.map ((s n).map ((zero hF s i).inv.app X)) ≫ (i n).hom.app ((s 0).obj X)

Tactic:
erw [(i n).hom.naturality]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom
-- 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
n : A
X : C
this :
  Eq (α := (s (0 + n) ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D (0 + n)).obj X) (NatTrans.app (Iso.hom (i (0 + n))) X)
    (eqToHom ⋯ ≫ (i n).hom.app X ≫ eqToHom ⋯)
⊢ (i n).hom.app X ≫
      map (shiftFunctor D n) (NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X)) ≫
        map (shiftFunctor D n) (NatTrans.app (Iso.inv (i 0)) X) =
    (i n).hom.app X ≫ (F ⋙ shiftFunctor D n).map ((zero hF s i).inv.app 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
n : A
X : C
⊢ Eq (α := (s (n + 0) ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D (n + 0)).obj X) (NatTrans.app (Iso.hom (i (n + 0))) X)
    (eqToHom ⋯ ≫ (i n).hom.app X ≫ eqToHom ⋯)

Tactic:
have := dcongr_arg (fun a => (i a).hom.app X) (add_zero n)
-- 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
n : A
X : C
this :
  Eq (α := (s (n + 0) ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D (n + 0)).obj X) (NatTrans.app (Iso.hom (i (n + 0))) X)
    (eqToHom ⋯ ≫ (i n).hom.app X ≫ eqToHom ⋯)
⊢ F.map (NatTrans.app (Iso.hom (add hF s i n 0)) X) = F.map (eqToHom ⋯ ≫ (zero hF s i).inv.app ((s n).obj X))

Tactic:
simp [this, ← NatTrans.naturality_assoc, eqToHom_map,
          shiftFunctorAdd_add_zero_hom_app]

Premises used: CategoryTheory.eqToHom_map, CategoryTheory.shiftFunctorAdd_add_zero_hom_app, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
w :
  ∀ (x : C),
    Eq (α :=
      (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0 ⋙ F).obj x ⟶ (F ⋙ shiftFunctor.{v_2, u_2, u_4} D (A := A) 0).obj x)
      (NatTrans.app (Iso.hom (isoZero' F A 0 ⋯)) x) (NatTrans.app (Iso.hom (isoZero F A)) x)
⊢ Eq (α := shiftFunctor.{v_1, u_1, u_4} C (A := A) 0 ⋙ F ≅ F ⋙ shiftFunctor.{v_2, u_2, u_4} D (A := A) 0)
    (isoZero' F A 0 ⋯) (isoZero F A)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
x : C
⊢ Eq (α :=
    (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0 ⋙ F).obj x ⟶ (F ⋙ shiftFunctor.{v_2, u_2, u_4} D (A := A) 0).obj x)
    (NatTrans.app (Iso.hom (isoZero' F A 0 ⋯)) x) (NatTrans.app (Iso.hom (isoZero F A)) x)

Tactic:
simp [isoZero', shiftFunctorZero']

Premises used: CategoryTheory.Functor.CommShift.isoZero', CategoryTheory.shiftFunctorZero'
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
X : C
⊢ (isoAdd e₁ e₂).hom.app X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      e₂.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        map (shiftFunctor D b) (e₁.hom.app X) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X)

Tactic:
simp only [isoAdd, isoAdd'_hom_app, shiftFunctorAdd'_eq_shiftFunctorAdd]

Premises used: CategoryTheory.Functor.CommShift.isoAdd, CategoryTheory.Functor.CommShift.isoAdd'_hom_app, CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
X : C
⊢ (isoAdd e₁ e₂).inv.app X =
    NatTrans.app (Iso.hom (shiftFunctorAdd D a b)) (F.obj X) ≫
      map (shiftFunctor D b) (e₁.inv.app X) ≫
        e₂.inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
          F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X)

Tactic:
simp only [isoAdd, isoAdd'_inv_app, shiftFunctorAdd'_eq_shiftFunctorAdd]

Premises used: CategoryTheory.Functor.CommShift.isoAdd, CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd, CategoryTheory.Functor.CommShift.isoAdd'_inv_app
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
a : A
e : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
w : ∀ (X : C), NatTrans.app (Iso.hom (isoAdd' ⋯ e (isoZero F A))) X = e.hom.app X
⊢ isoAdd' ⋯ e (isoZero F A) = e

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
a : A
e : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
X : C
⊢ NatTrans.app (Iso.hom (isoAdd' ⋯ e (isoZero F A))) X = e.hom.app X

Tactic:
simp [shiftFunctorAdd'_add_zero_hom_app, ← Functor.map_comp_assoc,
    shiftFunctorAdd'_add_zero_inv_app]

Premises used: CategoryTheory.shiftFunctorAdd'_add_zero_inv_app, CategoryTheory.shiftFunctorAdd'_add_zero_hom_app, CategoryTheory.Functor.map_comp_assoc
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
a : A
e : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
w : ∀ (X : C), NatTrans.app (Iso.hom (isoAdd' ⋯ (isoZero F A) e)) X = e.hom.app X
⊢ isoAdd' ⋯ (isoZero F A) e = e

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
a : A
e : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
X : C
⊢ Eq (α :=
    (shiftFunctor C a ⋙ F).obj (obj.{v_1, v_1, u_1, u_1} (𝟭 C) X) ⟶
      (F ⋙ shiftFunctor D a).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0) X))
    ((shiftFunctor C a ⋙ F).map (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X) ≫
      e.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0) X))
    (e.hom.app (obj.{v_1, v_1, u_1, u_1} (𝟭 C) X) ≫
      (F ⋙ shiftFunctor D a).map (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X))

Tactic:
have := e.hom.naturality ((shiftFunctorZero C A).inv.app X)
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
a : A
e : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
X : C
this :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a)
        (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0) X)))
    (F.map (map (shiftFunctor C a) (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X)) ≫
      e.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0) X))
    (e.hom.app X ≫ map (shiftFunctor D a) (F.map (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X)))
⊢ NatTrans.app (Iso.hom (isoAdd' ⋯ (isoZero F A) e)) X = e.hom.app X

Tactic:
simp [shiftFunctorAdd'_zero_add_hom_app,
    shiftFunctorAdd'_zero_add_inv_app, ← map_comp,
    reassoc_of% this]

Premises used: CategoryTheory.shiftFunctorAdd'_zero_add_inv_app, CategoryTheory.shiftFunctorAdd'_zero_add_hom_app, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
A : Type u_4
B : Type u_5
inst_3 : AddMonoid A
inst_4 : AddCommMonoid B
inst_5 : HasShift.{v_1, u_1, u_4} C A
inst_6 : HasShift.{v_2, u_2, u_4} D A
inst_7 : HasShift.{v_3, u_3, u_4} E A
inst_8 : HasShift.{v_1, u_1, u_5} C B
inst_9 : HasShift.{v_2, u_2, u_5} D B
a b c ab bc abc : A
ea : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
eb : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
ec : shiftFunctor C c ⋙ F ≅ F ⋙ shiftFunctor D c
hab : a + b = ab
hbc : b + c = bc
h rwa rwa₁ rwa₂ rwa₃ : a + b + c = abc
⊢ ab + c = abc

Tactic:
rwa [← hab]
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
A : Type u_4
B : Type u_5
inst_3 : AddMonoid A
inst_4 : AddCommMonoid B
inst_5 : HasShift.{v_1, u_1, u_4} C A
inst_6 : HasShift.{v_2, u_2, u_4} D A
inst_7 : HasShift.{v_3, u_3, u_4} E A
inst_8 : HasShift.{v_1, u_1, u_5} C B
inst_9 : HasShift.{v_2, u_2, u_5} D B
a b c ab bc abc : A
ea : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
eb : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
ec : shiftFunctor C c ⋙ F ≅ F ⋙ shiftFunctor D c
hab : a + b = ab
hbc : b + c = bc
h : a + b + c = abc
⊢ a + bc = abc

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
a b c ab bc abc : A
ea : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
eb : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
ec : shiftFunctor C c ⋙ F ≅ F ⋙ shiftFunctor D c
hab : a + b = ab
hbc : b + c = bc
h : a + b + c = abc
w :
  ∀ (X : C),
    Eq (α := (shiftFunctor C abc ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D abc).obj X)
      (NatTrans.app (Iso.hom (isoAdd' ⋯ (isoAdd' hab ea eb) ec)) X)
      (NatTrans.app (Iso.hom (isoAdd' ⋯ ea (isoAdd' hbc eb ec))) X)
⊢ Eq (α := shiftFunctor C abc ⋙ F ≅ F ⋙ shiftFunctor D abc) (isoAdd' ⋯ (isoAdd' hab ea eb) ec)
    (isoAdd' ⋯ ea (isoAdd' hbc eb ec))

Tactic:
ext X