Module: Mathlib.Analysis.InnerProductSpace.OfNorm

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : 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 :
  𝓚 ‖I • x + I • y + z + (I • x - z)‖ * 𝓚 ‖I • x + I • y + z + (I • x - z)‖ +
      𝓚 ‖I • x + I • y + z - (I • x - z)‖ * 𝓚 ‖I • x + I • y + z - (I • x - z)‖ =
    2 * (𝓚 ‖I • x + I • y + z‖ * 𝓚 ‖I • x + I • y + z‖ + 𝓚 ‖I • x - z‖ * 𝓚 ‖I • x - z‖)
h6 :
  𝓚 ‖I • x + I • y - z + (I • x + z)‖ * 𝓚 ‖I • x + I • y - z + (I • x + z)‖ +
      𝓚 ‖I • x + I • y - z - (I • x + z)‖ * 𝓚 ‖I • x + I • y - z - (I • x + z)‖ =
    2 * (𝓚 ‖I • x + I • y - z‖ * 𝓚 ‖I • x + I • y - z‖ + 𝓚 ‖I • x + z‖ * 𝓚 ‖I • x + z‖)
h7 :
  𝓚 ‖I • y + z + z‖ * 𝓚 ‖I • y + z + z‖ + 𝓚 ‖I • y + z - z‖ * 𝓚 ‖I • y + z - z‖ =
    2 * (𝓚 ‖I • y + z‖ * 𝓚 ‖I • y + z‖ + 𝓚 ‖z‖ * 𝓚 ‖z‖)
h8 :
  𝓚 ‖I • y - z + z‖ * 𝓚 ‖I • y - z + z‖ + 𝓚 ‖I • y - z - z‖ * 𝓚 ‖I • y - z - z‖ =
    2 * (𝓚 ‖I • y - z‖ * 𝓚 ‖I • y - z‖ + 𝓚 ‖z‖ * 𝓚 ‖z‖)
⊢ 4⁻¹ *
      (𝓚 ‖x + y + z‖ * 𝓚 ‖x + y + z‖ - 𝓚 ‖x + y - z‖ * 𝓚 ‖x + y - z‖ +
          I * 𝓚 ‖I • x + I • y + z‖ * 𝓚 ‖I • x + I • y + z‖ -
        I * 𝓚 ‖I • x + I • y - z‖ * 𝓚 ‖I • x + I • y - z‖) =
    4⁻¹ *
        (𝓚 ‖x + z‖ * 𝓚 ‖x + z‖ - 𝓚 ‖x - z‖ * 𝓚 ‖x - z‖ + I * 𝓚 ‖I • x + z‖ * 𝓚 ‖I • x + z‖ -
          I * 𝓚 ‖I • x - z‖ * 𝓚 ‖I • x - z‖) +
      4⁻¹ *
        (𝓚 ‖y + z‖ * 𝓚 ‖y + z‖ - 𝓚 ‖y - z‖ * 𝓚 ‖y - z‖ + I * 𝓚 ‖I • y + z‖ * 𝓚 ‖I • y + z‖ -
          I * 𝓚 ‖I • y - z‖ * 𝓚 ‖I • y - z‖)

Tactic:
abel_nf at *

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h8 :
  𝓚 ‖I • y‖ * 𝓚 ‖I • y‖ + 𝓚 ‖-2 • z + I • y‖ * 𝓚 ‖-2 • z + I • y‖ =
    2 * (𝓚 ‖-1 • z + I • y‖ * 𝓚 ‖-1 • z + I • y‖ + 𝓚 ‖z‖ * 𝓚 ‖z‖)
h7 : 𝓚 ‖I • y‖ * 𝓚 ‖I • y‖ + 𝓚 ‖2 • z + I • y‖ * 𝓚 ‖2 • z + I • y‖ = 2 * (𝓚 ‖z‖ * 𝓚 ‖z‖ + 𝓚 ‖z + I • y‖ * 𝓚 ‖z + I • y‖)
h6 :
  𝓚 ‖-2 • z + I • y‖ * 𝓚 ‖-2 • z + I • y‖ + 𝓚 ‖2 • I • x + I • y‖ * 𝓚 ‖2 • I • x + I • y‖ =
    2 * (𝓚 ‖-1 • z + (I • x + I • y)‖ * 𝓚 ‖-1 • z + (I • x + I • y)‖ + 𝓚 ‖z + I • x‖ * 𝓚 ‖z + I • x‖)
h5 :
  𝓚 ‖2 • z + I • y‖ * 𝓚 ‖2 • z + I • y‖ + 𝓚 ‖2 • I • x + I • y‖ * 𝓚 ‖2 • I • x + I • y‖ =
    2 * (𝓚 ‖z + (I • x + I • y)‖ * 𝓚 ‖z + (I • x + I • y)‖ + 𝓚 ‖-1 • z + I • x‖ * 𝓚 ‖-1 • z + I • x‖)
h4 : 𝓚 ‖y‖ * 𝓚 ‖y‖ + 𝓚 ‖y + -2 • z‖ * 𝓚 ‖y + -2 • z‖ = 2 * (𝓚 ‖y + -1 • z‖ * 𝓚 ‖y + -1 • z‖ + 𝓚 ‖z‖ * 𝓚 ‖z‖)
h3 : 𝓚 ‖y‖ * 𝓚 ‖y‖ + 𝓚 ‖y + 2 • z‖ * 𝓚 ‖y + 2 • z‖ = 2 * (𝓚 ‖y + z‖ * 𝓚 ‖y + z‖ + 𝓚 ‖z‖ * 𝓚 ‖z‖)
h2 :
  𝓚 ‖y + -2 • z‖ * 𝓚 ‖y + -2 • z‖ + 𝓚 ‖2 • x + y‖ * 𝓚 ‖2 • x + y‖ =
    2 * (𝓚 ‖x + (y + -1 • z)‖ * 𝓚 ‖x + (y + -1 • z)‖ + 𝓚 ‖x + z‖ * 𝓚 ‖x + z‖)
h1 :
  𝓚 ‖y + 2 • z‖ * 𝓚 ‖y + 2 • z‖ + 𝓚 ‖2 • x + y‖ * 𝓚 ‖2 • x + y‖ =
    2 * (𝓚 ‖x + (y + z)‖ * 𝓚 ‖x + (y + z)‖ + 𝓚 ‖x + -1 • z‖ * 𝓚 ‖x + -1 • z‖)
⊢ 4⁻¹ *
      (𝓚 ‖x + (y + z)‖ * 𝓚 ‖x + (y + z)‖ +
        (-1 • (𝓚 ‖x + (y + -1 • z)‖ * 𝓚 ‖x + (y + -1 • z)‖) +
          (I * 𝓚 ‖z + (I • x + I • y)‖ * 𝓚 ‖z + (I • x + I • y)‖ +
            -1 • (I * 𝓚 ‖-1 • z + (I • x + I • y)‖ * 𝓚 ‖-1 • z + (I • x + I • y)‖)))) =
    4⁻¹ *
        (𝓚 ‖x + z‖ * 𝓚 ‖x + z‖ +
          (-1 • (𝓚 ‖x + -1 • z‖ * 𝓚 ‖x + -1 • z‖) +
            (I * 𝓚 ‖z + I • x‖ * 𝓚 ‖z + I • x‖ + -1 • (I * 𝓚 ‖-1 • z + I • x‖ * 𝓚 ‖-1 • z + I • x‖)))) +
      4⁻¹ *
        (𝓚 ‖y + z‖ * 𝓚 ‖y + z‖ +
          (-1 • (𝓚 ‖y + -1 • z‖ * 𝓚 ‖y + -1 • z‖) +
            (I * 𝓚 ‖z + I • y‖ * 𝓚 ‖z + I • y‖ + -1 • (I * 𝓚 ‖-1 • z + I • y‖ * 𝓚 ‖-1 • z + I • y‖))))