ι : Type u_2
α : Type ?u.143423
β : Type ?u.143426
M : Type u_1
N : Type ?u.143432
G : Type ?u.143435
k : Type ?u.143438
R : Type ?u.143441
inst✝ : LinearOrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
Hle : ∀ (i : ι), i ∈ s → g i ≤ f i
⊢ ∏ i in s, g i ≤ ∏ i in s, f i
ι : Type u_2
α : Type ?u.143423
β : Type ?u.143426
M : Type u_1
N : Type ?u.143432
G : Type ?u.143435
k : Type ?u.143438
R : Type ?u.143441
inst✝ : LinearOrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
Hlt : ∏ i in s, f i < ∏ i in s, g i
⊢ ∃ i, i ∈ s ∧ f i < g i
contrapose! Hlt with Hle
no goals
ι : Type u_2
α : Type ?u.143423
β : Type ?u.143426
M : Type u_1
N : Type ?u.143432
G : Type ?u.143435
k : Type ?u.143438
R : Type ?u.143441
inst✝ : LinearOrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
Hle : ∀ (i : ι), i ∈ s → g i ≤ f i
⊢ ∏ i in s, g i ≤ ∏ i in s, f i
exact prod_le_prod' Hle