α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
⊢ ¬I = ⊤ → I = ⊥
α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
⊢ I = ⊥ ∨ I = ⊤
rw [or_iff_not_imp_right]
α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
⊢ I ≠ ⊤ → I = ⊥
α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
⊢ ¬I = ⊤ → I = ⊥
change _ ≠ _ → _
α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
⊢ ¬1 ∈ I → I = ⊥
α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
⊢ I ≠ ⊤ → I = ⊥
rw [Ideal.ne_top_iff_one]
α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : ¬1 ∈ I
⊢ I = ⊥
α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
⊢ ¬1 ∈ I → I = ⊥
intro h1
α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : ¬1 ∈ I
⊢ I ≤ ⊥
α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : ¬1 ∈ I
⊢ I = ⊥
rw [eq_bot_iff]
α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : ¬1 ∈ I
r : K
hr : r ∈ I
⊢ r ∈ ⊥
α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : ¬1 ∈ I
⊢ I ≤ ⊥
intro r hr
case pos
α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : ¬1 ∈ I
r : K
hr : r ∈ I
H : r = 0
⊢ r ∈ ⊥

case neg
α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : ¬1 ∈ I
r : K
hr : r ∈ I
H : ¬r = 0
⊢ r ∈ ⊥
α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : ¬1 ∈ I
r : K
hr : r ∈ I
⊢ r ∈ ⊥
by_cases H : r = 0
no goals
case neg
α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : ¬1 ∈ I
r : K
hr : r ∈ I
H : ¬r = 0
⊢ r ∈ ⊥
simpa [H, h1] using I.mul_mem_left r⁻¹ hr
no goals
case pos
α : Type u
β : Type v
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : ¬1 ∈ I
r : K
hr : r ∈ I
H : r = 0
⊢ r ∈ ⊥
simpa