α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
this : Ideal.span {a} ≠ ⊤
⊢ ∃ I, Ideal.IsMaximal I ∧ a ∈ I
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
⊢ ∃ I, Ideal.IsMaximal I ∧ a ∈ I
have : Ideal.span ({a} : Set α) ≠ ⊤ := by
  intro H
  rw [Ideal.span_singleton_eq_top] at H
  contradiction
case intro.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
this : Ideal.span {a} ≠ ⊤
I : Ideal α
Imax : Ideal.IsMaximal I
H : Ideal.span {a} ≤ I
⊢ ∃ I, Ideal.IsMaximal I ∧ a ∈ I
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
this : Ideal.span {a} ≠ ⊤
⊢ ∃ I, Ideal.IsMaximal I ∧ a ∈ I
rcases Ideal.exists_le_maximal _ this with ⟨I, Imax, H⟩
case intro.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
this : Ideal.span {a} ≠ ⊤
I : Ideal α
Imax : Ideal.IsMaximal I
H : Ideal.span {a} ≤ I
⊢ a ∈ I
case intro.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
this : Ideal.span {a} ≠ ⊤
I : Ideal α
Imax : Ideal.IsMaximal I
H : Ideal.span {a} ≤ I
⊢ ∃ I, Ideal.IsMaximal I ∧ a ∈ I
use I, Imax
case intro.intro.a
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
this : Ideal.span {a} ≠ ⊤
I : Ideal α
Imax : Ideal.IsMaximal I
H : Ideal.span {a} ≤ I
⊢ a ∈ Ideal.span {a}
case intro.intro
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
this : Ideal.span {a} ≠ ⊤
I : Ideal α
Imax : Ideal.IsMaximal I
H : Ideal.span {a} ≤ I
⊢ a ∈ I
apply H
case intro.intro.a.a
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
this : Ideal.span {a} ≠ ⊤
I : Ideal α
Imax : Ideal.IsMaximal I
H : Ideal.span {a} ≤ I
⊢ a ∈ {a}
case intro.intro.a
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
this : Ideal.span {a} ≠ ⊤
I : Ideal α
Imax : Ideal.IsMaximal I
H : Ideal.span {a} ≤ I
⊢ a ∈ Ideal.span {a}
apply Ideal.subset_span
no goals
case intro.intro.a.a
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
this : Ideal.span {a} ≠ ⊤
I : Ideal α
Imax : Ideal.IsMaximal I
H : Ideal.span {a} ≤ I
⊢ a ∈ {a}
exact Set.mem_singleton a
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
H : Ideal.span {a} = ⊤
⊢ False
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
⊢ Ideal.span {a} ≠ ⊤
intro H
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
H : IsUnit a
⊢ False
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
H : Ideal.span {a} = ⊤
⊢ False
rw [Ideal.span_singleton_eq_top] at H
no goals
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
H : IsUnit a
⊢ False
contradiction