awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)
hJ : J = ⊤
mpr : ∀ (hJ : ⊤ ≤ J), LE.le (α := Ideal R) ⊤ (Ideal.under R J)
⊢ LE.le (α := Ideal R) ⊤ (Ideal.under R J)
have mpr₁ : ∀
  (hJ :
    LE.le.{u_1} (α := Ideal R)
      (((orderEmbedding M S : OrderEmbedding.{u_2, u_1} (Ideal S) (Ideal R)) : (a : Ideal S) → Ideal R) ⊤ : Ideal R)
      (((orderEmbedding M S : OrderEmbedding.{u_2, u_1} (Ideal S) (Ideal R)) : (a : Ideal S) → Ideal R) J : Ideal R)),
  LE.le (α := Ideal R) ⊤ (Ideal.under R J)
Tactic: rwa [eq_top_iff, ← (orderEmbedding M S).le_iff_le] at hJ
Cleared hypotheses: hJ
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)
x y : S
hxy : x * y ∈ J
⊢ x ∈ J ∨ y ∈ J
have mpr : ∀ (a : R) (s : ↥M) (ha : mk' S a s = x), x ∈ J ∨ y ∈ J
Tactic: obtain ⟨a, s, ha⟩ := exists_mk'_eq M x
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
⊢ x ∈ J ∨ y ∈ J
have mpr : ∀ (b : R) (t : ↥M) (hb : mk' S b t = y), x ∈ J ∨ y ∈ J
Tactic: obtain ⟨b, t, hb⟩ := exists_mk'_eq M y
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
b : R
t : ↥M
hb : mk' S b t = y
⊢ mk' S (a * b) (s * t) ∈ J
have rwa : mk' S a s * mk' S b t ∈ J
Tactic: rwa [mk'_mul, ha, hb]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
b : R
t : ↥M
hb : mk' S b t = y
rwa : mk' S a s * mk' S b t ∈ J
⊢ mk' S (a * b) (s * t) ∈ J
have rwa₁ : x * mk' S b t ∈ J
Tactic: rwa [mk'_mul, ha, hb]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
b : R
t : ↥M
hb : mk' S b t = y
⊢ x ∈ J ∨ y ∈ J
have this : mk' S (a * b) (s * t) ∈ J
Tactic: have : mk' S (a * b) (s * t) ∈ J := by rwa [mk'_mul, ha, hb]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
b : R
t : ↥M
hb : mk' S b t = y
this : mk' S (a * b) (s * t) ∈ J
⊢ x ∈ J ∨ y ∈ J
have this₁ : Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) J) (a * b)
Tactic: rw [mk'_mem_iff, ← Ideal.mem_comap] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
b : R
t : ↥M
hb : mk' S b t = y
this : Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) J) (a * b)
⊢ x ∈ J ∨ y ∈ J
have this₂ : Membership.mem (γ := Ideal R) (Ideal.under R J) a ∨ Membership.mem (γ := Ideal R) (Ideal.under R J) b
Tactic: have this₂ := (h.1).mul_mem_iff_mem_or_mem.1 this
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
b : R
t : ↥M
hb : mk' S b t = y
this : Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) J) (a * b)
this₂ : Membership.mem (γ := Ideal R) (Ideal.under R J) a ∨ Membership.mem (γ := Ideal R) (Ideal.under R J) b
⊢ x ∈ J ∨ y ∈ J
have this₃ : Membership.mem (α := S) J ((algebraMap R S : (a : R) → S) a : S) ∨
  Membership.mem (α := S) J ((algebraMap R S : (a : R) → S) b : S)
Tactic: rw [Ideal.mem_comap, Ideal.mem_comap] at this₂
Cleared hypotheses: this₂
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
b : R
t : ↥M
hb : mk' S b t = y
this : Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) J) (a * b)
this₂ :
  Membership.mem (α := S) J ((algebraMap R S : (a : R) → S) a : S) ∨
    Membership.mem (α := S) J ((algebraMap R S : (a : R) → S) b : S)
⊢ x ∈ J ∨ y ∈ J
have mpr : mk' S a s ∈ J ∨ y ∈ J
Tactic: rwa [← ha, ← hb, mk'_mem_iff, mk'_mem_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
b : R
t : ↥M
hb : mk' S b t = y
this : Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) J) (a * b)
this₂ :
  Membership.mem (α := S) J ((algebraMap R S : (a : R) → S) a : S) ∨
    Membership.mem (α := S) J ((algebraMap R S : (a : R) → S) b : S)
mpr : mk' S a s ∈ J ∨ y ∈ J
⊢ x ∈ J ∨ y ∈ J
have mpr₁ : mk' S a s ∈ J ∨ mk' S b t ∈ J
Tactic: rwa [← ha, ← hb, mk'_mem_iff, mk'_mem_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
J : Ideal S
h : Ideal.IsPrime (Ideal.under R J) ∧ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
b : R
t : ↥M
hb : mk' S b t = y
this : Membership.mem (γ := Ideal R) (Ideal.comap (F := R →+* S) (algebraMap R S) J) (a * b)
this₂ :
  Membership.mem (α := S) J ((algebraMap R S : (a : R) → S) a : S) ∨
    Membership.mem (α := S) J ((algebraMap R S : (a : R) → S) b : S)
mpr : mk' S a s ∈ J ∨ y ∈ J
mpr₁ : mk' S a s ∈ J ∨ mk' S b t ∈ J
⊢ x ∈ J ∨ y ∈ J
have mpr₂ : Membership.mem (α := S) J ((algebraMap R S : (a : R) → S) a : S) ∨ mk' S b t ∈ J
Tactic: rwa [← ha, ← hb, mk'_mem_iff, mk'_mem_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal R
hp : I.IsPrime
hd : Disjoint (↑M : Set R) (↑I : Set R)
⊢ Ideal.IsPrime.{u_2} (α := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
have rw : I.IsPrime ∧ Disjoint (↑M : Set R) (↑I : Set R)
Tactic: rw [isPrime_iff_isPrime_disjoint M S, under_map_of_isPrime_disjoint M S hp hd]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
J : Ideal S
⊢ Disjoint (↑M : Set R) (↑(Ideal.under R J) : Set R) ↔ J ≠ ⊤
have rw : J = ⊤ ↔ ∃ x ∈ (↑M : Set R), x ∈ (↑(Ideal.under R J) : Set R)
Tactic: rw [← iff_not_comm, Set.not_disjoint_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
J : Ideal S
⊢ J = ⊤ ↔ ∃ x ∈ (↑M : Set R), x ∈ (↑(Ideal.under R J) : Set R)
have mp : J = ⊤ → ∃ x ∈ (↑M : Set R), x ∈ (↑(Ideal.under R J) : Set R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
J : Ideal S
mp : J = ⊤ → ∃ x ∈ (↑M : Set R), x ∈ (↑(Ideal.under R J) : Set R)
⊢ J = ⊤ ↔ ∃ x ∈ (↑M : Set R), x ∈ (↑(Ideal.under R J) : Set R)
have mpr : (∃ x ∈ (↑M : Set R), x ∈ (↑(Ideal.under R J) : Set R)) → J = ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal R
⊢ Eq.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I.radical)
    (Ideal.radical (Ideal.map (F := R →+* S) (algebraMap R S) I))
have refine : LE.le.{u_2} (α := Ideal S) (Ideal.radical (Ideal.map (F := R →+* S) (algebraMap R S) I))
  (Ideal.map (F := R →+* S) (algebraMap R S) I.radical)
Tactic: refine (I.map_radical_le (algebraMap R S)).antisymm ?_
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal R
x : S
n : ℕ
hn : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) (x ^ n)
⊢ Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I.radical) x
have obtain : ∀ (x : R) (s : ↥M) (hn : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) (mk' S x s ^ n)),
  Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I.radical) (mk' S x s)
Tactic: obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq M x
Cleared hypotheses: x, hn
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal R
n : ℕ
x : R
s : ↥M
hn : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) (mk' S x s ^ n)
⊢ Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I.radical) (mk' S x s)
have simp : ∀ (hn : ∃ s ∈ M, s * x ^ n ∈ I), ∃ s ∈ M, s * x ∈ I.radical
Tactic: simp only [← IsLocalization.mk'_pow, IsLocalization.mk'_mem_map_algebraMap_iff M] at hn ⊢
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal R
n : ℕ
x : R
s : ↥M
hn : ∃ s ∈ M, s * x ^ n ∈ I
⊢ ∃ s ∈ M, s * x ∈ I.radical
have obtain : ∀ (s : R) (hs : s ∈ M) (h : s * x ^ n ∈ I), ∃ s ∈ M, s * x ∈ I.radical
Tactic: obtain ⟨s, hs, h⟩ := hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal R
n : ℕ
x : R
s_1 : ↥M
s : R
hs : s ∈ M
h : s * x ^ n ∈ I
⊢ (s * x) ^ (n + 1) ∈ I
have h₁ : (s * x) ^ (n + 1) = s ^ n * x * (s * x ^ n)
Tactic: convert! I.mul_mem_left (s ^ n * x) h
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Finset R
hS : Eq (α := Ideal R) (Ideal.span (↑S : Set R)) ⊤
I : Ideal R
⊢ I =
    ⨅ f ∈ S,
      Ideal.under R (B := Localization.Away f)
        (Ideal.map (F := R →+* Localization.Away f) (algebraMap R (Localization.Away f)) I)
have a : I ≤
  ⨅ f ∈ S,
    Ideal.under R (B := Localization.Away f)
      (Ideal.map (F := R →+* Localization.Away f) (algebraMap R (Localization.Away f)) I)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Finset R
hS : Eq (α := Ideal R) (Ideal.span (↑S : Set R)) ⊤
I : Ideal R
a :
  I ≤
    ⨅ f ∈ S,
      Ideal.under R (B := Localization.Away f)
        (Ideal.map (F := R →+* Localization.Away f) (algebraMap R (Localization.Away f)) I)
⊢ I =
    ⨅ f ∈ S,
      Ideal.under R (B := Localization.Away f)
        (Ideal.map (F := R →+* Localization.Away f) (algebraMap R (Localization.Away f)) I)
have a₁ : ⨅ f ∈ S,
    Ideal.under R (B := Localization.Away f)
      (Ideal.map (F := R →+* Localization.Away f) (algebraMap R (Localization.Away f)) I) ≤
  I
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Finset R
hS : Eq (α := Ideal R) (Ideal.span (↑S : Set R)) ⊤
I : Ideal R
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (⨅ f ∈ S,
      Ideal.under R (B := Localization.Away f)
        (Ideal.map (F := R →+* Localization.Away f) (algebraMap R (Localization.Away f)) I))
    x
⊢ x ∈ I
have a : ∀ (r : (↑(↑S : Set R) : Type u_1)), ∃ (n : ℕ), (↑r : R) ^ n • x ∈ I
Tactic: apply Submodule.mem_of_span_eq_top_of_smul_pow_mem _ _ hS
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
S : Finset R
hS : Eq (α := Ideal R) (Ideal.span (↑S : Set R)) ⊤
I : Ideal R
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (⨅ f ∈ S,
      Ideal.under R (B := Localization.Away f)
        (Ideal.map (F := R →+* Localization.Away f) (algebraMap R (Localization.Away f)) I))
    x
s : R
hs : s ∈ (↑S : Set R)
⊢ ∃ (n : ℕ), (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ (↑S : Set R)) s hs) : R) ^ n • x ∈ I
have hx₁ : ∀ (i : R) (i_1 : i ∈ S),
  Membership.mem (α := Localization.Away i) (γ := Ideal (Localization.Away i))
    (Ideal.map (F := R →+* Localization.Away i) (algebraMap R (Localization.Away i)) I)
    ((algebraMap R (Localization.Away i) : (a : R) → Localization.Away i) x : Localization.Away i)
Tactic: simp only [Ideal.mem_iInf, Ideal.mem_comap] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Finset R
hS : Eq (α := Ideal R) (Ideal.span (↑S : Set R)) ⊤
I : Ideal R
x s : R
hs : s ∈ (↑S : Set R)
hx :
  ∀ (i : R) (i_1 : i ∈ S),
    Membership.mem (α := Localization.Away i) (γ := Ideal (Localization.Away i))
      (Ideal.map (F := R →+* Localization.Away i) (algebraMap R (Localization.Away i)) I)
      ((algebraMap R (Localization.Away i) : (a : R) → Localization.Away i) x : Localization.Away i)
⊢ ∃ (n : ℕ), (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ (↑S : Set R)) s hs) : R) ^ n • x ∈ I
have a : ∀ (y : ↥I) (n : ℕ)
  (e :
    HMul.hMul (α := Localization.Away s) (β := Localization.Away s)
        ((algebraMap R (Localization.Away s) : (a : R) → Localization.Away s) x : Localization.Away s)
        ((algebraMap R (Localization.Away s) : (a : R) → Localization.Away s)
            (↑(y,
                    Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers s) x)
                      ((fun (x : ℕ) ↦ s ^ x) n) sorry).2 :
              R) :
          Localization.Away s) =
      (algebraMap R (Localization.Away s) : (a : R) → Localization.Away s)
        (↑(y,
                Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers s) x)
                  ((fun (x : ℕ) ↦ s ^ x) n) sorry).1 :
          R)),
  ∃ (n : ℕ), (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ (↑S : Set R)) s hs) : R) ^ n • x ∈ I
Tactic: obtain ⟨⟨y, ⟨_, n, rfl⟩⟩, e⟩ :=
      (IsLocalization.mem_map_algebraMap_iff (.powers s) _).mp (hx s hs)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
S : Finset R
hS : Eq (α := Ideal R) (Ideal.span (↑S : Set R)) ⊤
I : Ideal R
x s : R
hs : s ∈ (↑S : Set R)
hx :
  ∀ (i : R) (i_1 : i ∈ S),
    Membership.mem (α := Localization.Away i) (γ := Ideal (Localization.Away i))
      (Ideal.map (F := R →+* Localization.Away i) (algebraMap R (Localization.Away i)) I)
      ((algebraMap R (Localization.Away i) : (a : R) → Localization.Away i) x : Localization.Away i)
y : ↥I
n : ℕ
e :
  HMul.hMul (α := Localization.Away s) (β := Localization.Away s)
      ((algebraMap R (Localization.Away s) : (a : R) → Localization.Away s) x : Localization.Away s)
      ((algebraMap R (Localization.Away s) : (a : R) → Localization.Away s) (s ^ n) : Localization.Away s) =
    (algebraMap R (Localization.Away s) : (a : R) → Localization.Away s) (↑y : R)
⊢ ∃ (n : ℕ), (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ (↑S : Set R)) s hs) : R) ^ n • x ∈ I
have e₁ : ∃ (c : ↥(Submonoid.powers s)), (↑c : R) * (x * s ^ n) = (↑c : R) * (↑y : R)
Tactic: rw [← map_mul, IsLocalization.eq_iff_exists (.powers s)] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Finset R
hS : Eq (α := Ideal R) (Ideal.span (↑S : Set R)) ⊤
I : Ideal R
x s : R
hs : s ∈ (↑S : Set R)
hx :
  ∀ (i : R) (i_1 : i ∈ S),
    Membership.mem (α := Localization.Away i) (γ := Ideal (Localization.Away i))
      (Ideal.map (F := R →+* Localization.Away i) (algebraMap R (Localization.Away i)) I)
      ((algebraMap R (Localization.Away i) : (a : R) → Localization.Away i) x : Localization.Away i)
y : ↥I
n : ℕ
e : ∃ (c : ↥(Submonoid.powers s)), (↑c : R) * (x * s ^ n) = (↑c : R) * (↑y : R)
⊢ ∃ (n : ℕ), (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ (↑S : Set R)) s hs) : R) ^ n • x ∈ I
have a : ∀ (m : ℕ)
  (e :
    (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers s) x)
              ((fun (x : ℕ) ↦ s ^ x) m) sorry) :
          R) *
        (x * s ^ n) =
      (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers s) x)
              ((fun (x : ℕ) ↦ s ^ x) m) sorry) :
          R) *
        (↑y : R)),
  ∃ (n : ℕ), (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ (↑S : Set R)) s hs) : R) ^ n • x ∈ I
Tactic: obtain ⟨⟨_, m, rfl⟩, e⟩ := e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Finset R
hS : Eq (α := Ideal R) (Ideal.span (↑S : Set R)) ⊤
I : Ideal R
x s : R
hs : s ∈ (↑S : Set R)
hx :
  ∀ (i : R) (i_1 : i ∈ S),
    Membership.mem (α := Localization.Away i) (γ := Ideal (Localization.Away i))
      (Ideal.map (F := R →+* Localization.Away i) (algebraMap R (Localization.Away i)) I)
      ((algebraMap R (Localization.Away i) : (a : R) → Localization.Away i) x : Localization.Away i)
y : ↥I
n m : ℕ
e :
  (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers s) x) ((fun (x : ℕ) ↦ s ^ x) m)
            ⋯) :
        R) *
      (x * s ^ n) =
    (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers s) x)
            ((fun (x : ℕ) ↦ s ^ x) m) ⋯) :
        R) *
      (↑y : R)
⊢ ∃ (n : ℕ), (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ (↑S : Set R)) s hs) : R) ^ n • x ∈ I
have h : (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ (↑S : Set R)) s hs) : R) ^ (m + n) • x ∈ I
Tactic: use m + n
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Finset R
hS : Eq (α := Ideal R) (Ideal.span (↑S : Set R)) ⊤
I : Ideal R
x s : R
hs : s ∈ (↑S : Set R)
hx :
  ∀ (i : R) (i_1 : i ∈ S),
    Membership.mem (α := Localization.Away i) (γ := Ideal (Localization.Away i))
      (Ideal.map (F := R →+* Localization.Away i) (algebraMap R (Localization.Away i)) I)
      ((algebraMap R (Localization.Away i) : (a : R) → Localization.Away i) x : Localization.Away i)
y : ↥I
n m : ℕ
e :
  (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers s) x) ((fun (x : ℕ) ↦ s ^ x) m)
            ⋯) :
        R) *
      (x * s ^ n) =
    (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers s) x)
            ((fun (x : ℕ) ↦ s ^ x) m) ⋯) :
        R) *
      (↑y : R)
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ (↑S : Set R)) s hs) : R) ^ (m + n) • x ∈ I
have h : s ^ (m + n) * x ∈ I
Tactic: dsimp at e ⊢
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Finset R
hS : Eq (α := Ideal R) (Ideal.span (↑S : Set R)) ⊤
I : Ideal R
x s : R
hs : s ∈ (↑S : Set R)
hx :
  ∀ (i : R) (i_1 : i ∈ S),
    Membership.mem (α := Localization.Away i) (γ := Ideal (Localization.Away i))
      (Ideal.map (F := R →+* Localization.Away i) (algebraMap R (Localization.Away i)) I)
      ((algebraMap R (Localization.Away i) : (a : R) → Localization.Away i) x : Localization.Away i)
y : ↥I
n m : ℕ
e : s ^ m * (x * s ^ n) = s ^ m * (↑y : R)
⊢ s ^ (m + n) * x ∈ I
have h : s ^ m * (↑y : R) ∈ I
Tactic: rw [pow_add, mul_assoc, ← mul_comm x, e]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal R
hle : ¬(↑I : Set R) ⊆ (↑M : Set R)ᶜ
⊢ Eq.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) ⊤
have hle₁ : ∃ x ∈ (↑I : Set R), x ∈ (↑M : Set R)
Tactic: simp only [Set.not_subset_iff_exists_mem_notMem, Set.mem_compl_iff, not_not] at hle
Cleared hypotheses: hle
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal R
hle : ∃ x ∈ (↑I : Set R), x ∈ (↑M : Set R)
⊢ Eq.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) ⊤
have obtain : ∀ (y : R) (hy : y ∈ (↑I : Set R)) (hny : y ∈ (↑M : Set R)),
  Eq.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) ⊤
Tactic: obtain ⟨y, hy, hny⟩ := hle
Cleared hypotheses: hle
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal R
y : R
hy : y ∈ (↑I : Set R)
hny : y ∈ (↑M : Set R)
⊢ Eq.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) ⊤
have hx : Membership.mem.{u_2, u_2} (α := S) (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
  ((algebraMap R S : (a : R) → S) y : S)
Tactic: apply Ideal.eq_top_of_isUnit_mem
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal R
y : R
hy : y ∈ (↑I : Set R)
hny : y ∈ (↑M : Set R)
hx :
  Membership.mem.{u_2, u_2} (α := S) (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
    ((algebraMap R S : (a : R) → S) y : S)
⊢ Eq.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) ⊤
have h : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) y : S)
Tactic: apply Ideal.eq_top_of_isUnit_mem