ι : Type u_2
α : Type ?u.101039
M : Type u_1
N : Type ?u.101045
P : Type ?u.101048
M₀ : Type ?u.101051
G : Type ?u.101054
R : Type ?u.101057
inst✝⁷ : Monoid M
inst✝⁶ : Monoid N
inst✝⁵ : Monoid P
l✝ l₁ l₂ : List M
a : M
inst✝⁴ : LinearOrder M
inst✝³ : CovariantClass M M (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
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l : List ι
hl : l ≠ []
f g : ι → M
h : ∀ (x : ι), x ∈ l → g x < f x
⊢ prod (map g l) < prod (map f l)
ι : Type u_2
α : Type ?u.101039
M : Type u_1
N : Type ?u.101045
P : Type ?u.101048
M₀ : Type ?u.101051
G : Type ?u.101054
R : Type ?u.101057
inst✝⁷ : Monoid M
inst✝⁶ : Monoid N
inst✝⁵ : Monoid P
l✝ l₁ l₂ : List M
a : M
inst✝⁴ : LinearOrder M
inst✝³ : CovariantClass M M (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
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l : List ι
hl : l ≠ []
f g : ι → M
h : prod (map f l) ≤ prod (map g l)
⊢ ∃ x, x ∈ l ∧ f x ≤ g x
contrapose! h
no goals
ι : Type u_2
α : Type ?u.101039
M : Type u_1
N : Type ?u.101045
P : Type ?u.101048
M₀ : Type ?u.101051
G : Type ?u.101054
R : Type ?u.101057
inst✝⁷ : Monoid M
inst✝⁶ : Monoid N
inst✝⁵ : Monoid P
l✝ l₁ l₂ : List M
a : M
inst✝⁴ : LinearOrder M
inst✝³ : CovariantClass M M (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
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l : List ι
hl : l ≠ []
f g : ι → M
h : ∀ (x : ι), x ∈ l → g x < f x
⊢ prod (map g l) < prod (map f l)
exact prod_lt_prod_of_ne_nil hl _ _ h