Theorem: polarDual_zero (src/Polar.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
⊢ polarDual {0} = Set.univ
Tactic:
rw [polarDual]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
⊢ ⋂₀ (SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' {0}))) = Set.univ

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
⊢ ⋂₀ (SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' {0}))) = Set.univ
Tactic:
have : (@Subtype.val E fun p => p ≠ 0) ⁻¹' {0} = ∅ := by
  rw [Set.preimage_singleton_eq_empty]
  simp only [ne_eq, Subtype.range_coe_subtype, Set.mem_setOf_eq, not_true, not_false_eq_true]
  done
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
this : Subtype.val ⁻¹' {0} = ∅
⊢ ⋂₀ (SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' {0}))) = Set.univ

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
this : Subtype.val ⁻¹' {0} = ∅
⊢ ⋂₀ (SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' {0}))) = Set.univ
Tactic:
rw [this, Set.image_empty, Set.image_empty, Set.sInter_empty]
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
⊢ Subtype.val ⁻¹' {0} = ∅
Tactic:
rw [Set.preimage_singleton_eq_empty]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
⊢ 0 ∉ Set.range Subtype.val

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
⊢ 0 ∉ Set.range Subtype.val
Tactic:
simp only [ne_eq, Subtype.range_coe_subtype, Set.mem_setOf_eq, not_true, not_false_eq_true]
State after:
no goals