ι : Type u_1
α : Type ?u.144180
β : Type ?u.144183
M : Type u_2
N : Type ?u.144189
G : Type ?u.144192
k : Type ?u.144195
R : Type ?u.144198
inst✝ : LinearOrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
hs : Finset.Nonempty s
Hlt : ∀ (i : ι), i ∈ s → g i < f i
⊢ ∏ i in s, g i < ∏ i in s, f i
ι : Type u_1
α : Type ?u.144180
β : Type ?u.144183
M : Type u_2
N : Type ?u.144189
G : Type ?u.144192
k : Type ?u.144195
R : Type ?u.144198
inst✝ : LinearOrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
hs : Finset.Nonempty s
Hle : ∏ i in s, f i ≤ ∏ i in s, g i
⊢ ∃ i, i ∈ s ∧ f i ≤ g i
contrapose! Hle with Hlt
no goals
ι : Type u_1
α : Type ?u.144180
β : Type ?u.144183
M : Type u_2
N : Type ?u.144189
G : Type ?u.144192
k : Type ?u.144195
R : Type ?u.144198
inst✝ : LinearOrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
hs : Finset.Nonempty s
Hlt : ∀ (i : ι), i ∈ s → g i < f i
⊢ ∏ i in s, g i < ∏ i in s, f i
exact prod_lt_prod_of_nonempty' hs Hlt