awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
A : Type w
inst_4 : AddMonoid A
inst_5 : HasShift.{v₁, u₁, w} C A
F : Functor.{v₁, v₃, u₁, u₃} C E
F' : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : Lifting L W F F'
inst_7 : HasShift.{v₂, u₂, w} D A
inst_8 : HasShift.{v₃, u₃, w} E A
inst_9 : L.CommShift A
inst_10 : F.CommShift A
X : C
w :
  Eq (α :=
    F'.obj (obj.{v₂, v₂, u₂, u₂} (shiftFunctor.{v₂, u₂, w} D (A := A) 0) (L.obj X)) ⟶
      obj.{v₃, v₃, u₃, u₃} (shiftFunctor.{v₃, u₃, w} E (A := A) 0) (F'.obj (L.obj X)))
    (F'.map (NatTrans.app (Iso.hom (shiftFunctorZero D A)) (L.obj X)) ≫
      CategoryStruct.comp (Y := F'.obj (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor.{v₁, u₁, w} C (A := A) 0) X)))
        (F'.map (L.map (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X)))
        ((L ⋙ F').map (NatTrans.app (Iso.hom (shiftFunctorZero C A)) X) ≫
          (Lifting.iso L W F F').hom.app X ≫
            map (𝟭 E) ((Lifting.iso L W F F').inv.app X) ≫
              NatTrans.app (Iso.inv (shiftFunctorZero E A)) (F'.obj (L.obj X))))
    (F'.map (NatTrans.app (Iso.hom (shiftFunctorZero D A)) (L.obj X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorZero E A)) (F'.obj (L.obj X)))
⊢ Eq (α :=
    F'.obj (obj.{v₂, v₂, u₂, u₂} (shiftFunctor.{v₂, u₂, w} D (A := A) 0) (L.obj X)) ⟶
      obj.{v₃, v₃, u₃, u₃} (shiftFunctor.{v₃, u₃, w} E (A := A) 0) (F'.obj (L.obj X)))
    (NatTrans.app (Iso.hom (commShiftOfLocalization.iso L W F F' 0)) (L.obj X))
    (NatTrans.app (Iso.hom (CommShift.isoZero F' A)) (L.obj X))

Tactic:
simp only [commShiftOfLocalization.iso_hom_app, comp_obj, commShiftIso_zero,
      CommShift.isoZero_inv_app, map_comp, CommShift.isoZero_hom_app, Category.assoc,
      ← NatTrans.naturality_assoc, ← NatTrans.naturality]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Functor.CommShift.isoZero_hom_app, CategoryTheory.Functor.commShiftOfLocalization.iso_hom_app, CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.CommShift.isoZero_inv_app, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.naturality_assoc, CategoryTheory.Functor.CommShift.commShiftIso_zero
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
A : Type w
inst_4 : AddMonoid A
inst_5 : HasShift.{v₁, u₁, w} C A
F : Functor.{v₁, v₃, u₁, u₃} C E
F' : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : Lifting L W F F'
inst_7 : HasShift.{v₂, u₂, w} D A
inst_8 : HasShift.{v₃, u₃, w} E A
inst_9 : L.CommShift A
inst_10 : F.CommShift A
X : C
w :
  Eq (α :=
    F'.obj (obj.{v₂, v₂, u₂, u₂} (shiftFunctor.{v₂, u₂, w} D (A := A) 0) (L.obj X)) ⟶
      obj.{v₃, v₃, u₃, u₃} (shiftFunctor.{v₃, u₃, w} E (A := A) 0) (F'.obj (L.obj X)))
    (F'.map (NatTrans.app (Iso.hom (shiftFunctorZero D A)) (L.obj X)) ≫
      CategoryStruct.comp (Y := F'.obj (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor.{v₁, u₁, w} C (A := A) 0) X)))
        (F'.map (L.map (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X)))
        (F'.map (L.map (NatTrans.app (Iso.hom (shiftFunctorZero C A)) X)) ≫
          (Lifting.iso L W F F').hom.app X ≫
            (Lifting.iso L W F F').inv.app X ≫ NatTrans.app (Iso.inv (shiftFunctorZero E A)) (F'.obj (L.obj X))))
    (F'.map (NatTrans.app (Iso.hom (shiftFunctorZero D A)) (L.obj X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorZero E A)) (F'.obj (L.obj X)))
⊢ Eq (α :=
    F'.obj (obj.{v₂, v₂, u₂, u₂} (shiftFunctor.{v₂, u₂, w} D (A := A) 0) (L.obj X)) ⟶
      obj.{v₃, v₃, u₃, u₃} (shiftFunctor.{v₃, u₃, w} E (A := A) 0) (F'.obj (L.obj X)))
    (F'.map (NatTrans.app (Iso.hom (shiftFunctorZero D A)) (L.obj X)) ≫
      CategoryStruct.comp (Y := F'.obj (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor.{v₁, u₁, w} C (A := A) 0) X)))
        (F'.map (L.map (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X)))
        ((L ⋙ F').map (NatTrans.app (Iso.hom (shiftFunctorZero C A)) X) ≫
          (Lifting.iso L W F F').hom.app X ≫
            map (𝟭 E) ((Lifting.iso L W F F').inv.app X) ≫
              NatTrans.app (Iso.inv (shiftFunctorZero E A)) (F'.obj (L.obj X))))
    (F'.map (NatTrans.app (Iso.hom (shiftFunctorZero D A)) (L.obj X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorZero E A)) (F'.obj (L.obj X)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
A : Type w
inst_4 : AddMonoid A
inst_5 : HasShift.{v₁, u₁, w} C A
F : Functor.{v₁, v₃, u₁, u₃} C E
F' : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : Lifting L W F F'
inst_7 : HasShift.{v₂, u₂, w} D A
inst_8 : HasShift.{v₃, u₃, w} E A
inst_9 : L.CommShift A
inst_10 : F.CommShift A
X : C
⊢ Eq (α :=
    F'.obj (obj.{v₂, v₂, u₂, u₂} (shiftFunctor.{v₂, u₂, w} D (A := A) 0) (L.obj X)) ⟶
      obj.{v₃, v₃, u₃, u₃} (shiftFunctor.{v₃, u₃, w} E (A := A) 0) (F'.obj (L.obj X)))
    (F'.map (NatTrans.app (Iso.hom (shiftFunctorZero D A)) (L.obj X)) ≫
      CategoryStruct.comp (Y := F'.obj (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor.{v₁, u₁, w} C (A := A) 0) X)))
        (F'.map (L.map (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X)))
        (F'.map (L.map (NatTrans.app (Iso.hom (shiftFunctorZero C A)) X)) ≫
          (Lifting.iso L W F F').hom.app X ≫
            (Lifting.iso L W F F').inv.app X ≫ NatTrans.app (Iso.inv (shiftFunctorZero E A)) (F'.obj (L.obj X))))
    (F'.map (NatTrans.app (Iso.hom (shiftFunctorZero D A)) (L.obj X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorZero E A)) (F'.obj (L.obj X)))

Tactic:
simp only [← Functor.map_comp_assoc, ← Functor.map_comp,
      Iso.inv_hom_id_app, id_obj, map_id, Category.id_comp, Iso.hom_inv_id_app_assoc]

Premises used: CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Iso.hom_inv_id_app_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
A : Type w
inst_4 : AddMonoid A
inst_5 : HasShift.{v₁, u₁, w} C A
F : Functor.{v₁, v₃, u₁, u₃} C E
F' : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : Lifting L W F F'
inst_7 : HasShift.{v₂, u₂, w} D A
inst_8 : HasShift.{v₃, u₃, w} E A
inst_9 : L.CommShift A
inst_10 : F.CommShift A
a b : A
w :
  Eq (α := shiftFunctor D (a + b) ⋙ F' ⟶ F' ⋙ shiftFunctor E (a + b))
    (Iso.hom (commShiftOfLocalization.iso L W F F' (a + b)))
    (Iso.hom (CommShift.isoAdd (commShiftOfLocalization.iso L W F F' a) (commShiftOfLocalization.iso L W F F' b)))
⊢ Eq (α := shiftFunctor D (a + b) ⋙ F' ≅ F' ⋙ shiftFunctor E (a + b)) (commShiftOfLocalization.iso L W F F' (a + b))
    (CommShift.isoAdd (commShiftOfLocalization.iso L W F F' a) (commShiftOfLocalization.iso L W F F' b))

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
A : Type w
inst_4 : AddMonoid A
inst_5 : HasShift.{v₁, u₁, w} C A
F : Functor.{v₁, v₃, u₁, u₃} C E
F' : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : Lifting L W F F'
inst_7 : HasShift.{v₂, u₂, w} D A
inst_8 : HasShift.{v₃, u₃, w} E A
inst_9 : L.CommShift A
inst_10 : F.CommShift A
a b : A
w :
  ∀ (X : C),
    Eq (α := (shiftFunctor D (a + b) ⋙ F').obj (L.obj X) ⟶ (F' ⋙ shiftFunctor E (a + b)).obj (L.obj X))
      (NatTrans.app (Iso.hom (commShiftOfLocalization.iso L W F F' (a + b))) (L.obj X))
      (NatTrans.app
        (Iso.hom (CommShift.isoAdd (commShiftOfLocalization.iso L W F F' a) (commShiftOfLocalization.iso L W F F' b)))
        (L.obj X))
⊢ Eq (α := shiftFunctor D (a + b) ⋙ F' ⟶ F' ⋙ shiftFunctor E (a + b))
    (Iso.hom (commShiftOfLocalization.iso L W F F' (a + b)))
    (Iso.hom (CommShift.isoAdd (commShiftOfLocalization.iso L W F F' a) (commShiftOfLocalization.iso L W F F' b)))

Tactic:
apply natTrans_ext L W

Premises used: CategoryTheory.Localization.natTrans_ext
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
A : Type w
inst_4 : AddMonoid A
inst_5 : HasShift.{v₁, u₁, w} C A
F : Functor.{v₁, v₃, u₁, u₃} C E
F' : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : Lifting L W F F'
inst_7 : HasShift.{v₂, u₂, w} D A
inst_8 : HasShift.{v₃, u₃, w} E A
inst_9 : L.CommShift A
inst_10 : F.CommShift A
a b : A
X : C
w :
  Eq (α :=
    F'.obj (obj.{v₂, v₂, u₂, u₂} (shiftFunctor D (a + b)) (L.obj X)) ⟶
      obj.{v₃, v₃, u₃, u₃} (shiftFunctor E (a + b)) (F'.obj (L.obj X)))
    (NatTrans.app (Iso.hom (commShiftOfLocalization.iso L W F F' (a + b))) (L.obj X))
    (NatTrans.app
      (Iso.hom (CommShift.isoAdd (commShiftOfLocalization.iso L W F F' a) (commShiftOfLocalization.iso L W F F' b)))
      (L.obj X))
⊢ Eq (α := (shiftFunctor D (a + b) ⋙ F').obj (L.obj X) ⟶ (F' ⋙ shiftFunctor E (a + b)).obj (L.obj X))
    (NatTrans.app (Iso.hom (commShiftOfLocalization.iso L W F F' (a + b))) (L.obj X))
    (NatTrans.app
      (Iso.hom (CommShift.isoAdd (commShiftOfLocalization.iso L W F F' a) (commShiftOfLocalization.iso L W F F' b)))
      (L.obj X))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
A : Type w
inst_4 : AddMonoid A
inst_5 : HasShift.{v₁, u₁, w} C A
F : Functor.{v₁, v₃, u₁, u₃} C E
F' : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : Lifting L W F F'
inst_7 : HasShift.{v₂, u₂, w} D A
inst_8 : HasShift.{v₃, u₃, w} E A
inst_9 : L.CommShift A
inst_10 : F.CommShift A
a b : A
X : C
erw :
  F'.map (NatTrans.app (Iso.inv (commShiftIso L b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
    F'.map (L.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X)) ≫
      (L ⋙ F').map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
        (Lifting.iso L W F F').hom.app
            (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C b) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
          NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) ≫
            map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
              NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (F.obj X) ≫
                map (shiftFunctor E (a + b)) ((Lifting.iso L W F F').inv.app X)
| F'.map (NatTrans.app (Iso.inv (commShiftIso L b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
    F'.map (L.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X)) ≫
      (Lifting.iso L W F F').hom.app (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C (a + b)) X) ≫
        F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
          NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) ≫
            map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
              NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (F.obj X) ≫
                map (shiftFunctor E (a + b)) ((Lifting.iso L W F F').inv.app X)

Tactic:
erw [← NatTrans.naturality_assoc]

Premises used: CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
A : Type w
inst_4 : AddMonoid A
inst_5 : HasShift.{v₁, u₁, w} C A
F : Functor.{v₁, v₃, u₁, u₃} C E
F' : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : Lifting L W F F'
inst_7 : HasShift.{v₂, u₂, w} D A
inst_8 : HasShift.{v₃, u₃, w} E A
inst_9 : L.CommShift A
inst_10 : F.CommShift A
a b : A
X : C
dsimp :
  F'.map (NatTrans.app (Iso.inv (commShiftIso L b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
    F'.map (L.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X)) ≫
      F'.map (L.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X)) ≫
        (Lifting.iso L W F F').hom.app
            (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C b) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
          NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) ≫
            map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
              NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (F.obj X) ≫
                map (shiftFunctor E (a + b)) ((Lifting.iso L W F F').inv.app X)
| F'.map (NatTrans.app (Iso.inv (commShiftIso L b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
    F'.map (L.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X)) ≫
      (L ⋙ F').map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
        (Lifting.iso L W F F').hom.app
            (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C b) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
          NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) ≫
            map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
              NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (F.obj X) ≫
                map (shiftFunctor E (a + b)) ((Lifting.iso L W F F').inv.app X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
A : Type w
inst_4 : AddMonoid A
inst_5 : HasShift.{v₁, u₁, w} C A
F : Functor.{v₁, v₃, u₁, u₃} C E
F' : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : Lifting L W F F'
inst_7 : HasShift.{v₂, u₂, w} D A
inst_8 : HasShift.{v₃, u₃, w} E A
inst_9 : L.CommShift A
inst_10 : F.CommShift A
a b : A
X : C
rw :
  F'.map
      (NatTrans.app (Iso.inv (commShiftIso L b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) ≫
        L.map (𝟙 (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a ⋙ shiftFunctor C b) X))) ≫
    (Lifting.iso L W F F').hom.app
        (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C b) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
      NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) ≫
        map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (F.obj X) ≫
            map (shiftFunctor E (a + b)) ((Lifting.iso L W F F').inv.app X)
| F'.map (NatTrans.app (Iso.inv (commShiftIso L b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
    F'.map (L.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X)) ≫
      F'.map (L.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X)) ≫
        (Lifting.iso L W F F').hom.app
            (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C b) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
          NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) ≫
            map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
              NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (F.obj X) ≫
                map (shiftFunctor E (a + b)) ((Lifting.iso L W F F').inv.app X)

Tactic:
rw [← Functor.map_comp_assoc, ← map_comp_assoc, Category.assoc,
        ← map_comp, Iso.inv_hom_id_app]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
A : Type w
inst_4 : AddMonoid A
inst_5 : HasShift.{v₁, u₁, w} C A
F : Functor.{v₁, v₃, u₁, u₃} C E
F' : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : Lifting L W F F'
inst_7 : HasShift.{v₂, u₂, w} D A
inst_8 : HasShift.{v₃, u₃, w} E A
inst_9 : L.CommShift A
inst_10 : F.CommShift A
a b : A
X : C
dsimp :
  F'.map
      (NatTrans.app (Iso.inv (commShiftIso L b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) ≫
        L.map (𝟙 (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C b) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)))) ≫
    (Lifting.iso L W F F').hom.app
        (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C b) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
      NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) ≫
        map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (F.obj X) ≫
            map (shiftFunctor E (a + b)) ((Lifting.iso L W F F').inv.app X)
| F'.map
      (NatTrans.app (Iso.inv (commShiftIso L b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) ≫
        L.map (𝟙 (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a ⋙ shiftFunctor C b) X))) ≫
    (Lifting.iso L W F F').hom.app
        (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C b) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
      NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) ≫
        map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (F.obj X) ≫
            map (shiftFunctor E (a + b)) ((Lifting.iso L W F F').inv.app X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
A : Type w
inst_4 : AddMonoid A
inst_5 : HasShift.{v₁, u₁, w} C A
F : Functor.{v₁, v₃, u₁, u₃} C E
F' : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : Lifting L W F F'
inst_7 : HasShift.{v₂, u₂, w} D A
inst_8 : HasShift.{v₃, u₃, w} E A
inst_9 : L.CommShift A
inst_10 : F.CommShift A
a b : A
X : C
rw :
  CategoryStruct.comp (Y :=
    F'.obj (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C b) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X))))
    (F'.map (NatTrans.app (Iso.inv (commShiftIso L b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)))
    ((Lifting.iso L W F F').hom.app
        (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C b) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
      NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) ≫
        map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
          map (shiftFunctor E a ⋙ shiftFunctor E b) ((Lifting.iso L W F F').inv.app X) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (F'.obj (L.obj X)))
| F'.map
      (NatTrans.app (Iso.inv (commShiftIso L b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) ≫
        L.map (𝟙 (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C b) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)))) ≫
    (Lifting.iso L W F F').hom.app
        (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C b) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
      NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) ≫
        map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (F.obj X) ≫
            map (shiftFunctor E (a + b)) ((Lifting.iso L W F F').inv.app X)

Tactic:
rw [map_id, Category.comp_id, ← NatTrans.naturality]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Shift.Localization
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
A : Type w
inst_4 : AddMonoid A
inst_5 : HasShift.{v₁, u₁, w} C A
F : Functor.{v₁, v₃, u₁, u₃} C E
F' : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : Lifting L W F F'
inst_7 : HasShift.{v₂, u₂, w} D A
inst_8 : HasShift.{v₃, u₃, w} E A
inst_9 : L.CommShift A
inst_10 : F.CommShift A
a b : A
X : C
dsimp :
  CategoryStruct.comp (Y :=
    F'.obj (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C b) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X))))
    (F'.map (NatTrans.app (Iso.inv (commShiftIso L b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)))
    ((Lifting.iso L W F F').hom.app
        (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C b) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
      CategoryStruct.comp (Y :=
        obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (F.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)))
        (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X))
        (CategoryStruct.comp (Y :=
          obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (obj.{v₃, v₃, u₃, u₃} (shiftFunctor E a) (F.obj X)))
          (map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso F a)) X))
          (map (shiftFunctor E b) (map (shiftFunctor E a) ((Lifting.iso L W F F').inv.app X)) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (F'.obj (L.obj X)))))
| CategoryStruct.comp (Y :=
    F'.obj (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C b) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X))))
    (F'.map (NatTrans.app (Iso.inv (commShiftIso L b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)))
    ((Lifting.iso L W F F').hom.app
        (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C b) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
      NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) ≫
        map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
          map (shiftFunctor E a ⋙ shiftFunctor E b) ((Lifting.iso L W F F').inv.app X) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (F'.obj (L.obj X)))

Tactic:
dsimp