-- Mathlib/Analysis/InnerProductSpace/OfNorm.lean
theorem add_left (x y z : E) : inner_ 𝕜 (x + y) z = inner_ 𝕜 x z + inner_ 𝕜 y z

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
H_re :
  -(‖2 • x + y‖ * ‖2 • x + y‖ + ‖2 • z + y‖ * ‖2 • z + y‖) + (‖2 • x + y‖ * ‖2 • x + y‖ + ‖y - 2 • z‖ * ‖y - 2 • z‖) +
        (‖2 • z + y‖ * ‖2 • z + y‖ + ‖y‖ * ‖y‖) -
      (‖y‖ * ‖y‖ + ‖y - 2 • z‖ * ‖y - 2 • z‖) =
    -(2 * (‖x + y + z‖ * ‖x + y + z‖ + ‖x - z‖ * ‖x - z‖)) + 2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖) +
        2 * (‖y + z‖ * ‖y + z‖ + ‖z‖ * ‖z‖) -
      2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)
H_im :
  -(‖I • (2 • x + y)‖ * ‖I • (2 • x + y)‖ + ‖I • y + 2 • z‖ * ‖I • y + 2 • z‖) +
          (‖I • (2 • x + y)‖ * ‖I • (2 • x + y)‖ + ‖I • y - 2 • z‖ * ‖I • y - 2 • z‖) +
        (‖I • y + 2 • z‖ * ‖I • y + 2 • z‖ + ‖I • y‖ * ‖I • y‖) -
      (‖I • y‖ * ‖I • y‖ + ‖I • y - 2 • z‖ * ‖I • y - 2 • z‖) =
    -(2 * (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ + ‖I • x - z‖ * ‖I • x - z‖)) +
          2 * (‖I • (x + y) - z‖ * ‖I • (x + y) - z‖ + ‖I • x + z‖ * ‖I • x + z‖) +
        2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖) -
      2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖)
H :
  𝓚
        (-(‖2 • x + y‖ * ‖2 • x + y‖ + ‖2 • z + y‖ * ‖2 • z + y‖) +
              (‖2 • x + y‖ * ‖2 • x + y‖ + ‖y - 2 • z‖ * ‖y - 2 • z‖) +
            (‖2 • z + y‖ * ‖2 • z + y‖ + ‖y‖ * ‖y‖) -
          (‖y‖ * ‖y‖ + ‖y - 2 • z‖ * ‖y - 2 • z‖)) +
      I *
        𝓚
          (-(‖I • (2 • x + y)‖ * ‖I • (2 • x + y)‖ + ‖I • y + 2 • z‖ * ‖I • y + 2 • z‖) +
                (‖I • (2 • x + y)‖ * ‖I • (2 • x + y)‖ + ‖I • y - 2 • z‖ * ‖I • y - 2 • z‖) +
              (‖I • y + 2 • z‖ * ‖I • y + 2 • z‖ + ‖I • y‖ * ‖I • y‖) -
            (‖I • y‖ * ‖I • y‖ + ‖I • y - 2 • z‖ * ‖I • y - 2 • z‖)) =
    𝓚
        (-(2 * (‖x + y + z‖ * ‖x + y + z‖ + ‖x - z‖ * ‖x - z‖)) + 2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖) +
            2 * (‖y + z‖ * ‖y + z‖ + ‖z‖ * ‖z‖) -
          2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)) +
      I *
        𝓚
          (-(2 * (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ + ‖I • x - z‖ * ‖I • x - z‖)) +
                2 * (‖I • (x + y) - z‖ * ‖I • (x + y) - z‖ + ‖I • x + z‖ * ‖I • x + z‖) +
              2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖) -
            2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖))
⊢ inner_ 𝕜 (x + y) z = inner_ 𝕜 x z + inner_ 𝕜 y z

Tactic:
simp only [inner_, map_add, map_sub, map_neg, map_mul, map_ofNat] at H ⊢

Result:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
H_re :
  -(‖2 • x + y‖ * ‖2 • x + y‖ + ‖2 • z + y‖ * ‖2 • z + y‖) + (‖2 • x + y‖ * ‖2 • x + y‖ + ‖y - 2 • z‖ * ‖y - 2 • z‖) +
        (‖2 • z + y‖ * ‖2 • z + y‖ + ‖y‖ * ‖y‖) -
      (‖y‖ * ‖y‖ + ‖y - 2 • z‖ * ‖y - 2 • z‖) =
    -(2 * (‖x + y + z‖ * ‖x + y + z‖ + ‖x - z‖ * ‖x - z‖)) + 2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖) +
        2 * (‖y + z‖ * ‖y + z‖ + ‖z‖ * ‖z‖) -
      2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)
H_im :
  -(‖I • (2 • x + y)‖ * ‖I • (2 • x + y)‖ + ‖I • y + 2 • z‖ * ‖I • y + 2 • z‖) +
          (‖I • (2 • x + y)‖ * ‖I • (2 • x + y)‖ + ‖I • y - 2 • z‖ * ‖I • y - 2 • z‖) +
        (‖I • y + 2 • z‖ * ‖I • y + 2 • z‖ + ‖I • y‖ * ‖I • y‖) -
      (‖I • y‖ * ‖I • y‖ + ‖I • y - 2 • z‖ * ‖I • y - 2 • z‖) =
    -(2 * (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ + ‖I • x - z‖ * ‖I • x - z‖)) +
          2 * (‖I • (x + y) - z‖ * ‖I • (x + y) - z‖ + ‖I • x + z‖ * ‖I • x + z‖) +
        2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖) -
      2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖)
H :
  -(𝓚 ‖2 • x + y‖ * 𝓚 ‖2 • x + y‖ + 𝓚 ‖2 • z + y‖ * 𝓚 ‖2 • z + y‖) +
            (𝓚 ‖2 • x + y‖ * 𝓚 ‖2 • x + y‖ + 𝓚 ‖y - 2 • z‖ * 𝓚 ‖y - 2 • z‖) +
          (𝓚 ‖2 • z + y‖ * 𝓚 ‖2 • z + y‖ + 𝓚 ‖y‖ * 𝓚 ‖y‖) -
        (𝓚 ‖y‖ * 𝓚 ‖y‖ + 𝓚 ‖y - 2 • z‖ * 𝓚 ‖y - 2 • z‖) +
      I *
        (-(𝓚 ‖I • (2 • x + y)‖ * 𝓚 ‖I • (2 • x + y)‖ + 𝓚 ‖I • y + 2 • z‖ * 𝓚 ‖I • y + 2 • z‖) +
              (𝓚 ‖I • (2 • x + y)‖ * 𝓚 ‖I • (2 • x + y)‖ + 𝓚 ‖I • y - 2 • z‖ * 𝓚 ‖I • y - 2 • z‖) +
            (𝓚 ‖I • y + 2 • z‖ * 𝓚 ‖I • y + 2 • z‖ + 𝓚 ‖I • y‖ * 𝓚 ‖I • y‖) -
          (𝓚 ‖I • y‖ * 𝓚 ‖I • y‖ + 𝓚 ‖I • y - 2 • z‖ * 𝓚 ‖I • y - 2 • z‖)) =
    -(2 * (𝓚 ‖x + y + z‖ * 𝓚 ‖x + y + z‖ + 𝓚 ‖x - z‖ * 𝓚 ‖x - z‖)) +
            2 * (𝓚 ‖x + y - z‖ * 𝓚 ‖x + y - z‖ + 𝓚 ‖x + z‖ * 𝓚 ‖x + z‖) +
          2 * (𝓚 ‖y + z‖ * 𝓚 ‖y + z‖ + 𝓚 ‖z‖ * 𝓚 ‖z‖) -
        2 * (𝓚 ‖y - z‖ * 𝓚 ‖y - z‖ + 𝓚 ‖z‖ * 𝓚 ‖z‖) +
      I *
        (-(2 * (𝓚 ‖I • (x + y) + z‖ * 𝓚 ‖I • (x + y) + z‖ + 𝓚 ‖I • x - z‖ * 𝓚 ‖I • x - z‖)) +
              2 * (𝓚 ‖I • (x + y) - z‖ * 𝓚 ‖I • (x + y) - z‖ + 𝓚 ‖I • x + z‖ * 𝓚 ‖I • x + z‖) +
            2 * (𝓚 ‖I • y + z‖ * 𝓚 ‖I • y + z‖ + 𝓚 ‖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 + y) + z‖ * 𝓚 ‖I • (x + y) + z‖ -
        I * 𝓚 ‖I • (x + y) - z‖ * 𝓚 ‖I • (x + 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‖)