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_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:
exact 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
-- 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₂
inst_4 : Φ.IsLocalizedFullyFaithful (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₂.IsLocalization W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
F : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
iso : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
inst_6 : F.Full
inst_7 : F.Faithful
inst_8 : L₁.EssSurj
x x_1 : C₁
f : x ⟶ x_1
hf : W₁ f
rw : IsIso (F.map (L₁.map f))
⊢ IsIso (L₁.map f)

Tactic:
rw [← isIso_iff_of_reflects_iso  _ F]

Premises used: CategoryTheory.isIso_iff_of_reflects_iso
-- 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₂
inst_4 : Φ.IsLocalizedFullyFaithful (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₂.IsLocalization W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
F : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
iso : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
inst_6 : F.Full
inst_7 : F.Faithful
inst_8 : L₁.EssSurj
x x_1 : C₁
f : x ⟶ x_1
hf : W₁ f
⊢ IsIso (F.map (L₁.map f))

Tactic:
((MorphismProperty.isomorphisms _).arrow_mk_iso_iff
      (Arrow.isoOfNatIso iso f)).1 (Localization.inverts L₂ W₂ _ (Φ.map _ hf))

Premises used: CategoryTheory.MorphismProperty.isomorphisms, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.LocalizerMorphism.map, Iff.mp, CategoryTheory.Arrow.isoOfNatIso, CategoryTheory.Localization.inverts, CategoryTheory.Arrow.mk
-- 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₂
inst_4 : Φ.IsLocalizedFullyFaithful (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₂.IsLocalization W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
F : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
iso : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
inst_6 : F.Full
inst_7 : F.Faithful
inst_8 : L₁.EssSurj
x x_1 : C₁
f : x ⟶ x_1
hf : W₁ f
⊢ IsIso (F.map (L₁.map f))

Tactic:
exact ((MorphismProperty.isomorphisms _).arrow_mk_iso_iff
      (Arrow.isoOfNatIso iso f)).1 (Localization.inverts L₂ W₂ _ (Φ.map _ hf))

Premises used: CategoryTheory.MorphismProperty.isomorphisms, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.LocalizerMorphism.map, Iff.mp, CategoryTheory.Arrow.isoOfNatIso, CategoryTheory.Localization.inverts, CategoryTheory.Arrow.mk
-- 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₂
inst_4 : Φ.IsLocalizedFullyFaithful (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₂.IsLocalization W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
F : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
iso : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
inst_6 : F.Full
inst_7 : F.Faithful
inst_8 : L₁.EssSurj
⊢ W₁.IsInvertedBy L₁

Tactic:
have h : W₁.IsInvertedBy L₁ := fun _ _ f hf ↦ by
    rw [← isIso_iff_of_reflects_iso  _ F]
    exact ((MorphismProperty.isomorphisms _).arrow_mk_iso_iff
      (Arrow.isoOfNatIso iso f)).1 (Localization.inverts L₂ W₂ _ (Φ.map _ hf))
-- 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₂
inst_4 : Φ.IsLocalizedFullyFaithful (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₂.IsLocalization W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
F : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
iso : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
inst_6 : F.Full
inst_7 : F.Faithful
inst_8 : L₁.EssSurj
h : W₁.IsInvertedBy L₁
G : W₁.Localization ⥤ D₁ := lift (W := W₁) L₁ h W₁.Q
e : W₁.Q ⋙ G ≅ L₁ := fac (W := W₁) L₁ h W₁.Q
this : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q L₂ (G ⋙ F) :=
  { iso := iso ≪≫ isoWhiskerRight e.symm F ≪≫ W₁.Q.associator G F }
have : ∀ (hG : G.FullyFaithful), L₁.IsLocalization W₁
⊢ L₁.IsLocalization W₁

Tactic:
have hG : G.FullyFaithful := Functor.FullyFaithful.ofCompFaithful
    (Φ.fullyFaithful W₁.Q L₂ (G ⋙ F))
-- 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₂
inst_4 : Φ.IsLocalizedFullyFaithful (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₂.IsLocalization W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
F : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
iso : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
inst_6 : F.Full
inst_7 : F.Faithful
inst_8 : L₁.EssSurj
h : W₁.IsInvertedBy L₁
G : W₁.Localization ⥤ D₁ := lift (W := W₁) L₁ h W₁.Q
e : W₁.Q ⋙ G ≅ L₁ := fac (W := W₁) L₁ h W₁.Q
this : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q L₂ (G ⋙ F) :=
  { iso := iso ≪≫ isoWhiskerRight e.symm F ≪≫ W₁.Q.associator G F }
hG : G.FullyFaithful
⊢ G.Full

Tactic:
have := hG.full
-- 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₂
inst_4 : Φ.IsLocalizedFullyFaithful (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₂.IsLocalization W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
F : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
iso : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
inst_6 : F.Full
inst_7 : F.Faithful
inst_8 : L₁.EssSurj
h : W₁.IsInvertedBy L₁
G : W₁.Localization ⥤ D₁ := lift (W := W₁) L₁ h W₁.Q
e : W₁.Q ⋙ G ≅ L₁ := fac (W := W₁) L₁ h W₁.Q
this_1 : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q L₂ (G ⋙ F) :=
  { iso := iso ≪≫ isoWhiskerRight e.symm F ≪≫ W₁.Q.associator G F }
hG : G.FullyFaithful
this : G.Full
⊢ G.Faithful

Tactic:
have := hG.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₂
inst_4 : Φ.IsLocalizedFullyFaithful (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₂.IsLocalization W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
F : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
iso : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
inst_6 : F.Full
inst_7 : F.Faithful
inst_8 : L₁.EssSurj
h : W₁.IsInvertedBy L₁
G : W₁.Localization ⥤ D₁ := lift (W := W₁) L₁ h W₁.Q
e : W₁.Q ⋙ G ≅ L₁ := fac (W := W₁) L₁ h W₁.Q
this_1 : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q L₂ (G ⋙ F) :=
  { iso := iso ≪≫ isoWhiskerRight e.symm F ≪≫ W₁.Q.associator G F }
hG : G.FullyFaithful
this_2 : G.Full
this : G.Faithful
⊢ G.EssSurj

Tactic:
have : G.EssSurj :=
    ⟨fun X ↦ ⟨W₁.Q.obj (L₁.objPreimage X), ⟨e.app _ ≪≫ L₁.objObjPreimageIso X⟩⟩⟩
-- 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₂
inst_4 : Φ.IsLocalizedFullyFaithful (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₂.IsLocalization W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
F : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
iso : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
inst_6 : F.Full
inst_7 : F.Faithful
inst_8 : L₁.EssSurj
h : W₁.IsInvertedBy L₁
G : W₁.Localization ⥤ D₁ := lift (W := W₁) L₁ h W₁.Q
e : W₁.Q ⋙ G ≅ L₁ := fac (W := W₁) L₁ h W₁.Q
this_1 : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q L₂ (G ⋙ F) :=
  { iso := iso ≪≫ isoWhiskerRight e.symm F ≪≫ W₁.Q.associator G F }
hG : G.FullyFaithful
this_2 : G.Full
this_3 : G.Faithful
this : G.EssSurj
⊢ G.IsEquivalence

Tactic:
have : G.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₂
inst_4 : Φ.IsLocalizedFullyFaithful (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₂.IsLocalization W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
F : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
iso : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
inst_6 : F.Full
inst_7 : F.Faithful
inst_8 : L₁.EssSurj
h : W₁.IsInvertedBy L₁
G : W₁.Localization ⥤ D₁ := lift (W := W₁) L₁ h W₁.Q
e : W₁.Q ⋙ G ≅ L₁ := fac (W := W₁) L₁ h W₁.Q
this_1 : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q L₂ (G ⋙ F) :=
  { iso := iso ≪≫ isoWhiskerRight e.symm F ≪≫ W₁.Q.associator G F }
hG : G.FullyFaithful
this_2 : G.Full
this_3 : G.Faithful
this_4 : G.EssSurj
this : G.IsEquivalence
⊢ L₁.IsLocalization W₁

Tactic:
IsLocalization.of_equivalence_target W₁.Q W₁ L₁ G.asEquivalence e

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.asEquivalence, CategoryTheory.Functor.IsLocalization.of_equivalence_target
-- 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₂
inst_4 : Φ.IsLocalizedFullyFaithful (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₂.IsLocalization W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
F : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
iso : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ F
inst_6 : F.Full
inst_7 : F.Faithful
inst_8 : L₁.EssSurj
h : W₁.IsInvertedBy L₁
G : W₁.Localization ⥤ D₁ := lift (W := W₁) L₁ h W₁.Q
e : W₁.Q ⋙ G ≅ L₁ := fac (W := W₁) L₁ h W₁.Q
this_1 : CatCommSq (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q L₂ (G ⋙ F) :=
  { iso := iso ≪≫ isoWhiskerRight e.symm F ≪≫ W₁.Q.associator G F }
hG : G.FullyFaithful
this_2 : G.Full
this_3 : G.Faithful
this_4 : G.EssSurj
this : G.IsEquivalence
⊢ L₁.IsLocalization W₁

Tactic:
exact IsLocalization.of_equivalence_target W₁.Q W₁ L₁ G.asEquivalence e

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.asEquivalence, CategoryTheory.Functor.IsLocalization.of_equivalence_target
-- 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 W₂ W₃
inst_7 : Φ.IsLocalizedFullyFaithful (W₁ := W₁) (W₂ := W₂)
inst_8 : Ψ.IsLocalizedFullyFaithful (W₁ := W₂) (W₂ := W₃)
⊢ (Φ.comp (W₁ := W₁) (W₂ := W₂) (W₃ := W₃) Ψ).IsLocalizedFullyFaithful (W₁ := W₁) (W₂ := W₃)

Tactic:
letI : CatCommSq (Φ.comp Ψ).functor W₁.Q W₃.Q
      (Φ.localizedFunctor W₁.Q W₂.Q ⋙ Ψ.localizedFunctor W₂.Q W₃.Q) :=
    CatCommSq.hComp _ _ _ W₂.Q _ _ _
  IsLocalizedFullyFaithful.mk' _ W₁.Q W₃.Q _
    ((Φ.fullyFaithfulLocalizedFunctor W₁.Q W₂.Q).comp
      (Ψ.fullyFaithfulLocalizedFunctor W₂.Q W₃.Q))

Premises used: CategoryTheory.LocalizerMorphism.IsLocalizedFullyFaithful.mk', CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.comp, CategoryTheory.LocalizerMorphism.fullyFaithfulLocalizedFunctor, CategoryTheory.Functor.FullyFaithful.comp, CategoryTheory.LocalizerMorphism.localizedFunctor, CategoryTheory.LocalizerMorphism.comp
-- 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 : Φ.IsInduced (W₁ := W₁) (W₂ := W₂)
⊢ W₂.op.inverseImage (Φ.op (W₁ := W₁) (W₂ := W₂).functor (W₁ := W₁.op) (W₂ := W₂.op)) = W₁.op

Tactic:
simp [← Φ.inverseImage_eq]

Premises used: CategoryTheory.LocalizerMorphism.IsInduced.inverseImage_eq
-- 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 W₂ W₃
inst_7 : Φ.IsInduced (W₁ := W₁) (W₂ := W₂)
inst_8 : Ψ.IsInduced (W₁ := W₂) (W₂ := W₃)
⊢ W₃.inverseImage ((Φ.comp (W₁ := W₁) (W₂ := W₂) (W₃ := W₃) Ψ).functor (W₁ := W₁) (W₂ := W₃)) = W₁

Tactic:
simp [← Φ.inverseImage_eq, ← Ψ.inverseImage_eq]

Premises used: CategoryTheory.LocalizerMorphism.IsInduced.inverseImage_eq
-- 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 : Φ.IsInduced (W₁ := W₁) (W₂ := W₂)
simp :
  W₂.arrow.inverseImage Φ.functor (W₁ := W₁) (W₂ := W₂).mapArrow =
    (W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))).arrow
⊢ W₂.arrow.inverseImage (Φ.arrow (W₁ := W₁) (W₂ := W₂).functor (W₁ := W₁.arrow) (W₂ := W₂.arrow)) = W₁.arrow

Tactic:
simp only [← Φ.inverseImage_eq]

Premises used: CategoryTheory.LocalizerMorphism.IsInduced.inverseImage_eq
-- 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 : Φ.IsInduced (W₁ := W₁) (W₂ := W₂)
⊢ W₂.arrow.inverseImage Φ.functor (W₁ := W₁) (W₂ := W₂).mapArrow =
    (W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))).arrow

Tactic:
rfl
-- 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 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
inst_8 : Φ.IsInduced (W₁ := W₁) (W₂ := W₂)
inst_9 : W₂.RespectsIso
simp : W₂ ≤ (W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))).inverseImage Φ.functor (W₁ := W₁) (W₂ := W₂).inv
⊢ W₂ ≤ W₁.inverseImage Φ.functor (W₁ := W₁) (W₂ := W₂).inv

Tactic:
simp only [← Φ.inverseImage_eq]

Premises used: CategoryTheory.LocalizerMorphism.IsInduced.inverseImage_eq
-- 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 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
inst_8 : Φ.IsInduced (W₁ := W₁) (W₂ := W₂)
inst_9 : W₂.RespectsIso
X Y : C₂
f : X ⟶ Y
hf : W₂ f
⊢ (W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))).inverseImage Φ.functor (W₁ := W₁) (W₂ := W₂).inv f

Tactic:
(W₂.arrow_mk_iso_iff
      (Arrow.isoMk (Φ.functor.asEquivalence.counitIso.app _)
        (Φ.functor.asEquivalence.counitIso.app _))).2 hf

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.inverseImage, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.Functor.asEquivalence, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.Iso.app, CategoryTheory.Arrow.isoMk, CategoryTheory.Equivalence.counitIso
-- 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 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
inst_8 : Φ.IsInduced (W₁ := W₁) (W₂ := W₂)
inst_9 : W₂.RespectsIso
X Y : C₂
f : X ⟶ Y
hf : W₂ f
⊢ (W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))).inverseImage Φ.functor (W₁ := W₁) (W₂ := W₂).inv f

Tactic:
exact (W₂.arrow_mk_iso_iff
      (Arrow.isoMk (Φ.functor.asEquivalence.counitIso.app _)
        (Φ.functor.asEquivalence.counitIso.app _))).2 hf

Premises used: Iff.mpr, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.Functor.asEquivalence, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.Iso.app, CategoryTheory.Arrow.isoMk, CategoryTheory.Equivalence.counitIso
-- 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 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
inst_8 : Φ.IsInduced (W₁ := W₁) (W₂ := W₂)
inst_9 : W₂.RespectsIso
⊢ Φ.functor (W₁ := W₁) (W₂ := W₂).inv.IsEquivalence

Tactic:
infer_instance
-- 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 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
inst_8 : Φ.IsInduced (W₁ := W₁) (W₂ := W₂)
inst_9 : W₂.RespectsIso
h : ∀ ⦃X Y : C₂⦄ (f : X ⟶ Y), W₁.inverseImage (Φ.inv (W₁ := W₁) (W₂ := W₂).functor (W₁ := W₂) (W₂ := W₁)) f ↔ W₂ f
⊢ W₁.inverseImage (Φ.inv (W₁ := W₁) (W₂ := W₂).functor (W₁ := W₂) (W₂ := W₁)) = W₂

Tactic:
ext X Y f
-- 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 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
inst_8 : Φ.IsInduced (W₁ := W₁) (W₂ := W₂)
inst_9 : W₂.RespectsIso
X Y : C₂
f : X ⟶ Y
h :
  (W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))).inverseImage
      (Φ.inv (W₁ := W₁) (W₂ := W₂).functor (W₁ := W₂) (W₂ := W₁)) f ↔
    W₂ f
⊢ W₁.inverseImage (Φ.inv (W₁ := W₁) (W₂ := W₂).functor (W₁ := W₂) (W₂ := W₁)) f ↔ W₂ f

Tactic:
simp only [← Φ.inverseImage_eq]

Premises used: CategoryTheory.LocalizerMorphism.IsInduced.inverseImage_eq