awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
h₃ h₄ : ∀ (x : R), (∃ y ∉ I.radical, x * y ∈ I.radical) → ∃ (i : Ideal R), I.IsMinimalPrime i ∧ x ∈ i
⊢ Eq.{u_1 + 1} (α := Set R) (⋃ p ∈ I.minimalPrimes, (↑p : Set R)) {x : R | ∃ 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

Premises used: Ideal.minimalPrimes, Set.mem_iUnion, Set.mem_setOf_eq, map_pow, exists_prop, map_mul, SetLike.mem_coe
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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

Tactic:
obtain ⟨y, hy, n, hx⟩ := Ideal.iUnion_minimalPrimes.subset (Set.mem_biUnion hp hx)

Premises used: Set.mem_biUnion, Eq.subset, Ideal.iUnion_minimalPrimes
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
⊢ ∃ (m : ℕ), x ^ m * y ^ n ∈ I

Tactic:
have H : ∃ m, x ^ m * y ^ n ∈ I := ⟨n, mul_pow x y n ▸ hx⟩
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
h : Nat.find (p := fun (n_1 : ℕ) ↦ x ^ n_1 * y ^ n ∈ I) H = 0
⊢ y ^ n ∈ I

Tactic:
simpa only [h, pow_zero, one_mul] using Nat.find_spec H

Premises used: pow_zero, one_mul, Nat.find_spec
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
⊢ 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⟩
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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

Tactic:
⟨x ^ (Nat.find H - 1) * y ^ n, Nat.find_min H (Nat.sub_one_lt this), ?_⟩

Premises used: HMul.hMul, Nat.sub_one_lt, HSub.hSub, Nat.find_min, HPow.hPow, And.intro, Nat.find, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
refine : x * (x ^ (Nat.find (p := fun (n_1 : ℕ) ↦ x ^ n_1 * y ^ n ∈ I) H - 1) * y ^ n) ∈ I
⊢ ∃ y ∉ I, x * y ∈ I

Tactic:
refine ⟨x ^ (Nat.find H - 1) * y ^ n, Nat.find_min H (Nat.sub_one_lt this), ?_⟩
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
rw : x ^ Nat.find (p := fun (n_1 : ℕ) ↦ x ^ n_1 * y ^ n ∈ I) H * y ^ n ∈ I
⊢ x * (x ^ (Nat.find (p := fun (n_1 : ℕ) ↦ x ^ n_1 * y ^ n ∈ I) H - 1) * y ^ n) ∈ I

Tactic:
rw [← mul_assoc, ← pow_succ', tsub_add_cancel_of_le (Nat.one_le_iff_ne_zero.mpr this)]

Premises used: Iff.mpr, mul_assoc, tsub_add_cancel_of_le, Nat.one_le_iff_ne_zero, pow_succ'
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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 ^ Nat.find (p := fun (n_1 : ℕ) ↦ x ^ n_1 * y ^ n ∈ I) H * y ^ n ∈ I

Tactic:
Nat.find_spec H

Premises used: Set.Mem, Nat.find_spec
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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 ^ Nat.find (p := fun (n_1 : ℕ) ↦ x ^ n_1 * y ^ n ∈ I) H * y ^ n ∈ I

Tactic:
exact Nat.find_spec H

Premises used: Nat.find_spec
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
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
⊢ ∃ 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

Premises used: mul_assoc, Set.mem_biUnion, Eq.subset, Ideal.iUnion_minimalPrimes, pow_succ'
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
rcases :
  ∀ (y : R) (hy : y ∉ Module.annihilator R M) (hxy : Membership.mem (γ := Ideal R) (Module.annihilator R M) (x * y)),
    False
⊢ False

Tactic:
rcases Ideal.exists_mul_mem_of_mem_minimalPrimes hp hx with ⟨y, hy, hxy⟩

Premises used: Ideal.exists_mul_mem_of_mem_minimalPrimes
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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)
rcases : ∀ (m : M) (hm : ¬y • m = 0), False
⊢ False

Tactic:
rcases not_forall.mp (Module.mem_annihilator.not.mp hy) with ⟨m, hm⟩

Premises used: Module.mem_annihilator, Iff.not, Iff.mp, Classical.not_forall
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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)
m : M
hm : ¬y • m = 0
⊢ False

Tactic:
hm (reg.right_eq_zero_of_smul ((smul_smul x y m).trans (Module.mem_annihilator.mp hxy m)))

Premises used: Module.mem_annihilator, smul_smul, Iff.mp, IsSMulRegular.right_eq_zero_of_smul, Eq.trans
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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)
m : M
hm : ¬y • m = 0
⊢ False

Tactic:
exact hm (reg.right_eq_zero_of_smul ((smul_smul x y m).trans (Module.mem_annihilator.mp hxy m)))

Premises used: Module.mem_annihilator, smul_smul, Iff.mp, IsSMulRegular.right_eq_zero_of_smul, Eq.trans
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) p
simp_rw : ∀ ⦃a : R⦄, a ∈ p → ∃ (x : R), ¬x = 0 ∧ a * x = 0
⊢ Disjoint (↑p : Set R) (↑(nonZeroDivisors R) : Set R)

Tactic:
simp_rw [Set.disjoint_left, SetLike.mem_coe, mem_nonZeroDivisors_iff_right, not_forall,
    exists_prop, @and_comm (_ * _ = _), ← mul_comm]

Premises used: Set.disjoint_left, mem_nonZeroDivisors_iff_right, and_comm, exists_prop, SetLike.mem_coe, mul_comm, Classical.not_forall
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) p
⊢ ∀ ⦃a : R⦄, a ∈ p → ∃ (x : R), ¬x = 0 ∧ a * x = 0

Tactic:
fun _ ↦ Ideal.exists_mul_mem_of_mem_minimalPrimes hp

Premises used: Ideal.exists_mul_mem_of_mem_minimalPrimes, Set.Mem, setOf, Set.singleton
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) p
⊢ ∀ ⦃a : R⦄, a ∈ p → ∃ (x : R), ¬x = 0 ∧ a * x = 0

Tactic:
exact fun _ ↦ Ideal.exists_mul_mem_of_mem_minimalPrimes hp

Premises used: Ideal.exists_mul_mem_of_mem_minimalPrimes
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
x : R
q : Ideal R
hx : x ∈ q
hq : Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) q
⊢ x ∉ nonZeroDivisors R

Tactic:
Set.disjoint_left.mp (Ideal.disjoint_nonZeroDivisors_of_mem_minimalPrimes hq) hx

Premises used: Set.disjoint_left, Ideal.disjoint_nonZeroDivisors_of_mem_minimalPrimes, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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), p'.IsPrime ∧ I ≤ p' ∧ comap f p' = p

Tactic:
have := H.isPrime
  have ⟨p', hIp', hp', le⟩ := exists_ideal_comap_le_prime p I H.le
  ⟨p', hp', hIp', le.antisymm (H.2 ⟨inferInstance, comap_mono hIp'⟩ le)⟩

Premises used: Ideal.IsMinimalPrime.le, _private.0.Ideal.exists_comap_eq_of_mem_minimalPrimes.match_1, Exists, LE.le.antisymm, inferInstance, Ideal.exists_ideal_comap_le_prime, LE.le, Ideal.comap_mono, Ideal.IsMinimalPrime.isPrime, And, And.right, And.intro, Ideal.IsPrime, Ideal.comap, Exists.intro, Eq
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
rwa rwa₁ rwa₂ rwa₃ : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) p
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap f ⊥)) p

Tactic:
rwa [comap_bot_of_injective f hf]

Premises used: Ideal.comap_bot_of_injective
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
obtain : ∀ (p' : Ideal S) (h₁ : p'.IsPrime) (h₂ : I ≤ p') (h₃ : comap f p' = p), ∃ p' ∈ I.minimalPrimes, 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

Premises used: Ideal.exists_comap_eq_of_mem_minimalPrimes
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
obtain : ∀ (q : Ideal S) (hq : q ∈ I.minimalPrimes) (hq' : q ≤ p'), ∃ p' ∈ I.minimalPrimes, comap f p' = p
⊢ ∃ p' ∈ I.minimalPrimes, comap f p' = p

Tactic:
obtain ⟨q, hq, hq'⟩ := Ideal.exists_minimalPrimes_le h₂

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

Tactic:
⟨q, hq, Eq.symm ?_⟩

Premises used: And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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'
refine : p = comap f q
⊢ ∃ p' ∈ I.minimalPrimes, comap f p' = p

Tactic:
refine ⟨q, hq, Eq.symm ?_⟩
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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'
⊢ q.IsPrime

Tactic:
have := hq.isPrime
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
⊢ comap f q ≤ p

Tactic:
have := (Ideal.comap_mono hq').trans_eq h₃
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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_1 : q.IsPrime
this : comap f q ≤ p
⊢ p = comap f q

Tactic:
(H.2 ⟨inferInstance, Ideal.comap_mono hq.le⟩ this).antisymm this

Premises used: Ideal.IsMinimalPrime.le, LE.le.antisymm, inferInstance, Ideal.comap_mono, And.right, And.intro
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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_1 : q.IsPrime
this : comap f q ≤ p
⊢ p = comap f q

Tactic:
exact (H.2 ⟨inferInstance, Ideal.comap_mono hq.le⟩ this).antisymm this

Premises used: Ideal.IsMinimalPrime.le, LE.le.antisymm, inferInstance, Ideal.comap_mono, And.right, And.intro
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
J : Ideal S
⊢ Subset (α := Set (Ideal R)) (Ideal.minimalPrimes (comap f J)) (comap f '' J.minimalPrimes)

Tactic:
fun p hp ↦ Ideal.exists_minimalPrimes_comap_eq f p hp

Premises used: Set.Mem, setOf, Set.Subset, Set.image, Ideal.exists_minimalPrimes_comap_eq
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
⊢ J.IsPrime

Tactic:
have := h.isPrime
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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)

Tactic:
⟨⟨inferInstance, Ideal.comap_mono h.le⟩, ?_⟩

Premises used: Set.Mem, Ideal.IsMinimalPrime.le, setOf, inferInstance, Ideal.comap_mono, Ideal.IsMinimalPrime, And.intro, Minimal
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
refine : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ comap f I ≤ q) y → y ≤ comap f J → comap f J ≤ y
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap f I)) (comap f J)

Tactic:
refine ⟨⟨inferInstance, Ideal.comap_mono h.le⟩, ?_⟩
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
⊢ RingHom.ker f ≤ K

Tactic:
have : RingHom.ker f ≤ K := (Ideal.comap_mono bot_le).trans e₁
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
rw : LE.le (α := Ideal R) (comap f J) (comap f (map f K))
⊢ comap f J ≤ K

Tactic:
rw [← sup_eq_left.mpr this, RingHom.ker_eq_comap_bot, ← Ideal.comap_map_of_surjective f hf]

Premises used: Iff.mpr, sup_eq_left, Ideal.comap_map_of_surjective, RingHom.ker_eq_comap_bot
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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 : J ≤ map f K
⊢ LE.le (α := Ideal R) (comap f J) (comap f (map f K))

Tactic:
apply Ideal.comap_mono _

Premises used: Ideal.comap_mono
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
apply₁ : map f K ≤ J
⊢ J ≤ map f K

Tactic:
apply h.2 _ _

Premises used: And.right
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
⊢ IsPrime.{u_2} (α := S) (map f K) ∧ I ≤ map f K

Tactic:
⟨Ideal.map_isPrime_of_surjective hf this, Ideal.le_map_of_comap_le_of_surjective f hf e₁⟩

Premises used: Ideal.le_map_of_comap_le_of_surjective, And.intro, Ideal.map_isPrime_of_surjective
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
⊢ IsPrime.{u_2} (α := S) (map f K) ∧ I ≤ map f K

Tactic:
exact ⟨Ideal.map_isPrime_of_surjective hf this, Ideal.le_map_of_comap_le_of_surjective f hf e₁⟩
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
⊢ map f K ≤ J

Tactic:
Ideal.map_le_of_le_comap e₂

Premises used: Set.Mem, Ideal.map_le_of_le_comap
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
⊢ map f K ≤ J

Tactic:
exact Ideal.map_le_of_le_comap e₂

Premises used: Ideal.map_le_of_le_comap
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
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
⊢ Eq (α := Set (Ideal R)) (Ideal.minimalPrimes (comap f I)) (comap f '' I.minimalPrimes)

Tactic:
ext J