ι : Type u_2
α : Type ?u.97864
M : Type u_1
N : Type ?u.97870
P : Type ?u.97873
M₀ : Type ?u.97876
G : Type ?u.97879
R : Type ?u.97882
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l✝ l₁ l₂ : List M
a : M
inst✝² : LinearOrder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l : List ι
f g : ι → M
h : ∀ (i : ι), i ∈ l → g i ≤ f i
⊢ prod (map g l) ≤ prod (map f l)
ι : Type u_2
α : Type ?u.97864
M : Type u_1
N : Type ?u.97870
P : Type ?u.97873
M₀ : Type ?u.97876
G : Type ?u.97879
R : Type ?u.97882
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l✝ l₁ l₂ : List M
a : M
inst✝² : LinearOrder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l : List ι
f g : ι → M
h : prod (map f l) < prod (map g l)
⊢ ∃ i, i ∈ l ∧ f i < g i
contrapose! h
no goals
ι : Type u_2
α : Type ?u.97864
M : Type u_1
N : Type ?u.97870
P : Type ?u.97873
M₀ : Type ?u.97876
G : Type ?u.97879
R : Type ?u.97882
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l✝ l₁ l₂ : List M
a : M
inst✝² : LinearOrder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l : List ι
f g : ι → M
h : ∀ (i : ι), i ∈ l → g i ≤ f i
⊢ prod (map g l) ≤ prod (map f l)
exact prod_le_prod' h