chore(NumberTheory/Padics/Complex): remove an erw (leanprover-community#38774)

- rewrites `norm_eq_norm'` to expand `Valuation.restrict_def`, `embedding_restrict₀`, and `PadicAlgCl.valuation_coe` inside `simp only`

Extracted from leanprover-community#38415

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

Author: yuanyi-350

Mathlib/NumberTheory/Padics/Complex.lean

@@ -210,9 +210,7 @@ theorem norm_eq_norm' : (‖·‖ : ℂ_[p] → ℝ) = Valued.v.norm := by
     letI := S.toNonUnitalSeminormedRing.toSeminormedAddCommGroup.toSeminormedAddGroup
     exact @uniformContinuous_norm ℂ_[p] this
   · intro x
-    simp only [Valued.v.norm_def, RankOne.hom_eq_embedding]
-    erw [embedding_restrict (PadicComplex.valued p).v x, valuation_extends]
-    exact (PadicAlgCl.valuation_coe p x).symm
+    simp [Valued.v.norm_def, restrict_def]
 
 /-- The norm on `ℂ_[p]` is compatible with the valuation. -/
 theorem norm_eq_norm (x : ℂ_[p]) : ‖x‖ = Valued.v.norm x := by