awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
inst_3 : L.IsLocalization W
F : Functor.{v_1, v_3, u_1, u_3} C E
F' : Functor.{v_2, v_3, u_2, u_3} D E
h : Lifting L W F F'
X : C
⊢ Eq.{v_3 + 1} (α := F'.obj (L.obj X) ⟶ F'.obj (L.obj X)) (𝟙 ((L ⋙ F').obj X)) (𝟙 (F'.obj (L.obj X)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
L₁ L₂ : Functor.{v_1, v_2, u_1, u_2} C D
e : L₁ ≅ L₂
inst_2 : L₁.IsLocalization W
⊢ W.IsInvertedBy L₁

Tactic:
have h := Localization.inverts L₁ W
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
L₁ L₂ : Functor.{v_1, v_2, u_1, u_2} C D
e : L₁ ≅ L₂
inst_2 : L₁.IsLocalization W
h : W.IsInvertedBy L₁
⊢ W.IsInvertedBy L₂

Tactic:
rw [MorphismProperty.IsInvertedBy.iff_of_iso W e] at h

Premises used: CategoryTheory.MorphismProperty.IsInvertedBy.iff_of_iso
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
L₁ L₂ : Functor.{v_1, v_2, u_1, u_2} C D
e : L₁ ≅ L₂
inst_2 : L₁.IsLocalization W
h : W.IsInvertedBy L₂
F₁ : W.Localization ⥤ D := Construction.lift (W := W) L₁ ⋯
F₂ : W.Localization ⥤ D := Construction.lift (W := W) L₂ h
⊢ L₂.IsLocalization W

Tactic:
{ inverts := h
      isEquivalence := Functor.isEquivalence_of_iso (liftNatIso W.Q W L₁ L₂ F₁ F₂ e) }

Premises used: CategoryTheory.Localization.liftNatIso, CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.IsLocalization.mk, CategoryTheory.Functor.isEquivalence_of_iso
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
L₁ L₂ : Functor.{v_1, v_2, u_1, u_2} C D
e : L₁ ≅ L₂
inst_2 : L₁.IsLocalization W
h : W.IsInvertedBy L₂
F₁ : W.Localization ⥤ D := Construction.lift (W := W) L₁ ⋯
F₂ : W.Localization ⥤ D := Construction.lift (W := W) L₂ h
⊢ L₂.IsLocalization W

Tactic:
exact
    { inverts := h
      isEquivalence := Functor.isEquivalence_of_iso (liftNatIso W.Q W L₁ L₂ F₁ F₂ e) }
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_4
inst_2 : Category.{v_4, u_4} E
L' : Functor.{v_1, v_4, u_1, u_4} C E
eq : Equivalence.{v_2, v_4, u_2, u_4} D E
inst_3 : L.IsLocalization W
e : L ⋙ eq.functor ≅ L'
rw : W.IsInvertedBy (L ⋙ eq.functor)
⊢ W.IsInvertedBy L'

Tactic:
rw [← MorphismProperty.IsInvertedBy.iff_of_iso W e]

Premises used: CategoryTheory.MorphismProperty.IsInvertedBy.iff_of_iso
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_4
inst_2 : Category.{v_4, u_4} E
L' : Functor.{v_1, v_4, u_1, u_4} C E
eq : Equivalence.{v_2, v_4, u_2, u_4} D E
inst_3 : L.IsLocalization W
e : L ⋙ eq.functor ≅ L'
⊢ W.IsInvertedBy (L ⋙ eq.functor)

Tactic:
MorphismProperty.IsInvertedBy.of_comp W L (Localization.inverts L W) eq.functor

Premises used: CategoryTheory.MorphismProperty.IsInvertedBy.of_comp, CategoryTheory.Equivalence.functor, CategoryTheory.Localization.inverts
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_4
inst_2 : Category.{v_4, u_4} E
L' : Functor.{v_1, v_4, u_1, u_4} C E
eq : Equivalence.{v_2, v_4, u_2, u_4} D E
inst_3 : L.IsLocalization W
e : L ⋙ eq.functor ≅ L'
⊢ W.IsInvertedBy (L ⋙ eq.functor)

Tactic:
exact MorphismProperty.IsInvertedBy.of_comp W L (Localization.inverts L W) eq.functor

Premises used: CategoryTheory.MorphismProperty.IsInvertedBy.of_comp, CategoryTheory.Equivalence.functor, CategoryTheory.Localization.inverts
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_4
inst_2 : Category.{v_4, u_4} E
L' : Functor.{v_1, v_4, u_1, u_4} C E
eq : Equivalence.{v_2, v_4, u_2, u_4} D E
inst_3 : L.IsLocalization W
e : L ⋙ eq.functor ≅ L'
⊢ W.IsInvertedBy L'

Tactic:
have h : W.IsInvertedBy L' := by
    rw [← MorphismProperty.IsInvertedBy.iff_of_iso W e]
    exact MorphismProperty.IsInvertedBy.of_comp W L (Localization.inverts L W) eq.functor
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_4
inst_2 : Category.{v_4, u_4} E
L' : Functor.{v_1, v_4, u_1, u_4} C E
eq : Equivalence.{v_2, v_4, u_2, u_4} D E
inst_3 : L.IsLocalization W
e : L ⋙ eq.functor ≅ L'
h : W.IsInvertedBy L'
F₁ : W.Localization ⥤ D := Construction.lift (W := W) L ⋯
F₂ : W.Localization ⥤ E := Construction.lift (W := W) L' h
e' : F₁ ⋙ eq.functor ≅ F₂ := liftNatIso W.Q W (L ⋙ eq.functor) L' (F₁ ⋙ eq.functor) F₂ e
⊢ L'.IsLocalization W

Tactic:
{ inverts := h
      isEquivalence := Functor.isEquivalence_of_iso e' }

Premises used: CategoryTheory.Functor.IsLocalization.mk, CategoryTheory.Functor.isEquivalence_of_iso
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_4
inst_2 : Category.{v_4, u_4} E
L' : Functor.{v_1, v_4, u_1, u_4} C E
eq : Equivalence.{v_2, v_4, u_2, u_4} D E
inst_3 : L.IsLocalization W
e : L ⋙ eq.functor ≅ L'
h : W.IsInvertedBy L'
F₁ : W.Localization ⥤ D := Construction.lift (W := W) L ⋯
F₂ : W.Localization ⥤ E := Construction.lift (W := W) L' h
e' : F₁ ⋙ eq.functor ≅ F₂ := liftNatIso W.Q W (L ⋙ eq.functor) L' (F₁ ⋙ eq.functor) F₂ e
⊢ L'.IsLocalization W

Tactic:
exact
    { inverts := h
      isEquivalence := Functor.isEquivalence_of_iso e' }
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_3 : F.IsEquivalence
inst_4 : L.IsLocalization W
⊢ (L ⋙ F).IsLocalization W

Tactic:
of_equivalence_target L W _ F.asEquivalence (Iso.refl _)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Functor.asEquivalence, CategoryTheory.Functor.IsLocalization.of_equivalence_target
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
hW : W ≤ MorphismProperty.isomorphisms C
inst_2 : L.IsEquivalence
⊢ IsLocalization (𝟭 C) W

Tactic:
haveI : (𝟭 C).IsLocalization W := for_id W hW
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
hW : W ≤ MorphismProperty.isomorphisms C
inst_2 : L.IsEquivalence
this : IsLocalization (𝟭 C) W
⊢ L.IsLocalization W

Tactic:
of_equivalence_target (𝟭 C) W L L.asEquivalence L.leftUnitor

Premises used: CategoryTheory.Functor.id, CategoryTheory.Functor.asEquivalence, CategoryTheory.Functor.leftUnitor, CategoryTheory.Functor.IsLocalization.of_equivalence_target
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
hW : W ≤ MorphismProperty.isomorphisms C
inst_2 : L.IsEquivalence
this : IsLocalization (𝟭 C) W
⊢ L.IsLocalization W

Tactic:
exact of_equivalence_target (𝟭 C) W L L.asEquivalence L.leftUnitor

Premises used: CategoryTheory.Functor.id, CategoryTheory.Functor.asEquivalence, CategoryTheory.Functor.leftUnitor, CategoryTheory.Functor.IsLocalization.of_equivalence_target
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
P : MorphismProperty.{v_2, u_2} D
inst_3 : P.RespectsIso
inst_4 : P.IsMultiplicative
h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)
h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv
e : W.Q ⋙ (uniq W.Q L W).functor ≅ L := compUniqFunctor W.Q L W
X Y : C
f : X ⟶ Y
hf : W f
⊢ P.inverseImage (uniq W.Q L W).functor (Construction.wInv (W := W) f hf)

Tactic:
(P.arrow_mk_iso_iff (Arrow.isoMk (e.app _) (e.app _) ?_)).2 (h₂ f hf)

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.inverseImage, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.Iso.app, CategoryTheory.Arrow.isoMk
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
P : MorphismProperty.{v_2, u_2} D
inst_3 : P.RespectsIso
inst_4 : P.IsMultiplicative
h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)
h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv
e : W.Q ⋙ (uniq W.Q L W).functor ≅ L := compUniqFunctor W.Q L W
X Y : C
f : X ⟶ Y
hf : W f
refine :
  (e.app Y).hom ≫ (Arrow.mk (isoOfHom L W f hf).inv).hom =
    (Arrow.mk ((uniq W.Q L W).functor.map (Construction.wInv (W := W) f hf))).hom ≫ (e.app X).hom
⊢ P.inverseImage (uniq W.Q L W).functor (Construction.wInv (W := W) f hf)

Tactic:
refine (P.arrow_mk_iso_iff (Arrow.isoMk (e.app _) (e.app _) ?_)).2 (h₂ f hf)

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.Iso.app, CategoryTheory.Arrow.isoMk
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
P : MorphismProperty.{v_2, u_2} D
inst_3 : P.RespectsIso
inst_4 : P.IsMultiplicative
h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)
h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv
e : W.Q ⋙ (uniq W.Q L W).functor ≅ L := compUniqFunctor W.Q L W
X Y : C
f : X ⟶ Y
hf : W f
dsimp :
  e.hom.app Y ≫ (isoOfHom L W f hf).inv = (uniq W.Q L W).functor.map (Construction.wInv (W := W) f hf) ≫ e.hom.app X
⊢ (e.app Y).hom ≫ (Arrow.mk (isoOfHom L W f hf).inv).hom =
    (Arrow.mk ((uniq W.Q L W).functor.map (Construction.wInv (W := W) f hf))).hom ≫ (e.app X).hom

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
P : MorphismProperty.{v_2, u_2} D
inst_3 : P.RespectsIso
inst_4 : P.IsMultiplicative
h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)
h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv
e : W.Q ⋙ (uniq W.Q L W).functor ≅ L := compUniqFunctor W.Q L W
X Y : C
f : X ⟶ Y
hf : W f
rw : e.hom.app Y ≫ (isoOfHom L W f hf).inv = (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X
rw₁ :
  (e.hom.app Y ≫ (isoOfHom L W f hf).inv) ≫ (isoOfHom L W f hf).hom =
    ((uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X) ≫ (isoOfHom L W f hf).hom
rw₂ :
  e.hom.app Y ≫ (isoOfHom L W f hf).inv ≫ (isoOfHom L W f hf).hom =
    ((uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X) ≫ (isoOfHom L W f hf).hom
rw₃ :
  e.hom.app Y ≫ (isoOfHom L W f hf).inv ≫ (isoOfHom L W f hf).hom =
    (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X ≫ (isoOfHom L W f hf).hom
rw₄ :
  e.hom.app Y ≫ 𝟙 (L.1 Y) = (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X ≫ (isoOfHom L W f hf).hom
rw₅ : e.hom.app Y = (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X ≫ (isoOfHom L W f hf).hom
rw₆ : e.hom.app Y = (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X ≫ L.map f
rw₇ :
  e.hom.app Y =
    (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ (W.Q ⋙ (uniq W.Q L W).functor).map f ≫ e.hom.app Y
rw₈ :
  e.hom.app Y =
    (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ (uniq W.Q L W).functor.map (W.Q.map f) ≫ e.hom.app Y
rw₉ : e.hom.app Y = (uniq W.Q L W).functor.map ((isoOfHom W.Q W f hf).inv ≫ W.Q.map f) ≫ e.hom.app Y
rw₁₀ : e.hom.app Y = (uniq W.Q L W).functor.map (𝟙 (W.Q.obj Y)) ≫ e.hom.app Y
rw₁₁ : e.hom.app Y = 𝟙 ((uniq W.Q L W).functor.obj (W.Q.obj Y)) ≫ e.hom.app Y
rw₁₂ rw₁₃ : e.hom.app Y = e.hom.app Y
⊢ e.hom.app Y ≫ (isoOfHom L W f hf).inv = (uniq W.Q L W).functor.map (Construction.wInv (W := W) f hf) ≫ e.hom.app X

Tactic:
rw [Construction.wInv_eq_isoOfHom_inv, ← cancel_mono (isoOfHom L W f hf).hom,
          assoc, assoc, Iso.inv_hom_id, comp_id, isoOfHom_hom, ← NatTrans.naturality,
          Functor.comp_map, ← Functor.map_comp_assoc,
          isoOfHom_inv_hom_id, map_id, id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Localization.isoOfHom_inv_hom_id, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Localization.Construction.wInv_eq_isoOfHom_inv, CategoryTheory.Localization.isoOfHom_hom, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Localization.isoOfHom, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_id, CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom, CategoryTheory.Functor.comp_map, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
P : MorphismProperty.{v_2, u_2} D
inst_3 : P.RespectsIso
inst_4 : P.IsMultiplicative
h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)
h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv
e : W.Q ⋙ (uniq W.Q L W).functor ≅ L := compUniqFunctor W.Q L W
⊢ P.inverseImage (uniq W.Q L W).functor = ⊤

Tactic:
have hP : P.inverseImage (uniq W.Q L W).functor = ⊤ :=
    Construction.morphismProperty_eq_top _
      (fun _ _ f ↦ (P.arrow_mk_iso_iff
        (((Functor.mapArrowFunctor _ _).mapIso e).app (Arrow.mk f))).2 (h₁ f))
      (fun X Y f hf ↦ by
        refine (P.arrow_mk_iso_iff (Arrow.isoMk (e.app _) (e.app _) ?_)).2 (h₂ f hf)
        dsimp
        rw [Construction.wInv_eq_isoOfHom_inv, ← cancel_mono (isoOfHom L W f hf).hom,
          assoc, assoc, Iso.inv_hom_id, comp_id, isoOfHom_hom, ← NatTrans.naturality,
          Functor.comp_map, ← Functor.map_comp_assoc,
          isoOfHom_inv_hom_id, map_id, id_comp])
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
P : MorphismProperty.{v_2, u_2} D
inst_3 : P.RespectsIso
inst_4 : P.IsMultiplicative
h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)
h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv
e : W.Q ⋙ (uniq W.Q L W).functor ≅ L := compUniqFunctor W.Q L W
hP : P.inverseImage (uniq W.Q L W).functor = ⊤
rw : (P.inverseImage (uniq W.Q L W).functor).map (uniq W.Q L W).functor = ⊤
rw₁ : MorphismProperty.map ⊤ (uniq W.Q L W).functor = ⊤
rw₂ rw₃ : Eq (α := MorphismProperty.{v_2, u_2} D) ⊤ ⊤
⊢ P = ⊤

Tactic:
rw [← P.map_inverseImage_eq_of_isEquivalence (uniq W.Q L W).functor, hP,
    MorphismProperty.map_top_eq_top_of_essSurj_of_full]

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Localization.uniq, CategoryTheory.Equivalence.functor, CategoryTheory.MorphismProperty.map_top_eq_top_of_essSurj_of_full, CategoryTheory.MorphismProperty.map_inverseImage_eq_of_isEquivalence
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : L.IsLocalization ⊤
rw : Eq (α := MorphismProperty.{v_2, u_2} D) (MorphismProperty.isomorphisms D) ⊤
⊢ IsGroupoid.{v_2, u_2} D

Tactic:
rw [isGroupoid_iff_isomorphisms_eq_top]

Premises used: CategoryTheory.isGroupoid_iff_isomorphisms_eq_top
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : L.IsLocalization ⊤
x x_1 : C
f : x ⟶ x_1
⊢ ⊤ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : L.IsLocalization ⊤
⊢ Eq (α := MorphismProperty.{v_2, u_2} D) (MorphismProperty.isomorphisms D) ⊤

Tactic:
exact morphismProperty_eq_top L ⊤ _
    (fun _ _ f ↦ inverts L ⊤ _ (by simp))
    (fun _ _ f hf ↦ Iso.isIso_inv _)

Premises used: CategoryTheory.Localization.isoOfHom, CategoryTheory.Iso.isIso_inv, CategoryTheory.Localization.morphismProperty_eq_top, CategoryTheory.Localization.inverts, Top.top
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
E : Type u_3
inst_2 : Category.{v_3, u_3} E
D₁ : Type ?u.80119
D₂ : Type ?u.80122
inst_3 : Category.{v_4, ?u.80119} D₁
inst_4 : Category.{v_5, ?u.80122} D₂
L₁ : Functor.{v_1, v_4, u_1, ?u.80119} C D₁
L₂ : Functor.{v_1, v_5, u_1, ?u.80122} C D₂
W' : MorphismProperty.{v_1, u_1} C
inst_5 : L₁.IsLocalization W'
inst_6 : L₂.IsLocalization W'
⊢ IsGroupoid (MorphismProperty.Localization.{v_1, u_1} (C := C) ⊤)

Tactic:
isGroupoid <| MorphismProperty.Q ⊤

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Localization.isGroupoid, Top.top
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
inst_2 : L.IsLocalization W
mp : W.Q.map f = W.Q.map g → L.map f = L.map g
mpr : L.map f = L.map g → W.Q.map f = W.Q.map g
⊢ W.Q.map f = W.Q.map g ↔ L.map f = L.map g

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
inst_2 : L.IsLocalization W
h : W.Q.map f = W.Q.map g
e : W.Q ⋙ (Localization.uniq W.Q L W).functor ≅ L := Localization.compUniqFunctor W.Q L W
mp :
  e.inv.app X ≫ (W.Q ⋙ (Localization.uniq W.Q L W).functor).map f ≫ e.hom.app Y =
    e.inv.app X ≫ (W.Q ⋙ (Localization.uniq W.Q L W).functor).map g ≫ e.hom.app Y
⊢ L.map f = L.map g

Tactic:
rw [← NatIso.naturality_1 e f, ← NatIso.naturality_1 e g]

Premises used: CategoryTheory.NatIso.naturality_1
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
inst_2 : L.IsLocalization W
h : W.Q.map f = W.Q.map g
e : W.Q ⋙ (Localization.uniq W.Q L W).functor ≅ L := Localization.compUniqFunctor W.Q L W
mp :
  e.inv.app X ≫ (Localization.uniq W.Q L W).functor.map (W.Q.map f) ≫ e.hom.app Y =
    e.inv.app X ≫ (Localization.uniq W.Q L W).functor.map (W.Q.map g) ≫ e.hom.app Y
⊢ e.inv.app X ≫ (W.Q ⋙ (Localization.uniq W.Q L W).functor).map f ≫ e.hom.app Y =
    e.inv.app X ≫ (W.Q ⋙ (Localization.uniq W.Q L W).functor).map g ≫ e.hom.app Y

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
inst_2 : L.IsLocalization W
h : W.Q.map f = W.Q.map g
e : W.Q ⋙ (Localization.uniq W.Q L W).functor ≅ L := Localization.compUniqFunctor W.Q L W
mp mp₁ :
  e.inv.app X ≫ (Localization.uniq W.Q L W).functor.map (W.Q.map g) ≫ e.hom.app Y =
    e.inv.app X ≫ (Localization.uniq W.Q L W).functor.map (W.Q.map g) ≫ e.hom.app Y
⊢ e.inv.app X ≫ (Localization.uniq W.Q L W).functor.map (W.Q.map f) ≫ e.hom.app Y =
    e.inv.app X ≫ (Localization.uniq W.Q L W).functor.map (W.Q.map g) ≫ e.hom.app Y

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
inst_2 : L.IsLocalization W
h : L.map f = L.map g
e : L ⋙ (Localization.uniq L W.Q W).functor ≅ W.Q := Localization.compUniqFunctor L W.Q W
mpr :
  e.inv.app X ≫ (L ⋙ (Localization.uniq L W.Q W).functor).map f ≫ e.hom.app Y =
    e.inv.app X ≫ (L ⋙ (Localization.uniq L W.Q W).functor).map g ≫ e.hom.app Y
⊢ W.Q.map f = W.Q.map g

Tactic:
rw [← NatIso.naturality_1 e f, ← NatIso.naturality_1 e g]

Premises used: CategoryTheory.NatIso.naturality_1
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
inst_2 : L.IsLocalization W
h : L.map f = L.map g
e : L ⋙ (Localization.uniq L W.Q W).functor ≅ W.Q := Localization.compUniqFunctor L W.Q W
mpr mpr₁ :
  e.inv.app X ≫ (Localization.uniq L W.Q W).functor.map (L.map g) ≫ e.hom.app Y =
    e.inv.app X ≫ (Localization.uniq L W.Q W).functor.map (L.map g) ≫ e.hom.app Y
⊢ e.inv.app X ≫ (Localization.uniq L W.Q W).functor.map (L.map f) ≫ e.hom.app Y =
    e.inv.app X ≫ (Localization.uniq L W.Q W).functor.map (L.map g) ≫ e.hom.app Y

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : L.IsLocalization W
h : L.map f = L.map g
⊢ AreEqualizedByLocalization W f g

Tactic:
(areEqualizedByLocalization_iff L W f g).2 h

Premises used: Iff.mpr, CategoryTheory.areEqualizedByLocalization_iff
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h : AreEqualizedByLocalization W f g
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : L.IsLocalization W
⊢ L.map f = L.map g

Tactic:
(areEqualizedByLocalization_iff L W f g).1 h

Premises used: CategoryTheory.areEqualizedByLocalization_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Localization.Predicate
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h : AreEqualizedByLocalization W f g
F : Functor.{v_1, v_2, u_1, u_2} C D
hF : W.IsInvertedBy F
⊢ F.map f = F.map g

Tactic:
simp [← NatIso.naturality_1 (Localization.fac F hF W.Q), h.map_eq W.Q]

Premises used: CategoryTheory.NatIso.naturality_1, CategoryTheory.MorphismProperty.Q, CategoryTheory.AreEqualizedByLocalization.map_eq, CategoryTheory.Localization.fac