awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
h : (∃ (i : Ideal R), I.IsMinimalPrime i ∧ x ∈ i) ↔ ∃ y ∉ I.radical, x * y ∈ I.radical
⊢ Membership.mem (γ := Set R) (⋃ p ∈ I.minimalPrimes, (↑p : Set R)) x ↔
    Membership.mem (γ := Set R) {x : R | ∃ y ∉ I.radical, x * y ∈ I.radical} x

Tactic:
simp only [Set.mem_iUnion, SetLike.mem_coe, exists_prop, Set.mem_setOf_eq]

Premises used: Set.mem_iUnion, Set.mem_setOf_eq, exists_prop, SetLike.mem_coe
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
h : (∃ (i : Ideal R), I.IsMinimalPrime i ∧ x ∈ i) → ∃ y ∉ I.radical, x * y ∈ I.radical
h₁ : (∃ y ∉ I.radical, x * y ∈ I.radical) → ∃ (i : Ideal R), I.IsMinimalPrime i ∧ x ∈ i
⊢ (∃ (i : Ideal R), I.IsMinimalPrime i ∧ x ∈ i) ↔ ∃ y ∉ I.radical, x * y ∈ I.radical

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
rw :
  ∀ (b : Ideal (Localization.AtPrime p)),
    Membership.mem (γ := Set (Ideal (Localization.AtPrime p)))
        {J : Ideal (Localization.AtPrime p) |
          map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I ≤ J ∧ J.IsPrime}
        b →
      map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p ≤ b
⊢ LE.le (α := Ideal (Localization.AtPrime p))
    (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p)
    (radical (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I))

Tactic:
rw [Ideal.radical_eq_sInf, le_sInf_iff]

Premises used: le_sInf_iff, Ideal.radical_eq_sInf
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
q : Ideal (Localization.AtPrime p)
hq' : map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I ≤ q
hq : q.IsPrime
⊢ IsPrime.{u_1} (α := R)
    (↑((IsLocalization.AtPrime.orderIsoOfPrime (Localization.AtPrime p) p :
            (a : { p_1 : Ideal (Localization.AtPrime p) // p_1.IsPrime }) → { p_1 : Ideal R // p_1.IsPrime ∧ p_1 ≤ p })
          (Subtype.mk (p := fun (p_1 : Ideal (Localization.AtPrime p)) ↦ p_1.IsPrime) q hq)) :
      Ideal R)

Tactic:
obtain ⟨h₁, h₂⟩ := ((IsLocalization.AtPrime.orderIsoOfPrime _ p) ⟨q, hq⟩).2

Premises used: IsLocalization.AtPrime.orderIsoOfPrime, Subtype.mk, DFunLike.coe, Subtype.property
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
q : Ideal (Localization.AtPrime p)
hq' : map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I ≤ q
hq : q.IsPrime
h₁ :
  IsPrime.{u_1} (α := R)
    (↑((IsLocalization.AtPrime.orderIsoOfPrime (Localization.AtPrime p) p :
            (a : { p_1 : Ideal (Localization.AtPrime p) // p_1.IsPrime }) → { p_1 : Ideal R // p_1.IsPrime ∧ p_1 ≤ p })
          (Subtype.mk (p := fun (p_1 : Ideal (Localization.AtPrime p)) ↦ p_1.IsPrime) q hq)) :
      Ideal R)
⊢ (↑((IsLocalization.AtPrime.orderIsoOfPrime (Localization.AtPrime p) p :
            (a : { p_1 : Ideal (Localization.AtPrime p) // p_1.IsPrime }) → { p_1 : Ideal R // p_1.IsPrime ∧ p_1 ≤ p })
          (Subtype.mk (p := fun (p_1 : Ideal (Localization.AtPrime p)) ↦ p_1.IsPrime) q hq)) :
      Ideal R) ≤
    p

Tactic:
obtain ⟨h₁, h₂⟩ := ((IsLocalization.AtPrime.orderIsoOfPrime _ p) ⟨q, hq⟩).2

Premises used: IsLocalization.AtPrime.orderIsoOfPrime, Subtype.mk, DFunLike.coe, Subtype.property
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
q : Ideal (Localization.AtPrime p)
hq' : map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I ≤ q
hq : q.IsPrime
h₁ :
  IsPrime.{u_1} (α := R)
    (↑((IsLocalization.AtPrime.orderIsoOfPrime (Localization.AtPrime p) p :
            (a : { p_1 : Ideal (Localization.AtPrime p) // p_1.IsPrime }) → { p_1 : Ideal R // p_1.IsPrime ∧ p_1 ≤ p })
          (Subtype.mk (p := fun (p_1 : Ideal (Localization.AtPrime p)) ↦ p_1.IsPrime) q hq)) :
      Ideal R)
h₂ :
  (↑((IsLocalization.AtPrime.orderIsoOfPrime (Localization.AtPrime p) p :
            (a : { p_1 : Ideal (Localization.AtPrime p) // p_1.IsPrime }) → { p_1 : Ideal R // p_1.IsPrime ∧ p_1 ≤ p })
          (Subtype.mk (p := fun (p_1 : Ideal (Localization.AtPrime p)) ↦ p_1.IsPrime) q hq)) :
      Ideal R) ≤
    p
rw :
  ∀ (hq' : I ≤ comap (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) q) (hq : q.IsPrime)
    (h₁ :
      IsPrime.{u_1} (α := R)
        (↑((IsLocalization.AtPrime.orderIsoOfPrime (Localization.AtPrime p) p :
                (a : { p_1 : Ideal (Localization.AtPrime p) // p_1.IsPrime }) →
                  { p_1 : Ideal R // p_1.IsPrime ∧ p_1 ≤ p })
              (Subtype.mk (p := fun (p_1 : Ideal (Localization.AtPrime p)) ↦ p_1.IsPrime) q hq)) :
          Ideal R))
    (h₂ :
      (↑((IsLocalization.AtPrime.orderIsoOfPrime (Localization.AtPrime p) p :
                (a : { p_1 : Ideal (Localization.AtPrime p) // p_1.IsPrime }) →
                  { p_1 : Ideal R // p_1.IsPrime ∧ p_1 ≤ p })
              (Subtype.mk (p := fun (p_1 : Ideal (Localization.AtPrime p)) ↦ p_1.IsPrime) q hq)) :
          Ideal R) ≤
        p),
    p ≤ comap (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) q
⊢ map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p ≤ q

Tactic:
rw [Ideal.map_le_iff_le_comap] at hq' ⊢

Premises used: Ideal.map_le_iff_le_comap
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
q : Ideal (Localization.AtPrime p)
hq' : I ≤ comap (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) q
hq : q.IsPrime
h₁ :
  IsPrime.{u_1} (α := R)
    (↑((IsLocalization.AtPrime.orderIsoOfPrime (Localization.AtPrime p) p :
            (a : { p_1 : Ideal (Localization.AtPrime p) // p_1.IsPrime }) → { p_1 : Ideal R // p_1.IsPrime ∧ p_1 ≤ p })
          (Subtype.mk (p := fun (p_1 : Ideal (Localization.AtPrime p)) ↦ p_1.IsPrime) q hq)) :
      Ideal R)
h₂ :
  (↑((IsLocalization.AtPrime.orderIsoOfPrime (Localization.AtPrime p) p :
            (a : { p_1 : Ideal (Localization.AtPrime p) // p_1.IsPrime }) → { p_1 : Ideal R // p_1.IsPrime ∧ p_1 ≤ p })
          (Subtype.mk (p := fun (p_1 : Ideal (Localization.AtPrime p)) ↦ p_1.IsPrime) q hq)) :
      Ideal R) ≤
    p
⊢ p ≤ comap (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) q

Tactic:
hp₃ ⟨h₁, hq'⟩ h₂

Premises used: And.intro
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
q : Ideal (Localization.AtPrime p)
hq' : I ≤ comap (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) q
hq : q.IsPrime
h₁ :
  IsPrime.{u_1} (α := R)
    (↑((IsLocalization.AtPrime.orderIsoOfPrime (Localization.AtPrime p) p :
            (a : { p_1 : Ideal (Localization.AtPrime p) // p_1.IsPrime }) → { p_1 : Ideal R // p_1.IsPrime ∧ p_1 ≤ p })
          (Subtype.mk (p := fun (p_1 : Ideal (Localization.AtPrime p)) ↦ p_1.IsPrime) q hq)) :
      Ideal R)
h₂ :
  (↑((IsLocalization.AtPrime.orderIsoOfPrime (Localization.AtPrime p) p :
            (a : { p_1 : Ideal (Localization.AtPrime p) // p_1.IsPrime }) → { p_1 : Ideal R // p_1.IsPrime ∧ p_1 ≤ p })
          (Subtype.mk (p := fun (p_1 : Ideal (Localization.AtPrime p)) ↦ p_1.IsPrime) q hq)) :
      Ideal R) ≤
    p
⊢ p ≤ comap (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) q

Tactic:
exact hp₃ ⟨h₁, hq'⟩ h₂

Premises used: And.intro
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
⊢ LE.le (α := Ideal (Localization.AtPrime p))
    (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p)
    (radical (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I))

Tactic:
have : p.map (algebraMap R (Localization.AtPrime p)) ≤ (I.map (algebraMap _ _)).radical := by
      rw [Ideal.radical_eq_sInf, le_sInf_iff]
      rintro q ⟨hq', hq⟩
      obtain ⟨h₁, h₂⟩ := ((IsLocalization.AtPrime.orderIsoOfPrime _ p) ⟨q, hq⟩).2
      rw [Ideal.map_le_iff_le_comap] at hq' ⊢
      exact hp₃ ⟨h₁, hq'⟩ h₂
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this :
  LE.le (α := Ideal (Localization.AtPrime p))
    (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p)
    (radical (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I))
h :
  ∀ (n : ℕ)
    (hn :
      Membership.mem (γ := Ideal (Localization.AtPrime p))
        (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I)
        (HPow.hPow (α := Localization.AtPrime p)
          ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) x : Localization.AtPrime p) n)),
    ∃ y ∉ I.radical, x * y ∈ I.radical
⊢ ∃ y ∉ I.radical, x * y ∈ I.radical

Tactic:
obtain ⟨n, hn⟩ := this (Ideal.mem_map_of_mem _ hxp)

Premises used: Ideal.mem_map_of_mem
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this :
  LE.le (α := Ideal (Localization.AtPrime p))
    (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p)
    (radical (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I))
n : ℕ
hn :
  Membership.mem (γ := Ideal (Localization.AtPrime p))
    (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I)
    (HPow.hPow (α := Localization.AtPrime p)
      ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) x : Localization.AtPrime p) n)
⊢ ∃ (x_1 : ↥I × ↥p.primeCompl),
    HMul.hMul (β := Localization.AtPrime p)
        (HPow.hPow (α := Localization.AtPrime p)
          ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) x : Localization.AtPrime p) n)
        ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x_1.2 : R) :
          Localization.AtPrime p) =
      (algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x_1.1 : R)

Tactic:
rw [IsLocalization.mem_map_algebraMap_iff (M := p.primeCompl)] at hn

Premises used: Ideal.primeCompl, IsLocalization.mem_map_algebraMap_iff
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this :
  LE.le (α := Ideal (Localization.AtPrime p))
    (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p)
    (radical (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I))
n : ℕ
hn :
  ∃ (x_1 : ↥I × ↥p.primeCompl),
    HMul.hMul (β := Localization.AtPrime p)
        (HPow.hPow (α := Localization.AtPrime p)
          ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) x : Localization.AtPrime p) n)
        ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x_1.2 : R) :
          Localization.AtPrime p) =
      (algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x_1.1 : R)
h :
  ∀ (a : ↥I) (b : ↥p.primeCompl)
    (hn :
      HMul.hMul (β := Localization.AtPrime p)
          (HPow.hPow (α := Localization.AtPrime p)
            ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) x : Localization.AtPrime p) n)
          ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑(a, b).2 : R) :
            Localization.AtPrime p) =
        (algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑(a, b).1 : R)),
    ∃ y ∉ I.radical, x * y ∈ I.radical
⊢ ∃ y ∉ I.radical, x * y ∈ I.radical

Tactic:
obtain ⟨⟨a, b⟩, hn⟩ := hn
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this :
  LE.le (α := Ideal (Localization.AtPrime p))
    (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p)
    (radical (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I))
n : ℕ
a : ↥I
b : ↥p.primeCompl
hn :
  HMul.hMul (β := Localization.AtPrime p)
      (HPow.hPow (α := Localization.AtPrime p)
        ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) x : Localization.AtPrime p) n)
      ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑(a, b).2 : R) :
        Localization.AtPrime p) =
    (algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑(a, b).1 : R)
⊢ ∃ (c : ↥p.primeCompl), (↑c : R) * (x ^ n * (↑(a, b).2 : R)) = (↑c : R) * (↑(a, b).1 : R)

Tactic:
rw [← map_pow, ← map_mul, IsLocalization.eq_iff_exists p.primeCompl] at hn

Premises used: map_pow, map_mul, Ideal.primeCompl, IsLocalization.eq_iff_exists
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this :
  LE.le (α := Ideal (Localization.AtPrime p))
    (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p)
    (radical (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I))
n : ℕ
a : ↥I
b : ↥p.primeCompl
hn : ∃ (c : ↥p.primeCompl), (↑c : R) * (x ^ n * (↑(a, b).2 : R)) = (↑c : R) * (↑(a, b).1 : R)
h :
  ∀ (t : ↥p.primeCompl) (ht : (↑t : R) * (x ^ n * (↑(a, b).2 : R)) = (↑t : R) * (↑(a, b).1 : R)),
    ∃ y ∉ I.radical, x * y ∈ I.radical
⊢ ∃ y ∉ I.radical, x * y ∈ I.radical

Tactic:
obtain ⟨t, ht⟩ := hn
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this :
  LE.le (α := Ideal (Localization.AtPrime p))
    (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p)
    (radical (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I))
n : ℕ
a : ↥I
b t : ↥p.primeCompl
ht : (↑t : R) * (x ^ n * (↑(a, b).2 : R)) = (↑t : R) * (↑(a, b).1 : R)
⊢ ∃ y ∉ I.radical, x * y ∈ I.radical

Tactic:
⟨t * b, fun h ↦ (t * b).2 (hp₁.radical_le_iff.mpr hp₂ h), n + 1, ?_⟩

Premises used: Iff.mpr, HMul.hMul, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat, Subtype.val, Ideal.IsPrime.radical_le_iff, Subtype.property
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this :
  LE.le (α := Ideal (Localization.AtPrime p))
    (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p)
    (radical (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I))
n : ℕ
a : ↥I
b t : ↥p.primeCompl
ht : (↑t : R) * (x ^ n * (↑(a, b).2 : R)) = (↑t : R) * (↑(a, b).1 : R)
h : (x * ((↑t : R) * (↑b : R))) ^ (n + 1) ∈ I
⊢ ∃ y ∉ I.radical, x * y ∈ I.radical

Tactic:
refine ⟨t * b, fun h ↦ (t * b).2 (hp₁.radical_le_iff.mpr hp₂ h), n + 1, ?_⟩
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this :
  LE.le (α := Ideal (Localization.AtPrime p))
    (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p)
    (radical (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I))
n : ℕ
a : ↥I
b t : ↥p.primeCompl
ht : (↑t : R) * (x ^ n * (↑b : R)) = (↑t : R) * (↑a : R)
rw : (x * ((↑t : R) * (↑b : R))) ^ (n + 1) = (↑t : R) ^ n * (↑b : R) ^ n * x * ((↑t : R) * (x ^ n * (↑b : R)))
⊢ (x * ((↑t : R) * (↑b : R))) ^ (n + 1) = (↑t : R) ^ n * (↑b : R) ^ n * x * (↑t : R) * (↑a : R)

Tactic:
rw [mul_assoc, ← ht]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this :
  LE.le (α := Ideal (Localization.AtPrime p))
    (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p)
    (radical (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I))
n : ℕ
a : ↥I
b t : ↥p.primeCompl
ht : (↑t : R) * (x ^ n * (↑b : R)) = (↑t : R) * (↑a : R)
⊢ (x * ((↑t : R) * (↑b : R))) ^ (n + 1) = (↑t : R) ^ n * (↑b : R) ^ n * x * ((↑t : R) * (x ^ n * (↑b : R)))

Tactic:
ring
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this :
  LE.le (α := Ideal (Localization.AtPrime p))
    (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p)
    (radical (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I))
n : ℕ
a : ↥I
b t : ↥p.primeCompl
ht : (↑t : R) * (x ^ n * (↑b : R)) = (↑t : R) * (↑a : R)
⊢ (x * ((↑t : R) * (↑b : R))) ^ (n + 1) = (↑t : R) ^ n * (↑b : R) ^ n * x * (↑t : R) * (↑a : R)

Tactic:
have : (x * (t.1 * b.1)) ^ (n + 1) = (t.1 ^ n * b.1 ^ n * x * t.1) * a := by
      rw [mul_assoc, ← ht]; ring
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this_1 :
  LE.le (α := Ideal (Localization.AtPrime p))
    (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p)
    (radical (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I))
n : ℕ
a : ↥I
b t : ↥p.primeCompl
ht : (↑t : R) * (x ^ n * (↑b : R)) = (↑t : R) * (↑a : R)
this : (x * ((↑t : R) * (↑b : R))) ^ (n + 1) = (↑t : R) ^ n * (↑b : R) ^ n * x * (↑t : R) * (↑a : R)
h : (↑t : R) ^ n * (↑b : R) ^ n * x * (↑t : R) * (↑a : R) ∈ I
⊢ (x * ((↑t : R) * (↑b : R))) ^ (n + 1) ∈ I

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this_1 :
  LE.le (α := Ideal (Localization.AtPrime p))
    (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p)
    (radical (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I))
n : ℕ
a : ↥I
b t : ↥p.primeCompl
ht : (↑t : R) * (x ^ n * (↑b : R)) = (↑t : R) * (↑a : R)
this : (x * ((↑t : R) * (↑b : R))) ^ (n + 1) = (↑t : R) ^ n * (↑b : R) ^ n * x * (↑t : R) * (↑a : R)
⊢ (↑t : R) ^ n * (↑b : R) ^ n * x * (↑t : R) * (↑a : R) ∈ I

Tactic:
I.mul_mem_left _ a.2

Premises used: Ideal.mul_mem_left, Subtype.property
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this_1 :
  LE.le (α := Ideal (Localization.AtPrime p))
    (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p)
    (radical (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I))
n : ℕ
a : ↥I
b t : ↥p.primeCompl
ht : (↑t : R) * (x ^ n * (↑b : R)) = (↑t : R) * (↑a : R)
this : (x * ((↑t : R) * (↑b : R))) ^ (n + 1) = (↑t : R) ^ n * (↑b : R) ^ n * x * (↑t : R) * (↑a : R)
⊢ (↑t : R) ^ n * (↑b : R) ^ n * x * (↑t : R) * (↑a : R) ∈ I

Tactic:
exact I.mul_mem_left _ a.2

Premises used: Ideal.mul_mem_left, Subtype.property
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x y : R
hy : y ∉ I.radical
hx : x * y ∈ I.radical
⊢ ∃ p ∈ I.minimalPrimes, y ∉ p

Tactic:
simpa [← Ideal.sInf_minimalPrimes] using hy

Premises used: Ideal.sInf_minimalPrimes
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x y : R
hy : y ∉ I.radical
hx : x * y ∈ I.radical
h : ∀ (p : Ideal R) (hp : p ∈ I.minimalPrimes) (hyp : y ∉ p), ∃ (i : Ideal R), I.IsMinimalPrime i ∧ x ∈ i
⊢ ∃ (i : Ideal R), I.IsMinimalPrime i ∧ x ∈ i

Tactic:
obtain ⟨p, hp, hyp⟩ : ∃ p ∈ I.minimalPrimes, y ∉ p := by
      simpa [← Ideal.sInf_minimalPrimes] using hy

Premises used: Ideal.minimalPrimes
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x y : R
hy : y ∉ I.radical
hx : x * y ∈ I.radical
p : Ideal R
hp : p ∈ I.minimalPrimes
hyp : y ∉ p
⊢ ∃ (i : Ideal R), I.IsMinimalPrime i ∧ x ∈ i

Tactic:
⟨p, hp, (hp.isPrime.mem_or_mem ?_).resolve_right hyp⟩

Premises used: Ideal.IsPrime.mem_or_mem, Ideal.IsMinimalPrime.isPrime, And.intro, Exists.intro, Or.resolve_right
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x y : R
hy : y ∉ I.radical
hx : x * y ∈ I.radical
p : Ideal R
hp : p ∈ I.minimalPrimes
hyp : y ∉ p
h : x * y ∈ p
⊢ ∃ (i : Ideal R), I.IsMinimalPrime i ∧ x ∈ i

Tactic:
refine ⟨p, hp, (hp.isPrime.mem_or_mem ?_).resolve_right hyp⟩
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x y : R
hy : y ∉ I.radical
hx : x * y ∈ I.radical
p : Ideal R
hp : p ∈ I.minimalPrimes
hyp : y ∉ p
⊢ x * y ∈ p

Tactic:
hp.isPrime.radical_le_iff.mpr hp.le hx

Premises used: Iff.mpr, Set.Mem, Ideal.IsMinimalPrime.le, Ideal.IsMinimalPrime.isPrime, Ideal.IsPrime.radical_le_iff
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x y : R
hy : y ∉ I.radical
hx : x * y ∈ I.radical
p : Ideal R
hp : p ∈ I.minimalPrimes
hyp : y ∉ p
⊢ x * y ∈ p

Tactic:
exact hp.isPrime.radical_le_iff.mpr hp.le hx

Premises used: Iff.mpr, Ideal.IsMinimalPrime.le, Ideal.IsMinimalPrime.isPrime, Ideal.IsPrime.radical_le_iff