-- 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
⊢ inner_ 𝕜 (x + y) z = inner_ 𝕜 x z + inner_ 𝕜 y z

Tactic:
have H_re := congr(- $(add_left_aux1 x y z) + $(add_left_aux2 x y z)
  + $(add_left_aux3 y z) - $(add_left_aux4 y z))

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‖)
⊢ 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‖)
⊢ inner_ 𝕜 (x + y) z = inner_ 𝕜 x z + inner_ 𝕜 y z

Tactic:
have H_im := congr(- $(add_left_aux5 𝕜 x y z) + $(add_left_aux6 𝕜 x y z)
    + $(add_left_aux7 𝕜 y z) - $(add_left_aux8 𝕜 y z))

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‖)
⊢ 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‖)
⊢ inner_ 𝕜 (x + y) z = inner_ 𝕜 x z + inner_ 𝕜 y z

Tactic:
have H := congr(𝓚 $H_re + I * 𝓚 $H_im)

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‖))
⊢ inner_ 𝕜 (x + y) z = inner_ 𝕜 x z + inner_ 𝕜 y z