-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst : MeasurableSpace δ
inst_1 : NormedAddCommGroup β
inst_2 : NormedAddCommGroup γ
inst_3 : TopologicalSpace ε
inst_4 : ContinuousENorm ε
inst_5 : TopologicalSpace ε'
inst_6 : ContinuousENorm ε'
inst_7 : ENorm ε''
E : Type u_8
inst_8 : NormedAddCommGroup E
inst_9 : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
r : ℝ
u : ↥(Lp E 1 (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)))
h :
  ∀ (a : α),
    ((↑(f a) : ℝ≥0∞) ≠ 0 →
        (↑(↑(r • u) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) a =
          (r • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E)) a) →
      (↑(↑(MemLp.toLp
                      (fun (x : α) ↦
                        f x • (↑(↑(r • u) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                      ⋯) :
                  α →ₘ[μ] E) :
              α → E)
            a =
          f a • (↑(↑(r • u) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) a →
        (↑(↑(r •
                        MemLp.toLp
                          (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                          ⋯) :
                    α →ₘ[μ] E) :
                α → E)
              a =
            (r •
                (↑(↑(MemLp.toLp
                          (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                          ⋯) :
                      α →ₘ[μ] E) :
                  α → E))
              a →
          (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                          ⋯) :
                      α →ₘ[μ] E) :
                  α → E)
                a =
              f a • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) a →
            (↑(↑(MemLp.toLp
                          (fun (x : α) ↦
                            f x • (↑(↑(r • u) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                          ⋯) :
                      α →ₘ[μ] E) :
                  α → E)
                a =
              (↑(↑(HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ)
                          (MemLp.toLp
                            (fun (x : α) ↦
                              f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                            ⋯)) :
                      α →ₘ[μ] E) :
                  α → E)
                a
⊢ (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑(r • u) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
              ⋯) :
          α →ₘ[μ] E) :
      α → E) =ᶠ[ae μ]
    (↑(↑(HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ)
              (MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                ⋯)) :
          α →ₘ[μ] E) :
      α → E)

Tactic:
filter_upwards [(ae_withDensity_iff f_meas.coe_nnreal_ennreal).1 (Lp.coeFn_smul r u),
      (memL1_smul_of_L1_withDensity f_meas (r • u)).coeFn_toLp,
      Lp.coeFn_smul r ((memL1_smul_of_L1_withDensity f_meas u).toLp _),
      (memL1_smul_of_L1_withDensity f_meas u).coeFn_toLp]

Premises used: Measurable.coe_nnreal_ennreal, MeasureTheory.ae_withDensity_iff, MeasureTheory.Lp.coeFn_smul, MeasureTheory.memL1_smul_of_L1_withDensity, MeasureTheory.MemLp.toLp, Iff.mp, MeasureTheory.MemLp.coeFn_toLp, HSMul.hSMul