∀ {α : Type u_1} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {R : Type u_5} [inst : NormedRing R]
  [inst_1 : NormedSpace ℝ R] [inst_2 : CompleteSpace R] (n : ℕ) [inst_3 : n.AtLeastTwo] (f : α → R),
  (μ[OfNat.ofNat n * f | m] =ᵐ[μ] OfNat.ofNat n * μ[f | m]) = True