case nil
α : Type u_1
β : Type ?u.111970
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l✝ l : List α
a : α
h✝ : ∀ (x : α), x ∈ l → x ≤ a
h : ∀ (x : α), x ∈ [] → x ≤ a
⊢ foldr max ⊥ [] ≤ a

case cons
α : Type u_1
β : Type ?u.111970
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l✝¹ l✝ : List α
a : α
h✝ : ∀ (x : α), x ∈ l✝ → x ≤ a
y : α
l : List α
IH : (∀ (x : α), x ∈ l → x ≤ a) → foldr max ⊥ l ≤ a
h : ∀ (x : α), x ∈ y :: l → x ≤ a
⊢ foldr max ⊥ (y :: l) ≤ a
α : Type u_1
β : Type ?u.111970
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l✝ l : List α
a : α
h : ∀ (x : α), x ∈ l → x ≤ a
⊢ foldr max ⊥ l ≤ a
induction' l with y l IH
no goals
case nil
α : Type u_1
β : Type ?u.111970
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l✝ l : List α
a : α
h✝ : ∀ (x : α), x ∈ l → x ≤ a
h : ∀ (x : α), x ∈ [] → x ≤ a
⊢ foldr max ⊥ [] ≤ a
simp
no goals
case cons
α : Type u_1
β : Type ?u.111970
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l✝¹ l✝ : List α
a : α
h✝ : ∀ (x : α), x ∈ l✝ → x ≤ a
y : α
l : List α
IH : (∀ (x : α), x ∈ l → x ≤ a) → foldr max ⊥ l ≤ a
h : ∀ (x : α), x ∈ y :: l → x ≤ a
⊢ foldr max ⊥ (y :: l) ≤ a
simpa [h y (mem_cons_self _ _)] using IH fun x hx => h x <| mem_cons_of_mem _ hx