R : Type u
ι : Type ?u.327198
inst✝ : CommSemiring R
I✝ J K L I : Ideal R
r : R
hr : r ∈ sInf {J | I ≤ J ∧ IsPrime J}
hri : ¬r ∈ radical I
hrm : ¬r ∈ radical ⊤
him : I ≤ ⊤
hm : ∀ (z : Ideal R), z ∈ {K | ¬r ∈ radical K} → ⊤ ≤ z → z = ⊤
this : ∀ (x : R), ¬x ∈ ⊤ → r ∈ radical (⊤ ⊔ span {x})
⊢ False
R : Type u
ι : Type ?u.327198
inst✝ : CommSemiring R
I✝ J K L I : Ideal R
r : R
hr : r ∈ sInf {J | I ≤ J ∧ IsPrime J}
hri : ¬r ∈ radical I
m : Ideal R
hrm : ¬r ∈ radical m
him : I ≤ m
hm : ∀ (z : Ideal R), z ∈ {K | ¬r ∈ radical K} → m ≤ z → z = m
this : ∀ (x : R), ¬x ∈ m → r ∈ radical (m ⊔ span {x})
⊢ m ≠ ⊤
rintro rfl
R : Type u
ι : Type ?u.327198
inst✝ : CommSemiring R
I✝ J K L I : Ideal R
r : R
hr : r ∈ sInf {J | I ≤ J ∧ IsPrime J}
hri : ¬r ∈ radical I
hrm : ¬r ∈ ⊤
him : I ≤ ⊤
hm : ∀ (z : Ideal R), z ∈ {K | ¬r ∈ radical K} → ⊤ ≤ z → z = ⊤
this : ∀ (x : R), ¬x ∈ ⊤ → r ∈ radical (⊤ ⊔ span {x})
⊢ False
R : Type u
ι : Type ?u.327198
inst✝ : CommSemiring R
I✝ J K L I : Ideal R
r : R
hr : r ∈ sInf {J | I ≤ J ∧ IsPrime J}
hri : ¬r ∈ radical I
hrm : ¬r ∈ radical ⊤
him : I ≤ ⊤
hm : ∀ (z : Ideal R), z ∈ {K | ¬r ∈ radical K} → ⊤ ≤ z → z = ⊤
this : ∀ (x : R), ¬x ∈ ⊤ → r ∈ radical (⊤ ⊔ span {x})
⊢ False
rw [radical_top] at hrm
no goals
R : Type u
ι : Type ?u.327198
inst✝ : CommSemiring R
I✝ J K L I : Ideal R
r : R
hr : r ∈ sInf {J | I ≤ J ∧ IsPrime J}
hri : ¬r ∈ radical I
hrm : ¬r ∈ ⊤
him : I ≤ ⊤
hm : ∀ (z : Ideal R), z ∈ {K | ¬r ∈ radical K} → ⊤ ≤ z → z = ⊤
this : ∀ (x : R), ¬x ∈ ⊤ → r ∈ radical (⊤ ⊔ span {x})
⊢ False
exact hrm trivial
R : Type u
ι : Type ?u.327198
inst✝ : CommSemiring R
I✝ J K L I : Ideal R
r : R
hr : r ∈ sInf {J | I ≤ J ∧ IsPrime J}
hri : ¬r ∈ radical I
m : Ideal R
hrm : ¬r ∈ radical m
him : I ≤ m
hm : ∀ (z : Ideal R), z ∈ {K | ¬r ∈ radical K} → m ≤ z → z = m
this : ∀ (x : R), ¬x ∈ m → r ∈ radical (m ⊔ span {x})
x y : R
hxym : x * y ∈ m
hxm : ¬x ∈ m
hym : ¬y ∈ m
n : ℕ
hrn : r ^ n ∈ m ⊔ span {x}
p : R
hpm : p ∈ m
q : R
hq : q ∈ span {x}
hpqrn : p + q = r ^ n
c : R
hcxq : c * x = q
k : ℕ
hrk : r ^ k ∈ m ⊔ span {y}
f : R
hfm : f ∈ m
g : R
hg : g ∈ span {y}
hfgrk : f + g = r ^ k
d : R
hdyg : d * y = g
⊢ p * (f + d * y) + (c * x * f + c * d * (x * y)) ∈ m
R : Type u
ι : Type ?u.327198
inst✝ : CommSemiring R
I✝ J K L I : Ideal R
r : R
hr : r ∈ sInf {J | I ≤ J ∧ IsPrime J}
hri : ¬r ∈ radical I
m : Ideal R
hrm : ¬r ∈ radical m
him : I ≤ m
hm : ∀ (z : Ideal R), z ∈ {K | ¬r ∈ radical K} → m ≤ z → z = m
this : ∀ (x : R), ¬x ∈ m → r ∈ radical (m ⊔ span {x})
x y : R
hxym : x * y ∈ m
hxm : ¬x ∈ m
hym : ¬y ∈ m
n : ℕ
hrn : r ^ n ∈ m ⊔ span {x}
p : R
hpm : p ∈ m
q : R
hq : q ∈ span {x}
hpqrn : p + q = r ^ n
c : R
hcxq : c * x = q
k : ℕ
hrk : r ^ k ∈ m ⊔ span {y}
f : R
hfm : f ∈ m
g : R
hg : g ∈ span {y}
hfgrk : f + g = r ^ k
d : R
hdyg : d * y = g
⊢ r ^ (n + k) ∈ m
rw [pow_add, ← hpqrn, ← hcxq, ← hfgrk, ← hdyg, add_mul, mul_add (c * x),
    mul_assoc c x (d * y), mul_left_comm x, ← mul_assoc]
no goals
R : Type u
ι : Type ?u.327198
inst✝ : CommSemiring R
I✝ J K L I : Ideal R
r : R
hr : r ∈ sInf {J | I ≤ J ∧ IsPrime J}
hri : ¬r ∈ radical I
m : Ideal R
hrm : ¬r ∈ radical m
him : I ≤ m
hm : ∀ (z : Ideal R), z ∈ {K | ¬r ∈ radical K} → m ≤ z → z = m
this : ∀ (x : R), ¬x ∈ m → r ∈ radical (m ⊔ span {x})
x y : R
hxym : x * y ∈ m
hxm : ¬x ∈ m
hym : ¬y ∈ m
n : ℕ
hrn : r ^ n ∈ m ⊔ span {x}
p : R
hpm : p ∈ m
q : R
hq : q ∈ span {x}
hpqrn : p + q = r ^ n
c : R
hcxq : c * x = q
k : ℕ
hrk : r ^ k ∈ m ⊔ span {y}
f : R
hfm : f ∈ m
g : R
hg : g ∈ span {y}
hfgrk : f + g = r ^ k
d : R
hdyg : d * y = g
⊢ p * (f + d * y) + (c * x * f + c * d * (x * y)) ∈ m
refine'
  m.add_mem (m.mul_mem_right _ hpm)
    (m.add_mem (m.mul_mem_left _ hfm) (m.mul_mem_left _ hxym))