awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Shift.Induced
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_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
n : A
X : C
eq :
  Eq (α := (F ⋙ s (0 + n)).obj X ⟶ (shiftFunctor C (0 + n) ⋙ F).obj X) (NatTrans.app (Iso.hom (i (0 + n))) X)
    (eqToHom ⋯ ≫ (i n).hom.app X ≫ eqToHom ⋯)
a :
  Eq.{v_2 + 1} (α := (s (0 + n)).obj (F.obj X) ⟶ (s n).obj ((s 0).obj (F.obj X)))
    (eqToHom ⋯ ≫
        (F ⋙ s n).map (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X) ≫ (s n).map (NatTrans.app (Iso.inv (i 0)) X) :
      (F ⋙ s (0 + n)).obj X ⟶ (s n).obj ((F ⋙ s 0).obj X))
    (eqToHom ⋯ ≫
        (s n).map (F.map (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X)) ≫
          (s n).map (NatTrans.app (Iso.inv (i 0)) X) :
      (s (0 + n)).obj (F.obj X) ⟶ (s n).obj ((s 0).obj (F.obj X)))
⊢ Eq.{v_2 + 1} (α := (s (0 + n)).obj (F.obj X) ⟶ (s n).obj ((s 0).obj (F.obj X)))
    (eqToHom ⋯ ≫
        (i n).hom.app X ≫
          F.map (map (shiftFunctor C n) (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X)) ≫
            (i n).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0) X) ≫
              (s n).map (NatTrans.app (Iso.inv (i 0)) X) :
      (F ⋙ s (0 + n)).obj X ⟶ (s n).obj ((F ⋙ s 0).obj X))
    (eqToHom ⋯ ≫
        (s n).map (F.map (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X)) ≫
          (s n).map (NatTrans.app (Iso.inv (i 0)) X) :
      (s (0 + n)).obj (F.obj X) ⟶ (s n).obj ((s 0).obj (F.obj X)))

Tactic:
erw [← NatTrans.naturality_assoc, Iso.hom_inv_id_app_assoc]

Premises used: CategoryTheory.Iso.hom_inv_id_app_assoc, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Shift.Induced
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_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
n : A
X : C
eq :
  Eq (α := (F ⋙ s (0 + n)).obj X ⟶ (shiftFunctor C (0 + n) ⋙ F).obj X) (NatTrans.app (Iso.hom (i (0 + n))) X)
    (eqToHom ⋯ ≫ (i n).hom.app X ≫ eqToHom ⋯)
⊢ Eq.{v_2 + 1} (α := (s (0 + n)).obj (F.obj X) ⟶ (s n).obj ((s 0).obj (F.obj X)))
    (eqToHom ⋯ ≫
        (F ⋙ s n).map (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X) ≫ (s n).map (NatTrans.app (Iso.inv (i 0)) X) :
      (F ⋙ s (0 + n)).obj X ⟶ (s n).obj ((F ⋙ s 0).obj X))
    (eqToHom ⋯ ≫
        (s n).map (F.map (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X)) ≫
          (s n).map (NatTrans.app (Iso.inv (i 0)) X) :
      (s (0 + n)).obj (F.obj X) ⟶ (s n).obj ((s 0).obj (F.obj X)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Shift.Induced
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_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
n : A
rw : s n = s n ⋙ 𝟭 D
⊢ s (n + 0) = s n ⋙ 𝟭 D

Tactic:
rw [add_zero]

Premises used: add_zero
-- Module: Mathlib.CategoryTheory.Shift.Induced
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_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
n : A
⊢ s n = s n ⋙ 𝟭 D

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Shift.Induced
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_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
n : A
this :
  Eq (α := s (n + 0) ⟶ s n ⋙ s 0) (Iso.hom (Induced.add F s i n 0))
    (eqToHom ⋯ ≫ (s n).whiskerLeft (Induced.zero F s i).inv)
X : D
⊢ NatTrans.app (Iso.hom (Induced.add F s i n 0)) X = eqToHom ⋯ ≫ (Induced.zero F s i).inv.app ((s n).obj X)

Tactic:
simpa using NatTrans.congr_app this X

Premises used: CategoryTheory.NatTrans.congr_app
-- Module: Mathlib.CategoryTheory.Shift.Induced
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_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
n : A
suffices :
  Eq (α := s (n + 0) ⟶ s n ⋙ s 0) (Iso.hom (Induced.add F s i n 0))
    (eqToHom ⋯ ≫ (s n).whiskerLeft (Induced.zero F s i).inv)
⊢ ∀ (X : D), NatTrans.app (Iso.hom (Induced.add F s i n 0)) X = eqToHom ⋯ ≫ (Induced.zero F s i).inv.app ((s n).obj X)

Tactic:
suffices (Induced.add F s i n 0).hom =
            eqToHom (by rw [add_zero]; rfl) ≫ whiskerLeft (s n) (Induced.zero F s i).inv by
          intro X
          simpa using NatTrans.congr_app this X
-- Module: Mathlib.CategoryTheory.Shift.Induced
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_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
n : A
a :
  Eq (α := obj (obj (whiskeringLeft C D D) F) (s (n + 0)) ⟶ obj (obj (whiskeringLeft C D D) F) (s n ⋙ s 0))
    (map (obj (whiskeringLeft C D D) F) (Iso.hom (Induced.add F s i n 0)))
    (map (obj (whiskeringLeft C D D) F) (eqToHom ⋯ ≫ (s n).whiskerLeft (Induced.zero F s i).inv))
⊢ Eq (α := s (n + 0) ⟶ s n ⋙ s 0) (Iso.hom (Induced.add F s i n 0))
    (eqToHom ⋯ ≫ (s n).whiskerLeft (Induced.zero F s i).inv)

Tactic:
apply ((whiskeringLeft C D D).obj F).map_injective

Premises used: CategoryTheory.Functor.whiskeringLeft, CategoryTheory.Functor.map_injective, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Shift.Induced
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_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
n : A
a :
  ∀ (X : C),
    Eq (α :=
      (obj (obj (whiskeringLeft C D D) F) (s (n + 0))).obj X ⟶ (obj (obj (whiskeringLeft C D D) F) (s n ⋙ s 0)).obj X)
      (NatTrans.app (map (obj (whiskeringLeft C D D) F) (Iso.hom (Induced.add F s i n 0))) X)
      (NatTrans.app (map (obj (whiskeringLeft C D D) F) (eqToHom ⋯ ≫ (s n).whiskerLeft (Induced.zero F s i).inv)) X)
⊢ Eq (α := obj (obj (whiskeringLeft C D D) F) (s (n + 0)) ⟶ obj (obj (whiskeringLeft C D D) F) (s n ⋙ s 0))
    (map (obj (whiskeringLeft C D D) F) (Iso.hom (Induced.add F s i n 0)))
    (map (obj (whiskeringLeft C D D) F) (eqToHom ⋯ ≫ (s n).whiskerLeft (Induced.zero F s i).inv))

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Shift.Induced
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_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
n : A
X : C
a :
  Eq (α := (s (n + 0)).obj (F.obj X) ⟶ (s 0).obj ((s n).obj (F.obj X)))
    (NatTrans.app (Iso.hom (Induced.add F s i n 0)) (F.obj X))
    (CategoryStruct.comp (Y := (s n).obj (F.obj X)) (NatTrans.app (eqToHom ⋯) (F.obj X))
      ((Induced.zero F s i).inv.app ((s n).obj (F.obj X))))
⊢ Eq (α :=
    (obj (obj (whiskeringLeft C D D) F) (s (n + 0))).obj X ⟶ (obj (obj (whiskeringLeft C D D) F) (s n ⋙ s 0)).obj X)
    (NatTrans.app (map (obj (whiskeringLeft C D D) F) (Iso.hom (Induced.add F s i n 0))) X)
    (NatTrans.app (map (obj (whiskeringLeft C D D) F) (eqToHom ⋯ ≫ (s n).whiskerLeft (Induced.zero F s i).inv)) X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Shift.Induced
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_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
n : A
X : C
a :
  Eq.{v_2 + 1} (α := (F ⋙ s (n + 0)).obj X ⟶ (s 0).obj ((shiftFunctor C n ⋙ F).obj X))
    (eqToHom ⋯ ≫
        (i n).hom.app X ≫
          eqToHom ⋯ ≫
            F.map
                (eqToHom ⋯ ≫
                  NatTrans.app (Iso.inv (shiftFunctorZero C A)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)) ≫
              NatTrans.app (Iso.inv (i 0)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X) :
      (F ⋙ s (n + 0)).obj X ⟶ (s 0).obj ((shiftFunctor C n ⋙ F).obj X))
    (CategoryStruct.comp (Y := (s n).obj (F.obj X)) (NatTrans.app (eqToHom ⋯) (F.obj X))
        (map (𝟭 D) ((i n).hom.app X) ≫
          F.map (NatTrans.app (Iso.inv (shiftFunctorZero C A)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)) ≫
            NatTrans.app (Iso.inv (i 0)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)) :
      (F ⋙ s (n + 0)).obj X ⟶ (s 0).obj ((shiftFunctor C n ⋙ F).obj X))
⊢ Eq (α := (s (n + 0)).obj (F.obj X) ⟶ (s 0).obj ((s n).obj (F.obj X)))
    (NatTrans.app (Iso.hom (Induced.add F s i n 0)) (F.obj X))
    (CategoryStruct.comp (Y := (s n).obj (F.obj X)) (NatTrans.app (eqToHom ⋯) (F.obj X))
      ((Induced.zero F s i).inv.app ((s n).obj (F.obj X))))

Tactic:
erw [Induced.add_hom_app_obj, dcongr_arg (fun a => (i a).hom.app X) (add_zero n),
          ← cancel_mono ((s 0).map ((i n).hom.app X)), Category.assoc,
          Category.assoc, Category.assoc, Category.assoc, Category.assoc,
          Category.assoc, ← (s 0).map_comp, Iso.inv_hom_id_app, Functor.map_id, Category.comp_id,
          ← NatTrans.naturality, Induced.zero_inv_app_obj,
          shiftFunctorAdd_add_zero_hom_app]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.HasShift.Induced.zero_inv_app_obj, CategoryTheory.HasShift.Induced.add_hom_app_obj, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map, CategoryTheory.Functor.map_id, CategoryTheory.NatTrans.naturality, CategoryTheory.shiftFunctorAdd_add_zero_hom_app, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app, add_zero, OfNat.ofNat, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app, CategoryTheory.dcongr_arg
-- Module: Mathlib.CategoryTheory.Shift.Induced
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_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
n : A
X : C
⊢ Eq.{v_2 + 1} (α := (F ⋙ s (n + 0)).obj X ⟶ (s 0).obj ((shiftFunctor C n ⋙ F).obj X))
    (eqToHom ⋯ ≫
        (i n).hom.app X ≫
          eqToHom ⋯ ≫
            F.map
                (eqToHom ⋯ ≫
                  NatTrans.app (Iso.inv (shiftFunctorZero C A)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)) ≫
              NatTrans.app (Iso.inv (i 0)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X) :
      (F ⋙ s (n + 0)).obj X ⟶ (s 0).obj ((shiftFunctor C n ⋙ F).obj X))
    (CategoryStruct.comp (Y := (s n).obj (F.obj X)) (NatTrans.app (eqToHom ⋯) (F.obj X))
        (map (𝟭 D) ((i n).hom.app X) ≫
          F.map (NatTrans.app (Iso.inv (shiftFunctorZero C A)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)) ≫
            NatTrans.app (Iso.inv (i 0)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)) :
      (F ⋙ s (n + 0)).obj X ⟶ (s 0).obj ((shiftFunctor C n ⋙ F).obj X))

Tactic:
simp [eqToHom_map, eqToHom_app]

Premises used: CategoryTheory.eqToHom_map, CategoryTheory.eqToHom_app
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_3
D : Type u_1
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_2, u_1} D
F : Functor.{v_1, v_2, u_3, u_1} C D
A : Type u_2
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_3, u_2} C A
s : A → Functor.{v_2, v_2, u_1, u_1} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
a : A
⊢ shiftFunctor D a = s a

Tactic:
rfl

Premises used: CategoryTheory.shiftFunctor, rfl
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_3
D : Type u_1
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_2, u_1} D
F : Functor.{v_1, v_2, u_3, u_1} C D
A : Type u_2
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_3, u_2} C A
s : A → Functor.{v_2, v_2, u_1, u_1} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
X : C
⊢ NatTrans.app (Iso.hom (shiftFunctorZero D A)) (F.obj X) =
    NatTrans.app (Iso.hom (i 0)) X ≫ F.map (NatTrans.app (Iso.hom (shiftFunctorZero C A)) X)

Tactic:
simp only [ShiftMkCore.shiftFunctorZero_eq, HasShift.Induced.zero_hom_app_obj]

Premises used: CategoryTheory.HasShift.Induced.zero_hom_app_obj, CategoryTheory.ShiftMkCore.shiftFunctorZero_eq
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_2
D : Type u_1
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} D
F : Functor.{v_1, v_2, u_2, u_1} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_3} C A
s : A → Functor.{v_2, v_2, u_1, u_1} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
X : C
⊢ NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X) =
    F.map (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X) ≫ NatTrans.app (Iso.inv (i 0)) X

Tactic:
simp only [ShiftMkCore.shiftFunctorZero_eq, HasShift.Induced.zero_inv_app_obj]

Premises used: CategoryTheory.HasShift.Induced.zero_inv_app_obj, CategoryTheory.ShiftMkCore.shiftFunctorZero_eq
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_3
D : Type u_1
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_2, u_1} D
F : Functor.{v_1, v_2, u_3, u_1} C D
A : Type u_2
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_3, u_2} C A
s : A → Functor.{v_2, v_2, u_1, u_1} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
a b : A
X : C
⊢ NatTrans.app (Iso.hom (shiftFunctorAdd D a b)) (F.obj X) =
    NatTrans.app (Iso.hom (i (a + b))) X ≫
      F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
        (i b).inv.app (obj.{v_1, v_1, u_3, u_3} (shiftFunctor C a) X) ≫ (s b).map ((i a).inv.app X)

Tactic:
simp only [ShiftMkCore.shiftFunctorAdd_eq, HasShift.Induced.add_hom_app_obj]

Premises used: CategoryTheory.HasShift.Induced.add_hom_app_obj, CategoryTheory.ShiftMkCore.shiftFunctorAdd_eq
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_3
D : Type u_1
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_2, u_1} D
F : Functor.{v_1, v_2, u_3, u_1} C D
A : Type u_2
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_3, u_2} C A
s : A → Functor.{v_2, v_2, u_1, u_1} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
a b : A
X : C
⊢ NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X) =
    (s b).map ((i a).hom.app X) ≫
      (i b).hom.app (obj.{v_1, v_1, u_3, u_3} (shiftFunctor C a) X) ≫
        F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X

Tactic:
simp only [ShiftMkCore.shiftFunctorAdd_eq, HasShift.Induced.add_inv_app_obj]

Premises used: CategoryTheory.HasShift.Induced.add_inv_app_obj, CategoryTheory.ShiftMkCore.shiftFunctorAdd_eq
-- Module: Mathlib.CategoryTheory.Shift.Induced
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_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
this : HasShift.{v_2, u_2, u_3} D A := HasShift.induced F A s i
w :
  ∀ (X : C),
    Eq (α := (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0 ⋙ F).obj X ⟶ (F ⋙ s 0).obj X)
      (NatTrans.app (Iso.hom (Iso.symm (i 0))) X) (NatTrans.app (Iso.hom (isoZero F A)) X)
⊢ Eq (α := shiftFunctor.{v_1, u_1, u_3} C (A := A) 0 ⋙ F ≅ F ⋙ shiftFunctor.{v_2, u_2, u_3} D (A := A) 0)
    (Iso.symm (i 0)) (isoZero F A)

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Shift.Induced
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_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
this : HasShift.{v_2, u_2, u_3} D A := HasShift.induced F A s i
X : C
w :
  Eq (α := F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0) X) ⟶ (s 0).obj (F.obj X))
    (NatTrans.app (Iso.inv (i 0)) X) (NatTrans.app (Iso.hom (isoZero F A)) X)
⊢ Eq (α := (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0 ⋙ F).obj X ⟶ (F ⋙ s 0).obj X)
    (NatTrans.app (Iso.hom (Iso.symm (i 0))) X) (NatTrans.app (Iso.hom (isoZero F A)) X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Shift.Induced
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_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
this : HasShift.{v_2, u_2, u_3} D A := HasShift.induced F A s i
X : C
⊢ Eq (α := F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0) X) ⟶ (s 0).obj (F.obj X))
    (NatTrans.app (Iso.inv (i 0)) X) (NatTrans.app (Iso.hom (isoZero F A)) X)

Tactic:
simp only [isoZero_hom_app, shiftFunctorZero_inv_app_obj_of_induced,
          ← F.map_comp_assoc, Iso.hom_inv_id_app, F.map_id, Category.id_comp]

Premises used: CategoryTheory.shiftFunctorZero_inv_app_obj_of_induced, CategoryTheory.Functor.CommShift.isoZero_hom_app, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Shift.Induced
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_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
this : HasShift.{v_2, u_2, u_3} D A := HasShift.induced F A s i
a b : A
w :
  ∀ (X : C),
    Eq (α := (shiftFunctor C (a + b) ⋙ F).obj X ⟶ (F ⋙ s (a + b)).obj X)
      (NatTrans.app (Iso.hom (Iso.symm (i (a + b)))) X) (NatTrans.app (Iso.hom (isoAdd (i a).symm (i b).symm)) X)
⊢ Eq (α := shiftFunctor C (a + b) ⋙ F ≅ F ⋙ shiftFunctor D (a + b)) (Iso.symm (i (a + b)))
    (isoAdd (i a).symm (i b).symm)

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Shift.Induced
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_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
this : HasShift.{v_2, u_2, u_3} D A := HasShift.induced F A s i
a b : A
X : C
w :
  Eq (α := F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X) ⟶ (s (a + b)).obj (F.obj X))
    (NatTrans.app (Iso.inv (i (a + b))) X) (NatTrans.app (Iso.hom (isoAdd (i a).symm (i b).symm)) X)
⊢ Eq (α := (shiftFunctor C (a + b) ⋙ F).obj X ⟶ (F ⋙ s (a + b)).obj X) (NatTrans.app (Iso.hom (Iso.symm (i (a + b)))) X)
    (NatTrans.app (Iso.hom (isoAdd (i a).symm (i b).symm)) X)

Tactic:
dsimp