awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (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
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_2, u_2, u_5} D A
F G : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
e : F ≅ G
n : A
X : C
rw : (e.hom.hom n ≫ e.inv.hom n).app X = 𝟙 ((F.functor n).obj X)
rw₁ : NatTrans.app (𝟙 (F.functor n)) X = 𝟙 ((F.functor n).obj X)
⊢ (e.hom.hom n).app X ≫ (e.inv.hom n).app X = 𝟙 ((F.functor n).obj X)
have rw₂ : Eq.{v_2 + 1} (α := (F.functor n).obj X ⟶ (F.functor n).obj X) (𝟙 ((F.functor n).obj X)) (𝟙 ((F.functor n).obj X))
Tactic: rw [← NatTrans.comp_app, hom_inv_id_hom, NatTrans.id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (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
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_2, u_2, u_5} D A
F G : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
e : F ≅ G
n : A
X : C
⊢ (e.inv.hom n).app X ≫ (e.hom.hom n).app X = 𝟙 ((G.functor n).obj X)
have rw : (e.inv.hom n ≫ e.hom.hom n).app X = 𝟙 ((G.functor n).obj X)
Tactic: rw [← NatTrans.comp_app, inv_hom_id_hom, NatTrans.id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (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
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_2, u_2, u_5} D A
F G : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
e : F ≅ G
n : A
X : C
rw : (e.inv.hom n ≫ e.hom.hom n).app X = 𝟙 ((G.functor n).obj X)
⊢ (e.inv.hom n).app X ≫ (e.hom.hom n).app X = 𝟙 ((G.functor n).obj X)
have rw₁ : NatTrans.app (𝟙 (G.functor n)) X = 𝟙 ((G.functor n).obj X)
Tactic: rw [← NatTrans.comp_app, inv_hom_id_hom, NatTrans.id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (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
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_2, u_2, u_5} D A
F G : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
e : F ≅ G
n : A
X : C
rw : (e.inv.hom n ≫ e.hom.hom n).app X = 𝟙 ((G.functor n).obj X)
rw₁ : NatTrans.app (𝟙 (G.functor n)) X = 𝟙 ((G.functor n).obj X)
⊢ (e.inv.hom n).app X ≫ (e.hom.hom n).app X = 𝟙 ((G.functor n).obj X)
have rw₂ : Eq.{v_2 + 1} (α := (G.functor n).obj X ⟶ (G.functor n).obj X) (𝟙 ((G.functor n).obj X)) (𝟙 ((G.functor n).obj X))
Tactic: rw [← NatTrans.comp_app, inv_hom_id_hom, NatTrans.id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G_1 H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_8 : G.CommShift A
a : A
⊢ (F.functor a).associator G (shiftFunctor.{v_3, u_3, u_5} E (A := A) 0) ≪≫
      (F.functor a).isoWhiskerLeft (Iso.symm (commShiftIso G 0)) ≪≫
        ((F.functor a).associator (shiftFunctor.{v_2, u_2, u_5} D (A := A) 0) G).symm ≪≫
          isoWhiskerRight (F.shiftIso 0 a a ⋯) G =
    (F.functor a ⋙ G).isoWhiskerLeft (shiftFunctorZero E A)
have w : ∀ (X : C),
  ((F.functor a).associator G (shiftFunctor.{v_3, u_3, u_5} E (A := A) 0) ≪≫
            (F.functor a).isoWhiskerLeft (Iso.symm (commShiftIso G 0)) ≪≫
              ((F.functor a).associator (shiftFunctor.{v_2, u_2, u_5} D (A := A) 0) G).symm ≪≫
                isoWhiskerRight (F.shiftIso 0 a a sorry) G).hom.app
      X =
    NatTrans.app (Iso.hom ((F.functor a ⋙ G).isoWhiskerLeft (shiftFunctorZero E A))) X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G_1 H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_8 : G.CommShift A
a : A
X : C
⊢ ((F.functor a).associator G (shiftFunctor.{v_3, u_3, u_5} E (A := A) 0) ≪≫
            (F.functor a).isoWhiskerLeft (Iso.symm (commShiftIso G 0)) ≪≫
              ((F.functor a).associator (shiftFunctor.{v_2, u_2, u_5} D (A := A) 0) G).symm ≪≫
                isoWhiskerRight (F.shiftIso 0 a a ⋯) G).hom.app
      X =
    NatTrans.app (Iso.hom ((F.functor a ⋙ G).isoWhiskerLeft (shiftFunctorZero E A))) X
have w : 𝟙 (obj.{v_3, v_3, u_3, u_3} (shiftFunctor.{v_3, u_3, u_5} E (A := A) 0) (G.obj ((F.functor a).obj X))) ≫
    NatTrans.app (Iso.inv (commShiftIso G 0)) ((F.functor a).obj X) ≫
      𝟙 (G.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_5} D (A := A) 0) ((F.functor a).obj X))) ≫
        G.map (NatTrans.app (Iso.hom (F.shiftIso 0 a a sorry)) X) =
  NatTrans.app (Iso.hom (shiftFunctorZero E A)) (G.obj ((F.functor a).obj X))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G_1 H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_8 : G.CommShift A
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
⊢ (F.functor a'').associator G (shiftFunctor E (m + n)) ≪≫
      (F.functor a'').isoWhiskerLeft (Iso.symm (commShiftIso G (m + n))) ≪≫
        ((F.functor a'').associator (shiftFunctor D (m + n)) G).symm ≪≫ isoWhiskerRight (F.shiftIso (m + n) a a'' ⋯) G =
    (F.functor a'' ⋙ G).isoWhiskerLeft (shiftFunctorAdd E m n) ≪≫
      ((F.functor a'' ⋙ G).associator (shiftFunctor E m) (shiftFunctor E n)).symm ≪≫
        isoWhiskerRight
            ((F.functor a'').associator G (shiftFunctor E m) ≪≫
              (F.functor a'').isoWhiskerLeft (Iso.symm (commShiftIso G m)) ≪≫
                ((F.functor a'').associator (shiftFunctor D m) G).symm ≪≫ isoWhiskerRight (F.shiftIso m a' a'' ha'') G)
            (shiftFunctor E n) ≪≫
          (F.functor a').associator G (shiftFunctor E n) ≪≫
            (F.functor a').isoWhiskerLeft (Iso.symm (commShiftIso G n)) ≪≫
              ((F.functor a').associator (shiftFunctor D n) G).symm ≪≫ isoWhiskerRight (F.shiftIso n a a' ha') G
have w : ∀ (X : C),
  ((F.functor a'').associator G (shiftFunctor E (m + n)) ≪≫
            (F.functor a'').isoWhiskerLeft (Iso.symm (commShiftIso G (m + n))) ≪≫
              ((F.functor a'').associator (shiftFunctor D (m + n)) G).symm ≪≫
                isoWhiskerRight (F.shiftIso (m + n) a a'' sorry) G).hom.app
      X =
    ((F.functor a'' ⋙ G).isoWhiskerLeft (shiftFunctorAdd E m n) ≪≫
            ((F.functor a'' ⋙ G).associator (shiftFunctor E m) (shiftFunctor E n)).symm ≪≫
              isoWhiskerRight
                  ((F.functor a'').associator G (shiftFunctor E m) ≪≫
                    (F.functor a'').isoWhiskerLeft (Iso.symm (commShiftIso G m)) ≪≫
                      ((F.functor a'').associator (shiftFunctor D m) G).symm ≪≫
                        isoWhiskerRight (F.shiftIso m a' a'' ha'') G)
                  (shiftFunctor E n) ≪≫
                (F.functor a').associator G (shiftFunctor E n) ≪≫
                  (F.functor a').isoWhiskerLeft (Iso.symm (commShiftIso G n)) ≪≫
                    ((F.functor a').associator (shiftFunctor D n) G).symm ≪≫
                      isoWhiskerRight (F.shiftIso n a a' ha') G).hom.app
      X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G_1 H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_8 : G.CommShift A
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ ((F.functor a'').associator G (shiftFunctor E (m + n)) ≪≫
            (F.functor a'').isoWhiskerLeft (Iso.symm (commShiftIso G (m + n))) ≪≫
              ((F.functor a'').associator (shiftFunctor D (m + n)) G).symm ≪≫
                isoWhiskerRight (F.shiftIso (m + n) a a'' ⋯) G).hom.app
      X =
    ((F.functor a'' ⋙ G).isoWhiskerLeft (shiftFunctorAdd E m n) ≪≫
            ((F.functor a'' ⋙ G).associator (shiftFunctor E m) (shiftFunctor E n)).symm ≪≫
              isoWhiskerRight
                  ((F.functor a'').associator G (shiftFunctor E m) ≪≫
                    (F.functor a'').isoWhiskerLeft (Iso.symm (commShiftIso G m)) ≪≫
                      ((F.functor a'').associator (shiftFunctor D m) G).symm ≪≫
                        isoWhiskerRight (F.shiftIso m a' a'' ha'') G)
                  (shiftFunctor E n) ≪≫
                (F.functor a').associator G (shiftFunctor E n) ≪≫
                  (F.functor a').isoWhiskerLeft (Iso.symm (commShiftIso G n)) ≪≫
                    ((F.functor a').associator (shiftFunctor D n) G).symm ≪≫
                      isoWhiskerRight (F.shiftIso n a a' ha') G).hom.app
      X
have w : 𝟙 (obj.{v_3, v_3, u_3, u_3} (shiftFunctor E (m + n)) (G.obj ((F.functor a'').obj X))) ≫
    NatTrans.app (Iso.inv (commShiftIso G (m + n))) ((F.functor a'').obj X) ≫
      𝟙 (G.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (m + n)) ((F.functor a'').obj X))) ≫
        G.map ((F.shiftIso (m + n) a a'' sorry).hom.app X) =
  NatTrans.app (Iso.hom (shiftFunctorAdd E m n)) (G.obj ((F.functor a'').obj X)) ≫
    𝟙
        (obj.{v_3, v_3, u_3, u_3} (shiftFunctor E n)
          (obj.{v_3, v_3, u_3, u_3} (shiftFunctor E m) (G.obj ((F.functor a'').obj X)))) ≫
      Functor.map (shiftFunctor E n)
          (𝟙 (obj.{v_3, v_3, u_3, u_3} (shiftFunctor E m) (G.obj ((F.functor a'').obj X))) ≫
            NatTrans.app (Iso.inv (commShiftIso G m)) ((F.functor a'').obj X) ≫
              𝟙 (G.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D m) ((F.functor a'').obj X))) ≫
                G.map ((F.shiftIso m a' a'' ha'').hom.app X)) ≫
        𝟙 (obj.{v_3, v_3, u_3, u_3} (shiftFunctor E n) (G.obj ((F.functor a').obj X))) ≫
          NatTrans.app (Iso.inv (commShiftIso G n)) ((F.functor a').obj X) ≫
            𝟙 (G.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) ((F.functor a').obj X))) ≫
              G.map ((F.shiftIso n a a' ha').hom.app X)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G_1 H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_8 : G.CommShift A
F₁ F₂ : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
φ : F₁ ⟶ F₂
n a a' : A
ha' : n + a = a'
⊢ Eq (α := functor (F₁.postcomp G) a' ⋙ shiftFunctor E n ⟶ functor (F₂.postcomp G) a)
    (Iso.hom (shiftIso (F₁.postcomp G) n a a' ha') ≫ whiskerRight (φ.hom a) G)
    (whiskerRight (whiskerRight (φ.hom a') G) (shiftFunctor E n) ≫ Iso.hom (shiftIso (F₂.postcomp G) n a a' ha'))
have w : ∀ (X : C),
  Eq (α := (functor (F₁.postcomp G) a' ⋙ shiftFunctor E n).obj X ⟶ (functor (F₂.postcomp G) a).obj X)
    (NatTrans.app (Iso.hom (shiftIso (F₁.postcomp G) n a a' ha') ≫ whiskerRight (φ.hom a) G) X)
    (NatTrans.app
      (whiskerRight (whiskerRight (φ.hom a') G) (shiftFunctor E n) ≫ Iso.hom (shiftIso (F₂.postcomp G) n a a' ha')) X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G_1 H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
G : Functor.{v_2, v_3, u_2, u_3} D E
G' : Functor.{v_3, v_4, u_3, u_4} E E'
inst_8 : G.CommShift A
inst_9 : G'.CommShift A
n a a' : A
ha' : n + a = a'
⊢ Eq (α := functor (postcomp (F.postcomp G) G') a' ⋙ shiftFunctor E' n ⟶ functor (F.postcomp (G ⋙ G')) a)
    (Iso.hom (shiftIso (postcomp (F.postcomp G) G') n a a' ha') ≫
      Iso.hom ((fun (x : A) ↦ (F.functor x).associator G G') a))
    (whiskerRight (Iso.hom ((fun (x : A) ↦ (F.functor x).associator G G') a')) (shiftFunctor E' n) ≫
      Iso.hom (shiftIso (F.postcomp (G ⋙ G')) n a a' ha'))
have w : ∀ (X : C),
  Eq (α :=
    (functor (postcomp (F.postcomp G) G') a' ⋙ shiftFunctor E' n).obj X ⟶ (functor (F.postcomp (G ⋙ G')) a).obj X)
    (NatTrans.app
      (Iso.hom (shiftIso (postcomp (F.postcomp G) G') n a a' ha') ≫
        Iso.hom ((fun (x : A) ↦ (F.functor x).associator G G') a))
      X)
    (NatTrans.app
      (whiskerRight (Iso.hom ((fun (x : A) ↦ (F.functor x).associator G G') a')) (shiftFunctor E' n) ≫
        Iso.hom (shiftIso (F.postcomp (G ⋙ G')) n a a' ha'))
      X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G_1 H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
G G' : Functor.{v_2, v_3, u_2, u_3} D E
e : G ≅ G'
inst_8 : G.CommShift A
inst_9 : G'.CommShift A
inst_10 : NatTrans.CommShift e.hom A
n a a' : A
ha' : n + a = a'
⊢ Eq (α := functor (F.postcomp G) a' ⋙ shiftFunctor E n ⟶ functor (F.postcomp G') a)
    (Iso.hom (shiftIso (F.postcomp G) n a a' ha') ≫ Iso.hom ((fun (a : A) ↦ (F.functor a).isoWhiskerLeft e) a))
    (whiskerRight (Iso.hom ((fun (a : A) ↦ (F.functor a).isoWhiskerLeft e) a')) (shiftFunctor E n) ≫
      Iso.hom (shiftIso (F.postcomp G') n a a' ha'))
have w : ∀ (X : C),
  Eq (α := (functor (F.postcomp G) a' ⋙ shiftFunctor E n).obj X ⟶ (functor (F.postcomp G') a).obj X)
    (NatTrans.app
      (Iso.hom (shiftIso (F.postcomp G) n a a' ha') ≫ Iso.hom ((fun (a : A) ↦ (F.functor a).isoWhiskerLeft e) a)) X)
    (NatTrans.app
      (whiskerRight (Iso.hom ((fun (a : A) ↦ (F.functor a).isoWhiskerLeft e) a')) (shiftFunctor E n) ≫
        Iso.hom (shiftIso (F.postcomp G') n a a' ha'))
      X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctorsLift (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{u_5, u_1} C
inst_1 : Category.{u_6, u_2} D
inst_2 : Category.{u_7, u_3} E
A : Type u_4
inst_3 : AddMonoid A
inst_4 : HasShift.{u_6, u_2, u_4} D A
inst_5 : HasShift.{u_7, u_3, u_4} E A
F : SingleFunctors.{u_5, u_1, u_7, u_3, u_4} C E A
G : Functor.{u_6, u_7, u_2, u_3} D E
inst_6 : G.CommShift A
inst_7 : G.Full
inst_8 : G.Faithful
Φ : A → Functor.{u_5, u_6, u_1, u_2} C D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
a : A
⊢ Eq (α := Φ a ⋙ shiftFunctor.{u_6, u_2, u_4} D (A := A) 0 ≅ Φ a) (lift.shiftIso hΦ 0 a a ⋯)
    ((Φ a).isoWhiskerLeft (shiftFunctorZero D A))
have w : ∀ (X : C),
  Eq (α := (Φ a ⋙ shiftFunctor.{u_6, u_2, u_4} D (A := A) 0).obj X ⟶ (Φ a).obj X)
    (NatTrans.app (Iso.hom (lift.shiftIso hΦ 0 a a sorry)) X)
    (NatTrans.app (Iso.hom ((Φ a).isoWhiskerLeft (shiftFunctorZero D A))) X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctorsLift (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{u_5, u_1} C
inst_1 : Category.{u_6, u_2} D
inst_2 : Category.{u_7, u_3} E
A : Type u_4
inst_3 : AddMonoid A
inst_4 : HasShift.{u_6, u_2, u_4} D A
inst_5 : HasShift.{u_7, u_3, u_4} E A
F : SingleFunctors.{u_5, u_1, u_7, u_3, u_4} C E A
G : Functor.{u_6, u_7, u_2, u_3} D E
inst_6 : G.CommShift A
inst_7 : G.Full
inst_8 : G.Faithful
Φ : A → Functor.{u_5, u_6, u_1, u_2} C D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
a : A
X : C
⊢ Eq (α := (Φ a ⋙ shiftFunctor.{u_6, u_2, u_4} D (A := A) 0).obj X ⟶ (Φ a).obj X)
    (NatTrans.app (Iso.hom (lift.shiftIso hΦ 0 a a ⋯)) X)
    (NatTrans.app (Iso.hom ((Φ a).isoWhiskerLeft (shiftFunctorZero D A))) X)
have w : Eq (α := G.obj ((Φ a ⋙ shiftFunctor.{u_6, u_2, u_4} D (A := A) 0).obj X) ⟶ G.obj ((Φ a).obj X))
  (G.map (NatTrans.app (Iso.hom (lift.shiftIso hΦ 0 a a sorry)) X))
  (G.map (NatTrans.app (Iso.hom ((Φ a).isoWhiskerLeft (shiftFunctorZero D A))) X))
Tactic: apply G.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctorsLift (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{u_5, u_1} C
inst_1 : Category.{u_6, u_2} D
inst_2 : Category.{u_7, u_3} E
A : Type u_4
inst_3 : AddMonoid A
inst_4 : HasShift.{u_6, u_2, u_4} D A
inst_5 : HasShift.{u_7, u_3, u_4} E A
F : SingleFunctors.{u_5, u_1, u_7, u_3, u_4} C E A
G : Functor.{u_6, u_7, u_2, u_3} D E
inst_6 : G.CommShift A
inst_7 : G.Full
inst_8 : G.Faithful
Φ : A → Functor.{u_5, u_6, u_1, u_2} C D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
⊢ lift.shiftIso hΦ (m + n) a a'' ⋯ =
    (Φ a'').isoWhiskerLeft (shiftFunctorAdd D m n) ≪≫
      ((Φ a'').associator (shiftFunctor D m) (shiftFunctor D n)).symm ≪≫
        isoWhiskerRight (lift.shiftIso hΦ m a' a'' ha'') (shiftFunctor D n) ≪≫ lift.shiftIso hΦ n a a' ha'
have w : ∀ (X : C),
  NatTrans.app (Iso.hom (lift.shiftIso hΦ (m + n) a a'' sorry)) X =
    ((Φ a'').isoWhiskerLeft (shiftFunctorAdd D m n) ≪≫
            ((Φ a'').associator (shiftFunctor D m) (shiftFunctor D n)).symm ≪≫
              isoWhiskerRight (lift.shiftIso hΦ m a' a'' ha'') (shiftFunctor D n) ≪≫
                lift.shiftIso hΦ n a a' ha').hom.app
      X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctorsLift (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{u_5, u_1} C
inst_1 : Category.{u_6, u_2} D
inst_2 : Category.{u_7, u_3} E
A : Type u_4
inst_3 : AddMonoid A
inst_4 : HasShift.{u_6, u_2, u_4} D A
inst_5 : HasShift.{u_7, u_3, u_4} E A
F : SingleFunctors.{u_5, u_1, u_7, u_3, u_4} C E A
G : Functor.{u_6, u_7, u_2, u_3} D E
inst_6 : G.CommShift A
inst_7 : G.Full
inst_8 : G.Faithful
Φ : A → Functor.{u_5, u_6, u_1, u_2} C D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ NatTrans.app (Iso.hom (lift.shiftIso hΦ (m + n) a a'' ⋯)) X =
    ((Φ a'').isoWhiskerLeft (shiftFunctorAdd D m n) ≪≫
            ((Φ a'').associator (shiftFunctor D m) (shiftFunctor D n)).symm ≪≫
              isoWhiskerRight (lift.shiftIso hΦ m a' a'' ha'') (shiftFunctor D n) ≪≫
                lift.shiftIso hΦ n a a' ha').hom.app
      X
have w : G.map (NatTrans.app (Iso.hom (lift.shiftIso hΦ (m + n) a a'' sorry)) X) =
  G.map
    (((Φ a'').isoWhiskerLeft (shiftFunctorAdd D m n) ≪≫
            ((Φ a'').associator (shiftFunctor D m) (shiftFunctor D n)).symm ≪≫
              isoWhiskerRight (lift.shiftIso hΦ m a' a'' ha'') (shiftFunctor D n) ≪≫
                lift.shiftIso hΦ n a a' ha').hom.app
      X)
Tactic: apply G.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctorsLift (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{u_5, u_1} C
inst_1 : Category.{u_6, u_2} D
inst_2 : Category.{u_7, u_3} E
A : Type u_4
inst_3 : AddMonoid A
inst_4 : HasShift.{u_6, u_2, u_4} D A
inst_5 : HasShift.{u_7, u_3, u_4} E A
F : SingleFunctors.{u_5, u_1, u_7, u_3, u_4} C E A
G : Functor.{u_6, u_7, u_2, u_3} D E
inst_6 : G.CommShift A
inst_7 : G.Full
inst_8 : G.Faithful
Φ : A → Functor.{u_5, u_6, u_1, u_2} C D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ G.map (NatTrans.app (Iso.hom (lift.shiftIso hΦ (m + n) a a'' ⋯)) X) =
    G.map
      (((Φ a'').isoWhiskerLeft (shiftFunctorAdd D m n) ≪≫
              ((Φ a'').associator (shiftFunctor D m) (shiftFunctor D n)).symm ≪≫
                isoWhiskerRight (lift.shiftIso hΦ m a' a'' ha'') (shiftFunctor D n) ≪≫
                  lift.shiftIso hΦ n a a' ha').hom.app
        X)
have w : G.map (NatTrans.app (Iso.hom (lift.shiftIso hΦ (m + n) a a'' sorry)) X) =
  G.map
    (NatTrans.app (Iso.hom (shiftFunctorAdd D m n)) ((Φ a'').obj X) ≫
      𝟙 (obj.{u_6, u_6, u_2, u_2} (shiftFunctor D n) (obj.{u_6, u_6, u_2, u_2} (shiftFunctor D m) ((Φ a'').obj X))) ≫
        map (shiftFunctor D n) (NatTrans.app (Iso.hom (lift.shiftIso hΦ m a' a'' ha'')) X) ≫
          NatTrans.app (Iso.hom (lift.shiftIso hΦ n a a' ha')) X)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctorsLift (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{u_5, u_1} C
inst_1 : Category.{u_6, u_2} D
inst_2 : Category.{u_7, u_3} E
A : Type u_4
inst_3 : AddMonoid A
inst_4 : HasShift.{u_6, u_2, u_4} D A
inst_5 : HasShift.{u_7, u_3, u_4} E A
F : SingleFunctors.{u_5, u_1, u_7, u_3, u_4} C E A
G : Functor.{u_6, u_7, u_2, u_3} D E
inst_6 : G.CommShift A
inst_7 : G.Full
inst_8 : G.Faithful
Φ : A → Functor.{u_5, u_6, u_1, u_2} C D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ G.map (NatTrans.app (Iso.hom (lift.shiftIso hΦ (m + n) a a'' ⋯)) X) =
    G.map
      (NatTrans.app (Iso.hom (shiftFunctorAdd D m n)) ((Φ a'').obj X) ≫
        𝟙 (obj.{u_6, u_6, u_2, u_2} (shiftFunctor D n) (obj.{u_6, u_6, u_2, u_2} (shiftFunctor D m) ((Φ a'').obj X))) ≫
          map (shiftFunctor D n) (NatTrans.app (Iso.hom (lift.shiftIso hΦ m a' a'' ha'')) X) ≫
            NatTrans.app (Iso.hom (lift.shiftIso hΦ n a a' ha')) X)
have w : NatTrans.app (Iso.hom (commShiftIso G (m + n))) ((Φ a'').obj X) ≫
    map (shiftFunctor E (m + n)) ((hΦ a'').hom.app X) ≫ (F.shiftIso (m + n) a a'' sorry).hom.app X ≫ (hΦ a).inv.app X =
  G.map (NatTrans.app (Iso.hom (shiftFunctorAdd D m n)) ((Φ a'').obj X)) ≫
    G.map
        (𝟙
          (obj.{u_6, u_6, u_2, u_2} (shiftFunctor D n) (obj.{u_6, u_6, u_2, u_2} (shiftFunctor D m) ((Φ a'').obj X)))) ≫
      NatTrans.app (Iso.hom (commShiftIso G n)) (obj.{u_6, u_6, u_2, u_2} (shiftFunctor D m) ((Φ a'').obj X)) ≫
        (map (shiftFunctor E n) (NatTrans.app (Iso.hom (commShiftIso G m)) ((Φ a'').obj X)) ≫
            map (shiftFunctor E n) (map (shiftFunctor E m) ((hΦ a'').hom.app X)) ≫
              map (shiftFunctor E n) ((F.shiftIso m a' a'' ha'').hom.app X) ≫
                map (shiftFunctor E n) ((hΦ a').inv.app X)) ≫
          map (shiftFunctor E n) ((hΦ a').hom.app X) ≫ (F.shiftIso n a a' ha').hom.app X ≫ (hΦ a).inv.app X
Tactic: simp only [lift.map_shiftIso_hom_app, map_comp, commShiftIso_hom_naturality_assoc]