Monotonicity of finprod

Stream: mathlib4

[Michael Stoll]

import Mathlib

open NNReal

-- Mathlib has this:
example {α} {s : Finset α} (f g : α → ℝ≥0) (h : f ≤ g) :
    ∏ a ∈ s, f a ≤ ∏ a ∈ s, g a :=
  Finset.prod_le_prod' fun i _ ↦ h i

-- but apparently not this:
example {α} {f g : α → ℝ≥0} (hf : f.mulSupport.Finite) (hg : g.mulSupport.Finite) (h : f ≤ g) :
    ∏ᶠ a, f a ≤ ∏ᶠ a, g a := by
  -- `exact?` fails; `apply?` and `rw?` do not seem to proudce something helpful
  have : (f.mulSupport ∪ g.mulSupport).Finite := Set.Finite.union hf hg
  have : Fintype ↑(f.mulSupport ∪ g.mulSupport) := this.fintype
  let s := (f.mulSupport ∪ g.mulSupport).toFinset
  have hf₁ : f.mulSupport ⊆ s := by
    simp only [Set.coe_toFinset, Set.subset_union_left, s]
  have hg₁ : g.mulSupport ⊆ s := by
    simp only [Set.coe_toFinset, Set.subset_union_right, s]
  rw [finprod_eq_finset_prod_of_mulSupport_subset f hf₁, finprod_eq_finset_prod_of_mulSupport_subset g hg₁]
  exact Finset.prod_le_prod' fun i a => h i

• Can this be done more elegantly?
• Is this an API gap?