awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Shift.Quotient
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
r : HomRel.{u, v} C
A : Type w
inst_2 : AddMonoid A
inst_3 : HasShift.{v, u, w} C A
inst_4 : HasShift.{v', u', w} D A
inst_5 : r.IsCompatibleWithShift A
inst_6 : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b : A
w :
  Eq (α := shiftFunctor (Quotient r) (a + b) ⋙ lift r F hF ⟶ lift r F hF ⋙ shiftFunctor D (a + b))
    (Iso.hom (LiftCommShift.iso F r hF (a + b)))
    (Iso.hom (Functor.CommShift.isoAdd (LiftCommShift.iso F r hF a) (LiftCommShift.iso F r hF b)))
⊢ Eq (α := shiftFunctor (Quotient r) (a + b) ⋙ lift r F hF ≅ lift r F hF ⋙ shiftFunctor D (a + b))
    (LiftCommShift.iso F r hF (a + b))
    (Functor.CommShift.isoAdd (LiftCommShift.iso F r hF a) (LiftCommShift.iso F r hF b))

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Shift.Quotient
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
r : HomRel.{u, v} C
A : Type w
inst_2 : AddMonoid A
inst_3 : HasShift.{v, u, w} C A
inst_4 : HasShift.{v', u', w} D A
inst_5 : r.IsCompatibleWithShift A
inst_6 : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b : A
w :
  Eq (α :=
    functor r ⋙ shiftFunctor (Quotient r) (a + b) ⋙ lift r F hF ⟶ functor r ⋙ lift r F hF ⋙ shiftFunctor D (a + b))
    ((functor r).whiskerLeft (Iso.hom (LiftCommShift.iso F r hF (a + b))))
    ((functor r).whiskerLeft
      (Iso.hom (Functor.CommShift.isoAdd (LiftCommShift.iso F r hF a) (LiftCommShift.iso F r hF b))))
⊢ Eq (α := shiftFunctor (Quotient r) (a + b) ⋙ lift r F hF ⟶ lift r F hF ⋙ shiftFunctor D (a + b))
    (Iso.hom (LiftCommShift.iso F r hF (a + b)))
    (Iso.hom (Functor.CommShift.isoAdd (LiftCommShift.iso F r hF a) (LiftCommShift.iso F r hF b)))

Tactic:
apply natTrans_ext

Premises used: CategoryTheory.Quotient.natTrans_ext
-- Module: Mathlib.CategoryTheory.Shift.Quotient
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
r : HomRel.{u, v} C
A : Type w
inst_2 : AddMonoid A
inst_3 : HasShift.{v, u, w} C A
inst_4 : HasShift.{v', u', w} D A
inst_5 : r.IsCompatibleWithShift A
inst_6 : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b : A
w :
  ∀ (X : C),
    Eq (α :=
      (functor r ⋙ shiftFunctor (Quotient r) (a + b) ⋙ lift r F hF).obj X ⟶
        (functor r ⋙ lift r F hF ⋙ shiftFunctor D (a + b)).obj X)
      (NatTrans.app ((functor r).whiskerLeft (Iso.hom (LiftCommShift.iso F r hF (a + b)))) X)
      (NatTrans.app
        ((functor r).whiskerLeft
          (Iso.hom (Functor.CommShift.isoAdd (LiftCommShift.iso F r hF a) (LiftCommShift.iso F r hF b))))
        X)
⊢ Eq (α :=
    functor r ⋙ shiftFunctor (Quotient r) (a + b) ⋙ lift r F hF ⟶ functor r ⋙ lift r F hF ⋙ shiftFunctor D (a + b))
    ((functor r).whiskerLeft (Iso.hom (LiftCommShift.iso F r hF (a + b))))
    ((functor r).whiskerLeft
      (Iso.hom (Functor.CommShift.isoAdd (LiftCommShift.iso F r hF a) (LiftCommShift.iso F r hF b))))

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Shift.Quotient
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
r : HomRel.{u, v} C
A : Type w
inst_2 : AddMonoid A
inst_3 : HasShift.{v, u, w} C A
inst_4 : HasShift.{v', u', w} D A
inst_5 : r.IsCompatibleWithShift A
inst_6 : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b : A
X : C
w :
  Eq (α :=
    (lift r F hF).obj (Functor.obj.{v, v, u, u} (shiftFunctor (Quotient r) (a + b)) ((functor r).obj X)) ⟶
      Functor.obj.{v', v', u', u'} (shiftFunctor D (a + b)) ((lift r F hF).obj ((functor r).obj X)))
    (NatTrans.app (Iso.hom (LiftCommShift.iso F r hF (a + b))) ((functor r).obj X))
    (NatTrans.app (Iso.hom (Functor.CommShift.isoAdd (LiftCommShift.iso F r hF a) (LiftCommShift.iso F r hF b)))
      ((functor r).obj X))
⊢ Eq (α :=
    (functor r ⋙ shiftFunctor (Quotient r) (a + b) ⋙ lift r F hF).obj X ⟶
      (functor r ⋙ lift r F hF ⋙ shiftFunctor D (a + b)).obj X)
    (NatTrans.app ((functor r).whiskerLeft (Iso.hom (LiftCommShift.iso F r hF (a + b)))) X)
    (NatTrans.app
      ((functor r).whiskerLeft
        (Iso.hom (Functor.CommShift.isoAdd (LiftCommShift.iso F r hF a) (LiftCommShift.iso F r hF b))))
      X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Shift.Quotient
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
r : HomRel.{u, v} C
A : Type w
inst_2 : AddMonoid A
inst_3 : HasShift.{v, u, w} C A
inst_4 : HasShift.{v', u', w} D A
inst_5 : r.IsCompatibleWithShift A
inst_6 : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b : A
X : C
⊢ Eq (α :=
    ((shiftFunctor C a ⋙ functor r) ⋙ shiftFunctor (Quotient r) b ⋙ lift r F hF).obj X ⟶
      (F ⋙ shiftFunctor D (a + b)).obj X)
    (CategoryStruct.comp (Y :=
      ((functor r ⋙ shiftFunctor (Quotient r) a) ⋙ shiftFunctor (Quotient r) b ⋙ lift r F hF).obj X)
      ((shiftFunctor (Quotient r) b ⋙ lift r F hF).map (NatTrans.app (Iso.hom (Functor.commShiftIso (functor r) a)) X))
      (CategoryStruct.comp (Y := (((shiftFunctor C a ⋙ functor r) ⋙ shiftFunctor (Quotient r) b) ⋙ lift r F hF).obj X)
        ((shiftFunctor (Quotient r) b ⋙ lift r F hF).map
          (NatTrans.app (Iso.inv (Functor.commShiftIso (functor r) a)) X))
        ((lift r F hF).map
            (NatTrans.app (Iso.inv (Functor.commShiftIso (functor r) b))
              (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)) ≫
          F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫
            F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
              CategoryStruct.comp (Y := (shiftFunctor C a ⋙ F ⋙ shiftFunctor D b).obj X)
                (NatTrans.app (Iso.hom (Functor.commShiftIso F b)) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X))
                (Functor.map (shiftFunctor D b) (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X) ≫
                  NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X)))))
    (NatTrans.app (Iso.hom (LiftCommShift.iso F r hF b)) ((shiftFunctor C a ⋙ functor r).obj X) ≫
      CategoryStruct.comp (Y := (lift r F hF ⋙ shiftFunctor D b).obj ((functor r ⋙ shiftFunctor (Quotient r) a).obj X))
        ((lift r F hF ⋙ shiftFunctor D b).map (NatTrans.app (Iso.hom (Functor.commShiftIso (functor r) a)) X))
        (Functor.map (shiftFunctor D b)
            (CategoryStruct.comp (Y := ((shiftFunctor C a ⋙ functor r) ⋙ lift r F hF).obj X)
              ((lift r F hF).map (NatTrans.app (Iso.inv (Functor.commShiftIso (functor r) a)) X))
              (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) ((functor r ⋙ lift r F hF).obj X)))

Tactic:
simp only [Functor.comp_obj, LiftCommShift.iso_hom_app, Iso.hom_inv_id_app,
      Functor.comp_map, assoc, ← Functor.map_comp_assoc, Iso.inv_hom_id_app,
      Functor.map_id, id_comp, lift_obj_functor_obj]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Quotient.LiftCommShift.iso_hom_app, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Quotient.lift_obj_functor_obj, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Functor.comp_map, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Shift.Quotient
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
r : HomRel.{u, v} C
A : Type w
inst_2 : AddMonoid A
inst_3 : HasShift.{v, u, w} C A
inst_4 : HasShift.{v', u', w} D A
inst_5 : r.IsCompatibleWithShift A
inst_6 : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a : A
w :
  ∀ (X : C),
    Eq (α := (shiftFunctor C a ⋙ functor r ⋙ lift r F hF).obj X ⟶ (F ⋙ shiftFunctor D a).obj X)
      (NatTrans.app
        (Iso.hom (Functor.commShiftIso (functor r ⋙ lift r F hF) a) ≫
          Functor.whiskerRight (lift.isLift r F hF).hom (shiftFunctor D a))
        X)
      (NatTrans.app
        (Functor.whiskerLeft (shiftFunctor C a) (lift.isLift r F hF).hom ≫ Iso.hom (Functor.commShiftIso F a)) X)
⊢ Eq (α := shiftFunctor C a ⋙ functor r ⋙ lift r F hF ⟶ F ⋙ shiftFunctor D a)
    (Iso.hom (Functor.commShiftIso (functor r ⋙ lift r F hF) a) ≫
      Functor.whiskerRight (lift.isLift r F hF).hom (shiftFunctor D a))
    (Functor.whiskerLeft (shiftFunctor C a) (lift.isLift r F hF).hom ≫ Iso.hom (Functor.commShiftIso F a))

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Shift.Quotient
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
r : HomRel.{u, v} C
A : Type w
inst_2 : AddMonoid A
inst_3 : HasShift.{v, u, w} C A
inst_4 : HasShift.{v', u', w} D A
inst_5 : r.IsCompatibleWithShift A
inst_6 : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a : A
X : C
w :
  Eq (α :=
    (lift r F hF).obj ((functor r).obj (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)) ⟶
      Functor.obj.{v', v', u', u'} (shiftFunctor D a) (F.obj X))
    (NatTrans.app (Iso.hom (Functor.commShiftIso (functor r ⋙ lift r F hF) a)) X ≫
      Functor.map (shiftFunctor D a) (𝟙 (F.obj X)))
    (𝟙 (F.obj (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)) ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X)
⊢ Eq (α := (shiftFunctor C a ⋙ functor r ⋙ lift r F hF).obj X ⟶ (F ⋙ shiftFunctor D a).obj X)
    (NatTrans.app
      (Iso.hom (Functor.commShiftIso (functor r ⋙ lift r F hF) a) ≫
        Functor.whiskerRight (lift.isLift r F hF).hom (shiftFunctor D a))
      X)
    (NatTrans.app (Functor.whiskerLeft (shiftFunctor C a) (lift.isLift r F hF).hom ≫ Iso.hom (Functor.commShiftIso F a))
      X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Shift.Quotient
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
r : HomRel.{u, v} C
A : Type w
inst_2 : AddMonoid A
inst_3 : HasShift.{v, u, w} C A
inst_4 : HasShift.{v', u', w} D A
inst_5 : r.IsCompatibleWithShift A
inst_6 : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a : A
X : C
w :
  Eq (α :=
    (lift r F hF).obj ((functor r).obj (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)) ⟶
      Functor.obj.{v', v', u', u'} (shiftFunctor D a) (F.obj X))
    (((lift r F hF).map (𝟙 ((shiftFunctor C a ⋙ functor r).obj X)) ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X) ≫
      Functor.map (shiftFunctor D a) (𝟙 (F.obj X)))
    (𝟙 (F.obj (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)) ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X)
⊢ Eq (α :=
    (lift r F hF).obj ((functor r).obj (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)) ⟶
      Functor.obj.{v', v', u', u'} (shiftFunctor D a) (F.obj X))
    (NatTrans.app (Iso.hom (Functor.commShiftIso (functor r ⋙ lift r F hF) a)) X ≫
      Functor.map (shiftFunctor D a) (𝟙 (F.obj X)))
    (𝟙 (F.obj (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)) ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X)

Tactic:
rw [Functor.commShiftIso_comp_hom_app, liftCommShift_commShiftIso,
      LiftCommShift.iso_hom_app, ← Functor.map_comp_assoc, Iso.hom_inv_id_app]

Premises used: CategoryTheory.Functor.commShiftIso_comp_hom_app, CategoryTheory.Quotient.LiftCommShift.iso_hom_app, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Quotient.liftCommShift_commShiftIso
-- Module: Mathlib.CategoryTheory.Shift.Quotient
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
r : HomRel.{u, v} C
A : Type w
inst_2 : AddMonoid A
inst_3 : HasShift.{v, u, w} C A
inst_4 : HasShift.{v', u', w} D A
inst_5 : r.IsCompatibleWithShift A
inst_6 : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a : A
X : C
⊢ Eq (α :=
    (lift r F hF).obj ((functor r).obj (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)) ⟶
      Functor.obj.{v', v', u', u'} (shiftFunctor D a) (F.obj X))
    (((lift r F hF).map (𝟙 ((shiftFunctor C a ⋙ functor r).obj X)) ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X) ≫
      Functor.map (shiftFunctor D a) (𝟙 (F.obj X)))
    (𝟙 (F.obj (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)) ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X)

Tactic:
simp [lift, Quotient.functor]

Premises used: CategoryTheory.Quotient.functor, CategoryTheory.Quotient.lift
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
sequence : M → Functor.{v_1, v_2, u_1, u_2} C A
isoZero : sequence 0 ≅ F
shiftIso : (n a a' : M) → (ha' : n + a = a') → shiftFunctor C n ⋙ sequence a ≅ sequence a'
shiftIso_zero :
  ∀ (a : M), shiftIso 0 a a ⋯ = isoWhiskerRight (shiftFunctorZero C M) (sequence a) ≪≫ (sequence a).leftUnitor
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
rw : m + (n + a) = a''
rw₁ : m + a' = a''
rw₂ rw₃ : a'' = a''
⊢ m + n + a = a''

Tactic:
rw [add_assoc, ha', ha'']

Premises used: add_assoc
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
a : M
rw :
  Eq (α := shiftFunctor.{v_1, u_1, u_3} C (A := M) 0 ⋙ shiftFunctor C a ⋙ F ≅ shiftFunctor C a ⋙ F)
    (Iso.symm (associator (shiftFunctor.{v_1, u_1, u_3} C (A := M) 0) (shiftFunctor C a) F) ≪≫
      isoWhiskerRight
        (Iso.symm
          (Iso.symm (leftUnitor (shiftFunctor C a)) ≪≫
            isoWhiskerRight (Iso.symm (shiftFunctorZero C M)) (shiftFunctor C a)))
        F)
    (isoWhiskerRight (shiftFunctorZero C M) (shiftFunctor C a ⋙ F) ≪≫ (shiftFunctor C a ⋙ F).leftUnitor)
⊢ Iso.symm (associator (shiftFunctor.{v_1, u_1, u_3} C (A := M) 0) (shiftFunctor C a) F) ≪≫
      isoWhiskerRight (Iso.symm (shiftFunctorAdd' C 0 a a ⋯)) F =
    isoWhiskerRight (shiftFunctorZero C M) (shiftFunctor C a ⋙ F) ≪≫ (shiftFunctor C a ⋙ F).leftUnitor

Tactic:
rw [shiftFunctorAdd'_zero_add]

Premises used: CategoryTheory.shiftFunctorAdd'_zero_add
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
w :
  ∀ (X : C),
    NatTrans.app
        (Iso.hom
          (Iso.symm (associator (shiftFunctor C (m + n)) (shiftFunctor C a) F) ≪≫
            isoWhiskerRight (Iso.symm (shiftFunctorAdd' C (m + n) a a'' ⋯)) F))
        X =
      (isoWhiskerRight (shiftFunctorAdd C m n) (shiftFunctor C a ⋙ F) ≪≫
              associator (shiftFunctor C m) (shiftFunctor C n) (shiftFunctor C a ⋙ F) ≪≫
                isoWhiskerLeft (shiftFunctor C m)
                    (Iso.symm (associator (shiftFunctor C n) (shiftFunctor C a) F) ≪≫
                      isoWhiskerRight (Iso.symm (shiftFunctorAdd' C n a a' ha')) F) ≪≫
                  Iso.symm (associator (shiftFunctor C m) (shiftFunctor C a') F) ≪≫
                    isoWhiskerRight (Iso.symm (shiftFunctorAdd' C m a' a'' ha'')) F).hom.app
        X
⊢ Iso.symm (associator (shiftFunctor C (m + n)) (shiftFunctor C a) F) ≪≫
      isoWhiskerRight (Iso.symm (shiftFunctorAdd' C (m + n) a a'' ⋯)) F =
    isoWhiskerRight (shiftFunctorAdd C m n) (shiftFunctor C a ⋙ F) ≪≫
      associator (shiftFunctor C m) (shiftFunctor C n) (shiftFunctor C a ⋙ F) ≪≫
        isoWhiskerLeft (shiftFunctor C m)
            (Iso.symm (associator (shiftFunctor C n) (shiftFunctor C a) F) ≪≫
              isoWhiskerRight (Iso.symm (shiftFunctorAdd' C n a a' ha')) F) ≪≫
          Iso.symm (associator (shiftFunctor C m) (shiftFunctor C a') F) ≪≫
            isoWhiskerRight (Iso.symm (shiftFunctorAdd' C m a' a'' ha'')) F

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
w :
  𝟙 (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m + n)) X))) ≫
      F.map (NatTrans.app (Iso.inv (shiftFunctorAdd' C (m + n) a a'' ⋯)) X) =
    F.map (map (shiftFunctor C a) (NatTrans.app (Iso.hom (shiftFunctorAdd C m n)) X)) ≫
      𝟙
          (F.obj
            (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
              (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X)))) ≫
        (𝟙
              (F.obj
                (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
                  (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X)))) ≫
            F.map
              (NatTrans.app (Iso.inv (shiftFunctorAdd' C n a a' ha'))
                (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X))) ≫
          𝟙 (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X))) ≫
            F.map (NatTrans.app (Iso.inv (shiftFunctorAdd' C m a' a'' ha'')) X)
⊢ NatTrans.app
      (Iso.hom
        (Iso.symm (associator (shiftFunctor C (m + n)) (shiftFunctor C a) F) ≪≫
          isoWhiskerRight (Iso.symm (shiftFunctorAdd' C (m + n) a a'' ⋯)) F))
      X =
    (isoWhiskerRight (shiftFunctorAdd C m n) (shiftFunctor C a ⋙ F) ≪≫
            associator (shiftFunctor C m) (shiftFunctor C n) (shiftFunctor C a ⋙ F) ≪≫
              isoWhiskerLeft (shiftFunctor C m)
                  (Iso.symm (associator (shiftFunctor C n) (shiftFunctor C a) F) ≪≫
                    isoWhiskerRight (Iso.symm (shiftFunctorAdd' C n a a' ha')) F) ≪≫
                Iso.symm (associator (shiftFunctor C m) (shiftFunctor C a') F) ≪≫
                  isoWhiskerRight (Iso.symm (shiftFunctorAdd' C m a' a'' ha'')) F).hom.app
      X

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
w :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m + n)) X)) ⟶
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a'') X))
    (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd' C (m + n) a a'' ⋯)) X))
    (F.map
      (map (shiftFunctor C a) (NatTrans.app (Iso.hom (shiftFunctorAdd C m n)) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C m a' a'' ha'')) X))
⊢ 𝟙 (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m + n)) X))) ≫
      F.map (NatTrans.app (Iso.inv (shiftFunctorAdd' C (m + n) a a'' ⋯)) X) =
    F.map (map (shiftFunctor C a) (NatTrans.app (Iso.hom (shiftFunctorAdd C m n)) X)) ≫
      𝟙
          (F.obj
            (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
              (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X)))) ≫
        (𝟙
              (F.obj
                (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
                  (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X)))) ≫
            F.map
              (NatTrans.app (Iso.inv (shiftFunctorAdd' C n a a' ha'))
                (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X))) ≫
          𝟙 (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X))) ≫
            F.map (NatTrans.app (Iso.inv (shiftFunctorAdd' C m a' a'' ha'')) X)

Tactic:
simp only [id_comp, ← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
w :
  Eq.{v_1 + 1} (α :=
    obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m + n)) X) ⟶
      obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a'') X)
    (NatTrans.app (Iso.inv (shiftFunctorAdd' C (m + n) a a'' ⋯)) X)
    (map (shiftFunctor C a) (NatTrans.app (Iso.hom (shiftFunctorAdd C m n)) X) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C m a' a'' ha'')) X)
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m + n)) X)) ⟶
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a'') X))
    (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd' C (m + n) a a'' ⋯)) X))
    (F.map
      (map (shiftFunctor C a) (NatTrans.app (Iso.hom (shiftFunctorAdd C m n)) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C m a' a'' ha'')) X))

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
rw : m + n + a = m + a'
rw₁ : m + n + a = m + (n + a)
rw₂ rw₃ : m + (n + a) = m + (n + a)
⊢ m + n + a = a''

Tactic:
rw [← ha'', ← ha', add_assoc]

Premises used: add_assoc
-- Module: Mathlib.CategoryTheory.Shift.ShiftSequence
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ Eq.{v_1 + 1} (α :=
    obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m + n)) X) ⟶
      obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a'') X)
    (NatTrans.app (Iso.inv (shiftFunctorAdd' C (m + n) a a'' ⋯)) X)
    (map (shiftFunctor C a) (NatTrans.app (Iso.hom (shiftFunctorAdd C m n)) X) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C m a' a'' ha'')) X)

Tactic:
simpa only [← cancel_epi ((shiftFunctor C a).map ((shiftFunctorAdd C m n).hom.app X)),
      shiftFunctorAdd'_eq_shiftFunctorAdd, ← Functor.map_comp_assoc, Iso.hom_inv_id_app,
      Functor.map_id, id_comp] using shiftFunctorAdd'_assoc_inv_app m n a (m + n) a' a'' rfl ha'
        (by rw [← ha'', ← ha', add_assoc]) X

Premises used: CategoryTheory.shiftFunctorAdd'_assoc_inv_app, CategoryTheory.shiftFunctor, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.shiftFunctorAdd, CategoryTheory.Functor.map, CategoryTheory.Functor.map_comp_assoc, HAdd.hAdd, CategoryTheory.Functor.map_id, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app, rfl, CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd, CategoryTheory.Category.id_comp