-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
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 μ)
⊢ 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)
have 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)
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