Theorem: Halfspace.val_C (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_').α = H_'.α
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
⊢ ((fun H_ x => H_) (Classical.choose ⋯) ⋯).α = H_'.α

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