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 H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
iso : (a : A) → F.functor a ≅ G.functor a
comm :
  ∀ (n a a' : A) (ha' : n + a = a'),
    (F.shiftIso n a a' ha').hom ≫ (iso a).hom =
      whiskerRight (iso a').hom (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
n a a' : A
ha' : n + a = a'
rw :
  ((G.shiftIso n a a' ha').hom ≫ (iso a).inv) ≫ (iso a).hom =
    (whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom) ≫ (iso a).hom
rw₁ :
  (G.shiftIso n a a' ha').hom ≫ (iso a).inv ≫ (iso a).hom =
    (whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom) ≫ (iso a).hom
rw₂ :
  (G.shiftIso n a a' ha').hom ≫ (iso a).inv ≫ (iso a).hom =
    whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom ≫ (iso a).hom
rw₃ :
  (G.shiftIso n a a' ha').hom ≫ 𝟙 (G.functor a) =
    whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom ≫ (iso a).hom
rw₄ :
  (G.shiftIso n a a' ha').hom = whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom ≫ (iso a).hom
rw₅ :
  (G.shiftIso n a a' ha').hom =
    whiskerRight (iso a').inv (shiftFunctor D n) ≫
      whiskerRight (iso a').hom (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
rw₆ :
  (G.shiftIso n a a' ha').hom =
    whiskerRight ((iso a').inv ≫ (iso a').hom) (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
rw₇ : (G.shiftIso n a a' ha').hom = whiskerRight (𝟙 (G.functor a')) (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
rw₈ : (G.shiftIso n a a' ha').hom = 𝟙 (G.functor a' ⋙ shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
rw₉ rw₁₀ : (G.shiftIso n a a' ha').hom = (G.shiftIso n a a' ha').hom
⊢ (G.shiftIso n a a' ha').hom ≫ (iso a).inv = whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom

Tactic:
rw [← cancel_mono (iso a).hom, assoc, assoc, Iso.inv_hom_id, comp_id, comm,
          ← whiskerRight_comp_assoc, Iso.inv_hom_id, whiskerRight_id', id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Functor.whiskerRight_id', CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Functor.whiskerRight_comp_assoc, CategoryTheory.Iso.hom, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctors
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
rw : (e.hom ≫ e.inv).hom n = 𝟙 (F.functor n)
rw₁ : Hom.hom (𝟙 F) n = 𝟙 (F.functor n)
rw₂ rw₃ : 𝟙 (F.functor n) = 𝟙 (F.functor n)
⊢ e.hom.hom n ≫ e.inv.hom n = 𝟙 (F.functor n)

Tactic:
rw [← comp_hom, e.hom_inv_id, id_hom]

Premises used: CategoryTheory.SingleFunctors.id_hom, CategoryTheory.Iso.hom_inv_id, CategoryTheory.SingleFunctors.comp_hom
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctors
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
rw : (e.inv ≫ e.hom).hom n = 𝟙 (G.functor n)
rw₁ : Hom.hom (𝟙 G) n = 𝟙 (G.functor n)
rw₂ rw₃ : 𝟙 (G.functor n) = 𝟙 (G.functor n)
⊢ e.inv.hom n ≫ e.hom.hom n = 𝟙 (G.functor n)

Tactic:
rw [← comp_hom, e.inv_hom_id, id_hom]

Premises used: CategoryTheory.SingleFunctors.id_hom, CategoryTheory.Iso.inv_hom_id, CategoryTheory.SingleFunctors.comp_hom
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctors
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)
rw₂ 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))
⊢ (e.hom.hom n).app X ≫ (e.inv.hom n).app X = 𝟙 ((F.functor n).obj X)

Tactic:
rw [← NatTrans.comp_app, hom_inv_id_hom, NatTrans.id_app]

Premises used: CategoryTheory.SingleFunctors.hom_inv_id_hom, CategoryTheory.NatTrans.id_app, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Shift.SingleFunctors
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)
rw₂ 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))
⊢ (e.inv.hom n).app X ≫ (e.hom.hom n).app X = 𝟙 ((G.functor n).obj X)

Tactic:
rw [← NatTrans.comp_app, inv_hom_id_hom, NatTrans.id_app]

Premises used: CategoryTheory.NatTrans.id_app, CategoryTheory.NatTrans.comp_app, CategoryTheory.SingleFunctors.inv_hom_id_hom
-- 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 H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
f : F ⟶ G
inst_8 : IsIso f
n : A
⊢ IsIso (f.hom n)

Tactic:
inferInstanceAs <| IsIso ((evaluation C D n).map f)

Premises used: _private.0.CategoryTheory.SingleFunctors.instIsIsoFunctorHom._proof_1
-- 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 : Functor.{v_2, v_3, u_2, u_3} D E
inst_8 : G.CommShift A
a : A
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 ⋯) G).hom.app
        X =
      NatTrans.app (Iso.hom ((F.functor a ⋙ G).isoWhiskerLeft (shiftFunctorZero E A))) X
⊢ (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)

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 : Functor.{v_2, v_3, u_2, u_3} D E
inst_8 : G.CommShift A
a : A
X : C
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 ⋯)) X) =
    NatTrans.app (Iso.hom (shiftFunctorZero E A)) (G.obj ((F.functor a).obj X))
⊢ ((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

Tactic:
dsimp
-- 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 : Functor.{v_2, v_3, u_2, u_3} D E
inst_8 : G.CommShift A
a : A
X : C
⊢ 𝟙 (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 ⋯)) X) =
    NatTrans.app (Iso.hom (shiftFunctorZero E A)) (G.obj ((F.functor a).obj X))

Tactic:
simp only [Functor.commShiftIso_zero, Functor.CommShift.isoZero_inv_app,
      SingleFunctors.shiftIso_zero_hom_app, id_comp, assoc, ← G.map_comp, Iso.inv_hom_id_app,
      Functor.map_id, Functor.id_obj, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.CommShift.isoZero_inv_app, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.SingleFunctors.shiftIso_zero_hom_app, CategoryTheory.Functor.CommShift.commShiftIso_zero, CategoryTheory.Category.id_comp
-- 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 : 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''
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'' ⋯) 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
⊢ (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

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 : 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
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'' ⋯).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)
⊢ ((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

Tactic:
dsimp
-- 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 : 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
⊢ Eq (α :=
    obj.{v_3, v_3, u_3, u_3} (shiftFunctor E (m + n)) (G.obj ((F.functor a'').obj X)) ⟶ G.obj ((F.functor a).obj X))
    (NatTrans.app (Iso.hom (shiftFunctorAdd E m n)) (G.obj ((F.functor a'').obj X)) ≫
      Functor.map (shiftFunctor E n) (NatTrans.app (Iso.inv (commShiftIso G m)) ((F.functor a'').obj X)) ≫
        NatTrans.app (Iso.inv (commShiftIso G n))
            (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D m) ((F.functor a'').obj X)) ≫
          G.map (NatTrans.app (Iso.inv (shiftFunctorAdd D m n)) ((F.functor a'').obj X)) ≫
            G.map (NatTrans.app (Iso.hom (shiftFunctorAdd D m n)) ((F.functor a'').obj X)) ≫
              G.map (Functor.map (shiftFunctor D n) ((F.shiftIso m a' a'' ha'').hom.app X)) ≫
                G.map ((F.shiftIso n a a' ha').hom.app X))
    (NatTrans.app (Iso.hom (shiftFunctorAdd E m n)) (G.obj ((F.functor a'').obj X)) ≫
      Functor.map (shiftFunctor E n) (NatTrans.app (Iso.inv (commShiftIso G m)) ((F.functor a'').obj X)) ≫
        NatTrans.app (Iso.inv (commShiftIso G n))
            (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D m) ((F.functor a'').obj X)) ≫
          G.map (Functor.map (shiftFunctor D n) ((F.shiftIso m a' a'' ha'').hom.app X)) ≫
            G.map ((F.shiftIso n a a' ha').hom.app X))

Tactic:
simp only [← G.map_comp, Iso.inv_hom_id_app_assoc]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app_assoc
-- 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 : 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'
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)
⊢ 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'))

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 : 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'
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:
simpa using G.congr_map (congr_app (φ.comm n a a' ha') X)

Premises used: CategoryTheory.SingleFunctors.Hom.comm, CategoryTheory.Functor.congr_map, CategoryTheory.congr_app
-- 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 : 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'
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)
⊢ 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'))

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 : 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'
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:
simp [Functor.commShiftIso_comp_inv_app]

Premises used: CategoryTheory.Functor.commShiftIso_comp_inv_app