awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Shift.CommShiftTwo
Goal:
C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₁'
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₂'
inst_4 : Category.{v_5, u_5} D
M : Type u_6
inst_5 : AddCommMonoid M
inst_6 : HasShift.{v_1, u_1, u_6} C₁ M
inst_7 : HasShift.{v_3, u_3, u_6} C₂ M
inst_8 : HasShift.{v_5, u_5, u_6} D M
G₁ G₂ G₃ : C₁ ⥤ Functor.{v_3, v_5, u_3, u_5} C₂ D
τ : G₁ ⟶ G₂
τ' : G₂ ⟶ G₃
h : CommShift₂Setup.{v_5, u_5, u_6} D M
inst_9 : G₁.CommShift₂ h
inst_10 : G₂.CommShift₂ h
inst_11 : G₃.CommShift₂ h
inst_12 : CommShift₂ τ h
inst_13 : CommShift₂ τ' h
x : C₂
⊢ CommShift (F₁ := G₁.flip.obj x) (F₂ := G₃.flip.obj x)
    (CategoryStruct.comp (Y := G₂.flip.obj x) (app (Functor.map (flipFunctor C₁ C₂ D) τ) x)
        (app (Functor.map (flipFunctor C₁ C₂ D) τ') x) :
      G₁.flip.obj x ⟶ G₃.flip.obj x)
    M

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_3
D : Type u_1
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_2, u_1} D
F : Functor.{v_1, v_2, u_3, u_1} C D
A : Type u_2
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_3, u_2} C A
s : A → Functor.{v_2, v_2, u_1, u_1} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
X : C
⊢ F.whiskerLeft (zero F s i).hom =
    (i 0 ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm).hom

Tactic:
have h : whiskerLeft F (zero F s i).hom = _ :=
    ((whiskeringLeft C D D).obj F).map_preimage _
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_3
D : Type u_1
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_2, u_1} D
F : Functor.{v_1, v_2, u_3, u_1} C D
A : Type u_2
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_3, u_2} C A
s : A → Functor.{v_2, v_2, u_1, u_1} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
X : C
h :
  F.whiskerLeft (zero F s i).hom =
    (i 0 ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm).hom
⊢ (i 0 ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm).hom.app X =
    NatTrans.app (Iso.hom (i 0)) X ≫ F.map (NatTrans.app (Iso.hom (shiftFunctorZero C A)) X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_3
D : Type u_1
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_2, u_1} D
F : Functor.{v_1, v_2, u_3, u_1} C D
A : Type u_2
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_3, u_2} C A
s : A → Functor.{v_2, v_2, u_1, u_1} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
X : C
h :
  F.whiskerLeft (zero F s i).hom =
    (i 0 ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm).hom
⊢ (zero F s i).hom.app (F.obj X) =
    NatTrans.app (Iso.hom (i 0)) X ≫ F.map (NatTrans.app (Iso.hom (shiftFunctorZero C A)) X)

Tactic:
exact (NatTrans.congr_app h X).trans (by simp)

Premises used: CategoryTheory.NatTrans.congr_app, Eq.trans
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_2
D : Type u_1
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} D
F : Functor.{v_1, v_2, u_2, u_1} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_3} C A
s : A → Functor.{v_2, v_2, u_1, u_1} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
X : C
⊢ F.whiskerLeft (zero F s i).inv =
    (i 0 ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm).inv

Tactic:
have h : whiskerLeft F (zero F s i).inv = _ :=
    ((whiskeringLeft C D D).obj F).map_preimage _
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_2
D : Type u_1
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} D
F : Functor.{v_1, v_2, u_2, u_1} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_3} C A
s : A → Functor.{v_2, v_2, u_1, u_1} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
X : C
h :
  F.whiskerLeft (zero F s i).inv =
    (i 0 ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm).inv
⊢ (i 0 ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm).inv.app X =
    F.map (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X) ≫ NatTrans.app (Iso.inv (i 0)) X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_2
D : Type u_1
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} D
F : Functor.{v_1, v_2, u_2, u_1} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_3} C A
s : A → Functor.{v_2, v_2, u_1, u_1} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
X : C
h :
  F.whiskerLeft (zero F s i).inv =
    (i 0 ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm).inv
⊢ (zero F s i).inv.app (F.obj X) =
    F.map (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X) ≫ NatTrans.app (Iso.inv (i 0)) X

Tactic:
exact (NatTrans.congr_app h X).trans (by simp)

Premises used: CategoryTheory.NatTrans.congr_app, Eq.trans
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_3
D : Type u_1
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_2, u_1} D
F : Functor.{v_1, v_2, u_3, u_1} C D
A : Type u_2
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_3, u_2} C A
s : A → Functor.{v_2, v_2, u_1, u_1} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
a b : A
X : C
⊢ F.whiskerLeft (add F s i a b).hom =
    (i (a + b) ≪≫
        isoWhiskerRight (shiftFunctorAdd C a b) F ≪≫
          associator (shiftFunctor C a) (shiftFunctor C b) F ≪≫
            isoWhiskerLeft (shiftFunctor C a) (i b).symm ≪≫
              Iso.symm (associator (shiftFunctor C a) F (s b)) ≪≫
                isoWhiskerRight (i a).symm (s b) ≪≫ F.associator (s a) (s b)).hom

Tactic:
have h : whiskerLeft F (add F s i a b).hom = _ :=
    ((whiskeringLeft C D D).obj F).map_preimage _
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_3
D : Type u_1
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_2, u_1} D
F : Functor.{v_1, v_2, u_3, u_1} C D
A : Type u_2
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_3, u_2} C A
s : A → Functor.{v_2, v_2, u_1, u_1} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
a b : A
X : C
h :
  F.whiskerLeft (add F s i a b).hom =
    (i (a + b) ≪≫
        isoWhiskerRight (shiftFunctorAdd C a b) F ≪≫
          associator (shiftFunctor C a) (shiftFunctor C b) F ≪≫
            isoWhiskerLeft (shiftFunctor C a) (i b).symm ≪≫
              Iso.symm (associator (shiftFunctor C a) F (s b)) ≪≫
                isoWhiskerRight (i a).symm (s b) ≪≫ F.associator (s a) (s b)).hom
⊢ (i (a + b) ≪≫
            isoWhiskerRight (shiftFunctorAdd C a b) F ≪≫
              associator (shiftFunctor C a) (shiftFunctor C b) F ≪≫
                isoWhiskerLeft (shiftFunctor C a) (i b).symm ≪≫
                  Iso.symm (associator (shiftFunctor C a) F (s b)) ≪≫
                    isoWhiskerRight (i a).symm (s b) ≪≫ F.associator (s a) (s b)).hom.app
      X =
    NatTrans.app (Iso.hom (i (a + b))) X ≫
      F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
        (i b).inv.app (obj.{v_1, v_1, u_3, u_3} (shiftFunctor C a) X) ≫ (s b).map ((i a).inv.app X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_3
D : Type u_1
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_2, u_1} D
F : Functor.{v_1, v_2, u_3, u_1} C D
A : Type u_2
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_3, u_2} C A
s : A → Functor.{v_2, v_2, u_1, u_1} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
a b : A
X : C
h :
  F.whiskerLeft (add F s i a b).hom =
    (i (a + b) ≪≫
        isoWhiskerRight (shiftFunctorAdd C a b) F ≪≫
          associator (shiftFunctor C a) (shiftFunctor C b) F ≪≫
            isoWhiskerLeft (shiftFunctor C a) (i b).symm ≪≫
              Iso.symm (associator (shiftFunctor C a) F (s b)) ≪≫
                isoWhiskerRight (i a).symm (s b) ≪≫ F.associator (s a) (s b)).hom
⊢ (add F s i a b).hom.app (F.obj X) =
    NatTrans.app (Iso.hom (i (a + b))) X ≫
      F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
        (i b).inv.app (obj.{v_1, v_1, u_3, u_3} (shiftFunctor C a) X) ≫ (s b).map ((i a).inv.app X)

Tactic:
exact (NatTrans.congr_app h X).trans (by simp)

Premises used: CategoryTheory.NatTrans.congr_app, Eq.trans
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_2
D : Type u_1
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} D
F : Functor.{v_1, v_2, u_2, u_1} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_3} C A
s : A → Functor.{v_2, v_2, u_1, u_1} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
a b : A
X : C
⊢ F.whiskerLeft (add F s i a b).inv =
    (i (a + b) ≪≫
        isoWhiskerRight (shiftFunctorAdd C a b) F ≪≫
          associator (shiftFunctor C a) (shiftFunctor C b) F ≪≫
            isoWhiskerLeft (shiftFunctor C a) (i b).symm ≪≫
              Iso.symm (associator (shiftFunctor C a) F (s b)) ≪≫
                isoWhiskerRight (i a).symm (s b) ≪≫ F.associator (s a) (s b)).inv

Tactic:
have h : whiskerLeft F (add F s i a b).inv = _ :=
    ((whiskeringLeft C D D).obj F).map_preimage _
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_2
D : Type u_1
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} D
F : Functor.{v_1, v_2, u_2, u_1} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_3} C A
s : A → Functor.{v_2, v_2, u_1, u_1} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
a b : A
X : C
h :
  F.whiskerLeft (add F s i a b).inv =
    (i (a + b) ≪≫
        isoWhiskerRight (shiftFunctorAdd C a b) F ≪≫
          associator (shiftFunctor C a) (shiftFunctor C b) F ≪≫
            isoWhiskerLeft (shiftFunctor C a) (i b).symm ≪≫
              Iso.symm (associator (shiftFunctor C a) F (s b)) ≪≫
                isoWhiskerRight (i a).symm (s b) ≪≫ F.associator (s a) (s b)).inv
⊢ (i (a + b) ≪≫
            isoWhiskerRight (shiftFunctorAdd C a b) F ≪≫
              associator (shiftFunctor C a) (shiftFunctor C b) F ≪≫
                isoWhiskerLeft (shiftFunctor C a) (i b).symm ≪≫
                  Iso.symm (associator (shiftFunctor C a) F (s b)) ≪≫
                    isoWhiskerRight (i a).symm (s b) ≪≫ F.associator (s a) (s b)).inv.app
      X =
    (s b).map ((i a).hom.app X) ≫
      (i b).hom.app (obj.{v_1, v_1, u_2, u_2} (shiftFunctor C a) X) ≫
        F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_2
D : Type u_1
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} D
F : Functor.{v_1, v_2, u_2, u_1} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_3} C A
s : A → Functor.{v_2, v_2, u_1, u_1} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
a b : A
X : C
h :
  F.whiskerLeft (add F s i a b).inv =
    (i (a + b) ≪≫
        isoWhiskerRight (shiftFunctorAdd C a b) F ≪≫
          associator (shiftFunctor C a) (shiftFunctor C b) F ≪≫
            isoWhiskerLeft (shiftFunctor C a) (i b).symm ≪≫
              Iso.symm (associator (shiftFunctor C a) F (s b)) ≪≫
                isoWhiskerRight (i a).symm (s b) ≪≫ F.associator (s a) (s b)).inv
⊢ (add F s i a b).inv.app (F.obj X) =
    (s b).map ((i a).hom.app X) ≫
      (i b).hom.app (obj.{v_1, v_1, u_2, u_2} (shiftFunctor C a) X) ≫
        F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X

Tactic:
exact (NatTrans.congr_app h X).trans (by simp)

Premises used: CategoryTheory.NatTrans.congr_app, Eq.trans
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
m₁ m₂ m₃ : A
rw rw₁ : s (m₁ + (m₂ + m₃)) = s (m₁ + (m₂ + m₃))
⊢ s (m₁ + m₂ + m₃) = s (m₁ + (m₂ + m₃))

Tactic:
rw [add_assoc]

Premises used: add_assoc
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
m₁ m₂ m₃ : A
this :
  Iso.hom (Induced.add F s i (m₁ + m₂) m₃) ≫ whiskerRight (Induced.add F s i m₁ m₂).hom (s m₃) =
    eqToHom ⋯ ≫ Iso.hom (Induced.add F s i m₁ (m₂ + m₃)) ≫ (s m₁).whiskerLeft (Induced.add F s i m₂ m₃).hom
X : D
⊢ NatTrans.app (Iso.hom (Induced.add F s i (m₁ + m₂) m₃)) X ≫ (s m₃).map ((Induced.add F s i m₁ m₂).hom.app X) =
    eqToHom ⋯ ≫
      NatTrans.app (Iso.hom (Induced.add F s i m₁ (m₂ + m₃))) X ≫ (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj X)

Tactic:
simpa using NatTrans.congr_app this X

Premises used: CategoryTheory.NatTrans.congr_app
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
m₁ m₂ m₃ : A
suffices :
  Iso.hom (Induced.add F s i (m₁ + m₂) m₃) ≫ whiskerRight (Induced.add F s i m₁ m₂).hom (s m₃) =
    eqToHom ⋯ ≫ Iso.hom (Induced.add F s i m₁ (m₂ + m₃)) ≫ (s m₁).whiskerLeft (Induced.add F s i m₂ m₃).hom
⊢ ∀ (X : D),
    NatTrans.app (Iso.hom (Induced.add F s i (m₁ + m₂) m₃)) X ≫ (s m₃).map ((Induced.add F s i m₁ m₂).hom.app X) =
      eqToHom ⋯ ≫
        NatTrans.app (Iso.hom (Induced.add F s i m₁ (m₂ + m₃))) X ≫ (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj X)

Tactic:
suffices (Induced.add F s i (m₁ + m₂) m₃).hom ≫
            whiskerRight (Induced.add F s i m₁ m₂).hom (s m₃) =
            eqToHom (by rw [add_assoc]) ≫ (Induced.add F s i m₁ (m₂ + m₃)).hom ≫
              whiskerLeft (s m₁) (Induced.add F s i m₂ m₃).hom by
          intro X
          simpa using NatTrans.congr_app this X
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
m₁ m₂ m₃ : A
a :
  Eq (α :=
    obj (obj (whiskeringLeft C D D) F) (s (m₁ + m₂ + m₃)) ⟶ obj (obj (whiskeringLeft C D D) F) ((s m₁ ⋙ s m₂) ⋙ s m₃))
    (map (obj (whiskeringLeft C D D) F)
      (Iso.hom (Induced.add F s i (m₁ + m₂) m₃) ≫ whiskerRight (Induced.add F s i m₁ m₂).hom (s m₃)))
    (map (obj (whiskeringLeft C D D) F)
      (eqToHom ⋯ ≫ Iso.hom (Induced.add F s i m₁ (m₂ + m₃)) ≫ (s m₁).whiskerLeft (Induced.add F s i m₂ m₃).hom))
⊢ Iso.hom (Induced.add F s i (m₁ + m₂) m₃) ≫ whiskerRight (Induced.add F s i m₁ m₂).hom (s m₃) =
    eqToHom ⋯ ≫ Iso.hom (Induced.add F s i m₁ (m₂ + m₃)) ≫ (s m₁).whiskerLeft (Induced.add F s i m₂ m₃).hom

Tactic:
apply ((whiskeringLeft C D D).obj F).map_injective

Premises used: CategoryTheory.Functor.whiskeringLeft, CategoryTheory.Functor.map_injective, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
m₁ m₂ m₃ : A
a :
  ∀ (X : C),
    Eq (α :=
      (obj (obj (whiskeringLeft C D D) F) (s (m₁ + m₂ + m₃))).obj X ⟶
        (obj (obj (whiskeringLeft C D D) F) ((s m₁ ⋙ s m₂) ⋙ s m₃)).obj X)
      (NatTrans.app
        (map (obj (whiskeringLeft C D D) F)
          (Iso.hom (Induced.add F s i (m₁ + m₂) m₃) ≫ whiskerRight (Induced.add F s i m₁ m₂).hom (s m₃)))
        X)
      (NatTrans.app
        (map (obj (whiskeringLeft C D D) F)
          (eqToHom ⋯ ≫ Iso.hom (Induced.add F s i m₁ (m₂ + m₃)) ≫ (s m₁).whiskerLeft (Induced.add F s i m₂ m₃).hom))
        X)
⊢ Eq (α :=
    obj (obj (whiskeringLeft C D D) F) (s (m₁ + m₂ + m₃)) ⟶ obj (obj (whiskeringLeft C D D) F) ((s m₁ ⋙ s m₂) ⋙ s m₃))
    (map (obj (whiskeringLeft C D D) F)
      (Iso.hom (Induced.add F s i (m₁ + m₂) m₃) ≫ whiskerRight (Induced.add F s i m₁ m₂).hom (s m₃)))
    (map (obj (whiskeringLeft C D D) F)
      (eqToHom ⋯ ≫ Iso.hom (Induced.add F s i m₁ (m₂ + m₃)) ≫ (s m₁).whiskerLeft (Induced.add F s i m₂ m₃).hom))

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
m₁ m₂ m₃ : A
X : C
a :
  NatTrans.app (Iso.hom (Induced.add F s i (m₁ + m₂) m₃)) (F.obj X) ≫
      (s m₃).map ((Induced.add F s i m₁ m₂).hom.app (F.obj X)) =
    NatTrans.app (eqToHom ⋯) (F.obj X) ≫
      NatTrans.app (Iso.hom (Induced.add F s i m₁ (m₂ + m₃))) (F.obj X) ≫
        (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X))
⊢ Eq (α :=
    (obj (obj (whiskeringLeft C D D) F) (s (m₁ + m₂ + m₃))).obj X ⟶
      (obj (obj (whiskeringLeft C D D) F) ((s m₁ ⋙ s m₂) ⋙ s m₃)).obj X)
    (NatTrans.app
      (map (obj (whiskeringLeft C D D) F)
        (Iso.hom (Induced.add F s i (m₁ + m₂) m₃) ≫ whiskerRight (Induced.add F s i m₁ m₂).hom (s m₃)))
      X)
    (NatTrans.app
      (map (obj (whiskeringLeft C D D) F)
        (eqToHom ⋯ ≫ Iso.hom (Induced.add F s i m₁ (m₂ + m₃)) ≫ (s m₁).whiskerLeft (Induced.add F s i m₂ m₃).hom))
      X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
m₁ m₂ m₃ : A
X : C
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m₁ + m₂ + m₃)) X) ⟶
      F.obj
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₃)
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁ ⋙ shiftFunctor C m₂) X)))
    (F.map
      (NatTrans.app (Iso.hom (shiftFunctorAdd' C (m₁ + m₂) m₃ (m₁ + m₂ + m₃) ⋯)) X ≫
        map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd' C m₁ m₂ (m₁ + m₂) ⋯)) X)))
    (F.map
      (NatTrans.app (Iso.hom (shiftFunctorAdd' C m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯)) X ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C m₂ m₃ (m₂ + m₃) ⋯)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X)))

Tactic:
have eq := F.congr_map (shiftFunctorAdd'_assoc_hom_app
          m₁ m₂ m₃ _ _ (m₁ + m₂ + m₃) rfl rfl rfl X)
-- Module: Mathlib.CategoryTheory.Shift.Induced
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
m₁ m₂ m₃ : A
X : C
eq :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m₁ + m₂ + m₃)) X) ⟶
      F.obj
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₃)
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁ ⋙ shiftFunctor C m₂) X)))
    (F.map
      (NatTrans.app (Iso.hom (shiftFunctorAdd' C (m₁ + m₂) m₃ (m₁ + m₂ + m₃) ⋯)) X ≫
        map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd' C m₁ m₂ (m₁ + m₂) ⋯)) X)))
    (F.map
      (NatTrans.app (Iso.hom (shiftFunctorAdd' C m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯)) X ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C m₂ m₃ (m₂ + m₃) ⋯)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X)))
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m₁ + m₂ + m₃)) X) ⟶
      F.obj
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₃)
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁ ⋙ shiftFunctor C m₂) X)))
    (F.map
      (NatTrans.app (Iso.hom (shiftFunctorAdd C (m₁ + m₂) m₃)) X ≫
        map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ m₂)) X)))
    (F.map
      (NatTrans.app (Iso.hom (shiftFunctorAdd' C m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯)) X ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X)))

Tactic:
simp only [shiftFunctorAdd'_eq_shiftFunctorAdd] at eq

Premises used: CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd