-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
x y z : E
h1 :
  ‖x + y + z + (x - z)‖ * ‖x + y + z + (x - z)‖ + ‖x + y + z - (x - z)‖ * ‖x + y + z - (x - z)‖ =
    2 * (‖x + y + z‖ * ‖x + y + z‖ + ‖x - z‖ * ‖x - z‖)
h2 :
  ‖x + y - z + (x + z)‖ * ‖x + y - z + (x + z)‖ + ‖x + y - z - (x + z)‖ * ‖x + y - z - (x + z)‖ =
    2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖)
h3 : ‖y + z + z‖ * ‖y + z + z‖ + ‖y + z - z‖ * ‖y + z - z‖ = 2 * (‖y + z‖ * ‖y + z‖ + ‖z‖ * ‖z‖)
h4 : ‖y - z + z‖ * ‖y - z + z‖ + ‖y - z - z‖ * ‖y - z - z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)
h5 :
  ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z + (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z)‖ *
        ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z + (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z)‖ +
      ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z - (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z)‖ *
        ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z - (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z)‖ =
    2 *
      (‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z‖ +
        ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z‖)
h6 :
  ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z + (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z)‖ *
        ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z + (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z)‖ +
      ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z - (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z)‖ *
        ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z - (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z)‖ =
    2 *
      (‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z‖ +
        ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z‖)
h7 :
  ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z + z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z + z‖ +
      ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z - z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z - z‖ =
    2 * (‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z‖ + ‖z‖ * ‖z‖)
h8 :
  ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z + z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z + z‖ +
      ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z - z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z - z‖ =
    2 * (‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z‖ + ‖z‖ * ‖z‖)
h1₁ :
  Eq (α := 𝕜)
    ((𝓚 : (a : ℝ) → 𝕜) (‖x + y + z + (x - z)‖ * ‖x + y + z + (x - z)‖ + ‖x + y + z - (x - z)‖ * ‖x + y + z - (x - z)‖) :
      𝕜)
    ((𝓚 : (a : ℝ) → 𝕜) (2 * (‖x + y + z‖ * ‖x + y + z‖ + ‖x - z‖ * ‖x - z‖)) : 𝕜)
h2₁ :
  Eq (α := 𝕜)
    ((𝓚 : (a : ℝ) → 𝕜) (‖x + y - z + (x + z)‖ * ‖x + y - z + (x + z)‖ + ‖x + y - z - (x + z)‖ * ‖x + y - z - (x + z)‖) :
      𝕜)
    ((𝓚 : (a : ℝ) → 𝕜) (2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖)) : 𝕜)
h3₁ :
  Eq (α := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) (‖y + z + z‖ * ‖y + z + z‖ + ‖y + z - z‖ * ‖y + z - z‖) : 𝕜)
    ((𝓚 : (a : ℝ) → 𝕜) (2 * (‖y + z‖ * ‖y + z‖ + ‖z‖ * ‖z‖)) : 𝕜)
h4₁ :
  Eq (α := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) (‖y - z + z‖ * ‖y - z + z‖ + ‖y - z - z‖ * ‖y - z - z‖) : 𝕜)
    ((𝓚 : (a : ℝ) → 𝕜) (2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)) : 𝕜)
h5₁ :
  Eq (α := 𝕜)
    ((𝓚 : (a : ℝ) → 𝕜)
        (‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z + (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z)‖ *
            ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z + (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z)‖ +
          ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z - (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z)‖ *
            ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z - (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z)‖) :
      𝕜)
    ((𝓚 : (a : ℝ) → 𝕜)
        (2 *
          (‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z‖ +
            ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z‖)) :
      𝕜)
h6₁ :
  Eq (α := 𝕜)
    ((𝓚 : (a : ℝ) → 𝕜)
        (‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z + (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z)‖ *
            ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z + (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z)‖ +
          ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z - (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z)‖ *
            ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z - (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z)‖) :
      𝕜)
    ((𝓚 : (a : ℝ) → 𝕜)
        (2 *
          (‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z‖ +
            ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z‖)) :
      𝕜)
⊢ Eq (α := 𝕜)
    ((𝓚 : (a : ℝ) → 𝕜)
        (‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z + z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z + z‖ +
          ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z - z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z - z‖) :
      𝕜)
    ((𝓚 : (a : ℝ) → 𝕜)
        (2 *
          (‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z‖ +
            ‖z‖ * ‖z‖)) :
      𝕜)

Tactic:
apply_fun 𝓚 at h1 h2 h3 h4 h5 h6 h7 h8