-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
𝕜_1 : Type u_2
𝕜'_1 : Type u_3
E : Type u_4
F_1 : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F_1
g_1 : E → F_1
c : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' F_1
σ : 𝕜 →+* 𝕜'
inst_6 : RingHomIsometric σ
F : Type u_8
G : Type u_9
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
B : G →L[𝕜] E →L[𝕜] F
g h : G
f : ↥(Lp E p μ)
h₁ :
  ∀ (x : α)
    (hx :
      Eq.{u_8 + 1} (α := F)
        ((↑(↑(compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜)
                      ((B : (a : G) → E →L[𝕜] F) (g + h)) f) :
                  α →ₘ[μ] F) :
              α → F)
            x :
          F)
        ((((B : (a : G) → E →L[𝕜] F) (g + h) : E →L[𝕜] F) : (a : E) → F) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F))
    (hg :
      Eq.{u_8 + 1} (α := F)
        ((↑(↑(compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜) ((B : (a : G) → E →L[𝕜] F) g) f) :
                  α →ₘ[μ] F) :
              α → F)
            x :
          F)
        ((((B : (a : G) → E →L[𝕜] F) g : E →L[𝕜] F) : (a : E) → F) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F))
    (hh :
      Eq.{u_8 + 1} (α := F)
        ((↑(↑(compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜) ((B : (a : G) → E →L[𝕜] F) h) f) :
                  α →ₘ[μ] F) :
              α → F)
            x :
          F)
        ((((B : (a : G) → E →L[𝕜] F) h : E →L[𝕜] F) : (a : E) → F) ((↑(↑f : α →ₘ[μ] E) : α → E) x) : F))
    (hadd :
      (↑(↑(HAdd.hAdd (α := ↥(Lp F p μ))
                    (compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜)
                      ((B : (a : G) → E →L[𝕜] F) g) f)
                    (compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜)
                      ((B : (a : G) → E →L[𝕜] F) h) f)) :
                α →ₘ[μ] F) :
            α → F)
          x =
        HAdd.hAdd (α := α → F) (β := α → F)
          (↑(↑(compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜) ((B : (a : G) → E →L[𝕜] F) g)
                    f) :
                α →ₘ[μ] F) :
            α → F)
          (↑(↑(compLp.{u_1, u_4, u_8, u_6, u_6} (𝕜 := 𝕜) (𝕜' := 𝕜) (σ := RingHom.id 𝕜) ((B : (a : G) → E →L[𝕜] F) h)
                    f) :
                α →ₘ[μ] F) :
            α → F)
          x),
    Eq.{u_8 + 1} (α := F)
      ((↑(↑((compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) (g + h)) : (a : ↥(Lp E p μ)) → ↥(Lp F p μ)) f) : α →ₘ[μ] F) : α → F)
        x)
      ((↑(↑((HAdd.hAdd (α := ↥(Lp E p μ) →ₗ[𝕜] ↥(Lp F p μ)) (compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) g))
                      (compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) h)) :
                    (a : ↥(Lp E p μ)) → ↥(Lp F p μ))
                  f) :
              α →ₘ[μ] F) :
          α → F)
        x)
⊢ EventuallyEq.{u_1, u_8} (β := F) (ae μ)
    (↑(↑((compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) (g + h)) : (a : ↥(Lp E p μ)) → ↥(Lp F p μ)) f) : α →ₘ[μ] F) : α → F)
    (↑(↑((HAdd.hAdd (α := ↥(Lp E p μ) →ₗ[𝕜] ↥(Lp F p μ)) (compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) g))
                  (compLpₗ p μ ((B : (a : G) → E →L[𝕜] F) h)) :
                (a : ↥(Lp E p μ)) → ↥(Lp F p μ))
              f) :
          α →ₘ[μ] F) :
      α → F)

Tactic:
filter_upwards [(B (g + h)).coeFn_compLp f, (B g).coeFn_compLp f, (B h).coeFn_compLp f,
      Lp.coeFn_add ((B g).compLp f) ((B h).compLp f)] with x hx hg hh hadd

Premises used: MeasureTheory.Lp.coeFn_add, ContinuousLinearMap.compLp, HAdd.hAdd, ContinuousLinearMap.coeFn_compLp, DFunLike.coe