Theorem: unitSphereDual_neg (src/Halfspace.lean)

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : { f // ‖f‖ = 1 }
⊢ ↑(-f) = -↑f
Tactic:
change (⟨-f.1, _ ⟩: {f : (NormedSpace.Dual ℝ E) // norm f = 1}).1 = -f.1
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : { f // ‖f‖ = 1 }
⊢ ↑{ val := -↑f, property := ⋯ } = -↑f

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
f : { f // ‖f‖ = 1 }
⊢ ↑{ val := -↑f, property := ⋯ } = -↑f
Tactic:
simp
State after:
no goals