Theorem: pointDual_origin (src/Polar.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
⊢ 0 ∈ ↑(pointDual p)
Tactic:
rw [pointDual.h, map_smulₛₗ, map_inv₀, IsROrC.conj_to_real, Set.preimage_setOf_eq,
  Set.mem_setOf_eq, map_zero, ← one_div]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
⊢ 0 ≤ 1 / ‖↑p‖

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
⊢ 0 ≤ 1 / ‖↑p‖
Tactic:
apply le_of_lt
State after:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
⊢ 0 < 1 / ‖↑p‖

State before:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
⊢ 0 < 1 / ‖↑p‖
Tactic:
rw [div_pos_iff]
State after:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
⊢ 0 < 1 ∧ 0 < ‖↑p‖ ∨ 1 < 0 ∧ ‖↑p‖ < 0

State before:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
⊢ 0 < 1 ∧ 0 < ‖↑p‖ ∨ 1 < 0 ∧ ‖↑p‖ < 0
Tactic:
left
State after:
case a.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
⊢ 0 < 1 ∧ 0 < ‖↑p‖

State before:
case a.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
⊢ 0 < 1 ∧ 0 < ‖↑p‖
Tactic:
exact ⟨ zero_lt_one, by rw [norm_pos_iff]; exact p.2 ⟩
State after:
no goals

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

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