case mk.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
⊢ ∃ n, I = maximalIdeal R ^ n
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
h' : Submodule.IsPrincipal (maximalIdeal R)
I : Ideal R
hI : I ≠ ⊥
⊢ ∃ n, I = maximalIdeal R ^ n
obtain ⟨x, hx : _ = Ideal.span _⟩ := h'
case pos
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : I = ⊤
⊢ ∃ n, I = maximalIdeal R ^ n

case neg
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
⊢ ∃ n, I = maximalIdeal R ^ n
case mk.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
⊢ ∃ n, I = maximalIdeal R ^ n
by_cases hI' : I = ⊤
case neg
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
⊢ ∃ n, I = maximalIdeal R ^ n
case neg
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
⊢ ∃ n, I = maximalIdeal R ^ n
have H : ∀ r : R, ¬IsUnit r ↔ x ∣ r := fun r =>
  (SetLike.ext_iff.mp hx r).trans Ideal.mem_span_singleton
case neg
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this : x ≠ 0
⊢ ∃ n, I = maximalIdeal R ^ n
case neg
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
⊢ ∃ n, I = maximalIdeal R ^ n
have : x ≠ 0 := by
  rintro rfl
  apply Ring.ne_bot_of_isMaximal_of_not_isField (maximalIdeal.isMaximal R) h
  simp [hx]
case neg
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this : x ≠ 0
hx' : Irreducible x
⊢ ∃ n, I = maximalIdeal R ^ n
case neg
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this : x ≠ 0
⊢ ∃ n, I = maximalIdeal R ^ n
have hx' := DiscreteValuationRing.irreducible_of_span_eq_maximalIdeal x this hx
case neg
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
⊢ ∃ n, I = maximalIdeal R ^ n
case neg
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
⊢ ∃ n, I = maximalIdeal R ^ n
have : ∃ n : ℕ, x ^ n ∈ I := by
  obtain ⟨r, hr₁, hr₂⟩ : ∃ r : R, r ∈ I ∧ r ≠ 0 := by
    by_contra' h; apply hI; rw [eq_bot_iff]; exact h
  obtain ⟨n, u, rfl⟩ := H' r hr₂ (le_maximalIdeal hI' hr₁)
  use n
  rwa [← I.unit_mul_mem_iff_mem u.isUnit, mul_comm]
case neg
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
⊢ I = maximalIdeal R ^ Nat.find this
case neg
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
⊢ ∃ n, I = maximalIdeal R ^ n
use Nat.find this
case neg.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
⊢ I ≤ maximalIdeal R ^ Nat.find this

case neg.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
⊢ maximalIdeal R ^ Nat.find this ≤ I
case neg
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
⊢ I = maximalIdeal R ^ Nat.find this
apply le_antisymm
case pos
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : I = ⊤
⊢ I = maximalIdeal R ^ 0
case pos
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : I = ⊤
⊢ ∃ n, I = maximalIdeal R ^ n
use 0
no goals
case pos
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : I = ⊤
⊢ I = maximalIdeal R ^ 0
rw [pow_zero, hI', Ideal.one_eq_top]
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
hI' : ¬I = ⊤
hx : maximalIdeal R = Ideal.span {0}
H : ∀ (r : R), ¬IsUnit r ↔ 0 ∣ r
⊢ False
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
⊢ x ≠ 0
rintro rfl
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
hI' : ¬I = ⊤
hx : maximalIdeal R = Ideal.span {0}
H : ∀ (r : R), ¬IsUnit r ↔ 0 ∣ r
⊢ maximalIdeal R = ⊥
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
hI' : ¬I = ⊤
hx : maximalIdeal R = Ideal.span {0}
H : ∀ (r : R), ¬IsUnit r ↔ 0 ∣ r
⊢ False
apply Ring.ne_bot_of_isMaximal_of_not_isField (maximalIdeal.isMaximal R) h
no goals
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
hI' : ¬I = ⊤
hx : maximalIdeal R = Ideal.span {0}
H : ∀ (r : R), ¬IsUnit r ↔ 0 ∣ r
⊢ maximalIdeal R = ⊥
simp [hx]
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this : x ≠ 0
hx' : Irreducible x
r : R
hr₁ : r ≠ 0
hr₂ : r ∈ nonunits R
⊢ ∃ n, Associated (x ^ n) r
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this : x ≠ 0
hx' : Irreducible x
⊢ ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
intro r hr₁ hr₂
case intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this : x ≠ 0
hx' : Irreducible x
f : Multiset R
hf₁ : ∀ (b : R), b ∈ f → Irreducible b
hf₂ : f ≠ ∅
hr₁ : Multiset.prod f ≠ 0
hr₂ : Multiset.prod f ∈ nonunits R
⊢ ∃ n, Associated (x ^ n) (Multiset.prod f)
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this : x ≠ 0
hx' : Irreducible x
r : R
hr₁ : r ≠ 0
hr₂ : r ∈ nonunits R
⊢ ∃ n, Associated (x ^ n) r
obtain ⟨f, hf₁, rfl, hf₂⟩ := (WfDvdMonoid.not_unit_iff_exists_factors_eq r hr₁).mp hr₂
case intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
f : Multiset R
hf₁ : ∀ (b : R), b ∈ f → Irreducible b
hf₂ : f ≠ ∅
hr₁ : Multiset.prod f ≠ 0
hr₂ : Multiset.prod f ∈ nonunits R
this : ∀ (b : R), b ∈ f → Associated x b
⊢ ∃ n, Associated (x ^ n) (Multiset.prod f)
case intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this : x ≠ 0
hx' : Irreducible x
f : Multiset R
hf₁ : ∀ (b : R), b ∈ f → Irreducible b
hf₂ : f ≠ ∅
hr₁ : Multiset.prod f ≠ 0
hr₂ : Multiset.prod f ∈ nonunits R
⊢ ∃ n, Associated (x ^ n) (Multiset.prod f)
have : ∀ b ∈ f, Associated x b := by
  intro b hb
  exact Irreducible.associated_of_dvd hx' (hf₁ b hb) ((H b).mp (hf₁ b hb).1)
case intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
f : Multiset R
hf₂ : f ≠ ∅
this : ∀ (b : R), b ∈ f → Associated x b
⊢ ∃ n, Associated (x ^ n) (Multiset.prod f)
case intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
f : Multiset R
hf₁ : ∀ (b : R), b ∈ f → Irreducible b
hf₂ : f ≠ ∅
hr₁ : Multiset.prod f ≠ 0
hr₂ : Multiset.prod f ∈ nonunits R
this : ∀ (b : R), b ∈ f → Associated x b
⊢ ∃ n, Associated (x ^ n) (Multiset.prod f)
clear hr₁ hr₂ hf₁
case intro.intro.intro.empty
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝¹ : x ≠ 0
hx' : Irreducible x
f : Multiset R
hf₂✝ : f ≠ ∅
this✝ : ∀ (b : R), b ∈ f → Associated x b
hf₂ : 0 ≠ ∅
this : ∀ (b : R), b ∈ 0 → Associated x b
⊢ ∃ n, Associated (x ^ n) (Multiset.prod 0)

case intro.intro.intro.cons
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝¹ : x ≠ 0
hx' : Irreducible x
f : Multiset R
hf₂✝ : f ≠ ∅
this✝ : ∀ (b : R), b ∈ f → Associated x b
fa : R
fs : Multiset R
fh : fs ≠ ∅ → (∀ (b : R), b ∈ fs → Associated x b) → ∃ n, Associated (x ^ n) (Multiset.prod fs)
hf₂ : fa ::ₘ fs ≠ ∅
this : ∀ (b : R), b ∈ fa ::ₘ fs → Associated x b
⊢ ∃ n, Associated (x ^ n) (Multiset.prod (fa ::ₘ fs))
case intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
f : Multiset R
hf₂ : f ≠ ∅
this : ∀ (b : R), b ∈ f → Associated x b
⊢ ∃ n, Associated (x ^ n) (Multiset.prod f)
induction' f using Multiset.induction with fa fs fh
case intro.intro.intro.cons.inl
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝¹ : x ≠ 0
hx' : Irreducible x
f : Multiset R
hf₂✝ : f ≠ ∅
this✝ : ∀ (b : R), b ∈ f → Associated x b
fa : R
fh : ∅ ≠ ∅ → (∀ (b : R), b ∈ ∅ → Associated x b) → ∃ n, Associated (x ^ n) (Multiset.prod ∅)
hf₂ : fa ::ₘ ∅ ≠ ∅
this : ∀ (b : R), b ∈ fa ::ₘ ∅ → Associated x b
⊢ ∃ n, Associated (x ^ n) (Multiset.prod (fa ::ₘ ∅))

case intro.intro.intro.cons.inr
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝¹ : x ≠ 0
hx' : Irreducible x
f : Multiset R
hf₂✝ : f ≠ ∅
this✝ : ∀ (b : R), b ∈ f → Associated x b
fa : R
fs : Multiset R
fh : fs ≠ ∅ → (∀ (b : R), b ∈ fs → Associated x b) → ∃ n, Associated (x ^ n) (Multiset.prod fs)
hf₂ : fa ::ₘ fs ≠ ∅
this : ∀ (b : R), b ∈ fa ::ₘ fs → Associated x b
hf' : fs ≠ ∅
⊢ ∃ n, Associated (x ^ n) (Multiset.prod (fa ::ₘ fs))
case intro.intro.intro.cons
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝¹ : x ≠ 0
hx' : Irreducible x
f : Multiset R
hf₂✝ : f ≠ ∅
this✝ : ∀ (b : R), b ∈ f → Associated x b
fa : R
fs : Multiset R
fh : fs ≠ ∅ → (∀ (b : R), b ∈ fs → Associated x b) → ∃ n, Associated (x ^ n) (Multiset.prod fs)
hf₂ : fa ::ₘ fs ≠ ∅
this : ∀ (b : R), b ∈ fa ::ₘ fs → Associated x b
⊢ ∃ n, Associated (x ^ n) (Multiset.prod (fa ::ₘ fs))
rcases eq_or_ne fs ∅ with (rfl | hf')
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this : x ≠ 0
hx' : Irreducible x
f : Multiset R
hf₁ : ∀ (b : R), b ∈ f → Irreducible b
hf₂ : f ≠ ∅
hr₁ : Multiset.prod f ≠ 0
hr₂ : Multiset.prod f ∈ nonunits R
b : R
hb : b ∈ f
⊢ Associated x b
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this : x ≠ 0
hx' : Irreducible x
f : Multiset R
hf₁ : ∀ (b : R), b ∈ f → Irreducible b
hf₂ : f ≠ ∅
hr₁ : Multiset.prod f ≠ 0
hr₂ : Multiset.prod f ∈ nonunits R
⊢ ∀ (b : R), b ∈ f → Associated x b
intro b hb
no goals
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this : x ≠ 0
hx' : Irreducible x
f : Multiset R
hf₁ : ∀ (b : R), b ∈ f → Irreducible b
hf₂ : f ≠ ∅
hr₁ : Multiset.prod f ≠ 0
hr₂ : Multiset.prod f ∈ nonunits R
b : R
hb : b ∈ f
⊢ Associated x b
exact Irreducible.associated_of_dvd hx' (hf₁ b hb) ((H b).mp (hf₁ b hb).1)
no goals
case intro.intro.intro.empty
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝¹ : x ≠ 0
hx' : Irreducible x
f : Multiset R
hf₂✝ : f ≠ ∅
this✝ : ∀ (b : R), b ∈ f → Associated x b
hf₂ : 0 ≠ ∅
this : ∀ (b : R), b ∈ 0 → Associated x b
⊢ ∃ n, Associated (x ^ n) (Multiset.prod 0)
exact (hf₂ rfl).elim
case intro.intro.intro.cons.inl
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝¹ : x ≠ 0
hx' : Irreducible x
f : Multiset R
hf₂✝ : f ≠ ∅
this✝ : ∀ (b : R), b ∈ f → Associated x b
fa : R
fh : ∅ ≠ ∅ → (∀ (b : R), b ∈ ∅ → Associated x b) → ∃ n, Associated (x ^ n) (Multiset.prod ∅)
hf₂ : fa ::ₘ ∅ ≠ ∅
this : ∀ (b : R), b ∈ fa ::ₘ ∅ → Associated x b
⊢ Associated (x ^ 1) (Multiset.prod (fa ::ₘ ∅))
case intro.intro.intro.cons.inl
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝¹ : x ≠ 0
hx' : Irreducible x
f : Multiset R
hf₂✝ : f ≠ ∅
this✝ : ∀ (b : R), b ∈ f → Associated x b
fa : R
fh : ∅ ≠ ∅ → (∀ (b : R), b ∈ ∅ → Associated x b) → ∃ n, Associated (x ^ n) (Multiset.prod ∅)
hf₂ : fa ::ₘ ∅ ≠ ∅
this : ∀ (b : R), b ∈ fa ::ₘ ∅ → Associated x b
⊢ ∃ n, Associated (x ^ n) (Multiset.prod (fa ::ₘ ∅))
use 1
case intro.intro.intro.cons.inl
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝¹ : x ≠ 0
hx' : Irreducible x
f : Multiset R
hf₂✝ : f ≠ ∅
this✝ : ∀ (b : R), b ∈ f → Associated x b
fa : R
fh : ∅ ≠ ∅ → (∀ (b : R), b ∈ ∅ → Associated x b) → ∃ n, Associated (x ^ n) (Multiset.prod ∅)
hf₂ : fa ::ₘ ∅ ≠ ∅
this : ∀ (b : R), b ∈ fa ::ₘ ∅ → Associated x b
⊢ Associated x fa
case intro.intro.intro.cons.inl
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝¹ : x ≠ 0
hx' : Irreducible x
f : Multiset R
hf₂✝ : f ≠ ∅
this✝ : ∀ (b : R), b ∈ f → Associated x b
fa : R
fh : ∅ ≠ ∅ → (∀ (b : R), b ∈ ∅ → Associated x b) → ∃ n, Associated (x ^ n) (Multiset.prod ∅)
hf₂ : fa ::ₘ ∅ ≠ ∅
this : ∀ (b : R), b ∈ fa ::ₘ ∅ → Associated x b
⊢ Associated (x ^ 1) (Multiset.prod (fa ::ₘ ∅))
rw [pow_one, Multiset.prod_cons, Multiset.empty_eq_zero, Multiset.prod_zero, mul_one]
no goals
case intro.intro.intro.cons.inl
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝¹ : x ≠ 0
hx' : Irreducible x
f : Multiset R
hf₂✝ : f ≠ ∅
this✝ : ∀ (b : R), b ∈ f → Associated x b
fa : R
fh : ∅ ≠ ∅ → (∀ (b : R), b ∈ ∅ → Associated x b) → ∃ n, Associated (x ^ n) (Multiset.prod ∅)
hf₂ : fa ::ₘ ∅ ≠ ∅
this : ∀ (b : R), b ∈ fa ::ₘ ∅ → Associated x b
⊢ Associated x fa
exact this _ (Multiset.mem_cons_self _ _)
case intro.intro.intro.cons.inr.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝¹ : x ≠ 0
hx' : Irreducible x
f : Multiset R
hf₂✝ : f ≠ ∅
this✝ : ∀ (b : R), b ∈ f → Associated x b
fa : R
fs : Multiset R
fh : fs ≠ ∅ → (∀ (b : R), b ∈ fs → Associated x b) → ∃ n, Associated (x ^ n) (Multiset.prod fs)
hf₂ : fa ::ₘ fs ≠ ∅
this : ∀ (b : R), b ∈ fa ::ₘ fs → Associated x b
hf' : fs ≠ ∅
n : ℕ
hn : Associated (x ^ n) (Multiset.prod fs)
⊢ ∃ n, Associated (x ^ n) (Multiset.prod (fa ::ₘ fs))
case intro.intro.intro.cons.inr
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝¹ : x ≠ 0
hx' : Irreducible x
f : Multiset R
hf₂✝ : f ≠ ∅
this✝ : ∀ (b : R), b ∈ f → Associated x b
fa : R
fs : Multiset R
fh : fs ≠ ∅ → (∀ (b : R), b ∈ fs → Associated x b) → ∃ n, Associated (x ^ n) (Multiset.prod fs)
hf₂ : fa ::ₘ fs ≠ ∅
this : ∀ (b : R), b ∈ fa ::ₘ fs → Associated x b
hf' : fs ≠ ∅
⊢ ∃ n, Associated (x ^ n) (Multiset.prod (fa ::ₘ fs))
obtain ⟨n, hn⟩ := fh hf' fun b hb => this _ (Multiset.mem_cons_of_mem hb)
case intro.intro.intro.cons.inr.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝¹ : x ≠ 0
hx' : Irreducible x
f : Multiset R
hf₂✝ : f ≠ ∅
this✝ : ∀ (b : R), b ∈ f → Associated x b
fa : R
fs : Multiset R
fh : fs ≠ ∅ → (∀ (b : R), b ∈ fs → Associated x b) → ∃ n, Associated (x ^ n) (Multiset.prod fs)
hf₂ : fa ::ₘ fs ≠ ∅
this : ∀ (b : R), b ∈ fa ::ₘ fs → Associated x b
hf' : fs ≠ ∅
n : ℕ
hn : Associated (x ^ n) (Multiset.prod fs)
⊢ Associated (x ^ (n + 1)) (Multiset.prod (fa ::ₘ fs))
case intro.intro.intro.cons.inr.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝¹ : x ≠ 0
hx' : Irreducible x
f : Multiset R
hf₂✝ : f ≠ ∅
this✝ : ∀ (b : R), b ∈ f → Associated x b
fa : R
fs : Multiset R
fh : fs ≠ ∅ → (∀ (b : R), b ∈ fs → Associated x b) → ∃ n, Associated (x ^ n) (Multiset.prod fs)
hf₂ : fa ::ₘ fs ≠ ∅
this : ∀ (b : R), b ∈ fa ::ₘ fs → Associated x b
hf' : fs ≠ ∅
n : ℕ
hn : Associated (x ^ n) (Multiset.prod fs)
⊢ ∃ n, Associated (x ^ n) (Multiset.prod (fa ::ₘ fs))
use n + 1
case intro.intro.intro.cons.inr.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝¹ : x ≠ 0
hx' : Irreducible x
f : Multiset R
hf₂✝ : f ≠ ∅
this✝ : ∀ (b : R), b ∈ f → Associated x b
fa : R
fs : Multiset R
fh : fs ≠ ∅ → (∀ (b : R), b ∈ fs → Associated x b) → ∃ n, Associated (x ^ n) (Multiset.prod fs)
hf₂ : fa ::ₘ fs ≠ ∅
this : ∀ (b : R), b ∈ fa ::ₘ fs → Associated x b
hf' : fs ≠ ∅
n : ℕ
hn : Associated (x ^ n) (Multiset.prod fs)
⊢ Associated (x * x ^ n) (fa * Multiset.prod fs)
case intro.intro.intro.cons.inr.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝¹ : x ≠ 0
hx' : Irreducible x
f : Multiset R
hf₂✝ : f ≠ ∅
this✝ : ∀ (b : R), b ∈ f → Associated x b
fa : R
fs : Multiset R
fh : fs ≠ ∅ → (∀ (b : R), b ∈ fs → Associated x b) → ∃ n, Associated (x ^ n) (Multiset.prod fs)
hf₂ : fa ::ₘ fs ≠ ∅
this : ∀ (b : R), b ∈ fa ::ₘ fs → Associated x b
hf' : fs ≠ ∅
n : ℕ
hn : Associated (x ^ n) (Multiset.prod fs)
⊢ Associated (x ^ (n + 1)) (Multiset.prod (fa ::ₘ fs))
rw [pow_add, Multiset.prod_cons, mul_comm, pow_one]
no goals
case intro.intro.intro.cons.inr.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝¹ : x ≠ 0
hx' : Irreducible x
f : Multiset R
hf₂✝ : f ≠ ∅
this✝ : ∀ (b : R), b ∈ f → Associated x b
fa : R
fs : Multiset R
fh : fs ≠ ∅ → (∀ (b : R), b ∈ fs → Associated x b) → ∃ n, Associated (x ^ n) (Multiset.prod fs)
hf₂ : fa ::ₘ fs ≠ ∅
this : ∀ (b : R), b ∈ fa ::ₘ fs → Associated x b
hf' : fs ≠ ∅
n : ℕ
hn : Associated (x ^ n) (Multiset.prod fs)
⊢ Associated (x * x ^ n) (fa * Multiset.prod fs)
exact Associated.mul_mul (this _ (Multiset.mem_cons_self _ _)) hn
case intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
r : R
hr₁ : r ∈ I
hr₂ : r ≠ 0
⊢ ∃ n, x ^ n ∈ I
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
⊢ ∃ n, x ^ n ∈ I
obtain ⟨r, hr₁, hr₂⟩ : ∃ r : R, r ∈ I ∧ r ≠ 0 := by
  by_contra' h; apply hI; rw [eq_bot_iff]; exact h
case intro.intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
n : ℕ
u : Rˣ
hr₁ : x ^ n * ↑u ∈ I
hr₂ : x ^ n * ↑u ≠ 0
⊢ ∃ n, x ^ n ∈ I
case intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
r : R
hr₁ : r ∈ I
hr₂ : r ≠ 0
⊢ ∃ n, x ^ n ∈ I
obtain ⟨n, u, rfl⟩ := H' r hr₂ (le_maximalIdeal hI' hr₁)
case intro.intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
n : ℕ
u : Rˣ
hr₁ : x ^ n * ↑u ∈ I
hr₂ : x ^ n * ↑u ≠ 0
⊢ x ^ n ∈ I
case intro.intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
n : ℕ
u : Rˣ
hr₁ : x ^ n * ↑u ∈ I
hr₂ : x ^ n * ↑u ≠ 0
⊢ ∃ n, x ^ n ∈ I
use n
no goals
case intro.intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
n : ℕ
u : Rˣ
hr₁ : x ^ n * ↑u ∈ I
hr₂ : x ^ n * ↑u ≠ 0
⊢ x ^ n ∈ I
rwa [← I.unit_mul_mem_iff_mem u.isUnit, mul_comm]
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h✝ : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
h : ∀ (r : R), r ∈ I → r = 0
⊢ False
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
⊢ ∃ r, r ∈ I ∧ r ≠ 0
by_contra' h
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h✝ : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
h : ∀ (r : R), r ∈ I → r = 0
⊢ I = ⊥
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h✝ : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
h : ∀ (r : R), r ∈ I → r = 0
⊢ False
apply hI
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h✝ : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
h : ∀ (r : R), r ∈ I → r = 0
⊢ I ≤ ⊥
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h✝ : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
h : ∀ (r : R), r ∈ I → r = 0
⊢ I = ⊥
rw [eq_bot_iff]
no goals
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h✝ : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
h : ∀ (r : R), r ∈ I → r = 0
⊢ I ≤ ⊥
exact h
case neg.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
⊢ ∀ (s : R), s ∈ I → s ∈ maximalIdeal R ^ Nat.find this
case neg.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
⊢ I ≤ maximalIdeal R ^ Nat.find this
change ∀ s ∈ I, s ∈ _
case neg.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
hI'' : ¬∀ (s : R), s ∈ I → s ∈ maximalIdeal R ^ Nat.find this
⊢ False
case neg.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
⊢ ∀ (s : R), s ∈ I → s ∈ maximalIdeal R ^ Nat.find this
by_contra hI''
case neg.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
hI'' : ∃ s, s ∈ I ∧ ¬s ∈ maximalIdeal R ^ Nat.find this
⊢ False
case neg.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
hI'' : ¬∀ (s : R), s ∈ I → s ∈ maximalIdeal R ^ Nat.find this
⊢ False
push_neg at hI''
case neg.a.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
s : R
hs₁ : s ∈ I
hs₂ : ¬s ∈ maximalIdeal R ^ Nat.find this
⊢ False
case neg.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
hI'' : ∃ s, s ∈ I ∧ ¬s ∈ maximalIdeal R ^ Nat.find this
⊢ False
obtain ⟨s, hs₁, hs₂⟩ := hI''
case neg.a.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
s : R
hs₁ : s ∈ I
hs₂ : ¬s ∈ maximalIdeal R ^ Nat.find this
⊢ s ∈ maximalIdeal R ^ Nat.find this
case neg.a.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
s : R
hs₁ : s ∈ I
hs₂ : ¬s ∈ maximalIdeal R ^ Nat.find this
⊢ False
apply hs₂
case pos
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
s : R
hs₁ : s ∈ I
hs₂ : ¬s ∈ maximalIdeal R ^ Nat.find this
hs₃ : s = 0
⊢ s ∈ maximalIdeal R ^ Nat.find this

case neg
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
s : R
hs₁ : s ∈ I
hs₂ : ¬s ∈ maximalIdeal R ^ Nat.find this
hs₃ : ¬s = 0
⊢ s ∈ maximalIdeal R ^ Nat.find this
case neg.a.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
s : R
hs₁ : s ∈ I
hs₂ : ¬s ∈ maximalIdeal R ^ Nat.find this
⊢ s ∈ maximalIdeal R ^ Nat.find this
by_cases hs₃ : s = 0
case neg.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
n : ℕ
u : Rˣ
hs₁ : x ^ n * ↑u ∈ I
hs₂ : ¬x ^ n * ↑u ∈ maximalIdeal R ^ Nat.find this
hs₃ : ¬x ^ n * ↑u = 0
⊢ x ^ n * ↑u ∈ maximalIdeal R ^ Nat.find this
case neg
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
s : R
hs₁ : s ∈ I
hs₂ : ¬s ∈ maximalIdeal R ^ Nat.find this
hs₃ : ¬s = 0
⊢ s ∈ maximalIdeal R ^ Nat.find this
obtain ⟨n, u, rfl⟩ := H' s hs₃ (le_maximalIdeal hI' hs₁)
case neg.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
n : ℕ
u : Rˣ
hs₁ : x ^ n ∈ I
hs₂ : ¬x ^ n * ↑u ∈ maximalIdeal R ^ Nat.find this
hs₃ : ¬x ^ n * ↑u = 0
⊢ x ^ n ∈ maximalIdeal R ^ Nat.find this
case neg.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
n : ℕ
u : Rˣ
hs₁ : x ^ n * ↑u ∈ I
hs₂ : ¬x ^ n * ↑u ∈ maximalIdeal R ^ Nat.find this
hs₃ : ¬x ^ n * ↑u = 0
⊢ x ^ n * ↑u ∈ maximalIdeal R ^ Nat.find this
rw [mul_comm, Ideal.unit_mul_mem_iff_mem _ u.isUnit] at hs₁ ⊢
case neg.intro.intro.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
n : ℕ
u : Rˣ
hs₁ : x ^ n ∈ I
hs₂ : ¬x ^ n * ↑u ∈ maximalIdeal R ^ Nat.find this
hs₃ : ¬x ^ n * ↑u = 0
⊢ x ^ n ∈ maximalIdeal R ^ n
case neg.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
n : ℕ
u : Rˣ
hs₁ : x ^ n ∈ I
hs₂ : ¬x ^ n * ↑u ∈ maximalIdeal R ^ Nat.find this
hs₃ : ¬x ^ n * ↑u = 0
⊢ x ^ n ∈ maximalIdeal R ^ Nat.find this
apply Ideal.pow_le_pow (Nat.find_min' this hs₁)
case neg.intro.intro.a.hx
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
n : ℕ
u : Rˣ
hs₁ : x ^ n ∈ I
hs₂ : ¬x ^ n * ↑u ∈ maximalIdeal R ^ Nat.find this
hs₃ : ¬x ^ n * ↑u = 0
⊢ x ∈ maximalIdeal R
case neg.intro.intro.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
n : ℕ
u : Rˣ
hs₁ : x ^ n ∈ I
hs₂ : ¬x ^ n * ↑u ∈ maximalIdeal R ^ Nat.find this
hs₃ : ¬x ^ n * ↑u = 0
⊢ x ^ n ∈ maximalIdeal R ^ n
apply Ideal.pow_mem_pow
no goals
case neg.intro.intro.a.hx
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
n : ℕ
u : Rˣ
hs₁ : x ^ n ∈ I
hs₂ : ¬x ^ n * ↑u ∈ maximalIdeal R ^ Nat.find this
hs₃ : ¬x ^ n * ↑u = 0
⊢ x ∈ maximalIdeal R
exact (H _).mpr (dvd_refl _)
case pos
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
s : R
hs₁ : s ∈ I
hs₂ : ¬s ∈ maximalIdeal R ^ Nat.find this
hs₃ : s = 0
⊢ 0 ∈ maximalIdeal R ^ Nat.find this
case pos
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
s : R
hs₁ : s ∈ I
hs₂ : ¬s ∈ maximalIdeal R ^ Nat.find this
hs₃ : s = 0
⊢ s ∈ maximalIdeal R ^ Nat.find this
rw [hs₃]
no goals
case pos
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
s : R
hs₁ : s ∈ I
hs₂ : ¬s ∈ maximalIdeal R ^ Nat.find this
hs₃ : s = 0
⊢ 0 ∈ maximalIdeal R ^ Nat.find this
exact zero_mem _
case neg.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
⊢ x ^ Nat.find this ∈ ↑I
case neg.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
⊢ maximalIdeal R ^ Nat.find this ≤ I
rw [hx, Ideal.span_singleton_pow, Ideal.span_le, Set.singleton_subset_iff]
no goals
case neg.a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.321
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsNoetherianRing R
inst✝¹ : LocalRing R
inst✝ : IsDomain R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
x : R
hx : maximalIdeal R = Ideal.span {x}
hI' : ¬I = ⊤
H : ∀ (r : R), ¬IsUnit r ↔ x ∣ r
this✝ : x ≠ 0
hx' : Irreducible x
H' : ∀ (r : R), r ≠ 0 → r ∈ nonunits R → ∃ n, Associated (x ^ n) r
this : ∃ n, x ^ n ∈ I
⊢ x ^ Nat.find this ∈ ↑I
exact Nat.find_spec this