awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Ideal
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
x : R
hxM : x ∈ (↑M : Set R)
hxJ : x ∈ (↑(Ideal.under R J) : Set R)
⊢ J = ⊤

Tactic:
exact J.eq_top_of_isUnit_mem hxJ (IsLocalization.map_units S ⟨x, hxM⟩)

Premises used: Ideal.eq_top_of_isUnit_mem, Subtype.mk, IsLocalization.map_units
-- Module: Mathlib.RingTheory.Localization.Ideal
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 I' : { p : Ideal S // p.IsPrime }
⊢ LE.le.{u_1} (α := { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
      (({
              toFun := fun (p : { p : Ideal S // p.IsPrime }) ↦
                Subtype.mk (p := fun (p : Ideal R) ↦ p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R))
                  (Ideal.under R (↑p : Ideal S)) ⋯,
              invFun := fun (p : { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) }) ↦
                Subtype.mk (p := fun (p : Ideal S) ↦ p.IsPrime)
                  (Ideal.map (F := R →+* S) (algebraMap R S) (↑p : Ideal R)) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : { p : Ideal S // p.IsPrime }) → { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
          I :
        { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
      (({
              toFun := fun (p : { p : Ideal S // p.IsPrime }) ↦
                Subtype.mk (p := fun (p : Ideal R) ↦ p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R))
                  (Ideal.under R (↑p : Ideal S)) ⋯,
              invFun := fun (p : { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) }) ↦
                Subtype.mk (p := fun (p : Ideal S) ↦ p.IsPrime)
                  (Ideal.map (F := R →+* S) (algebraMap R S) (↑p : Ideal R)) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : { p : Ideal S // p.IsPrime }) → { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
          I' :
        { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) }) →
    I ≤ I'

Tactic:
fun h => show I.val ≤ I'.val from map_under M S I.val ▸
        map_under M S I'.val ▸ Ideal.map_mono h

Premises used: Eq.rec, IsLocalization.map_under, Ideal.map_mono, Subtype.val
-- Module: Mathlib.RingTheory.Localization.Ideal
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 I' : { p : Ideal S // p.IsPrime }
⊢ LE.le.{u_1} (α := { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
      (({
              toFun := fun (p : { p : Ideal S // p.IsPrime }) ↦
                Subtype.mk (p := fun (p : Ideal R) ↦ p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R))
                  (Ideal.under R (↑p : Ideal S)) ⋯,
              invFun := fun (p : { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) }) ↦
                Subtype.mk (p := fun (p : Ideal S) ↦ p.IsPrime)
                  (Ideal.map (F := R →+* S) (algebraMap R S) (↑p : Ideal R)) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : { p : Ideal S // p.IsPrime }) → { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
          I :
        { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
      (({
              toFun := fun (p : { p : Ideal S // p.IsPrime }) ↦
                Subtype.mk (p := fun (p : Ideal R) ↦ p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R))
                  (Ideal.under R (↑p : Ideal S)) ⋯,
              invFun := fun (p : { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) }) ↦
                Subtype.mk (p := fun (p : Ideal S) ↦ p.IsPrime)
                  (Ideal.map (F := R →+* S) (algebraMap R S) (↑p : Ideal R)) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : { p : Ideal S // p.IsPrime }) → { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
          I' :
        { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) }) →
    I ≤ I'

Tactic:
exact fun h => show I.val ≤ I'.val from map_under M S I.val ▸
        map_under M S I'.val ▸ Ideal.map_mono h

Premises used: Eq.rec, IsLocalization.map_under, Ideal.map_mono, Subtype.val
-- Module: Mathlib.RingTheory.Localization.Ideal
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 I' : { p : Ideal S // p.IsPrime }
⊢ I ≤ I' →
    LE.le.{u_1} (α := { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
      (({
              toFun := fun (p : { p : Ideal S // p.IsPrime }) ↦
                Subtype.mk (p := fun (p : Ideal R) ↦ p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R))
                  (Ideal.under R (↑p : Ideal S)) ⋯,
              invFun := fun (p : { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) }) ↦
                Subtype.mk (p := fun (p : Ideal S) ↦ p.IsPrime)
                  (Ideal.map (F := R →+* S) (algebraMap R S) (↑p : Ideal R)) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : { p : Ideal S // p.IsPrime }) → { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
          I :
        { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
      (({
              toFun := fun (p : { p : Ideal S // p.IsPrime }) ↦
                Subtype.mk (p := fun (p : Ideal R) ↦ p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R))
                  (Ideal.under R (↑p : Ideal S)) ⋯,
              invFun := fun (p : { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) }) ↦
                Subtype.mk (p := fun (p : Ideal S) ↦ p.IsPrime)
                  (Ideal.map (F := R →+* S) (algebraMap R S) (↑p : Ideal R)) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : { p : Ideal S // p.IsPrime }) → { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
          I' :
        { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })

Tactic:
fun h x hx => h hx

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.RingTheory.Localization.Ideal
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 I' : { p : Ideal S // p.IsPrime }
⊢ I ≤ I' →
    LE.le.{u_1} (α := { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
      (({
              toFun := fun (p : { p : Ideal S // p.IsPrime }) ↦
                Subtype.mk (p := fun (p : Ideal R) ↦ p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R))
                  (Ideal.under R (↑p : Ideal S)) ⋯,
              invFun := fun (p : { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) }) ↦
                Subtype.mk (p := fun (p : Ideal S) ↦ p.IsPrime)
                  (Ideal.map (F := R →+* S) (algebraMap R S) (↑p : Ideal R)) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : { p : Ideal S // p.IsPrime }) → { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
          I :
        { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
      (({
              toFun := fun (p : { p : Ideal S // p.IsPrime }) ↦
                Subtype.mk (p := fun (p : Ideal R) ↦ p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R))
                  (Ideal.under R (↑p : Ideal S)) ⋯,
              invFun := fun (p : { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) }) ↦
                Subtype.mk (p := fun (p : Ideal S) ↦ p.IsPrime)
                  (Ideal.map (F := R →+* S) (algebraMap R S) (↑p : Ideal R)) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : { p : Ideal S // p.IsPrime }) → { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })
          I' :
        { p : Ideal R // p.IsPrime ∧ Disjoint (↑M : Set R) (↑p : Set R) })

Tactic:
exact fun h x hx => h hx
-- Module: Mathlib.RingTheory.Localization.Ideal
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))

Tactic:
(I.map_radical_le (algebraMap R S)).antisymm ?_

Premises used: Algebra.algebraMap, LE.le.antisymm, Ideal.map_radical_le
-- Module: Mathlib.RingTheory.Localization.Ideal
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
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)
⊢ 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))

Tactic:
refine (I.map_radical_le (algebraMap R S)).antisymm ?_

Premises used: Algebra.algebraMap, LE.le.antisymm, Ideal.map_radical_le
-- Module: Mathlib.RingTheory.Localization.Ideal
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)
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)
⊢ Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I.radical) x

Tactic:
obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq M x

Premises used: rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.Localization.Ideal
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)
simp : ∀ (hn : ∃ s ∈ M, s * x ^ n ∈ I), ∃ s ∈ M, s * x ∈ I.radical
⊢ Membership.mem (γ := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I.radical) (mk' S x s)

Tactic:
simp only [← IsLocalization.mk'_pow, IsLocalization.mk'_mem_map_algebraMap_iff M] at hn ⊢

Premises used: IsLocalization.mk'_pow, IsLocalization.mk'_mem_map_algebraMap_iff
-- Module: Mathlib.RingTheory.Localization.Ideal
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
obtain : ∀ (s : R) (hs : s ∈ M) (h : s * x ^ n ∈ I), ∃ s ∈ M, s * x ∈ I.radical
⊢ ∃ s ∈ M, s * x ∈ I.radical

Tactic:
obtain ⟨s, hs, h⟩ := hn
-- Module: Mathlib.RingTheory.Localization.Ideal
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 ^ n * x * (s * x ^ n) ∈ I

Tactic:
I.mul_mem_left (s ^ n * x) h

Premises used: HMul.hMul, HPow.hPow, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Localization.Ideal
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
h₁ : (s * x) ^ (n + 1) = s ^ n * x * (s * x ^ n)
⊢ (s * x) ^ (n + 1) ∈ I

Tactic:
convert! I.mul_mem_left (s ^ n * x) h

Premises used: HMul.hMul, HPow.hPow, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Localization.Ideal
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) = s ^ n * x * (s * x ^ n)

Tactic:
ring
-- Module: Mathlib.RingTheory.Localization.Ideal
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 ∈ M, s * x ∈ I.radical

Tactic:
refine ⟨s, hs, n + 1, by convert! I.mul_mem_left (s ^ n * x) h; ring⟩
-- Module: Mathlib.RingTheory.Localization.Ideal
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)
a₁ :
  ⨅ f ∈ S,
      Ideal.under R (B := Localization.Away f)
        (Ideal.map (F := R →+* Localization.Away f) (algebraMap R (Localization.Away f)) I) ≤
    I
⊢ 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

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Localization.Ideal
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)

Tactic:
simp only [le_iInf₂_iff, ← Ideal.map_le_iff_le_comap, le_refl, implies_true]

Premises used: le_refl, le_iInf₂_iff, Ideal.map_le_iff_le_comap, implies_true
-- Module: Mathlib.RingTheory.Localization.Ideal
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
a : ∀ (r : (↑(↑S : Set R) : Type u_1)), ∃ (n : ℕ), (↑r : R) ^ n • x ∈ I
⊢ x ∈ I

Tactic:
apply Submodule.mem_of_span_eq_top_of_smul_pow_mem _ _ hS

Premises used: Submodule.mem_of_span_eq_top_of_smul_pow_mem
-- Module: Mathlib.RingTheory.Localization.Ideal
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)
⊢ ∀ (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

Premises used: Ideal.mem_iInf, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Localization.Ideal
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)
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) ⋯).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) ⋯).1 :
            R)),
    ∃ (n : ℕ), (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ (↑S : Set R)) s hs) : R) ^ n • x ∈ I
⊢ ∃ (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)

Premises used: Submonoid.powers, Iff.mp, IsLocalization.mem_map_algebraMap_iff, rfl
-- Module: Mathlib.RingTheory.Localization.Ideal
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)
⊢ ∃ (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

Premises used: map_mul, Submonoid.powers, IsLocalization.eq_iff_exists
-- Module: Mathlib.RingTheory.Localization.Ideal
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)
a :
  ∀ (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
⊢ ∃ (n : ℕ), (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ (↑S : Set R)) s hs) : R) ^ n • x ∈ I

Tactic:
obtain ⟨⟨_, m, rfl⟩, e⟩ := e

Premises used: rfl
-- Module: Mathlib.RingTheory.Localization.Ideal
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)
h : (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ (↑S : Set R)) s hs) : R) ^ (m + n) • x ∈ I
⊢ ∃ (n : ℕ), (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ (↑S : Set R)) s hs) : R) ^ n • x ∈ I

Tactic:
use m + n
-- Module: Mathlib.RingTheory.Localization.Ideal
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)
h : s ^ (m + n) * x ∈ I
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ (↑S : Set R)) s hs) : R) ^ (m + n) • x ∈ I

Tactic:
dsimp at e ⊢
-- Module: Mathlib.RingTheory.Localization.Ideal
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)
h : s ^ m * (↑y : R) ∈ I
⊢ s ^ (m + n) * x ∈ I

Tactic:
rw [pow_add, mul_assoc, ← mul_comm x, e]

Premises used: mul_assoc, pow_add, mul_comm
-- Module: Mathlib.RingTheory.Localization.Ideal
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 * (↑y : R) ∈ I

Tactic:
I.mul_mem_left _ y.2

Premises used: Set.Mem, Ideal.mul_mem_left, Subtype.property
-- Module: Mathlib.RingTheory.Localization.Ideal
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 * (↑y : R) ∈ I

Tactic:
exact I.mul_mem_left _ y.2

Premises used: Ideal.mul_mem_left, Subtype.property
-- Module: Mathlib.RingTheory.Localization.Ideal
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)ᶜ
⊢ ∃ 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

Premises used: Classical.not_not, Set.not_subset_iff_exists_mem_notMem, Set.mem_compl_iff
-- Module: Mathlib.RingTheory.Localization.Ideal
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)
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) ⊤
⊢ Eq.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) ⊤

Tactic:
obtain ⟨y, hy, hny⟩ := hle