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
inst_3 : HasSmallLocalizedHom W X Y
inst_4 : HasSmallLocalizedHom W X Y
e : SmallHom W X Y
obtain :
  ∀ (f : W.Q.obj X ⟶ W.Q.obj Y),
    Eq.{v₂ + 1} (α := L.obj X ⟶ L.obj Y)
      ((equiv W L : (a : SmallHom W X Y) → L.obj X ⟶ L.obj Y)
          ((chgUniv (W := W) : (a : SmallHom W X Y) → SmallHom W X Y)
            ((Equiv.symm (equiv W W.Q) : (a : W.Q.obj X ⟶ W.Q.obj Y) → SmallHom W X Y) f : SmallHom W X Y)) :
        L.obj X ⟶ L.obj Y)
      ((equiv W L : (a : SmallHom W X Y) → L.obj X ⟶ L.obj Y)
          ((Equiv.symm (equiv W W.Q) : (a : W.Q.obj X ⟶ W.Q.obj Y) → SmallHom W X Y) f) :
        L.obj X ⟶ L.obj Y)
⊢ Eq.{v₂ + 1} (α := L.obj X ⟶ L.obj Y)
    ((equiv W L : (a : SmallHom W X Y) → L.obj X ⟶ L.obj Y)
        ((chgUniv (W := W) : (a : SmallHom W X Y) → SmallHom W X Y) e) :
      L.obj X ⟶ L.obj Y)
    ((equiv W L : (a : SmallHom W X Y) → L.obj X ⟶ L.obj Y) e : L.obj X ⟶ L.obj Y)

Tactic:
obtain ⟨f, rfl⟩ := (equiv W W.Q).symm.surjective e

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Localization.SmallHom.equiv, Equiv.surjective, Equiv.symm, 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 : C
inst_3 : HasSmallLocalizedHom W X Y
inst_4 : HasSmallLocalizedHom W X Y
f : W.Q.obj X ⟶ W.Q.obj Y
⊢ Eq.{v₂ + 1} (α := L.obj X ⟶ L.obj Y)
    ((equiv W L : (a : SmallHom W X Y) → L.obj X ⟶ L.obj Y)
        ((Equiv.symm (equiv W W.Q) : (a : W.Q.obj X ⟶ W.Q.obj Y) → SmallHom W X Y)
          ((equiv W W.Q : (a : SmallHom W X Y) → W.Q.obj X ⟶ W.Q.obj Y)
              ((Equiv.symm (equiv W W.Q) : (a : W.Q.obj X ⟶ W.Q.obj Y) → SmallHom W X Y) f) :
            W.Q.obj X ⟶ W.Q.obj Y)) :
      L.obj X ⟶ L.obj Y)
    ((equiv W L : (a : SmallHom W X Y) → L.obj X ⟶ L.obj Y)
        ((Equiv.symm (equiv W W.Q) : (a : W.Q.obj X ⟶ W.Q.obj Y) → SmallHom W X Y) f) :
      L.obj X ⟶ L.obj Y)

Tactic:
simp only [Equiv.apply_symm_apply,
    equiv_equiv_symm W _ _ _ (Localization.compUniqFunctor W.Q L W)]

Premises used: Equiv.apply_symm_apply, CategoryTheory.Localization.SmallHom.equiv_equiv_symm, CategoryTheory.MorphismProperty.Q, CategoryTheory.Localization.compUniqFunctor
-- 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
inst_7 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
G : Functor.{v₃, v₄, u₃, u₄} D₁ D₂
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G
f : SmallHom W₁ X Y
obtain :
  ∀ (g : W₁.Q.obj X ⟶ W₁.Q.obj Y),
    (SmallHom.equiv W₂ L₂ :
          (a : SmallHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)) → L₂.obj (Φ.functor.obj X) ⟶ L₂.obj (Φ.functor.obj Y))
        (smallHomMap.{w, w', v₁, v₂, u₁, u₂} (W₁ := W₁) (W₂ := W₂) Φ
          ((Equiv.symm (SmallHom.equiv W₁ W₁.Q) : (a : W₁.Q.obj X ⟶ W₁.Q.obj Y) → SmallHom W₁ X Y) g)) =
      e.hom.app X ≫
        G.map
            ((SmallHom.equiv W₁ L₁ : (a : SmallHom W₁ X Y) → L₁.obj X ⟶ L₁.obj Y)
              ((Equiv.symm (SmallHom.equiv W₁ W₁.Q) : (a : W₁.Q.obj X ⟶ W₁.Q.obj Y) → SmallHom W₁ X Y) g)) ≫
          e.inv.app Y
⊢ (SmallHom.equiv W₂ L₂ :
        (a : SmallHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)) → L₂.obj (Φ.functor.obj X) ⟶ L₂.obj (Φ.functor.obj Y))
      (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) f) =
    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

Tactic:
obtain ⟨g, rfl⟩ := (SmallHom.equiv W₁ W₁.Q).symm.surjective f

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Localization.SmallHom.equiv, Equiv.surjective, Equiv.symm, rfl
-- 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
inst_7 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
G : Functor.{v₃, v₄, u₃, u₄} D₁ D₂
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G
g : W₁.Q.obj X ⟶ W₁.Q.obj Y
simp :
  (SmallHom.equiv W₂ L₂ :
        (a : SmallHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)) → L₂.obj (Φ.functor.obj X) ⟶ L₂.obj (Φ.functor.obj Y))
      ((Equiv.symm (SmallHom.equiv W₂ W₂.Q) :
          (a : W₂.Q.obj (Φ.functor.obj X) ⟶ W₂.Q.obj (Φ.functor.obj Y)) →
            SmallHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y))
        ((Iso.homCongr
                (Iso.app
                  (Iso.symm
                    (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q
                      (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))
                  X)
                (Iso.app
                  (Iso.symm
                    (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q
                      (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))
                  Y) :
              (a : (W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q).obj X ⟶ (W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q).obj Y) →
                (Φ.functor ⋙ W₂.Q).obj X ⟶ (Φ.functor ⋙ W₂.Q).obj Y)
            ((Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).map g) :
          (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q).obj X ⟶ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q).obj Y)) =
    e.hom.app X ≫
      G.map
          ((SmallHom.equiv W₁ L₁ : (a : SmallHom W₁ X Y) → L₁.obj X ⟶ L₁.obj Y)
            ((Equiv.symm (SmallHom.equiv W₁ W₁.Q) : (a : W₁.Q.obj X ⟶ W₁.Q.obj Y) → SmallHom W₁ X Y) g)) ≫
        e.inv.app Y
⊢ (SmallHom.equiv W₂ L₂ :
        (a : SmallHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)) → L₂.obj (Φ.functor.obj X) ⟶ L₂.obj (Φ.functor.obj Y))
      (smallHomMap.{w, w', v₁, v₂, u₁, u₂} (W₁ := W₁) (W₂ := W₂) Φ
        ((Equiv.symm (SmallHom.equiv W₁ W₁.Q) : (a : W₁.Q.obj X ⟶ W₁.Q.obj Y) → SmallHom W₁ X Y) g)) =
    e.hom.app X ≫
      G.map
          ((SmallHom.equiv W₁ L₁ : (a : SmallHom W₁ X Y) → L₁.obj X ⟶ L₁.obj Y)
            ((Equiv.symm (SmallHom.equiv W₁ W₁.Q) : (a : W₁.Q.obj X ⟶ W₁.Q.obj Y) → SmallHom W₁ X Y) g)) ≫
        e.inv.app Y

Tactic:
simp only [smallHomMap, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, 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₂
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
inst_7 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
G : Functor.{v₃, v₄, u₃, u₄} D₁ D₂
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G
g : W₁.Q.obj X ⟶ W₁.Q.obj Y
G' : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
β : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ G' := CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q G'
E₁ : W₁.Localization ⥤ D₁ := (uniq W₁.Q L₁ W₁).functor
α₁ : W₁.Q ⋙ E₁ ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁
E₂ : W₂.Localization ⥤ D₂ := (uniq W₂.Q L₂ W₂).functor
α₂ : W₂.Q ⋙ E₂ ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂
change :
  α₂.inv.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ≫
      E₂.map (β.hom.app X ≫ G'.map g ≫ β.inv.app Y) ≫ α₂.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) =
    e.hom.app X ≫ G.map (α₁.inv.app X ≫ E₁.map g ≫ α₁.hom.app Y) ≫ e.inv.app Y
⊢ α₂.inv.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ≫
      E₂.map
          ((Iso.homCongr
                (Iso.app
                  (Iso.symm
                    (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q
                      (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))
                  X)
                (Iso.app
                  (Iso.symm
                    (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q
                      (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))
                  Y) :
              (a : (W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q).obj X ⟶ (W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q).obj Y) →
                (Φ.functor ⋙ W₂.Q).obj X ⟶ (Φ.functor ⋙ W₂.Q).obj Y)
            ((Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).map g)) ≫
        α₂.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) =
    e.hom.app X ≫ G.map (α₁.inv.app X ≫ E₁.map g ≫ α₁.hom.app Y) ≫ e.inv.app Y

Tactic:
change α₂.inv.app _ ≫ E₂.map (β.hom.app X ≫ G'.map g ≫ β.inv.app Y) ≫ _ = _

Premises used: CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app
-- 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_1 Y : C₁
inst_6 : HasSmallLocalizedHom W₁ X_1 Y
inst_7 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X_1) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
G : Functor.{v₃, v₄, u₃, u₄} D₁ D₂
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G
g : W₁.Q.obj X_1 ⟶ W₁.Q.obj Y
G' : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
β : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ G' := CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q G'
E₁ : W₁.Localization ⥤ D₁ := (uniq W₁.Q L₁ W₁).functor
α₁ : W₁.Q ⋙ E₁ ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁
E₂ : W₂.Localization ⥤ D₂ := (uniq W₂.Q L₂ W₂).functor
α₂ : W₂.Q ⋙ E₂ ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂
γ : G' ⋙ E₂ ≅ E₁ ⋙ G :=
  liftNatIso W₁.Q W₁ (W₁.Q ⋙ G' ⋙ E₂) (W₁.Q ⋙ E₁ ⋙ G) (G' ⋙ E₂) (E₁ ⋙ G)
    ((W₁.Q.associator G' E₂).symm ≪≫
      Functor.isoWhiskerRight β.symm E₂ ≪≫
        Φ.functor (W₁ := W₁) (W₂ := W₂).associator W₂.Q E₂ ≪≫
          Φ.functor (W₁ := W₁) (W₂ := W₂).isoWhiskerLeft α₂ ≪≫
            e ≪≫ Functor.isoWhiskerRight α₁.symm G ≪≫ W₁.Q.associator E₁ G)
X : C₁
⊢ γ.hom.app (W₁.Q.obj X) =
    E₂.map (β.inv.app X) ≫ α₂.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ≫ e.hom.app X ≫ G.map (α₁.inv.app X)

Tactic:
simp [γ, id_comp, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- 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
inst_7 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
G : Functor.{v₃, v₄, u₃, u₄} D₁ D₂
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G
g : W₁.Q.obj X ⟶ W₁.Q.obj Y
G' : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
β : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ G' := CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q G'
E₁ : W₁.Localization ⥤ D₁ := (uniq W₁.Q L₁ W₁).functor
α₁ : W₁.Q ⋙ E₁ ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁
E₂ : W₂.Localization ⥤ D₂ := (uniq W₂.Q L₂ W₂).functor
α₂ : W₂.Q ⋙ E₂ ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂
γ : G' ⋙ E₂ ≅ E₁ ⋙ G :=
  liftNatIso W₁.Q W₁ (W₁.Q ⋙ G' ⋙ E₂) (W₁.Q ⋙ E₁ ⋙ G) (G' ⋙ E₂) (E₁ ⋙ G)
    ((W₁.Q.associator G' E₂).symm ≪≫
      Functor.isoWhiskerRight β.symm E₂ ≪≫
        Φ.functor (W₁ := W₁) (W₂ := W₂).associator W₂.Q E₂ ≪≫
          Φ.functor (W₁ := W₁) (W₂ := W₂).isoWhiskerLeft α₂ ≪≫
            e ≪≫ Functor.isoWhiskerRight α₁.symm G ≪≫ W₁.Q.associator E₁ G)
⊢ ∀ (X : C₁),
    γ.hom.app (W₁.Q.obj X) =
      E₂.map (β.inv.app X) ≫ α₂.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ≫ e.hom.app X ≫ G.map (α₁.inv.app X)

Tactic:
have hγ : ∀ (X : C₁), γ.hom.app (W₁.Q.obj X) =
      E₂.map (β.inv.app X) ≫ α₂.hom.app (Φ.functor.obj X) ≫
        e.hom.app X ≫ G.map (α₁.inv.app X) := fun X ↦ by
    simp [γ, id_comp, comp_id]
-- 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
inst_7 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
G : Functor.{v₃, v₄, u₃, u₄} D₁ D₂
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G
g : W₁.Q.obj X ⟶ W₁.Q.obj Y
G' : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
β : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ G' := CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q G'
E₁ : W₁.Localization ⥤ D₁ := (uniq W₁.Q L₁ W₁).functor
α₁ : W₁.Q ⋙ E₁ ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁
E₂ : W₂.Localization ⥤ D₂ := (uniq W₂.Q L₂ W₂).functor
α₂ : W₂.Q ⋙ E₂ ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂
γ : G' ⋙ E₂ ≅ E₁ ⋙ G :=
  liftNatIso W₁.Q W₁ (W₁.Q ⋙ G' ⋙ E₂) (W₁.Q ⋙ E₁ ⋙ G) (G' ⋙ E₂) (E₁ ⋙ G)
    ((W₁.Q.associator G' E₂).symm ≪≫
      Functor.isoWhiskerRight β.symm E₂ ≪≫
        Φ.functor (W₁ := W₁) (W₂ := W₂).associator W₂.Q E₂ ≪≫
          Φ.functor (W₁ := W₁) (W₂ := W₂).isoWhiskerLeft α₂ ≪≫
            e ≪≫ Functor.isoWhiskerRight α₁.symm G ≪≫ W₁.Q.associator E₁ G)
hγ :
  ∀ (X : C₁),
    γ.hom.app (W₁.Q.obj X) =
      E₂.map (β.inv.app X) ≫ α₂.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ≫ e.hom.app X ≫ G.map (α₁.inv.app X)
⊢ γ.hom.app (W₁.Q.obj X) ≫
      G.map (α₁.hom.app X) ≫
        e.inv.app X ≫
          α₂.inv.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ≫
            E₂.map (β.hom.app X) ≫
              (G' ⋙ E₂).map g ≫ E₂.map (β.inv.app Y) ≫ α₂.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) =
    (G' ⋙ E₂).map g ≫ γ.hom.app (W₁.Q.obj Y) ≫ G.map (α₁.hom.app Y) ≫ e.inv.app Y

Tactic:
simp only [hγ, assoc, ← Functor.map_comp_assoc, Iso.inv_hom_id_app,
    Functor.map_id, id_comp, Iso.hom_inv_id_app_assoc,
    Iso.hom_inv_id_app, Functor.comp_obj, comp_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Iso.hom_inv_id_app_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Category.id_comp
-- 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
inst_3 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
f : X ⟶ Y
a :
  Eq (α := W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ⟶ W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y))
    ((SmallHom.equiv W₂ W₂.Q :
          (a : SmallHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)) →
            W₂.Q.obj (Φ.functor.obj X) ⟶ W₂.Q.obj (Φ.functor.obj Y))
        (smallHomMap.{w, w', v₁, v₂, u₁, u₂} (W₁ := W₁) (W₂ := W₂) Φ (SmallHom.mk W₁ f)) :
      W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ⟶ W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y))
    ((SmallHom.equiv W₂ W₂.Q :
          (a : SmallHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)) →
            W₂.Q.obj (Φ.functor.obj X) ⟶ W₂.Q.obj (Φ.functor.obj Y))
        (SmallHom.mk W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).map f)) :
      W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ⟶ W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y))
⊢ Eq.{w' + 1} (α := SmallHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y))
    (smallHomMap.{w, w', v₁, v₂, u₁, u₂} (W₁ := W₁) (W₂ := W₂) Φ (SmallHom.mk W₁ f))
    (SmallHom.mk W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).map f))

Tactic:
apply (SmallHom.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₁
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
inst_3 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
f : X ⟶ Y
⊢ Eq (α := W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ⟶ W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y))
    ((SmallHom.equiv W₂ W₂.Q :
          (a : SmallHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)) →
            W₂.Q.obj (Φ.functor.obj X) ⟶ W₂.Q.obj (Φ.functor.obj Y))
        (smallHomMap.{w, w', v₁, v₂, u₁, u₂} (W₁ := W₁) (W₂ := W₂) Φ (SmallHom.mk W₁ f)) :
      W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ⟶ W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y))
    ((SmallHom.equiv W₂ W₂.Q :
          (a : SmallHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)) →
            W₂.Q.obj (Φ.functor.obj X) ⟶ W₂.Q.obj (Φ.functor.obj Y))
        (SmallHom.mk W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).map f)) :
      W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ⟶ W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y))

Tactic:
simp [Φ.equiv_smallHomMap W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q) (CatCommSq.iso _ _ _ _)]

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.CatCommSq.iso, CategoryTheory.LocalizerMorphism.equiv_smallHomMap, CategoryTheory.LocalizerMorphism.localizedFunctor
-- 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
inst_5 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
inst_6 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z)
inst_7 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z)
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
a :
  Eq (α := W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ⟶ W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z))
    ((SmallHom.equiv W₂ W₂.Q :
          (a : SmallHom W₂ (Φ.functor.obj X) (Φ.functor.obj Z)) →
            W₂.Q.obj (Φ.functor.obj X) ⟶ W₂.Q.obj (Φ.functor.obj Z))
        (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) (f.comp (W := W₁) g)) :
      W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ⟶ W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z))
    ((SmallHom.equiv W₂ W₂.Q :
          (a : SmallHom W₂ (Φ.functor.obj X) (Φ.functor.obj Z)) →
            W₂.Q.obj (Φ.functor.obj X) ⟶ W₂.Q.obj (Φ.functor.obj Z))
        (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) f) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g)) :
      W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ⟶ W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z))
⊢ Eq.{w' + 1} (α := SmallHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z))
    (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) (f.comp (W := W₁) g))
    (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) f) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g))

Tactic:
apply (SmallHom.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₁
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
inst_5 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
inst_6 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z)
inst_7 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z)
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
⊢ Eq (α := W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ⟶ W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z))
    ((SmallHom.equiv W₂ W₂.Q :
          (a : SmallHom W₂ (Φ.functor.obj X) (Φ.functor.obj Z)) →
            W₂.Q.obj (Φ.functor.obj X) ⟶ W₂.Q.obj (Φ.functor.obj Z))
        (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) (f.comp (W := W₁) g)) :
      W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ⟶ W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z))
    ((SmallHom.equiv W₂ W₂.Q :
          (a : SmallHom W₂ (Φ.functor.obj X) (Φ.functor.obj Z)) →
            W₂.Q.obj (Φ.functor.obj X) ⟶ W₂.Q.obj (Φ.functor.obj Z))
        (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) f) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g)) :
      W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ⟶ W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z))

Tactic:
simp [Φ.equiv_smallHomMap W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q) (CatCommSq.iso _ _ _ _),
    SmallHom.equiv_comp]

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.CatCommSq.iso, CategoryTheory.Localization.SmallHom.equiv_comp, CategoryTheory.LocalizerMorphism.equiv_smallHomMap, CategoryTheory.LocalizerMorphism.localizedFunctor
-- 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
⊢ HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Y'

Tactic:
have := hasSmallLocalizedHom_of_isos.{w'} W₂ eY.symm (Iso.refl Y')