no goals
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedRing α
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module α β
inst✝¹ : OrderedSMul α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Monovary f g
⊢ ∑ i : ι, f (↑σ i) • g i < ∑ i : ι, f i • g i ↔ ¬Monovary (f ∘ ↑σ) g
simp [(hfg.monovaryOn _).sum_comp_perm_smul_lt_sum_smul_iff fun _ _ ↦ mem_univ _]