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] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] {f : α → NNReal} (hf : Measurable f) {g : α → E} : AEMeasurable g (μ.withDensity fun (x : α) => ↑(f x)) ↔ AEMeasurable (fun (x : α) => ↑(f x) • g x) μ