awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.OfQuotient
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
r : HomRel.{u_1, v_1} C
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F₁ F₂ : Functor.{v_1, v_3, u_1, u_3} (Quotient r) E
h : functor r ⋙ F₁ = functor r ⋙ F₂
X : C
⊢ F₁.obj (mk (r := r) X) = F₂.obj (mk (r := r) X)

Tactic:
exact Functor.congr_obj h X

Premises used: CategoryTheory.Functor.congr_obj
-- Module: Mathlib.CategoryTheory.Localization.OfQuotient
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
r : HomRel.{u_1, v_1} C
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F₁ F₂ : Functor.{v_1, v_3, u_1, u_3} (Quotient r) E
h : functor r ⋙ F₁ = functor r ⋙ F₂
X Y : C
f_1 : Quiver.Hom (V := Quotient r) (mk (r := r) X) (mk (r := r) Y)
f : as (r := r) (mk (r := r) X) ⟶ as (r := r) (mk (r := r) Y)
⊢ F₁.map (Quot.mk (HomRel.CompClosure r) f) = eqToHom ⋯ ≫ F₂.map (Quot.mk (HomRel.CompClosure r) f) ≫ eqToHom ⋯

Tactic:
Functor.congr_hom h f

Premises used: CategoryTheory.Functor.congr_hom
-- Module: Mathlib.CategoryTheory.Localization.OfQuotient
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
r : HomRel.{u_1, v_1} C
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F₁ F₂ : Functor.{v_1, v_3, u_1, u_3} (Quotient r) E
h : functor r ⋙ F₁ = functor r ⋙ F₂
X Y : C
f_1 : Quiver.Hom (V := Quotient r) (mk (r := r) X) (mk (r := r) Y)
f : as (r := r) (mk (r := r) X) ⟶ as (r := r) (mk (r := r) Y)
⊢ F₁.map (Quot.mk (HomRel.CompClosure r) f) = eqToHom ⋯ ≫ F₂.map (Quot.mk (HomRel.CompClosure r) f) ≫ eqToHom ⋯

Tactic:
exact Functor.congr_hom h f

Premises used: CategoryTheory.Functor.congr_hom
-- Module: Mathlib.CategoryTheory.Localization.OfQuotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
h₁ : Localization.StrictUniversalPropertyFixedTarget (functor r) W (Quotient r)
h₂ : Localization.StrictUniversalPropertyFixedTarget (functor r) W W.Localization
⊢ (functor r).IsLocalization W

Tactic:
apply Functor.IsLocalization.mk'

Premises used: CategoryTheory.Functor.IsLocalization.mk'
-- Module: Mathlib.CategoryTheory.Localization.OfQuotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
⊢ Localization.StrictUniversalPropertyFixedTarget (functor r) W (Quotient r)

Tactic:
apply isLocalization_functor.strictUniversalPropertyFixedTarget hW hr

Premises used: _private.0.CategoryTheory.Quotient.isLocalization_functor.strictUniversalPropertyFixedTarget
-- Module: Mathlib.CategoryTheory.Localization.OfQuotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
⊢ Localization.StrictUniversalPropertyFixedTarget (functor r) W W.Localization

Tactic:
apply isLocalization_functor.strictUniversalPropertyFixedTarget hW hr

Premises used: _private.0.CategoryTheory.Quotient.isLocalization_functor.strictUniversalPropertyFixedTarget
-- Module: Mathlib.CategoryTheory.Localization.OfQuotient
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.EssSurj
inst_3 : L.Full
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy L
hr :
  ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), L.map f₀ = L.map f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
⊢ ∀ (x y : C) (f₁ f₂ : x ⟶ y), L.homRel f₁ f₂ → L.map f₁ = L.map f₂

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Localization.OfQuotient
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.EssSurj
inst_3 : L.Full
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy L
hr :
  ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), L.map f₀ = L.map f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
F : Functor.{v_1, v_2, u_1, u_2} (Quotient L.homRel) D := Quotient.lift L.homRel L ⋯
x x_1 : C
f : x ⟶ x_1
hf : W f
⊢ IsIso (F.map ((Quotient.functor L.homRel).map f))

Tactic:
have : IsIso (F.map ((Quotient.functor L.homRel).map f)) := hW _ hf
-- Module: Mathlib.CategoryTheory.Localization.OfQuotient
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.EssSurj
inst_3 : L.Full
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy L
hr :
  ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), L.map f₀ = L.map f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
F : Functor.{v_1, v_2, u_1, u_2} (Quotient L.homRel) D := Quotient.lift L.homRel L ⋯
x x_1 : C
f : x ⟶ x_1
hf : W f
this : IsIso (F.map ((Quotient.functor L.homRel).map f))
⊢ IsIso ((Quotient.functor L.homRel).map f)

Tactic:
apply isIso_of_reflects_iso _ F

Premises used: CategoryTheory.isIso_of_reflects_iso
-- Module: Mathlib.CategoryTheory.Localization.OfQuotient
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.EssSurj
inst_3 : L.Full
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy L
hr :
  ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), L.map f₀ = L.map f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
F : Functor.{v_1, v_2, u_1, u_2} (Quotient L.homRel) D := Quotient.lift L.homRel L ⋯
⊢ W.IsInvertedBy (Quotient.functor L.homRel)

Tactic:
have hW' : W.IsInvertedBy (Quotient.functor L.homRel) := fun _ _ f hf ↦ by
    have : IsIso (F.map ((Quotient.functor L.homRel).map f)) := hW _ hf
    apply isIso_of_reflects_iso _ F
-- Module: Mathlib.CategoryTheory.Localization.OfQuotient
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.EssSurj
inst_3 : L.Full
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy L
hr :
  ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), L.map f₀ = L.map f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
F : Functor.{v_1, v_2, u_1, u_2} (Quotient L.homRel) D := Quotient.lift L.homRel L ⋯
hW' : W.IsInvertedBy (Quotient.functor L.homRel)
⊢ (Quotient.functor L.homRel).IsLocalization W

Tactic:
have := Quotient.isLocalization_functor L.homRel W hW' hr
-- Module: Mathlib.CategoryTheory.Localization.OfQuotient
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.EssSurj
inst_3 : L.Full
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy L
hr :
  ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), L.map f₀ = L.map f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
F : Functor.{v_1, v_2, u_1, u_2} (Quotient L.homRel) D := Quotient.lift L.homRel L ⋯
hW' : W.IsInvertedBy (Quotient.functor L.homRel)
this : (Quotient.functor L.homRel).IsLocalization W
⊢ L.IsLocalization W

Tactic:
IsLocalization.of_equivalence_target (Quotient.functor L.homRel) W L
    F.asEquivalence (Iso.refl _)

Premises used: CategoryTheory.Quotient.functor, CategoryTheory.Iso.refl, CategoryTheory.Functor.asEquivalence, CategoryTheory.Functor.IsLocalization.of_equivalence_target, CategoryTheory.Functor.homRel
-- Module: Mathlib.CategoryTheory.Localization.OfQuotient
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.EssSurj
inst_3 : L.Full
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy L
hr :
  ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), L.map f₀ = L.map f₁ → ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W P.π
F : Functor.{v_1, v_2, u_1, u_2} (Quotient L.homRel) D := Quotient.lift L.homRel L ⋯
hW' : W.IsInvertedBy (Quotient.functor L.homRel)
this : (Quotient.functor L.homRel).IsLocalization W
⊢ L.IsLocalization W

Tactic:
exact IsLocalization.of_equivalence_target (Quotient.functor L.homRel) W L
    F.asEquivalence (Iso.refl _)

Premises used: CategoryTheory.Quotient.functor, CategoryTheory.Iso.refl, CategoryTheory.Functor.asEquivalence, CategoryTheory.Functor.IsLocalization.of_equivalence_target, CategoryTheory.Functor.homRel
-- Module: Mathlib.CategoryTheory.Localization.OfQuotient
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.EssSurj
inst_3 : L.Full
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy L
hr :
  ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y),
    L.map f₀ = L.map f₁ → ∃ (P : PrepathObject.{v_1, u_1} Y) (x : P.RightHomotopy f₀ f₁), W P.ι
rw : L.op.IsLocalization W.op
⊢ L.IsLocalization W

Tactic:
rw [← Functor.IsLocalization.op_iff]

Premises used: CategoryTheory.Functor.IsLocalization.op_iff
-- Module: Mathlib.CategoryTheory.Localization.OfQuotient
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.EssSurj
inst_3 : L.Full
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy L
hr :
  ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y),
    L.map f₀ = L.map f₁ → ∃ (P : PrepathObject.{v_1, u_1} Y) (x : P.RightHomotopy f₀ f₁), W P.ι
⊢ L.op.IsLocalization W.op

Tactic:
isLocalization_of_essSurj_of_full_of_exists_cylinders L.op W.op hW.op
    (fun X Y f₀ f₁ hf ↦ ?_)

Premises used: CategoryTheory.Functor.op, CategoryTheory.MorphismProperty.op, CategoryTheory.MorphismProperty.IsInvertedBy.op, CategoryTheory.Functor.isLocalization_of_essSurj_of_full_of_exists_cylinders
-- Module: Mathlib.CategoryTheory.Localization.OfQuotient
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.EssSurj
inst_3 : L.Full
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy L
hr :
  ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y),
    L.map f₀ = L.map f₁ → ∃ (P : PrepathObject.{v_1, u_1} Y) (x : P.RightHomotopy f₀ f₁), W P.ι
refine :
  ∀ (X Y : Cᵒᵖ) (f₀ f₁ : X ⟶ Y) (hf : L.op.map f₀ = L.op.map f₁),
    ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W.op P.π
⊢ L.op.IsLocalization W.op

Tactic:
refine isLocalization_of_essSurj_of_full_of_exists_cylinders L.op W.op hW.op
    (fun X Y f₀ f₁ hf ↦ ?_)

Premises used: CategoryTheory.Functor.op, CategoryTheory.MorphismProperty.op, CategoryTheory.MorphismProperty.IsInvertedBy.op, CategoryTheory.Functor.isLocalization_of_essSurj_of_full_of_exists_cylinders
-- Module: Mathlib.CategoryTheory.Localization.OfQuotient
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.EssSurj
inst_3 : L.Full
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy L
hr :
  ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y),
    L.map f₀ = L.map f₁ → ∃ (P : PrepathObject.{v_1, u_1} Y) (x : P.RightHomotopy f₀ f₁), W P.ι
X Y : Cᵒᵖ
f₀ f₁ : X ⟶ Y
hf : L.op.map f₀ = L.op.map f₁
obtain :
  ∀ (P : PrepathObject.{v_1, u_1} (Opposite.unop X)) (h : P.RightHomotopy f₀.unop f₁.unop) (hι : W P.ι),
    ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W.op P.π
⊢ ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W.op P.π

Tactic:
obtain ⟨P, h, hι⟩ := hr f₀.unop f₁.unop (Quiver.Hom.op_inj hf)

Premises used: Quiver.Hom.op_inj, Quiver.Hom.unop
-- Module: Mathlib.CategoryTheory.Localization.OfQuotient
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.EssSurj
inst_3 : L.Full
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy L
hr :
  ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y),
    L.map f₀ = L.map f₁ → ∃ (P : PrepathObject.{v_1, u_1} Y) (x : P.RightHomotopy f₀ f₁), W P.ι
X Y : Cᵒᵖ
f₀ f₁ : X ⟶ Y
hf : L.op.map f₀ = L.op.map f₁
P : PrepathObject.{v_1, u_1} (Opposite.unop X)
h : P.RightHomotopy f₀.unop f₁.unop
hι : W P.ι
⊢ ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W.op P.π

Tactic:
⟨P.op, h.op, hι⟩

Premises used: HomotopicalAlgebra.PrepathObject.op, Exists.intro, HomotopicalAlgebra.PrepathObject.RightHomotopy.op
-- Module: Mathlib.CategoryTheory.Localization.OfQuotient
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.EssSurj
inst_3 : L.Full
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy L
hr :
  ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y),
    L.map f₀ = L.map f₁ → ∃ (P : PrepathObject.{v_1, u_1} Y) (x : P.RightHomotopy f₀ f₁), W P.ι
X Y : Cᵒᵖ
f₀ f₁ : X ⟶ Y
hf : L.op.map f₀ = L.op.map f₁
P : PrepathObject.{v_1, u_1} (Opposite.unop X)
h : P.RightHomotopy f₀.unop f₁.unop
hι : W P.ι
⊢ ∃ (P : Precylinder.{v_1, u_1} X) (x : P.LeftHomotopy f₀ f₁), W.op P.π

Tactic:
exact ⟨P.op, h.op, hι⟩
-- Module: Mathlib.CategoryTheory.Localization.OfQuotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_1 : Congruence r
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ (P : PrepathObject.{v_1, u_1} Y) (x : P.RightHomotopy f₀ f₁), W P.ι
X Y : C
f₀ f₁ : X ⟶ Y
hf : (functor r).map f₀ = (functor r).map f₁
⊢ r f₀ f₁

Tactic:
rw [functor_map_eq_iff] at hf

Premises used: CategoryTheory.Quotient.functor_map_eq_iff
-- Module: Mathlib.CategoryTheory.Localization.OfQuotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_1 : Congruence r
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ (P : PrepathObject.{v_1, u_1} Y) (x : P.RightHomotopy f₀ f₁), W P.ι
X Y : C
f₀ f₁ : X ⟶ Y
hf : r f₀ f₁
⊢ ∃ (P : PrepathObject.{v_1, u_1} Y) (x : P.RightHomotopy f₀ f₁), W P.ι

Tactic:
hr _ _ hf
-- Module: Mathlib.CategoryTheory.Localization.OfQuotient
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
r : HomRel.{u_1, v_1} C
inst_1 : Congruence r
W : MorphismProperty.{v_1, u_1} C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ (P : PrepathObject.{v_1, u_1} Y) (x : P.RightHomotopy f₀ f₁), W P.ι
X Y : C
f₀ f₁ : X ⟶ Y
hf : r f₀ f₁
⊢ ∃ (P : PrepathObject.{v_1, u_1} Y) (x : P.RightHomotopy f₀ f₁), W P.ι

Tactic:
exact hr _ _ hf
-- Module: Mathlib.CategoryTheory.Localization.Opposite
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
h : StrictUniversalPropertyFixedTarget.{v_1, u_1, v_2, u_2, v_3, u_3} L W Eᵒᵖ
F : Functor.{v_1, v_3, u_1, u_3} Cᵒᵖ E
hF : W.op.IsInvertedBy F
⊢ (L ⋙ h.lift (W := W) F.rightOp ⋯).leftOp = F.rightOp.leftOp

Tactic:
congr_arg Functor.leftOp (h.fac F.rightOp hF.rightOp)

Premises used: CategoryTheory.MorphismProperty.IsInvertedBy.rightOp, congr_arg, CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.fac, CategoryTheory.Functor.rightOp, CategoryTheory.Functor.leftOp
-- Module: Mathlib.CategoryTheory.Localization.Opposite
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
h : StrictUniversalPropertyFixedTarget.{v_1, u_1, v_2, u_2, v_3, u_3} L W Eᵒᵖ
F : Functor.{v_1, v_3, u_1, u_3} Cᵒᵖ E
hF : W.op.IsInvertedBy F
⊢ L.op ⋙ (h.lift (W := W) F.rightOp ⋯).leftOp = F

Tactic:
convert! congr_arg Functor.leftOp (h.fac F.rightOp hF.rightOp)

Premises used: CategoryTheory.MorphismProperty.IsInvertedBy.rightOp, congr_arg, CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.fac, CategoryTheory.Functor.rightOp, CategoryTheory.Functor.leftOp
-- Module: Mathlib.CategoryTheory.Localization.Opposite
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
h : StrictUniversalPropertyFixedTarget.{v_1, u_1, v_2, u_2, v_3, u_3} L W Eᵒᵖ
F₁ F₂ : Functor.{v_2, v_3, u_2, u_3} Dᵒᵖ E
eq : L.op ⋙ F₁ = L.op ⋙ F₂
this : F₁.rightOp = F₂.rightOp
rw : F₁.rightOp.leftOp = F₂
rw₁ : F₁.rightOp.leftOp = F₂.rightOp.leftOp
rw₂ rw₃ : F₂.rightOp.leftOp = F₂.rightOp.leftOp
⊢ F₁ = F₂

Tactic:
rw [← F₁.rightOp_leftOp_eq, ← F₂.rightOp_leftOp_eq, this]

Premises used: CategoryTheory.Functor.rightOp_leftOp_eq
-- Module: Mathlib.CategoryTheory.Localization.Opposite
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
h : StrictUniversalPropertyFixedTarget.{v_1, u_1, v_2, u_2, v_3, u_3} L W Eᵒᵖ
F₁ F₂ : Functor.{v_2, v_3, u_2, u_3} Dᵒᵖ E
eq : L.op ⋙ F₁ = L.op ⋙ F₂
suffices : F₁.rightOp = F₂.rightOp
⊢ F₁ = F₂

Tactic:
suffices F₁.rightOp = F₂.rightOp by
      rw [← F₁.rightOp_leftOp_eq, ← F₂.rightOp_leftOp_eq, this]
-- Module: Mathlib.CategoryTheory.Localization.Opposite
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
h : StrictUniversalPropertyFixedTarget.{v_1, u_1, v_2, u_2, v_3, u_3} L W Eᵒᵖ
F₁ F₂ : Functor.{v_2, v_3, u_2, u_3} Dᵒᵖ E
eq : L.op ⋙ F₁ = L.op ⋙ F₂
⊢ (L.op ⋙ F₁).rightOp = (L.op ⋙ F₂).rightOp

Tactic:
have eq' := congr_arg Functor.rightOp eq
-- Module: Mathlib.CategoryTheory.Localization.Opposite
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
h : StrictUniversalPropertyFixedTarget.{v_1, u_1, v_2, u_2, v_3, u_3} L W Eᵒᵖ
F₁ F₂ : Functor.{v_2, v_3, u_2, u_3} Dᵒᵖ E
eq : L.op ⋙ F₁ = L.op ⋙ F₂
eq' : (L.op ⋙ F₁).rightOp = (L.op ⋙ F₂).rightOp
⊢ F₁.rightOp = F₂.rightOp

Tactic:
h.uniq _ _ eq'

Premises used: CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.uniq
-- Module: Mathlib.CategoryTheory.Localization.Opposite
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
h : StrictUniversalPropertyFixedTarget.{v_1, u_1, v_2, u_2, v_3, u_3} L W Eᵒᵖ
F₁ F₂ : Functor.{v_2, v_3, u_2, u_3} Dᵒᵖ E
eq : L.op ⋙ F₁ = L.op ⋙ F₂
eq' : (L.op ⋙ F₁).rightOp = (L.op ⋙ F₂).rightOp
⊢ F₁.rightOp = F₂.rightOp

Tactic:
exact h.uniq _ _ eq'
-- Module: Mathlib.CategoryTheory.Localization.Opposite
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
⊢ W.Q.op.IsLocalization W.op

Tactic:
Functor.IsLocalization.mk' W.Q.op W.op (strictUniversalPropertyFixedTargetQ W _).op
    (strictUniversalPropertyFixedTargetQ W _).op

Premises used: CategoryTheory.Functor.op, CategoryTheory.Localization.strictUniversalPropertyFixedTargetQ, CategoryTheory.MorphismProperty.Q, CategoryTheory.MorphismProperty.op, CategoryTheory.Functor.IsLocalization.mk', CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.op
-- Module: Mathlib.CategoryTheory.Localization.Opposite
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
⊢ L.op.IsLocalization W.op

Tactic:
IsLocalization.of_equivalence_target W.Q.op W.op L.op (Localization.equivalenceFromModel L W).op
    (NatIso.op (Localization.qCompEquivalenceFromModelFunctorIso L W).symm)

Premises used: CategoryTheory.Functor.op, CategoryTheory.MorphismProperty.Q, CategoryTheory.Equivalence.op, CategoryTheory.MorphismProperty.op, CategoryTheory.Localization.equivalenceFromModel, CategoryTheory.Iso.symm, CategoryTheory.NatIso.op, CategoryTheory.Functor.IsLocalization.of_equivalence_target, CategoryTheory.Localization.qCompEquivalenceFromModelFunctorIso
-- Module: Mathlib.CategoryTheory.Localization.Opposite
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_1 : Functor.{v_1, v_2, u_1, u_2} C D
W_1 : MorphismProperty.{v_1, u_1} C
inst_2 : L_1.IsLocalization W_1
L : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ Dᵒᵖ
W : MorphismProperty.{v_1, u_1} Cᵒᵖ
inst_3 : L.IsLocalization W
this : CatCommSq (Equivalence.functor (opOpEquivalence C)) L.op L.unop (Equivalence.functor (opOpEquivalence D))
x x_1 : C
x_2 : x ⟶ x_1
hf : W.unop x_2
⊢ IsIso (L.map x_2.op)

Tactic:
have := Localization.inverts L W _ hf
-- Module: Mathlib.CategoryTheory.Localization.Opposite
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_1 : Functor.{v_1, v_2, u_1, u_2} C D
W_1 : MorphismProperty.{v_1, u_1} C
inst_2 : L_1.IsLocalization W_1
L : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ Dᵒᵖ
W : MorphismProperty.{v_1, u_1} Cᵒᵖ
inst_3 : L.IsLocalization W
this_1 : CatCommSq (Equivalence.functor (opOpEquivalence C)) L.op L.unop (Equivalence.functor (opOpEquivalence D))
x x_1 : C
x_2 : x ⟶ x_1
hf : W.unop x_2
this : IsIso (L.map x_2.op)
dsimp : IsIso (L.map x_2.op).unop
⊢ IsIso (L.unop.map x_2)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Localization.Opposite
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_1 : Functor.{v_1, v_2, u_1, u_2} C D
W_1 : MorphismProperty.{v_1, u_1} C
inst_2 : L_1.IsLocalization W_1
L : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ Dᵒᵖ
W : MorphismProperty.{v_1, u_1} Cᵒᵖ
inst_3 : L.IsLocalization W
this_1 : CatCommSq (Equivalence.functor (opOpEquivalence C)) L.op L.unop (Equivalence.functor (opOpEquivalence D))
x x_1 : C
x_2 : x ⟶ x_1
hf : W.unop x_2
this : IsIso (L.map x_2.op)
⊢ IsIso (L.map x_2.op).unop

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Localization.Opposite
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
⊢ L.op.IsLocalization W.op ↔ L.IsLocalization W

Tactic:
⟨fun _ ↦ inferInstanceAs (L.op.unop.IsLocalization W.op.unop),
    fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro, _private.0.CategoryTheory.Functor.IsLocalization.op_iff._proof_1
-- Module: Mathlib.CategoryTheory.Localization.Opposite
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
X Y : Cᵒᵖ
w : X ⟶ Y
hw : W.op w
w₁ : (isoOfHom L.op W.op w hw).unop.hom = (isoOfHom L W w.unop hw).hom
⊢ (isoOfHom L.op W.op w hw).unop = isoOfHom L W w.unop hw

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Localization.Opposite
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
X Y : Cᵒᵖ
w : X ⟶ Y
hw : W.op w
⊢ (isoOfHom L.op W.op w hw).unop.hom = (isoOfHom L W w.unop hw).hom

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Localization.Opposite
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
X Y : Cᵒᵖ
w : X ⟶ Y
hw : W.op w
⊢ (isoOfHom L.op W.op w hw).inv = (isoOfHom L W w.unop hw).inv.op

Tactic:
congr_arg Quiver.Hom.op (congr_arg Iso.inv (isoOfHom_unop L W w hw))

Premises used: CategoryTheory.Localization.isoOfHom_unop, Quiver.Hom.op, congr_arg, CategoryTheory.Iso.inv