awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
W₁ : MorphismProperty.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
W₂ : MorphismProperty.{v₂, u₂} C₂
D₁ : Type u₃
inst_2 : Category.{v₃, u₃} D₁
D₂ : Type u₄
inst_3 : Category.{v₄, u₄} D₂
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₃, u₁, u₃} C₁ D₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
inst_5 : L₂.IsLocalization W₂
X Y : C₁
inst_6 : HasSmallLocalizedHom W₁ X Y
X' Y' : C₂
inst_7 : HasSmallLocalizedHom W₂ X' X'
inst_8 : HasSmallLocalizedHom W₂ X' Y'
inst_9 : HasSmallLocalizedHom W₂ Y' Y'
eX : Φ.functor (W₁ := W₁) (W₂ := W₂).obj X ≅ X'
eY : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y ≅ Y'
G : Functor.{v₃, v₄, u₃, u₄} D₁ D₂
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G
f : SmallHom W₁ X Y
this : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Y'
⊢ (SmallHom.equiv W₂ L₂ : (a : SmallHom W₂ X' Y') → L₂.obj X' ⟶ L₂.obj Y')
      (Φ.smallHomMap' (W₁ := W₁) (W₂ := W₂) eX eY f) =
    L₂.map eX.inv ≫
      e.hom.app X ≫
        G.map ((SmallHom.equiv W₁ L₁ : (a : SmallHom W₁ X Y) → L₁.obj X ⟶ L₁.obj Y) f) ≫ e.inv.app Y ≫ L₂.map eY.hom

Tactic:
simp [smallHomMap', SmallHom.equiv_comp, Φ.equiv_smallHomMap L₁ L₂ G e]

Premises used: CategoryTheory.Localization.SmallHom.equiv_comp, CategoryTheory.LocalizerMorphism.equiv_smallHomMap, CategoryTheory.LocalizerMorphism.smallHomMap'
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
W₁ : MorphismProperty.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
X Y : C₁
inst_2 : HasSmallLocalizedHom W₁ X Y
X' Y' : C₂
inst_3 : HasSmallLocalizedHom W₂ X' X'
inst_4 : HasSmallLocalizedHom W₂ X' Y'
inst_5 : HasSmallLocalizedHom W₂ Y' Y'
eX : Φ.functor (W₁ := W₁) (W₂ := W₂).obj X ≅ X'
eY : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y ≅ Y'
f : X ⟶ Y
⊢ Eq.{w' + 1} (α := SmallHom W₂ X' Y')
    (smallHomMap'.{w, w', v₁, v₂, u₁, u₂} (W₁ := W₁) (W₂ := W₂) Φ eX eY (SmallHom.mk W₁ f))
    (SmallHom.mk W₂ (eX.inv ≫ Φ.functor (W₁ := W₁) (W₂ := W₂).map f ≫ eY.hom))

Tactic:
simp [smallHomMap', SmallHom.mk_comp_mk]

Premises used: CategoryTheory.Localization.SmallHom.mk_comp_mk, CategoryTheory.LocalizerMorphism.smallHomMap'
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
W₁ : MorphismProperty.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst_2 : HasSmallLocalizedHom W₁ X Y
inst_3 : HasSmallLocalizedHom W₁ Y Z
inst_4 : HasSmallLocalizedHom W₁ X Z
X' Y' Z' : C₂
inst_5 : HasSmallLocalizedHom W₂ X' X'
inst_6 : HasSmallLocalizedHom W₂ Y' Y'
inst_7 : HasSmallLocalizedHom W₂ Z' Z'
inst_8 : HasSmallLocalizedHom W₂ X' Y'
inst_9 : HasSmallLocalizedHom W₂ Y' Z'
inst_10 : HasSmallLocalizedHom W₂ X' Z'
eX : Φ.functor (W₁ := W₁) (W₂ := W₂).obj X ≅ X'
eY : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y ≅ Y'
eZ : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z ≅ Z'
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
⊢ HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)

Tactic:
have := hasSmallLocalizedHom_of_isos.{w'} W₂ eX.symm eY.symm
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
W₁ : MorphismProperty.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst_2 : HasSmallLocalizedHom W₁ X Y
inst_3 : HasSmallLocalizedHom W₁ Y Z
inst_4 : HasSmallLocalizedHom W₁ X Z
X' Y' Z' : C₂
inst_5 : HasSmallLocalizedHom W₂ X' X'
inst_6 : HasSmallLocalizedHom W₂ Y' Y'
inst_7 : HasSmallLocalizedHom W₂ Z' Z'
inst_8 : HasSmallLocalizedHom W₂ X' Y'
inst_9 : HasSmallLocalizedHom W₂ Y' Z'
inst_10 : HasSmallLocalizedHom W₂ X' Z'
eX : Φ.functor (W₁ := W₁) (W₂ := W₂).obj X ≅ X'
eY : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y ≅ Y'
eZ : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z ≅ Z'
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
this : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
⊢ HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Y'

Tactic:
have := hasSmallLocalizedHom_of_isos.{w'} W₂ eY.symm (Iso.refl Y')
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
W₁ : MorphismProperty.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst_2 : HasSmallLocalizedHom W₁ X Y
inst_3 : HasSmallLocalizedHom W₁ Y Z
inst_4 : HasSmallLocalizedHom W₁ X Z
X' Y' Z' : C₂
inst_5 : HasSmallLocalizedHom W₂ X' X'
inst_6 : HasSmallLocalizedHom W₂ Y' Y'
inst_7 : HasSmallLocalizedHom W₂ Z' Z'
inst_8 : HasSmallLocalizedHom W₂ X' Y'
inst_9 : HasSmallLocalizedHom W₂ Y' Z'
inst_10 : HasSmallLocalizedHom W₂ X' Z'
eX : Φ.functor (W₁ := W₁) (W₂ := W₂).obj X ≅ X'
eY : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y ≅ Y'
eZ : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z ≅ Z'
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
this_1 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
this : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Y'
⊢ HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) Z'

Tactic:
have := hasSmallLocalizedHom_of_isos.{w'} W₂ eX.symm (Iso.refl Z')
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
W₁ : MorphismProperty.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst_2 : HasSmallLocalizedHom W₁ X Y
inst_3 : HasSmallLocalizedHom W₁ Y Z
inst_4 : HasSmallLocalizedHom W₁ X Z
X' Y' Z' : C₂
inst_5 : HasSmallLocalizedHom W₂ X' X'
inst_6 : HasSmallLocalizedHom W₂ Y' Y'
inst_7 : HasSmallLocalizedHom W₂ Z' Z'
inst_8 : HasSmallLocalizedHom W₂ X' Y'
inst_9 : HasSmallLocalizedHom W₂ Y' Z'
inst_10 : HasSmallLocalizedHom W₂ X' Z'
eX : Φ.functor (W₁ := W₁) (W₂ := W₂).obj X ≅ X'
eY : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y ≅ Y'
eZ : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z ≅ Z'
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
this_1 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
this_2 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Y'
this : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) Z'
⊢ HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z)

Tactic:
have := hasSmallLocalizedHom_of_isos.{w'} W₂ eY.symm eZ.symm
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
W₁ : MorphismProperty.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst_2 : HasSmallLocalizedHom W₁ X Y
inst_3 : HasSmallLocalizedHom W₁ Y Z
inst_4 : HasSmallLocalizedHom W₁ X Z
X' Y' Z' : C₂
inst_5 : HasSmallLocalizedHom W₂ X' X'
inst_6 : HasSmallLocalizedHom W₂ Y' Y'
inst_7 : HasSmallLocalizedHom W₂ Z' Z'
inst_8 : HasSmallLocalizedHom W₂ X' Y'
inst_9 : HasSmallLocalizedHom W₂ Y' Z'
inst_10 : HasSmallLocalizedHom W₂ X' Z'
eX : Φ.functor (W₁ := W₁) (W₂ := W₂).obj X ≅ X'
eY : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y ≅ Y'
eZ : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z ≅ Z'
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
this_1 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
this_2 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Y'
this_3 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) Z'
this : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z)
⊢ HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Z'

Tactic:
have := hasSmallLocalizedHom_of_isos.{w'} W₂ eY.symm (Iso.refl Z')
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
W₁ : MorphismProperty.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst_2 : HasSmallLocalizedHom W₁ X Y
inst_3 : HasSmallLocalizedHom W₁ Y Z
inst_4 : HasSmallLocalizedHom W₁ X Z
X' Y' Z' : C₂
inst_5 : HasSmallLocalizedHom W₂ X' X'
inst_6 : HasSmallLocalizedHom W₂ Y' Y'
inst_7 : HasSmallLocalizedHom W₂ Z' Z'
inst_8 : HasSmallLocalizedHom W₂ X' Y'
inst_9 : HasSmallLocalizedHom W₂ Y' Z'
inst_10 : HasSmallLocalizedHom W₂ X' Z'
eX : Φ.functor (W₁ := W₁) (W₂ := W₂).obj X ≅ X'
eY : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y ≅ Y'
eZ : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z ≅ Z'
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
this_1 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
this_2 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Y'
this_3 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) Z'
this_4 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z)
this : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Z'
⊢ HasSmallLocalizedHom W₂ Y' (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)

Tactic:
have := hasSmallLocalizedHom_of_isos.{w'} W₂ (Iso.refl Y') eY.symm
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
W₁ : MorphismProperty.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst_2 : HasSmallLocalizedHom W₁ X Y
inst_3 : HasSmallLocalizedHom W₁ Y Z
inst_4 : HasSmallLocalizedHom W₁ X Z
X' Y' Z' : C₂
inst_5 : HasSmallLocalizedHom W₂ X' X'
inst_6 : HasSmallLocalizedHom W₂ Y' Y'
inst_7 : HasSmallLocalizedHom W₂ Z' Z'
inst_8 : HasSmallLocalizedHom W₂ X' Y'
inst_9 : HasSmallLocalizedHom W₂ Y' Z'
inst_10 : HasSmallLocalizedHom W₂ X' Z'
eX : Φ.functor (W₁ := W₁) (W₂ := W₂).obj X ≅ X'
eY : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y ≅ Y'
eZ : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z ≅ Z'
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
this_1 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
this_2 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Y'
this_3 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) Z'
this_4 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z)
this_5 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Z'
this : HasSmallLocalizedHom W₂ Y' (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
⊢ HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)

Tactic:
have := hasSmallLocalizedHom_of_isos.{w'} W₂ eY.symm eY.symm
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
W₁ : MorphismProperty.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst_2 : HasSmallLocalizedHom W₁ X Y
inst_3 : HasSmallLocalizedHom W₁ Y Z
inst_4 : HasSmallLocalizedHom W₁ X Z
X' Y' Z' : C₂
inst_5 : HasSmallLocalizedHom W₂ X' X'
inst_6 : HasSmallLocalizedHom W₂ Y' Y'
inst_7 : HasSmallLocalizedHom W₂ Z' Z'
inst_8 : HasSmallLocalizedHom W₂ X' Y'
inst_9 : HasSmallLocalizedHom W₂ Y' Z'
inst_10 : HasSmallLocalizedHom W₂ X' Z'
eX : Φ.functor (W₁ := W₁) (W₂ := W₂).obj X ≅ X'
eY : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y ≅ Y'
eZ : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z ≅ Z'
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
this_1 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
this_2 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Y'
this_3 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) Z'
this_4 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z)
this_5 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Z'
this_6 : HasSmallLocalizedHom W₂ Y' (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
this : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
simp :
  Eq.{w' + 1} (α := SmallHom W₂ X' Z')
    (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eX.inv)
      (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) f)
        (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))))
    (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eX.inv)
      (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) f)
        (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eY.hom)
          (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eY.inv)
            (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))))))
⊢ Eq.{w' + 1} (α := SmallHom W₂ X' Z') (Φ.smallHomMap' (W₁ := W₁) (W₂ := W₂) eX eZ (f.comp (W := W₁) g))
    (SmallHom.comp (W := W₂) (Φ.smallHomMap' (W₁ := W₁) (W₂ := W₂) eX eY f)
      (Φ.smallHomMap' (W₁ := W₁) (W₂ := W₂) eY eZ g))

Tactic:
simp only [smallHomMap', smallHomMap_comp, SmallHom.comp_assoc]

Premises used: CategoryTheory.LocalizerMorphism.smallHomMap_comp, CategoryTheory.Localization.SmallHom.comp_assoc, CategoryTheory.LocalizerMorphism.smallHomMap'
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
W₁ : MorphismProperty.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst_2 : HasSmallLocalizedHom W₁ X Y
inst_3 : HasSmallLocalizedHom W₁ Y Z
inst_4 : HasSmallLocalizedHom W₁ X Z
X' Y' Z' : C₂
inst_5 : HasSmallLocalizedHom W₂ X' X'
inst_6 : HasSmallLocalizedHom W₂ Y' Y'
inst_7 : HasSmallLocalizedHom W₂ Z' Z'
inst_8 : HasSmallLocalizedHom W₂ X' Y'
inst_9 : HasSmallLocalizedHom W₂ Y' Z'
inst_10 : HasSmallLocalizedHom W₂ X' Z'
eX : Φ.functor (W₁ := W₁) (W₂ := W₂).obj X ≅ X'
eY : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y ≅ Y'
eZ : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z ≅ Z'
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
this_1 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
this_2 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Y'
this_3 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) Z'
this_4 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z)
this_5 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Z'
this_6 : HasSmallLocalizedHom W₂ Y' (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
this : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
e_β :
  Eq.{w' + 1} (α := SmallHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Z')
    (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))
    (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eY.hom)
      (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eY.inv)
        (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))))
⊢ Eq.{w' + 1} (α := SmallHom W₂ X' Z')
    (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eX.inv)
      (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) f)
        (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))))
    (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eX.inv)
      (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) f)
        (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eY.hom)
          (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eY.inv)
            (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))))))

Tactic:
congr 2
-- 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
⊢ ∀ (a b : M),
    Small.{w, v₂} ((shiftFunctor C a ⋙ L).obj X ⟶ (shiftFunctor C b ⋙ L).obj Y) ↔
      Small.{w, v₂} ((L ⋙ shiftFunctor D a).obj X ⟶ (L ⋙ shiftFunctor D b).obj Y)

Tactic:
have eq := fun (a b : M) ↦ small_congr.{w}
    (Iso.homCongr ((L.commShiftIso a).app X) ((L.commShiftIso b).app Y))
-- 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
eq :
  ∀ (a b : M),
    Small.{w, v₂}
        (L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) ⟶
          L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C b) Y)) ↔
      Small.{w, v₂}
        (Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj X) ⟶
          Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D b) (L.obj Y))
⊢ (∀ (a b : M),
      HasSmallLocalizedHom W (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)
        (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C b) Y)) ↔
    ∀ (a b : M),
      Small.{w, v₂}
        (Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj X) ⟶
          Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D b) (L.obj Y))

Tactic:
simp only [hasSmallLocalizedHom_iff _ L, eq]

Premises used: CategoryTheory.Localization.hasSmallLocalizedHom_iff
-- 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 : W.IsCompatibleWithShift M
Y' : C
f : Y ⟶ Y'
hf : W f
⊢ HasSmallLocalizedShiftedHom W M X Y ↔ HasSmallLocalizedShiftedHom W M X Y'

Tactic:
forall_congr' (fun a ↦ forall_congr' (fun b ↦
    hasSmallLocalizedHom_iff_target W (X⟦a⟧) (f⟦b⟧') (W.shift hf b)))

Premises used: CategoryTheory.shiftFunctor, CategoryTheory.Localization.hasSmallLocalizedHom_iff_target, CategoryTheory.Functor.map, CategoryTheory.MorphismProperty.shift, forall_congr', CategoryTheory.Functor.obj
-- 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 : C
inst_3 : W.IsCompatibleWithShift M
X' : C
f : X ⟶ X'
hf : W f
Y : C
⊢ HasSmallLocalizedShiftedHom W M X Y ↔ HasSmallLocalizedShiftedHom W M X' Y

Tactic:
forall_congr' (fun a ↦ forall_congr' (fun b ↦
    hasSmallLocalizedHom_iff_source W (f⟦a⟧') (W.shift hf a) (Y⟦b⟧)))

Premises used: CategoryTheory.shiftFunctor, CategoryTheory.Localization.hasSmallLocalizedHom_iff_source, CategoryTheory.Functor.map, CategoryTheory.MorphismProperty.shift, forall_congr', CategoryTheory.Functor.obj
-- 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
⊢ HasSmallLocalizedHom W X Y

Tactic:
(hasSmallLocalizedHom_iff_of_isos W
    ((shiftFunctorZero C M).app X) ((shiftFunctorZero C M).app Y)).1 inferInstance

Premises used: CategoryTheory.Localization.hasSmallLocalizedHom_iff_of_isos, CategoryTheory.shiftFunctorZero, inferInstance, Iff.mp, CategoryTheory.Iso.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
X Y : C
inst_5 : HasSmallLocalizedShiftedHom W M X Y
m : M
⊢ HasSmallLocalizedHom W X (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C m) Y)

Tactic:
(hasSmallLocalizedHom_iff_of_isos W
    ((shiftFunctorZero C M).app X) (Iso.refl (Y⟦m⟧))).1 inferInstance

Premises used: CategoryTheory.Localization.hasSmallLocalizedHom_iff_of_isos, CategoryTheory.shiftFunctor, CategoryTheory.shiftFunctorZero, inferInstance, CategoryTheory.Iso.refl, Iff.mp, CategoryTheory.Iso.app, CategoryTheory.Functor.obj
-- 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
m : M
⊢ HasSmallLocalizedHom W (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C m) X) Y

Tactic:
(hasSmallLocalizedHom_iff_of_isos W
    (Iso.refl (X⟦m⟧)) ((shiftFunctorZero C M).app Y)).1 inferInstance

Premises used: CategoryTheory.Localization.hasSmallLocalizedHom_iff_of_isos, CategoryTheory.shiftFunctor, CategoryTheory.shiftFunctorZero, inferInstance, CategoryTheory.Iso.refl, Iff.mp, CategoryTheory.Iso.app, CategoryTheory.Functor.obj
-- 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
m m' n : M
⊢ HasSmallLocalizedHom W
    (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C m') (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C m) X))
    (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C n) Y)

Tactic:
(hasSmallLocalizedHom_iff_of_isos W
    ((shiftFunctorAdd C m m').app X) (Iso.refl (Y⟦n⟧))).1 inferInstance

Premises used: CategoryTheory.Localization.hasSmallLocalizedHom_iff_of_isos, CategoryTheory.shiftFunctor, inferInstance, CategoryTheory.Iso.refl, CategoryTheory.shiftFunctorAdd, Iff.mp, CategoryTheory.Iso.app, CategoryTheory.Functor.obj
-- 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
m n n' : M
⊢ HasSmallLocalizedHom W (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C m) X)
    (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C n') (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C n) Y))

Tactic:
(hasSmallLocalizedHom_iff_of_isos W
    (Iso.refl (X⟦m⟧)) ((shiftFunctorAdd C n n').app Y)).1 inferInstance

Premises used: CategoryTheory.Localization.hasSmallLocalizedHom_iff_of_isos, CategoryTheory.shiftFunctor, inferInstance, CategoryTheory.Iso.refl, CategoryTheory.shiftFunctorAdd, Iff.mp, CategoryTheory.Iso.app, CategoryTheory.Functor.obj