case nil
α : Type u_1
β : Type ?u.107747
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
h✝ : l ≠ []
h : [] ≠ []
⊢ ↑(foldr max ⊥ []) = maximum []

case cons
α : Type u_1
β : Type ?u.107747
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
h✝ : l ≠ []
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = maximum tl
h : hd :: tl ≠ []
⊢ ↑(foldr max ⊥ (hd :: tl)) = maximum (hd :: tl)
α : Type u_1
β : Type ?u.107747
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
h : l ≠ []
⊢ ↑(foldr max ⊥ l) = maximum l
induction' l with hd tl IH
no goals
case nil
α : Type u_1
β : Type ?u.107747
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
h✝ : l ≠ []
h : [] ≠ []
⊢ ↑(foldr max ⊥ []) = maximum []
contradiction
case cons
α : Type u_1
β : Type ?u.107747
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
h✝ : l ≠ []
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = maximum tl
h : hd :: tl ≠ []
⊢ max ↑hd ↑(foldr max ⊥ tl) = max (↑hd) (maximum tl)
case cons
α : Type u_1
β : Type ?u.107747
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
h✝ : l ≠ []
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = maximum tl
h : hd :: tl ≠ []
⊢ ↑(foldr max ⊥ (hd :: tl)) = maximum (hd :: tl)
rw [maximum_cons, foldr, WithBot.coe_max]
case pos
α : Type u_1
β : Type ?u.107747
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
h✝¹ : l ≠ []
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = maximum tl
h✝ : hd :: tl ≠ []
h : tl = []
⊢ max ↑hd ↑(foldr max ⊥ tl) = max (↑hd) (maximum tl)

case neg
α : Type u_1
β : Type ?u.107747
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
h✝¹ : l ≠ []
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = maximum tl
h✝ : hd :: tl ≠ []
h : ¬tl = []
⊢ max ↑hd ↑(foldr max ⊥ tl) = max (↑hd) (maximum tl)
case cons
α : Type u_1
β : Type ?u.107747
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
h✝ : l ≠ []
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = maximum tl
h : hd :: tl ≠ []
⊢ max ↑hd ↑(foldr max ⊥ tl) = max (↑hd) (maximum tl)
by_cases h : tl = []
no goals
case pos
α : Type u_1
β : Type ?u.107747
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
h✝¹ : l ≠ []
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = maximum tl
h✝ : hd :: tl ≠ []
h : tl = []
⊢ max ↑hd ↑(foldr max ⊥ tl) = max (↑hd) (maximum tl)
simp [h]
no goals
case neg
α : Type u_1
β : Type ?u.107747
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
h✝¹ : l ≠ []
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = maximum tl
h✝ : hd :: tl ≠ []
h : ¬tl = []
⊢ max ↑hd ↑(foldr max ⊥ tl) = max (↑hd) (maximum tl)
simp [IH h]