-- Mathlib/Analysis/InnerProductSpace/Symmetric.lean
theorem isSymmetric_iff_inner_map_self_real (T : V →ₗ[ℂ] V) :
    IsSymmetric T ↔ ∀ v : V, conj ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ

Proof state:
case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
x y : V
⊢ (⟪T (x + y), x + y⟫_ℂ - ⟪T (x - y), x - y⟫_ℂ - Complex.I * ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ +
        Complex.I * ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ) /
      4 =
    (⟪T (x + y), x + y⟫_ℂ - ⟪T (x - y), x - y⟫_ℂ + ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ * -Complex.I -
        ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ * -Complex.I) /
      (starRingEnd ℂ) 4

Tactic:
norm_num

Result:
case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
x y : V
⊢ (⟪T x + T y, x + y⟫_ℂ - ⟪T x - T y, x - y⟫_ℂ - Complex.I * ⟪T x + Complex.I • T y, x + Complex.I • y⟫_ℂ +
        Complex.I * ⟪T x - Complex.I • T y, x - Complex.I • y⟫_ℂ) /
      4 =
    (⟪T x + T y, x + y⟫_ℂ - ⟪T x - T y, x - y⟫_ℂ + -(⟪T x + Complex.I • T y, x + Complex.I • y⟫_ℂ * Complex.I) +
        ⟪T x - Complex.I • T y, x - Complex.I • y⟫_ℂ * Complex.I) /
      4

Proof state:
case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
x y : V
⊢ ⟪T x, y⟫_ℂ =
    (starRingEnd ℂ)
      ((⟪T (x + y), x + y⟫_ℂ - ⟪T (x - y), x - y⟫_ℂ + Complex.I * ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ -
          Complex.I * ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ) /
        4)

Tactic:
simp only [starRingEnd_apply, star_div₀, star_sub, star_add, star_mul]

Result:
case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
x y : V
⊢ ⟪T x, y⟫_ℂ =
    (star ⟪T (x + y), x + y⟫_ℂ - star ⟪T (x - y), x - y⟫_ℂ +
          star ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ * star Complex.I -
        star ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ * star Complex.I) /
      star 4

Proof state:
case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
x y : V
⊢ ⟪T x, y⟫_ℂ =
    ((starRingEnd ℂ) ⟪T (x + y), x + y⟫_ℂ - (starRingEnd ℂ) ⟪T (x - y), x - y⟫_ℂ +
          (starRingEnd ℂ) ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ * (starRingEnd ℂ) Complex.I -
        (starRingEnd ℂ) ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ * (starRingEnd ℂ) Complex.I) /
      (starRingEnd ℂ) 4

Tactic:
rw [h (x + y), h (x - y), h (x + Complex.I • y), h (x - Complex.I • y)]

Result:
case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
x y : V
⊢ ⟪T x, y⟫_ℂ =
    (⟪T (x + y), x + y⟫_ℂ - ⟪T (x - y), x - y⟫_ℂ +
          ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ * (starRingEnd ℂ) Complex.I -
        ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ * (starRingEnd ℂ) Complex.I) /
      (starRingEnd ℂ) 4

Proof state:
case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
x y : V
⊢ ⟪T x, y⟫_ℂ =
    (star ⟪T (x + y), x + y⟫_ℂ - star ⟪T (x - y), x - y⟫_ℂ +
          star ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ * star Complex.I -
        star ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ * star Complex.I) /
      star 4

Tactic:
simp only [← starRingEnd_apply]

Result:
case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
x y : V
⊢ ⟪T x, y⟫_ℂ =
    ((starRingEnd ℂ) ⟪T (x + y), x + y⟫_ℂ - (starRingEnd ℂ) ⟪T (x - y), x - y⟫_ℂ +
          (starRingEnd ℂ) ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ * (starRingEnd ℂ) Complex.I -
        (starRingEnd ℂ) ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ * (starRingEnd ℂ) Complex.I) /
      (starRingEnd ℂ) 4

Proof state:
case mp
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ T.IsSymmetric → ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ

Tactic:
intro hT v

Result:
case mp
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : T.IsSymmetric
v : V
⊢ (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ

Proof state:
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ T.IsSymmetric ↔ ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ

Tactic:
constructor

Result:
case mp
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ T.IsSymmetric → ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ

case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ (∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ) → T.IsSymmetric

Proof state:
case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
x y : V
⊢ ⟪T x, y⟫_ℂ =
    (⟪T (x + y), x + y⟫_ℂ - ⟪T (x - y), x - y⟫_ℂ + ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ * -Complex.I -
        ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ * -Complex.I) /
      (starRingEnd ℂ) 4

Tactic:
rw [inner_map_polarization']

Result:
case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
x y : V
⊢ (⟪T (x + y), x + y⟫_ℂ - ⟪T (x - y), x - y⟫_ℂ - Complex.I * ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ +
        Complex.I * ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ) /
      4 =
    (⟪T (x + y), x + y⟫_ℂ - ⟪T (x - y), x - y⟫_ℂ + ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ * -Complex.I -
        ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ * -Complex.I) /
      (starRingEnd ℂ) 4

Proof state:
case mp
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : T.IsSymmetric
v : V
⊢ (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ

Tactic:
apply IsSymmetric.conj_inner_sym hT

Result:
no goals

Proof state:
case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
x y : V
⊢ ⟪T x, y⟫_ℂ = (starRingEnd ℂ) ⟪T y, x⟫_ℂ

Tactic:
rw [inner_map_polarization T x y]

Result:
case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
x y : V
⊢ ⟪T x, y⟫_ℂ =
    (starRingEnd ℂ)
      ((⟪T (x + y), x + y⟫_ℂ - ⟪T (x - y), x - y⟫_ℂ + Complex.I * ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ -
          Complex.I * ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ) /
        4)

Proof state:
case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
x y : V
⊢ ⟪T x, y⟫_ℂ =
    (⟪T (x + y), x + y⟫_ℂ - ⟪T (x - y), x - y⟫_ℂ +
          ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ * (starRingEnd ℂ) Complex.I -
        ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ * (starRingEnd ℂ) Complex.I) /
      (starRingEnd ℂ) 4

Tactic:
simp only [Complex.conj_I]

Result:
case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
x y : V
⊢ ⟪T x, y⟫_ℂ =
    (⟪T (x + y), x + y⟫_ℂ - ⟪T (x - y), x - y⟫_ℂ + ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ * -Complex.I -
        ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ * -Complex.I) /
      (starRingEnd ℂ) 4