awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} D₁
inst_4 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
W₃ : MorphismProperty.{v₃, u₃} C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
inst_5 : L₁.IsLocalization W₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_6 : L₂.IsLocalization W₂
G : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
inst_7 : Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)
⊢ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).IsLocalization W₁

Tactic:
Functor.IsLocalization.of_iso _ ((Φ.catCommSq W₁.Q L₂).iso).symm

Premises used: CategoryTheory.CatCommSq.iso, CategoryTheory.Functor.IsLocalization.of_iso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₁
ε₁ : 𝟭 C₁ ⟶ Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ Ψ.functor (W₁ := W₂) (W₂ := W₁)
ε₂ : 𝟭 C₂ ⟶ Ψ.functor (W₁ := W₂) (W₂ := W₁) ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hε₁ : ∀ (X₁ : C₁), W₁ (ε₁.app X₁)
hε₂ : ∀ (X₂ : C₂), W₂ (ε₂.app X₂)
rw : ∀ (X : C₁), IsIso ((whiskerRight ε₁ W₁.Q).app X)
⊢ IsIso (whiskerRight ε₁ W₁.Q)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₁
ε₁ : 𝟭 C₁ ⟶ Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ Ψ.functor (W₁ := W₂) (W₂ := W₁)
ε₂ : 𝟭 C₂ ⟶ Ψ.functor (W₁ := W₂) (W₂ := W₁) ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hε₁ : ∀ (X₁ : C₁), W₁ (ε₁.app X₁)
hε₂ : ∀ (X₂ : C₂), W₂ (ε₂.app X₂)
⊢ ∀ (X : C₁), IsIso ((whiskerRight ε₁ W₁.Q).app X)

Tactic:
fun _ ↦ Localization.inverts W₁.Q W₁ _ (hε₁ _)

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Localization.inverts, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₁
ε₁ : 𝟭 C₁ ⟶ Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ Ψ.functor (W₁ := W₂) (W₂ := W₁)
ε₂ : 𝟭 C₂ ⟶ Ψ.functor (W₁ := W₂) (W₂ := W₁) ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hε₁ : ∀ (X₁ : C₁), W₁ (ε₁.app X₁)
hε₂ : ∀ (X₂ : C₂), W₂ (ε₂.app X₂)
⊢ ∀ (X : C₁), IsIso ((whiskerRight ε₁ W₁.Q).app X)

Tactic:
exact fun _ ↦ Localization.inverts W₁.Q W₁ _ (hε₁ _)

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Localization.inverts, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₁
ε₁ : 𝟭 C₁ ⟶ Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ Ψ.functor (W₁ := W₂) (W₂ := W₁)
ε₂ : 𝟭 C₂ ⟶ Ψ.functor (W₁ := W₂) (W₂ := W₁) ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hε₁ : ∀ (X₁ : C₁), W₁ (ε₁.app X₁)
hε₂ : ∀ (X₂ : C₂), W₂ (ε₂.app X₂)
⊢ IsIso (whiskerRight ε₁ W₁.Q)

Tactic:
have : IsIso (whiskerRight ε₁ W₁.Q) := by
      rw [NatTrans.isIso_iff_isIso_app]
      exact fun _ ↦ Localization.inverts W₁.Q W₁ _ (hε₁ _)
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₁
ε₁ : 𝟭 C₁ ⟶ Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ Ψ.functor (W₁ := W₂) (W₂ := W₁)
ε₂ : 𝟭 C₂ ⟶ Ψ.functor (W₁ := W₂) (W₂ := W₁) ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hε₁ : ∀ (X₁ : C₁), W₁ (ε₁.app X₁)
hε₂ : ∀ (X₂ : C₂), W₂ (ε₂.app X₂)
this : IsIso (whiskerRight ε₁ W₁.Q)
rw : ∀ (X : C₂), IsIso ((whiskerRight ε₂ W₂.Q).app X)
⊢ IsIso (whiskerRight ε₂ W₂.Q)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₁
ε₁ : 𝟭 C₁ ⟶ Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ Ψ.functor (W₁ := W₂) (W₂ := W₁)
ε₂ : 𝟭 C₂ ⟶ Ψ.functor (W₁ := W₂) (W₂ := W₁) ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hε₁ : ∀ (X₁ : C₁), W₁ (ε₁.app X₁)
hε₂ : ∀ (X₂ : C₂), W₂ (ε₂.app X₂)
this : IsIso (whiskerRight ε₁ W₁.Q)
⊢ ∀ (X : C₂), IsIso ((whiskerRight ε₂ W₂.Q).app X)

Tactic:
fun _ ↦ Localization.inverts W₂.Q W₂ _ (hε₂ _)

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Localization.inverts, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₁
ε₁ : 𝟭 C₁ ⟶ Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ Ψ.functor (W₁ := W₂) (W₂ := W₁)
ε₂ : 𝟭 C₂ ⟶ Ψ.functor (W₁ := W₂) (W₂ := W₁) ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hε₁ : ∀ (X₁ : C₁), W₁ (ε₁.app X₁)
hε₂ : ∀ (X₂ : C₂), W₂ (ε₂.app X₂)
this : IsIso (whiskerRight ε₁ W₁.Q)
⊢ ∀ (X : C₂), IsIso ((whiskerRight ε₂ W₂.Q).app X)

Tactic:
exact fun _ ↦ Localization.inverts W₂.Q W₂ _ (hε₂ _)

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Localization.inverts, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₁
ε₁ : 𝟭 C₁ ⟶ Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ Ψ.functor (W₁ := W₂) (W₂ := W₁)
ε₂ : 𝟭 C₂ ⟶ Ψ.functor (W₁ := W₂) (W₂ := W₁) ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hε₁ : ∀ (X₁ : C₁), W₁ (ε₁.app X₁)
hε₂ : ∀ (X₂ : C₂), W₂ (ε₂.app X₂)
this : IsIso (whiskerRight ε₁ W₁.Q)
⊢ IsIso (whiskerRight ε₂ W₂.Q)

Tactic:
have : IsIso (whiskerRight ε₂ W₂.Q) := by
      rw [NatTrans.isIso_iff_isIso_app]
      exact fun _ ↦ Localization.inverts W₂.Q W₂ _ (hε₂ _)
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₁
ε₁ : 𝟭 C₁ ⟶ Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ Ψ.functor (W₁ := W₂) (W₂ := W₁)
ε₂ : 𝟭 C₂ ⟶ Ψ.functor (W₁ := W₂) (W₂ := W₁) ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hε₁ : ∀ (X₁ : C₁), W₁ (ε₁.app X₁)
hε₂ : ∀ (X₂ : C₂), W₂ (ε₂.app X₂)
this_1 : IsIso (whiskerRight ε₁ W₁.Q)
this : IsIso (whiskerRight ε₂ W₂.Q)
⊢ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).IsEquivalence

Tactic:
(Localization.equivalence W₁.Q W₁ W₂.Q W₂ (Φ.functor ⋙ W₂.Q)
      (Φ.localizedFunctor W₁.Q W₂.Q)
      (Ψ.functor ⋙ W₁.Q) (Ψ.localizedFunctor W₂.Q W₁.Q) ?_ ?_).isEquivalence_functor

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.comp, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.Functor.objPreimage, CategoryTheory.Equivalence.isEquivalence_functor, Classical.choose, CategoryTheory.Localization.equivalence, CategoryTheory.LocalizerMorphism.localizedFunctor, CategoryTheory.Localization.lift, CategoryTheory.Functor.essImage.witness
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₁
ε₁ : 𝟭 C₁ ⟶ Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ Ψ.functor (W₁ := W₂) (W₂ := W₁)
ε₂ : 𝟭 C₂ ⟶ Ψ.functor (W₁ := W₂) (W₂ := W₁) ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hε₁ : ∀ (X₁ : C₁), W₁ (ε₁.app X₁)
hε₂ : ∀ (X₂ : C₂), W₂ (ε₂.app X₂)
this_1 : IsIso (whiskerRight ε₁ W₁.Q)
this : IsIso (whiskerRight ε₂ W₂.Q)
refine_1 : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q) ⋙ Ψ.localizedFunctor (W₁ := W₂) (W₂ := W₁) W₂.Q W₁.Q ≅ W₁.Q
refine_2 : (Ψ.functor (W₁ := W₂) (W₂ := W₁) ⋙ W₁.Q) ⋙ Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q ≅ W₂.Q
⊢ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).IsEquivalence

Tactic:
refine (Localization.equivalence W₁.Q W₁ W₂.Q W₂ (Φ.functor ⋙ W₂.Q)
      (Φ.localizedFunctor W₁.Q W₂.Q)
      (Ψ.functor ⋙ W₁.Q) (Ψ.localizedFunctor W₂.Q W₁.Q) ?_ ?_).isEquivalence_functor

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.comp, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.Equivalence.isEquivalence_functor, CategoryTheory.Localization.equivalence, CategoryTheory.LocalizerMorphism.localizedFunctor
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₁
ε₁ : 𝟭 C₁ ⟶ Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ Ψ.functor (W₁ := W₂) (W₂ := W₁)
ε₂ : 𝟭 C₂ ⟶ Ψ.functor (W₁ := W₂) (W₂ := W₁) ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hε₁ : ∀ (X₁ : C₁), W₁ (ε₁.app X₁)
hε₂ : ∀ (X₂ : C₂), W₂ (ε₂.app X₂)
this_1 : IsIso (whiskerRight ε₁ W₁.Q)
this : IsIso (whiskerRight ε₂ W₂.Q)
⊢ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q) ⋙ Ψ.localizedFunctor (W₁ := W₂) (W₂ := W₁) W₂.Q W₁.Q ≅ W₁.Q

Tactic:
exact Functor.associator _ _ _ ≪≫
        isoWhiskerLeft _ (CatCommSq.iso Ψ.functor W₂.Q W₁.Q _).symm ≪≫
        (Functor.associator _ _ _).symm ≪≫
        (asIso (whiskerRight ε₁ W₁.Q)).symm ≪≫ Functor.leftUnitor _

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.associator, CategoryTheory.CatCommSq.iso, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Functor.whiskerRight, CategoryTheory.Functor.leftUnitor, CategoryTheory.Iso.symm, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₁
ε₁ : 𝟭 C₁ ⟶ Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ Ψ.functor (W₁ := W₂) (W₂ := W₁)
ε₂ : 𝟭 C₂ ⟶ Ψ.functor (W₁ := W₂) (W₂ := W₁) ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hε₁ : ∀ (X₁ : C₁), W₁ (ε₁.app X₁)
hε₂ : ∀ (X₂ : C₂), W₂ (ε₂.app X₂)
this_1 : IsIso (whiskerRight ε₁ W₁.Q)
this : IsIso (whiskerRight ε₂ W₂.Q)
⊢ (Ψ.functor (W₁ := W₂) (W₂ := W₁) ⋙ W₁.Q) ⋙ Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q ≅ W₂.Q

Tactic:
exact Functor.associator _ _ _ ≪≫
        isoWhiskerLeft _ (CatCommSq.iso Φ.functor W₁.Q W₂.Q _).symm ≪≫
        (Functor.associator _ _ _).symm ≪≫
        (asIso (whiskerRight ε₂ W₂.Q)).symm ≪≫ Functor.leftUnitor _

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.associator, CategoryTheory.CatCommSq.iso, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Functor.whiskerRight, CategoryTheory.Functor.leftUnitor, CategoryTheory.Iso.symm, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} D₁
inst_4 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
W₃ : MorphismProperty.{v₃, u₃} C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
inst_5 : L₁.IsLocalization W₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_6 : L₂.IsLocalization W₂
G : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
⊢ (LocalizerMorphism.id W₁).IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₁)

Tactic:
have : ((LocalizerMorphism.id W₁).functor ⋙ W₁.Q).IsLocalization W₁ :=
    Functor.IsLocalization.of_iso _ (Functor.leftUnitor _).symm
  of_isLocalization_of_isLocalization _ W₁.Q

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.IsLocalization.of_iso, CategoryTheory.Functor.leftUnitor, CategoryTheory.LocalizerMorphism.id, CategoryTheory.Iso.symm, CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.of_isLocalization_of_isLocalization
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} D₁
inst_4 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
W₃ : MorphismProperty.{v₃, u₃} C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
inst_5 : L₁.IsLocalization W₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_6 : L₂.IsLocalization W₂
G : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
inst_7 : Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)
Ψ : LocalizerMorphism W₂ W₃
inst_8 : Ψ.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₃)
⊢ (Φ.comp (W₁ := W₁) (W₂ := W₂) (W₃ := W₃) Ψ).IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₃)

Tactic:
have : ((Φ.comp Ψ).functor ⋙ W₃.Q).IsLocalization W₁ :=
    Functor.IsLocalization.of_iso _ (Functor.associator _ _ _).symm
  of_isLocalization_of_isLocalization _ W₃.Q

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.associator, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.Functor.IsLocalization.of_iso, CategoryTheory.Iso.symm, CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.of_isLocalization_of_isLocalization, CategoryTheory.LocalizerMorphism.comp
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₄, u₄} D₁
inst_3 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : 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₂
G : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
inst_6 : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ G
hG : G.FullyFaithful
rw : Nonempty G.FullyFaithful
⊢ Nonempty (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).FullyFaithful

Tactic:
rw [Φ.nonempty_fullyFaithful_iff W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q) L₁ L₂ G]

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.LocalizerMorphism.nonempty_fullyFaithful_iff, CategoryTheory.LocalizerMorphism.localizedFunctor
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₄, u₄} D₁
inst_3 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : 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₂
G : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
inst_6 : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ G
hG : G.FullyFaithful
⊢ Nonempty G.FullyFaithful

Tactic:
⟨hG⟩

Premises used: Nonempty.intro
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₄, u₄} D₁
inst_3 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : 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₂
G : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
inst_6 : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ G
hG : G.FullyFaithful
⊢ Nonempty G.FullyFaithful

Tactic:
exact ⟨hG⟩
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} D₁
inst_4 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
W₃ : MorphismProperty.{v₃, u₃} C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
inst_5 : L₁.IsLocalization W₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_6 : L₂.IsLocalization W₂
G : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
h : Φ.IsLocalizedFullyFaithful (W₁ := W₁) (W₂ := W₂)
inst_7 : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ G
rw : Nonempty (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).FullyFaithful
⊢ Nonempty G.FullyFaithful

Tactic:
rw [Φ.nonempty_fullyFaithful_iff L₁ L₂ G W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)]

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.LocalizerMorphism.nonempty_fullyFaithful_iff, CategoryTheory.LocalizerMorphism.localizedFunctor
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} D₁
inst_4 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
W₃ : MorphismProperty.{v₃, u₃} C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
inst_5 : L₁.IsLocalization W₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_6 : L₂.IsLocalization W₂
G : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
h : Φ.IsLocalizedFullyFaithful (W₁ := W₁) (W₂ := W₂)
inst_7 : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ G
⊢ Nonempty (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).FullyFaithful

Tactic:
h.nonempty_fullyFaithful

Premises used: CategoryTheory.LocalizerMorphism.IsLocalizedFullyFaithful.nonempty_fullyFaithful
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} D₁
inst_4 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
W₃ : MorphismProperty.{v₃, u₃} C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
inst_5 : L₁.IsLocalization W₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_6 : L₂.IsLocalization W₂
G : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
h : Φ.IsLocalizedFullyFaithful (W₁ := W₁) (W₂ := W₂)
inst_7 : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ G
⊢ Nonempty (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).FullyFaithful

Tactic:
exact h.nonempty_fullyFaithful

Premises used: CategoryTheory.LocalizerMorphism.IsLocalizedFullyFaithful.nonempty_fullyFaithful
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₄, u₄} D₁
inst_3 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : 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₂
G : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
inst_6 : Φ.IsLocalizedFullyFaithful (W₁ := W₁) (W₂ := W₂)
inst_7 : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ G
⊢ G.Faithful

Tactic:
(Φ.fullyFaithful L₁ L₂ G).faithful

Premises used: CategoryTheory.LocalizerMorphism.fullyFaithful, CategoryTheory.Functor.FullyFaithful.faithful
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₄, u₄} D₁
inst_3 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : 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₂
G : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
inst_6 : Φ.IsLocalizedFullyFaithful (W₁ := W₁) (W₂ := W₂)
inst_7 : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ G
⊢ G.Full

Tactic:
(Φ.fullyFaithful L₁ L₂ G).full

Premises used: CategoryTheory.LocalizerMorphism.fullyFaithful, CategoryTheory.Functor.FullyFaithful.full
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} D₁
inst_4 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
W₃ : MorphismProperty.{v₃, u₃} C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
inst_5 : L₁.IsLocalization W₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_6 : L₂.IsLocalization W₂
G : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
inst_7 : Φ.IsLocalizedFullyFaithful (W₁ := W₁) (W₂ := W₂)
⊢ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂).Full

Tactic:
Φ.full L₁ L₂ _

Premises used: CategoryTheory.LocalizerMorphism.full
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} D₁
inst_4 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
W₃ : MorphismProperty.{v₃, u₃} C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
inst_5 : L₁.IsLocalization W₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_6 : L₂.IsLocalization W₂
G : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
inst_7 : Φ.IsLocalizedFullyFaithful (W₁ := W₁) (W₂ := W₂)
⊢ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂).Faithful

Tactic:
Φ.faithful L₁ L₂ _

Premises used: CategoryTheory.LocalizerMorphism.faithful
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} D₁
inst_4 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
W₃ : MorphismProperty.{v₃, u₃} C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
inst_5 : L₁.IsLocalization W₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_6 : L₂.IsLocalization W₂
G_1 : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
inst_7 : Φ.IsLocalizedFullyFaithful (W₁ := W₁) (W₂ := W₂)
G : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
this : CatCommSq (Φ.op (W₁ := W₁) (W₂ := W₂).functor (W₁ := W₁.op) (W₂ := W₂.op)) W₁.Q.op W₂.Q.op G.op :=
  { iso := NatIso.op (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q G).symm }
⊢ Φ.op (W₁ := W₁) (W₂ := W₂).IsLocalizedFullyFaithful (W₁ := W₁.op) (W₂ := W₂.op)

Tactic:
IsLocalizedFullyFaithful.mk' Φ.op W₁.Q.op W₂.Q.op G.op
    (Φ.fullyFaithful W₁.Q W₂.Q G).op

Premises used: CategoryTheory.Functor.op, CategoryTheory.LocalizerMorphism.IsLocalizedFullyFaithful.mk', CategoryTheory.LocalizerMorphism.fullyFaithful, CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.FullyFaithful.op, CategoryTheory.LocalizerMorphism.op