Theorem: unitSphereDual_surj (src/Halfspace.lean)

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
⊢ ∀ (f : { f // ‖f‖ = 1 }), Function.Surjective ⇑↑f
Tactic:
intro f
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : { f // ‖f‖ = 1 }
⊢ Function.Surjective ⇑↑f

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : { f // ‖f‖ = 1 }
⊢ Function.Surjective ⇑↑f
Tactic:
apply LinearMap.surjective_of_ne_zero
State after:
case h
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : { f // ‖f‖ = 1 }
⊢ ↑↑f ≠ 0

State before:
case h
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : { f // ‖f‖ = 1 }
⊢ ↑↑f ≠ 0
Tactic:
intro h
State after:
case h
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : { f // ‖f‖ = 1 }
h : ↑↑f = 0
⊢ False

State before:
case h
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : { f // ‖f‖ = 1 }
h : ↑↑f = 0
⊢ False
Tactic:
rw [← ContinuousLinearMap.coe_zero, ContinuousLinearMap.coe_inj] at h
State after:
case h
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : { f // ‖f‖ = 1 }
h : ↑f = 0
⊢ False

State before:
case h
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : { f // ‖f‖ = 1 }
h : ↑f = 0
⊢ False
Tactic:
have := h ▸ f.2
State after:
case h
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : { f // ‖f‖ = 1 }
h : ↑f = 0
this : ‖0‖ = 1
⊢ False

State before:
case h
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : { f // ‖f‖ = 1 }
h : ↑f = 0
this : ‖0‖ = 1
⊢ False
Tactic:
simp only [norm_zero, zero_ne_one] at this
State after:
no goals