awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : 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_3 : L₂.IsLocalization W₂
⊢ W₁.IsInvertedBy (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂)

Tactic:
fun _ _ _ hf => Localization.inverts L₂ W₂ _ (Φ.map _ hf)

Premises used: CategoryTheory.LocalizerMorphism.functor, CategoryTheory.MorphismProperty.IsInvertedBy, CategoryTheory.Functor.map, CategoryTheory.LocalizerMorphism.map, CategoryTheory.Localization.inverts
-- 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
D₁' : Type u₄'
D₂' : Type u₅'
inst_7 : Category.{v₄', u₄'} D₁'
inst_8 : Category.{v₅', u₅'} D₂'
L₁' : Functor.{v₁, v₄', u₁, u₄'} C₁ D₁'
L₂' : Functor.{v₂, v₅', u₂, u₅'} C₂ D₂'
inst_9 : L₁'.IsLocalization W₁
inst_10 : L₂'.IsLocalization W₂
G' : Functor.{v₄', v₅', u₄', u₅'} D₁' D₂'
inst_11 : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁' L₂' G'
inst_12 : G.IsEquivalence
⊢ G'.IsEquivalence

Tactic:
let E₁ := Localization.uniq L₁ L₁' W₁
  let E₂ := Localization.uniq L₂ L₂' W₂
  let e : L₁ ⋙ G ⋙ E₂.functor ≅ L₁ ⋙ E₁.functor ⋙ G' :=
    calc
      L₁ ⋙ G ⋙ E₂.functor ≅ Φ.functor ⋙ L₂ ⋙ E₂.functor :=
          (associator _ _ _).symm ≪≫
            isoWhiskerRight (CatCommSq.iso Φ.functor L₁ L₂ G).symm E₂.functor ≪≫
            associator _ _ _
      _ ≅ Φ.functor ⋙ L₂' := isoWhiskerLeft Φ.functor (compUniqFunctor L₂ L₂' W₂)
      _ ≅ L₁' ⋙ G' := CatCommSq.iso Φ.functor L₁' L₂' G'
      _ ≅ L₁ ⋙ E₁.functor ⋙ G' :=
            isoWhiskerRight (compUniqFunctor L₁ L₁' W₁).symm G' ≪≫ associator _ _ _
  have := Functor.isEquivalence_of_iso
    (liftNatIso L₁ W₁ _ _ (G ⋙ E₂.functor) (E₁.functor ⋙ G') e)
  Functor.isEquivalence_of_comp_left E₁.functor G'

Premises used: CategoryTheory.Localization.liftNatIso, CategoryTheory.Functor.isEquivalence_of_comp_left, Trans.trans, CategoryTheory.Functor.comp, CategoryTheory.Functor.isEquivalence_of_iso, CategoryTheory.Functor.associator, CategoryTheory.Localization.uniq, CategoryTheory.Equivalence.functor, CategoryTheory.CatCommSq.iso, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.Localization.compUniqFunctor, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.Functor.isoWhiskerRight
-- 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
D₁' : Type u₄'
D₂' : Type u₅'
inst_7 : Category.{v₄', u₄'} D₁'
inst_8 : Category.{v₅', u₅'} D₂'
L₁' : Functor.{v₁, v₄', u₁, u₄'} C₁ D₁'
L₂' : Functor.{v₂, v₅', u₂, u₅'} C₂ D₂'
inst_9 : L₁'.IsLocalization W₁
inst_10 : L₂'.IsLocalization W₂
G' : Functor.{v₄', v₅', u₄', u₅'} D₁' D₂'
inst_11 : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁' L₂' G'
⊢ G.IsEquivalence ↔ G'.IsEquivalence

Tactic:
⟨fun _ => Φ.isEquivalence_imp L₁ L₂ G L₁' L₂' G',
    fun _ => Φ.isEquivalence_imp L₁' L₂' G' L₁ L₂ G⟩

Premises used: CategoryTheory.LocalizerMorphism.isEquivalence_imp, Iff.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
D₁' : Type u₄'
D₂' : Type u₅'
inst_7 : Category.{v₄', u₄'} D₁'
inst_8 : Category.{v₅', u₅'} D₂'
L₁' : Functor.{v₁, v₄', u₁, u₄'} C₁ D₁'
L₂' : Functor.{v₂, v₅', u₂, u₅'} C₂ D₂'
inst_9 : L₁'.IsLocalization W₁
inst_10 : L₂'.IsLocalization W₂
G' : Functor.{v₄', v₅', u₄', u₅'} D₁' D₂'
inst_11 : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁' L₂' G'
⊢ Nonempty G.FullyFaithful ↔ Nonempty G'.FullyFaithful

Tactic:
⟨fun ⟨h⟩ => ⟨Φ.fullyFaithfulImp L₁ L₂ G L₁' L₂' G' h⟩,
    fun ⟨h⟩ => ⟨Φ.fullyFaithfulImp L₁' L₂' G' L₁ L₂ G h⟩⟩

Premises used: _private.0.CategoryTheory.LocalizerMorphism.nonempty_fullyFaithful_iff.match_1, Nonempty.intro, Iff.intro, _private.0.CategoryTheory.LocalizerMorphism.fullyFaithfulImp, Nonempty, CategoryTheory.Functor.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 : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ G
inst_7 rw : G.IsEquivalence
⊢ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).IsEquivalence

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

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.LocalizerMorphism.localizedFunctor, CategoryTheory.LocalizerMorphism.isEquivalence_iff
-- 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
inst_7 : G.IsEquivalence
⊢ G.IsEquivalence

Tactic:
inferInstance

Premises used: inferInstance
-- 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
inst_7 : G.IsEquivalence
⊢ G.IsEquivalence

Tactic:
exact inferInstance
-- 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₂
h : Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)
inst_6 : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ G
rw : (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).IsEquivalence
⊢ G.IsEquivalence

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

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.LocalizerMorphism.localizedFunctor, CategoryTheory.LocalizerMorphism.isEquivalence_iff
-- 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₂
h : Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)
inst_6 : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ G
⊢ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).IsEquivalence

Tactic:
h.isEquivalence

Premises used: CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.isEquivalence
-- 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₂
h : Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)
inst_6 : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ G
⊢ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).IsEquivalence

Tactic:
exact h.isEquivalence

Premises used: CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.isEquivalence
-- 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 : Φ.IsLocalizedEquivalence (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 }
⊢ G.IsEquivalence

Tactic:
have := Φ.isEquivalence W₁.Q W₂.Q G
-- 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 : Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)
G : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
this_1 : 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 }
this : G.IsEquivalence
⊢ Φ.op (W₁ := W₁) (W₂ := W₂).IsLocalizedEquivalence (W₁ := W₁.op) (W₂ := W₂.op)

Tactic:
IsLocalizedEquivalence.mk' Φ.op W₁.Q.op W₂.Q.op G.op

Premises used: CategoryTheory.Functor.op, CategoryTheory.MorphismProperty.Q, CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.mk', CategoryTheory.LocalizerMorphism.op
-- 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 : Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)
G : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
this_1 : 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 }
this : G.IsEquivalence
⊢ Φ.op (W₁ := W₁) (W₂ := W₂).IsLocalizedEquivalence (W₁ := W₁.op) (W₂ := W₂.op)

Tactic:
exact IsLocalizedEquivalence.mk' Φ.op W₁.Q.op W₂.Q.op G.op

Premises used: CategoryTheory.Functor.op, CategoryTheory.MorphismProperty.Q, CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.mk', CategoryTheory.LocalizerMorphism.op
-- 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₂)
⊢ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂).IsEquivalence

Tactic:
Φ.isEquivalence L₁ L₂ _

Premises used: CategoryTheory.LocalizerMorphism.isEquivalence
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : 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_3 : L₂.IsLocalization W₂
inst_4 : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).IsLocalization W₁
have :
  ∀ (this : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂) L₂ (𝟭 D₂)),
    Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)
⊢ Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)

Tactic:
have : CatCommSq Φ.functor (Φ.functor ⋙ L₂) L₂ (𝟭 D₂) :=
    CatCommSq.mk (rightUnitor _).symm
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : 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_3 : L₂.IsLocalization W₂
inst_4 : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).IsLocalization W₁
this : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂) L₂ (𝟭 D₂)
⊢ Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)

Tactic:
IsLocalizedEquivalence.mk' Φ (Φ.functor ⋙ L₂) L₂ (𝟭 D₂)

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.id, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.mk'
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₂ : Type u₅
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : 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_3 : L₂.IsLocalization W₂
inst_4 : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).IsLocalization W₁
this : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂) L₂ (𝟭 D₂)
⊢ Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)

Tactic:
exact IsLocalizedEquivalence.mk' Φ (Φ.functor ⋙ L₂) L₂ (𝟭 D₂)

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.id, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.mk'
-- 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₂
inst_2 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
h : W₂ ≤ W₁.map (Φ.functor (W₁ := W₁) (W₂ := W₂))
⊢ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q).IsLocalization W₁

Tactic:
Functor.IsLocalization.of_equivalence_source W₂.Q W₂ (Φ.functor ⋙ W₂.Q) W₁
      (asEquivalence Φ.functor).symm ?_ (Φ.inverts W₂.Q)
      ((associator _ _ _).symm ≪≫ isoWhiskerRight ((Equivalence.unitIso _).symm) _ ≪≫
        leftUnitor _)

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.comp, CategoryTheory.Functor.associator, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.Functor.asEquivalence, CategoryTheory.Functor.IsLocalization.of_equivalence_source, CategoryTheory.Functor.leftUnitor, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.LocalizerMorphism.inverts, CategoryTheory.Functor.isoWhiskerRight, CategoryTheory.Equivalence.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₂
inst_2 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
h : W₂ ≤ W₁.map (Φ.functor (W₁ := W₁) (W₂ := W₂))
refine : W₂ ≤ W₁.isoClosure.inverseImage Φ.functor (W₁ := W₁) (W₂ := W₂).asEquivalence.symm.functor
⊢ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q).IsLocalization W₁

Tactic:
refine Functor.IsLocalization.of_equivalence_source W₂.Q W₂ (Φ.functor ⋙ W₂.Q) W₁
      (asEquivalence Φ.functor).symm ?_ (Φ.inverts W₂.Q)
      ((associator _ _ _).symm ≪≫ isoWhiskerRight ((Equivalence.unitIso _).symm) _ ≪≫
        leftUnitor _)

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.comp, CategoryTheory.Functor.associator, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.Functor.asEquivalence, CategoryTheory.Functor.IsLocalization.of_equivalence_source, CategoryTheory.Functor.leftUnitor, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.LocalizerMorphism.inverts, CategoryTheory.Functor.isoWhiskerRight, CategoryTheory.Equivalence.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₂
inst_2 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
h : W₂ ≤ W₁.map (Φ.functor (W₁ := W₁) (W₂ := W₂))
erw : W₂ ≤ W₁.isoClosure.map Φ.functor (W₁ := W₁) (W₂ := W₂).asEquivalence.functor
⊢ W₂ ≤ W₁.isoClosure.inverseImage Φ.functor (W₁ := W₁) (W₂ := W₂).asEquivalence.symm.functor

Tactic:
erw [W₁.isoClosure.inverseImage_equivalence_functor_eq_map_inverse]

Premises used: CategoryTheory.MorphismProperty.isoClosure, CategoryTheory.MorphismProperty.inverseImage_equivalence_functor_eq_map_inverse
-- 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₂
inst_2 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
h : W₂ ≤ W₁.map (Φ.functor (W₁ := W₁) (W₂ := W₂))
rw : W₂ ≤ W₁.map Φ.functor (W₁ := W₁) (W₂ := W₂).asEquivalence.functor
⊢ W₂ ≤ W₁.isoClosure.map Φ.functor (W₁ := W₁) (W₂ := W₂).asEquivalence.functor

Tactic:
rw [MorphismProperty.map_isoClosure]

Premises used: CategoryTheory.MorphismProperty.map_isoClosure
-- 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₂
inst_2 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
h : W₂ ≤ W₁.map (Φ.functor (W₁ := W₁) (W₂ := W₂))
⊢ W₂ ≤ W₁.map Φ.functor (W₁ := W₁) (W₂ := W₂).asEquivalence.functor

Tactic:
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₂
inst_2 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
h : W₂ ≤ W₁.map (Φ.functor (W₁ := W₁) (W₂ := W₂))
⊢ W₂ ≤ W₁.map Φ.functor (W₁ := W₁) (W₂ := W₂).asEquivalence.functor

Tactic:
exact 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₂
inst_2 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
h : W₂ ≤ W₁.map (Φ.functor (W₁ := W₁) (W₂ := W₂))
⊢ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q).IsLocalization W₁

Tactic:
haveI : Functor.IsLocalization (Φ.functor ⋙ MorphismProperty.Q W₂) W₁ := by
    refine Functor.IsLocalization.of_equivalence_source W₂.Q W₂ (Φ.functor ⋙ W₂.Q) W₁
      (asEquivalence Φ.functor).symm ?_ (Φ.inverts W₂.Q)
      ((associator _ _ _).symm ≪≫ isoWhiskerRight ((Equivalence.unitIso _).symm) _ ≪≫
        leftUnitor _)
    erw [W₁.isoClosure.inverseImage_equivalence_functor_eq_map_inverse]
    rw [MorphismProperty.map_isoClosure]
    exact 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₂
inst_2 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
h : W₂ ≤ W₁.map (Φ.functor (W₁ := W₁) (W₂ := W₂))
this : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q).IsLocalization W₁
⊢ Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)

Tactic:
IsLocalizedEquivalence.of_isLocalization_of_isLocalization Φ W₂.Q

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.of_isLocalization_of_isLocalization
-- 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₂
inst_2 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
h : W₂ ≤ W₁.map (Φ.functor (W₁ := W₁) (W₂ := W₂))
this : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q).IsLocalization W₁
⊢ Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)

Tactic:
exact IsLocalizedEquivalence.of_isLocalization_of_isLocalization Φ W₂.Q

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.of_isLocalization_of_isLocalization