Theorem: mem_pointDual (src/Polar.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
x : E
⊢ x ∈ ↑(pointDual p) ↔ ⟪↑p, x⟫_ℝ ≤ 1
Tactic:
rw [pointDual.h, Set.mem_preimage, InnerProductSpace.toDual_apply, Set.mem_setOf,
  inner_smul_left, IsROrC.conj_to_real, ← mul_le_mul_left (by rw [norm_pos_iff]; exact p.2 : 0 < norm p.1),
  ← mul_assoc, mul_inv_cancel (norm_ne_zero_iff.mpr p.2), one_mul]
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
x : E
⊢ 0 < ‖↑p‖
Tactic:
rw [norm_pos_iff]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
x : E
⊢ ↑p ≠ 0

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
x : E
⊢ ↑p ≠ 0
Tactic:
exact p.2
State after:
no goals