-- Mathlib/Analysis/Normed/Module/Dual.lean
theorem polar_ball_subset_closedBall_div {c : 𝕜} (hc : 1 < ‖c‖) {r : ℝ} (hr : 0 < r) :
    polar 𝕜 (ball (0 : E) r) ⊆ closedBall (0 : Dual 𝕜 E) (‖c‖ / r)

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
hx' : ∀ (z : E), ‖z‖ < r → ‖x' z‖ ≤ 1
⊢ ‖x'‖ ≤ ‖c‖ / r

Tactic:
have hcr : 0 < ‖c‖ / r := div_pos (zero_lt_one.trans hc) hr

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
hx' : ∀ (z : E), ‖z‖ < r → ‖x' z‖ ≤ 1
hcr : 0 < ‖c‖ / r
⊢ ‖x'‖ ≤ ‖c‖ / r

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
hx' : ∀ (z : E), ‖z‖ < r → ‖x' z‖ ≤ 1
hcr : 0 < ‖c‖ / r
⊢ ‖x'‖ ≤ ‖c‖ / r

Tactic:
refine ContinuousLinearMap.opNorm_le_of_shell hr hcr.le hc fun x h₁ h₂ => ?_

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
hx' : ∀ (z : E), ‖z‖ < r → ‖x' z‖ ≤ 1
hcr : 0 < ‖c‖ / r
x : E
h₁ : r / ‖c‖ ≤ ‖x‖
h₂ : ‖x‖ < r
⊢ ‖x' x‖ ≤ ‖c‖ / r * ‖x‖

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
hx' : ∀ (z : E), ‖z‖ < r → ‖x' z‖ ≤ 1
hcr : 0 < ‖c‖ / r
x : E
h₁ : r / ‖c‖ ≤ ‖x‖
h₂ : ‖x‖ < r
⊢ ‖x' x‖ ≤ ‖c‖ / r * ‖x‖

Tactic:
calc
  ‖x' x‖ ≤ 1 := hx' _ h₂
  _ ≤ ‖c‖ / r * ‖x‖ := (inv_le_iff_one_le_mul₀' hcr).1 (by rwa [inv_div])

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
hx' : x' ∈ polar 𝕜 (ball 0 r)
⊢ x' ∈ closedBall 0 (‖c‖ / r)

Tactic:
rw [mem_polar_iff] at hx'

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
hx' : ∀ z ∈ ball 0 r, ‖x' z‖ ≤ 1
⊢ x' ∈ closedBall 0 (‖c‖ / r)

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
⊢ polar 𝕜 (ball 0 r) ⊆ closedBall 0 (‖c‖ / r)

Tactic:
intro x' hx'

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
hx' : x' ∈ polar 𝕜 (ball 0 r)
⊢ x' ∈ closedBall 0 (‖c‖ / r)

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
hx' : ∀ z ∈ ball 0 r, ‖x' z‖ ≤ 1
⊢ x' ∈ closedBall 0 (‖c‖ / r)

Tactic:
simp only [polar, mem_setOf, mem_closedBall_zero_iff, mem_ball_zero_iff] at *

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
hx' : ∀ (z : E), ‖z‖ < r → ‖x' z‖ ≤ 1
⊢ ‖x'‖ ≤ ‖c‖ / r

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
hx' : ∀ (z : E), ‖z‖ < r → ‖x' z‖ ≤ 1
hcr : 0 < ‖c‖ / r
x : E
h₁ : r / ‖c‖ ≤ ‖x‖
h₂ : ‖x‖ < r
⊢ (‖c‖ / r)⁻¹ ≤ ‖x‖

Tactic:
rwa [inv_div]

Result:
no goals