no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.3418113
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
dec_E : DecidableEq E
inst✝ : NormedSpace ℝ E
r : ℝ
x y : E
⊢ inner (r • x, y).fst (r • x, y).snd = r • inner (x, y).fst (x, y).snd
simp only [← algebraMap_smul 𝕜 r x, algebraMap_eq_ofReal, inner_smul_real_left]
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.3418113
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
dec_E : DecidableEq E
inst✝ : NormedSpace ℝ E
r : ℝ
x y : E
⊢ inner (x, r • y).fst (x, r • y).snd = r • inner (x, y).fst (x, y).snd
simp only [← algebraMap_smul 𝕜 r y, algebraMap_eq_ofReal, inner_smul_real_right]
𝕜 : Type u_2
E : Type u_1
F : Type ?u.3418113
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
dec_E : DecidableEq E
inst✝ : NormedSpace ℝ E
x y : E
⊢ ‖inner (x, y).fst (x, y).snd‖ ≤ ‖x‖ * ‖y‖
𝕜 : Type u_2
E : Type u_1
F : Type ?u.3418113
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
dec_E : DecidableEq E
inst✝ : NormedSpace ℝ E
x y : E
⊢ ‖inner (x, y).fst (x, y).snd‖ ≤ 1 * ‖x‖ * ‖y‖
rw [one_mul]
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.3418113
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
dec_E : DecidableEq E
inst✝ : NormedSpace ℝ E
x y : E
⊢ ‖inner (x, y).fst (x, y).snd‖ ≤ ‖x‖ * ‖y‖
exact norm_inner_le_norm x y