-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
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∞)))
⊢ (↑(↑(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)
have h : ∀ (a : α),
  (↑(↑(MemLp.toLp (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x) sorry) :
              α →ₘ[μ] 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) sorry) :
                α →ₘ[μ] 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)
                      sorry) :
                  α →ₘ[μ] 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)
                          sorry +
                        MemLp.toLp
                          (fun (x : α) ↦ f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                          sorry) :
                    α →ₘ[μ] E) :
                α → E)
              a =
            ((↑(↑(MemLp.toLp
                          (fun (x : α) ↦ f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                          sorry) :
                      α →ₘ[μ] E) :
                  α → E) +
                (↑(↑(MemLp.toLp
                          (fun (x : α) ↦ f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                          sorry) :
                      α →ₘ[μ] 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)
                          sorry) :
                      α →ₘ[μ] E) :
                  α → E)
                a =
              (↑(↑(MemLp.toLp
                            (fun (x : α) ↦
                              f x • (↑(↑u : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                            sorry +
                          MemLp.toLp
                            (fun (x : α) ↦
                              f x • (↑(↑v : α →ₘ[μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)] E) : α → E) x)
                            sorry) :
                      α →ₘ[μ] E) :
                  α → E)
                a
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)]