awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact ⟨Opposite.op Z, t₁.op, t₂.op, Quiver.Hom.unop_inj hs,
    Quiver.Hom.unop_inj hf, ht⟩
-- 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₂ : RightFraction.{v_1, u_1} W 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.unop) (z₁.unop (W := W)) (z₂.unop (W := W))
⊢ LeftFractionRel (W := W.unop) (z₁.unop (W := W)) (z₂.unop (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₂ : RightFraction.{v_1, u_1} W 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.unop) (z₁.unop (W := W)) (z₂.unop (W := W))

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

Premises used: Quiver.Hom.op_inj, Quiver.Hom.unop, CategoryTheory.MorphismProperty.LeftFractionRel, Exists.intro, Opposite.unop
-- 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₂ : RightFraction.{v_1, u_1} W 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.unop) (z₁.unop (W := W)) (z₂.unop (W := W))

Tactic:
exact ⟨Opposite.unop Z, t₁.unop, t₂.unop, Quiver.Hom.op_inj hs,
    Quiver.Hom.op_inj hf, ht⟩
-- 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.LeftFraction X Y
h : LeftFractionRel (W := W) z₁ z₂
obtain :
  ∀ (Z : C) (t₁ : z₁.Y' (W := W) ⟶ Z) (t₂ : z₂.Y' (W := W) ⟶ Z) (hs : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂)
    (hf : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂) (ht : W (z₁.s (W := W) ≫ t₁)),
    RightFractionRel (W := W.op) (z₁.op (W := W)) (z₂.op (W := W))
⊢ RightFractionRel (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.LeftFraction X Y
Z : C
t₁ : z₁.Y' (W := W) ⟶ Z
t₂ : z₂.Y' (W := W) ⟶ Z
hs : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hf : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
⊢ RightFractionRel (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, Quiver.Hom.unop_inj, Opposite.op, Exists.intro, CategoryTheory.MorphismProperty.RightFractionRel
-- 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.LeftFraction X Y
Z : C
t₁ : z₁.Y' (W := W) ⟶ Z
t₂ : z₂.Y' (W := W) ⟶ Z
hs : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hf : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
⊢ RightFractionRel (W := W.op) (z₁.op (W := W)) (z₂.op (W := W))

Tactic:
exact ⟨Opposite.op Z, t₁.op, t₂.op, Quiver.Hom.unop_inj hs,
    Quiver.Hom.unop_inj hf, ht⟩
-- 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₂ : LeftFraction.{v_1, u_1} W X Y
h : LeftFractionRel (W := W) z₁ z₂
obtain :
  ∀ (Z : Cᵒᵖ) (t₁ : z₁.Y' (W := W) ⟶ Z) (t₂ : z₂.Y' (W := W) ⟶ Z) (hs : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂)
    (hf : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂) (ht : W (z₁.s (W := W) ≫ t₁)),
    RightFractionRel (W := W.unop) (z₁.unop (W := W)) (z₂.unop (W := W))
⊢ RightFractionRel (W := W.unop) (z₁.unop (W := W)) (z₂.unop (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₂ : LeftFraction.{v_1, u_1} W X Y
Z : Cᵒᵖ
t₁ : z₁.Y' (W := W) ⟶ Z
t₂ : z₂.Y' (W := W) ⟶ Z
hs : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hf : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
⊢ RightFractionRel (W := W.unop) (z₁.unop (W := W)) (z₂.unop (W := W))

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

Premises used: Quiver.Hom.op_inj, Quiver.Hom.unop, Exists.intro, CategoryTheory.MorphismProperty.RightFractionRel, Opposite.unop
-- 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₂ : LeftFraction.{v_1, u_1} W X Y
Z : Cᵒᵖ
t₁ : z₁.Y' (W := W) ⟶ Z
t₂ : z₂.Y' (W := W) ⟶ Z
hs : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hf : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
⊢ RightFractionRel (W := W.unop) (z₁.unop (W := W)) (z₂.unop (W := W))

Tactic:
exact ⟨Opposite.unop Z, t₁.unop, t₂.unop, Quiver.Hom.op_inj hs,
    Quiver.Hom.op_inj hf, ht⟩
-- 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
⊢ LeftFractionRel (W := W.op) (z₁.op (W := W)) (z₂.op (W := W)) ↔ RightFractionRel (W := W) z₁ z₂

Tactic:
⟨fun h => h.unop, fun h => h.op⟩

Premises used: CategoryTheory.MorphismProperty.LeftFractionRel.unop, CategoryTheory.MorphismProperty.RightFractionRel.op, Iff.intro
-- 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.LeftFraction X Y
⊢ RightFractionRel (W := W.op) (z₁.op (W := W)) (z₂.op (W := W)) ↔ LeftFractionRel (W := W) z₁ z₂

Tactic:
⟨fun h => h.unop, fun h => h.op⟩

Premises used: CategoryTheory.MorphismProperty.RightFractionRel.unop, Iff.intro, CategoryTheory.MorphismProperty.LeftFractionRel.op
-- 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 : W.RightFraction X Y
⊢ RightFractionRel (W := W) z z

Tactic:
(LeftFractionRel.refl z.op).unop

Premises used: CategoryTheory.MorphismProperty.LeftFractionRel.unop, CategoryTheory.MorphismProperty.LeftFraction.unop, CategoryTheory.MorphismProperty.unop, Quiver.Hom.unop, CategoryTheory.MorphismProperty.op, CategoryTheory.MorphismProperty.RightFraction.op, CategoryTheory.MorphismProperty.LeftFractionRel.refl
-- 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₂
⊢ RightFractionRel (W := W) z₂ z₁

Tactic:
h.op.symm.unop

Premises used: CategoryTheory.MorphismProperty.LeftFractionRel.unop, CategoryTheory.MorphismProperty.LeftFraction.unop, CategoryTheory.MorphismProperty.unop, Quiver.Hom.unop, CategoryTheory.MorphismProperty.RightFractionRel.op, CategoryTheory.MorphismProperty.op, CategoryTheory.MorphismProperty.LeftFractionRel.symm
-- 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₂ z₃ : W.RightFraction X Y
inst_1 : W.HasRightCalculusOfFractions
h₁₂ : RightFractionRel (W := W) z₁ z₂
h₂₃ : RightFractionRel (W := W) z₂ z₃
⊢ RightFractionRel (W := W) z₁ z₃

Tactic:
(h₁₂.op.trans h₂₃.op).unop

Premises used: CategoryTheory.MorphismProperty.LeftFractionRel.unop, CategoryTheory.MorphismProperty.LeftFraction.unop, CategoryTheory.MorphismProperty.unop, Quiver.Hom.unop, CategoryTheory.MorphismProperty.RightFractionRel.op, CategoryTheory.MorphismProperty.op, CategoryTheory.MorphismProperty.LeftFractionRel.trans
-- 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.HasRightCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
obtain :
  ∀ (φ : MorphismProperty.LeftFraction.{v_1, u_1} W.op (Opposite.op Y) (Opposite.op X))
    (eq : f.op = φ.map (W := W.op) L.op ⋯), ∃ (φ : W.RightFraction X Y), f = φ.map (W := W) L ⋯
⊢ ∃ (φ : W.RightFraction X Y), f = φ.map (W := W) L ⋯

Tactic:
obtain ⟨φ, eq⟩ := Localization.exists_leftFraction L.op W.op f.op

Premises used: CategoryTheory.Functor.op, Quiver.Hom.op, CategoryTheory.MorphismProperty.op, CategoryTheory.Localization.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
inst_3 : W.HasRightCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
φ : MorphismProperty.LeftFraction.{v_1, u_1} W.op (Opposite.op Y) (Opposite.op X)
eq : f.op = φ.map (W := W.op) L.op ⋯
⊢ ∃ (φ : W.RightFraction X Y), f = φ.map (W := W) L ⋯

Tactic:
⟨φ.unop, Quiver.Hom.op_inj ?_⟩

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 : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasRightCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
φ : MorphismProperty.LeftFraction.{v_1, u_1} W.op (Opposite.op Y) (Opposite.op X)
eq : f.op = φ.map (W := W.op) L.op ⋯
refine : f.op = (φ.unop (W := W.op).map (W := W) L ⋯).op
⊢ ∃ (φ : W.RightFraction X Y), f = φ.map (W := W) L ⋯

Tactic:
refine ⟨φ.unop, Quiver.Hom.op_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 : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasRightCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
φ : MorphismProperty.LeftFraction.{v_1, u_1} W.op (Opposite.op Y) (Opposite.op X)
eq : f.op = φ.map (W := W.op) L.op ⋯
rw : φ.map (W := W.op) L.op ⋯ = φ.unop (W := W.op).op (W := W).map (W := W.op) L.op ⋯
⊢ f.op = (φ.unop (W := W.op).map (W := W) L ⋯).op

Tactic:
rw [eq, MorphismProperty.RightFraction.op_map]

Premises used: CategoryTheory.MorphismProperty.RightFraction.op_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
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.HasRightCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
φ : MorphismProperty.LeftFraction.{v_1, u_1} W.op (Opposite.op Y) (Opposite.op X)
eq : f.op = φ.map (W := W.op) L.op ⋯
⊢ φ.map (W := W.op) L.op ⋯ = φ.unop (W := W.op).op (W := W).map (W := W.op) L.op ⋯

Tactic:
rfl
-- 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.HasRightCalculusOfFractions
X Y : C
φ ψ : W.RightFraction X Y
rw : φ.map (W := W) L ⋯ = ψ.map (W := W) L ⋯ ↔ (φ.map (W := W) L ⋯).op = (ψ.map (W := W) L ⋯).op
⊢ φ.map (W := W) L ⋯ = ψ.map (W := W) L ⋯ ↔ RightFractionRel (W := W) φ ψ

Tactic:
rw [← leftFractionRel_op_iff, ← LeftFraction.map_eq_iff L.op W.op φ.op ψ.op,
    ← φ.op_map L (Localization.inverts _ _), ← ψ.op_map L (Localization.inverts _ _)]

Premises used: CategoryTheory.Functor.op, CategoryTheory.MorphismProperty.op, CategoryTheory.MorphismProperty.LeftFraction.map_eq_iff, CategoryTheory.MorphismProperty.RightFraction.op_map, CategoryTheory.MorphismProperty.RightFraction.op, CategoryTheory.MorphismProperty.leftFractionRel_op_iff, CategoryTheory.Localization.inverts
-- 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.HasRightCalculusOfFractions
X Y : C
φ ψ : W.RightFraction X Y
mp : φ.map (W := W) L ⋯ = ψ.map (W := W) L ⋯ → (φ.map (W := W) L ⋯).op = (ψ.map (W := W) L ⋯).op
mpr : (φ.map (W := W) L ⋯).op = (ψ.map (W := W) L ⋯).op → φ.map (W := W) L ⋯ = ψ.map (W := W) L ⋯
⊢ φ.map (W := W) L ⋯ = ψ.map (W := W) L ⋯ ↔ (φ.map (W := W) L ⋯).op = (ψ.map (W := W) L ⋯).op

Tactic:
constructor
-- 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.HasRightCalculusOfFractions
X Y : C
φ ψ : W.RightFraction X Y
⊢ φ.map (W := W) L ⋯ = ψ.map (W := W) L ⋯ → (φ.map (W := W) L ⋯).op = (ψ.map (W := W) L ⋯).op

Tactic:
apply Quiver.Hom.unop_inj

Premises used: 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 : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasRightCalculusOfFractions
X Y : C
φ ψ : W.RightFraction X Y
⊢ (φ.map (W := W) L ⋯).op = (ψ.map (W := W) L ⋯).op → φ.map (W := W) L ⋯ = ψ.map (W := W) L ⋯

Tactic:
apply Quiver.Hom.op_inj

Premises used: Quiver.Hom.op_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 : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasRightCalculusOfFractions
Y Z : C
f₁ f₂ : Y ⟶ Z
mp : L.map f₁ = L.map f₂ → ∃ (X : C) (s : X ⟶ Y) (_ : W s), s ≫ f₁ = s ≫ f₂
mpr : (∃ (X : C) (s : X ⟶ Y) (_ : W s), s ≫ f₁ = s ≫ f₂) → L.map f₁ = L.map f₂
⊢ L.map f₁ = L.map f₂ ↔ ∃ (X : C) (s : X ⟶ Y) (_ : W s), s ≫ f₁ = s ≫ f₂

Tactic:
constructor
-- 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.HasRightCalculusOfFractions
Y Z : C
f₁ f₂ : Y ⟶ Z
h : L.map f₁ = L.map f₂
⊢ RightFractionRel (W := W) (RightFraction.ofHom W f₁) (RightFraction.ofHom W f₂)

Tactic:
rw [← RightFraction.map_ofHom W _ L (Localization.inverts _ _),
      ← RightFraction.map_ofHom W _ L (Localization.inverts _ _),
      RightFraction.map_eq_iff] at h

Premises used: CategoryTheory.MorphismProperty.RightFraction.map_eq_iff, CategoryTheory.MorphismProperty.RightFraction.map_ofHom, CategoryTheory.Localization.inverts
-- 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.HasRightCalculusOfFractions
Y Z : C
f₁ f₂ : Y ⟶ Z
h : RightFractionRel (W := W) (RightFraction.ofHom W f₁) (RightFraction.ofHom W f₂)
mp :
  ∀ (Z_1 : C) (t₁ : Z_1 ⟶ (RightFraction.ofHom W f₁).X' (W := W)) (t₂ : Z_1 ⟶ (RightFraction.ofHom W f₂).X' (W := W))
    (hst : t₁ ≫ (RightFraction.ofHom W f₁).s (W := W) = t₂ ≫ (RightFraction.ofHom W f₂).s (W := W))
    (hft : t₁ ≫ (RightFraction.ofHom W f₁).f (W := W) = t₂ ≫ (RightFraction.ofHom W f₂).f (W := W))
    (ht : W (t₁ ≫ (RightFraction.ofHom W f₁).s (W := W))), ∃ (X : C) (s : X ⟶ Y) (_ : W s), s ≫ f₁ = s ≫ f₂
⊢ ∃ (X : C) (s : X ⟶ Y) (_ : W s), s ≫ f₁ = s ≫ f₂

Tactic:
obtain ⟨Z, t₁, t₂, hst, hft, ht⟩ := h
-- 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.HasRightCalculusOfFractions
Y Z_1 : C
f₁ f₂ : Y ⟶ Z_1
Z : C
t₁ t₂ : Z ⟶ Y
hst : t₁ ≫ 𝟙 Y = t₂ ≫ 𝟙 Y
hft : t₁ ≫ f₁ = t₂ ≫ f₂
ht : W (t₁ ≫ 𝟙 Y)
⊢ ∃ (X : C) (s : X ⟶ Y) (_ : W s), s ≫ f₁ = s ≫ f₂

Tactic:
grind
-- 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.HasRightCalculusOfFractions
Y Z_1 : C
f₁ f₂ : Y ⟶ Z_1
Z : C
s : Z ⟶ Y
hs : W s
fac : s ≫ f₁ = s ≫ f₂
⊢ L.map f₁ = L.map f₂

Tactic:
simp only [← cancel_epi (Localization.isoOfHom L W s hs).hom,
      Localization.isoOfHom_hom, ← L.map_comp, fac]

Premises used: CategoryTheory.Localization.isoOfHom_hom, CategoryTheory.Localization.isoOfHom, CategoryTheory.Functor.map_comp, 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
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.HasRightCalculusOfFractions
f : Arrow.{v_2, u_2} D
⊢ L.op.mapArrow.EssSurj

Tactic:
have := Localization.essSurj_mapArrow L.op W.op
-- 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.HasRightCalculusOfFractions
f : Arrow.{v_2, u_2} D
this : L.op.mapArrow.EssSurj
⊢ ∃ (g : Arrow.{v_1, u_1} Cᵒᵖ), Nonempty.{v_2 + 1} (L.op.mapArrow.obj g ≅ Arrow.mk f.hom.op)

Tactic:
⟨_, ⟨Functor.objObjPreimageIso _ _⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Functor.objObjPreimageIso, 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
inst_3 : W.HasRightCalculusOfFractions
f : Arrow.{v_2, u_2} D
this : L.op.mapArrow.EssSurj
obtain : ∀ (g : Arrow.{v_1, u_1} Cᵒᵖ) (e : L.op.mapArrow.obj g ≅ Arrow.mk f.hom.op), L.mapArrow.essImage f
⊢ L.mapArrow.essImage f

Tactic:
obtain ⟨g, ⟨e⟩⟩ : ∃ (g : _), Nonempty (L.op.mapArrow.obj g ≅ Arrow.mk f.hom.op) :=
      ⟨_, ⟨Functor.objObjPreimageIso _ _⟩⟩
-- 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.HasRightCalculusOfFractions
f : Arrow.{v_2, u_2} D
this : L.op.mapArrow.EssSurj
g : Arrow.{v_1, u_1} Cᵒᵖ
e : L.op.mapArrow.obj g ≅ Arrow.mk f.hom.op
⊢ L.mapArrow.essImage f

Tactic:
⟨Arrow.mk g.hom.unop, ⟨Arrow.isoMk (Arrow.rightFunc.mapIso e.symm).unop
      (Arrow.leftFunc.mapIso e.symm).unop (Quiver.Hom.op_inj e.inv.w.symm)⟩⟩

Premises used: Quiver.Hom.op_inj, Quiver.Hom.unop, CategoryTheory.Arrow.hom, CategoryTheory.Functor.essImage, CategoryTheory.Arrow.Hom.w, CategoryTheory.Arrow.leftFunc, Nonempty.intro, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.Arrow.rightFunc, CategoryTheory.Arrow.mk, Eq.symm, CategoryTheory.Functor.mapIso, CategoryTheory.Iso.inv, CategoryTheory.Arrow.isoMk, CategoryTheory.Iso.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 : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasRightCalculusOfFractions
f : Arrow.{v_2, u_2} D
this : L.op.mapArrow.EssSurj
g : Arrow.{v_1, u_1} Cᵒᵖ
e : L.op.mapArrow.obj g ≅ Arrow.mk f.hom.op
⊢ L.mapArrow.essImage f

Tactic:
exact ⟨Arrow.mk g.hom.unop, ⟨Arrow.isoMk (Arrow.rightFunc.mapIso e.symm).unop
      (Arrow.leftFunc.mapIso e.symm).unop (Quiver.Hom.op_inj e.inv.w.symm)⟩⟩
-- Module: Mathlib.CategoryTheory.Localization.Composition
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
E : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} E
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
h₁ : StrictUniversalPropertyFixedTarget.{v₁, u₁, v₂, u₂, v₄, u₄} L₁ W₁ E
h₂ : StrictUniversalPropertyFixedTarget.{v₂, u₂, v₃, u₃, v₄, u₄} L₂ W₂ E
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
F : Functor.{v₁, v₄, u₁, u₄} C₁ E
hF : W₃.IsInvertedBy F
⊢ W₂.IsInvertedBy (h₁.lift (W := W₁) F ⋯)

Tactic:
MorphismProperty.IsInvertedBy.of_le _ _ _ ?_ hW₂₃

Premises used: CategoryTheory.MorphismProperty.IsInvertedBy.of_le
-- Module: Mathlib.CategoryTheory.Localization.Composition
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
E : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} E
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
h₁ : StrictUniversalPropertyFixedTarget.{v₁, u₁, v₂, u₂, v₄, u₄} L₁ W₁ E
h₂ : StrictUniversalPropertyFixedTarget.{v₂, u₂, v₃, u₃, v₄, u₄} L₂ W₂ E
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
F : Functor.{v₁, v₄, u₁, u₄} C₁ E
hF : W₃.IsInvertedBy F
refine : (W₃.map L₁).IsInvertedBy (h₁.lift (W := W₁) F ⋯)
⊢ W₂.IsInvertedBy (h₁.lift (W := W₁) F ⋯)

Tactic:
refine MorphismProperty.IsInvertedBy.of_le _ _ _ ?_ hW₂₃

Premises used: CategoryTheory.MorphismProperty.IsInvertedBy.of_le
-- Module: Mathlib.CategoryTheory.Localization.Composition
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
E : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} E
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
h₁ : StrictUniversalPropertyFixedTarget.{v₁, u₁, v₂, u₂, v₄, u₄} L₁ W₁ E
h₂ : StrictUniversalPropertyFixedTarget.{v₂, u₂, v₃, u₃, v₄, u₄} L₂ W₂ E
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
F : Functor.{v₁, v₄, u₁, u₄} C₁ E
hF : W₃.IsInvertedBy F
⊢ (W₃.map L₁).IsInvertedBy (h₁.lift (W := W₁) F ⋯)

Tactic:
simpa only [MorphismProperty.IsInvertedBy.map_iff, h₁.fac F] using hF

Premises used: CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.fac, CategoryTheory.MorphismProperty.IsInvertedBy.map_iff