case nil
α : Type u_1
β : Type ?u.114493
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l✝ l : List α
a x : α
hx✝ : x ∈ l
h : a ≤ x
hx : x ∈ []
⊢ a ≤ foldr max ⊥ []

case cons
α : Type u_1
β : Type ?u.114493
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l✝¹ l✝ : List α
a x : α
hx✝ : x ∈ l✝
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
hx : x ∈ y :: l
⊢ a ≤ foldr max ⊥ (y :: l)
α : Type u_1
β : Type ?u.114493
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l✝ l : List α
a x : α
hx : x ∈ l
h : a ≤ x
⊢ a ≤ foldr max ⊥ l
induction' l with y l IH
no goals
case nil
α : Type u_1
β : Type ?u.114493
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l✝ l : List α
a x : α
hx✝ : x ∈ l
h : a ≤ x
hx : x ∈ []
⊢ a ≤ foldr max ⊥ []
exact absurd hx (not_mem_nil _)
case cons.head
α : Type u_1
β : Type ?u.114493
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l✝¹ l✝ : List α
a x : α
hx : x ∈ l✝
h : a ≤ x
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
⊢ a ≤ foldr max ⊥ (x :: l)

case cons.tail
α : Type u_1
β : Type ?u.114493
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l✝¹ l✝ : List α
a x : α
hx : x ∈ l✝
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
a✝ : Mem x l
⊢ a ≤ foldr max ⊥ (y :: l)
case cons
α : Type u_1
β : Type ?u.114493
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l✝¹ l✝ : List α
a x : α
hx✝ : x ∈ l✝
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
hx : x ∈ y :: l
⊢ a ≤ foldr max ⊥ (y :: l)
obtain hl | hl := hx
case cons.head
α : Type u_1
β : Type ?u.114493
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l✝¹ l✝ : List α
a x : α
hx : x ∈ l✝
h : a ≤ x
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
⊢ a ≤ max x (foldr max ⊥ l)

case cons.tail
α : Type u_1
β : Type ?u.114493
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l✝¹ l✝ : List α
a x : α
hx : x ∈ l✝
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
a✝ : Mem x l
⊢ a ≤ foldr max ⊥ (y :: l)
case cons.head
α : Type u_1
β : Type ?u.114493
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l✝¹ l✝ : List α
a x : α
hx : x ∈ l✝
h : a ≤ x
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
⊢ a ≤ foldr max ⊥ (x :: l)

case cons.tail
α : Type u_1
β : Type ?u.114493
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l✝¹ l✝ : List α
a x : α
hx : x ∈ l✝
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
a✝ : Mem x l
⊢ a ≤ foldr max ⊥ (y :: l)
simp only [foldr, foldr_cons]
no goals
case cons.head
α : Type u_1
β : Type ?u.114493
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l✝¹ l✝ : List α
a x : α
hx : x ∈ l✝
h : a ≤ x
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
⊢ a ≤ max x (foldr max ⊥ l)
exact le_max_of_le_left h
no goals
case cons.tail
α : Type u_1
β : Type ?u.114493
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l✝¹ l✝ : List α
a x : α
hx : x ∈ l✝
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
a✝ : Mem x l
⊢ a ≤ foldr max ⊥ (y :: l)
exact le_max_of_le_right (IH (by assumption))
no goals
α : Type u_1
β : Type ?u.114493
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l✝¹ l✝ : List α
a x : α
hx : x ∈ l✝
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
a✝ : Mem x l
⊢ x ∈ l
assumption