awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
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
have h : x * y ∈ p
Tactic: refine ⟨p, hp, (hp.isPrime.mem_or_mem ?_).resolve_right hyp⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
⊢ Eq.{u_1 + 1} (α := Set R) (⋃ p ∈ I.minimalPrimes, (↑p : Set R)) {x : R | ∃ y ∉ I.radical, x * y ∈ I.radical}
have h : ∀ (x : R),
  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: classical
  ext x
  simp only [Set.mem_iUnion, SetLike.mem_coe, exists_prop, Set.mem_setOf_eq]
  constructor
  · rintro ⟨p, ⟨⟨hp₁, hp₂⟩, hp₃⟩, hxp⟩
    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₂
    obtain ⟨n, hn⟩ := this (Ideal.mem_map_of_mem _ hxp)
    rw [IsLocalization.mem_map_algebraMap_iff (M := p.primeCompl)] at hn
    obtain ⟨⟨a, b⟩, hn⟩ := hn
    rw [← map_pow, ← map_mul, IsLocalization.eq_iff_exists p.primeCompl] at hn
    obtain ⟨t, ht⟩ := hn
    refine ⟨t * b, fun h ↦ (t * b).2 (hp₁.radical_le_iff.mpr hp₂ h), n + 1, ?_⟩
    simp only at ht
    have : (x * (t.1 * b.1)) ^ (n + 1) = (t.1 ^ n * b.1 ^ n * x * t.1) * a := by
      rw [mul_assoc, ← ht]; ring
    rw [this]
    exact I.mul_mem_left _ a.2
  · rintro ⟨y, hy, hx⟩
    obtain ⟨p, hp, hyp⟩ : ∃ p ∈ I.minimalPrimes, y ∉ p := by
      simpa [← Ideal.sInf_minimalPrimes] using hy
    refine ⟨p, hp, (hp.isPrime.mem_or_mem ?_).resolve_right hyp⟩
    exact hp.isPrime.radical_le_iff.mpr hp.le hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
h :
  ∀ (x : R),
    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
⊢ Eq.{u_1 + 1} (α := Set R) (⋃ p ∈ I.minimalPrimes, (↑p : Set R)) {x : R | ∃ y ∉ I.radical, x * y ∈ I.radical}
have h₁ : ∀ (x : R), (∃ (i : Ideal R), I.IsMinimalPrime i ∧ x ∈ i) ↔ ∃ y ∉ I.radical, x * y ∈ I.radical
Tactic: classical
  ext x
  simp only [Set.mem_iUnion, SetLike.mem_coe, exists_prop, Set.mem_setOf_eq]
  constructor
  · rintro ⟨p, ⟨⟨hp₁, hp₂⟩, hp₃⟩, hxp⟩
    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₂
    obtain ⟨n, hn⟩ := this (Ideal.mem_map_of_mem _ hxp)
    rw [IsLocalization.mem_map_algebraMap_iff (M := p.primeCompl)] at hn
    obtain ⟨⟨a, b⟩, hn⟩ := hn
    rw [← map_pow, ← map_mul, IsLocalization.eq_iff_exists p.primeCompl] at hn
    obtain ⟨t, ht⟩ := hn
    refine ⟨t * b, fun h ↦ (t * b).2 (hp₁.radical_le_iff.mpr hp₂ h), n + 1, ?_⟩
    simp only at ht
    have : (x * (t.1 * b.1)) ^ (n + 1) = (t.1 ^ n * b.1 ^ n * x * t.1) * a := by
      rw [mul_assoc, ← ht]; ring
    rw [this]
    exact I.mul_mem_left _ a.2
  · rintro ⟨y, hy, hx⟩
    obtain ⟨p, hp, hyp⟩ : ∃ p ∈ I.minimalPrimes, y ∉ p := by
      simpa [← Ideal.sInf_minimalPrimes] using hy
    refine ⟨p, hp, (hp.isPrime.mem_or_mem ?_).resolve_right hyp⟩
    exact hp.isPrime.radical_le_iff.mpr hp.le hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
h :
  ∀ (x : R),
    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
h₁ : ∀ (x : R), (∃ (i : Ideal R), I.IsMinimalPrime i ∧ x ∈ i) ↔ ∃ y ∉ I.radical, x * y ∈ I.radical
⊢ Eq.{u_1 + 1} (α := Set R) (⋃ p ∈ I.minimalPrimes, (↑p : Set R)) {x : R | ∃ y ∉ I.radical, x * y ∈ I.radical}
have h₂ : ∀ (x : R), (∃ (i : Ideal R), I.IsMinimalPrime i ∧ x ∈ i) → ∃ y ∉ I.radical, x * y ∈ I.radical
Tactic: classical
  ext x
  simp only [Set.mem_iUnion, SetLike.mem_coe, exists_prop, Set.mem_setOf_eq]
  constructor
  · rintro ⟨p, ⟨⟨hp₁, hp₂⟩, hp₃⟩, hxp⟩
    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₂
    obtain ⟨n, hn⟩ := this (Ideal.mem_map_of_mem _ hxp)
    rw [IsLocalization.mem_map_algebraMap_iff (M := p.primeCompl)] at hn
    obtain ⟨⟨a, b⟩, hn⟩ := hn
    rw [← map_pow, ← map_mul, IsLocalization.eq_iff_exists p.primeCompl] at hn
    obtain ⟨t, ht⟩ := hn
    refine ⟨t * b, fun h ↦ (t * b).2 (hp₁.radical_le_iff.mpr hp₂ h), n + 1, ?_⟩
    simp only at ht
    have : (x * (t.1 * b.1)) ^ (n + 1) = (t.1 ^ n * b.1 ^ n * x * t.1) * a := by
      rw [mul_assoc, ← ht]; ring
    rw [this]
    exact I.mul_mem_left _ a.2
  · rintro ⟨y, hy, hx⟩
    obtain ⟨p, hp, hyp⟩ : ∃ p ∈ I.minimalPrimes, y ∉ p := by
      simpa [← Ideal.sInf_minimalPrimes] using hy
    refine ⟨p, hp, (hp.isPrime.mem_or_mem ?_).resolve_right hyp⟩
    exact hp.isPrime.radical_le_iff.mpr hp.le hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
h :
  ∀ (x : R),
    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
h₁ : ∀ (x : R), (∃ (i : Ideal R), I.IsMinimalPrime i ∧ x ∈ i) ↔ ∃ y ∉ I.radical, x * y ∈ I.radical
h₂ : ∀ (x : R), (∃ (i : Ideal R), I.IsMinimalPrime i ∧ x ∈ i) → ∃ y ∉ I.radical, x * y ∈ I.radical
⊢ Eq.{u_1 + 1} (α := Set R) (⋃ p ∈ I.minimalPrimes, (↑p : Set R)) {x : R | ∃ y ∉ I.radical, x * y ∈ I.radical}
have h₃ : ∀ (x : R), (∃ y ∉ I.radical, x * y ∈ I.radical) → ∃ (i : Ideal R), I.IsMinimalPrime i ∧ x ∈ i
Tactic: classical
  ext x
  simp only [Set.mem_iUnion, SetLike.mem_coe, exists_prop, Set.mem_setOf_eq]
  constructor
  · rintro ⟨p, ⟨⟨hp₁, hp₂⟩, hp₃⟩, hxp⟩
    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₂
    obtain ⟨n, hn⟩ := this (Ideal.mem_map_of_mem _ hxp)
    rw [IsLocalization.mem_map_algebraMap_iff (M := p.primeCompl)] at hn
    obtain ⟨⟨a, b⟩, hn⟩ := hn
    rw [← map_pow, ← map_mul, IsLocalization.eq_iff_exists p.primeCompl] at hn
    obtain ⟨t, ht⟩ := hn
    refine ⟨t * b, fun h ↦ (t * b).2 (hp₁.radical_le_iff.mpr hp₂ h), n + 1, ?_⟩
    simp only at ht
    have : (x * (t.1 * b.1)) ^ (n + 1) = (t.1 ^ n * b.1 ^ n * x * t.1) * a := by
      rw [mul_assoc, ← ht]; ring
    rw [this]
    exact I.mul_mem_left _ a.2
  · rintro ⟨y, hy, hx⟩
    obtain ⟨p, hp, hyp⟩ : ∃ p ∈ I.minimalPrimes, y ∉ p := by
      simpa [← Ideal.sInf_minimalPrimes] using hy
    refine ⟨p, hp, (hp.isPrime.mem_or_mem ?_).resolve_right hyp⟩
    exact hp.isPrime.radical_le_iff.mpr hp.le hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I p : Ideal R
hp : p ∈ I.minimalPrimes
x : R
hx : x ∈ p
⊢ ∃ y ∉ I, x * y ∈ I
have obtain : ∀ (y : R) (hy : y ∉ I.radical) (n : ℕ) (hx : (x * y) ^ n ∈ I), ∃ y ∉ I, x * y ∈ I
Tactic: obtain ⟨y, hy, n, hx⟩ := Ideal.iUnion_minimalPrimes.subset (Set.mem_biUnion hp hx)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
I p : Ideal R
hp : p ∈ I.minimalPrimes
x : R
hx_1 : x ∈ p
y : R
hy : y ∉ I.radical
n : ℕ
hx : (x * y) ^ n ∈ I
⊢ ∃ y ∉ I, x * y ∈ I
have H : ∃ (m : ℕ), x ^ m * y ^ n ∈ I
Tactic: have H : ∃ m, x ^ m * y ^ n ∈ I := ⟨n, mul_pow x y n ▸ hx⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
I p : Ideal R
hp : p ∈ I.minimalPrimes
x : R
hx_1 : x ∈ p
y : R
hy : y ∉ I.radical
n : ℕ
hx : (x * y) ^ n ∈ I
H : ∃ (m : ℕ), x ^ m * y ^ n ∈ I
⊢ ∃ y ∉ I, x * y ∈ I
have this : Nat.find (p := fun (n_1 : ℕ) ↦ x ^ n_1 * y ^ n ∈ I) H ≠ 0
Tactic: have : Nat.find H ≠ 0 :=
    fun h ↦ hy ⟨n, by simpa only [h, pow_zero, one_mul] using Nat.find_spec H⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I p : Ideal R
hp : p ∈ I.minimalPrimes
x : R
hx_1 : x ∈ p
y : R
hy : y ∉ I.radical
n : ℕ
hx : (x * y) ^ n ∈ I
H : ∃ (m : ℕ), x ^ m * y ^ n ∈ I
this : Nat.find (p := fun (n_1 : ℕ) ↦ x ^ n_1 * y ^ n ∈ I) H ≠ 0
⊢ ∃ y ∉ I, x * y ∈ I
have refine : x * (x ^ (Nat.find (p := fun (n_1 : ℕ) ↦ x ^ n_1 * y ^ n ∈ I) H - 1) * y ^ n) ∈ I
Tactic: refine ⟨x ^ (Nat.find H - 1) * y ^ n, Nat.find_min H (Nat.sub_one_lt this), ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I p : Ideal R
hp : p ∈ I.minimalPrimes
x : R
hx_1 : x ∈ p
y : R
hy : y ∉ I.radical
n : ℕ
hx : (x * y) ^ n ∈ I
H : ∃ (m : ℕ), x ^ m * y ^ n ∈ I
this : Nat.find (p := fun (n_1 : ℕ) ↦ x ^ n_1 * y ^ n ∈ I) H ≠ 0
⊢ x * (x ^ (Nat.find (p := fun (n_1 : ℕ) ↦ x ^ n_1 * y ^ n ∈ I) H - 1) * y ^ n) ∈ I
have rw : x ^ Nat.find (p := fun (n_1 : ℕ) ↦ x ^ n_1 * y ^ n ∈ I) H * y ^ n ∈ I
Tactic: rw [← mul_assoc, ← pow_succ', tsub_add_cancel_of_le (Nat.one_le_iff_ne_zero.mpr this)]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I p : Ideal R
hp : p ∈ I.minimalPrimes
x : R
hx : x ∈ p
⊢ ∃ y ∉ I, x * y ∈ I
have obtain : ∀ (y : R) (hy : y ∉ I.radical) (n : ℕ) (hx : (x * y) ^ n ∈ I), ∃ y ∉ I, x * y ∈ I
Tactic: classical
  obtain ⟨y, hy, n, hx⟩ := Ideal.iUnion_minimalPrimes.subset (Set.mem_biUnion hp hx)
  have H : ∃ m, x ^ m * y ^ n ∈ I := ⟨n, mul_pow x y n ▸ hx⟩
  have : Nat.find H ≠ 0 :=
    fun h ↦ hy ⟨n, by simpa only [h, pow_zero, one_mul] using Nat.find_spec H⟩
  refine ⟨x ^ (Nat.find H - 1) * y ^ n, Nat.find_min H (Nat.sub_one_lt this), ?_⟩
  rw [← mul_assoc, ← pow_succ', tsub_add_cancel_of_le (Nat.one_le_iff_ne_zero.mpr this)]
  exact Nat.find_spec H
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I p : Ideal R
hp : p ∈ I.minimalPrimes
x : R
hx : x ∈ p
obtain : ∀ (y : R) (hy : y ∉ I.radical) (n : ℕ) (hx : (x * y) ^ n ∈ I), ∃ y ∉ I, x * y ∈ I
⊢ ∃ y ∉ I, x * y ∈ I
have obtain₁ : ∀ (y : R) (hy : y ∉ I.radical) (n : ℕ) (hx : (x * y) ^ n ∈ I) (H : ∃ (m : ℕ), x ^ m * y ^ n ∈ I), ∃ y ∉ I, x * y ∈ I
Tactic: classical
  obtain ⟨y, hy, n, hx⟩ := Ideal.iUnion_minimalPrimes.subset (Set.mem_biUnion hp hx)
  have H : ∃ m, x ^ m * y ^ n ∈ I := ⟨n, mul_pow x y n ▸ hx⟩
  have : Nat.find H ≠ 0 :=
    fun h ↦ hy ⟨n, by simpa only [h, pow_zero, one_mul] using Nat.find_spec H⟩
  refine ⟨x ^ (Nat.find H - 1) * y ^ n, Nat.find_min H (Nat.sub_one_lt this), ?_⟩
  rw [← mul_assoc, ← pow_succ', tsub_add_cancel_of_le (Nat.one_le_iff_ne_zero.mpr this)]
  exact Nat.find_spec H
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I p : Ideal R
hp : p ∈ I.minimalPrimes
x : R
hx : x ∈ p
obtain : ∀ (y : R) (hy : y ∉ I.radical) (n : ℕ) (hx : (x * y) ^ n ∈ I), ∃ y ∉ I, x * y ∈ I
obtain₁ :
  ∀ (y : R) (hy : y ∉ I.radical) (n : ℕ) (hx : (x * y) ^ n ∈ I) (H : ∃ (m : ℕ), x ^ m * y ^ n ∈ I), ∃ y ∉ I, x * y ∈ I
⊢ ∃ y ∉ I, x * y ∈ I
have obtain₂ : ∀ (y : R) (hy : y ∉ I.radical) (n : ℕ) (hx : (x * y) ^ n ∈ I) (H : ∃ (m : ℕ), x ^ m * y ^ n ∈ I)
  (this : Nat.find (p := fun (n_1 : ℕ) ↦ x ^ n_1 * y ^ n ∈ I) H ≠ 0), ∃ y ∉ I, x * y ∈ I
Tactic: classical
  obtain ⟨y, hy, n, hx⟩ := Ideal.iUnion_minimalPrimes.subset (Set.mem_biUnion hp hx)
  have H : ∃ m, x ^ m * y ^ n ∈ I := ⟨n, mul_pow x y n ▸ hx⟩
  have : Nat.find H ≠ 0 :=
    fun h ↦ hy ⟨n, by simpa only [h, pow_zero, one_mul] using Nat.find_spec H⟩
  refine ⟨x ^ (Nat.find H - 1) * y ^ n, Nat.find_min H (Nat.sub_one_lt this), ?_⟩
  rw [← mul_assoc, ← pow_succ', tsub_add_cancel_of_le (Nat.one_le_iff_ne_zero.mpr this)]
  exact Nat.find_spec H
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I p : Ideal R
hp : p ∈ I.minimalPrimes
x : R
hx : x ∈ p
obtain : ∀ (y : R) (hy : y ∉ I.radical) (n : ℕ) (hx : (x * y) ^ n ∈ I), ∃ y ∉ I, x * y ∈ I
obtain₁ :
  ∀ (y : R) (hy : y ∉ I.radical) (n : ℕ) (hx : (x * y) ^ n ∈ I) (H : ∃ (m : ℕ), x ^ m * y ^ n ∈ I), ∃ y ∉ I, x * y ∈ I
obtain₂ :
  ∀ (y : R) (hy : y ∉ I.radical) (n : ℕ) (hx : (x * y) ^ n ∈ I) (H : ∃ (m : ℕ), x ^ m * y ^ n ∈ I)
    (this : Nat.find (p := fun (n_1 : ℕ) ↦ x ^ n_1 * y ^ n ∈ I) H ≠ 0), ∃ y ∉ I, x * y ∈ I
⊢ ∃ y ∉ I, x * y ∈ I
have obtain₃ : ∀ (y : R) (hy : y ∉ I.radical) (n : ℕ) (hx : (x * y) ^ n ∈ I) (H : ∃ (m : ℕ), x ^ m * y ^ n ∈ I)
  (this : Nat.find (p := fun (n_1 : ℕ) ↦ x ^ n_1 * y ^ n ∈ I) H ≠ 0),
  x * (x ^ (Nat.find (p := fun (n_1 : ℕ) ↦ x ^ n_1 * y ^ n ∈ I) H - 1) * y ^ n) ∈ I
Tactic: classical
  obtain ⟨y, hy, n, hx⟩ := Ideal.iUnion_minimalPrimes.subset (Set.mem_biUnion hp hx)
  have H : ∃ m, x ^ m * y ^ n ∈ I := ⟨n, mul_pow x y n ▸ hx⟩
  have : Nat.find H ≠ 0 :=
    fun h ↦ hy ⟨n, by simpa only [h, pow_zero, one_mul] using Nat.find_spec H⟩
  refine ⟨x ^ (Nat.find H - 1) * y ^ n, Nat.find_min H (Nat.sub_one_lt this), ?_⟩
  rw [← mul_assoc, ← pow_succ', tsub_add_cancel_of_le (Nat.one_le_iff_ne_zero.mpr this)]
  exact Nat.find_spec H
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I p : Ideal R
hp : p ∈ I.minimalPrimes
x : R
hx : x ∈ p
obtain : ∀ (y : R) (hy : y ∉ I.radical) (n : ℕ) (hx : (x * y) ^ n ∈ I), ∃ y ∉ I, x * y ∈ I
obtain₁ :
  ∀ (y : R) (hy : y ∉ I.radical) (n : ℕ) (hx : (x * y) ^ n ∈ I) (H : ∃ (m : ℕ), x ^ m * y ^ n ∈ I), ∃ y ∉ I, x * y ∈ I
obtain₂ :
  ∀ (y : R) (hy : y ∉ I.radical) (n : ℕ) (hx : (x * y) ^ n ∈ I) (H : ∃ (m : ℕ), x ^ m * y ^ n ∈ I)
    (this : Nat.find (p := fun (n_1 : ℕ) ↦ x ^ n_1 * y ^ n ∈ I) H ≠ 0), ∃ y ∉ I, x * y ∈ I
obtain₃ :
  ∀ (y : R) (hy : y ∉ I.radical) (n : ℕ) (hx : (x * y) ^ n ∈ I) (H : ∃ (m : ℕ), x ^ m * y ^ n ∈ I)
    (this : Nat.find (p := fun (n_1 : ℕ) ↦ x ^ n_1 * y ^ n ∈ I) H ≠ 0),
    x * (x ^ (Nat.find (p := fun (n_1 : ℕ) ↦ x ^ n_1 * y ^ n ∈ I) H - 1) * y ^ n) ∈ I
⊢ ∃ y ∉ I, x * y ∈ I
have obtain₄ : ∀ (y : R) (hy : y ∉ I.radical) (n : ℕ) (hx : (x * y) ^ n ∈ I) (H : ∃ (m : ℕ), x ^ m * y ^ n ∈ I)
  (this : Nat.find (p := fun (n_1 : ℕ) ↦ x ^ n_1 * y ^ n ∈ I) H ≠ 0),
  x ^ Nat.find (p := fun (n_1 : ℕ) ↦ x ^ n_1 * y ^ n ∈ I) H * y ^ n ∈ I
Tactic: classical
  obtain ⟨y, hy, n, hx⟩ := Ideal.iUnion_minimalPrimes.subset (Set.mem_biUnion hp hx)
  have H : ∃ m, x ^ m * y ^ n ∈ I := ⟨n, mul_pow x y n ▸ hx⟩
  have : Nat.find H ≠ 0 :=
    fun h ↦ hy ⟨n, by simpa only [h, pow_zero, one_mul] using Nat.find_spec H⟩
  refine ⟨x ^ (Nat.find H - 1) * y ^ n, Nat.find_min H (Nat.sub_one_lt this), ?_⟩
  rw [← mul_assoc, ← pow_succ', tsub_add_cancel_of_le (Nat.one_le_iff_ne_zero.mpr this)]
  exact Nat.find_spec H
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : R
reg : IsSMulRegular M x
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (Module.annihilator R M)) p
hx : x ∈ p
⊢ False
have rcases : ∀ (y : R) (hy : y ∉ Module.annihilator R M) (hxy : Membership.mem (γ := Ideal R) (Module.annihilator R M) (x * y)),
  False
Tactic: rcases Ideal.exists_mul_mem_of_mem_minimalPrimes hp hx with ⟨y, hy, hxy⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : R
reg : IsSMulRegular M x
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (Module.annihilator R M)) p
hx : x ∈ p
y : R
hy : y ∉ Module.annihilator R M
hxy : Membership.mem (γ := Ideal R) (Module.annihilator R M) (x * y)
⊢ False
have rcases : ∀ (m : M) (hm : ¬y • m = 0), False
Tactic: rcases not_forall.mp (Module.mem_annihilator.not.mp hy) with ⟨m, hm⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) p
⊢ Disjoint (↑p : Set R) (↑(nonZeroDivisors R) : Set R)
have simp_rw : ∀ ⦃a : R⦄, a ∈ p → ∃ (x : R), ¬x = 0 ∧ a * x = 0
Tactic: simp_rw [Set.disjoint_left, SetLike.mem_coe, mem_nonZeroDivisors_iff_right, not_forall,
    exists_prop, @and_comm (_ * _ = _), ← mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : Ideal R
H : Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) p
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap f ⊥)) p
have rwa : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) p
Tactic: rwa [comap_bot_of_injective f hf]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
I : Ideal S
f : R →+* S
p : Ideal R
H : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap f I)) p
⊢ ∃ p' ∈ I.minimalPrimes, comap f p' = p
have obtain : ∀ (p' : Ideal S) (h₁ : p'.IsPrime) (h₂ : I ≤ p') (h₃ : comap f p' = p), ∃ p' ∈ I.minimalPrimes, comap f p' = p
Tactic: obtain ⟨p', h₁, h₂, h₃⟩ := Ideal.exists_comap_eq_of_mem_minimalPrimes f p H
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
I : Ideal S
f : R →+* S
p : Ideal R
H : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap f I)) p
p' : Ideal S
h₁ : p'.IsPrime
h₂ : I ≤ p'
h₃ : comap f p' = p
⊢ ∃ p' ∈ I.minimalPrimes, comap f p' = p
have obtain : ∀ (q : Ideal S) (hq : q ∈ I.minimalPrimes) (hq' : q ≤ p'), ∃ p' ∈ I.minimalPrimes, comap f p' = p
Tactic: obtain ⟨q, hq, hq'⟩ := Ideal.exists_minimalPrimes_le h₂
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
I : Ideal S
f : R →+* S
p : Ideal R
H : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap f I)) p
p' : Ideal S
h₁ : p'.IsPrime
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ I.minimalPrimes
hq' : q ≤ p'
⊢ ∃ p' ∈ I.minimalPrimes, comap f p' = p
have refine : p = comap f q
Tactic: refine ⟨q, hq, Eq.symm ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
I : Ideal S
f : R →+* S
p : Ideal R
H : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap f I)) p
p' : Ideal S
h₁ : p'.IsPrime
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ I.minimalPrimes
hq' : q ≤ p'
⊢ p = comap f q
have this : q.IsPrime
Tactic: have := hq.isPrime
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
I : Ideal S
f : R →+* S
p : Ideal R
H : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap f I)) p
p' : Ideal S
h₁ : p'.IsPrime
h₂ : I ≤ p'
h₃ : comap f p' = p
q : Ideal S
hq : q ∈ I.minimalPrimes
hq' : q ≤ p'
this : q.IsPrime
⊢ p = comap f q
have this₁ : comap f q ≤ p
Tactic: have := (Ideal.comap_mono hq').trans_eq h₃
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I J : Ideal S
h : J ∈ I.minimalPrimes
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap f I)) (comap f J)
have this : J.IsPrime
Tactic: have := h.isPrime
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I J : Ideal S
h : J ∈ I.minimalPrimes
this : J.IsPrime
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap f I)) (comap f J)
have refine : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ comap f I ≤ q) y → y ≤ comap f J → comap f J ≤ y
Tactic: refine ⟨⟨inferInstance, Ideal.comap_mono h.le⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I J : Ideal S
h : J ∈ I.minimalPrimes
this : J.IsPrime
K : Ideal R
hK : K.IsPrime
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
⊢ comap f J ≤ K
have this₁ : RingHom.ker f ≤ K
Tactic: have : RingHom.ker f ≤ K := (Ideal.comap_mono bot_le).trans e₁
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I J : Ideal S
h : J ∈ I.minimalPrimes
this_1 : J.IsPrime
K : Ideal R
hK : K.IsPrime
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ comap f J ≤ K
have rw : LE.le (α := Ideal R) (comap f J) (comap f (map f K))
Tactic: rw [← sup_eq_left.mpr this, RingHom.ker_eq_comap_bot, ← Ideal.comap_map_of_surjective f hf]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I J : Ideal S
h : J ∈ I.minimalPrimes
this_1 : J.IsPrime
K : Ideal R
hK : K.IsPrime
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ LE.le (α := Ideal R) (comap f J) (comap f (map f K))
have apply : J ≤ map f K
Tactic: apply Ideal.comap_mono _
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I J : Ideal S
h : J ∈ I.minimalPrimes
this_1 : J.IsPrime
K : Ideal R
hK : K.IsPrime
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ J ≤ map f K
have apply : IsPrime.{u_2} (α := S) (map f K) ∧ I ≤ map f K
Tactic: apply h.2 _ _
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I J : Ideal S
h : J ∈ I.minimalPrimes
this_1 : J.IsPrime
K : Ideal R
hK : K.IsPrime
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
apply : IsPrime.{u_2} (α := S) (map f K) ∧ I ≤ map f K
⊢ J ≤ map f K
have apply₁ : map f K ≤ J
Tactic: apply h.2 _ _
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal S
⊢ Eq (α := Set (Ideal R)) (Ideal.minimalPrimes (comap f I)) (comap f '' I.minimalPrimes)
have h : ∀ (J : Ideal R),
  Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap f I)) J ↔
    Membership.mem (γ := Set (Ideal R)) (comap f '' I.minimalPrimes) J
Tactic: ext J