awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
A : Type u_4
inst_3 : AddMonoid A
inst_4 : HasShift.{v_2, u_2, u_4} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v_1, v_1, u_1, u_1} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
this : HasShift.{v_1, u_1, u_4} C A := hF.hasShift s i
a b : A
X : C
⊢ Eq (α := (s (a + b) ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D (a + b)).obj X) (NatTrans.app (Iso.hom (i (a + b))) X)
    (NatTrans.app (Iso.hom (isoAdd (i a) (i b))) X)

Tactic:
simp [ShiftMkCore.shiftFunctorAdd_eq, ShiftMkCore.shiftFunctor_eq,
        ← Functor.map_comp_assoc]

Premises used: CategoryTheory.Functor.map_comp_assoc, CategoryTheory.ShiftMkCore.shiftFunctorAdd_eq, CategoryTheory.ShiftMkCore.shiftFunctor_eq
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
A : Type u_4
inst_3 : AddMonoid A
inst_4 : HasShift.{v_2, u_2, u_4} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v_1, v_1, u_1, u_1} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
this : HasShift.{v_1, u_1, u_4} C A := hF.hasShift s i
⊢ F.CommShift A

Tactic:
exact
  { commShiftIso := i
    commShiftIso_zero := by
      ext X
      simp [ShiftMkCore.shiftFunctorZero_eq]
    commShiftIso_add := fun a b => by
      ext X
      simp [ShiftMkCore.shiftFunctorAdd_eq, ShiftMkCore.shiftFunctor_eq,
        ← Functor.map_comp_assoc] }
-- Module: Mathlib.CategoryTheory.Shift.CommShift
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_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_2, u_2, u_4} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v_1, v_1, u_1, u_1} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
a : A
⊢ commShiftIso F a = i a

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Shift.CommShift
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_4
inst_2 : AddCommMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.CommShift A
X : C
a b : A
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a ⋙ shiftFunctor C b) X) ⟶
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b ⋙ shiftFunctor C a) X))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorComm C a b)) X))
    (CategoryStruct.comp (Y := (F ⋙ shiftFunctor D b).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.hom (shiftFunctorComm D a b)) (F.obj X) ≫
          map (shiftFunctor D a) (NatTrans.app (Iso.inv (commShiftIso F b)) X) ≫
            NatTrans.app (Iso.inv (commShiftIso F a)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))

Tactic:
map_shiftFunctorComm_hom_app _ _ _ _

Premises used: CategoryTheory.Functor.map_shiftFunctorComm_hom_app
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_3 : G.Full
inst_4 : G.Faithful
A : Type u_5
inst_5 : AddMonoid A
inst_6 : HasShift.{v_1, u_1, u_5} C A
inst_7 : HasShift.{v_2, u_2, u_5} D A
inst_8 : HasShift.{v_3, u_3, u_5} E A
inst_9 : G.CommShift A
inst_10 : H.CommShift A
a : A
X : C
⊢ Eq (α :=
    obj (obj (whiskeringRight C D E) G) (shiftFunctor C a ⋙ F) ⟶
      obj (obj (whiskeringRight C D E) G) (F ⋙ shiftFunctor D a))
    (map (obj (whiskeringRight C D E) G) (Iso.hom (iso e a)))
    (Iso.hom
      (associator (shiftFunctor C a) F G ≪≫
        isoWhiskerLeft (shiftFunctor C a) e ≪≫
          commShiftIso H a ≪≫
            isoWhiskerRight e.symm (shiftFunctor E a) ≪≫
              F.associator G (shiftFunctor E a) ≪≫
                F.isoWhiskerLeft (Iso.symm (commShiftIso G a)) ≪≫ (F.associator (shiftFunctor D a) G).symm))

Tactic:
have h : ((whiskeringRight C D E).obj G).map (iso e a).hom = _ :=
    Functor.map_preimage _ _
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_3 : G.Full
inst_4 : G.Faithful
A : Type u_5
inst_5 : AddMonoid A
inst_6 : HasShift.{v_1, u_1, u_5} C A
inst_7 : HasShift.{v_2, u_2, u_5} D A
inst_8 : HasShift.{v_3, u_3, u_5} E A
inst_9 : G.CommShift A
inst_10 : H.CommShift A
a : A
X : C
h :
  Eq (α :=
    obj (obj (whiskeringRight C D E) G) (shiftFunctor C a ⋙ F) ⟶
      obj (obj (whiskeringRight C D E) G) (F ⋙ shiftFunctor D a))
    (map (obj (whiskeringRight C D E) G) (Iso.hom (iso e a)))
    (Iso.hom
      (associator (shiftFunctor C a) F G ≪≫
        isoWhiskerLeft (shiftFunctor C a) e ≪≫
          commShiftIso H a ≪≫
            isoWhiskerRight e.symm (shiftFunctor E a) ≪≫
              F.associator G (shiftFunctor E a) ≪≫
                F.isoWhiskerLeft (Iso.symm (commShiftIso G a)) ≪≫ (F.associator (shiftFunctor D a) G).symm))
⊢ Eq (α := G.obj ((shiftFunctor C a ⋙ F).obj X) ⟶ G.obj ((F ⋙ shiftFunctor D a).obj X))
    (G.map (NatTrans.app (Iso.hom (iso e a)) X))
    (e.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      CategoryStruct.comp (Y := (H ⋙ shiftFunctor E a).obj X) (NatTrans.app (Iso.hom (commShiftIso H a)) X)
        (map (shiftFunctor E a) (e.inv.app X) ≫ NatTrans.app (Iso.inv (commShiftIso G a)) (F.obj X)))

Tactic:
simpa using congr_app h X

Premises used: CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_3 : G.Full
inst_4 : G.Faithful
A : Type u_5
inst_5 : AddMonoid A
inst_6 : HasShift.{v_1, u_1, u_5} C A
inst_7 : HasShift.{v_2, u_2, u_5} D A
inst_8 : HasShift.{v_3, u_3, u_5} E A
inst_9 : G.CommShift A
inst_10 : H.CommShift A
a : A
X : C
⊢ Eq (α :=
    obj (obj (whiskeringRight C D E) G) (F ⋙ shiftFunctor D a) ⟶
      obj (obj (whiskeringRight C D E) G) (shiftFunctor C a ⋙ F))
    (map (obj (whiskeringRight C D E) G) (Iso.inv (iso e a)))
    (Iso.inv
      (associator (shiftFunctor C a) F G ≪≫
        isoWhiskerLeft (shiftFunctor C a) e ≪≫
          commShiftIso H a ≪≫
            isoWhiskerRight e.symm (shiftFunctor E a) ≪≫
              F.associator G (shiftFunctor E a) ≪≫
                F.isoWhiskerLeft (Iso.symm (commShiftIso G a)) ≪≫ (F.associator (shiftFunctor D a) G).symm))

Tactic:
have h : ((whiskeringRight C D E).obj G).map (iso e a).inv = _ :=
    Functor.map_preimage _ _
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_3 : G.Full
inst_4 : G.Faithful
A : Type u_5
inst_5 : AddMonoid A
inst_6 : HasShift.{v_1, u_1, u_5} C A
inst_7 : HasShift.{v_2, u_2, u_5} D A
inst_8 : HasShift.{v_3, u_3, u_5} E A
inst_9 : G.CommShift A
inst_10 : H.CommShift A
a : A
X : C
h :
  Eq (α :=
    obj (obj (whiskeringRight C D E) G) (F ⋙ shiftFunctor D a) ⟶
      obj (obj (whiskeringRight C D E) G) (shiftFunctor C a ⋙ F))
    (map (obj (whiskeringRight C D E) G) (Iso.inv (iso e a)))
    (Iso.inv
      (associator (shiftFunctor C a) F G ≪≫
        isoWhiskerLeft (shiftFunctor C a) e ≪≫
          commShiftIso H a ≪≫
            isoWhiskerRight e.symm (shiftFunctor E a) ≪≫
              F.associator G (shiftFunctor E a) ≪≫
                F.isoWhiskerLeft (Iso.symm (commShiftIso G a)) ≪≫ (F.associator (shiftFunctor D a) G).symm))
⊢ Eq (α := G.obj ((F ⋙ shiftFunctor D a).obj X) ⟶ G.obj ((shiftFunctor C a ⋙ F).obj X))
    (G.map (NatTrans.app (Iso.inv (iso e a)) X))
    (CategoryStruct.comp (Y := (G ⋙ shiftFunctor E a).obj (F.obj X))
      (NatTrans.app (Iso.hom (commShiftIso G a)) (F.obj X))
      (map (shiftFunctor E a) (e.hom.app X) ≫
        NatTrans.app (Iso.inv (commShiftIso H a)) X ≫ e.inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))

Tactic:
simpa using congr_app h X

Premises used: CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
A_1 : Type u_4
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_3 : G.Full
inst_4 : G.Faithful
A : Type u_5
inst_5 : AddMonoid A
inst_6 : HasShift.{v_1, u_1, u_5} C A
inst_7 : HasShift.{v_2, u_2, u_5} D A
inst_8 : HasShift.{v_3, u_3, u_5} E A
inst_9 : G.CommShift A
inst_10 : H.CommShift A
w :
  ∀ (X : C),
    Eq (α :=
      (shiftFunctor.{v_1, u_1, u_5} C (A := A) 0 ⋙ F).obj X ⟶ (F ⋙ shiftFunctor.{v_2, u_2, u_5} D (A := A) 0).obj X)
      (NatTrans.app (Iso.hom (OfComp.iso e 0)) X) (NatTrans.app (Iso.hom (isoZero F A)) X)
⊢ Eq (α := shiftFunctor.{v_1, u_1, u_5} C (A := A) 0 ⋙ F ≅ F ⋙ shiftFunctor.{v_2, u_2, u_5} D (A := A) 0)
    (OfComp.iso e 0) (isoZero F A)

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
A_1 : Type u_4
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_3 : G.Full
inst_4 : G.Faithful
A : Type u_5
inst_5 : AddMonoid A
inst_6 : HasShift.{v_1, u_1, u_5} C A
inst_7 : HasShift.{v_2, u_2, u_5} D A
inst_8 : HasShift.{v_3, u_3, u_5} E A
inst_9 : G.CommShift A
inst_10 : H.CommShift A
X : C
w :
  Eq (α :=
    G.obj ((shiftFunctor.{v_1, u_1, u_5} C (A := A) 0 ⋙ F).obj X) ⟶
      G.obj ((F ⋙ shiftFunctor.{v_2, u_2, u_5} D (A := A) 0).obj X))
    (G.map (NatTrans.app (Iso.hom (OfComp.iso e 0)) X)) (G.map (NatTrans.app (Iso.hom (isoZero F A)) X))
⊢ Eq (α :=
    (shiftFunctor.{v_1, u_1, u_5} C (A := A) 0 ⋙ F).obj X ⟶ (F ⋙ shiftFunctor.{v_2, u_2, u_5} D (A := A) 0).obj X)
    (NatTrans.app (Iso.hom (OfComp.iso e 0)) X) (NatTrans.app (Iso.hom (isoZero F A)) X)

Tactic:
apply G.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
A_1 : Type u_4
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_3 : G.Full
inst_4 : G.Faithful
A : Type u_5
inst_5 : AddMonoid A
inst_6 : HasShift.{v_1, u_1, u_5} C A
inst_7 : HasShift.{v_2, u_2, u_5} D A
inst_8 : HasShift.{v_3, u_3, u_5} E A
inst_9 : G.CommShift A
inst_10 : H.CommShift A
X : C
⊢ Eq (α :=
    G.obj ((shiftFunctor.{v_1, u_1, u_5} C (A := A) 0 ⋙ F).obj X) ⟶
      G.obj ((F ⋙ shiftFunctor.{v_2, u_2, u_5} D (A := A) 0).obj X))
    (G.map (NatTrans.app (Iso.hom (OfComp.iso e 0)) X)) (G.map (NatTrans.app (Iso.hom (isoZero F A)) X))

Tactic:
simp [G.commShiftIso_zero, H.commShiftIso_zero]

Premises used: CategoryTheory.Functor.CommShift.commShiftIso_zero
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
A_1 : Type u_4
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_3 : G.Full
inst_4 : G.Faithful
A : Type u_5
inst_5 : AddMonoid A
inst_6 : HasShift.{v_1, u_1, u_5} C A
inst_7 : HasShift.{v_2, u_2, u_5} D A
inst_8 : HasShift.{v_3, u_3, u_5} E A
inst_9 : G.CommShift A
inst_10 : H.CommShift A
a b : A
w :
  ∀ (X : C),
    Eq (α := (shiftFunctor C (a + b) ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D (a + b)).obj X)
      (NatTrans.app (Iso.hom (OfComp.iso e (a + b))) X)
      (NatTrans.app (Iso.hom (isoAdd (OfComp.iso e a) (OfComp.iso e b))) X)
⊢ Eq (α := shiftFunctor C (a + b) ⋙ F ≅ F ⋙ shiftFunctor D (a + b)) (OfComp.iso e (a + b))
    (isoAdd (OfComp.iso e a) (OfComp.iso e b))

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
A_1 : Type u_4
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_3 : G.Full
inst_4 : G.Faithful
A : Type u_5
inst_5 : AddMonoid A
inst_6 : HasShift.{v_1, u_1, u_5} C A
inst_7 : HasShift.{v_2, u_2, u_5} D A
inst_8 : HasShift.{v_3, u_3, u_5} E A
inst_9 : G.CommShift A
inst_10 : H.CommShift A
a b : A
X : C
w :
  Eq (α := G.obj ((shiftFunctor C (a + b) ⋙ F).obj X) ⟶ G.obj ((F ⋙ shiftFunctor D (a + b)).obj X))
    (G.map (NatTrans.app (Iso.hom (OfComp.iso e (a + b))) X))
    (G.map (NatTrans.app (Iso.hom (isoAdd (OfComp.iso e a) (OfComp.iso e b))) X))
⊢ Eq (α := (shiftFunctor C (a + b) ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D (a + b)).obj X)
    (NatTrans.app (Iso.hom (OfComp.iso e (a + b))) X)
    (NatTrans.app (Iso.hom (isoAdd (OfComp.iso e a) (OfComp.iso e b))) X)

Tactic:
apply G.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
A_1 : Type u_4
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_3 : G.Full
inst_4 : G.Faithful
A : Type u_5
inst_5 : AddMonoid A
inst_6 : HasShift.{v_1, u_1, u_5} C A
inst_7 : HasShift.{v_2, u_2, u_5} D A
inst_8 : HasShift.{v_3, u_3, u_5} E A
inst_9 : G.CommShift A
inst_10 : H.CommShift A
a b : A
X : C
w :
  Eq (α :=
    obj.{v_3, v_3, u_3, u_3} (shiftFunctor E b) (H.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ⟶
      obj.{v_3, v_3, u_3, u_3} (shiftFunctor E b) (G.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))))
    (map (shiftFunctor E b)
      (CategoryStruct.comp (Y := obj.{v_3, v_3, u_3, u_3} (shiftFunctor E a) (H.obj X))
        (NatTrans.app (Iso.hom (commShiftIso H a)) X)
        (map (shiftFunctor E a) (e.inv.app X) ≫ NatTrans.app (Iso.inv (commShiftIso G a)) (F.obj X))))
    (map (shiftFunctor E b)
      (e.inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫ G.map (NatTrans.app (Iso.hom (OfComp.iso e a)) X)))
⊢ Eq (α :=
    G.obj (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X)) ⟶
      G.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X)))
    ((F ⋙ G).map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      e.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        CategoryStruct.comp (Y :=
          obj.{v_3, v_3, u_3, u_3} (shiftFunctor E b) (H.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
          (NatTrans.app (Iso.hom (commShiftIso H b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
          (map (shiftFunctor E b)
              (CategoryStruct.comp (Y := obj.{v_3, v_3, u_3, u_3} (shiftFunctor E a) (H.obj X))
                (NatTrans.app (Iso.hom (commShiftIso H a)) X)
                (map (shiftFunctor E a) (e.inv.app X) ≫ NatTrans.app (Iso.inv (commShiftIso G a)) (F.obj X))) ≫
            NatTrans.app (Iso.inv (commShiftIso G b)) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)) ≫
              G.map (NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X))))
    (G.map (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X)) ≫
      e.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        CategoryStruct.comp (Y :=
          obj.{v_3, v_3, u_3, u_3} (shiftFunctor E b) (H.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
          (NatTrans.app (Iso.hom (commShiftIso H b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
          (map (shiftFunctor E b)
              (e.inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
                G.map (NatTrans.app (Iso.hom (OfComp.iso e a)) X)) ≫
            NatTrans.app (Iso.inv (commShiftIso G b)) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)) ≫
              G.map (NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X))))

Tactic:
congr 4
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
A_1 : Type u_4
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_3 : G.Full
inst_4 : G.Faithful
A : Type u_5
inst_5 : AddMonoid A
inst_6 : HasShift.{v_1, u_1, u_5} C A
inst_7 : HasShift.{v_2, u_2, u_5} D A
inst_8 : HasShift.{v_3, u_3, u_5} E A
inst_9 : G.CommShift A
inst_10 : H.CommShift A
a b : A
X : C
⊢ Eq (α :=
    obj.{v_3, v_3, u_3, u_3} (shiftFunctor E b) (H.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ⟶
      obj.{v_3, v_3, u_3, u_3} (shiftFunctor E b) (G.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))))
    (map (shiftFunctor E b)
      (CategoryStruct.comp (Y := obj.{v_3, v_3, u_3, u_3} (shiftFunctor E a) (H.obj X))
        (NatTrans.app (Iso.hom (commShiftIso H a)) X)
        (map (shiftFunctor E a) (e.inv.app X) ≫ NatTrans.app (Iso.inv (commShiftIso G a)) (F.obj X))))
    (map (shiftFunctor E b)
      (e.inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫ G.map (NatTrans.app (Iso.hom (OfComp.iso e a)) X)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_3 : G.Full
inst_4 : G.Faithful
A : Type u_5
inst_5 : AddMonoid A
inst_6 : HasShift.{v_1, u_1, u_5} C A
inst_7 : HasShift.{v_2, u_2, u_5} D A
inst_8 : HasShift.{v_3, u_3, u_5} E A
inst_9 : G.CommShift A
inst_10 : H.CommShift A
this : (A : Type u_5) →
  [inst_11 : AddMonoid A] →
    [inst_12 : HasShift.{v_1, u_1, u_5} C A] →
      [inst_13 : HasShift.{v_2, u_2, u_5} D A] →
        [inst_14 : HasShift.{v_3, u_3, u_5} E A] → [G.CommShift A] → [H.CommShift A] → F.CommShift A :=
  ofComp e
⊢ NatTrans.CommShift e.hom A

Tactic:
⟨fun a ↦ ?_⟩

Premises used: CategoryTheory.NatTrans.CommShift.mk
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_3 : G.Full
inst_4 : G.Faithful
A : Type u_5
inst_5 : AddMonoid A
inst_6 : HasShift.{v_1, u_1, u_5} C A
inst_7 : HasShift.{v_2, u_2, u_5} D A
inst_8 : HasShift.{v_3, u_3, u_5} E A
inst_9 : G.CommShift A
inst_10 : H.CommShift A
this : (A : Type u_5) →
  [inst_11 : AddMonoid A] →
    [inst_12 : HasShift.{v_1, u_1, u_5} C A] →
      [inst_13 : HasShift.{v_2, u_2, u_5} D A] →
        [inst_14 : HasShift.{v_3, u_3, u_5} E A] → [G.CommShift A] → [H.CommShift A] → F.CommShift A :=
  ofComp e
refine :
  ∀ (a : A),
    Eq (α := shiftFunctor C a ⋙ F ⋙ G ⟶ H ⋙ shiftFunctor E a)
      (Iso.hom (commShiftIso (F ⋙ G) a) ≫ whiskerRight e.hom (shiftFunctor E a))
      (whiskerLeft (shiftFunctor C a) e.hom ≫ Iso.hom (commShiftIso H a))
⊢ NatTrans.CommShift e.hom A

Tactic:
refine ⟨fun a ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_3 : G.Full
inst_4 : G.Faithful
A : Type u_5
inst_5 : AddMonoid A
inst_6 : HasShift.{v_1, u_1, u_5} C A
inst_7 : HasShift.{v_2, u_2, u_5} D A
inst_8 : HasShift.{v_3, u_3, u_5} E A
inst_9 : G.CommShift A
inst_10 : H.CommShift A
this : (A : Type u_5) →
  [inst_11 : AddMonoid A] →
    [inst_12 : HasShift.{v_1, u_1, u_5} C A] →
      [inst_13 : HasShift.{v_2, u_2, u_5} D A] →
        [inst_14 : HasShift.{v_3, u_3, u_5} E A] → [G.CommShift A] → [H.CommShift A] → F.CommShift A :=
  ofComp e
a : A
w :
  ∀ (X : C),
    Eq (α := (shiftFunctor C a ⋙ F ⋙ G).obj X ⟶ (H ⋙ shiftFunctor E a).obj X)
      (NatTrans.app (Iso.hom (commShiftIso (F ⋙ G) a) ≫ whiskerRight e.hom (shiftFunctor E a)) X)
      (NatTrans.app (whiskerLeft (shiftFunctor C a) e.hom ≫ Iso.hom (commShiftIso H a)) X)
⊢ Eq (α := shiftFunctor C a ⋙ F ⋙ G ⟶ H ⋙ shiftFunctor E a)
    (Iso.hom (commShiftIso (F ⋙ G) a) ≫ whiskerRight e.hom (shiftFunctor E a))
    (whiskerLeft (shiftFunctor C a) e.hom ≫ Iso.hom (commShiftIso H a))

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Shift.CommShift
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_3 : G.Full
inst_4 : G.Faithful
A : Type u_5
inst_5 : AddMonoid A
inst_6 : HasShift.{v_1, u_1, u_5} C A
inst_7 : HasShift.{v_2, u_2, u_5} D A
inst_8 : HasShift.{v_3, u_3, u_5} E A
inst_9 : G.CommShift A
inst_10 : H.CommShift A
this : (A : Type u_5) →
  [inst_11 : AddMonoid A] →
    [inst_12 : HasShift.{v_1, u_1, u_5} C A] →
      [inst_13 : HasShift.{v_2, u_2, u_5} D A] →
        [inst_14 : HasShift.{v_3, u_3, u_5} E A] → [G.CommShift A] → [H.CommShift A] → F.CommShift A :=
  ofComp e
a : A
X : C
⊢ Eq (α := (shiftFunctor C a ⋙ F ⋙ G).obj X ⟶ (H ⋙ shiftFunctor E a).obj X)
    (NatTrans.app (Iso.hom (commShiftIso (F ⋙ G) a) ≫ whiskerRight e.hom (shiftFunctor E a)) X)
    (NatTrans.app (whiskerLeft (shiftFunctor C a) e.hom ≫ Iso.hom (commShiftIso H a)) X)

Tactic:
simp [commShiftIso_comp_hom_app, show F.commShiftIso a = OfComp.iso e a from rfl,
    ← Functor.map_comp]

Premises used: CategoryTheory.Functor.commShiftIso_comp_hom_app, CategoryTheory.Functor.map_comp, rfl