𝕜 : Type u_1
E : Type u_2
F : Type ?u.3288929
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x : E
⊢ ‖x‖ ≤ ‖↑(innerSL 𝕜) x‖
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3288929
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x : E
⊢ ‖↑(innerSL 𝕜) x‖ = ‖x‖
refine'
  le_antisymm ((innerSL 𝕜 x).op_norm_le_bound (norm_nonneg _) fun y => norm_inner_le_norm _ _) _
case inl
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3288929
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
⊢ ‖0‖ ≤ ‖↑(innerSL 𝕜) 0‖

case inr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3288929
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x : E
h : x ≠ 0
⊢ ‖x‖ ≤ ‖↑(innerSL 𝕜) x‖
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3288929
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x : E
⊢ ‖x‖ ≤ ‖↑(innerSL 𝕜) x‖
rcases eq_or_ne x 0 with (rfl | h)
no goals
case inl
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3288929
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
⊢ ‖0‖ ≤ ‖↑(innerSL 𝕜) 0‖
simp
case inr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3288929
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x : E
h : x ≠ 0
⊢ ‖x‖ * ‖x‖ ≤ ‖↑(innerSL 𝕜) x‖ * ‖x‖
case inr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3288929
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x : E
h : x ≠ 0
⊢ ‖x‖ ≤ ‖↑(innerSL 𝕜) x‖
refine' (mul_le_mul_right (norm_pos_iff.2 h)).mp _
no goals
case inr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3288929
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x : E
h : x ≠ 0
⊢ ‖x‖ * ‖x‖ ≤ ‖↑(innerSL 𝕜) x‖ * ‖x‖
calc
  ‖x‖ * ‖x‖ = ‖(⟪x, x⟫ : 𝕜)‖ := by
    rw [← sq, inner_self_eq_norm_sq_to_K, norm_pow, norm_ofReal, abs_norm]
  _ ≤ ‖innerSL 𝕜 x‖ * ‖x‖ := (innerSL 𝕜 x).le_op_norm _
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3288929
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x : E
h : x ≠ 0
⊢ ‖x‖ * ‖x‖ = ‖inner x x‖
rw [← sq, inner_self_eq_norm_sq_to_K, norm_pow, norm_ofReal, abs_norm]