-- Mathlib/Analysis/Normed/Module/Dual.lean
theorem polar_ball {𝕜 E : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ}
    (hr : 0 < r) : polar 𝕜 (ball (0 : E) r) = closedBall (0 : Dual 𝕜 E) r⁻¹

Proof state:
case a.h
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x : Dual 𝕜 E
hx : x ∈ polar 𝕜 (ball 0 r)
a : ℝ
ha : r⁻¹ < a
⊢ x ∈ closedBall 0 (‖↑(r * a)‖ / r)

Tactic:
apply polar_ball_subset_closedBall_div _ hr hx

Result:
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x : Dual 𝕜 E
hx : x ∈ polar 𝕜 (ball 0 r)
a : ℝ
ha : r⁻¹ < a
⊢ 1 < ‖↑(r * a)‖

Proof state:
case a.h
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x : Dual 𝕜 E
hx : x ∈ polar 𝕜 (ball 0 r)
a : ℝ
ha : r⁻¹ < a
⊢ x ∈ closedBall 0 (r * a / r)

Tactic:
rw [← RCLike.norm_of_nonneg (K := 𝕜) (le_trans zero_le_one
  (le_of_lt ((inv_lt_iff_one_lt_mul₀' hr).mp ha)))]

Result:
case a.h
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x : Dual 𝕜 E
hx : x ∈ polar 𝕜 (ball 0 r)
a : ℝ
ha : r⁻¹ < a
⊢ x ∈ closedBall 0 (‖↑(r * a)‖ / r)

Proof state:
case a.h
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x : Dual 𝕜 E
hx : x ∈ polar 𝕜 (ball 0 r)
⊢ ∀ (a : ℝ), r⁻¹ < a → ‖x‖ ≤ a

Tactic:
intro a ha

Result:
case a.h
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x : Dual 𝕜 E
hx : x ∈ polar 𝕜 (ball 0 r)
a : ℝ
ha : r⁻¹ < a
⊢ ‖x‖ ≤ a

Proof state:
case a
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ polar 𝕜 (closedBall 0 r) ≤ polar 𝕜 (ball 0 r)

Tactic:
exact LinearMap.polar_antitone _ ball_subset_closedBall

Result:
no goals

Proof state:
case a
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ closedBall 0 r⁻¹ ≤ polar 𝕜 (ball 0 r)

Tactic:
rw [← polar_closedBall hr]

Result:
case a
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ polar 𝕜 (closedBall 0 r) ≤ polar 𝕜 (ball 0 r)

Proof state:
case a.h
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x : Dual 𝕜 E
hx : x ∈ polar 𝕜 (ball 0 r)
a : ℝ
ha : r⁻¹ < a
⊢ ‖x‖ ≤ a

Tactic:
rw [← mem_closedBall_zero_iff, ← (mul_div_cancel_left₀ a (Ne.symm (ne_of_lt hr)))]

Result:
case a.h
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x : Dual 𝕜 E
hx : x ∈ polar 𝕜 (ball 0 r)
a : ℝ
ha : r⁻¹ < a
⊢ x ∈ closedBall 0 (r * a / r)

Proof state:
case a
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ polar 𝕜 (ball 0 r) ≤ closedBall 0 r⁻¹

Tactic:
intro x hx

Result:
case a
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x : Dual 𝕜 E
hx : x ∈ polar 𝕜 (ball 0 r)
⊢ x ∈ closedBall 0 r⁻¹

Proof state:
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x : Dual 𝕜 E
hx : x ∈ polar 𝕜 (ball 0 r)
a : ℝ
ha : r⁻¹ < a
⊢ 1 < r * a

Tactic:
exact (inv_lt_iff_one_lt_mul₀' hr).mp ha

Result:
no goals

Proof state:
case a
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x : Dual 𝕜 E
hx : x ∈ polar 𝕜 (ball 0 r)
⊢ x ∈ closedBall 0 r⁻¹

Tactic:
rw [mem_closedBall_zero_iff]

Result:
case a
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x : Dual 𝕜 E
hx : x ∈ polar 𝕜 (ball 0 r)
⊢ ‖x‖ ≤ r⁻¹

Proof state:
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x : Dual 𝕜 E
hx : x ∈ polar 𝕜 (ball 0 r)
a : ℝ
ha : r⁻¹ < a
⊢ 1 < ‖↑(r * a)‖

Tactic:
rw [RCLike.norm_of_nonneg (K := 𝕜) (le_trans zero_le_one
  (le_of_lt ((inv_lt_iff_one_lt_mul₀' hr).mp ha)))]

Result:
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x : Dual 𝕜 E
hx : x ∈ polar 𝕜 (ball 0 r)
a : ℝ
ha : r⁻¹ < a
⊢ 1 < r * a

Proof state:
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ polar 𝕜 (ball 0 r) = closedBall 0 r⁻¹

Tactic:
apply le_antisymm

Result:
case a
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ polar 𝕜 (ball 0 r) ≤ closedBall 0 r⁻¹

case a
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ closedBall 0 r⁻¹ ≤ polar 𝕜 (ball 0 r)

Proof state:
case a
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x : Dual 𝕜 E
hx : x ∈ polar 𝕜 (ball 0 r)
⊢ ‖x‖ ≤ r⁻¹

Tactic:
apply le_of_forall_gt_imp_ge_of_dense

Result:
case a.h
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x : Dual 𝕜 E
hx : x ∈ polar 𝕜 (ball 0 r)
⊢ ∀ (a : ℝ), r⁻¹ < a → ‖x‖ ≤ a