-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
Goal:
α : Type u_1
E : Type u_4
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : ↥(simpleFunc E p μ)
a : α
h h₁ :
  ∀
    (h :
      (toSimpleFunc (f - g) : (a : α) → E) a =
        (↑((↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) - (↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a),
    (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
      (toSimpleFunc g : (a : α) → E) a = (↑(↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
        (↑((↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) - (↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a =
            (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a - (↑(↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
          (toSimpleFunc (f - g) : (a : α) → E) a =
            HSub.hSub (α := E) (β := E) ((toSimpleFunc f : (a : α) → E) a : E) ((toSimpleFunc g : (a : α) → E) a : E)
h₂ :
  ∀
    (h :
      (toSimpleFunc (f - g) : (a : α) → E) a =
        (↑((↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) - (↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a),
    (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
      (toSimpleFunc g : (a : α) → E) a = (↑(↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
        (↑((↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) - (↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a =
            (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a - (↑(↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
          (↑((↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) - (↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a =
            HSub.hSub (α := E) (β := E) ((toSimpleFunc f : (a : α) → E) a : E) ((toSimpleFunc g : (a : α) → E) a : E)
h₃ :
  ∀
    (h :
      (toSimpleFunc (f - g) : (a : α) → E) a =
        (↑((↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) - (↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a)
    (h : (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a),
    (toSimpleFunc g : (a : α) → E) a = (↑(↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
      (↑((↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) - (↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a =
          (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a - (↑(↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
        (↑((↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) - (↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a =
          HSub.hSub (β := E) ((↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a) ((toSimpleFunc g : (a : α) → E) a : E)
h₄ :
  ∀
    (h :
      (toSimpleFunc (f - g) : (a : α) → E) a =
        (↑((↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) - (↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a)
    (h : (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a)
    (h : (toSimpleFunc g : (a : α) → E) a = (↑(↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a),
    (↑((↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) - (↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a =
        (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a - (↑(↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
      (↑((↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) - (↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a =
        (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a - (↑(↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a
⊢ (toSimpleFunc (f - g) : (a : α) → E) a =
      (↑((↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) - (↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a →
    (toSimpleFunc f : (a : α) → E) a = (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
      (toSimpleFunc g : (a : α) → E) a = (↑(↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
        (↑((↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) - (↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E)) : α → E) a =
            (↑(↑(↑f : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a - (↑(↑(↑g : ↥(Lp E p μ)) : α →ₘ[μ] E) : α → E) a →
          (toSimpleFunc (f - g) : (a : α) → E) a =
            HSub.hSub (α := E) (β := E) ((toSimpleFunc f : (a : α) → E) a : E) ((toSimpleFunc g : (a : α) → E) a : E)

Tactic:
repeat' intro h; rw [h]