-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.OfNorm (goal)
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 :
  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‖ : 𝕜))
have abel_nf : ∀
  (h8 :
    HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜)
          ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜) +
        HMul.hMul (α := 𝕜) (β := 𝕜)
          ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul (α := ℤ) (-2) z + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜)
          ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul (α := ℤ) (-2) z + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜) =
      2 *
        (HMul.hMul (α := 𝕜) (β := 𝕜)
            ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul (α := ℤ) (-1) z + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜)
            ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul (α := ℤ) (-1) z + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜) +
          HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖z‖ : 𝕜)))
  (h7 :
    HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜)
          ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜) +
        HMul.hMul (α := 𝕜) (β := 𝕜)
          ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul (α := ℤ) 2 z + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜)
          ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul (α := ℤ) 2 z + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜) =
      2 *
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖z‖ : 𝕜) +
          HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖z + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜)
            ((𝓚 : (a : ℝ) → 𝕜) ‖z + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜)))
  (h6 :
    HMul.hMul (α := 𝕜) (β := 𝕜)
          ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul (α := ℤ) (-2) z + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜)
          ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul (α := ℤ) (-2) z + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜) +
        HMul.hMul (α := 𝕜) (β := 𝕜)
          ((𝓚 : (a : ℝ) → 𝕜)
              ‖HSMul.hSMul (α := ℤ) 2 (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x) +
                  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ :
            𝕜)
          ((𝓚 : (a : ℝ) → 𝕜)
              ‖HSMul.hSMul (α := ℤ) 2 (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x) +
                  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ :
            𝕜) =
      2 *
        (HMul.hMul (α := 𝕜) (β := 𝕜)
            ((𝓚 : (a : ℝ) → 𝕜)
                ‖HSMul.hSMul (α := ℤ) (-1) z +
                    (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y)‖ :
              𝕜)
            ((𝓚 : (a : ℝ) → 𝕜)
                ‖HSMul.hSMul (α := ℤ) (-1) z +
                    (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y)‖ :
              𝕜) +
          HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖z + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x‖ : 𝕜)
            ((𝓚 : (a : ℝ) → 𝕜) ‖z + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x‖ : 𝕜)))
  (h5 :
    HMul.hMul (α := 𝕜) (β := 𝕜)
          ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul (α := ℤ) 2 z + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜)
          ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul (α := ℤ) 2 z + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜) +
        HMul.hMul (α := 𝕜) (β := 𝕜)
          ((𝓚 : (a : ℝ) → 𝕜)
              ‖HSMul.hSMul (α := ℤ) 2 (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x) +
                  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ :
            𝕜)
          ((𝓚 : (a : ℝ) → 𝕜)
              ‖HSMul.hSMul (α := ℤ) 2 (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x) +
                  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ :
            𝕜) =
      2 *
        (HMul.hMul (α := 𝕜) (β := 𝕜)
            ((𝓚 : (a : ℝ) → 𝕜)
                ‖z + (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y)‖ :
              𝕜)
            ((𝓚 : (a : ℝ) → 𝕜)
                ‖z + (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y)‖ :
              𝕜) +
          HMul.hMul (α := 𝕜) (β := 𝕜)
            ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul (α := ℤ) (-1) z + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x‖ : 𝕜)
            ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul (α := ℤ) (-1) z + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x‖ : 𝕜)))
  (h4 :
    HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y‖ : 𝕜) +
        HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y + HSMul.hSMul (α := ℤ) (-2) z‖ : 𝕜)
          ((𝓚 : (a : ℝ) → 𝕜) ‖y + HSMul.hSMul (α := ℤ) (-2) z‖ : 𝕜) =
      2 *
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y + HSMul.hSMul (α := ℤ) (-1) z‖ : 𝕜)
            ((𝓚 : (a : ℝ) → 𝕜) ‖y + HSMul.hSMul (α := ℤ) (-1) z‖ : 𝕜) +
          HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖z‖ : 𝕜)))
  (h3 :
    HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y‖ : 𝕜) +
        HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y + HSMul.hSMul (α := ℤ) 2 z‖ : 𝕜)
          ((𝓚 : (a : ℝ) → 𝕜) ‖y + HSMul.hSMul (α := ℤ) 2 z‖ : 𝕜) =
      2 *
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y + z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y + z‖ : 𝕜) +
          HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖z‖ : 𝕜)))
  (h2 :
    HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y + HSMul.hSMul (α := ℤ) (-2) z‖ : 𝕜)
          ((𝓚 : (a : ℝ) → 𝕜) ‖y + HSMul.hSMul (α := ℤ) (-2) z‖ : 𝕜) +
        HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul (α := ℤ) 2 x + y‖ : 𝕜)
          ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul (α := ℤ) 2 x + y‖ : 𝕜) =
      2 *
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + (y + HSMul.hSMul (α := ℤ) (-1) z)‖ : 𝕜)
            ((𝓚 : (a : ℝ) → 𝕜) ‖x + (y + HSMul.hSMul (α := ℤ) (-1) z)‖ : 𝕜) +
          HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + z‖ : 𝕜)))
  (h1 :
    HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y + HSMul.hSMul (α := ℤ) 2 z‖ : 𝕜)
          ((𝓚 : (a : ℝ) → 𝕜) ‖y + HSMul.hSMul (α := ℤ) 2 z‖ : 𝕜) +
        HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul (α := ℤ) 2 x + y‖ : 𝕜)
          ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul (α := ℤ) 2 x + y‖ : 𝕜) =
      2 *
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + (y + z)‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + (y + z)‖ : 𝕜) +
          HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + HSMul.hSMul (α := ℤ) (-1) z‖ : 𝕜)
            ((𝓚 : (a : ℝ) → 𝕜) ‖x + HSMul.hSMul (α := ℤ) (-1) z‖ : 𝕜))),
  4⁻¹ *
      (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + (y + z)‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + (y + z)‖ : 𝕜) +
        (HSMul.hSMul (α := ℤ) (-1)
            (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + (y + HSMul.hSMul (α := ℤ) (-1) z)‖ : 𝕜)
              ((𝓚 : (a : ℝ) → 𝕜) ‖x + (y + HSMul.hSMul (α := ℤ) (-1) z)‖ : 𝕜)) +
          (HMul.hMul (β := 𝕜)
              (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
                ((𝓚 : (a : ℝ) → 𝕜)
                    ‖z + (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y)‖ :
                  𝕜))
              ((𝓚 : (a : ℝ) → 𝕜)
                  ‖z + (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y)‖ :
                𝕜) +
            HSMul.hSMul (α := ℤ) (-1)
              (HMul.hMul (β := 𝕜)
                (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
                  ((𝓚 : (a : ℝ) → 𝕜)
                      ‖HSMul.hSMul (α := ℤ) (-1) z +
                          (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y)‖ :
                    𝕜))
                ((𝓚 : (a : ℝ) → 𝕜)
                    ‖HSMul.hSMul (α := ℤ) (-1) z +
                        (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y)‖ :
                  𝕜))))) =
    4⁻¹ *
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + z‖ : 𝕜) +
          (HSMul.hSMul (α := ℤ) (-1)
              (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + HSMul.hSMul (α := ℤ) (-1) z‖ : 𝕜)
                ((𝓚 : (a : ℝ) → 𝕜) ‖x + HSMul.hSMul (α := ℤ) (-1) z‖ : 𝕜)) +
            (HMul.hMul (β := 𝕜)
                (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
                  ((𝓚 : (a : ℝ) → 𝕜) ‖z + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x‖ : 𝕜))
                ((𝓚 : (a : ℝ) → 𝕜) ‖z + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x‖ : 𝕜) +
              HSMul.hSMul (α := ℤ) (-1)
                (HMul.hMul (β := 𝕜)
                  (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
                    ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul (α := ℤ) (-1) z + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x‖ : 𝕜))
                  ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul (α := ℤ) (-1) z + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x‖ : 𝕜))))) +
      4⁻¹ *
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y + z‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y + z‖ : 𝕜) +
          (HSMul.hSMul (α := ℤ) (-1)
              (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖y + HSMul.hSMul (α := ℤ) (-1) z‖ : 𝕜)
                ((𝓚 : (a : ℝ) → 𝕜) ‖y + HSMul.hSMul (α := ℤ) (-1) z‖ : 𝕜)) +
            (HMul.hMul (β := 𝕜)
                (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
                  ((𝓚 : (a : ℝ) → 𝕜) ‖z + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜))
                ((𝓚 : (a : ℝ) → 𝕜) ‖z + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜) +
              HSMul.hSMul (α := ℤ) (-1)
                (HMul.hMul (β := 𝕜)
                  (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
                    ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul (α := ℤ) (-1) z + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜))
                  ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul (α := ℤ) (-1) z + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜)))))
Tactic: abel_nf at *
Cleared hypotheses: h1, h2, h3, h4, h5, h6, h7, h8