case mp
𝕜 : Type ?u.2752580
E : Type ?u.2752583
F : Type ?u.2752586
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ (∀ (x : V), inner (↑T x) x = 0) → T = 0

case mpr
𝕜 : Type ?u.2752580
E : Type ?u.2752583
F : Type ?u.2752586
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ T = 0 → ∀ (x : V), inner (↑T x) x = 0
𝕜 : Type ?u.2752580
E : Type ?u.2752583
F : Type ?u.2752586
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ (∀ (x : V), inner (↑T x) x = 0) ↔ T = 0
constructor
case mp
𝕜 : Type ?u.2752580
E : Type ?u.2752583
F : Type ?u.2752586
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : ∀ (x : V), inner (↑T x) x = 0
⊢ T = 0
case mp
𝕜 : Type ?u.2752580
E : Type ?u.2752583
F : Type ?u.2752586
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ (∀ (x : V), inner (↑T x) x = 0) → T = 0
intro hT
case mp.h
𝕜 : Type ?u.2752580
E : Type ?u.2752583
F : Type ?u.2752586
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : ∀ (x : V), inner (↑T x) x = 0
x : V
⊢ ↑T x = ↑0 x
case mp
𝕜 : Type ?u.2752580
E : Type ?u.2752583
F : Type ?u.2752586
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : ∀ (x : V), inner (↑T x) x = 0
⊢ T = 0
ext x
case mp.h
𝕜 : Type ?u.2752580
E : Type ?u.2752583
F : Type ?u.2752586
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : ∀ (x : V), inner (↑T x) x = 0
x : V
⊢ inner (↑T x) (↑T x) = 0
case mp.h
𝕜 : Type ?u.2752580
E : Type ?u.2752583
F : Type ?u.2752586
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : ∀ (x : V), inner (↑T x) x = 0
x : V
⊢ ↑T x = ↑0 x
simp only [LinearMap.zero_apply, ← @inner_self_eq_zero ℂ V]
case mp.h
𝕜 : Type ?u.2752580
E : Type ?u.2752583
F : Type ?u.2752586
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : ∀ (x : V), inner (↑T x) x = 0
x : V
⊢ (inner (↑T (↑T x + x)) (↑T x + x) - inner (↑T (↑T x - x)) (↑T x - x) +
          Complex.I * inner (↑T (↑T x + Complex.I • x)) (↑T x + Complex.I • x) -
        Complex.I * inner (↑T (↑T x - Complex.I • x)) (↑T x - Complex.I • x)) /
      4 =
    0
case mp.h
𝕜 : Type ?u.2752580
E : Type ?u.2752583
F : Type ?u.2752586
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : ∀ (x : V), inner (↑T x) x = 0
x : V
⊢ inner (↑T x) (↑T x) = 0
simp (config := {singlePass := true}) only [inner_map_polarization]
case mp.h
𝕜 : Type ?u.2752580
E : Type ?u.2752583
F : Type ?u.2752586
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : ∀ (x : V), inner (↑T x) x = 0
x : V
⊢ (0 - 0 + Complex.I * 0 - Complex.I * 0) / 4 = 0
case mp.h
𝕜 : Type ?u.2752580
E : Type ?u.2752583
F : Type ?u.2752586
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : ∀ (x : V), inner (↑T x) x = 0
x : V
⊢ (inner (↑T (↑T x + x)) (↑T x + x) - inner (↑T (↑T x - x)) (↑T x - x) +
          Complex.I * inner (↑T (↑T x + Complex.I • x)) (↑T x + Complex.I • x) -
        Complex.I * inner (↑T (↑T x - Complex.I • x)) (↑T x - Complex.I • x)) /
      4 =
    0
simp only [hT]
no goals
case mp.h
𝕜 : Type ?u.2752580
E : Type ?u.2752583
F : Type ?u.2752586
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : ∀ (x : V), inner (↑T x) x = 0
x : V
⊢ (0 - 0 + Complex.I * 0 - Complex.I * 0) / 4 = 0
norm_num
case mpr
𝕜 : Type ?u.2752580
E : Type ?u.2752583
F : Type ?u.2752586
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
x : V
⊢ inner (↑0 x) x = 0
case mpr
𝕜 : Type ?u.2752580
E : Type ?u.2752583
F : Type ?u.2752586
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ T = 0 → ∀ (x : V), inner (↑T x) x = 0
rintro rfl x
no goals
case mpr
𝕜 : Type ?u.2752580
E : Type ?u.2752583
F : Type ?u.2752586
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
x : V
⊢ inner (↑0 x) x = 0
simp only [LinearMap.zero_apply, inner_zero_left]