awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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
inst_3 : W.HasLeftCalculusOfFractions
f : Arrow.{v_2, u_2} D
this : L.EssSurj
X : C
eX : L.obj X ≅ f.left
Y : C
eY : L.obj Y ≅ f.right
φ : W.LeftFraction X Y
hφ : eX.hom ≫ f.hom ≫ eY.inv = φ.map (W := W) L ⋯
dsimp : eX.inv ≫ L.map (φ.f (W := W)) = f.hom ≫ eY.inv ≫ L.map (φ.s (W := W))
⊢ eX.symm.hom ≫ (L.mapArrow.obj (Arrow.mk (φ.f (W := W)))).hom = f.hom ≫ (eY.symm ≪≫ isoOfHom L W (φ.s (W := W)) ⋯).hom

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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
inst_3 : W.HasLeftCalculusOfFractions
f : Arrow.{v_2, u_2} D
this : L.EssSurj
X : C
eX : L.obj X ≅ f.left
Y : C
eY : L.obj Y ≅ f.right
φ : W.LeftFraction X Y
hφ : eX.hom ≫ f.hom ≫ eY.inv = φ.map (W := W) L ⋯
⊢ eX.inv ≫ L.map (φ.f (W := W)) = f.hom ≫ eY.inv ≫ L.map (φ.s (W := W))

Tactic:
simp only [← cancel_epi eX.hom, Iso.hom_inv_id_assoc, reassoc_of% hφ,
      MorphismProperty.LeftFraction.map_comp_map_s]

Premises used: CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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
φ : W.RightFraction X Y
L : Functor.{v_1, v_2, u_1, u_2} C D
hL : W.IsInvertedBy L
dsimp :
  Eq.{v_2 + 1} (α := Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
    ((L.map (φ.f (W := W))).op ≫ (inv (L.map (φ.s (W := W)))).op : Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
    ((L.map (φ.f (W := W))).op ≫ inv (L.map (φ.s (W := W))).op : Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
⊢ (φ.map (W := W) L hL).op = φ.op (W := W).map (W := W.op) L.op ⋯

Tactic:
dsimp [map, LeftFraction.map]

Premises used: CategoryTheory.MorphismProperty.RightFraction.map, CategoryTheory.MorphismProperty.LeftFraction.map
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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
φ : W.RightFraction X Y
L : Functor.{v_1, v_2, u_1, u_2} C D
hL : W.IsInvertedBy L
rw rw₁ :
  Eq.{v_2 + 1} (α := Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
    ((L.map (φ.f (W := W))).op ≫ inv (L.map (φ.s (W := W))).op : Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
    ((L.map (φ.f (W := W))).op ≫ inv (L.map (φ.s (W := W))).op : Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
⊢ Eq.{v_2 + 1} (α := Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
    ((L.map (φ.f (W := W))).op ≫ (inv (L.map (φ.s (W := W)))).op : Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
    ((L.map (φ.f (W := W))).op ≫ inv (L.map (φ.s (W := W))).op : Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))

Tactic:
rw [op_inv]

Premises used: CategoryTheory.op_inv
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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
φ : W.LeftFraction X Y
L : Functor.{v_1, v_2, u_1, u_2} C D
hL : W.IsInvertedBy L
dsimp :
  Eq.{v_2 + 1} (α := Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
    ((inv (L.map (φ.s (W := W)))).op ≫ (L.map (φ.f (W := W))).op : Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
    (inv (L.map (φ.s (W := W))).op ≫ (L.map (φ.f (W := W))).op : Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
⊢ (φ.map (W := W) L hL).op = φ.op (W := W).map (W := W.op) L.op ⋯

Tactic:
dsimp [map, RightFraction.map]

Premises used: CategoryTheory.MorphismProperty.RightFraction.map, CategoryTheory.MorphismProperty.LeftFraction.map
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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
φ : W.LeftFraction X Y
L : Functor.{v_1, v_2, u_1, u_2} C D
hL : W.IsInvertedBy L
rw rw₁ :
  Eq.{v_2 + 1} (α := Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
    (inv (L.map (φ.s (W := W))).op ≫ (L.map (φ.f (W := W))).op : Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
    (inv (L.map (φ.s (W := W))).op ≫ (L.map (φ.f (W := W))).op : Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
⊢ Eq.{v_2 + 1} (α := Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
    ((inv (L.map (φ.s (W := W)))).op ≫ (L.map (φ.f (W := W))).op : Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
    (inv (L.map (φ.s (W := W))).op ≫ (L.map (φ.f (W := W))).op : Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))

Tactic:
rw [op_inv]

Premises used: CategoryTheory.op_inv
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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
h : W.HasLeftCalculusOfFractions
X Y : Cᵒᵖ
φ : LeftFraction.{v_1, u_1} W.op X Y
obtain :
  ∀ (ψ : W.LeftFraction (Opposite.unop Y) (Opposite.unop X))
    (eq : φ.unop (W := W.op).f (W := W) ≫ ψ.s (W := W) = φ.unop (W := W.op).s (W := W) ≫ ψ.f (W := W)),
    ∃ (ψ : RightFraction.{v_1, u_1} W.op X Y), ψ.s (W := W.op) ≫ φ.f (W := W.op) = ψ.f (W := W.op) ≫ φ.s (W := W.op)
⊢ ∃ (ψ : RightFraction.{v_1, u_1} W.op X Y), ψ.s (W := W.op) ≫ φ.f (W := W.op) = ψ.f (W := W.op) ≫ φ.s (W := W.op)

Tactic:
obtain ⟨ψ, eq⟩ := h.exists_leftFraction φ.unop

Premises used: CategoryTheory.MorphismProperty.LeftFraction.unop, CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.exists_leftFraction
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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
h : W.HasLeftCalculusOfFractions
X Y : Cᵒᵖ
φ : LeftFraction.{v_1, u_1} W.op X Y
ψ : W.LeftFraction (Opposite.unop Y) (Opposite.unop X)
eq : φ.unop (W := W.op).f (W := W) ≫ ψ.s (W := W) = φ.unop (W := W.op).s (W := W) ≫ ψ.f (W := W)
⊢ ∃ (ψ : RightFraction.{v_1, u_1} W.op X Y), ψ.s (W := W.op) ≫ φ.f (W := W.op) = ψ.f (W := W.op) ≫ φ.s (W := W.op)

Tactic:
⟨ψ.op, Quiver.Hom.unop_inj eq⟩

Premises used: CategoryTheory.MorphismProperty.LeftFraction.op, Quiver.Hom.unop_inj, Exists.intro
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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
h : W.HasLeftCalculusOfFractions
X Y : Cᵒᵖ
φ : LeftFraction.{v_1, u_1} W.op X Y
ψ : W.LeftFraction (Opposite.unop Y) (Opposite.unop X)
eq : φ.unop (W := W.op).f (W := W) ≫ ψ.s (W := W) = φ.unop (W := W.op).s (W := W) ≫ ψ.f (W := W)
⊢ ∃ (ψ : RightFraction.{v_1, u_1} W.op X Y), ψ.s (W := W.op) ≫ φ.f (W := W.op) = ψ.f (W := W.op) ≫ φ.s (W := W.op)

Tactic:
exact ⟨ψ.op, Quiver.Hom.unop_inj eq⟩
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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
h : W.HasLeftCalculusOfFractions
X Y Y' : Cᵒᵖ
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : W.op s
eq : f₁ ≫ s = f₂ ≫ s
obtain :
  ∀ (X' : C) (t : Opposite.unop X ⟶ X') (ht : W t) (fac : f₁.unop ≫ t = f₂.unop ≫ t),
    ∃ (X' : Cᵒᵖ) (t : X' ⟶ X) (_ : W.op t), t ≫ f₁ = t ≫ f₂
⊢ ∃ (X' : Cᵒᵖ) (t : X' ⟶ X) (_ : W.op t), t ≫ f₁ = t ≫ f₂

Tactic:
obtain ⟨X', t, ht, fac⟩ := h.ext f₁.unop f₂.unop s.unop hs (Quiver.Hom.op_inj eq)

Premises used: Quiver.Hom.op_inj, Quiver.Hom.unop, CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.ext
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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
h : W.HasLeftCalculusOfFractions
X Y Y' : Cᵒᵖ
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : W.op s
eq : f₁ ≫ s = f₂ ≫ s
X' : C
t : Opposite.unop X ⟶ X'
ht : W t
fac : f₁.unop ≫ t = f₂.unop ≫ t
⊢ ∃ (X' : Cᵒᵖ) (t : X' ⟶ X) (_ : W.op t), t ≫ f₁ = t ≫ f₂

Tactic:
⟨Opposite.op X', t.op, ht, Quiver.Hom.unop_inj fac⟩

Premises used: Quiver.Hom.op, Quiver.Hom.unop_inj, Opposite.op, Exists.intro
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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
h : W.HasLeftCalculusOfFractions
X Y Y' : Cᵒᵖ
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : W.op s
eq : f₁ ≫ s = f₂ ≫ s
X' : C
t : Opposite.unop X ⟶ X'
ht : W t
fac : f₁.unop ≫ t = f₂.unop ≫ t
⊢ ∃ (X' : Cᵒᵖ) (t : X' ⟶ X) (_ : W.op t), t ≫ f₁ = t ≫ f₂

Tactic:
exact ⟨Opposite.op X', t.op, ht, Quiver.Hom.unop_inj fac⟩
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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
h : W.HasRightCalculusOfFractions
X Y : Cᵒᵖ
φ : RightFraction.{v_1, u_1} W.op X Y
obtain :
  ∀ (ψ : W.RightFraction (Opposite.unop Y) (Opposite.unop X))
    (eq : ψ.s (W := W) ≫ φ.unop (W := W.op).f (W := W) = ψ.f (W := W) ≫ φ.unop (W := W.op).s (W := W)),
    ∃ (ψ : LeftFraction.{v_1, u_1} W.op X Y), φ.f (W := W.op) ≫ ψ.s (W := W.op) = φ.s (W := W.op) ≫ ψ.f (W := W.op)
⊢ ∃ (ψ : LeftFraction.{v_1, u_1} W.op X Y), φ.f (W := W.op) ≫ ψ.s (W := W.op) = φ.s (W := W.op) ≫ ψ.f (W := W.op)

Tactic:
obtain ⟨ψ, eq⟩ := h.exists_rightFraction φ.unop

Premises used: CategoryTheory.MorphismProperty.RightFraction.unop, CategoryTheory.MorphismProperty.HasRightCalculusOfFractions.exists_rightFraction
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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
h : W.HasRightCalculusOfFractions
X Y : Cᵒᵖ
φ : RightFraction.{v_1, u_1} W.op X Y
ψ : W.RightFraction (Opposite.unop Y) (Opposite.unop X)
eq : ψ.s (W := W) ≫ φ.unop (W := W.op).f (W := W) = ψ.f (W := W) ≫ φ.unop (W := W.op).s (W := W)
⊢ ∃ (ψ : LeftFraction.{v_1, u_1} W.op X Y), φ.f (W := W.op) ≫ ψ.s (W := W.op) = φ.s (W := W.op) ≫ ψ.f (W := W.op)

Tactic:
⟨ψ.op, Quiver.Hom.unop_inj eq⟩

Premises used: CategoryTheory.MorphismProperty.RightFraction.op, Quiver.Hom.unop_inj, Exists.intro
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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
h : W.HasRightCalculusOfFractions
X Y : Cᵒᵖ
φ : RightFraction.{v_1, u_1} W.op X Y
ψ : W.RightFraction (Opposite.unop Y) (Opposite.unop X)
eq : ψ.s (W := W) ≫ φ.unop (W := W.op).f (W := W) = ψ.f (W := W) ≫ φ.unop (W := W.op).s (W := W)
⊢ ∃ (ψ : LeftFraction.{v_1, u_1} W.op X Y), φ.f (W := W.op) ≫ ψ.s (W := W.op) = φ.s (W := W.op) ≫ ψ.f (W := W.op)

Tactic:
exact ⟨ψ.op, Quiver.Hom.unop_inj eq⟩
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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
h : W.HasRightCalculusOfFractions
X' X Y : Cᵒᵖ
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : W.op s
eq : s ≫ f₁ = s ≫ f₂
obtain :
  ∀ (Y' : C) (t : Y' ⟶ Opposite.unop Y) (ht : W t) (fac : t ≫ f₁.unop = t ≫ f₂.unop),
    ∃ (Y' : Cᵒᵖ) (t : Y ⟶ Y') (_ : W.op t), f₁ ≫ t = f₂ ≫ t
⊢ ∃ (Y' : Cᵒᵖ) (t : Y ⟶ Y') (_ : W.op t), f₁ ≫ t = f₂ ≫ t

Tactic:
obtain ⟨Y', t, ht, fac⟩ := h.ext f₁.unop f₂.unop s.unop hs (Quiver.Hom.op_inj eq)

Premises used: Quiver.Hom.op_inj, Quiver.Hom.unop, CategoryTheory.MorphismProperty.HasRightCalculusOfFractions.ext
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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
h : W.HasRightCalculusOfFractions
X' X Y : Cᵒᵖ
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : W.op s
eq : s ≫ f₁ = s ≫ f₂
Y' : C
t : Y' ⟶ Opposite.unop Y
ht : W t
fac : t ≫ f₁.unop = t ≫ f₂.unop
⊢ ∃ (Y' : Cᵒᵖ) (t : Y ⟶ Y') (_ : W.op t), f₁ ≫ t = f₂ ≫ t

Tactic:
⟨Opposite.op Y', t.op, ht, Quiver.Hom.unop_inj fac⟩

Premises used: Quiver.Hom.op, Quiver.Hom.unop_inj, Opposite.op, Exists.intro
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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
h : W.HasRightCalculusOfFractions
X' X Y : Cᵒᵖ
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : W.op s
eq : s ≫ f₁ = s ≫ f₂
Y' : C
t : Y' ⟶ Opposite.unop Y
ht : W t
fac : t ≫ f₁.unop = t ≫ f₂.unop
⊢ ∃ (Y' : Cᵒᵖ) (t : Y ⟶ Y') (_ : W.op t), f₁ ≫ t = f₂ ≫ t

Tactic:
exact ⟨Opposite.op Y', t.op, ht, Quiver.Hom.unop_inj fac⟩
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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_1 : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W_1
W : MorphismProperty.{v_1, u_1} Cᵒᵖ
h : HasLeftCalculusOfFractions.{v_1, u_1} (C := Cᵒᵖ) W
X Y : C
φ : W.unop.LeftFraction X Y
obtain :
  ∀ (ψ : LeftFraction.{v_1, u_1} W (Opposite.op Y) (Opposite.op X))
    (eq : φ.op (W := W.unop).f (W := W) ≫ ψ.s (W := W) = φ.op (W := W.unop).s (W := W) ≫ ψ.f (W := W)),
    ∃ (ψ : W.unop.RightFraction X Y), ψ.s (W := W.unop) ≫ φ.f (W := W.unop) = ψ.f (W := W.unop) ≫ φ.s (W := W.unop)
⊢ ∃ (ψ : W.unop.RightFraction X Y), ψ.s (W := W.unop) ≫ φ.f (W := W.unop) = ψ.f (W := W.unop) ≫ φ.s (W := W.unop)

Tactic:
obtain ⟨ψ, eq⟩ := h.exists_leftFraction φ.op

Premises used: CategoryTheory.MorphismProperty.LeftFraction.op, CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.exists_leftFraction
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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_1 : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W_1
W : MorphismProperty.{v_1, u_1} Cᵒᵖ
h : HasLeftCalculusOfFractions.{v_1, u_1} (C := Cᵒᵖ) W
X Y : C
φ : W.unop.LeftFraction X Y
ψ : LeftFraction.{v_1, u_1} W (Opposite.op Y) (Opposite.op X)
eq : φ.op (W := W.unop).f (W := W) ≫ ψ.s (W := W) = φ.op (W := W.unop).s (W := W) ≫ ψ.f (W := W)
⊢ ∃ (ψ : W.unop.RightFraction X Y), ψ.s (W := W.unop) ≫ φ.f (W := W.unop) = ψ.f (W := W.unop) ≫ φ.s (W := W.unop)

Tactic:
⟨ψ.unop, Quiver.Hom.op_inj eq⟩

Premises used: CategoryTheory.MorphismProperty.LeftFraction.unop, Quiver.Hom.op_inj, Exists.intro
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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_1 : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W_1
W : MorphismProperty.{v_1, u_1} Cᵒᵖ
h : HasLeftCalculusOfFractions.{v_1, u_1} (C := Cᵒᵖ) W
X Y : C
φ : W.unop.LeftFraction X Y
ψ : LeftFraction.{v_1, u_1} W (Opposite.op Y) (Opposite.op X)
eq : φ.op (W := W.unop).f (W := W) ≫ ψ.s (W := W) = φ.op (W := W.unop).s (W := W) ≫ ψ.f (W := W)
⊢ ∃ (ψ : W.unop.RightFraction X Y), ψ.s (W := W.unop) ≫ φ.f (W := W.unop) = ψ.f (W := W.unop) ≫ φ.s (W := W.unop)

Tactic:
exact ⟨ψ.unop, Quiver.Hom.op_inj eq⟩
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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_1 : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W_1
W : MorphismProperty.{v_1, u_1} Cᵒᵖ
h : HasLeftCalculusOfFractions.{v_1, u_1} (C := Cᵒᵖ) W
X Y Y' : C
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : W.unop s
eq : f₁ ≫ s = f₂ ≫ s
obtain :
  ∀ (X' : Cᵒᵖ) (t : Opposite.op X ⟶ X') (ht : W t) (fac : Eq (α := Opposite.op Y ⟶ X') (f₁.op ≫ t) (f₂.op ≫ t)),
    ∃ (X' : C) (t : X' ⟶ X) (_ : W.unop t), t ≫ f₁ = t ≫ f₂
⊢ ∃ (X' : C) (t : X' ⟶ X) (_ : W.unop t), t ≫ f₁ = t ≫ f₂

Tactic:
obtain ⟨X', t, ht, fac⟩ := h.ext f₁.op f₂.op s.op hs (Quiver.Hom.unop_inj eq)

Premises used: Quiver.Hom.op, CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.ext, Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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_1 : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W_1
W : MorphismProperty.{v_1, u_1} Cᵒᵖ
h : HasLeftCalculusOfFractions.{v_1, u_1} (C := Cᵒᵖ) W
X Y Y' : C
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : W.unop s
eq : f₁ ≫ s = f₂ ≫ s
X' : Cᵒᵖ
t : Opposite.op X ⟶ X'
ht : W t
fac : Eq (α := Opposite.op Y ⟶ X') (f₁.op ≫ t) (f₂.op ≫ t)
⊢ ∃ (X' : C) (t : X' ⟶ X) (_ : W.unop t), t ≫ f₁ = t ≫ f₂

Tactic:
⟨Opposite.unop X', t.unop, ht, Quiver.Hom.op_inj fac⟩

Premises used: Quiver.Hom.op_inj, Quiver.Hom.unop, Exists.intro, Opposite.unop
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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_1 : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W_1
W : MorphismProperty.{v_1, u_1} Cᵒᵖ
h : HasLeftCalculusOfFractions.{v_1, u_1} (C := Cᵒᵖ) W
X Y Y' : C
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : W.unop s
eq : f₁ ≫ s = f₂ ≫ s
X' : Cᵒᵖ
t : Opposite.op X ⟶ X'
ht : W t
fac : Eq (α := Opposite.op Y ⟶ X') (f₁.op ≫ t) (f₂.op ≫ t)
⊢ ∃ (X' : C) (t : X' ⟶ X) (_ : W.unop t), t ≫ f₁ = t ≫ f₂

Tactic:
exact ⟨Opposite.unop X', t.unop, ht, Quiver.Hom.op_inj fac⟩
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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_1 : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W_1
W : MorphismProperty.{v_1, u_1} Cᵒᵖ
h : HasRightCalculusOfFractions.{v_1, u_1} (C := Cᵒᵖ) W
X Y : C
φ : W.unop.RightFraction X Y
obtain :
  ∀ (ψ : RightFraction.{v_1, u_1} W (Opposite.op Y) (Opposite.op X))
    (eq : ψ.s (W := W) ≫ φ.op (W := W.unop).f (W := W) = ψ.f (W := W) ≫ φ.op (W := W.unop).s (W := W)),
    ∃ (ψ : W.unop.LeftFraction X Y), φ.f (W := W.unop) ≫ ψ.s (W := W.unop) = φ.s (W := W.unop) ≫ ψ.f (W := W.unop)
⊢ ∃ (ψ : W.unop.LeftFraction X Y), φ.f (W := W.unop) ≫ ψ.s (W := W.unop) = φ.s (W := W.unop) ≫ ψ.f (W := W.unop)

Tactic:
obtain ⟨ψ, eq⟩ := h.exists_rightFraction φ.op

Premises used: CategoryTheory.MorphismProperty.RightFraction.op, CategoryTheory.MorphismProperty.HasRightCalculusOfFractions.exists_rightFraction
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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_1 : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W_1
W : MorphismProperty.{v_1, u_1} Cᵒᵖ
h : HasRightCalculusOfFractions.{v_1, u_1} (C := Cᵒᵖ) W
X Y : C
φ : W.unop.RightFraction X Y
ψ : RightFraction.{v_1, u_1} W (Opposite.op Y) (Opposite.op X)
eq : ψ.s (W := W) ≫ φ.op (W := W.unop).f (W := W) = ψ.f (W := W) ≫ φ.op (W := W.unop).s (W := W)
⊢ ∃ (ψ : W.unop.LeftFraction X Y), φ.f (W := W.unop) ≫ ψ.s (W := W.unop) = φ.s (W := W.unop) ≫ ψ.f (W := W.unop)

Tactic:
⟨ψ.unop, Quiver.Hom.op_inj eq⟩

Premises used: Quiver.Hom.op_inj, CategoryTheory.MorphismProperty.RightFraction.unop, Exists.intro
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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_1 : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W_1
W : MorphismProperty.{v_1, u_1} Cᵒᵖ
h : HasRightCalculusOfFractions.{v_1, u_1} (C := Cᵒᵖ) W
X Y : C
φ : W.unop.RightFraction X Y
ψ : RightFraction.{v_1, u_1} W (Opposite.op Y) (Opposite.op X)
eq : ψ.s (W := W) ≫ φ.op (W := W.unop).f (W := W) = ψ.f (W := W) ≫ φ.op (W := W.unop).s (W := W)
⊢ ∃ (ψ : W.unop.LeftFraction X Y), φ.f (W := W.unop) ≫ ψ.s (W := W.unop) = φ.s (W := W.unop) ≫ ψ.f (W := W.unop)

Tactic:
exact ⟨ψ.unop, Quiver.Hom.op_inj eq⟩
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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_1 : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W_1
W : MorphismProperty.{v_1, u_1} Cᵒᵖ
h : HasRightCalculusOfFractions.{v_1, u_1} (C := Cᵒᵖ) W
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : W.unop s
eq : s ≫ f₁ = s ≫ f₂
obtain :
  ∀ (Y' : Cᵒᵖ) (t : Y' ⟶ Opposite.op Y) (ht : W t) (fac : t ≫ f₁.op = t ≫ f₂.op),
    ∃ (Y' : C) (t : Y ⟶ Y') (_ : W.unop t), f₁ ≫ t = f₂ ≫ t
⊢ ∃ (Y' : C) (t : Y ⟶ Y') (_ : W.unop t), f₁ ≫ t = f₂ ≫ t

Tactic:
obtain ⟨Y', t, ht, fac⟩ := h.ext f₁.op f₂.op s.op hs (Quiver.Hom.unop_inj eq)

Premises used: Quiver.Hom.op, CategoryTheory.MorphismProperty.HasRightCalculusOfFractions.ext, Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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_1 : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W_1
W : MorphismProperty.{v_1, u_1} Cᵒᵖ
h : HasRightCalculusOfFractions.{v_1, u_1} (C := Cᵒᵖ) W
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : W.unop s
eq : s ≫ f₁ = s ≫ f₂
Y' : Cᵒᵖ
t : Y' ⟶ Opposite.op Y
ht : W t
fac : t ≫ f₁.op = t ≫ f₂.op
⊢ ∃ (Y' : C) (t : Y ⟶ Y') (_ : W.unop t), f₁ ≫ t = f₂ ≫ t

Tactic:
⟨Opposite.unop Y', t.unop, ht, Quiver.Hom.op_inj fac⟩

Premises used: Quiver.Hom.op_inj, Quiver.Hom.unop, Exists.intro, Opposite.unop
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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_1 : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W_1
W : MorphismProperty.{v_1, u_1} Cᵒᵖ
h : HasRightCalculusOfFractions.{v_1, u_1} (C := Cᵒᵖ) W
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : W.unop s
eq : s ≫ f₁ = s ≫ f₂
Y' : Cᵒᵖ
t : Y' ⟶ Opposite.op Y
ht : W t
fac : t ≫ f₁.op = t ≫ f₂.op
⊢ ∃ (Y' : C) (t : Y ⟶ Y') (_ : W.unop t), f₁ ≫ t = f₂ ≫ t

Tactic:
exact ⟨Opposite.unop Y', t.unop, ht, Quiver.Hom.op_inj fac⟩
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z₁ z₂ : W.RightFraction X Y
h : RightFractionRel (W := W) z₁ z₂
obtain :
  ∀ (Z : C) (t₁ : Z ⟶ z₁.X' (W := W)) (t₂ : Z ⟶ z₂.X' (W := W)) (hs : t₁ ≫ z₁.s (W := W) = t₂ ≫ z₂.s (W := W))
    (hf : t₁ ≫ z₁.f (W := W) = t₂ ≫ z₂.f (W := W)) (ht : W (t₁ ≫ z₁.s (W := W))),
    LeftFractionRel (W := W.op) (z₁.op (W := W)) (z₂.op (W := W))
⊢ LeftFractionRel (W := W.op) (z₁.op (W := W)) (z₂.op (W := W))

Tactic:
obtain ⟨Z, t₁, t₂, hs, hf, ht⟩ := h
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z₁ z₂ : W.RightFraction X Y
Z : C
t₁ : Z ⟶ z₁.X' (W := W)
t₂ : Z ⟶ z₂.X' (W := W)
hs : t₁ ≫ z₁.s (W := W) = t₂ ≫ z₂.s (W := W)
hf : t₁ ≫ z₁.f (W := W) = t₂ ≫ z₂.f (W := W)
ht : W (t₁ ≫ z₁.s (W := W))
⊢ LeftFractionRel (W := W.op) (z₁.op (W := W)) (z₂.op (W := W))

Tactic:
⟨Opposite.op Z, t₁.op, t₂.op, Quiver.Hom.unop_inj hs,
    Quiver.Hom.unop_inj hf, ht⟩

Premises used: Quiver.Hom.op, CategoryTheory.MorphismProperty.LeftFractionRel, Quiver.Hom.unop_inj, Opposite.op, Exists.intro