case mp
𝕜 : Type ?u.76973
E : Type ?u.76976
E' : Type ?u.76979
F : Type ?u.76982
G : Type ?u.76985
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ IsSymmetric T → ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v

case mpr
𝕜 : Type ?u.76973
E : Type ?u.76976
E' : Type ?u.76979
F : Type ?u.76982
G : Type ?u.76985
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ (∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v) → IsSymmetric T
𝕜 : Type ?u.76973
E : Type ?u.76976
E' : Type ?u.76979
F : Type ?u.76982
G : Type ?u.76985
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ IsSymmetric T ↔ ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
constructor
case mp
𝕜 : Type ?u.76973
E : Type ?u.76976
E' : Type ?u.76979
F : Type ?u.76982
G : Type ?u.76985
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : IsSymmetric T
v : V
⊢ ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
case mp
𝕜 : Type ?u.76973
E : Type ?u.76976
E' : Type ?u.76979
F : Type ?u.76982
G : Type ?u.76985
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ IsSymmetric T → ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
intro hT v
no goals
case mp
𝕜 : Type ?u.76973
E : Type ?u.76976
E' : Type ?u.76979
F : Type ?u.76982
G : Type ?u.76985
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : IsSymmetric T
v : V
⊢ ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
apply IsSymmetric.conj_inner_sym hT
case mpr
𝕜 : Type ?u.76973
E : Type ?u.76976
E' : Type ?u.76979
F : Type ?u.76982
G : Type ?u.76985
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
x y : V
⊢ inner (↑T x) y = inner x (↑T y)
case mpr
𝕜 : Type ?u.76973
E : Type ?u.76976
E' : Type ?u.76979
F : Type ?u.76982
G : Type ?u.76985
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ (∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v) → IsSymmetric T
intro h x y
case mpr
𝕜 : Type ?u.76973
E : Type ?u.76976
E' : Type ?u.76979
F : Type ?u.76982
G : Type ?u.76985
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
x y : V
⊢ inner (↑T x) y = ↑(starRingEnd ℂ) (inner (↑T y) x)
case mpr
𝕜 : Type ?u.76973
E : Type ?u.76976
E' : Type ?u.76979
F : Type ?u.76982
G : Type ?u.76985
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
x y : V
⊢ inner (↑T x) y = inner x (↑T y)
rw [← inner_conj_symm x (T y)]
case mpr
𝕜 : Type ?u.76973
E : Type ?u.76976
E' : Type ?u.76979
F : Type ?u.76982
G : Type ?u.76985
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
x y : V
⊢ inner (↑T x) y =
    ↑(starRingEnd ℂ)
      ((inner (↑T (x + y)) (x + y) - inner (↑T (x - y)) (x - y) +
            Complex.I * inner (↑T (x + Complex.I • y)) (x + Complex.I • y) -
          Complex.I * inner (↑T (x - Complex.I • y)) (x - Complex.I • y)) /
        4)
case mpr
𝕜 : Type ?u.76973
E : Type ?u.76976
E' : Type ?u.76979
F : Type ?u.76982
G : Type ?u.76985
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
x y : V
⊢ inner (↑T x) y = ↑(starRingEnd ℂ) (inner (↑T y) x)
rw [inner_map_polarization T x y]
case mpr
𝕜 : Type ?u.76973
E : Type ?u.76976
E' : Type ?u.76979
F : Type ?u.76982
G : Type ?u.76985
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
x y : V
⊢ inner (↑T x) y =
    (star (inner (↑T (x + y)) (x + y)) - star (inner (↑T (x - y)) (x - y)) +
          star (inner (↑T (x + Complex.I • y)) (x + Complex.I • y)) * star Complex.I -
        star (inner (↑T (x - Complex.I • y)) (x - Complex.I • y)) * star Complex.I) /
      star 4
case mpr
𝕜 : Type ?u.76973
E : Type ?u.76976
E' : Type ?u.76979
F : Type ?u.76982
G : Type ?u.76985
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
x y : V
⊢ inner (↑T x) y =
    ↑(starRingEnd ℂ)
      ((inner (↑T (x + y)) (x + y) - inner (↑T (x - y)) (x - y) +
            Complex.I * inner (↑T (x + Complex.I • y)) (x + Complex.I • y) -
          Complex.I * inner (↑T (x - Complex.I • y)) (x - Complex.I • y)) /
        4)
simp only [starRingEnd_apply, star_div', star_sub, star_add, star_mul]
case mpr
𝕜 : Type ?u.76973
E : Type ?u.76976
E' : Type ?u.76979
F : Type ?u.76982
G : Type ?u.76985
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
x y : V
⊢ inner (↑T x) y =
    (↑(starRingEnd ℂ) (inner (↑T (x + y)) (x + y)) - ↑(starRingEnd ℂ) (inner (↑T (x - y)) (x - y)) +
          ↑(starRingEnd ℂ) (inner (↑T (x + Complex.I • y)) (x + Complex.I • y)) * ↑(starRingEnd ℂ) Complex.I -
        ↑(starRingEnd ℂ) (inner (↑T (x - Complex.I • y)) (x - Complex.I • y)) * ↑(starRingEnd ℂ) Complex.I) /
      ↑(starRingEnd ℂ) 4
case mpr
𝕜 : Type ?u.76973
E : Type ?u.76976
E' : Type ?u.76979
F : Type ?u.76982
G : Type ?u.76985
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
x y : V
⊢ inner (↑T x) y =
    (star (inner (↑T (x + y)) (x + y)) - star (inner (↑T (x - y)) (x - y)) +
          star (inner (↑T (x + Complex.I • y)) (x + Complex.I • y)) * star Complex.I -
        star (inner (↑T (x - Complex.I • y)) (x - Complex.I • y)) * star Complex.I) /
      star 4
simp only [← starRingEnd_apply]
case mpr
𝕜 : Type ?u.76973
E : Type ?u.76976
E' : Type ?u.76979
F : Type ?u.76982
G : Type ?u.76985
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
x y : V
⊢ inner (↑T x) y =
    (inner (↑T (x + y)) (x + y) - inner (↑T (x - y)) (x - y) +
          inner (↑T (x + Complex.I • y)) (x + Complex.I • y) * ↑(starRingEnd ℂ) Complex.I -
        inner (↑T (x - Complex.I • y)) (x - Complex.I • y) * ↑(starRingEnd ℂ) Complex.I) /
      ↑(starRingEnd ℂ) 4
case mpr
𝕜 : Type ?u.76973
E : Type ?u.76976
E' : Type ?u.76979
F : Type ?u.76982
G : Type ?u.76985
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
x y : V
⊢ inner (↑T x) y =
    (↑(starRingEnd ℂ) (inner (↑T (x + y)) (x + y)) - ↑(starRingEnd ℂ) (inner (↑T (x - y)) (x - y)) +
          ↑(starRingEnd ℂ) (inner (↑T (x + Complex.I • y)) (x + Complex.I • y)) * ↑(starRingEnd ℂ) Complex.I -
        ↑(starRingEnd ℂ) (inner (↑T (x - Complex.I • y)) (x - Complex.I • y)) * ↑(starRingEnd ℂ) Complex.I) /
      ↑(starRingEnd ℂ) 4
rw [h (x + y), h (x - y), h (x + Complex.I • y), h (x - Complex.I • y)]
case mpr
𝕜 : Type ?u.76973
E : Type ?u.76976
E' : Type ?u.76979
F : Type ?u.76982
G : Type ?u.76985
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
x y : V
⊢ inner (↑T x) y =
    (inner (↑T (x + y)) (x + y) - inner (↑T (x - y)) (x - y) +
          inner (↑T (x + Complex.I • y)) (x + Complex.I • y) * -Complex.I -
        inner (↑T (x - Complex.I • y)) (x - Complex.I • y) * -Complex.I) /
      ↑(starRingEnd ℂ) 4
case mpr
𝕜 : Type ?u.76973
E : Type ?u.76976
E' : Type ?u.76979
F : Type ?u.76982
G : Type ?u.76985
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
x y : V
⊢ inner (↑T x) y =
    (inner (↑T (x + y)) (x + y) - inner (↑T (x - y)) (x - y) +
          inner (↑T (x + Complex.I • y)) (x + Complex.I • y) * ↑(starRingEnd ℂ) Complex.I -
        inner (↑T (x - Complex.I • y)) (x - Complex.I • y) * ↑(starRingEnd ℂ) Complex.I) /
      ↑(starRingEnd ℂ) 4
simp only [Complex.conj_I]
case mpr
𝕜 : Type ?u.76973
E : Type ?u.76976
E' : Type ?u.76979
F : Type ?u.76982
G : Type ?u.76985
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
x y : V
⊢ (inner (↑T (x + y)) (x + y) - inner (↑T (x - y)) (x - y) -
          Complex.I * inner (↑T (x + Complex.I • y)) (x + Complex.I • y) +
        Complex.I * inner (↑T (x - Complex.I • y)) (x - Complex.I • y)) /
      4 =
    (inner (↑T (x + y)) (x + y) - inner (↑T (x - y)) (x - y) +
          inner (↑T (x + Complex.I • y)) (x + Complex.I • y) * -Complex.I -
        inner (↑T (x - Complex.I • y)) (x - Complex.I • y) * -Complex.I) /
      ↑(starRingEnd ℂ) 4
case mpr
𝕜 : Type ?u.76973
E : Type ?u.76976
E' : Type ?u.76979
F : Type ?u.76982
G : Type ?u.76985
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
x y : V
⊢ inner (↑T x) y =
    (inner (↑T (x + y)) (x + y) - inner (↑T (x - y)) (x - y) +
          inner (↑T (x + Complex.I • y)) (x + Complex.I • y) * -Complex.I -
        inner (↑T (x - Complex.I • y)) (x - Complex.I • y) * -Complex.I) /
      ↑(starRingEnd ℂ) 4
rw [inner_map_polarization']
case mpr
𝕜 : Type ?u.76973
E : Type ?u.76976
E' : Type ?u.76979
F : Type ?u.76982
G : Type ?u.76985
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
x y : V
⊢ (inner (↑T x + ↑T y) (x + y) - inner (↑T x - ↑T y) (x - y) -
          Complex.I * inner (↑T x + Complex.I • ↑T y) (x + Complex.I • y) +
        Complex.I * inner (↑T x - Complex.I • ↑T y) (x - Complex.I • y)) /
      4 =
    (inner (↑T x + ↑T y) (x + y) - inner (↑T x - ↑T y) (x - y) +
          -(inner (↑T x + Complex.I • ↑T y) (x + Complex.I • y) * Complex.I) +
        inner (↑T x - Complex.I • ↑T y) (x - Complex.I • y) * Complex.I) /
      4
case mpr
𝕜 : Type ?u.76973
E : Type ?u.76976
E' : Type ?u.76979
F : Type ?u.76982
G : Type ?u.76985
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
x y : V
⊢ (inner (↑T (x + y)) (x + y) - inner (↑T (x - y)) (x - y) -
          Complex.I * inner (↑T (x + Complex.I • y)) (x + Complex.I • y) +
        Complex.I * inner (↑T (x - Complex.I • y)) (x - Complex.I • y)) /
      4 =
    (inner (↑T (x + y)) (x + y) - inner (↑T (x - y)) (x - y) +
          inner (↑T (x + Complex.I • y)) (x + Complex.I • y) * -Complex.I -
        inner (↑T (x - Complex.I • y)) (x - Complex.I • y) * -Complex.I) /
      ↑(starRingEnd ℂ) 4
norm_num
no goals
case mpr
𝕜 : Type ?u.76973
E : Type ?u.76976
E' : Type ?u.76979
F : Type ?u.76982
G : Type ?u.76985
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace ℝ E'
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
x y : V
⊢ (inner (↑T x + ↑T y) (x + y) - inner (↑T x - ↑T y) (x - y) -
          Complex.I * inner (↑T x + Complex.I • ↑T y) (x + Complex.I • y) +
        Complex.I * inner (↑T x - Complex.I • ↑T y) (x - Complex.I • y)) /
      4 =
    (inner (↑T x + ↑T y) (x + y) - inner (↑T x - ↑T y) (x - y) +
          -(inner (↑T x + Complex.I • ↑T y) (x + Complex.I • y) * Complex.I) +
        inner (↑T x - Complex.I • ↑T y) (x - Complex.I • y) * Complex.I) /
      4
ring