theorem Set.polarSet_closedUnitBall_eq_closedUnitBall {𝓗 : Type u} [NormedAddCommGroup 𝓗] [InnerProductSpace ℝ 𝓗] : (Metric.closedBall 0 1).polarSet = Metric.closedBall 0 1

Exercise 7.7: the polar set of the closed unit ball B(0;1) is the closed unit ball itself.