awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
f : R →+* S
t : Set R
ht : Eq (α := Ideal R) (Ideal.span t) ⊤
H :
  ∀ (g : (↑t : Type u)),
    Ideal.FG
      (ker (F :=
        RingHom.{u, v} (Localization.Away (↑g : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑g : R) : S)))
        (Localization.awayMap f (↑g : R)))
g : (↑t : Type u)
⊢ Ideal.FG (R := Localization.Away (↑g : R))
    (Ideal.map (F := R →+* Localization.Away (↑g : R)) (algebraMap R (Localization.Away (↑g : R))) (ker f))
have rw : Ideal.FG
  (ker (F := RingHom.{u, v} (Localization.Away (↑g : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑g : R) : S)))
    (IsLocalization.map (M := Submonoid.powers (↑g : R)) (T := Submonoid.powers ((f : (a : R) → S) (↑g : R)))
      (Localization.Away (M := S) ((f : (a : R) → S) (↑g : R) : S)) f sorry))
Tactic: rw [← IsLocalization.ker_map (Localization.Away (f g.val)) f (Submonoid.map_powers f g.val)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (hypothesis)
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 : ℤ
hx : Membership.mem (γ := Submonoid ℤ) ℤ⁰ x
⊢ IsUnit (M := ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ)
        (↑(Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Submonoid ℤ) ℤ⁰ x) x hx) : ℤ) :
      ℚ)
have hx₁ : x ≠ 0
Tactic: rw [mem_nonZeroDivisors_iff_ne_zero] at hx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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
n : ℤ
d : ℕ
hd : d ≠ 0
h : n.natAbs.Coprime d
⊢ ∃ (x : ℤ × ↥ℤ⁰),
    HMul.hMul (β := ℚ) { num := n, den := d, den_nz := hd, reduced := h : ℚ }
        ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (↑x.2 : ℤ) : ℚ) =
      (algebraMap ℤ ℚ : (a : ℤ) → ℚ) x.1
have refine : Membership.mem (γ := Submonoid ℤ) ℤ⁰ (↑d : ℤ)
Tactic: refine ⟨⟨n, ⟨d, ?_⟩⟩, Rat.mul_den_eq_num _⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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
n : ℤ
d : ℕ
hd : d ≠ 0
h : n.natAbs.Coprime d
⊢ Membership.mem (γ := Submonoid ℤ) ℤ⁰ (↑d : ℤ)
have rw : 0 < d
Tactic: rw [mem_nonZeroDivisors_iff_ne_zero, Int.natCast_ne_zero_iff_pos]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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 : ℤ
⊢ Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) x : ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) y : ℚ) →
    ∃ (c : ↥ℤ⁰), (↑c : ℤ) * x = (↑c : ℤ) * y
have rw : x = y → ∃ (c : ↥ℤ⁰), (↑c : ℤ) * x = (↑c : ℤ) * y
Tactic: rw [eq_intCast, eq_intCast, Int.cast_inj]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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 : ℤ
⊢ ∃ (c : ↥ℤ⁰), (↑c : ℤ) * x = (↑c : ℤ) * x
have w : ↥ℤ⁰
Tactic: use 1
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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 : ℤ
w : ↥ℤ⁰
⊢ ∃ (c : ↥ℤ⁰), (↑c : ℤ) * x = (↑c : ℤ) * x
have h : (↑1 : ℤ) * x = (↑1 : ℤ) * x
Tactic: use 1
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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 : ℚ
⊢ ∃ (x : ℤ × ↥(Submonoid.pos ℤ)),
    HMul.hMul (β := ℚ) z ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (↑x.2 : ℤ) : ℚ) = (algebraMap ℤ ℚ : (a : ℤ) → ℚ) x.1
have 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
Tactic: obtain ⟨⟨x1, x2⟩, hx⟩ := IsLocalization.surj (nonZeroDivisors ℤ) z
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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
⊢ ∃ (x : ℤ × ↥(Submonoid.pos ℤ)),
    HMul.hMul (β := ℚ) z ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (↑x.2 : ℤ) : ℚ) = (algebraMap ℤ ℚ : (a : ℤ) → ℚ) x.1
have inl : ∀ (hx2 : (↑x2 : ℤ) < 0),
  ∃ (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)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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
⊢ ∃ (x : ℤ × ↥(Submonoid.pos ℤ)),
    HMul.hMul (β := ℚ) z ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (↑x.2 : ℤ) : ℚ) = (algebraMap ℤ ℚ : (a : ℤ) → ℚ) x.1
have inr : ∀ (hx2 : 0 < (↑x2 : ℤ)),
  ∃ (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)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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 × ↥(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
have 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
Tactic: have ⟨x, y, eq⟩ := surj z
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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)
⊢ ∃ (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
have 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
Tactic: obtain rfl | hy := eq_or_ne y 0
Cleared hypotheses: y, eq
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain rfl | hy := eq_or_ne y 0
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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)
⊢ ∃ (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
have 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
Tactic: obtain rfl : z = 0 := by simpa using eq
Cleared hypotheses: z, eq
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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)
have refine : ∀ (x : K) (hx : Membership.mem (γ := Submonoid K) K⁰ x), Membership.mem (γ := Submonoid K) (IsUnit.submonoid K) x
Tactic: refine le_antisymm (fun x hx ↦ ?_) (isUnit_le_nonZeroDivisors K)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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
⊢ Membership.mem (γ := Submonoid K) (IsUnit.submonoid K) x
have 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
Tactic: have ⟨r, eq⟩ := surj R⁰ x
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ IsFractionRing R R ↔ LE.le (α := Submonoid R) R⁰ (IsUnit.submonoid R)
have rw : Eq (α := Submonoid R) R⁰ (IsUnit.submonoid 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)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
Goal:
R : Type u_1
inst : CommRing R
rw : Eq (α := 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)
have 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)
Tactic: rw [self_iff_nonZeroDivisors_eq_isUnit, le_antisymm_iff,
    and_iff_left (isUnit_le_nonZeroDivisors R)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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)
⊢ IsFractionRing R R ↔ LE.le (α := Submonoid R) R⁰ (IsUnit.submonoid R)
have rw₂ : LE.le (α := Submonoid R) R⁰ (IsUnit.submonoid 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)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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 R R ↔ Function.Surjective.{u_1 + 1, u_5 + 1} (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
have 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)
Tactic: rw [self_iff_bijective K, Function.Bijective, and_iff_right (IsFractionRing.injective R K)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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)
⊢ IsFractionRing R R ↔ Function.Surjective.{u_1 + 1, u_5 + 1} (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
have 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)
Tactic: rw [self_iff_bijective K, Function.Bijective, and_iff_right (IsFractionRing.injective R K)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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)
⊢ IsFractionRing R R ↔ Function.Surjective.{u_1 + 1, u_5 + 1} (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
have 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)
Tactic: rw [self_iff_bijective K, Function.Bijective, and_iff_right (IsFractionRing.injective R K)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : CommRing K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDomain A
x : K
hx : x ≠ 0
⊢ x * IsFractionRing.inv A x = 1
have rw : x *
    HMul.hMul (β := K)
      (mk' K (↑(sec A⁰ x).2 : A)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) (sec A⁰ x).1 sorry))
      ((algebraMap A K : (a : A) → K)
          (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) (sec A⁰ x).1 sorry) :
            A) :
        K) =
  (algebraMap A K : (a : A) → K)
    (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) (sec A⁰ x).1 sorry) : A)
Tactic: rw [IsFractionRing.inv, dif_neg hx, ←
    IsUnit.mul_left_inj
      (map_units K
        ⟨(sec _ x).1,
          mem_nonZeroDivisors_iff_ne_zero.2 fun h0 =>
            hx <| eq_zero_of_fst_eq_zero (sec_spec (nonZeroDivisors A) x) h0⟩),
    one_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : CommRing K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDomain A
x : K
hx : x ≠ 0
⊢ x *
      HMul.hMul (β := K)
        (mk' K (↑(sec A⁰ x).2 : A)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) (sec A⁰ x).1 ⋯))
        ((algebraMap A K : (a : A) → K)
            (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) (sec A⁰ x).1 ⋯) :
              A) :
          K) =
    (algebraMap A K : (a : A) → K)
      (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) (sec A⁰ x).1 ⋯) : A)
have rw : x =
  mk'.{u_4, u_5} (R := A) (M := A⁰) K
    (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) (sec A⁰ x).1 sorry) : A)
    (sec A⁰ x).2
Tactic: rw [mk'_spec, ← eq_mk'_iff_mul_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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
inst_10 : IsDomain A
⊢ Eq.{u_5 + 1} (α := K) (IsFractionRing.inv A 0) 0
have rw : Eq.{u_5 + 1} (α := K)
  (if h : Eq.{u_5 + 1} (α := K) 0 0 then 0
  else
    mk' K (↑(sec.{u_4, u_5} A⁰ (S := K) 0).2 : A)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x)
        (sec.{u_4, u_5} A⁰ (S := K) 0).1 sorry))
  0
Tactic: rw [IsFractionRing.inv]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
z : K
x y : A
hy : Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) y
h : mk' K x (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) y hy) = z
⊢ HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) y : K) = z
have rwa : ∀
  (h :
    HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) x : K)
        ((algebraMap A K : (a : A) → K)
            (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) y hy) : A) :
          K) =
      z),
  HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) y : K) = z
Tactic: rwa [mk'_eq_div] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_5
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
x : R
y : ↥R⁰
⊢ mk' K x y = 0 ↔ x = 0
have this : Nontrivial R
Tactic: haveI := (algebraMap R K).domain_nontrivial
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (hypothesis)
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
x : A
y : ↥A⁰
⊢ mk' K x y = 1 ↔ x = (↑y : A)
have this : Nontrivial A
Tactic: haveI := (algebraMap A K).domain_nontrivial
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
x : A
y : ↥A⁰
this : Nontrivial A
hxy : x = (↑y : A)
⊢ mk' K x y = 1
have rw : mk' K (↑y : A) y = 1
Tactic: rw [hxy, mk'_self']
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
x : A
y : ↥A⁰
this : Nontrivial A
hxy : x = (↑y : A)
rw : mk' K (↑y : A) y = 1
⊢ mk' K x y = 1
have rw₁ : Eq.{u_5 + 1} (α := K) 1 1
Tactic: rw [hxy, mk'_self']
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
x : A
y : ↥A⁰
this : Nontrivial A
⊢ mk' K x y = 1 ↔ x = (↑y : A)
have refine : mk' K x y = 1 → x = (↑y : A)
Tactic: refine ⟨?_, fun hxy => by rw [hxy, mk'_self']⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (hypothesis)
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
x : A
y : ↥A⁰
this : Nontrivial A
hxy : mk' K x y = 1
⊢ x = (↑y : A)
have hy : Ne.{u_5 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑y : A) : K) (0 : K)
Tactic: have hy : (algebraMap A K) ↑y ≠ (0 : K) :=
    IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors y.property
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (hypothesis)
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
x : A
y : ↥A⁰
this : Nontrivial A
hxy : mk' K x y = 1
hy : Ne.{u_5 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑y : A) : K) (0 : K)
⊢ x = (↑y : A)
have hxy₁ : Eq.{u_5 + 1} (α := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) (↑y : A) : K)
Tactic: rw [IsFractionRing.mk'_eq_div, div_eq_one_iff_eq hy] at hxy
Cleared hypotheses: hxy, hy
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
L : Type u_7
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : Algebra A L
f : L →ₐ[A] K
⊢ IsFractionRing A L
have refine : ∀ (x : K), ∃ (a : L), (f : (a : L) → K) a = x
Tactic: refine IsFractionRing.of_algEquiv <| .symm <| .ofBijective f ⟨f.injective, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
L : Type u_7
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : Algebra A L
f : L →ₐ[A] K
x : K
⊢ ∃ (a : L), (f : (a : L) → K) a = x
have obtain : ∀ (x y : A) (hy : Membership.mem (γ := Submonoid A) A⁰ y),
  ∃ (a : L),
    (f : (a : L) → K) a =
      HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) y : K)
Tactic: obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective A x
Cleared hypotheses: x