A lemma about measurability with density under scalar multiplication in normed spaces

theorem aemeasurable_withDensity_iff {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace.SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] {f : α → NNReal} (hf : Measurable f) {g : α → E} : AEMeasurable g ↔ AEMeasurable fun x => ↑(f x) • g x