case pos
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖↑f x‖ ≤ M * ‖f‖
h : x = 0
⊢ ‖x‖ ≤ M

case neg
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖↑f x‖ ≤ M * ‖f‖
h : ¬x = 0
⊢ ‖x‖ ≤ M
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖↑f x‖ ≤ M * ‖f‖
⊢ ‖x‖ ≤ M
by_cases h : x = 0
no goals
case pos
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖↑f x‖ ≤ M * ‖f‖
h : x = 0
⊢ ‖x‖ ≤ M
simp only [h, hMp, norm_zero]
case neg.intro.intro
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖↑f x‖ ≤ M * ‖f‖
h : ¬x = 0
f : E →L[𝕜] 𝕜
hf₁ : ‖f‖ = 1
hfx : ↑f x = ↑‖x‖
⊢ ‖x‖ ≤ M
case neg
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖↑f x‖ ≤ M * ‖f‖
h : ¬x = 0
⊢ ‖x‖ ≤ M
obtain ⟨f, hf₁, hfx⟩ : ∃ f : E →L[𝕜] 𝕜, ‖f‖ = 1 ∧ f x = ‖x‖ := exists_dual_vector 𝕜 x h
no goals
case neg.intro.intro
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖↑f x‖ ≤ M * ‖f‖
h : ¬x = 0
f : E →L[𝕜] 𝕜
hf₁ : ‖f‖ = 1
hfx : ↑f x = ↑‖x‖
⊢ ‖x‖ ≤ M
calc
  ‖x‖ = ‖(‖x‖ : 𝕜)‖ := IsROrC.norm_coe_norm.symm
  _ = ‖f x‖ := by rw [hfx]
  _ ≤ M * ‖f‖ := (hM f)
  _ = M := by rw [hf₁, mul_one]
no goals
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖↑f x‖ ≤ M * ‖f‖
h : ¬x = 0
f : E →L[𝕜] 𝕜
hf₁ : ‖f‖ = 1
hfx : ↑f x = ↑‖x‖
⊢ ‖↑‖x‖‖ = ‖↑f x‖
rw [hfx]
no goals
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖↑f x‖ ≤ M * ‖f‖
h : ¬x = 0
f : E →L[𝕜] 𝕜
hf₁ : ‖f‖ = 1
hfx : ↑f x = ↑‖x‖
⊢ M * ‖f‖ = M
rw [hf₁, mul_one]