case intro.intro
α : Type u_1
β : Type ?u.23015
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
a b : α
h : a ≠ b
⊢ ⊥ ≠ ⊤
α : Type u_1
β : Type ?u.23015
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ ⊥ ≠ ⊤
obtain ⟨a, b, h⟩ := exists_pair_ne α
no goals
case intro.intro
α : Type u_1
β : Type ?u.23015
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
a b : α
h : a ≠ b
⊢ ⊥ ≠ ⊤
rcases eq_bot_or_eq_top a with (rfl | rfl) <;> rcases eq_bot_or_eq_top b with (rfl | rfl) <;>
  first |simpa|simpa using h.symm
no goals
case intro.intro.inr.inr
α : Type u_1
β : Type ?u.23015
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊤ ≠ ⊤
⊢ ⊥ ≠ ⊤
simpa
no goals
case intro.intro.inr.inr
α : Type u_1
β : Type ?u.23015
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊤ ≠ ⊤
⊢ ⊥ ≠ ⊤
simpa using h.symm