𝕜 : Type u_1
E : Type u_2
E' : Type ?u.196495
F : Type ?u.196498
G : Type ?u.196501
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
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.196495
F : Type ?u.196498
G : Type ?u.196501
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
simp_rw [LinearMap.ext_iff, zero_apply]
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.196495
F : Type ?u.196498
G : Type ?u.196501
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
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.196495
F : Type ?u.196498
G : Type ?u.196501
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
refine' ⟨fun h x => _, fun h => by simp_rw [h, inner_zero_left, forall_const]⟩
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.196495
F : Type ?u.196498
G : Type ?u.196501
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
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.196495
F : Type ?u.196498
G : Type ?u.196501
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
rw [← @inner_self_eq_zero 𝕜, hT.inner_map_polarization]
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.196495
F : Type ?u.196498
G : Type ?u.196501
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
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.196495
F : Type ?u.196498
G : Type ?u.196501
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
simp_rw [h _]
no goals
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.196495
F : Type ?u.196498
G : Type ?u.196501
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
ring
no goals
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.196495
F : Type ?u.196498
G : Type ?u.196501
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
simp_rw [h, inner_zero_left, forall_const]