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
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
hf' :
  W (X := Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C m₀) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero' C m₀ hm₀)) X ≫ f)
⊢ Eq.{v₂ + 1} (α := ShiftedHom (L.obj Y) (L.obj X) m₀)
    ((equiv W L : (a : SmallShiftedHom W Y X m₀) → ShiftedHom (L.obj Y) (L.obj X) m₀) (mk₀Inv (W := W) m₀ hm₀ f hf) :
      ShiftedHom (L.obj Y) (L.obj X) m₀)
    (ShiftedHom.mk₀ m₀ hm₀ (isoOfHom L W f hf).inv : ShiftedHom (L.obj Y) (L.obj X) m₀)

Tactic:
(SmallHom.equiv_mkInv L _ hf' =≫ _).trans ?_

Premises used: CategoryTheory.eq_whisker, CategoryTheory.Localization.SmallHom.equiv_mkInv, CategoryTheory.Localization.SmallShiftedHom.mk₀Inv, Eq.trans
-- 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
hf' :
  W (X := Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C m₀) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero' C m₀ hm₀)) X ≫ f)
refine :
  Eq (α := L.obj Y ⟶ (L ⋙ shiftFunctor D m₀).obj X)
    ((isoOfHom L W (NatTrans.app (Iso.hom (shiftFunctorZero' C m₀ hm₀)) X ≫ f) hf').inv ≫
      Iso.hom (Iso.app (Functor.commShiftIso L m₀) X))
    (ShiftedHom.mk₀ m₀ hm₀ (isoOfHom L W f hf).inv)
⊢ Eq.{v₂ + 1} (α := ShiftedHom (L.obj Y) (L.obj X) m₀)
    ((equiv W L : (a : SmallShiftedHom W Y X m₀) → ShiftedHom (L.obj Y) (L.obj X) m₀) (mk₀Inv (W := W) m₀ hm₀ f hf) :
      ShiftedHom (L.obj Y) (L.obj X) m₀)
    (ShiftedHom.mk₀ m₀ hm₀ (isoOfHom L W f hf).inv : ShiftedHom (L.obj Y) (L.obj X) m₀)

Tactic:
refine (SmallHom.equiv_mkInv L _ hf' =≫ _).trans ?_

Premises used: CategoryTheory.eq_whisker, CategoryTheory.Localization.SmallHom.equiv_mkInv, Eq.trans
-- 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
hf' :
  W (X := Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C m₀) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero' C m₀ hm₀)) X ≫ f)
rw :
  Eq (α := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C m₀) X) ⟶ (L ⋙ shiftFunctor D m₀).obj X)
    (Iso.hom (Iso.app (Functor.commShiftIso L m₀) X))
    ((isoOfHom L W (NatTrans.app (Iso.hom (shiftFunctorZero' C m₀ hm₀)) X ≫ f) hf').hom ≫
      ShiftedHom.mk₀ m₀ hm₀ (isoOfHom L W f hf).inv)
⊢ Eq (α := L.obj Y ⟶ (L ⋙ shiftFunctor D m₀).obj X)
    ((isoOfHom L W (NatTrans.app (Iso.hom (shiftFunctorZero' C m₀ hm₀)) X ≫ f) hf').inv ≫
      Iso.hom (Iso.app (Functor.commShiftIso L m₀) X))
    (ShiftedHom.mk₀ m₀ hm₀ (isoOfHom L W f hf).inv)

Tactic:
rw [← cancel_epi (isoOfHom L W _ hf').hom, Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Localization.isoOfHom, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- 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
hf' :
  W (X := Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C m₀) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero' C m₀ hm₀)) X ≫ f)
⊢ Eq (α := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C m₀) X) ⟶ (L ⋙ shiftFunctor D m₀).obj X)
    (Iso.hom (Iso.app (Functor.commShiftIso L m₀) X))
    ((isoOfHom L W (NatTrans.app (Iso.hom (shiftFunctorZero' C m₀ hm₀)) X ≫ f) hf').hom ≫
      ShiftedHom.mk₀ m₀ hm₀ (isoOfHom L W f hf).inv)

Tactic:
simp [ShiftedHom.mk₀, Functor.commShiftIso_zero' _ _ m₀ hm₀]

Premises used: CategoryTheory.ShiftedHom.mk₀, CategoryTheory.Functor.commShiftIso_zero'
-- 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
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
inst_6 : HasSmallLocalizedShiftedHom W M X Y
inst_7 : HasSmallLocalizedShiftedHom W M X Z
inst_8 : HasSmallLocalizedShiftedHom W M X T
inst_9 : HasSmallLocalizedShiftedHom W M Y Z
inst_10 : HasSmallLocalizedShiftedHom W M Y T
inst_11 : HasSmallLocalizedShiftedHom W M Z T
inst_12 : HasSmallLocalizedShiftedHom W M Z Z
inst_13 : HasSmallLocalizedShiftedHom W M T T
α : SmallShiftedHom W X Y a₁
β : SmallShiftedHom W Y Z a₂
γ : SmallShiftedHom W Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h : a₃ + a₂ + a₁ = a
rw : a₃ + (a₂ + a₁) = a
rw₁ : a₃ + a₂ + a₁ = a
rw₂ rw₃ : a = a
⊢ a₃ + a₁₂ = a

Tactic:
rw [← h₁₂, ← add_assoc, h]

Premises used: add_assoc
-- 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
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
inst_6 : HasSmallLocalizedShiftedHom W M X Y
inst_7 : HasSmallLocalizedShiftedHom W M X Z
inst_8 : HasSmallLocalizedShiftedHom W M X T
inst_9 : HasSmallLocalizedShiftedHom W M Y Z
inst_10 : HasSmallLocalizedShiftedHom W M Y T
inst_11 : HasSmallLocalizedShiftedHom W M Z T
inst_12 : HasSmallLocalizedShiftedHom W M Z Z
inst_13 : HasSmallLocalizedShiftedHom W M T T
α : SmallShiftedHom W X Y a₁
β : SmallShiftedHom W Y Z a₂
γ : SmallShiftedHom W Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h rw : a₃ + a₂ + a₁ = a
rw₁ rw₂ : a = a
⊢ a₂₃ + a₁ = a

Tactic:
rw [← h₂₃, h]
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
M : Type w'
inst_1 : AddMonoid M
inst_2 : HasShift.{v₁, u₁, w'} C M
inst_3 : W.IsCompatibleWithShift M
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
inst_4 : HasSmallLocalizedShiftedHom W M X Y
inst_5 : HasSmallLocalizedShiftedHom W M X Z
inst_6 : HasSmallLocalizedShiftedHom W M X T
inst_7 : HasSmallLocalizedShiftedHom W M Y Z
inst_8 : HasSmallLocalizedShiftedHom W M Y T
inst_9 : HasSmallLocalizedShiftedHom W M Z T
inst_10 : HasSmallLocalizedShiftedHom W M Z Z
inst_11 : HasSmallLocalizedShiftedHom W M T T
α : SmallShiftedHom W X Y a₁
β : SmallShiftedHom W Y Z a₂
γ : SmallShiftedHom W Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h : a₃ + a₂ + a₁ = a
a₄ :
  Eq (α := ShiftedHom (W.Q.obj X) (W.Q.obj T) a)
    ((equiv W W.Q : (a_1 : SmallShiftedHom W X T a) → ShiftedHom (W.Q.obj X) (W.Q.obj T) a)
        (comp (W := W) (α.comp (W := W) β h₁₂) γ ⋯) :
      ShiftedHom (W.Q.obj X) (W.Q.obj T) a)
    ((equiv W W.Q : (a_1 : SmallShiftedHom W X T a) → ShiftedHom (W.Q.obj X) (W.Q.obj T) a)
        (α.comp (W := W) (β.comp (W := W) γ h₂₃) ⋯) :
      ShiftedHom (W.Q.obj X) (W.Q.obj T) a)
⊢ Eq (α := SmallShiftedHom W X T a) (comp (W := W) (α.comp (W := W) β h₁₂) γ ⋯)
    (α.comp (W := W) (β.comp (W := W) γ h₂₃) ⋯)

Tactic:
apply (equiv W W.Q).injective

Premises used: CategoryTheory.MorphismProperty.Q, Equiv.injective, CategoryTheory.Localization.SmallShiftedHom.equiv
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
M : Type w'
inst_1 : AddMonoid M
inst_2 : HasShift.{v₁, u₁, w'} C M
inst_3 : W.IsCompatibleWithShift M
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
inst_4 : HasSmallLocalizedShiftedHom W M X Y
inst_5 : HasSmallLocalizedShiftedHom W M X Z
inst_6 : HasSmallLocalizedShiftedHom W M X T
inst_7 : HasSmallLocalizedShiftedHom W M Y Z
inst_8 : HasSmallLocalizedShiftedHom W M Y T
inst_9 : HasSmallLocalizedShiftedHom W M Z T
inst_10 : HasSmallLocalizedShiftedHom W M Z Z
inst_11 : HasSmallLocalizedShiftedHom W M T T
α : SmallShiftedHom W X Y a₁
β : SmallShiftedHom W Y Z a₂
γ : SmallShiftedHom W Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h : a₃ + a₂ + a₁ = a
⊢ Eq (α := ShiftedHom (W.Q.obj X) (W.Q.obj T) a)
    ((equiv W W.Q : (a_1 : SmallShiftedHom W X T a) → ShiftedHom (W.Q.obj X) (W.Q.obj T) a)
        (comp (W := W) (α.comp (W := W) β h₁₂) γ ⋯) :
      ShiftedHom (W.Q.obj X) (W.Q.obj T) a)
    ((equiv W W.Q : (a_1 : SmallShiftedHom W X T a) → ShiftedHom (W.Q.obj X) (W.Q.obj T) a)
        (α.comp (W := W) (β.comp (W := W) γ h₂₃) ⋯) :
      ShiftedHom (W.Q.obj X) (W.Q.obj T) a)

Tactic:
simp only [equiv_comp, ShiftedHom.comp_assoc _ _ _ h₁₂ h₂₃ h]

Premises used: CategoryTheory.Localization.SmallShiftedHom.equiv_comp, CategoryTheory.ShiftedHom.comp_assoc
-- 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
X Y : C
inst_5 : HasSmallLocalizedShiftedHom W M X Y
inst_6 : HasSmallLocalizedShiftedHom W M Y Y
inst_7 : HasSmallLocalizedShiftedHom W M Y X
inst_8 : W.IsCompatibleWithShift M
inst_9 : W.RespectsIso
m₀ : M
hm₀ : m₀ = 0
f : Y ⟶ X
hf : W f
subst : HAdd.hAdd (α := M) 0 0 = 0
⊢ m₀ + m₀ = 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
X Y : C
inst_5 : HasSmallLocalizedShiftedHom W M X Y
inst_6 : HasSmallLocalizedShiftedHom W M Y Y
inst_7 : HasSmallLocalizedShiftedHom W M Y X
inst_8 : W.IsCompatibleWithShift M
inst_9 : W.RespectsIso
f : Y ⟶ X
hf : W f
⊢ HAdd.hAdd (α := M) 0 0 = 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
M : Type w'
inst_1 : AddMonoid M
inst_2 : HasShift.{v₁, u₁, w'} C M
X Y : C
inst_3 : HasSmallLocalizedShiftedHom W M X Y
inst_4 : HasSmallLocalizedShiftedHom W M Y Y
inst_5 : HasSmallLocalizedShiftedHom W M Y X
inst_6 : W.IsCompatibleWithShift M
inst_7 : W.RespectsIso
m₀ : M
hm₀ : m₀ = 0
f : Y ⟶ X
hf : W f
⊢ Eq (α := ShiftedHom (W.Q.obj Y) (W.Q.obj Y) m₀)
    ((equiv W W.Q : (a : SmallShiftedHom W Y Y m₀) → ShiftedHom (W.Q.obj Y) (W.Q.obj Y) m₀)
        (comp (W := W) (mk₀ W m₀ hm₀ f) (mk₀Inv (W := W) m₀ hm₀ f hf) ⋯) :
      ShiftedHom (W.Q.obj Y) (W.Q.obj Y) m₀)
    ((equiv W W.Q : (a : SmallShiftedHom W Y Y m₀) → ShiftedHom (W.Q.obj Y) (W.Q.obj Y) m₀) (mk₀ W m₀ hm₀ (𝟙 Y)) :
      ShiftedHom (W.Q.obj Y) (W.Q.obj Y) m₀)

Tactic:
simp [equiv_comp]

Premises used: CategoryTheory.Localization.SmallShiftedHom.equiv_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
X Y : C
inst_5 : HasSmallLocalizedShiftedHom W M X Y
inst_6 : HasSmallLocalizedShiftedHom W M X X
inst_7 : HasSmallLocalizedShiftedHom W M Y X
inst_8 : W.IsCompatibleWithShift M
inst_9 : W.RespectsIso
m₀ : M
hm₀ : m₀ = 0
f : Y ⟶ X
hf : W f
subst : HAdd.hAdd (α := M) 0 0 = 0
⊢ m₀ + m₀ = 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
X Y : C
inst_5 : HasSmallLocalizedShiftedHom W M X Y
inst_6 : HasSmallLocalizedShiftedHom W M X X
inst_7 : HasSmallLocalizedShiftedHom W M Y X
inst_8 : W.IsCompatibleWithShift M
inst_9 : W.RespectsIso
f : Y ⟶ X
hf : W f
⊢ HAdd.hAdd (α := M) 0 0 = 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
M : Type w'
inst_1 : AddMonoid M
inst_2 : HasShift.{v₁, u₁, w'} C M
X Y : C
inst_3 : HasSmallLocalizedShiftedHom W M X Y
inst_4 : HasSmallLocalizedShiftedHom W M X X
inst_5 : HasSmallLocalizedShiftedHom W M Y X
inst_6 : W.IsCompatibleWithShift M
inst_7 : W.RespectsIso
m₀ : M
hm₀ : m₀ = 0
f : Y ⟶ X
hf : W f
⊢ Eq (α := ShiftedHom (W.Q.obj X) (W.Q.obj X) m₀)
    ((equiv W W.Q : (a : SmallShiftedHom W X X m₀) → ShiftedHom (W.Q.obj X) (W.Q.obj X) m₀)
        (comp (W := W) (mk₀Inv (W := W) m₀ hm₀ f hf) (mk₀ W m₀ hm₀ f) ⋯) :
      ShiftedHom (W.Q.obj X) (W.Q.obj X) m₀)
    ((equiv W W.Q : (a : SmallShiftedHom W X X m₀) → ShiftedHom (W.Q.obj X) (W.Q.obj X) m₀) (mk₀ W m₀ hm₀ (𝟙 X)) :
      ShiftedHom (W.Q.obj X) (W.Q.obj X) m₀)

Tactic:
simp [equiv_comp]

Premises used: CategoryTheory.Localization.SmallShiftedHom.equiv_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
X Y : C
inst_5 : HasSmallLocalizedShiftedHom W M X Y
inst_6 : HasSmallLocalizedShiftedHom W M Y Y
inst_7 : W.IsCompatibleWithShift M
m : M
α : SmallShiftedHom W X Y m
m₀ : M
hm₀ : m₀ = 0
⊢ m₀ + m = m

Tactic:
simp_all
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
M : Type w'
inst_1 : AddMonoid M
inst_2 : HasShift.{v₁, u₁, w'} C M
X Y : C
inst_3 : HasSmallLocalizedShiftedHom W M X Y
inst_4 : HasSmallLocalizedShiftedHom W M Y Y
inst_5 : W.IsCompatibleWithShift M
m : M
α : SmallShiftedHom W X Y m
m₀ : M
hm₀ : m₀ = 0
⊢ Eq (α := ShiftedHom (W.Q.obj X) (W.Q.obj Y) m)
    ((equiv W W.Q : (a : SmallShiftedHom W X Y m) → ShiftedHom (W.Q.obj X) (W.Q.obj Y) m)
        (α.comp (W := W) (mk₀ W m₀ hm₀ (𝟙 Y)) ⋯) :
      ShiftedHom (W.Q.obj X) (W.Q.obj Y) m)
    ((equiv W W.Q : (a : SmallShiftedHom W X Y m) → ShiftedHom (W.Q.obj X) (W.Q.obj Y) m) α :
      ShiftedHom (W.Q.obj X) (W.Q.obj Y) m)

Tactic:
simp [equiv_comp]

Premises used: CategoryTheory.Localization.SmallShiftedHom.equiv_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
X Y : C
inst_5 : HasSmallLocalizedShiftedHom W M X Y
inst_6 : HasSmallLocalizedShiftedHom W M X X
inst_7 : HasSmallLocalizedShiftedHom W M Y Y
inst_8 : W.IsCompatibleWithShift M
m : M
α : SmallShiftedHom W X Y m
m₀ : M
hm₀ : m₀ = 0
⊢ m + m₀ = m

Tactic:
simp_all
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
M : Type w'
inst_1 : AddMonoid M
inst_2 : HasShift.{v₁, u₁, w'} C M
X Y : C
inst_3 : HasSmallLocalizedShiftedHom W M X Y
inst_4 : HasSmallLocalizedShiftedHom W M X X
inst_5 : HasSmallLocalizedShiftedHom W M Y Y
inst_6 : W.IsCompatibleWithShift M
m : M
α : SmallShiftedHom W X Y m
m₀ : M
hm₀ : m₀ = 0
⊢ Eq (α := ShiftedHom (W.Q.obj X) (W.Q.obj Y) m)
    ((equiv W W.Q : (a : SmallShiftedHom W X Y m) → ShiftedHom (W.Q.obj X) (W.Q.obj Y) m)
        (comp (W := W) (mk₀ W m₀ hm₀ (𝟙 X)) α ⋯) :
      ShiftedHom (W.Q.obj X) (W.Q.obj Y) m)
    ((equiv W W.Q : (a : SmallShiftedHom W X Y m) → ShiftedHom (W.Q.obj X) (W.Q.obj Y) m) α :
      ShiftedHom (W.Q.obj X) (W.Q.obj Y) m)

Tactic:
simp [equiv_comp]

Premises used: CategoryTheory.Localization.SmallShiftedHom.equiv_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
X Y Z : C
inst_5 : W.RespectsIso
inst_6 : W.IsCompatibleWithShift M
inst_7 : HasSmallLocalizedShiftedHom W M X Y
inst_8 : HasSmallLocalizedShiftedHom W M Y Z
inst_9 : HasSmallLocalizedShiftedHom W M X Z
inst_10 : HasSmallLocalizedShiftedHom W M Z Y
inst_11 : HasSmallLocalizedShiftedHom W M Y Y
inst_12 : HasSmallLocalizedShiftedHom W M Z Z
f : Y ⟶ Z
hf : W f
a : M
α : SmallShiftedHom W X Y a
⊢ (fun (β : SmallShiftedHom W X Z a) ↦ (β.comp (W := W) (mk₀Inv (W := W) 0 ⋯ f hf) ⋯ : SmallShiftedHom W X Y a))
      ((fun (α : SmallShiftedHom W X Y a) ↦ (α.comp (W := W) (mk₀ W 0 ⋯ f) ⋯ : SmallShiftedHom W X Z a)) α) =
    α

Tactic:
simp [comp_assoc]

Premises used: CategoryTheory.Localization.SmallShiftedHom.comp_assoc
-- 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
X Y Z : C
inst_5 : W.RespectsIso
inst_6 : W.IsCompatibleWithShift M
inst_7 : HasSmallLocalizedShiftedHom W M X Y
inst_8 : HasSmallLocalizedShiftedHom W M Y Z
inst_9 : HasSmallLocalizedShiftedHom W M X Z
inst_10 : HasSmallLocalizedShiftedHom W M Z Y
inst_11 : HasSmallLocalizedShiftedHom W M Y Y
inst_12 : HasSmallLocalizedShiftedHom W M Z Z
f : Y ⟶ Z
hf : W f
a : M
β : SmallShiftedHom W X Z a
⊢ (fun (α : SmallShiftedHom W X Y a) ↦ (α.comp (W := W) (mk₀ W 0 ⋯ f) ⋯ : SmallShiftedHom W X Z a))
      ((fun (β : SmallShiftedHom W X Z a) ↦ (β.comp (W := W) (mk₀Inv (W := W) 0 ⋯ f hf) ⋯ : SmallShiftedHom W X Y a))
        β) =
    β

Tactic:
simp [comp_assoc]

Premises used: CategoryTheory.Localization.SmallShiftedHom.comp_assoc
-- 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
X Y Z : C
inst_5 : W.RespectsIso
inst_6 : W.IsCompatibleWithShift M
inst_7 : HasSmallLocalizedShiftedHom W M X X
inst_8 : HasSmallLocalizedShiftedHom W M Y Y
inst_9 : HasSmallLocalizedShiftedHom W M X Y
inst_10 : HasSmallLocalizedShiftedHom W M Y X
inst_11 : HasSmallLocalizedShiftedHom W M Y Z
inst_12 : HasSmallLocalizedShiftedHom W M X Z
inst_13 : HasSmallLocalizedShiftedHom W M Z Z
f : X ⟶ Y
hf : W f
a : M
α : SmallShiftedHom W Y Z a
⊢ (fun (β : SmallShiftedHom W X Z a) ↦ (comp (W := W) (mk₀Inv (W := W) 0 ⋯ f hf) β ⋯ : SmallShiftedHom W Y Z a))
      ((fun (α : SmallShiftedHom W Y Z a) ↦ (comp (W := W) (mk₀ W 0 ⋯ f) α ⋯ : SmallShiftedHom W X Z a)) α) =
    α

Tactic:
simp [← comp_assoc]

Premises used: CategoryTheory.Localization.SmallShiftedHom.comp_assoc
-- 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
X Y Z : C
inst_5 : W.RespectsIso
inst_6 : W.IsCompatibleWithShift M
inst_7 : HasSmallLocalizedShiftedHom W M X X
inst_8 : HasSmallLocalizedShiftedHom W M Y Y
inst_9 : HasSmallLocalizedShiftedHom W M X Y
inst_10 : HasSmallLocalizedShiftedHom W M Y X
inst_11 : HasSmallLocalizedShiftedHom W M Y Z
inst_12 : HasSmallLocalizedShiftedHom W M X Z
inst_13 : HasSmallLocalizedShiftedHom W M Z Z
f : X ⟶ Y
hf : W f
a : M
β : SmallShiftedHom W X Z a
⊢ (fun (α : SmallShiftedHom W Y Z a) ↦ (comp (W := W) (mk₀ W 0 ⋯ f) α ⋯ : SmallShiftedHom W X Z a))
      ((fun (β : SmallShiftedHom W X Z a) ↦ (comp (W := W) (mk₀Inv (W := W) 0 ⋯ f hf) β ⋯ : SmallShiftedHom W Y Z a))
        β) =
    β

Tactic:
simp [← comp_assoc]

Premises used: CategoryTheory.Localization.SmallShiftedHom.comp_assoc
-- 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
m : M
inst_7 : HasSmallLocalizedShiftedHom W M X Y
inst_8 : HasSmallLocalizedShiftedHom W M X Y
e : SmallShiftedHom W X Y m
dsimp :
  Eq.{v₂ + 1} (α := 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 : SmallShiftedHom W X Y m) → L.obj X ⟶ L.obj ((shiftFunctor C m).obj Y))
          ((chgUniv (W := W) : (a : SmallShiftedHom W X Y m) → SmallShiftedHom W X Y m) e))
        (NatTrans.app (Iso.hom (Functor.commShiftIso L m)) Y) :
      L.obj X ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D m) (L.obj Y))
    (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C m) Y))
        ((SmallHom.equiv W L : (a : SmallShiftedHom W X Y m) → L.obj X ⟶ L.obj ((shiftFunctor C m).obj Y)) e)
        (NatTrans.app (Iso.hom (Functor.commShiftIso L m)) Y) :
      L.obj X ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D m) (L.obj Y))
⊢ 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)
        ((chgUniv (W := W) : (a : SmallShiftedHom W X Y m) → SmallShiftedHom W X Y m) e) :
      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) e :
      ShiftedHom (L.obj X) (L.obj Y) m)

Tactic:
dsimp [equiv]

Premises used: CategoryTheory.Localization.SmallShiftedHom.equiv