case nil
ι : Type ?u.146362
α : Type ?u.146365
M : Type u_1
N : Type u_2
P : Type ?u.146374
M₀ : Type ?u.146377
G : Type ?u.146380
R : Type ?u.146383
inst✝² : AddMonoid M
inst✝¹ : AddMonoid N
inst✝ : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ max (f x) (f y)
⊢ f (sum []) ≤ foldr max 0 (map f [])

case cons
ι : Type ?u.146362
α : Type ?u.146365
M : Type u_1
N : Type u_2
P : Type ?u.146374
M₀ : Type ?u.146377
G : Type ?u.146380
R : Type ?u.146383
inst✝² : AddMonoid M
inst✝¹ : AddMonoid N
inst✝ : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ max (f x) (f y)
hd : M
tl : List M
IH : f (sum tl) ≤ foldr max 0 (map f tl)
⊢ f (sum (hd :: tl)) ≤ foldr max 0 (map f (hd :: tl))
ι : Type ?u.146362
α : Type ?u.146365
M : Type u_1
N : Type u_2
P : Type ?u.146374
M₀ : Type ?u.146377
G : Type ?u.146380
R : Type ?u.146383
inst✝² : AddMonoid M
inst✝¹ : AddMonoid N
inst✝ : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ max (f x) (f y)
l : List M
⊢ f (sum l) ≤ foldr max 0 (map f l)
induction' l with hd tl IH
case cons
ι : Type ?u.146362
α : Type ?u.146365
M : Type u_1
N : Type u_2
P : Type ?u.146374
M₀ : Type ?u.146377
G : Type ?u.146380
R : Type ?u.146383
inst✝² : AddMonoid M
inst✝¹ : AddMonoid N
inst✝ : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ max (f x) (f y)
hd : M
tl : List M
IH : f (sum tl) ≤ foldr (fun x y => max (f x) y) 0 tl
⊢ f (hd + sum tl) ≤ max (f hd) (foldr (fun x y => max (f x) y) 0 tl)
case cons
ι : Type ?u.146362
α : Type ?u.146365
M : Type u_1
N : Type u_2
P : Type ?u.146374
M₀ : Type ?u.146377
G : Type ?u.146380
R : Type ?u.146383
inst✝² : AddMonoid M
inst✝¹ : AddMonoid N
inst✝ : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ max (f x) (f y)
hd : M
tl : List M
IH : f (sum tl) ≤ foldr max 0 (map f tl)
⊢ f (sum (hd :: tl)) ≤ foldr max 0 (map f (hd :: tl))
simp only [List.sum_cons, List.foldr_map, List.foldr] at IH⊢
no goals
case cons
ι : Type ?u.146362
α : Type ?u.146365
M : Type u_1
N : Type u_2
P : Type ?u.146374
M₀ : Type ?u.146377
G : Type ?u.146380
R : Type ?u.146383
inst✝² : AddMonoid M
inst✝¹ : AddMonoid N
inst✝ : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ max (f x) (f y)
hd : M
tl : List M
IH : f (sum tl) ≤ foldr (fun x y => max (f x) y) 0 tl
⊢ f (hd + sum tl) ≤ max (f hd) (foldr (fun x y => max (f x) y) 0 tl)
exact (hadd _ _).trans (max_le_max le_rfl IH)
no goals
case nil
ι : Type ?u.146362
α : Type ?u.146365
M : Type u_1
N : Type u_2
P : Type ?u.146374
M₀ : Type ?u.146377
G : Type ?u.146380
R : Type ?u.146383
inst✝² : AddMonoid M
inst✝¹ : AddMonoid N
inst✝ : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ max (f x) (f y)
⊢ f (sum []) ≤ foldr max 0 (map f [])
simpa using h0