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 : Antivary f g
⊢ ∑ i : ι, f i • g (↑σ i) = ∑ i : ι, f i • g i ↔ Antivary f (g ∘ ↑σ)
simp [(hfg.antivaryOn _).sum_smul_eq_sum_smul_comp_perm_iff fun _ _ ↦ mem_univ _]