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
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : L.IsLocalization W
X Y : C
h : HasSmallLocalizedHom W X Y
⊢ Small.{w, v₂} (L.obj X ⟶ L.obj Y)

Tactic:
small_map (homEquiv W W.Q L).symm

Premises used: CategoryTheory.Localization.homEquiv, CategoryTheory.MorphismProperty.Q, small_map, Equiv.symm
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : L.IsLocalization W
X Y : C
h : HasSmallLocalizedHom W X Y
⊢ Small.{w, v₂} (L.obj X ⟶ L.obj Y)

Tactic:
exact small_map (homEquiv W W.Q L).symm

Premises used: CategoryTheory.Localization.homEquiv, CategoryTheory.MorphismProperty.Q, small_map, Equiv.symm
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : L.IsLocalization W
X Y : C
h : Small.{w, v₂} (L.obj X ⟶ L.obj Y)
⊢ HasSmallLocalizedHom W X Y

Tactic:
⟨small_map (homEquiv W W.Q L)⟩

Premises used: CategoryTheory.Localization.homEquiv, CategoryTheory.MorphismProperty.Q, CategoryTheory.Localization.HasSmallLocalizedHom.mk, small_map
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : L.IsLocalization W
X Y : C
h : Small.{w, v₂} (L.obj X ⟶ L.obj Y)
⊢ HasSmallLocalizedHom W X Y

Tactic:
exact ⟨small_map (homEquiv W W.Q L)⟩
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : L.IsLocalization W
X Y : C
rw : Small.{v₂, v₂} (L.obj X ⟶ L.obj Y)
⊢ HasSmallLocalizedHom W X Y

Tactic:
rw [hasSmallLocalizedHom_iff W L]

Premises used: CategoryTheory.Localization.hasSmallLocalizedHom_iff
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : L.IsLocalization W
X Y : C
⊢ Small.{v₂, v₂} (L.obj X ⟶ L.obj Y)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : L.IsLocalization W
X Y : C
inst_3 rwa rwa₁ rwa₂ rwa₃ : HasSmallLocalizedHom W X Y
⊢ Small.{w, v₂} (L.obj X ⟶ L.obj Y)

Tactic:
rwa [← hasSmallLocalizedHom_iff W]

Premises used: CategoryTheory.Localization.hasSmallLocalizedHom_iff
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
X Y X' Y' : C
e : X ≅ X'
e' : Y ≅ Y'
simp : Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) ↔ Small.{w, max u₁ v₁} (W.Q.obj X' ⟶ W.Q.obj Y')
⊢ HasSmallLocalizedHom W X Y ↔ HasSmallLocalizedHom W X' Y'

Tactic:
simp only [hasSmallLocalizedHom_iff W W.Q]

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Localization.hasSmallLocalizedHom_iff
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
X Y X' Y' : C
e : X ≅ X'
e' : Y ≅ Y'
⊢ Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) ↔ Small.{w, max u₁ v₁} (W.Q.obj X' ⟶ W.Q.obj Y')

Tactic:
small_congr (Iso.homCongr (W.Q.mapIso e) (W.Q.mapIso e'))

Premises used: small_congr, CategoryTheory.MorphismProperty.Q, CategoryTheory.Iso.homCongr, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
X Y X' Y' : C
e : X ≅ X'
e' : Y ≅ Y'
⊢ Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) ↔ Small.{w, max u₁ v₁} (W.Q.obj X' ⟶ W.Q.obj Y')

Tactic:
exact small_congr (Iso.homCongr (W.Q.mapIso e) (W.Q.mapIso e'))

Premises used: small_congr, CategoryTheory.MorphismProperty.Q, CategoryTheory.Iso.homCongr, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
X Y X' Y' : C
e : X ≅ X'
e' : Y ≅ Y'
inst_1 rwa rwa₁ rwa₂ rwa₃ : HasSmallLocalizedHom W X Y
⊢ HasSmallLocalizedHom W X' Y'

Tactic:
rwa [← hasSmallLocalizedHom_iff_of_isos _ e e']

Premises used: CategoryTheory.Localization.hasSmallLocalizedHom_iff_of_isos
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
X Y Y' : C
f : Y ⟶ Y'
hf : W f
simp : Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) ↔ Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y')
⊢ HasSmallLocalizedHom W X Y ↔ HasSmallLocalizedHom W X Y'

Tactic:
simp only [hasSmallLocalizedHom_iff W W.Q]

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Localization.hasSmallLocalizedHom_iff
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
X Y Y' : C
f : Y ⟶ Y'
hf : W f
⊢ Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) ↔ Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y')

Tactic:
small_congr (Iso.homCongr (Iso.refl _) (Localization.isoOfHom W.Q W f hf))

Premises used: small_congr, CategoryTheory.MorphismProperty.Q, CategoryTheory.Iso.homCongr, CategoryTheory.Iso.refl, CategoryTheory.Localization.isoOfHom
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
X Y Y' : C
f : Y ⟶ Y'
hf : W f
⊢ Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) ↔ Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y')

Tactic:
exact small_congr (Iso.homCongr (Iso.refl _) (Localization.isoOfHom W.Q W f hf))

Premises used: small_congr, CategoryTheory.MorphismProperty.Q, CategoryTheory.Iso.homCongr, CategoryTheory.Iso.refl, CategoryTheory.Localization.isoOfHom
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
X X' : C
f : X ⟶ X'
hf : W f
Y : C
simp : Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) ↔ Small.{w, max u₁ v₁} (W.Q.obj X' ⟶ W.Q.obj Y)
⊢ HasSmallLocalizedHom W X Y ↔ HasSmallLocalizedHom W X' Y

Tactic:
simp only [hasSmallLocalizedHom_iff W W.Q]

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Localization.hasSmallLocalizedHom_iff
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
X X' : C
f : X ⟶ X'
hf : W f
Y : C
⊢ Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) ↔ Small.{w, max u₁ v₁} (W.Q.obj X' ⟶ W.Q.obj Y)

Tactic:
small_congr (Iso.homCongr (Localization.isoOfHom W.Q W f hf) (Iso.refl _))

Premises used: small_congr, CategoryTheory.MorphismProperty.Q, CategoryTheory.Iso.homCongr, CategoryTheory.Iso.refl, CategoryTheory.Localization.isoOfHom
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
X X' : C
f : X ⟶ X'
hf : W f
Y : C
⊢ Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) ↔ Small.{w, max u₁ v₁} (W.Q.obj X' ⟶ W.Q.obj Y)

Tactic:
exact small_congr (Iso.homCongr (Localization.isoOfHom W.Q W f hf) (Iso.refl _))

Premises used: small_congr, CategoryTheory.MorphismProperty.Q, CategoryTheory.Iso.homCongr, CategoryTheory.Iso.refl, CategoryTheory.Localization.isoOfHom
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
D' : Type u₃
inst_2 : Category.{v₃, u₃} D'
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : L.IsLocalization W
L' : Functor.{v₁, v₃, u₁, u₃} C D'
inst_4 : L'.IsLocalization W
G : Functor.{v₂, v₃, u₂, u₃} D D'
e : L ⋙ G ≅ L'
X Y : C
inst_5 : HasSmallLocalizedHom W X Y
f : L.obj X ⟶ L.obj Y
dsimp :
  (homEquiv W W.Q L' : (a : W.Q.obj X ⟶ W.Q.obj Y) → L'.obj X ⟶ L'.obj Y)
      ((Equiv.symm (equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) : (a : SmallHom W X Y) → W.Q.obj X ⟶ W.Q.obj Y)
        ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y) : (a : W.Q.obj X ⟶ W.Q.obj Y) → SmallHom W X Y)
          ((homEquiv W L W.Q : (a : L.obj X ⟶ L.obj Y) → W.Q.obj X ⟶ W.Q.obj Y) f : W.Q.obj X ⟶ W.Q.obj Y))) =
    e.inv.app X ≫ G.map f ≫ e.hom.app Y
⊢ (equiv W L' : (a : SmallHom W X Y) → L'.obj X ⟶ L'.obj Y)
      ((Equiv.symm (equiv W L) : (a : L.obj X ⟶ L.obj Y) → SmallHom W X Y) f) =
    e.inv.app X ≫ G.map f ≫ e.hom.app Y

Tactic:
dsimp [equiv]

Premises used: CategoryTheory.Localization.SmallHom.equiv
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
D' : Type u₃
inst_2 : Category.{v₃, u₃} D'
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : L.IsLocalization W
L' : Functor.{v₁, v₃, u₁, u₃} C D'
inst_4 : L'.IsLocalization W
G : Functor.{v₂, v₃, u₂, u₃} D D'
e : L ⋙ G ≅ L'
X Y : C
inst_5 : HasSmallLocalizedHom W X Y
f : L.obj X ⟶ L.obj Y
rw :
  ((homEquiv W L L' : Equiv.{v₂ + 1, v₃ + 1} (L.obj X ⟶ L.obj Y) (L'.obj X ⟶ L'.obj Y)) :
        (a : L.obj X ⟶ L.obj Y) → L'.obj X ⟶ L'.obj Y)
      f =
    e.inv.app X ≫ G.map f ≫ e.hom.app Y
⊢ (homEquiv W W.Q L' : (a : W.Q.obj X ⟶ W.Q.obj Y) → L'.obj X ⟶ L'.obj Y)
      ((Equiv.symm (equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) : (a : SmallHom W X Y) → W.Q.obj X ⟶ W.Q.obj Y)
        ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y) : (a : W.Q.obj X ⟶ W.Q.obj Y) → SmallHom W X Y)
          ((homEquiv W L W.Q : (a : L.obj X ⟶ L.obj Y) → W.Q.obj X ⟶ W.Q.obj Y) f : W.Q.obj X ⟶ W.Q.obj Y))) =
    e.inv.app X ≫ G.map f ≫ e.hom.app Y

Tactic:
rw [Equiv.symm_apply_apply, homEquiv_trans]

Premises used: Equiv.symm_apply_apply, CategoryTheory.Localization.homEquiv_trans
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
D' : Type u₃
inst_2 : Category.{v₃, u₃} D'
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : L.IsLocalization W
L' : Functor.{v₁, v₃, u₁, u₃} C D'
inst_4 : L'.IsLocalization W
G : Functor.{v₂, v₃, u₂, u₃} D D'
e : L ⋙ G ≅ L'
X Y : C
inst_5 : HasSmallLocalizedHom W X Y
f : L.obj X ⟶ L.obj Y
⊢ ((homEquiv W L L' : Equiv.{v₂ + 1, v₃ + 1} (L.obj X ⟶ L.obj Y) (L'.obj X ⟶ L'.obj Y)) :
        (a : L.obj X ⟶ L.obj Y) → L'.obj X ⟶ L'.obj Y)
      f =
    e.inv.app X ≫ G.map f ≫ e.hom.app Y

Tactic:
apply homEquiv_eq

Premises used: CategoryTheory.Localization.homEquiv_eq
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : L.IsLocalization W
X Y : C
inst_3 : HasSmallLocalizedHom W X Y
f : X ⟶ Y
⊢ (equiv W L : (a : SmallHom W X Y) → L.obj X ⟶ L.obj Y) (mk W f) = L.map f

Tactic:
simp [equiv, mk]

Premises used: CategoryTheory.Localization.SmallHom.mk, CategoryTheory.Localization.SmallHom.equiv
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : L.IsLocalization W
X Y : C
f : Y ⟶ X
hf : W f
inst_3 : HasSmallLocalizedHom W X Y
⊢ (equiv W L : (a : SmallHom W X Y) → L.obj X ⟶ L.obj Y) (mkInv (W := W) f hf) = (isoOfHom L W f hf).inv

Tactic:
simp only [equiv, mkInv, Equiv.symm_trans_apply, Equiv.symm_symm, homEquiv_symm_apply,
    Equiv.trans_apply, Equiv.symm_apply_apply, homEquiv_isoOfHom_inv]

Premises used: Equiv.trans_apply, Equiv.symm_apply_apply, CategoryTheory.Localization.SmallHom.equiv, Equiv.symm_symm, Equiv.symm_trans_apply, CategoryTheory.Localization.homEquiv_symm_apply, CategoryTheory.Localization.SmallHom.mkInv, CategoryTheory.Localization.homEquiv_isoOfHom_inv
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : L.IsLocalization W
X Y Z : C
inst_3 : HasSmallLocalizedHom W X Y
inst_4 : HasSmallLocalizedHom W Y Z
inst_5 : HasSmallLocalizedHom W X Z
α : SmallHom W X Y
β : SmallHom W Y Z
this_1 : Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) := ⋯
this : Small.{w, max u₁ v₁} (W.Q.obj Y ⟶ W.Q.obj Z) := ⋯
obtain :
  ∀ (α : W.Q.obj X ⟶ W.Q.obj Y),
    Eq.{v₂ + 1} (α := L.obj X ⟶ L.obj Z)
      ((equiv W L : (a : SmallHom W X Z) → L.obj X ⟶ L.obj Z)
          (comp (W := W)
            ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y) :
                (a : W.Q.obj X ⟶ W.Q.obj Y) → Shrink.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y))
              α)
            β) :
        L.obj X ⟶ L.obj Z)
      (CategoryStruct.comp (Y := L.obj Y)
          ((equiv W L : (a : SmallHom W X Y) → L.obj X ⟶ L.obj Y)
            ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y) :
                (a : W.Q.obj X ⟶ W.Q.obj Y) → Shrink.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y))
              α))
          ((equiv W L : (a : SmallHom W Y Z) → L.obj Y ⟶ L.obj Z) β) :
        L.obj X ⟶ L.obj Z)
⊢ Eq.{v₂ + 1} (α := L.obj X ⟶ L.obj Z)
    ((equiv W L : (a : SmallHom W X Z) → L.obj X ⟶ L.obj Z) (α.comp (W := W) β) : L.obj X ⟶ L.obj Z)
    (CategoryStruct.comp (Y := L.obj Y) ((equiv W L : (a : SmallHom W X Y) → L.obj X ⟶ L.obj Y) α)
        ((equiv W L : (a : SmallHom W Y Z) → L.obj Y ⟶ L.obj Z) β) :
      L.obj X ⟶ L.obj Z)

Tactic:
obtain ⟨α, rfl⟩ := (equivShrink _).surjective α

Premises used: Equiv.surjective, equivShrink, rfl
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : L.IsLocalization W
X Y Z : C
inst_3 : HasSmallLocalizedHom W X Y
inst_4 : HasSmallLocalizedHom W Y Z
inst_5 : HasSmallLocalizedHom W X Z
β : SmallHom W Y Z
this_1 : Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) := ⋯
this : Small.{w, max u₁ v₁} (W.Q.obj Y ⟶ W.Q.obj Z) := ⋯
α : W.Q.obj X ⟶ W.Q.obj Y
obtain :
  ∀ (β : W.Q.obj Y ⟶ W.Q.obj Z),
    Eq.{v₂ + 1} (α := L.obj X ⟶ L.obj Z)
      ((equiv W L : (a : SmallHom W X Z) → L.obj X ⟶ L.obj Z)
          (comp (W := W) (Y := Y)
            ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y) :
                (a : W.Q.obj X ⟶ W.Q.obj Y) → Shrink.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y))
              α)
            ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z) :
                (a : W.Q.obj Y ⟶ W.Q.obj Z) → Shrink.{w, max u₁ v₁} (W.Q.obj Y ⟶ W.Q.obj Z))
              β)) :
        L.obj X ⟶ L.obj Z)
      (CategoryStruct.comp (Y := L.obj Y)
          ((equiv W L : (a : SmallHom W X Y) → L.obj X ⟶ L.obj Y)
            ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y) :
                (a : W.Q.obj X ⟶ W.Q.obj Y) → Shrink.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y))
              α))
          ((equiv W L : (a : SmallHom W Y Z) → L.obj Y ⟶ L.obj Z)
            ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z) :
                (a : W.Q.obj Y ⟶ W.Q.obj Z) → Shrink.{w, max u₁ v₁} (W.Q.obj Y ⟶ W.Q.obj Z))
              β)) :
        L.obj X ⟶ L.obj Z)
⊢ Eq.{v₂ + 1} (α := L.obj X ⟶ L.obj Z)
    ((equiv W L : (a : SmallHom W X Z) → L.obj X ⟶ L.obj Z)
        (comp (W := W)
          ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y) :
              (a : W.Q.obj X ⟶ W.Q.obj Y) → Shrink.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y))
            α)
          β) :
      L.obj X ⟶ L.obj Z)
    (CategoryStruct.comp (Y := L.obj Y)
        ((equiv W L : (a : SmallHom W X Y) → L.obj X ⟶ L.obj Y)
          ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y) :
              (a : W.Q.obj X ⟶ W.Q.obj Y) → Shrink.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y))
            α))
        ((equiv W L : (a : SmallHom W Y Z) → L.obj Y ⟶ L.obj Z) β) :
      L.obj X ⟶ L.obj Z)

Tactic:
obtain ⟨β, rfl⟩ := (equivShrink _).surjective β

Premises used: Equiv.surjective, equivShrink, rfl
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : L.IsLocalization W
X Y Z : C
inst_3 : HasSmallLocalizedHom W X Y
inst_4 : HasSmallLocalizedHom W Y Z
inst_5 : HasSmallLocalizedHom W X Z
this_1 : Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) := ⋯
this : Small.{w, max u₁ v₁} (W.Q.obj Y ⟶ W.Q.obj Z) := ⋯
α : W.Q.obj X ⟶ W.Q.obj Y
β : W.Q.obj Y ⟶ W.Q.obj Z
⊢ Eq.{v₂ + 1} (α := L.obj X ⟶ L.obj Z)
    ((homEquiv W W.Q L : (a : W.Q.obj X ⟶ W.Q.obj Z) → L.obj X ⟶ L.obj Z)
        ((homEquiv W W.Q W.Q : (a : W.Q.obj X ⟶ W.Q.obj Z) → W.Q.obj X ⟶ W.Q.obj Z)
          (CategoryStruct.comp (Y := W.Q.obj Y)
            ((homEquiv W W.Q W.Q : (a : W.Q.obj X ⟶ W.Q.obj Y) → W.Q.obj X ⟶ W.Q.obj Y)
              ((Equiv.symm (equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) : (a : SmallHom W X Y) → W.Q.obj X ⟶ W.Q.obj Y)
                ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y) :
                    (a : W.Q.obj X ⟶ W.Q.obj Y) → Shrink.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y))
                  α)))
            ((homEquiv W W.Q W.Q : (a : W.Q.obj Y ⟶ W.Q.obj Z) → W.Q.obj Y ⟶ W.Q.obj Z)
              ((Equiv.symm (equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)) : (a : SmallHom W Y Z) → W.Q.obj Y ⟶ W.Q.obj Z)
                ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z) :
                    (a : W.Q.obj Y ⟶ W.Q.obj Z) → Shrink.{w, max u₁ v₁} (W.Q.obj Y ⟶ W.Q.obj Z))
                  β))))) :
      L.obj X ⟶ L.obj Z)
    (CategoryStruct.comp (Y := L.obj Y)
        ((homEquiv W W.Q L : (a : W.Q.obj X ⟶ W.Q.obj Y) → L.obj X ⟶ L.obj Y)
          ((Equiv.symm (equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) : (a : SmallHom W X Y) → W.Q.obj X ⟶ W.Q.obj Y)
            ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y) :
                (a : W.Q.obj X ⟶ W.Q.obj Y) → Shrink.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y))
              α)))
        ((homEquiv W W.Q L : (a : W.Q.obj Y ⟶ W.Q.obj Z) → L.obj Y ⟶ L.obj Z)
          ((Equiv.symm (equivShrink (W.Q.obj Y ⟶ W.Q.obj Z)) : (a : SmallHom W Y Z) → W.Q.obj Y ⟶ W.Q.obj Z)
            ((equivShrink (W.Q.obj Y ⟶ W.Q.obj Z) :
                (a : W.Q.obj Y ⟶ W.Q.obj Z) → Shrink.{w, max u₁ v₁} (W.Q.obj Y ⟶ W.Q.obj Z))
              β))) :
      L.obj X ⟶ L.obj Z)

Tactic:
simp only [homEquiv_refl, homEquiv_comp]

Premises used: CategoryTheory.Localization.homEquiv_comp, CategoryTheory.Localization.homEquiv_refl
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
X Y Z : C
inst_1 : HasSmallLocalizedHom W X Y
inst_2 : HasSmallLocalizedHom W Y Z
inst_3 : HasSmallLocalizedHom W X Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := W.Q.obj X ⟶ W.Q.obj Z)
    ((equiv W W.Q : (a : SmallHom W X Z) → W.Q.obj X ⟶ W.Q.obj Z) (comp (W := W) (mk W f) (mk W g)) :
      W.Q.obj X ⟶ W.Q.obj Z)
    ((equiv W W.Q : (a : SmallHom W X Z) → W.Q.obj X ⟶ W.Q.obj Z) (mk W (f ≫ g)) : W.Q.obj X ⟶ W.Q.obj Z)

Tactic:
simp [equiv_comp]

Premises used: CategoryTheory.Localization.SmallHom.equiv_comp
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
X Y : C
inst_1 : HasSmallLocalizedHom W X Y
inst_2 : HasSmallLocalizedHom W Y Y
α : SmallHom W X Y
⊢ Eq (α := W.Q.obj X ⟶ W.Q.obj Y)
    ((equiv W W.Q : (a : SmallHom W X Y) → W.Q.obj X ⟶ W.Q.obj Y) (α.comp (W := W) (mk W (𝟙 Y))) :
      W.Q.obj X ⟶ W.Q.obj Y)
    ((equiv W W.Q : (a : SmallHom W X Y) → W.Q.obj X ⟶ W.Q.obj Y) α : W.Q.obj X ⟶ W.Q.obj Y)

Tactic:
simp [equiv_comp]

Premises used: CategoryTheory.Localization.SmallHom.equiv_comp
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
X Y : C
inst_1 : HasSmallLocalizedHom W X Y
inst_2 : HasSmallLocalizedHom W X X
α : SmallHom W X Y
⊢ Eq (α := W.Q.obj X ⟶ W.Q.obj Y)
    ((equiv W W.Q : (a : SmallHom W X Y) → W.Q.obj X ⟶ W.Q.obj Y) (comp (W := W) (mk W (𝟙 X)) α) :
      W.Q.obj X ⟶ W.Q.obj Y)
    ((equiv W W.Q : (a : SmallHom W X Y) → W.Q.obj X ⟶ W.Q.obj Y) α : W.Q.obj X ⟶ W.Q.obj Y)

Tactic:
simp [equiv_comp]

Premises used: CategoryTheory.Localization.SmallHom.equiv_comp
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
X Y Z T : C
inst_1 : HasSmallLocalizedHom W X Y
inst_2 : HasSmallLocalizedHom W X Z
inst_3 : HasSmallLocalizedHom W X T
inst_4 : HasSmallLocalizedHom W Y Z
inst_5 : HasSmallLocalizedHom W Y T
inst_6 : HasSmallLocalizedHom W Z T
α : SmallHom W X Y
β : SmallHom W Y Z
γ : SmallHom W Z T
a :
  Eq (α := W.Q.obj X ⟶ W.Q.obj T)
    ((equiv W W.Q : (a : SmallHom W X T) → W.Q.obj X ⟶ W.Q.obj T) (comp (W := W) (α.comp (W := W) β) γ) :
      W.Q.obj X ⟶ W.Q.obj T)
    ((equiv W W.Q : (a : SmallHom W X T) → W.Q.obj X ⟶ W.Q.obj T) (α.comp (W := W) (β.comp (W := W) γ)) :
      W.Q.obj X ⟶ W.Q.obj T)
⊢ Eq (α := SmallHom W X T) (comp (W := W) (α.comp (W := W) β) γ) (α.comp (W := W) (β.comp (W := W) γ))

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

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Localization.SmallHom.equiv, Equiv.injective
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
X Y Z T : C
inst_1 : HasSmallLocalizedHom W X Y
inst_2 : HasSmallLocalizedHom W X Z
inst_3 : HasSmallLocalizedHom W X T
inst_4 : HasSmallLocalizedHom W Y Z
inst_5 : HasSmallLocalizedHom W Y T
inst_6 : HasSmallLocalizedHom W Z T
α : SmallHom W X Y
β : SmallHom W Y Z
γ : SmallHom W Z T
⊢ Eq (α := W.Q.obj X ⟶ W.Q.obj T)
    ((equiv W W.Q : (a : SmallHom W X T) → W.Q.obj X ⟶ W.Q.obj T) (comp (W := W) (α.comp (W := W) β) γ) :
      W.Q.obj X ⟶ W.Q.obj T)
    ((equiv W W.Q : (a : SmallHom W X T) → W.Q.obj X ⟶ W.Q.obj T) (α.comp (W := W) (β.comp (W := W) γ)) :
      W.Q.obj X ⟶ W.Q.obj T)

Tactic:
simp only [equiv_comp, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Localization.SmallHom.equiv_comp
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
X Y : C
inst_1 : HasSmallLocalizedHom W X Y
inst_2 : HasSmallLocalizedHom W Y X
inst_3 : HasSmallLocalizedHom W Y Y
f : Y ⟶ X
hf : W f
⊢ Eq (α := W.Q.obj Y ⟶ W.Q.obj Y)
    ((equiv W W.Q : (a : SmallHom W Y Y) → W.Q.obj Y ⟶ W.Q.obj Y) (comp (W := W) (mk W f) (mkInv (W := W) f hf)) :
      W.Q.obj Y ⟶ W.Q.obj Y)
    ((equiv W W.Q : (a : SmallHom W Y Y) → W.Q.obj Y ⟶ W.Q.obj Y) (mk W (𝟙 Y)) : W.Q.obj Y ⟶ W.Q.obj Y)

Tactic:
simp [equiv_comp]

Premises used: CategoryTheory.Localization.SmallHom.equiv_comp
-- Module: Mathlib.CategoryTheory.Localization.SmallHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
X Y : C
inst_1 : HasSmallLocalizedHom W X X
inst_2 : HasSmallLocalizedHom W X Y
inst_3 : HasSmallLocalizedHom W Y X
f : Y ⟶ X
hf : W f
⊢ Eq (α := W.Q.obj X ⟶ W.Q.obj X)
    ((equiv W W.Q : (a : SmallHom W X X) → W.Q.obj X ⟶ W.Q.obj X) (comp (W := W) (mkInv (W := W) f hf) (mk W f)) :
      W.Q.obj X ⟶ W.Q.obj X)
    ((equiv W W.Q : (a : SmallHom W X X) → W.Q.obj X ⟶ W.Q.obj X) (mk W (𝟙 X)) : W.Q.obj X ⟶ W.Q.obj X)

Tactic:
simp [equiv_comp]

Premises used: CategoryTheory.Localization.SmallHom.equiv_comp