Theorem: polarDual_origin (src/Polar.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
⊢ 0 ∈ polarDual X
Tactic:
intro Hi_s h
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Hi_s : Set E
h : Hi_s ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X))
⊢ 0 ∈ Hi_s

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Hi_s : Set E
h : Hi_s ∈ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' X))
⊢ 0 ∈ Hi_s
Tactic:
rw [Set.mem_image] at h
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Hi_s : Set E
h : ∃ x ∈ pointDual '' (Subtype.val ⁻¹' X), ↑x = Hi_s
⊢ 0 ∈ Hi_s

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X Hi_s : Set E
h : ∃ x ∈ pointDual '' (Subtype.val ⁻¹' X), ↑x = Hi_s
⊢ 0 ∈ Hi_s
Tactic:
rcases h with ⟨ Hi_, h, rfl ⟩
State after:
case intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
Hi_ : Halfspace E
h : Hi_ ∈ pointDual '' (Subtype.val ⁻¹' X)
⊢ 0 ∈ ↑Hi_

State before:
case intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
Hi_ : Halfspace E
h : Hi_ ∈ pointDual '' (Subtype.val ⁻¹' X)
⊢ 0 ∈ ↑Hi_
Tactic:
rw [Set.mem_image] at h
State after:
case intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
Hi_ : Halfspace E
h : ∃ x ∈ Subtype.val ⁻¹' X, pointDual x = Hi_
⊢ 0 ∈ ↑Hi_

State before:
case intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
Hi_ : Halfspace E
h : ∃ x ∈ Subtype.val ⁻¹' X, pointDual x = Hi_
⊢ 0 ∈ ↑Hi_
Tactic:
rcases h with ⟨ p, _, rfl ⟩
State after:
case intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
p : { p // p ≠ 0 }
left✝ : p ∈ Subtype.val ⁻¹' X
⊢ 0 ∈ ↑(pointDual p)

State before:
case intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
X : Set E
p : { p // p ≠ 0 }
left✝ : p ∈ Subtype.val ⁻¹' X
⊢ 0 ∈ ↑(pointDual p)
Tactic:
exact pointDual_origin p
State after:
no goals