Theorem: Halfspace.val_f (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
⊢ ∀ (x : ↥p), ↑(val p H_').f ↑x = ↑H_'.f x
Tactic:
unfold val
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
⊢ ∀ (x : ↥p), ↑((fun H_ x => H_) (Classical.choose ⋯) ⋯).f ↑x = ↑H_'.f x

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
H_' : Halfspace ↥p
⊢ ∀ (x : ↥p), ↑((fun H_ x => H_) (Classical.choose ⋯) ⋯).f ↑x = ↑H_'.f x
Tactic:
exact (Classical.choose_spec (Halfspace.val_raw p H_')).1.1
State after:
no goals