-- 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
u v : ↥(Lp E 1 (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)))
h :
  ∀ (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 • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯) :
                  α →ₘ[μ] E) :
              α → E)
            a =
          f a • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) a →
        (↑(↑(MemLp.toLp
                        (fun (x : α) ↦
                          f x • (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                        ⋯) :
                    α →ₘ[μ] E) :
                α → E)
              a =
            f a • (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) a →
          (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                            ⋯ +
                          MemLp.toLp
                            (fun (x : α) ↦
                              f x • (↑(↑v : α →ₘ[μ.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) +
                  (↑(↑(MemLp.toLp
                            (fun (x : α) ↦
                              f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                            ⋯) :
                        α →ₘ[μ] E) :
                    α → E))
                a →
            ((↑(f a) : ℝ≥0∞) ≠ 0 →
                (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) a =
                  ((↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) +
                      (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E))
                    a) →
              (↑(↑(MemLp.toLp
                            (fun (x : α) ↦
                              f x • (↑(↑(u + v) : α →ₘ[μ.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)
                              ⋯ +
                            MemLp.toLp
                              (fun (x : α) ↦
                                f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                              ⋯) :
                        α →ₘ[μ] E) :
                    α → E)
                  a
⊢ (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑(u + v) : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
              ⋯) :
          α →ₘ[μ] E) :
      α → E) =ᶠ[ae μ]
    (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) ⋯ +
              MemLp.toLp (fun (x : α) ↦ f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                ⋯) :
          α →ₘ[μ] E) :
      α → E)

Tactic:
filter_upwards [(memL1_smul_of_L1_withDensity f_meas u).coeFn_toLp,
      (memL1_smul_of_L1_withDensity f_meas v).coeFn_toLp,
      (memL1_smul_of_L1_withDensity f_meas (u + v)).coeFn_toLp,
      Lp.coeFn_add ((memL1_smul_of_L1_withDensity f_meas u).toLp _)
        ((memL1_smul_of_L1_withDensity f_meas v).toLp _),
      (ae_withDensity_iff f_meas.coe_nnreal_ennreal).1 (Lp.coeFn_add u v)]

Premises used: MeasureTheory.Lp.coeFn_add, Measurable.coe_nnreal_ennreal, MeasureTheory.ae_withDensity_iff, MeasureTheory.memL1_smul_of_L1_withDensity, HAdd.hAdd, MeasureTheory.MemLp.toLp, Iff.mp, MeasureTheory.MemLp.coeFn_toLp