awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
y : ↥(Submonoid.pos ℤ)
⊢ IsUnit (M := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (↑y : ℤ) : ℚ)

Tactic:
simpa using y.prop.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
z : ℚ
obtain :
  ∀ (x1 : ℤ) (x2 : ↥ℤ⁰)
    (hx :
      HMul.hMul (β := ℚ) z ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (↑(x1, x2).2 : ℤ) : ℚ) =
        (algebraMap ℤ ℚ : (a : ℤ) → ℚ) (x1, x2).1),
    ∃ (x : ℤ × ↥(Submonoid.pos ℤ)),
      HMul.hMul (β := ℚ) z ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (↑x.2 : ℤ) : ℚ) = (algebraMap ℤ ℚ : (a : ℤ) → ℚ) x.1
⊢ ∃ (x : ℤ × ↥(Submonoid.pos ℤ)),
    HMul.hMul (β := ℚ) z ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (↑x.2 : ℤ) : ℚ) = (algebraMap ℤ ℚ : (a : ℤ) → ℚ) x.1

Tactic:
obtain ⟨⟨x1, x2⟩, hx⟩ := IsLocalization.surj (nonZeroDivisors ℤ) z

Premises used: IsLocalization.surj, nonZeroDivisors, Int
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
z : ℚ
x1 : ℤ
x2 : ↥ℤ⁰
hx :
  HMul.hMul (β := ℚ) z ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (↑(x1, x2).2 : ℤ) : ℚ) =
    (algebraMap ℤ ℚ : (a : ℤ) → ℚ) (x1, x2).1
⊢ (↑x2 : ℤ) ≠ 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
z : ℚ
x1 : ℤ
x2 : ↥ℤ⁰
hx :
  HMul.hMul (β := ℚ) z ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (↑(x1, x2).2 : ℤ) : ℚ) =
    (algebraMap ℤ ℚ : (a : ℤ) → ℚ) (x1, x2).1
inl :
  ∀ (hx2 : (↑x2 : ℤ) < 0),
    ∃ (x : ℤ × ↥(Submonoid.pos ℤ)),
      HMul.hMul (β := ℚ) z ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (↑x.2 : ℤ) : ℚ) = (algebraMap ℤ ℚ : (a : ℤ) → ℚ) x.1
inr :
  ∀ (hx2 : 0 < (↑x2 : ℤ)),
    ∃ (x : ℤ × ↥(Submonoid.pos ℤ)),
      HMul.hMul (β := ℚ) z ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (↑x.2 : ℤ) : ℚ) = (algebraMap ℤ ℚ : (a : ℤ) → ℚ) x.1
⊢ ∃ (x : ℤ × ↥(Submonoid.pos ℤ)),
    HMul.hMul (β := ℚ) z ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (↑x.2 : ℤ) : ℚ) = (algebraMap ℤ ℚ : (a : ℤ) → ℚ) x.1

Tactic:
obtain hx2 | hx2 := lt_or_gt_of_ne (show x2.val ≠ 0 by simp)

Premises used: lt_or_gt_of_ne
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
z : ℚ
x1 : ℤ
x2 : ↥ℤ⁰
hx :
  HMul.hMul (β := ℚ) z ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (↑(x1, x2).2 : ℤ) : ℚ) =
    (algebraMap ℤ ℚ : (a : ℤ) → ℚ) (x1, x2).1
hx2 : (↑x2 : ℤ) < 0
⊢ Membership.mem (γ := Submonoid ℤ) (Submonoid.pos ℤ) (-(↑x2 : ℤ))

Tactic:
simpa using hx2
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
z : ℚ
x1 : ℤ
x2 : ↥ℤ⁰
hx :
  HMul.hMul (β := ℚ) z ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (↑(x1, x2).2 : ℤ) : ℚ) =
    (algebraMap ℤ ℚ : (a : ℤ) → ℚ) (x1, x2).1
hx2 : (↑x2 : ℤ) < 0
⊢ HMul.hMul (β := ℚ) z
      ((algebraMap ℤ ℚ : (a : ℤ) → ℚ)
          (↑(-x1,
                  Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Submonoid ℤ) (Submonoid.pos ℤ) x) (-(↑x2 : ℤ))
                    ⋯).2 :
            ℤ) :
        ℚ) =
    (algebraMap ℤ ℚ : (a : ℤ) → ℚ)
      (-x1, Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Submonoid ℤ) (Submonoid.pos ℤ) x) (-(↑x2 : ℤ)) ⋯).1

Tactic:
simpa using hx
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
z : ℚ
x1 : ℤ
x2 : ↥ℤ⁰
hx :
  HMul.hMul (β := ℚ) z ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (↑(x1, x2).2 : ℤ) : ℚ) =
    (algebraMap ℤ ℚ : (a : ℤ) → ℚ) (x1, x2).1
hx2 : (↑x2 : ℤ) < 0
⊢ ∃ (x : ℤ × ↥(Submonoid.pos ℤ)),
    HMul.hMul (β := ℚ) z ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (↑x.2 : ℤ) : ℚ) = (algebraMap ℤ ℚ : (a : ℤ) → ℚ) x.1

Tactic:
exact ⟨⟨-x1, ⟨-x2.val, by simpa using hx2⟩⟩, by simpa using hx⟩
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
z : ℚ
x1 : ℤ
x2 : ↥ℤ⁰
hx :
  HMul.hMul (β := ℚ) z ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (↑(x1, x2).2 : ℤ) : ℚ) =
    (algebraMap ℤ ℚ : (a : ℤ) → ℚ) (x1, x2).1
hx2 : 0 < (↑x2 : ℤ)
⊢ ∃ (x : ℤ × ↥(Submonoid.pos ℤ)),
    HMul.hMul (β := ℚ) z ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (↑x.2 : ℤ) : ℚ) = (algebraMap ℤ ℚ : (a : ℤ) → ℚ) x.1

Tactic:
⟨⟨x1, ⟨x2.val, hx2⟩⟩, hx⟩

Premises used: Prod.mk, Subtype.mk, Exists.intro, Subtype.val
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
z : ℚ
x1 : ℤ
x2 : ↥ℤ⁰
hx :
  HMul.hMul (β := ℚ) z ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (↑(x1, x2).2 : ℤ) : ℚ) =
    (algebraMap ℤ ℚ : (a : ℤ) → ℚ) (x1, x2).1
hx2 : 0 < (↑x2 : ℤ)
⊢ ∃ (x : ℤ × ↥(Submonoid.pos ℤ)),
    HMul.hMul (β := ℚ) z ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (↑x.2 : ℤ) : ℚ) = (algebraMap ℤ ℚ : (a : ℤ) → ℚ) x.1

Tactic:
exact ⟨⟨x1, ⟨x2.val, hx2⟩⟩, hx⟩
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
x y : ℤ
h : Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) x : ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) y : ℚ)
⊢ (↑1 : ℤ) * x = (↑1 : ℤ) * y

Tactic:
simpa using Rat.intCast_inj.mp h

Premises used: Rat.intCast_inj, Iff.mp
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
y : ↥ℕ⁰
⊢ IsUnit (M := ℚ≥0) ((algebraMap ℕ ℚ≥0 : (a : ℕ) → ℚ≥0) (↑y : ℕ) : ℚ≥0)

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
z : ℚ≥0
⊢ Membership.mem (γ := Submonoid ℕ) ℕ⁰ z.den

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
z : ℚ≥0
⊢ HMul.hMul (β := ℚ≥0) z
      ((algebraMap ℕ ℚ≥0 : (a : ℕ) → ℚ≥0)
          (↑(z.num, Subtype.mk (p := fun (x : ℕ) ↦ Membership.mem (γ := Submonoid ℕ) ℕ⁰ x) z.den ⋯).2 : ℕ) :
        ℚ≥0) =
    (algebraMap ℕ ℚ≥0 : (a : ℕ) → ℚ≥0)
      (z.num, Subtype.mk (p := fun (x : ℕ) ↦ Membership.mem (γ := Submonoid ℕ) ℕ⁰ x) z.den ⋯).1

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
x y : ℕ
h : Eq (α := ℚ≥0) ((algebraMap ℕ ℚ≥0 : (a : ℕ) → ℚ≥0) x : ℚ≥0) ((algebraMap ℕ ℚ≥0 : (a : ℕ) → ℚ≥0) y : ℚ≥0)
⊢ (↑1 : ℕ) * x = (↑1 : ℕ) * y

Tactic:
simpa using h
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
K : Type u_5
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : FaithfulSMul R K
surj :
  ∀ (z : K),
    ∃ (x : R) (y : R),
      z = HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K)
inj : Function.Injective.{u_1 + 1, u_5 + 1} (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
this_1 : NoZeroDivisors R
this : Nontrivial R
z : K
have :
  ∀ (x y : R)
    (eq :
      z = HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K)),
    ∃ (x : R × ↥(R⁰ : Submonoid R)),
      HMul.hMul (β := K) z ((algebraMap R K : (a : R) → K) (↑x.2 : R) : K) = (algebraMap R K : (a : R) → K) x.1
⊢ ∃ (x : R × ↥(R⁰ : Submonoid R)),
    HMul.hMul (β := K) z ((algebraMap R K : (a : R) → K) (↑x.2 : R) : K) = (algebraMap R K : (a : R) → K) x.1

Tactic:
have ⟨x, y, eq⟩ := surj z
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
K : Type u_5
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : FaithfulSMul R K
surj :
  ∀ (z : K),
    ∃ (x : R) (y : R),
      z = HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K)
inj : Function.Injective.{u_1 + 1, u_5 + 1} (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
this_1 : NoZeroDivisors R
this : Nontrivial R
z : K
x y : R
eq : z = HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K)
inl :
  ∀
    (eq :
      z = HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) 0 : K)),
    ∃ (x : R × ↥(R⁰ : Submonoid R)),
      HMul.hMul (β := K) z ((algebraMap R K : (a : R) → K) (↑x.2 : R) : K) = (algebraMap R K : (a : R) → K) x.1
inr :
  ∀ (hy : y ≠ 0),
    ∃ (x : R × ↥(R⁰ : Submonoid R)),
      HMul.hMul (β := K) z ((algebraMap R K : (a : R) → K) (↑x.2 : R) : K) = (algebraMap R K : (a : R) → K) x.1
⊢ ∃ (x : R × ↥(R⁰ : Submonoid R)),
    HMul.hMul (β := K) z ((algebraMap R K : (a : R) → K) (↑x.2 : R) : K) = (algebraMap R K : (a : R) → K) x.1

Tactic:
obtain rfl | hy := eq_or_ne y 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
K : Type u_5
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : FaithfulSMul R K
surj :
  ∀ (z : K),
    ∃ (x : R) (y : R),
      z = HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K)
inj : Function.Injective.{u_1 + 1, u_5 + 1} (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
this_1 : NoZeroDivisors R
this : Nontrivial R
z : K
x : R
eq : z = HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) 0 : K)
⊢ z = 0

Tactic:
simpa using eq
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
K : Type u_5
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : FaithfulSMul R K
surj :
  ∀ (z : K),
    ∃ (x : R) (y : R),
      z = HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K)
inj : Function.Injective.{u_1 + 1, u_5 + 1} (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
this_1 : NoZeroDivisors R
this : Nontrivial R
z : K
x : R
eq : z = HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) 0 : K)
inl :
  ∀
    (eq :
      0 = HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) 0 : K)),
    ∃ (x : R × ↥(R⁰ : Submonoid R)),
      HMul.hMul (α := K) (β := K) (0 : K) ((algebraMap R K : (a : R) → K) (↑x.2 : R) : K) =
        (algebraMap R K : (a : R) → K) x.1
⊢ ∃ (x : R × ↥(R⁰ : Submonoid R)),
    HMul.hMul (β := K) z ((algebraMap R K : (a : R) → K) (↑x.2 : R) : K) = (algebraMap R K : (a : R) → K) x.1

Tactic:
obtain rfl : z = 0 := by simpa using eq

Premises used: rfl
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
K : Type u_5
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : FaithfulSMul R K
surj :
  ∀ (z : K),
    ∃ (x : R) (y : R),
      z = HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K)
inj : Function.Injective.{u_1 + 1, u_5 + 1} (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
this_1 : NoZeroDivisors R
this : Nontrivial R
x : R
eq : 0 = HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) 0 : K)
⊢ HMul.hMul (α := K) (β := K) (0 : K) ((algebraMap R K : (a : R) → K) (↑(0, 1).2 : R) : K) =
    (algebraMap R K : (a : R) → K) (0, 1).1

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
K : Type u_5
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : FaithfulSMul R K
surj :
  ∀ (z : K),
    ∃ (x : R) (y : R),
      z = HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K)
inj : Function.Injective.{u_1 + 1, u_5 + 1} (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
this_1 : NoZeroDivisors R
this : Nontrivial R
x : R
eq : 0 = HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) 0 : K)
⊢ ∃ (x : R × ↥(R⁰ : Submonoid R)),
    HMul.hMul (α := K) (β := K) (0 : K) ((algebraMap R K : (a : R) → K) (↑x.2 : R) : K) =
      (algebraMap R K : (a : R) → K) x.1

Tactic:
exact ⟨(0, 1), by simp⟩
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
K : Type u_5
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : FaithfulSMul R K
surj :
  ∀ (z : K),
    ∃ (x : R) (y : R),
      z = HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K)
inj : Function.Injective.{u_1 + 1, u_5 + 1} (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
this_1 : NoZeroDivisors R
this : Nontrivial R
z : K
x y : R
eq : z = HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K)
hy : y ≠ 0
⊢ ∃ (x : R × ↥(R⁰ : Submonoid R)),
    HMul.hMul (β := K) z ((algebraMap R K : (a : R) → K) (↑x.2 : R) : K) = (algebraMap R K : (a : R) → K) x.1

Tactic:
⟨⟨x, y, mem_nonZeroDivisors_iff_ne_zero.mpr hy⟩,
      (eq_div_iff_mul_eq <| (map_ne_zero_iff _ inj).mpr hy).mp eq⟩

Premises used: Iff.mpr, Prod.mk, Subtype.mk, eq_div_iff_mul_eq, Exists.intro, Iff.mp, mem_nonZeroDivisors_iff_ne_zero, map_ne_zero_iff
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
K : Type u_5
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : FaithfulSMul R K
surj :
  ∀ (z : K),
    ∃ (x : R) (y : R),
      z = HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K)
inj : Function.Injective.{u_1 + 1, u_5 + 1} (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
this_1 : NoZeroDivisors R
this : Nontrivial R
z : K
x y : R
eq : z = HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K)
hy : y ≠ 0
⊢ ∃ (x : R × ↥(R⁰ : Submonoid R)),
    HMul.hMul (β := K) z ((algebraMap R K : (a : R) → K) (↑x.2 : R) : K) = (algebraMap R K : (a : R) → K) x.1

Tactic:
exact ⟨⟨x, y, mem_nonZeroDivisors_iff_ne_zero.mpr hy⟩,
      (eq_div_iff_mul_eq <| (map_ne_zero_iff _ inj).mpr hy).mp eq⟩
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
K : Type u_5
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : FaithfulSMul R K
surj :
  ∀ (z : K),
    ∃ (x : R) (y : R),
      z = HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K)
inj : Function.Injective.{u_1 + 1, u_5 + 1} (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
this_1 : NoZeroDivisors R
this : Nontrivial R
x y : R
eq : Eq.{u_5 + 1} (α := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K)
⊢ (↑1 : R) * x = (↑1 : R) * y

Tactic:
simpa using inj eq
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_6
inst : CommSemiring R
S : Type u_7
inst_1 : CommSemiring S
K : Type u_8
inst_2 : CommSemiring K
inst_3 : Algebra R K
e : R ≃+* S
inst_4 : Algebra S K
h :
  ∀ (x : R),
    Eq.{u_8 + 1} (α := K) ((algebraMap R K : (a : R) → K) x : K)
      ((algebraMap S K : (a : S) → K) ((e : (a : R) → S) x : S) : K)
inst_5 : IsFractionRing S K
⊢ IsFractionRing R K

Tactic:
IsLocalization.of_ringEquiv_left e (MulEquivClass.map_nonZeroDivisors e) h

Premises used: IsLocalization.of_ringEquiv_left, MulEquivClass.map_nonZeroDivisors
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
K : Type u_5
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
x : R
⊢ Eq.{u_5 + 1} (α := K) ((algebraMap R K : (a : R) → K) x : K) (0 : K) ↔ x = 0

Tactic:
IsLocalization.to_map_eq_zero_iff _ le_rfl

Premises used: IsLocalization.to_map_eq_zero_iff, le_rfl
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
K : Type u_5
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
⊢ Function.Injective.{u_1 + 1, u_5 + 1} (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)

Tactic:
IsLocalization.injective _ (le_of_eq rfl)

Premises used: IsLocalization.injective, le_of_eq, rfl
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
K : Type u_5
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
⊢ Eq (α := Submonoid K) K⁰ (IsUnit.submonoid K)

Tactic:
le_antisymm (fun x hx ↦ ?_) (isUnit_le_nonZeroDivisors K)

Premises used: isUnit_le_nonZeroDivisors, le_antisymm
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
K : Type u_5
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
refine :
  ∀ (x : K) (hx : Membership.mem (γ := Submonoid K) K⁰ x), Membership.mem (γ := Submonoid K) (IsUnit.submonoid K) x
⊢ Eq (α := Submonoid K) K⁰ (IsUnit.submonoid K)

Tactic:
refine le_antisymm (fun x hx ↦ ?_) (isUnit_le_nonZeroDivisors K)

Premises used: isUnit_le_nonZeroDivisors, le_antisymm
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
K : Type u_5
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
x : K
hx : Membership.mem (γ := Submonoid K) K⁰ x
have :
  ∀ (r : R × ↥(R⁰ : Submonoid R))
    (eq : HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) (↑r.2 : R) : K) = (algebraMap R K : (a : R) → K) r.1),
    Membership.mem (γ := Submonoid K) (IsUnit.submonoid K) x
⊢ Membership.mem (γ := Submonoid K) (IsUnit.submonoid K) x

Tactic:
have ⟨r, eq⟩ := surj R⁰ x
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
K : Type u_5
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
x : K
hx : Membership.mem (γ := Submonoid K) K⁰ x
r : R × ↥(R⁰ : Submonoid R)
eq : HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) (↑r.2 : R) : K) = (algebraMap R K : (a : R) → K) r.1
r' : ↥R⁰ := Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r.1 ⋯
⊢ Membership.mem (γ := Submonoid K) (IsUnit.submonoid K) x

Tactic:
isUnit_of_mul_isUnit_left <| eq ▸ map_units K r'

Premises used: Set.Mem, setOf, IsUnit, isUnit_of_mul_isUnit_left
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
K : Type u_5
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
x : K
hx : Membership.mem (γ := Submonoid K) K⁰ x
r : R × ↥(R⁰ : Submonoid R)
eq : HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) (↑r.2 : R) : K) = (algebraMap R K : (a : R) → K) r.1
r' : ↥R⁰ := Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r.1 ⋯
⊢ Membership.mem (γ := Submonoid K) (IsUnit.submonoid K) x

Tactic:
exact isUnit_of_mul_isUnit_left <| eq ▸ map_units K r'

Premises used: isUnit_of_mul_isUnit_left
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
K : Type u_5
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
⊢ IsFractionRing K K

Tactic:
IsLocalization.self (nonZeroDivisors_eq_isUnit R K).le

Premises used: IsFractionRing.nonZeroDivisors_eq_isUnit, IsLocalization.self, Eq.le
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
K : Type u_5
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
L : Type u_6
inst_4 : CommRing L
inst_5 : Algebra K L
inst_6 : IsFractionRing K L
inst_7 : Algebra R L
inst_8 : IsScalarTower R K L
⊢ IsFractionRing R L

Tactic:
isLocalization_of_algEquiv _ <| (algEquiv R K L).restrictScalars R

Premises used: IsFractionRing.algEquiv, AlgEquiv.restrictScalars, IsLocalization.isLocalization_of_algEquiv
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
inst_5 : CommRing K
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
inst_8 : Algebra A K
inst_9 : IsFractionRing A K
⊢ FaithfulSMul R K

Tactic:
(faithfulSMul_iff_algebraMap_injective R K).mpr <| IsFractionRing.injective R K

Premises used: Iff.mpr, faithfulSMul_iff_algebraMap_injective, IsFractionRing.injective
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
rw : Eq (α := Submonoid R) R⁰ (IsUnit.submonoid R) ↔ LE.le (α := Submonoid R) R⁰ (IsUnit.submonoid R)
rw₁ :
  LE.le (α := Submonoid R) R⁰ (IsUnit.submonoid R) ∧ LE.le (α := Submonoid R) (IsUnit.submonoid R) R⁰ ↔
    LE.le (α := Submonoid R) R⁰ (IsUnit.submonoid R)
rw₂ rw₃ : LE.le (α := Submonoid R) R⁰ (IsUnit.submonoid R) ↔ LE.le (α := Submonoid R) R⁰ (IsUnit.submonoid R)
⊢ IsFractionRing R R ↔ LE.le (α := Submonoid R) R⁰ (IsUnit.submonoid R)

Tactic:
rw [self_iff_nonZeroDivisors_eq_isUnit, le_antisymm_iff,
    and_iff_left (isUnit_le_nonZeroDivisors R)]

Premises used: isUnit_le_nonZeroDivisors, and_iff_left, le_antisymm_iff, IsFractionRing.self_iff_nonZeroDivisors_eq_isUnit
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
K : Type u_5
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
rw :
  Function.Bijective.{u_1 + 1, u_5 + 1} (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K) ↔
    Function.Surjective.{u_1 + 1, u_5 + 1} (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
rw₁ :
  Function.Injective.{u_1 + 1, u_5 + 1} (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K) ∧
      Function.Surjective.{u_1 + 1, u_5 + 1} (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K) ↔
    Function.Surjective.{u_1 + 1, u_5 + 1} (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
rw₂ rw₃ :
  Function.Surjective.{u_1 + 1, u_5 + 1} (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K) ↔
    Function.Surjective.{u_1 + 1, u_5 + 1} (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
⊢ IsFractionRing R R ↔ Function.Surjective.{u_1 + 1, u_5 + 1} (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)

Tactic:
rw [self_iff_bijective K, Function.Bijective, and_iff_right (IsFractionRing.injective R K)]

Premises used: IsFractionRing.injective, and_iff_right, Function.Bijective, IsFractionRing.self_iff_bijective
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
K : Type u_5
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
a b : R
⊢ Eq.{u_5 + 1} (α := K) (↑a : K) (↑b : K) ↔ a = b

Tactic:
algebraMap.coe_inj _ _

Premises used: algebraMap.coe_inj
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
K : Type u_5
inst_1 : CommRing K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : Nontrivial R
x : R
hx : Membership.mem (γ := Submonoid R) R⁰ x
⊢ Ne.{u_5 + 1} (α := K) ((algebraMap R K : (a : R) → K) x : K) (0 : K)

Tactic:
IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors _ le_rfl hx

Premises used: le_rfl, IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors