-- Mathlib/Analysis/InnerProductSpace/Symmetric.lean
theorem IsSymmetric.inner_map_polarization {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (x y : E) :
    ⟪T x, y⟫ =
      (⟪T (x + y), x + y⟫ - ⟪T (x - y), x - y⟫ - I * ⟪T (x + (I : 𝕜) • y), x + (I : 𝕜) • y⟫ +
          I * ⟪T (x - (I : 𝕜) • y), x - (I : 𝕜) • y⟫) /
        4

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
⊢ inner (T x) y =
    (inner (T (x + y)) (x + y) - inner (T (x - y)) (x - y) - I * inner (T (x + I • y)) (x + I • y) +
        I * inner (T (x - I • y)) (x - I • y)) /
      4

Tactic:
rcases@I_mul_I_ax 𝕜 _ with (h | h)

Result:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : I = 0
⊢ inner (T x) y =
    (inner (T (x + y)) (x + y) - inner (T (x - y)) (x - y) - I * inner (T (x + I • y)) (x + I • y) +
        I * inner (T (x - I • y)) (x - I • y)) /
      4

case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : I * I = -1
⊢ inner (T x) y =
    (inner (T (x + y)) (x + y) - inner (T (x - y)) (x - y) - I * inner (T (x + I • y)) (x + I • y) +
        I * inner (T (x - I • y)) (x - I • y)) /
      4

Proof state:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : I * I = -1
⊢ inner (T x) y =
    (inner (T x) x + inner (T x) y + (inner (T y) x + inner (T y) y) -
          (inner (T x) x - (inner (T x) y + (inner (T y) x - inner (T y) y)) +
            (I * inner (T x) x + -inner (T x) y + (inner (T y) x + I * inner (T y) y))) +
        (I * inner (T x) x - (-inner (T x) y + (inner (T y) x - I * inner (T y) y)))) /
      4

Tactic:
ring

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : I = 0
this : ↑(re (inner (T y) x)) = inner (T y) x
⊢ (starRingEnd 𝕜) (inner (T y) x) =
    (inner x (T x) + (starRingEnd 𝕜) (inner (T y) x) + (inner (T y) x + inner (T y) y) -
        (inner x (T x) - (starRingEnd 𝕜) (inner (T y) x) - (inner (T y) x - inner (T y) y))) /
      4

Tactic:
rw [conj_eq_iff_re.mpr this]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : I = 0
this : ↑(re (inner (T y) x)) = inner (T y) x
⊢ inner (T y) x =
    (inner x (T x) + inner (T y) x + (inner (T y) x + inner (T y) y) -
        (inner x (T x) - inner (T y) x - (inner (T y) x - inner (T y) y))) /
      4

Proof state:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : I = 0
⊢ (starRingEnd 𝕜) (inner (T y) x) =
    (inner x (T x) + (starRingEnd 𝕜) (inner (T y) x) + (inner (T y) x + inner (T y) y) -
        (inner x (T x) - (starRingEnd 𝕜) (inner (T y) x) - (inner (T y) x - inner (T y) y))) /
      4

Tactic:
suffices (re ⟪T y, x⟫ : 𝕜) = ⟪T y, x⟫ by
  rw [conj_eq_iff_re.mpr this]
  ring

Result:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : I = 0
⊢ ↑(re (inner (T y) x)) = inner (T y) x

Proof state:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : I = 0
⊢ ↑(re (inner (T y) x)) = inner (T y) x

Tactic:
rw [← re_add_im ⟪T y, x⟫]

Result:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : I = 0
⊢ ↑(re (↑(re (inner (T y) x)) + ↑(im (inner (T y) x)) * I)) = ↑(re (inner (T y) x)) + ↑(im (inner (T y) x)) * I

Proof state:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : I * I = -1
⊢ inner (T x) y =
    (inner (T (x + y)) (x + y) - inner (T (x - y)) (x - y) - I * inner (T (x + I • y)) (x + I • y) +
        I * inner (T (x - I • y)) (x - I • y)) /
      4

Tactic:
simp_rw [map_add, map_sub, inner_add_left, inner_add_right, inner_sub_left, inner_sub_right,
  LinearMap.map_smul, inner_smul_left, inner_smul_right, RCLike.conj_I, mul_add, mul_sub,
  sub_sub, ← mul_assoc, mul_neg, h, neg_neg, one_mul, neg_one_mul]

Result:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : I * I = -1
⊢ inner (T x) y =
    (inner (T x) x + inner (T x) y + (inner (T y) x + inner (T y) y) -
          (inner (T x) x - (inner (T x) y + (inner (T y) x - inner (T y) y)) +
            (I * inner (T x) x + -inner (T x) y + (inner (T y) x + I * inner (T y) y))) +
        (I * inner (T x) x - (-inner (T x) y + (inner (T y) x - I * inner (T y) y)))) /
      4

Proof state:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : I = 0
⊢ ↑(re (↑(re (inner (T y) x)) + ↑(im (inner (T y) x)) * I)) = ↑(re (inner (T y) x)) + ↑(im (inner (T y) x)) * I

Tactic:
simp_rw [h, mul_zero, add_zero]

Result:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : I = 0
⊢ ↑(re ↑(re (inner (T y) x))) = ↑(re (inner (T y) x))

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : I = 0
this : ↑(re (inner (T y) x)) = inner (T y) x
⊢ inner (T y) x =
    (inner x (T x) + inner (T y) x + (inner (T y) x + inner (T y) y) -
        (inner x (T x) - inner (T y) x - (inner (T y) x - inner (T y) y))) /
      4

Tactic:
ring

Result:
no goals

Proof state:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : I = 0
⊢ ↑(re ↑(re (inner (T y) x))) = ↑(re (inner (T y) x))

Tactic:
norm_cast

Result:
no goals

Proof state:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : I = 0
⊢ inner (T x) y =
    (inner (T (x + y)) (x + y) - inner (T (x - y)) (x - y) - I * inner (T (x + I • y)) (x + I • y) +
        I * inner (T (x - I • y)) (x - I • y)) /
      4

Tactic:
simp_rw [h, zero_mul, sub_zero, add_zero, map_add, map_sub, inner_add_left,
  inner_add_right, inner_sub_left, inner_sub_right, hT x, ← inner_conj_symm x (T y)]

Result:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : I = 0
⊢ (starRingEnd 𝕜) (inner (T y) x) =
    (inner x (T x) + (starRingEnd 𝕜) (inner (T y) x) + (inner (T y) x + inner (T y) y) -
        (inner x (T x) - (starRingEnd 𝕜) (inner (T y) x) - (inner (T y) x - inner (T y) y))) /
      4