-- 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 :
  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‖)) :
      𝕜)
h7 :
  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‖)) :
      𝕜)
h8 :
  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‖)) :
      𝕜)
simp :
  ∀
    (h1 :
      HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y + z + (x - z)‖ : 𝕜)
            ((𝓚 : (a : ℝ) → 𝕜) ‖x + y + z + (x - z)‖ : 𝕜) +
          HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y + z - (x - z)‖ : 𝕜)
            ((𝓚 : (a : ℝ) → 𝕜) ‖x + y + z - (x - z)‖ : 𝕜) =
        2 *
          (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y + z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y + z‖ : 𝕜) +
            HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x - z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x - z‖ : 𝕜)))
    (h2 :
      HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y - z + (x + z)‖ : 𝕜)
            ((𝓚 : (a : ℝ) → 𝕜) ‖x + y - z + (x + z)‖ : 𝕜) +
          HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y - z - (x + z)‖ : 𝕜)
            ((𝓚 : (a : ℝ) → 𝕜) ‖x + y - z - (x + z)‖ : 𝕜) =
        2 *
          (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y - z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y - z‖ : 𝕜) +
            HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + z‖ : 𝕜)))
    (h3 :
      HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y + z + z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y + z + z‖ : 𝕜) +
          HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y + z - z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y + z - z‖ : 𝕜) =
        2 *
          (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y + z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y + z‖ : 𝕜) +
            HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖z‖ : 𝕜)))
    (h4 :
      HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y - z + z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y - z + z‖ : 𝕜) +
          HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y - z - z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y - z - z‖ : 𝕜) =
        2 *
          (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y - z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y - z‖ : 𝕜) +
            HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖z‖ : 𝕜)))
    (h5 :
      HMul.hMul (α := 𝕜) (β := 𝕜)
            ((𝓚 : (a : ℝ) → 𝕜)
                ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z +
                    (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z)‖ :
              𝕜)
            ((𝓚 : (a : ℝ) → 𝕜)
                ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z +
                    (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z)‖ :
              𝕜) +
          HMul.hMul (α := 𝕜) (β := 𝕜)
            ((𝓚 : (a : ℝ) → 𝕜)
                ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z -
                    (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z)‖ :
              𝕜)
            ((𝓚 : (a : ℝ) → 𝕜)
                ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z -
                    (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z)‖ :
              𝕜) =
        2 *
          (HMul.hMul (α := 𝕜) (β := 𝕜)
              ((𝓚 : (a : ℝ) → 𝕜)
                  ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z‖ :
                𝕜)
              ((𝓚 : (a : ℝ) → 𝕜)
                  ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z‖ :
                𝕜) +
            HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z‖ : 𝕜)
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z‖ : 𝕜)))
    (h6 :
      HMul.hMul (α := 𝕜) (β := 𝕜)
            ((𝓚 : (a : ℝ) → 𝕜)
                ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z +
                    (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z)‖ :
              𝕜)
            ((𝓚 : (a : ℝ) → 𝕜)
                ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z +
                    (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z)‖ :
              𝕜) +
          HMul.hMul (α := 𝕜) (β := 𝕜)
            ((𝓚 : (a : ℝ) → 𝕜)
                ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z -
                    (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z)‖ :
              𝕜)
            ((𝓚 : (a : ℝ) → 𝕜)
                ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z -
                    (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z)‖ :
              𝕜) =
        2 *
          (HMul.hMul (α := 𝕜) (β := 𝕜)
              ((𝓚 : (a : ℝ) → 𝕜)
                  ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z‖ :
                𝕜)
              ((𝓚 : (a : ℝ) → 𝕜)
                  ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z‖ :
                𝕜) +
            HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z‖ : 𝕜)
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z‖ : 𝕜)))
    (h7 :
      HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z + z‖ : 𝕜)
            ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z + z‖ : 𝕜) +
          HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z - z‖ : 𝕜)
            ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z - z‖ : 𝕜) =
        2 *
          (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z‖ : 𝕜)
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z‖ : 𝕜) +
            HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖z‖ : 𝕜)))
    (h8 :
      HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z + z‖ : 𝕜)
            ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z + z‖ : 𝕜) +
          HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z - z‖ : 𝕜)
            ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z - z‖ : 𝕜) =
        2 *
          (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z‖ : 𝕜)
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z‖ : 𝕜) +
            HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖z‖ : 𝕜))),
    4⁻¹ *
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y + z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y + z‖ : 𝕜) -
              HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y - z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y - z‖ : 𝕜) +
            HMul.hMul (β := 𝕜)
              (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
                ((𝓚 : (a : ℝ) → 𝕜)
                    ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z‖ :
                  𝕜))
              ((𝓚 : (a : ℝ) → 𝕜)
                  ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z‖ :
                𝕜) -
          HMul.hMul (β := 𝕜)
            (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
              ((𝓚 : (a : ℝ) → 𝕜)
                  ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z‖ :
                𝕜))
            ((𝓚 : (a : ℝ) → 𝕜)
                ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z‖ :
              𝕜)) =
      4⁻¹ *
          (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + z‖ : 𝕜) -
                HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x - z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x - z‖ : 𝕜) +
              HMul.hMul (β := 𝕜)
                (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
                  ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z‖ : 𝕜))
                ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z‖ : 𝕜) -
            HMul.hMul (β := 𝕜)
              (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
                ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z‖ : 𝕜))
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z‖ : 𝕜)) +
        4⁻¹ *
          (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y + z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y + z‖ : 𝕜) -
                HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y - z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y - z‖ : 𝕜) +
              HMul.hMul (β := 𝕜)
                (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
                  ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z‖ : 𝕜))
                ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z‖ : 𝕜) -
            HMul.hMul (β := 𝕜)
              (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
                ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z‖ : 𝕜))
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z‖ : 𝕜))
⊢ 4⁻¹ *
      (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y + z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y + z‖ : 𝕜) -
            HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y - z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y - z‖ : 𝕜) +
          HMul.hMul (β := 𝕜)
            (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z‖ : 𝕜))
            ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z‖ : 𝕜) -
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
            ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z‖ : 𝕜))
          ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z‖ : 𝕜)) =
    4⁻¹ *
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + z‖ : 𝕜) -
              HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x - z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x - z‖ : 𝕜) +
            HMul.hMul (β := 𝕜)
              (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
                ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z‖ : 𝕜))
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z‖ : 𝕜) -
          HMul.hMul (β := 𝕜)
            (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z‖ : 𝕜))
            ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z‖ : 𝕜)) +
      4⁻¹ *
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y + z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y + z‖ : 𝕜) -
              HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y - z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y - z‖ : 𝕜) +
            HMul.hMul (β := 𝕜)
              (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
                ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z‖ : 𝕜))
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z‖ : 𝕜) -
          HMul.hMul (β := 𝕜)
            (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z‖ : 𝕜))
            ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z‖ : 𝕜))

Tactic:
simp only [map_add, map_mul, map_ofNat, smul_add] at *

Premises used: map_ofNat, map_add, map_mul, smul_add