-- 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 μ)
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
h₁ :
  (((B : (a : G) → E →L[𝕜] F) (g + h) : E →L[𝕜] F) : (a : E) → F) ((↑(↑f : α →ₘ[μ] E) : α → E) 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)

Tactic:
simp only [compLpₗ_apply, LinearMap.add_apply, hx, hadd]

Premises used: ContinuousLinearMap.compLpₗ_apply, LinearMap.add_apply