-- Mathlib/Analysis/NormedSpace/Extend.lean
theorem norm_extendTo𝕜'_bound (fr : F →L[ℝ] ℝ) (x : F) :
    ‖(fr.toLinearMap.extendTo𝕜' x : 𝕜)‖ ≤ ‖fr‖ * ‖x‖

Proof state:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := (↑fr).extendTo𝕜'
⊢ ‖lm x‖ ≤ ‖fr‖ * ‖x‖

Tactic:
by_cases h : lm x = 0

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

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

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

Tactic:
apply mul_nonneg <;> exact norm_nonneg _

Result:
no goals

Proof state:
case neg
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := (↑fr).extendTo𝕜'
h : ¬lm x = 0
⊢ ‖lm x‖ ^ 2 ≤ ‖lm x‖ * (‖fr‖ * ‖x‖)

Tactic:
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_opNorm _ _
  _ = ‖(lm x : 𝕜)‖ * (‖fr‖ * ‖x‖) := by rw [norm_smul, norm_conj, mul_left_comm]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
⊢ ‖(↑fr).extendTo𝕜' x‖ ≤ ‖fr‖ * ‖x‖

Tactic:
set lm : F →ₗ[𝕜] 𝕜 := fr.toLinearMap.extendTo𝕜'

Result:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := (↑fr).extendTo𝕜'
⊢ ‖lm x‖ ≤ ‖fr‖ * ‖x‖

Proof state:
case neg
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := (↑fr).extendTo𝕜'
h : ¬lm x = 0
⊢ ‖lm x‖ ≤ ‖fr‖ * ‖x‖

Tactic:
rw [← mul_le_mul_left (norm_pos_iff.2 h), ← sq]

Result:
case neg
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := (↑fr).extendTo𝕜'
h : ¬lm x = 0
⊢ ‖lm x‖ ^ 2 ≤ ‖lm x‖ * (‖fr‖ * ‖x‖)

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

Tactic:
rw [h, norm_zero]

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

Proof state:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →L[ℝ] ℝ
x : F
lm : F →ₗ[𝕜] 𝕜 := (↑fr).extendTo𝕜'
h : ¬lm x = 0
⊢ ‖fr‖ * ‖(starRingEnd 𝕜) (lm x) • x‖ = ‖lm x‖ * (‖fr‖ * ‖x‖)

Tactic:
rw [norm_smul, norm_conj, mul_left_comm]

Result:
no goals