awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctors
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'
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)
⊢ 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'))

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctors
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'
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:
simp [NatTrans.shift_app e.hom n]

Premises used: CategoryTheory.NatTrans.shift_app, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctorsLift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{u_7, u_1} C
inst_1 : Category.{u_6, u_2} D
inst_2 : Category.{u_5, 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_5, u_3, u_4} E A
F : SingleFunctors.{u_7, u_1, u_5, u_3, u_4} C E A
G : Functor.{u_6, u_5, u_2, u_3} D E
inst_6 : G.CommShift A
inst_7 : G.Full
inst_8 : G.Faithful
Φ : A → Functor.{u_7, u_6, u_1, u_2} C D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
n a a' : A
h : n + a = a'
X : C
⊢ Eq (α := G.obj (obj.{u_6, u_6, u_2, u_2} (shiftFunctor D n) ((Φ a').obj X)) ⟶ G.obj ((Φ a).obj X))
    (G.map (NatTrans.app (Iso.hom (shiftIso hΦ n a a' h)) X))
    (NatTrans.app (Iso.hom (commShiftIso G n)) ((Φ a').obj X) ≫
      map (shiftFunctor E n) ((hΦ a').hom.app X) ≫ (F.shiftIso n a a' h).hom.app X ≫ (hΦ a).inv.app X)

Tactic:
simp [shiftIso]

Premises used: CategoryTheory.SingleFunctors.lift.shiftIso
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctorsLift
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
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 ⋯)) X)
      (NatTrans.app (Iso.hom ((Φ a).isoWhiskerLeft (shiftFunctorZero D A))) X)
⊢ 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))

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctorsLift
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
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 ⋯)) X))
    (G.map (NatTrans.app (Iso.hom ((Φ a).isoWhiskerLeft (shiftFunctorZero D A))) X))
⊢ 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)

Tactic:
apply G.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctorsLift
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 (α := 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 ⋯)) X))
    (G.map (NatTrans.app (Iso.hom ((Φ a).isoWhiskerLeft (shiftFunctorZero D A))) X))

Tactic:
simp [lift.map_shiftIso_hom_app, Functor.commShiftIso_zero]

Premises used: _private.0.CategoryTheory.SingleFunctors.lift.map_shiftIso_hom_app, CategoryTheory.Functor.CommShift.commShiftIso_zero
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctorsLift
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''
w :
  ∀ (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
⊢ 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'

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctorsLift
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
w :
  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)
⊢ 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

Tactic:
apply G.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctorsLift
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
w :
  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)
⊢ 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)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctorsLift
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
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'' ⋯).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
⊢ 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)

Tactic:
simp only [lift.map_shiftIso_hom_app, map_comp, commShiftIso_hom_naturality_assoc]

Premises used: _private.0.CategoryTheory.SingleFunctors.lift.map_shiftIso_hom_app, CategoryTheory.Functor.commShiftIso_hom_naturality_assoc, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctorsLift
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
w :
  NatTrans.app (Iso.hom (commShiftIso G (m + n))) ((Φ a'').obj X) ≫
      map (shiftFunctor E (m + n)) ((hΦ a'').hom.app X) ≫
        ((F.functor a'').isoWhiskerLeft (shiftFunctorAdd E m n) ≪≫
                  ((F.functor a'').associator (shiftFunctor E m) (shiftFunctor E n)).symm ≪≫
                    isoWhiskerRight (F.shiftIso m a' a'' ha'') (shiftFunctor E n) ≪≫ F.shiftIso n a a' ha').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
⊢ 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'' ⋯).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:
rw [F.shiftIso_add n m a a' a'' ha' ha'']

Premises used: CategoryTheory.SingleFunctors.shiftIso_add
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctorsLift
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 (commShiftIso G (m + n))) ((Φ a'').obj X) ≫
      map (shiftFunctor E (m + n)) ((hΦ a'').hom.app X) ≫
        ((F.functor a'').isoWhiskerLeft (shiftFunctorAdd E m n) ≪≫
                  ((F.functor a'').associator (shiftFunctor E m) (shiftFunctor E n)).symm ≪≫
                    isoWhiskerRight (F.shiftIso m a' a'' ha'') (shiftFunctor E n) ≪≫ F.shiftIso n a a' ha').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 [commShiftIso_add, ← Functor.map_comp_assoc, -Functor.map_comp]

Premises used: CategoryTheory.Functor.CommShift.commShiftIso_add, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctorsLift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{u_7, u_1} C
inst_1 : Category.{u_6, u_2} D
inst_2 : Category.{u_5, 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_5, u_3, u_4} E A
F : SingleFunctors.{u_7, u_1, u_5, u_3, u_4} C E A
G : Functor.{u_6, u_5, u_2, u_3} D E
inst_6 : G.CommShift A
inst_7 : G.Full
inst_8 : G.Faithful
Φ : A → Functor.{u_7, u_6, u_1, u_2} C D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
n a a' : A
h : n + a = a'
X : C
⊢ Eq (α := G.obj (obj.{u_6, u_6, u_2, u_2} (shiftFunctor D n) ((Φ a').obj X)) ⟶ G.obj ((Φ a).obj X))
    (G.map (NatTrans.app (Iso.hom (shiftIso (F.lift G Φ hΦ) n a a' h)) X) :
      G.obj (obj.{u_6, u_6, u_2, u_2} (shiftFunctor D n) ((Φ a').obj X)) ⟶ G.obj ((Φ a).obj X))
    (NatTrans.app (Iso.hom (commShiftIso G n)) ((Φ a').obj X) ≫
        map (shiftFunctor E n) ((hΦ a').hom.app X) ≫ (F.shiftIso n a a' h).hom.app X ≫ (hΦ a).inv.app X :
      G.obj (obj.{u_6, u_6, u_2, u_2} (shiftFunctor D n) ((Φ a').obj X)) ⟶ G.obj ((Φ a).obj X))

Tactic:
lift.map_shiftIso_hom_app ..

Premises used: _private.0.CategoryTheory.SingleFunctors.lift.map_shiftIso_hom_app
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctorsLift
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 a a' : A
ha' : n + a = a'
w :
  ∀ (X : C),
    (Iso.hom (shiftIso (postcomp (F.lift G Φ hΦ) G) n a a' ha') ≫ (hΦ a).hom).app X =
      (whiskerRight (hΦ a').hom (shiftFunctor E n) ≫ (F.shiftIso n a a' ha').hom).app X
⊢ Iso.hom (shiftIso (postcomp (F.lift G Φ hΦ) G) n a a' ha') ≫ (hΦ a).hom =
    whiskerRight (hΦ a').hom (shiftFunctor E n) ≫ (F.shiftIso n a a' ha').hom

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctorsLift
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 a a' : A
ha' : n + a = a'
X : C
⊢ (hΦ a).inv.app X ≫ (hΦ a).hom.app X = 𝟙 ((F.functor a).obj X)

Tactic:
have := (hΦ a).inv_hom_id_app X
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctorsLift
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 a a' : A
ha' : n + a = a'
X : C
this : (hΦ a).inv.app X ≫ (hΦ a).hom.app X = 𝟙 ((F.functor a).obj X)
⊢ (Iso.hom (shiftIso (postcomp (F.lift G Φ hΦ) G) n a a' ha') ≫ (hΦ a).hom).app X =
    (whiskerRight (hΦ a').hom (shiftFunctor E n) ≫ (F.shiftIso n a a' ha').hom).app X

Tactic:
simp [map_lift_shiftIso_hom_app, this]

Premises used: CategoryTheory.SingleFunctors.map_lift_shiftIso_hom_app
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctorsLift
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
inst_9 : Preadditive.{u_5, u_1} C
inst_10 : Preadditive.{u_6, u_2} D
inst_11 : Preadditive.{u_7, u_3} E
inst_12 : G.Additive
a : A
inst_13 : (F.functor a).Additive
dsimp : (Φ a ⋙ G).Additive
⊢ (functor (F.lift G Φ hΦ) a ⋙ G).Additive

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctorsLift
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
inst_9 : Preadditive.{u_5, u_1} C
inst_10 : Preadditive.{u_6, u_2} D
inst_11 : Preadditive.{u_7, u_3} E
inst_12 : G.Additive
a : A
inst_13 rwa rwa₁ rwa₂ rwa₃ : (F.functor a).Additive
⊢ (Φ a ⋙ G).Additive

Tactic:
rwa [Functor.additive_iff_of_iso (hΦ a)]

Premises used: CategoryTheory.Functor.additive_iff_of_iso
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctorsLift
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
inst_9 : Preadditive.{u_5, u_1} C
inst_10 : Preadditive.{u_6, u_2} D
inst_11 : Preadditive.{u_7, u_3} E
inst_12 : G.Additive
a : A
inst_13 : (F.functor a).Additive
⊢ (functor (F.lift G Φ hΦ) a ⋙ G).Additive

Tactic:
have : ((lift F G Φ hΦ).functor a ⋙ G).Additive := by
    dsimp
    rwa [Functor.additive_iff_of_iso (hΦ a)]