case intro
E : Type ?u.1183703
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℝ
hz : 0 ≤ ↑z
⊢ ↑z = ↑‖↑z‖
E : Type ?u.1183703
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
hz : 0 ≤ z
⊢ z = ↑‖z‖
lift z to ℝ using hz.2.symm
no goals
case intro
E : Type ?u.1183703
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℝ
hz : 0 ≤ ↑z
⊢ ↑z = ↑‖↑z‖
rw [norm_eq_abs, abs_ofReal, _root_.abs_of_nonneg (id hz.1 : 0 ≤ z)]