R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I : Ideal A
⊢ I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I : Ideal A
h_nzI : I ≠ ⊥
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
revert h_nzI
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
⊢ (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) M
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I : Ideal A
⊢ I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
refine' IsNoetherian.induction (P := fun I => I ≠ ⊥ → ∃ Z : Multiset (PrimeSpectrum A),
    Multiset.prod (Z.map asIdeal) ≤ I ∧ Multiset.prod (Z.map asIdeal) ≠ ⊥)
  (fun (M : Ideal A) hgt => _) I
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
⊢ (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) M
intro h_nzM
case hA_nont
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
⊢ Nontrivial A

R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
have hA_nont : Nontrivial A
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
case hA_nont
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
⊢ Nontrivial A

R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
apply IsDomain.toNontrivial
case pos
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : M = ⊤
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥

case neg
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
by_cases h_topM : M = ⊤
case pos
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : Ideal.IsPrime M
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥

case neg
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
case neg
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
by_cases h_prM : M.IsPrime
case neg.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
case neg
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
obtain ⟨x, hx, y, hy, h_xy⟩ := (Ideal.not_isPrime_iff.mp h_prM).resolve_left h_topM
case neg.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
case neg.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
have lt_add : ∀ (z) (_ : z ∉ M), M < M + span A {z} := by
  intro z hz
  refine' lt_of_le_of_ne le_sup_left fun m_eq => hz _
  rw [m_eq]
  exact mem_sup_right (mem_span_singleton_self z)
case neg.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
case neg.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
obtain ⟨Wx, h_Wx_le, h_Wx_ne⟩ := hgt (M + span A {x}) (lt_add _ hx) (ne_bot_of_gt (lt_add _ hx))
case neg.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne✝ : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span A {y}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
case neg.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
obtain ⟨Wy, h_Wy_le, h_Wx_ne⟩ := hgt (M + span A {y}) (lt_add _ hy) (ne_bot_of_gt (lt_add _ hy))
case neg.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne✝ : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span A {y}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
⊢ Multiset.prod (Multiset.map asIdeal (Wx + Wy)) ≤ M ∧ Multiset.prod (Multiset.map asIdeal (Wx + Wy)) ≠ ⊥
case neg.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne✝ : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span A {y}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
use Wx + Wy
case neg.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne✝ : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span A {y}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
⊢ Multiset.prod (Multiset.map asIdeal Wx) * Multiset.prod (Multiset.map asIdeal Wy) ≤ M ∧
    Multiset.prod (Multiset.map asIdeal Wx) * Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
case neg.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne✝ : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span A {y}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
⊢ Multiset.prod (Multiset.map asIdeal (Wx + Wy)) ≤ M ∧ Multiset.prod (Multiset.map asIdeal (Wx + Wy)) ≠ ⊥
rw [Multiset.map_add, Multiset.prod_add]
case neg.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne✝ : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span A {y}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
⊢ (M + span A {x}) * (M + span A {y}) ≤ M

case neg.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne✝ : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span A {y}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
⊢ ¬(Multiset.prod (Multiset.map asIdeal Wx) = ⊥ ∨ Multiset.prod (Multiset.map asIdeal Wy) = ⊥)
case neg.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne✝ : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span A {y}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
⊢ Multiset.prod (Multiset.map asIdeal Wx) * Multiset.prod (Multiset.map asIdeal Wy) ≤ M ∧
    Multiset.prod (Multiset.map asIdeal Wx) * Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
refine' ⟨le_trans (Submodule.mul_le_mul h_Wx_le h_Wy_le) _, mt Ideal.mul_eq_bot.mp _⟩
case pos
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I : Ideal A
hA_nont : Nontrivial A
hgt :
  ∀ (J : Submodule A A),
    J > ⊤ →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : ⊤ ≠ ⊥
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ ⊤ ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
case pos
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : M = ⊤
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
rcases h_topM with rfl
case pos.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I : Ideal A
hA_nont : Nontrivial A
hgt :
  ∀ (J : Submodule A A),
    J > ⊤ →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : ⊤ ≠ ⊥
p_id : Ideal A
h_nzp : p_id ≠ ⊥
h_pp : Ideal.IsPrime p_id
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ ⊤ ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
case pos
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I : Ideal A
hA_nont : Nontrivial A
hgt :
  ∀ (J : Submodule A A),
    J > ⊤ →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : ⊤ ≠ ⊥
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ ⊤ ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
obtain ⟨p_id, h_nzp, h_pp⟩ : ∃ p : Ideal A, p ≠ ⊥ ∧ p.IsPrime := by
  apply Ring.not_isField_iff_exists_prime.mp h_fA
case pos.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I : Ideal A
hA_nont : Nontrivial A
hgt :
  ∀ (J : Submodule A A),
    J > ⊤ →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : ⊤ ≠ ⊥
p_id : Ideal A
h_nzp : p_id ≠ ⊥
h_pp : Ideal.IsPrime p_id
⊢ Multiset.prod (Multiset.map asIdeal {{ asIdeal := p_id, IsPrime := h_pp }}) ≠ ⊥
case pos.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I : Ideal A
hA_nont : Nontrivial A
hgt :
  ∀ (J : Submodule A A),
    J > ⊤ →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : ⊤ ≠ ⊥
p_id : Ideal A
h_nzp : p_id ≠ ⊥
h_pp : Ideal.IsPrime p_id
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ ⊤ ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
use ({⟨p_id, h_pp⟩} : Multiset (PrimeSpectrum A)), le_top
no goals
case pos.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I : Ideal A
hA_nont : Nontrivial A
hgt :
  ∀ (J : Submodule A A),
    J > ⊤ →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : ⊤ ≠ ⊥
p_id : Ideal A
h_nzp : p_id ≠ ⊥
h_pp : Ideal.IsPrime p_id
⊢ Multiset.prod (Multiset.map asIdeal {{ asIdeal := p_id, IsPrime := h_pp }}) ≠ ⊥
rwa [Multiset.map_singleton, Multiset.prod_singleton]
no goals
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I : Ideal A
hA_nont : Nontrivial A
hgt :
  ∀ (J : Submodule A A),
    J > ⊤ →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : ⊤ ≠ ⊥
⊢ ∃ p, p ≠ ⊥ ∧ Ideal.IsPrime p
apply Ring.not_isField_iff_exists_prime.mp h_fA
case pos
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : Ideal.IsPrime M
⊢ Multiset.prod (Multiset.map asIdeal {{ asIdeal := M, IsPrime := h_prM }}) ≤ M ∧
    Multiset.prod (Multiset.map asIdeal {{ asIdeal := M, IsPrime := h_prM }}) ≠ ⊥
case pos
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : Ideal.IsPrime M
⊢ ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ M ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥
use ({⟨M, h_prM⟩} : Multiset (PrimeSpectrum A))
case pos
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : Ideal.IsPrime M
⊢ { asIdeal := M, IsPrime := h_prM }.asIdeal ≤ M ∧ { asIdeal := M, IsPrime := h_prM }.asIdeal ≠ ⊥
case pos
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : Ideal.IsPrime M
⊢ Multiset.prod (Multiset.map asIdeal {{ asIdeal := M, IsPrime := h_prM }}) ≤ M ∧
    Multiset.prod (Multiset.map asIdeal {{ asIdeal := M, IsPrime := h_prM }}) ≠ ⊥
rw [Multiset.map_singleton, Multiset.prod_singleton]
no goals
case pos
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : Ideal.IsPrime M
⊢ { asIdeal := M, IsPrime := h_prM }.asIdeal ≤ M ∧ { asIdeal := M, IsPrime := h_prM }.asIdeal ≠ ⊥
exact ⟨le_rfl, h_nzM⟩
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
z : A
hz : ¬z ∈ M
⊢ M < M + span A {z}
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
⊢ ∀ (z : A), ¬z ∈ M → M < M + span A {z}
intro z hz
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
z : A
hz : ¬z ∈ M
m_eq : M = M + span A {z}
⊢ z ∈ M
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
z : A
hz : ¬z ∈ M
⊢ M < M + span A {z}
refine' lt_of_le_of_ne le_sup_left fun m_eq => hz _
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
z : A
hz : ¬z ∈ M
m_eq : M = M + span A {z}
⊢ z ∈ M + span A {z}
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
z : A
hz : ¬z ∈ M
m_eq : M = M + span A {z}
⊢ z ∈ M
rw [m_eq]
no goals
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
z : A
hz : ¬z ∈ M
m_eq : M = M + span A {z}
⊢ z ∈ M + span A {z}
exact mem_sup_right (mem_span_singleton_self z)
case neg.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne✝ : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span A {y}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
⊢ M * (M + span A {y}) + span A {x} * (M + span A {y}) ≤ M
case neg.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne✝ : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span A {y}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
⊢ (M + span A {x}) * (M + span A {y}) ≤ M
rw [add_mul]
case neg.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne✝ : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span A {y}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
⊢ span A {x} * (M + span A {y}) ≤ M
case neg.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne✝ : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span A {y}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
⊢ M * (M + span A {y}) + span A {x} * (M + span A {y}) ≤ M
apply sup_le (show M * (M + span A {y}) ≤ M from Ideal.mul_le_right)
case neg.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne✝ : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span A {y}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
⊢ span A {x} * M + span A {x} * span A {y} ≤ M
case neg.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne✝ : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span A {y}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
⊢ span A {x} * (M + span A {y}) ≤ M
rw [mul_add]
case neg.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne✝ : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span A {y}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
⊢ span A {x} * span A {y} ≤ M
case neg.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne✝ : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span A {y}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
⊢ span A {x} * M + span A {x} * span A {y} ≤ M
apply sup_le (show span A {x} * M ≤ M from Ideal.mul_le_left)
no goals
case neg.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne✝ : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span A {y}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
⊢ span A {x} * span A {y} ≤ M
rwa [span_mul_span, Set.singleton_mul_singleton, span_singleton_le_iff_mem]
no goals
case neg.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
I M : Ideal A
hgt :
  ∀ (J : Submodule A A),
    J > M →
      (fun I => I ≠ ⊥ → ∃ Z, Multiset.prod (Multiset.map asIdeal Z) ≤ I ∧ Multiset.prod (Multiset.map asIdeal Z) ≠ ⊥) J
h_nzM : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬Ideal.IsPrime M
x : A
hx : ¬x ∈ M
y : A
hy : ¬y ∈ M
h_xy : x * y ∈ M
lt_add : ∀ (z : A), ¬z ∈ M → M < M + span A {z}
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : Multiset.prod (Multiset.map asIdeal Wx) ≤ M + span A {x}
h_Wx_ne✝ : Multiset.prod (Multiset.map asIdeal Wx) ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : Multiset.prod (Multiset.map asIdeal Wy) ≤ M + span A {y}
h_Wx_ne : Multiset.prod (Multiset.map asIdeal Wy) ≠ ⊥
⊢ ¬(Multiset.prod (Multiset.map asIdeal Wx) = ⊥ ∨ Multiset.prod (Multiset.map asIdeal Wy) = ⊥)
rintro (hx | hy) <;> contradiction