Theorem: norm_eq_duals_iSup (Ray/Hartogs/Duals.lean)

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
x : E
⊢ ‖x‖ = ⨆ n, ‖(duals n) x‖
Tactic:
have h := norm_eq_duals_supr' (@monotone_id ℝ _) LipschitzWith.id x
State after:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
x : E
h : id ‖x‖ = ⨆ n, id ‖(duals n) x‖
⊢ ‖x‖ = ⨆ n, ‖(duals n) x‖

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
x : E
h : id ‖x‖ = ⨆ n, id ‖(duals n) x‖
⊢ ‖x‖ = ⨆ n, ‖(duals n) x‖
Tactic:
simpa only [Complex.norm_eq_abs] using h
State after:
no goals