[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
⊢ ↑(starRingEnd 𝕜) (inner (↑T x) y) = inner (↑T y) x
[PROOFSTEP]
rw [hT x y, inner_conj_symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
T S : E →ₗ[𝕜] E
hT : IsSymmetric T
hS : IsSymmetric S
⊢ IsSymmetric (T + S)
[PROOFSTEP]
intro x y
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
T S : E →ₗ[𝕜] E
hT : IsSymmetric T
hS : IsSymmetric S
x y : E
⊢ inner (↑(T + S) x) y = inner x (↑(T + S) y)
[PROOFSTEP]
rw [LinearMap.add_apply, inner_add_left, hT x y, hS x y, ← inner_add_right]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
T S : E →ₗ[𝕜] E
hT : IsSymmetric T
hS : IsSymmetric S
x y : E
⊢ inner x (↑T y + ↑S y) = inner x (↑(T + S) y)
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
⊢ Continuous ↑T
[PROOFSTEP]
refine' T.continuous_of_seq_closed_graph fun u x y hu hTu => _
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
⊢ y = ↑T x
[PROOFSTEP]
rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
⊢ inner (y - ↑T x) (y - ↑T x) = 0
[PROOFSTEP]
have hlhs : ∀ k : ℕ, ⟪T (u k) - T x, y - T x⟫ = ⟪u k - x, T (y - T x)⟫ :=
  by
  intro k
  rw [← T.map_sub, hT]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
⊢ ∀ (k : ℕ), inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
[PROOFSTEP]
intro k
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
k : ℕ
⊢ inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
[PROOFSTEP]
rw [← T.map_sub, hT]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
hlhs : ∀ (k : ℕ), inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
⊢ inner (y - ↑T x) (y - ↑T x) = 0
[PROOFSTEP]
refine' tendsto_nhds_unique ((hTu.sub_const _).inner tendsto_const_nhds) _
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
hlhs : ∀ (k : ℕ), inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
⊢ Filter.Tendsto (fun t => inner ((↑T ∘ u) t - ↑T x) (y - ↑T x)) Filter.atTop (nhds 0)
[PROOFSTEP]
simp_rw [Function.comp_apply, hlhs]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
hlhs : ∀ (k : ℕ), inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
⊢ Filter.Tendsto (fun t => inner (u t - x) (↑T (y - ↑T x))) Filter.atTop (nhds 0)
[PROOFSTEP]
rw [← inner_zero_left (T (y - T x))]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
hlhs : ∀ (k : ℕ), inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
⊢ Filter.Tendsto (fun t => inner (u t - x) (↑T (y - ↑T x))) Filter.atTop (nhds (inner 0 (↑T (y - ↑T x))))
[PROOFSTEP]
refine' Filter.Tendsto.inner _ tendsto_const_nhds
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
hlhs : ∀ (k : ℕ), inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
⊢ Filter.Tendsto (fun t => u t - x) Filter.atTop (nhds 0)
[PROOFSTEP]
rw [← sub_self x]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
inst✝ : CompleteSpace E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
u : ℕ → E
x y : E
hu : Filter.Tendsto u Filter.atTop (nhds x)
hTu : Filter.Tendsto (↑T ∘ u) Filter.atTop (nhds y)
hlhs : ∀ (k : ℕ), inner (↑T (u k) - ↑T x) (y - ↑T x) = inner (u k - x) (↑T (y - ↑T x))
⊢ Filter.Tendsto (fun t => u t - x) Filter.atTop (nhds (x - x))
[PROOFSTEP]
exact hu.sub_const _
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
T : E →L[𝕜] E
hT : IsSymmetric ↑T
x : E
⊢ ↑(ContinuousLinearMap.reApplyInnerSelf T x) = inner (↑T x) x
[PROOFSTEP]
rsuffices ⟨r, hr⟩ : ∃ r : ℝ, ⟪T x, x⟫ = r
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
T : E →L[𝕜] E
hT : IsSymmetric ↑T
x : E
r : ℝ
hr : inner (↑T x) x = ↑r
⊢ ↑(ContinuousLinearMap.reApplyInnerSelf T x) = inner (↑T x) x
[PROOFSTEP]
simp [hr, T.reApplyInnerSelf_apply]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
T : E →L[𝕜] E
hT : IsSymmetric ↑T
x : E
⊢ ∃ r, inner (↑T x) x = ↑r
[PROOFSTEP]
rw [← conj_eq_iff_real]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
T : E →L[𝕜] E
hT : IsSymmetric ↑T
x : E
⊢ ↑(starRingEnd 𝕜) (inner (↑T x) x) = inner (↑T x) x
[PROOFSTEP]
exact hT.conj_inner_sym x x
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
⊢ inner (↑(↑ℝ T) x) y = inner x (↑(↑ℝ T) y)
[PROOFSTEP]
simp [hT x y, real_inner_eq_re_inner, LinearMap.coe_restrictScalars ℝ]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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_6
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ IsSymmetric T ↔ ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
[PROOFSTEP]
constructor
[GOAL]
case mp
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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_6
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ IsSymmetric T → ∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
[PROOFSTEP]
intro hT v
[GOAL]
case mp
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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_6
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : IsSymmetric T
v : V
⊢ ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v
[PROOFSTEP]
apply IsSymmetric.conj_inner_sym hT
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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_6
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ (∀ (v : V), ↑(starRingEnd ℂ) (inner (↑T v) v) = inner (↑T v) v) → IsSymmetric T
[PROOFSTEP]
intro h x y
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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_6
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)
[PROOFSTEP]
rw [← inner_conj_symm x (T y)]
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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_6
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)
[PROOFSTEP]
rw [inner_map_polarization T x y]
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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_6
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)
[PROOFSTEP]
simp only [starRingEnd_apply, star_div', star_sub, star_add, star_mul]
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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_6
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
[PROOFSTEP]
simp only [← starRingEnd_apply]
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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_6
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
[PROOFSTEP]
rw [h (x + y), h (x - y), h (x + Complex.I • y), h (x - Complex.I • y)]
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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_6
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
[PROOFSTEP]
simp only [Complex.conj_I]
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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_6
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
[PROOFSTEP]
rw [inner_map_polarization']
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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_6
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
[PROOFSTEP]
norm_num
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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_6
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
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
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
[PROOFSTEP]
rcases@I_mul_I_ax 𝕜 _ with (h | h)
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
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
[PROOFSTEP]
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)]
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
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
[PROOFSTEP]
suffices (re ⟪T y, x⟫ : 𝕜) = ⟪T y, x⟫ by
  rw [conj_eq_iff_re.mpr this]
  ring
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
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
[PROOFSTEP]
rw [conj_eq_iff_re.mpr this]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
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
[PROOFSTEP]
ring
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
h : I = 0
⊢ ↑(↑re (inner (↑T y) x)) = inner (↑T y) x
[PROOFSTEP]
rw [← re_add_im ⟪T y, x⟫]
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
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
[PROOFSTEP]
simp_rw [h, mul_zero, add_zero]
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
h : I = 0
⊢ ↑(↑re ↑(↑re (inner (↑T y) x))) = ↑(↑re (inner (↑T y) x))
[PROOFSTEP]
norm_cast
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
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
[PROOFSTEP]
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, IsROrC.conj_I, mul_add, mul_sub, sub_sub, ← mul_assoc, mul_neg, h, neg_neg,
  one_mul, neg_one_mul]
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
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
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
⊢ (∀ (x : E), inner (↑T x) x = 0) ↔ T = 0
[PROOFSTEP]
simp_rw [LinearMap.ext_iff, zero_apply]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
⊢ (∀ (x : E), inner (↑T x) x = 0) ↔ ∀ (x : E), ↑T x = 0
[PROOFSTEP]
refine' ⟨fun h x => _, fun h => by simp_rw [h, inner_zero_left, forall_const]⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
h : ∀ (x : E), ↑T x = 0
⊢ ∀ (x : E), inner (↑T x) x = 0
[PROOFSTEP]
simp_rw [h, inner_zero_left, forall_const]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
h : ∀ (x : E), inner (↑T x) x = 0
x : E
⊢ ↑T x = 0
[PROOFSTEP]
rw [← @inner_self_eq_zero 𝕜, hT.inner_map_polarization]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
h : ∀ (x : E), inner (↑T x) x = 0
x : E
⊢ (inner (↑T (x + ↑T x)) (x + ↑T x) - inner (↑T (x - ↑T x)) (x - ↑T x) - I * inner (↑T (x + I • ↑T x)) (x + I • ↑T x) +
        I * inner (↑T (x - I • ↑T x)) (x - I • ↑T x)) /
      4 =
    0
[PROOFSTEP]
simp_rw [h _]
[GOAL]
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
G : Type u_5
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'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
h : ∀ (x : E), inner (↑T x) x = 0
x : E
⊢ (0 - 0 - I * 0 + I * 0) / 4 = 0
[PROOFSTEP]
ring
