awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
W : MorphismProperty.{v₁, u₁} C
M : Type w'
inst_2 : AddMonoid M
inst_3 : HasShift.{v₁, u₁, w'} C M
inst_4 : HasShift.{v₂, u₂, w'} D M
inst_5 : W.IsCompatibleWithShift M
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : L.IsLocalization W
inst_7 : L.CommShift M
X Y : C
inst_8 : HasSmallLocalizedHom W X Y
f : SmallHom W X Y
a : M
inst_9 :
  HasSmallLocalizedHom W (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)
    (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) Y)
⊢ Eq.{v₂ + 1} (α :=
    L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) ⟶
      L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) Y))
    ((equiv W L :
          (a_1 : SmallHom W ((shiftFunctor C a).obj X) ((shiftFunctor C a).obj Y)) →
            L.obj ((shiftFunctor C a).obj X) ⟶ L.obj ((shiftFunctor C a).obj Y))
        (f.shift (W := W) a) :
      L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) ⟶
        L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) Y))
    (CategoryStruct.comp (Y := (L ⋙ shiftFunctor D a).obj X) (NatTrans.app (Iso.hom (Functor.commShiftIso L a)) X)
        (Functor.map (shiftFunctor D a) ((equiv W L : (a : SmallHom W X Y) → L.obj X ⟶ L.obj Y) f) ≫
          NatTrans.app (Iso.inv (Functor.commShiftIso L a)) Y) :
      (shiftFunctor C a ⋙ L).obj X ⟶ (shiftFunctor C a ⋙ L).obj Y)

Tactic:
(W.shiftLocalizerMorphism a).equiv_smallHomMap _ _ _ (L.commShiftIso a) f

Premises used: CategoryTheory.Localization.SmallHom.shift, CategoryTheory.LocalizerMorphism.equiv_smallHomMap, CategoryTheory.MorphismProperty.shiftLocalizerMorphism, CategoryTheory.Functor.CommShift.commShiftIso
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
W : MorphismProperty.{v₁, u₁} C
M : Type w'
inst_2 : AddMonoid M
inst_3 : HasShift.{v₁, u₁, w'} C M
inst_4 : HasShift.{v₂, u₂, w'} D M
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_5 : L.IsLocalization W
inst_6 : L.CommShift M
X Y : C
inst_7 : HasSmallLocalizedShiftedHom W M X Y
m : M
f : SmallShiftedHom W X Y m
⊢ Eq.{v₂ + 1} (α := ShiftedHom (L.obj X) (L.obj Y) m)
    ((equiv W L : (a : SmallShiftedHom W X Y m) → ShiftedHom (L.obj X) (L.obj Y) m) f :
      ShiftedHom (L.obj X) (L.obj Y) m)
    (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C m) Y))
        ((SmallHom.equiv W L :
            (a : SmallHom W X ((shiftFunctor C m).obj Y)) → L.obj X ⟶ L.obj ((shiftFunctor C m).obj Y))
          f)
        (Iso.hom (Iso.app (Functor.commShiftIso L m) Y)) :
      L.obj X ⟶ (L ⋙ shiftFunctor D m).obj Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
W : MorphismProperty.{v₁, u₁} C
M : Type w'
inst_2 : AddMonoid M
inst_3 : HasShift.{v₁, u₁, w'} C M
inst_4 : HasShift.{v₂, u₂, w'} D M
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_5 : L.IsLocalization W
inst_6 : L.CommShift M
X Y : C
inst_7 : W.IsCompatibleWithShift M
a : M
inst_8 : HasSmallLocalizedShiftedHom W M X Y
inst_9 : HasSmallLocalizedShiftedHom W M Y Y
f : SmallShiftedHom W X Y a
n a' : M
h : a + n = a'
⊢ Eq.{v₂ + 1} (α :=
    L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C n) X) ⟶
      L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a') Y))
    ((SmallHom.equiv W L :
          (a : SmallHom W ((shiftFunctor C n).obj X) ((shiftFunctor C a').obj Y)) →
            L.obj ((shiftFunctor C n).obj X) ⟶ L.obj ((shiftFunctor C a').obj Y))
        (f.shift (W := W) n a' h) :
      L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C n) X) ⟶
        L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a') Y))
    (CategoryStruct.comp (Y := (L ⋙ shiftFunctor D n).obj X) (NatTrans.app (Iso.hom (Functor.commShiftIso L n)) X)
        (CategoryStruct.comp (Y :=
          Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D n) (L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) Y)))
          (Functor.map (shiftFunctor D n)
            ((SmallHom.equiv W L :
                (a_1 : SmallHom W X ((shiftFunctor C a).obj Y)) → L.obj X ⟶ L.obj ((shiftFunctor C a).obj Y))
              f))
          (Functor.map (shiftFunctor D n) (NatTrans.app (Iso.hom (Functor.commShiftIso L a)) Y) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd' D a n a' h)) (L.obj Y) ≫
              NatTrans.app (Iso.inv (Functor.commShiftIso L a')) Y)) :
      (shiftFunctor C n ⋙ L).obj X ⟶ (shiftFunctor C a' ⋙ L).obj Y)

Tactic:
simp only [shift, SmallHom.equiv_comp, SmallHom.equiv_shift, SmallHom.equiv_mk, assoc,
    L.commShiftIso_add' h, Functor.CommShift.isoAdd'_inv_app, Iso.inv_hom_id_app_assoc,
    ← Functor.map_comp_assoc, Iso.hom_inv_id_app, Functor.comp_obj, comp_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Functor.commShiftIso_add', CategoryTheory.Localization.SmallShiftedHom.shift, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Localization.SmallHom.equiv_mk, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Localization.SmallHom.equiv_comp, CategoryTheory.Localization.SmallHom.equiv_shift, CategoryTheory.Iso.inv_hom_id_app_assoc, CategoryTheory.Functor.CommShift.isoAdd'_inv_app
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
W : MorphismProperty.{v₁, u₁} C
M : Type w'
inst_2 : AddMonoid M
inst_3 : HasShift.{v₁, u₁, w'} C M
inst_4 : HasShift.{v₂, u₂, w'} D M
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_5 : L.IsLocalization W
inst_6 : L.CommShift M
X Y : C
inst_7 : W.IsCompatibleWithShift M
a : M
inst_8 : HasSmallLocalizedShiftedHom W M X Y
inst_9 : HasSmallLocalizedShiftedHom W M Y Y
f : SmallShiftedHom W X Y a
n a' : M
h : a + n = a'
dsimp :
  Eq.{v₂ + 1} (α := ShiftedHom (L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C n) X)) (L.obj Y) a')
    (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a') Y))
        ((SmallHom.equiv W L :
            (a : SmallShiftedHom W ((shiftFunctor C n).obj X) Y a') →
              L.obj ((shiftFunctor C n).obj X) ⟶ L.obj ((shiftFunctor C a').obj Y))
          (f.shift (W := W) n a' h))
        (NatTrans.app (Iso.hom (Functor.commShiftIso L a')) Y) :
      L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C n) X) ⟶
        Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a') (L.obj Y))
    (CategoryStruct.comp (Y := Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D n) (L.obj X))
        (NatTrans.app (Iso.hom (Functor.commShiftIso L n)) X)
        (Functor.map (shiftFunctor D n)
            (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) Y))
              ((SmallHom.equiv W L : (a_1 : SmallShiftedHom W X Y a) → L.obj X ⟶ L.obj ((shiftFunctor C a).obj Y)) f)
              (NatTrans.app (Iso.hom (Functor.commShiftIso L a)) Y)) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' D a n a' h)) (L.obj Y)) :
      L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C n) X) ⟶
        Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a') (L.obj Y))
⊢ Eq.{v₂ + 1} (α := ShiftedHom (L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C n) X)) (L.obj Y) a')
    ((equiv W L :
          (a : SmallShiftedHom W ((shiftFunctor C n).obj X) Y a') →
            ShiftedHom (L.obj ((shiftFunctor C n).obj X)) (L.obj Y) a')
        (f.shift (W := W) n a' h) :
      ShiftedHom (L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C n) X)) (L.obj Y) a')
    (CategoryStruct.comp (Y := (L ⋙ shiftFunctor D n).obj X) (NatTrans.app (Iso.hom (Functor.commShiftIso L n)) X)
        (Functor.map (shiftFunctor D n)
            ((equiv W L : (a_1 : SmallShiftedHom W X Y a) → ShiftedHom (L.obj X) (L.obj Y) a) f) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' D a n a' h)) (L.obj Y)) :
      (shiftFunctor C n ⋙ L).obj X ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a') (L.obj Y))

Tactic:
dsimp [equiv]

Premises used: CategoryTheory.Localization.SmallShiftedHom.equiv
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
W : MorphismProperty.{v₁, u₁} C
M : Type w'
inst_2 : AddMonoid M
inst_3 : HasShift.{v₁, u₁, w'} C M
inst_4 : HasShift.{v₂, u₂, w'} D M
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_5 : L.IsLocalization W
inst_6 : L.CommShift M
X Y : C
inst_7 : W.IsCompatibleWithShift M
a : M
inst_8 : HasSmallLocalizedShiftedHom W M X Y
inst_9 : HasSmallLocalizedShiftedHom W M Y Y
f : SmallShiftedHom W X Y a
n a' : M
h : a + n = a'
⊢ Eq (α := ShiftedHom (L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C n) X)) (L.obj Y) a')
    (CategoryStruct.comp (Y := Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D n) (L.obj X))
      (NatTrans.app (Iso.hom (Functor.commShiftIso L n)) X)
      (CategoryStruct.comp (Y :=
        Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D n) (L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) Y)))
        (Functor.map (shiftFunctor D n)
          ((SmallHom.equiv W L :
              (a_1 : SmallHom W X ((shiftFunctor C a).obj Y)) → L.obj X ⟶ L.obj ((shiftFunctor C a).obj Y))
            f))
        (Functor.map (shiftFunctor D n) (NatTrans.app (Iso.hom (Functor.commShiftIso L a)) Y) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' D a n a' h)) (L.obj Y))))
    (CategoryStruct.comp (Y := Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D n) (L.obj X))
      (NatTrans.app (Iso.hom (Functor.commShiftIso L n)) X)
      (CategoryStruct.comp (Y :=
        Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D n) (L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) Y)))
        (Functor.map (shiftFunctor D n)
          ((SmallHom.equiv W L : (a_1 : SmallShiftedHom W X Y a) → L.obj X ⟶ L.obj ((shiftFunctor C a).obj Y)) f))
        (Functor.map (shiftFunctor D n) (NatTrans.app (Iso.hom (Functor.commShiftIso L a)) Y) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' D a n a' h)) (L.obj Y))))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
W : MorphismProperty.{v₁, u₁} C
M : Type w'
inst_2 : AddMonoid M
inst_3 : HasShift.{v₁, u₁, w'} C M
inst_4 : HasShift.{v₂, u₂, w'} D M
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_5 : L.IsLocalization W
inst_6 : L.CommShift M
X Y Z : C
inst_7 : W.IsCompatibleWithShift M
inst_8 : HasSmallLocalizedShiftedHom W M X Y
inst_9 : HasSmallLocalizedShiftedHom W M Y Z
inst_10 : HasSmallLocalizedShiftedHom W M X Z
inst_11 : HasSmallLocalizedShiftedHom W M Z Z
a b c : M
f : SmallShiftedHom W X Y a
g : SmallShiftedHom W Y Z b
h : b + a = c
dsimp :
  Eq.{v₂ + 1} (α := ShiftedHom (L.obj X) (L.obj Z) c)
    (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C c) Z))
        ((SmallHom.equiv W L : (a : SmallShiftedHom W X Z c) → L.obj X ⟶ L.obj ((shiftFunctor C c).obj Z))
          (SmallHom.comp (W := W) f (g.shift (W := W) a c h)))
        (NatTrans.app (Iso.hom (Functor.commShiftIso L c)) Z) :
      L.obj X ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D c) (L.obj Z))
    (CategoryStruct.comp (Y := Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj Y))
        (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) Y))
            ((SmallHom.equiv W L : (a_1 : SmallShiftedHom W X Y a) → L.obj X ⟶ L.obj ((shiftFunctor C a).obj Y)) f)
            (NatTrans.app (Iso.hom (Functor.commShiftIso L a)) Y) :
          L.obj X ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj Y))
        (Functor.map (shiftFunctor D a)
              (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C b) Z))
                ((SmallHom.equiv W L : (a : SmallShiftedHom W Y Z b) → L.obj Y ⟶ L.obj ((shiftFunctor C b).obj Z)) g)
                (NatTrans.app (Iso.hom (Functor.commShiftIso L b)) Z)) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd' D b a c h)) (L.obj Z) :
          Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj Y) ⟶
            Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D c) (L.obj Z)) :
      L.obj X ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D c) (L.obj Z))
⊢ Eq.{v₂ + 1} (α := ShiftedHom (L.obj X) (L.obj Z) c)
    ((equiv W L : (a : SmallShiftedHom W X Z c) → ShiftedHom (L.obj X) (L.obj Z) c) (f.comp (W := W) g h) :
      ShiftedHom (L.obj X) (L.obj Z) c)
    (ShiftedHom.comp (Y := L.obj Y) ((equiv W L : (a_1 : SmallShiftedHom W X Y a) → ShiftedHom (L.obj X) (L.obj Y) a) f)
        ((equiv W L : (a : SmallShiftedHom W Y Z b) → ShiftedHom (L.obj Y) (L.obj Z) b) g) h :
      ShiftedHom (L.obj X) (L.obj Z) c)

Tactic:
dsimp [comp, equiv, ShiftedHom.comp]

Premises used: CategoryTheory.ShiftedHom.comp, CategoryTheory.Localization.SmallShiftedHom.comp, CategoryTheory.Localization.SmallShiftedHom.equiv
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
W : MorphismProperty.{v₁, u₁} C
M : Type w'
inst_2 : AddMonoid M
inst_3 : HasShift.{v₁, u₁, w'} C M
inst_4 : HasShift.{v₂, u₂, w'} D M
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_5 : L.IsLocalization W
inst_6 : L.CommShift M
X Y Z : C
inst_7 : W.IsCompatibleWithShift M
inst_8 : HasSmallLocalizedShiftedHom W M X Y
inst_9 : HasSmallLocalizedShiftedHom W M Y Z
inst_10 : HasSmallLocalizedShiftedHom W M X Z
inst_11 : HasSmallLocalizedShiftedHom W M Z Z
a b c : M
f : SmallShiftedHom W X Y a
g : SmallShiftedHom W Y Z b
h : b + a = c
⊢ Eq.{v₂ + 1} (α := ShiftedHom (L.obj X) (L.obj Z) c)
    (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) Y))
        ((SmallHom.equiv W L :
            (a_1 : SmallHom W X ((shiftFunctor C a).obj Y)) → L.obj X ⟶ L.obj ((shiftFunctor C a).obj Y))
          f)
        (CategoryStruct.comp (Y := Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj Y))
          (NatTrans.app (Iso.hom (Functor.commShiftIso L a)) Y)
          (CategoryStruct.comp (Y :=
            Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C b) Z)))
            (Functor.map (shiftFunctor D a)
              ((SmallHom.equiv W L :
                  (a : SmallHom W Y ((shiftFunctor C b).obj Z)) → L.obj Y ⟶ L.obj ((shiftFunctor C b).obj Z))
                g))
            (Functor.map (shiftFunctor D a) (NatTrans.app (Iso.hom (Functor.commShiftIso L b)) Z) ≫
              NatTrans.app (Iso.inv (shiftFunctorAdd' D b a c h)) (L.obj Z)))) :
      L.obj X ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D c) (L.obj Z))
    (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) Y))
        ((SmallHom.equiv W L : (a_1 : SmallShiftedHom W X Y a) → L.obj X ⟶ L.obj ((shiftFunctor C a).obj Y)) f)
        (CategoryStruct.comp (Y := Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj Y))
          (NatTrans.app (Iso.hom (Functor.commShiftIso L a)) Y)
          (CategoryStruct.comp (Y :=
            Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C b) Z)))
            (Functor.map (shiftFunctor D a)
              ((SmallHom.equiv W L : (a : SmallShiftedHom W Y Z b) → L.obj Y ⟶ L.obj ((shiftFunctor C b).obj Z)) g))
            (Functor.map (shiftFunctor D a) (NatTrans.app (Iso.hom (Functor.commShiftIso L b)) Z) ≫
              NatTrans.app (Iso.inv (shiftFunctorAdd' D b a c h)) (L.obj Z)))) :
      L.obj X ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D c) (L.obj Z))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
W : MorphismProperty.{v₁, u₁} C
M : Type w'
inst_2 : AddMonoid M
inst_3 : HasShift.{v₁, u₁, w'} C M
inst_4 : HasShift.{v₂, u₂, w'} D M
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_5 : L.IsLocalization W
inst_6 : L.CommShift M
X Y : C
inst_7 : HasSmallLocalizedShiftedHom W M X Y
m : M
f : ShiftedHom X Y m
⊢ Eq.{v₂ + 1} (α := L.obj X ⟶ (shiftFunctor C m ⋙ L).obj Y)
    ((SmallHom.equiv W L : (a : SmallHom W X ((shiftFunctor C m).obj Y)) → L.obj X ⟶ L.obj ((shiftFunctor C m).obj Y))
        (mk W f) :
      L.obj X ⟶ L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C m) Y))
    ((Equiv.symm (Iso.homToEquiv (Iso.app (Functor.commShiftIso L m) Y)) :
          (a : L.obj X ⟶ (L ⋙ shiftFunctor D m).obj Y) → L.obj X ⟶ (shiftFunctor C m ⋙ L).obj Y)
        (f.map L) :
      L.obj X ⟶ (shiftFunctor C m ⋙ L).obj Y)

Tactic:
simp [ShiftedHom.map, mk]

Premises used: CategoryTheory.ShiftedHom.map, CategoryTheory.Localization.SmallShiftedHom.mk
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
W : MorphismProperty.{v₁, u₁} C
M : Type w'
inst_2 : AddMonoid M
inst_3 : HasShift.{v₁, u₁, w'} C M
inst_4 : HasShift.{v₂, u₂, w'} D M
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_5 : L.IsLocalization W
inst_6 : L.CommShift M
X Y : C
inst_7 : HasSmallLocalizedShiftedHom W M X Y
m₀ : M
hm₀ : m₀ = 0
f : X ⟶ Y
subst :
  Eq (α := ShiftedHom.{v₂, u₂, w'} (M := M) (L.obj X) (L.obj Y) 0)
    ((equiv W L : (a : SmallShiftedHom W X Y 0) → ShiftedHom (L.obj X) (L.obj Y) 0) (mk₀ W 0 ⋯ f) :
      ShiftedHom.{v₂, u₂, w'} (M := M) (L.obj X) (L.obj Y) 0)
    (ShiftedHom.mk₀ 0 ⋯ (L.map f) : ShiftedHom.{v₂, u₂, w'} (M := M) (L.obj X) (L.obj Y) 0)
⊢ Eq.{v₂ + 1} (α := ShiftedHom (L.obj X) (L.obj Y) m₀)
    ((equiv W L : (a : SmallShiftedHom W X Y m₀) → ShiftedHom (L.obj X) (L.obj Y) m₀) (mk₀ W m₀ hm₀ f) :
      ShiftedHom (L.obj X) (L.obj Y) m₀)
    (ShiftedHom.mk₀ m₀ hm₀ (L.map f) : ShiftedHom (L.obj X) (L.obj Y) m₀)

Tactic:
subst hm₀
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
W : MorphismProperty.{v₁, u₁} C
M : Type w'
inst_2 : AddMonoid M
inst_3 : HasShift.{v₁, u₁, w'} C M
inst_4 : HasShift.{v₂, u₂, w'} D M
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_5 : L.IsLocalization W
inst_6 : L.CommShift M
X Y : C
inst_7 : HasSmallLocalizedShiftedHom W M X Y
f : X ⟶ Y
dsimp :
  Eq.{v₂ + 1} (α := ShiftedHom.{v₂, u₂, w'} (M := M) (L.obj X) (L.obj Y) 0)
    (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor.{v₁, u₁, w'} C (A := M) 0) Y))
        ((SmallHom.equiv W L : (a : SmallShiftedHom W X Y 0) → L.obj X ⟶ L.obj ((shiftFunctor C 0).obj Y))
          (mk W (ShiftedHom.mk₀ 0 ⋯ f)))
        (NatTrans.app (Iso.hom (Functor.commShiftIso L 0)) Y) :
      L.obj X ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor.{v₂, u₂, w'} D (A := M) 0) (L.obj Y))
    (ShiftedHom.mk₀ 0 ⋯ (L.map f) : ShiftedHom.{v₂, u₂, w'} (M := M) (L.obj X) (L.obj Y) 0)
⊢ Eq (α := ShiftedHom.{v₂, u₂, w'} (M := M) (L.obj X) (L.obj Y) 0)
    ((equiv W L : (a : SmallShiftedHom W X Y 0) → ShiftedHom (L.obj X) (L.obj Y) 0) (mk₀ W 0 ⋯ f) :
      ShiftedHom.{v₂, u₂, w'} (M := M) (L.obj X) (L.obj Y) 0)
    (ShiftedHom.mk₀ 0 ⋯ (L.map f) : ShiftedHom.{v₂, u₂, w'} (M := M) (L.obj X) (L.obj Y) 0)

Tactic:
dsimp [equiv, mk₀]

Premises used: CategoryTheory.Localization.SmallShiftedHom.mk₀, CategoryTheory.Localization.SmallShiftedHom.equiv
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
W : MorphismProperty.{v₁, u₁} C
M : Type w'
inst_2 : AddMonoid M
inst_3 : HasShift.{v₁, u₁, w'} C M
inst_4 : HasShift.{v₂, u₂, w'} D M
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_5 : L.IsLocalization W
inst_6 : L.CommShift M
X Y : C
inst_7 : HasSmallLocalizedShiftedHom W M X Y
f : X ⟶ Y
erw :
  Eq (α := ShiftedHom.{v₂, u₂, w'} (M := M) (L.obj X) (L.obj Y) 0)
    (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor.{v₁, u₁, w'} C (A := M) 0) Y))
      (L.map f ≫ L.map (NatTrans.app (Iso.inv (shiftFunctorZero' C 0 ⋯)) Y))
      (NatTrans.app (Iso.hom (Functor.commShiftIso L 0)) Y))
    (ShiftedHom.mk₀ 0 ⋯ (L.map f))
⊢ Eq.{v₂ + 1} (α := ShiftedHom.{v₂, u₂, w'} (M := M) (L.obj X) (L.obj Y) 0)
    (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor.{v₁, u₁, w'} C (A := M) 0) Y))
        ((SmallHom.equiv W L : (a : SmallShiftedHom W X Y 0) → L.obj X ⟶ L.obj ((shiftFunctor C 0).obj Y))
          (mk W (ShiftedHom.mk₀ 0 ⋯ f)))
        (NatTrans.app (Iso.hom (Functor.commShiftIso L 0)) Y) :
      L.obj X ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor.{v₂, u₂, w'} D (A := M) 0) (L.obj Y))
    (ShiftedHom.mk₀ 0 ⋯ (L.map f) : ShiftedHom.{v₂, u₂, w'} (M := M) (L.obj X) (L.obj Y) 0)

Tactic:
erw [SmallHom.equiv_mk, Functor.map_comp]

Premises used: CategoryTheory.Localization.SmallHom.equiv_mk, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
W : MorphismProperty.{v₁, u₁} C
M : Type w'
inst_2 : AddMonoid M
inst_3 : HasShift.{v₁, u₁, w'} C M
inst_4 : HasShift.{v₂, u₂, w'} D M
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_5 : L.IsLocalization W
inst_6 : L.CommShift M
X Y : C
inst_7 : HasSmallLocalizedShiftedHom W M X Y
f : X ⟶ Y
dsimp :
  (L.map f ≫
        L.map
          (NatTrans.app (Iso.inv (shiftFunctorZero C M)) Y ≫
            𝟙 (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor.{v₁, u₁, w'} C (A := M) 0) Y))) ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso L 0)) Y =
    L.map f ≫
      NatTrans.app (Iso.inv (shiftFunctorZero D M)) (L.obj Y) ≫
        𝟙 (Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor.{v₂, u₂, w'} D (A := M) 0) (L.obj Y))
⊢ Eq (α := ShiftedHom.{v₂, u₂, w'} (M := M) (L.obj X) (L.obj Y) 0)
    (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor.{v₁, u₁, w'} C (A := M) 0) Y))
      (L.map f ≫ L.map (NatTrans.app (Iso.inv (shiftFunctorZero' C 0 ⋯)) Y))
      (NatTrans.app (Iso.hom (Functor.commShiftIso L 0)) Y))
    (ShiftedHom.mk₀ 0 ⋯ (L.map f))

Tactic:
dsimp [equiv, mk₀, ShiftedHom.mk₀, shiftFunctorZero']

Premises used: CategoryTheory.ShiftedHom.mk₀, CategoryTheory.shiftFunctorZero', CategoryTheory.Localization.SmallShiftedHom.mk₀, CategoryTheory.Localization.SmallShiftedHom.equiv
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
W : MorphismProperty.{v₁, u₁} C
M : Type w'
inst_2 : AddMonoid M
inst_3 : HasShift.{v₁, u₁, w'} C M
inst_4 : HasShift.{v₂, u₂, w'} D M
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_5 : L.IsLocalization W
inst_6 : L.CommShift M
X Y : C
inst_7 : HasSmallLocalizedShiftedHom W M X Y
f : X ⟶ Y
⊢ (L.map f ≫
        L.map
          (NatTrans.app (Iso.inv (shiftFunctorZero C M)) Y ≫
            𝟙 (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor.{v₁, u₁, w'} C (A := M) 0) Y))) ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso L 0)) Y =
    L.map f ≫
      NatTrans.app (Iso.inv (shiftFunctorZero D M)) (L.obj Y) ≫
        𝟙 (Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor.{v₂, u₂, w'} D (A := M) 0) (L.obj Y))

Tactic:
simp only [comp_id, L.commShiftIso_zero, Functor.CommShift.isoZero_hom_app, assoc,
    ← Functor.map_comp_assoc, Iso.inv_hom_id_app, Functor.id_obj, Functor.map_id, id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.CommShift.isoZero_hom_app, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Functor.id_obj, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Functor.CommShift.commShiftIso_zero, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
W : MorphismProperty.{v₁, u₁} C
M : Type w'
inst_2 : AddMonoid M
inst_3 : HasShift.{v₁, u₁, w'} C M
inst_4 : HasShift.{v₂, u₂, w'} D M
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_5 : L.IsLocalization W
inst_6 : L.CommShift M
X Y : C
inst_7 : HasSmallLocalizedShiftedHom W M Y X
inst_8 : W.RespectsIso
m₀ : M
hm₀ : m₀ = 0
f : X ⟶ Y
hf : W f
⊢ W (X := Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C m₀) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero' C m₀ hm₀)) X ≫ f)

Tactic:
have hf' : W ((shiftFunctorZero' C m₀ hm₀).hom.app X ≫ f) :=
    MorphismProperty.RespectsIso.precomp _ _ _ hf