Theorem: Halfspace.val_raw (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
⊢ ∃ H_, ((∀ (x : ↥p), ↑H_.f ↑x = ↑H_'.f x) ∧ ‖↑H_.f‖ = ‖↑H_'.f‖) ∧ H_.α = H_'.α
Tactic:
rcases H_' with ⟨ ⟨ f, hf ⟩, C ⟩
State after:
case mk.mk
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
C : ℝ
f : NormedSpace.Dual ℝ ↥p
hf : ‖f‖ = 1
⊢ ∃ H_,
    ((∀ (x : ↥p), ↑H_.f ↑x = ↑{ f := { val := f, property := hf }, α := C }.f x) ∧
        ‖↑H_.f‖ = ‖↑{ f := { val := f, property := hf }, α := C }.f‖) ∧
      H_.α = { f := { val := f, property := hf }, α := C }.α

State before:
case mk.mk
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
C : ℝ
f : NormedSpace.Dual ℝ ↥p
hf : ‖f‖ = 1
⊢ ∃ H_,
    ((∀ (x : ↥p), ↑H_.f ↑x = ↑{ f := { val := f, property := hf }, α := C }.f x) ∧
        ‖↑H_.f‖ = ‖↑{ f := { val := f, property := hf }, α := C }.f‖) ∧
      H_.α = { f := { val := f, property := hf }, α := C }.α
Tactic:
choose g hg using Real.exists_extension_norm_eq p f
State after:
case mk.mk
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
C : ℝ
f : NormedSpace.Dual ℝ ↥p
hf : ‖f‖ = 1
g : E →L[ℝ] ℝ
hg : (∀ (x : ↥p), g ↑x = f x) ∧ ‖g‖ = ‖f‖
⊢ ∃ H_,
    ((∀ (x : ↥p), ↑H_.f ↑x = ↑{ f := { val := f, property := hf }, α := C }.f x) ∧
        ‖↑H_.f‖ = ‖↑{ f := { val := f, property := hf }, α := C }.f‖) ∧
      H_.α = { f := { val := f, property := hf }, α := C }.α

State before:
case mk.mk
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
p : Subspace ℝ E
inst✝ : CompleteSpace ↥p
C : ℝ
f : NormedSpace.Dual ℝ ↥p
hf : ‖f‖ = 1
g : E →L[ℝ] ℝ
hg : (∀ (x : ↥p), g ↑x = f x) ∧ ‖g‖ = ‖f‖
⊢ ∃ H_,
    ((∀ (x : ↥p), ↑H_.f ↑x = ↑{ f := { val := f, property := hf }, α := C }.f x) ∧
        ‖↑H_.f‖ = ‖↑{ f := { val := f, property := hf }, α := C }.f‖) ∧
      H_.α = { f := { val := f, property := hf }, α := C }.α
Tactic:
exact ⟨ ⟨ ⟨ g, hg.2 ▸ hf ⟩, C ⟩, hg, rfl ⟩
State after:
no goals