∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) {E : Type u_8} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : α → NNReal} (f_meas : Measurable f),
  MeasureTheory.withDensitySMulLI μ f_meas = MeasureTheory.withDensitySMulLI μ f_meas