Exp le exp of map

lemma exp_le_exp_of_map {f : Prob α} {g : Prob β} {u : α → ℝ} {v : β → ℝ} (i : α → β)    (inj : ∀ x0 x1, f.prob x0 * u x0 ≠ 0 → f.prob x1 * u x1 ≠ 0 → i x0 = i x1 → x0 = x1)    (uv : ∀ x, f.prob x * u x ≠ 0 → f.prob x * u x ≤ g.prob (i x) * v (i x))    (v0 : ∀ y, g.prob y ≠ 0 → 0 ≤ v y) : f.exp u ≤ g.exp v := by  simp only [exp, Finsupp.sum]  apply Finset.sum_le_sum_of_map i inj uv  · intro y m; simp only [Finsupp.mem_support_iff, not_not] at m; simp only [m, zero_mul]  · intro y m; simp only [Finsupp.mem_support_iff] at m; apply mul_nonneg (prob_nonneg _) (v0 _ m)