α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a b : α
M M' : Ideal α
hM : IsMaximal M
hM' : IsMaximal M'
h : M ⊔ M' ≠ ⊤
⊢ M = M'
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a b : α
M M' : Ideal α
hM : IsMaximal M
hM' : IsMaximal M'
hne : M ≠ M'
⊢ M ⊔ M' = ⊤
contrapose! hne with h
no goals
α : Type u
β : Type v
inst✝ : Semiring α
I : Ideal α
a b : α
M M' : Ideal α
hM : IsMaximal M
hM' : IsMaximal M'
h : M ⊔ M' ≠ ⊤
⊢ M = M'
exact hM.eq_of_le hM'.ne_top (le_sup_left.trans_eq (hM'.eq_of_le h le_sup_right).symm)