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)
m₁ m₂ m₃ : A
X : C
eq :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m₁ + m₂ + m₃)) X) ⟶
      F.obj
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₃)
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁ ⋙ shiftFunctor C m₂) X)))
    (F.map
      (NatTrans.app (Iso.hom (shiftFunctorAdd C (m₁ + m₂) m₃)) X ≫
        map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ m₂)) X)))
    (F.map
      (NatTrans.app (Iso.hom (shiftFunctorAdd' C m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯)) X ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X)))
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m₁ + m₂ + m₃)) X) ⟶
      F.obj
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₃)
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₂) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X))))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C (m₁ + m₂) m₃)) X) ≫
      F.map (map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ m₂)) X)))
    (F.map (eqToHom ⋯) ≫
      F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ (m₂ + m₃))) X) ≫
        F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X)))

Tactic:
simp only [Functor.comp_obj, Functor.map_comp, shiftFunctorAdd',
          Iso.trans_hom, eqToIso.hom, NatTrans.comp_app, eqToHom_app,
          Category.assoc] at eq

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.eqToIso.hom, CategoryTheory.eqToHom_app, CategoryTheory.shiftFunctorAdd', CategoryTheory.Iso.trans_hom, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.comp_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)
m₁ m₂ m₃ : A
X : C
eq :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m₁ + m₂ + m₃)) X) ⟶
      F.obj
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₃)
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₂) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X))))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C (m₁ + m₂) m₃)) X) ≫
      F.map (map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ m₂)) X)))
    (F.map (eqToHom ⋯) ≫
      F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ (m₂ + m₃))) X) ≫
        F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X)))
a :
  (NatTrans.app (Iso.hom (Induced.add F s i (m₁ + m₂) m₃)) (F.obj X) ≫
        (s m₃).map ((Induced.add F s i m₁ m₂).hom.app (F.obj X))) ≫
      (s m₃).map ((s m₂).map ((i m₁).hom.app X)) =
    (NatTrans.app (eqToHom ⋯) (F.obj X) ≫
        NatTrans.app (Iso.hom (Induced.add F s i m₁ (m₂ + m₃))) (F.obj X) ≫
          (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X))) ≫
      (s m₃).map ((s m₂).map ((i m₁).hom.app X))
⊢ NatTrans.app (Iso.hom (Induced.add F s i (m₁ + m₂) m₃)) (F.obj X) ≫
      (s m₃).map ((Induced.add F s i m₁ m₂).hom.app (F.obj X)) =
    NatTrans.app (eqToHom ⋯) (F.obj X) ≫
      NatTrans.app (Iso.hom (Induced.add F s i m₁ (m₂ + m₃))) (F.obj X) ≫
        (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X))

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

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.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)
m₁ m₂ m₃ : A
X : C
eq :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m₁ + m₂ + m₃)) X) ⟶
      F.obj
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₃)
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₂) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X))))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C (m₁ + m₂) m₃)) X) ≫
      F.map (map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ m₂)) X)))
    (F.map (eqToHom ⋯) ≫
      F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ (m₂ + m₃))) X) ≫
        F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X)))
a :
  Eq (α := (s (m₁ + m₂ + m₃)).obj (F.obj X) ⟶ (s m₃).obj ((s m₂).obj ((shiftFunctor C m₁ ⋙ F).obj X)))
    (NatTrans.app (Iso.hom (i (m₁ + m₂ + m₃))) X ≫
      F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C (m₁ + m₂) m₃)) X) ≫
        (i m₃).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m₁ + m₂)) X) ≫
          (s m₃).map (NatTrans.app (Iso.inv (i (m₁ + m₂))) X) ≫
            (s m₃).map (NatTrans.app (Iso.hom (i (m₁ + m₂))) X) ≫
              (s m₃).map (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ m₂)) X)) ≫
                (s m₃).map ((i m₂).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X)) ≫
                  (s m₃).map ((s m₂).map ((i m₁).inv.app X)) ≫ (s m₃).map ((s m₂).map ((i m₁).hom.app X)))
    (NatTrans.app (eqToHom ⋯) (F.obj X) ≫
      NatTrans.app (Iso.hom (i (m₁ + (m₂ + m₃)))) X ≫
        F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ (m₂ + m₃))) X) ≫
          NatTrans.app (Iso.inv (i (m₂ + m₃))) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X) ≫
            (s (m₂ + m₃)).map ((i m₁).inv.app X) ≫
              (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X)) ≫ (s m₃).map ((s m₂).map ((i m₁).hom.app X)))
⊢ (NatTrans.app (Iso.hom (Induced.add F s i (m₁ + m₂) m₃)) (F.obj X) ≫
        (s m₃).map ((Induced.add F s i m₁ m₂).hom.app (F.obj X))) ≫
      (s m₃).map ((s m₂).map ((i m₁).hom.app X)) =
    (NatTrans.app (eqToHom ⋯) (F.obj X) ≫
        NatTrans.app (Iso.hom (Induced.add F s i m₁ (m₂ + m₃))) (F.obj X) ≫
          (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X))) ≫
      (s m₃).map ((s m₂).map ((i m₁).hom.app X))

Tactic:
simp only [Induced.add_hom_app_obj, Category.assoc, Functor.map_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.HasShift.Induced.add_hom_app_obj, CategoryTheory.Functor.map_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)
m₁ m₂ m₃ : A
X : C
eq :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m₁ + m₂ + m₃)) X) ⟶
      F.obj
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₃)
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₂) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X))))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C (m₁ + m₂) m₃)) X) ≫
      F.map (map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ m₂)) X)))
    (F.map (eqToHom ⋯) ≫
      F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ (m₂ + m₃))) X) ≫
        F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X)))
a : 𝟙 ((s m₃).obj (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m₁ + m₂)) X)))
| (s m₃).map (NatTrans.app (Iso.inv (i (m₁ + m₂))) X) ≫ (s m₃).map (NatTrans.app (Iso.hom (i (m₁ + m₂))) X)

Tactic:
erw [← Functor.map_comp, Iso.inv_hom_id_app, Functor.map_id]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_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)
m₁ m₂ m₃ : A
X : C
eq :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m₁ + m₂ + m₃)) X) ⟶
      F.obj
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₃)
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₂) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X))))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C (m₁ + m₂) m₃)) X) ≫
      F.map (map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ m₂)) X)))
    (F.map (eqToHom ⋯) ≫
      F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ (m₂ + m₃))) X) ≫
        F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X)))
a : 𝟙 ((s m₃).obj ((F ⋙ s m₂).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X)))
| (s m₃).map ((s m₂).map ((i m₁).inv.app X)) ≫ (s m₃).map ((s m₂).map ((i m₁).hom.app X))

Tactic:
erw [← Functor.map_comp, ← Functor.map_comp, Iso.inv_hom_id_app,
            (s m₂).map_id, (s m₃).map_id]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_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)
m₁ m₂ m₃ : A
X : C
eq :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m₁ + m₂ + m₃)) X) ⟶
      F.obj
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₃)
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₂) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X))))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C (m₁ + m₂) m₃)) X) ≫
      F.map (map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ m₂)) X)))
    (F.map (eqToHom ⋯) ≫
      F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ (m₂ + m₃))) X) ≫
        F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X)))
⊢ NatTrans.app (Iso.hom (i (m₁ + m₂ + m₃))) X ≫
      F.map (eqToHom ⋯) ≫
        F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ (m₂ + m₃))) X) ≫
          F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X)) ≫
            (i m₃).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁ ⋙ shiftFunctor C m₂) X) ≫
              (s m₃).map ((i m₂).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X)) =
    CategoryStruct.comp (Y := (s (m₁ + (m₂ + m₃))).obj (F.obj X)) (NatTrans.app (eqToHom ⋯) (F.obj X))
      (CategoryStruct.comp (Y := (F ⋙ s (m₁ + m₂ + m₃)).obj X) (eqToHom ⋯)
          (NatTrans.app (Iso.hom (i (m₁ + m₂ + m₃))) X ≫ eqToHom ⋯) ≫
        F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ (m₂ + m₃))) X) ≫
          NatTrans.app (Iso.inv (i (m₂ + m₃))) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X) ≫
            (s (m₂ + m₃)).map ((i m₁).inv.app X) ≫
              (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X)) ≫ (s m₃).map ((s m₂).map ((i m₁).hom.app X)))

Tactic:
simp only [Functor.comp_obj, eqToHom_map, eqToHom_app, NatTrans.naturality_assoc,
          Induced.add_hom_app_obj, Functor.comp_map, Category.assoc, Iso.inv_hom_id_app_assoc,
          eqToHom_trans_assoc, eqToHom_refl, Category.id_comp, Category.comp_id,
          ← Functor.map_comp, Iso.inv_hom_id_app, Functor.map_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.HasShift.Induced.add_hom_app_obj, CategoryTheory.eqToHom_map, CategoryTheory.eqToHom_app, CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.eqToHom_trans_assoc, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Iso.inv_hom_id_app_assoc, CategoryTheory.Functor.comp_map, CategoryTheory.NatTrans.naturality_assoc, 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)
n : A
rw : s n = 𝟭 D ⋙ s n
⊢ s (0 + n) = 𝟭 D ⋙ s n

Tactic:
rw [zero_add]

Premises used: zero_add
-- 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 = 𝟭 D ⋙ s n

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 (0 + n) ⟶ s 0 ⋙ s n) (Iso.hom (Induced.add F s i 0 n))
    (eqToHom ⋯ ≫ whiskerRight (Induced.zero F s i).inv (s n))
X : D
⊢ NatTrans.app (Iso.hom (Induced.add F s i 0 n)) X = eqToHom ⋯ ≫ (s n).map ((Induced.zero F s i).inv.app 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 (0 + n) ⟶ s 0 ⋙ s n) (Iso.hom (Induced.add F s i 0 n))
    (eqToHom ⋯ ≫ whiskerRight (Induced.zero F s i).inv (s n))
⊢ ∀ (X : D), NatTrans.app (Iso.hom (Induced.add F s i 0 n)) X = eqToHom ⋯ ≫ (s n).map ((Induced.zero F s i).inv.app X)

Tactic:
suffices (Induced.add F s i 0 n).hom =
          eqToHom (by rw [zero_add]; rfl) ≫ whiskerRight (Induced.zero F s i).inv (s n) 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 (0 + n)) ⟶ obj (obj (whiskeringLeft C D D) F) (s 0 ⋙ s n))
    (map (obj (whiskeringLeft C D D) F) (Iso.hom (Induced.add F s i 0 n)))
    (map (obj (whiskeringLeft C D D) F) (eqToHom ⋯ ≫ whiskerRight (Induced.zero F s i).inv (s n)))
⊢ Eq (α := s (0 + n) ⟶ s 0 ⋙ s n) (Iso.hom (Induced.add F s i 0 n))
    (eqToHom ⋯ ≫ whiskerRight (Induced.zero F s i).inv (s n))

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 (0 + n))).obj X ⟶ (obj (obj (whiskeringLeft C D D) F) (s 0 ⋙ s n)).obj X)
      (NatTrans.app (map (obj (whiskeringLeft C D D) F) (Iso.hom (Induced.add F s i 0 n))) X)
      (NatTrans.app (map (obj (whiskeringLeft C D D) F) (eqToHom ⋯ ≫ whiskerRight (Induced.zero F s i).inv (s n))) X)
⊢ Eq (α := obj (obj (whiskeringLeft C D D) F) (s (0 + n)) ⟶ obj (obj (whiskeringLeft C D D) F) (s 0 ⋙ s n))
    (map (obj (whiskeringLeft C D D) F) (Iso.hom (Induced.add F s i 0 n)))
    (map (obj (whiskeringLeft C D D) F) (eqToHom ⋯ ≫ whiskerRight (Induced.zero F s i).inv (s n)))

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
⊢ 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 ⋯)

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

Tactic:
simp only [Induced.add_hom_app_obj, eq, shiftFunctorAdd_zero_add_hom_app,
          Functor.map_comp, eqToHom_map, Category.assoc, eqToHom_trans_assoc,
          eqToHom_refl, Category.id_comp, eqToHom_app, Induced.zero_inv_app_obj]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.HasShift.Induced.zero_inv_app_obj, CategoryTheory.HasShift.Induced.add_hom_app_obj, CategoryTheory.eqToHom_map, CategoryTheory.eqToHom_app, CategoryTheory.shiftFunctorAdd_zero_add_hom_app, CategoryTheory.eqToHom_refl, CategoryTheory.Functor.map_comp, CategoryTheory.eqToHom_trans_assoc, CategoryTheory.Category.id_comp