Theorem: Halfspace.val_eq (src/Halfspace.lean)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
⊢ ↑(val p H_') ∩ ↑p = Subtype.val '' ↑H_'
Tactic:
have := Halfspace.val_f p H_'
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
⊢ ↑(val p H_') ∩ ↑p = Subtype.val '' ↑H_'

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
⊢ ↑(val p H_') ∩ ↑p = Subtype.val '' ↑H_'
Tactic:
apply subset_antisymm <;> intro x <;> rw [Set.mem_inter_iff, Set.mem_image]
State after:
case a
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x : E
⊢ x ∈ ↑(val p H_') ∧ x ∈ ↑p → ∃ x_1 ∈ ↑H_', ↑x_1 = x

case a
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x : E
⊢ (∃ x_1 ∈ ↑H_', ↑x_1 = x) → x ∈ ↑(val p H_') ∧ x ∈ ↑p

State before:
case a
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x : E
⊢ x ∈ ↑(val p H_') ∧ x ∈ ↑p → ∃ x_1 ∈ ↑H_', ↑x_1 = x
Tactic:
rintro ⟨ hxH_', hxp ⟩
State after:
case a.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x : E
hxH_' : x ∈ ↑(val p H_')
hxp : x ∈ ↑p
⊢ ∃ x_1 ∈ ↑H_', ↑x_1 = x

State before:
case a.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x : E
hxH_' : x ∈ ↑(val p H_')
hxp : x ∈ ↑p
⊢ ∃ x_1 ∈ ↑H_', ↑x_1 = x
Tactic:
refine ⟨ ⟨ x, hxp ⟩, ?_, rfl ⟩
State after:
case a.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x : E
hxH_' : x ∈ ↑(val p H_')
hxp : x ∈ ↑p
⊢ { val := x, property := hxp } ∈ ↑H_'

State before:
case a.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x : E
hxH_' : x ∈ ↑(val p H_')
hxp : x ∈ ↑p
⊢ { val := x, property := hxp } ∈ ↑H_'
Tactic:
rw [Halfspace_mem, ← (this ⟨ x, hxp ⟩), ← Halfspace.val_C p H_']
State after:
case a.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x : E
hxH_' : x ∈ ↑(val p H_')
hxp : x ∈ ↑p
⊢ ↑(val p H_').f ↑{ val := x, property := hxp } ≤ (val p H_').α

State before:
case a.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x : E
hxH_' : x ∈ ↑(val p H_')
hxp : x ∈ ↑p
⊢ ↑(val p H_').f ↑{ val := x, property := hxp } ≤ (val p H_').α
Tactic:
exact hxH_'
State after:
no goals

State before:
case a
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x : E
⊢ (∃ x_1 ∈ ↑H_', ↑x_1 = x) → x ∈ ↑(val p H_') ∧ x ∈ ↑p
Tactic:
rintro ⟨ ⟨ x', hx'p ⟩, hx'H_', rfl ⟩
State after:
case a.intro.mk.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x' : E
hx'p : x' ∈ p
hx'H_' : { val := x', property := hx'p } ∈ ↑H_'
⊢ ↑{ val := x', property := hx'p } ∈ ↑(val p H_') ∧ ↑{ val := x', property := hx'p } ∈ ↑p

State before:
case a.intro.mk.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x' : E
hx'p : x' ∈ p
hx'H_' : { val := x', property := hx'p } ∈ ↑H_'
⊢ ↑{ val := x', property := hx'p } ∈ ↑(val p H_') ∧ ↑{ val := x', property := hx'p } ∈ ↑p
Tactic:
refine ⟨ ?_, hx'p ⟩
State after:
case a.intro.mk.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x' : E
hx'p : x' ∈ p
hx'H_' : { val := x', property := hx'p } ∈ ↑H_'
⊢ ↑{ val := x', property := hx'p } ∈ ↑(val p H_')

State before:
case a.intro.mk.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x' : E
hx'p : x' ∈ p
hx'H_' : { val := x', property := hx'p } ∈ ↑H_'
⊢ ↑{ val := x', property := hx'p } ∈ ↑(val p H_')
Tactic:
rw [Halfspace_mem, ← (this ⟨ x', hx'p ⟩), ← Halfspace.val_C p H_'] at hx'H_'
State after:
case a.intro.mk.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x' : E
hx'p : x' ∈ p
hx'H_' : ↑(val p H_').f ↑{ val := x', property := hx'p } ≤ (val p H_').α
⊢ ↑{ val := x', property := hx'p } ∈ ↑(val p H_')

State before:
case a.intro.mk.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
this : ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
x' : E
hx'p : x' ∈ p
hx'H_' : ↑(val p H_').f ↑{ val := x', property := hx'p } ≤ (val p H_').α
⊢ ↑{ val := x', property := hx'p } ∈ ↑(val p H_')
Tactic:
exact hx'H_'
State after:
no goals