case none
α : Type u_1
β : Type ?u.91154
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
l : List α
a m : α
ha : a ∈ l
h : maximum l = none
⊢ ¬none < ↑a

case some
α : Type u_1
β : Type ?u.91154
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
l : List α
a m : α
ha : a ∈ l
val✝ : α
h : maximum l = some val✝
⊢ ¬some val✝ < ↑a
α : Type u_1
β : Type ?u.91154
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
l : List α
a m : α
ha : a ∈ l
⊢ ¬maximum l < ↑a
cases h : l.maximum
no goals
case none
α : Type u_1
β : Type ?u.91154
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
l : List α
a m : α
ha : a ∈ l
h : maximum l = none
⊢ ¬none < ↑a
simp_all
no goals
case some
α : Type u_1
β : Type ?u.91154
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
l : List α
a m : α
ha : a ∈ l
val✝ : α
h : maximum l = some val✝
⊢ ¬some val✝ < ↑a
simp [WithBot.some_eq_coe, WithBot.coe_lt_coe, not_lt_maximum_of_mem ha h, not_false_iff]