case pos
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : c = 0
⊢ c⁻¹ • x' ∈ polar 𝕜 s

case neg
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
⊢ c⁻¹ • x' ∈ polar 𝕜 s
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
⊢ c⁻¹ • x' ∈ polar 𝕜 s
by_cases c_zero : c = 0
case neg
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • ↑x' z‖ = ‖c⁻¹‖ * ‖↑x' z‖
⊢ c⁻¹ • x' ∈ polar 𝕜 s
case neg
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
⊢ c⁻¹ • x' ∈ polar 𝕜 s
have eq : ∀ z, ‖c⁻¹ • x' z‖ = ‖c⁻¹‖ * ‖x' z‖ := fun z => norm_smul c⁻¹ _
case neg
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • ↑x' z‖ = ‖c⁻¹‖ * ‖↑x' z‖
le : ∀ (z : E), z ∈ s → ‖c⁻¹ • ↑x' z‖ ≤ ‖c⁻¹‖ * ‖c‖
⊢ c⁻¹ • x' ∈ polar 𝕜 s
case neg
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • ↑x' z‖ = ‖c⁻¹‖ * ‖↑x' z‖
⊢ c⁻¹ • x' ∈ polar 𝕜 s
have le : ∀ z, z ∈ s → ‖c⁻¹ • x' z‖ ≤ ‖c⁻¹‖ * ‖c‖ := by
  intro z hzs
  rw [eq z]
  apply mul_le_mul (le_of_eq rfl) (hc z hzs) (norm_nonneg _) (norm_nonneg _)
case neg
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • ↑x' z‖ = ‖c⁻¹‖ * ‖↑x' z‖
le : ∀ (z : E), z ∈ s → ‖c⁻¹ • ↑x' z‖ ≤ ‖c⁻¹‖ * ‖c‖
cancel : ‖c⁻¹‖ * ‖c‖ = 1
⊢ c⁻¹ • x' ∈ polar 𝕜 s
case neg
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • ↑x' z‖ = ‖c⁻¹‖ * ‖↑x' z‖
le : ∀ (z : E), z ∈ s → ‖c⁻¹ • ↑x' z‖ ≤ ‖c⁻¹‖ * ‖c‖
⊢ c⁻¹ • x' ∈ polar 𝕜 s
have cancel : ‖c⁻¹‖ * ‖c‖ = 1 := by
  simp only [c_zero, norm_eq_zero, Ne.def, not_false_iff, inv_mul_cancel, norm_inv]
no goals
case neg
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • ↑x' z‖ = ‖c⁻¹‖ * ‖↑x' z‖
le : ∀ (z : E), z ∈ s → ‖c⁻¹ • ↑x' z‖ ≤ ‖c⁻¹‖ * ‖c‖
cancel : ‖c⁻¹‖ * ‖c‖ = 1
⊢ c⁻¹ • x' ∈ polar 𝕜 s
rwa [cancel] at le
case pos
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : c = 0
⊢ 0 ∈ polar 𝕜 s
case pos
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : c = 0
⊢ c⁻¹ • x' ∈ polar 𝕜 s
simp only [c_zero, inv_zero, zero_smul]
no goals
case pos
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : c = 0
⊢ 0 ∈ polar 𝕜 s
exact (dualPairing 𝕜 E).flip.zero_mem_polar _
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • ↑x' z‖ = ‖c⁻¹‖ * ‖↑x' z‖
z : E
hzs : z ∈ s
⊢ ‖c⁻¹ • ↑x' z‖ ≤ ‖c⁻¹‖ * ‖c‖
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • ↑x' z‖ = ‖c⁻¹‖ * ‖↑x' z‖
⊢ ∀ (z : E), z ∈ s → ‖c⁻¹ • ↑x' z‖ ≤ ‖c⁻¹‖ * ‖c‖
intro z hzs
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • ↑x' z‖ = ‖c⁻¹‖ * ‖↑x' z‖
z : E
hzs : z ∈ s
⊢ ‖c⁻¹‖ * ‖↑x' z‖ ≤ ‖c⁻¹‖ * ‖c‖
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • ↑x' z‖ = ‖c⁻¹‖ * ‖↑x' z‖
z : E
hzs : z ∈ s
⊢ ‖c⁻¹ • ↑x' z‖ ≤ ‖c⁻¹‖ * ‖c‖
rw [eq z]
no goals
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • ↑x' z‖ = ‖c⁻¹‖ * ‖↑x' z‖
z : E
hzs : z ∈ s
⊢ ‖c⁻¹‖ * ‖↑x' z‖ ≤ ‖c⁻¹‖ * ‖c‖
apply mul_le_mul (le_of_eq rfl) (hc z hzs) (norm_nonneg _) (norm_nonneg _)
no goals
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • ↑x' z‖ = ‖c⁻¹‖ * ‖↑x' z‖
le : ∀ (z : E), z ∈ s → ‖c⁻¹ • ↑x' z‖ ≤ ‖c⁻¹‖ * ‖c‖
⊢ ‖c⁻¹‖ * ‖c‖ = 1
simp only [c_zero, norm_eq_zero, Ne.def, not_false_iff, inv_mul_cancel, norm_inv]