awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (goal)
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)))
| (s m₃).map ((s m₂).map ((i m₁).inv.app X)) ≫ (s m₃).map ((s m₂).map ((i m₁).hom.app X))
have a : 𝟙 ((s m₃).obj ((F ⋙ s m₂).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X)))
Tactic: erw [← Functor.map_comp, ← Functor.map_comp, Iso.inv_hom_id_app,
            (s m₂).map_id, (s m₃).map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (goal)
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 (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 (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))
have a : 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 (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₃).obj ((F ⋙ s m₂).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X))) =
  NatTrans.app (eqToHom sorry) (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))
Tactic: slice_lhs 6 7 =>
          erw [← Functor.map_comp, ← Functor.map_comp, Iso.inv_hom_id_app,
            (s m₂).map_id, (s m₃).map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (goal)
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 (0 + n) = 𝟭 D ⋙ s n
have rw : s n = 𝟭 D ⋙ s n
Tactic: rw [zero_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (goal)
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 : 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)
have suffices : Eq (α := s (0 + n) ⟶ s 0 ⋙ s n) (Iso.hom (Induced.add F s i 0 n))
  (eqToHom sorry ≫ whiskerRight (Induced.zero F s i).inv (s n))
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
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (goal)
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
⊢ 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))
have 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 sorry ≫ whiskerRight (Induced.zero F s i).inv (s n)))
Tactic: apply ((whiskeringLeft C D D).obj F).map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (goal)
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
⊢ 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)))
have 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 sorry ≫ whiskerRight (Induced.zero F s i).inv (s n))) X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (hypothesis)
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 (α :=
    (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)
have eq : Eq (α := (F ⋙ s (0 + n)).obj X ⟶ (shiftFunctor C (0 + n) ⋙ F).obj X) (NatTrans.app (Iso.hom (i (0 + n))) X)
  (eqToHom sorry ≫ (i n).hom.app X ≫ eqToHom sorry)
Tactic: have eq := dcongr_arg (fun a => (i a).hom.app X) (zero_add n)
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (goal)
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 (α :=
    (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)
have a : NatTrans.app (Iso.hom (Induced.add F s i 0 n)) (F.obj X) =
  NatTrans.app (eqToHom sorry) (F.obj X) ≫ (s n).map ((Induced.zero F s i).inv.app (F.obj X))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (goal)
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 ⋯)
⊢ 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))
have a : Eq.{v_2 + 1} (α := (s (0 + n)).obj (F.obj X) ⟶ (s n).obj ((s 0).obj (F.obj X)))
  (eqToHom sorry ≫
      (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 sorry ≫
      (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: 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (goal)
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 ⋯ ≫
        (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)))
have a : Eq.{v_2 + 1} (α := (s (0 + n)).obj (F.obj X) ⟶ (s n).obj ((s 0).obj (F.obj X)))
  (eqToHom sorry ≫
      (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 sorry ≫
      (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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (goal)
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 + 0) = s n ⋙ 𝟭 D
have rw : s n = s n ⋙ 𝟭 D
Tactic: rw [add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (goal)
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 : 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)
have suffices : Eq (α := s (n + 0) ⟶ s n ⋙ s 0) (Iso.hom (Induced.add F s i n 0))
  (eqToHom sorry ≫ (s n).whiskerLeft (Induced.zero F s i).inv)
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
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (goal)
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
⊢ 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)
have 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 sorry ≫ (s n).whiskerLeft (Induced.zero F s i).inv))
Tactic: apply ((whiskeringLeft C D D).obj F).map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (goal)
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
⊢ 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))
have 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 sorry ≫ (s n).whiskerLeft (Induced.zero F s i).inv)) X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (goal)
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 (α :=
    (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)
have 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 sorry) (F.obj X))
    ((Induced.zero F s i).inv.app ((s n).obj (F.obj X))))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (goal)
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 (α := (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))))
have a : Eq.{v_2 + 1} (α := (F ⋙ s (n + 0)).obj X ⟶ (s 0).obj ((shiftFunctor C n ⋙ F).obj X))
  (eqToHom sorry ≫
      (i n).hom.app X ≫
        eqToHom sorry ≫
          F.map
              (eqToHom sorry ≫
                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 sorry) (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: 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (goal)
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
⊢ 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)
have 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)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (goal)
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 (α := (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)
have 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)
Tactic: dsimp