𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
F : Type u_1
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := LinearMap.extendTo𝕜' ↑fr
⊢ ‖↑lm x‖ ≤ ‖fr‖ * ‖x‖
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
F : Type u_1
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
⊢ ‖↑(LinearMap.extendTo𝕜' ↑fr) x‖ ≤ ‖fr‖ * ‖x‖
set lm : F →ₗ[𝕜] 𝕜 := fr.toLinearMap.extendTo𝕜'
case pos
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
F : Type u_1
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := LinearMap.extendTo𝕜' ↑fr
h : ↑lm x = 0
⊢ ‖↑lm x‖ ≤ ‖fr‖ * ‖x‖

case neg
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
F : Type u_1
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := LinearMap.extendTo𝕜' ↑fr
h : ¬↑lm x = 0
⊢ ‖↑lm x‖ ≤ ‖fr‖ * ‖x‖
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
F : Type u_1
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := LinearMap.extendTo𝕜' ↑fr
⊢ ‖↑lm x‖ ≤ ‖fr‖ * ‖x‖
by_cases h : lm x = 0
case neg
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
F : Type u_1
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := LinearMap.extendTo𝕜' ↑fr
h : ¬↑lm x = 0
⊢ ‖↑lm x‖ ^ 2 ≤ ‖↑lm x‖ * (‖fr‖ * ‖x‖)
case neg
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
F : Type u_1
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := LinearMap.extendTo𝕜' ↑fr
h : ¬↑lm x = 0
⊢ ‖↑lm x‖ ≤ ‖fr‖ * ‖x‖
rw [← mul_le_mul_left (norm_pos_iff.2 h), ← sq]
no goals
case neg
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
F : Type u_1
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := LinearMap.extendTo𝕜' ↑fr
h : ¬↑lm x = 0
⊢ ‖↑lm x‖ ^ 2 ≤ ‖↑lm x‖ * (‖fr‖ * ‖x‖)
calc
  ‖lm x‖ ^ 2 = fr (conj (lm x : 𝕜) • x) := fr.toLinearMap.norm_extendTo𝕜'_apply_sq x
  _ ≤ ‖fr (conj (lm x : 𝕜) • x)‖ := (le_abs_self _)
  _ ≤ ‖fr‖ * ‖conj (lm x : 𝕜) • x‖ := (le_op_norm _ _)
  _ = ‖(lm x : 𝕜)‖ * (‖fr‖ * ‖x‖) := by rw [norm_smul, norm_conj, mul_left_comm]
case pos
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
F : Type u_1
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := LinearMap.extendTo𝕜' ↑fr
h : ↑lm x = 0
⊢ 0 ≤ ‖fr‖ * ‖x‖
case pos
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
F : Type u_1
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := LinearMap.extendTo𝕜' ↑fr
h : ↑lm x = 0
⊢ ‖↑lm x‖ ≤ ‖fr‖ * ‖x‖
rw [h, norm_zero]
no goals
case pos
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
F : Type u_1
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := LinearMap.extendTo𝕜' ↑fr
h : ↑lm x = 0
⊢ 0 ≤ ‖fr‖ * ‖x‖
apply mul_nonneg <;> exact norm_nonneg _
no goals
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
F : Type u_1
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := LinearMap.extendTo𝕜' ↑fr
h : ¬↑lm x = 0
⊢ ‖fr‖ * ‖↑(starRingEnd ((fun x => 𝕜) x)) (↑lm x) • x‖ = ‖↑lm x‖ * (‖fr‖ * ‖x‖)
rw [norm_smul, norm_conj, mul_left_comm]