x : ℍ
⊢ Real.sqrt
      (inner (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 0)
              (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 0) +
            inner (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 1)
              (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 1) +
          inner (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 2)
            (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 2) +
        inner (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 3)
          (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 3)) =
    Real.sqrt (x.re ^ 2 + x.imI ^ 2 + x.imJ ^ 2 + x.imK ^ 2)
x : ℍ
⊢ ‖↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x)‖ = ‖x‖
rw [norm_eq_sqrt_real_inner, norm_eq_sqrt_real_inner, inner_self, normSq_def', PiLp.inner_apply,
  Fin.sum_univ_four]
x : ℍ
⊢ Real.sqrt
      (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 0 ^ 2 +
            ↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 1 ^ 2 +
          ↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 2 ^ 2 +
        ↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 3 ^ 2) =
    Real.sqrt (x.re ^ 2 + x.imI ^ 2 + x.imJ ^ 2 + x.imK ^ 2)
x : ℍ
⊢ Real.sqrt
      (inner (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 0)
              (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 0) +
            inner (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 1)
              (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 1) +
          inner (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 2)
            (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 2) +
        inner (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 3)
          (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 3)) =
    Real.sqrt (x.re ^ 2 + x.imI ^ 2 + x.imJ ^ 2 + x.imK ^ 2)
simp_rw [IsROrC.inner_apply, starRingEnd_apply, star_trivial, ← sq]
no goals
x : ℍ
⊢ Real.sqrt
      (↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 0 ^ 2 +
            ↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 1 ^ 2 +
          ↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 2 ^ 2 +
        ↑(PiLp.equiv 2 fun x => ℝ).symm (↑(equivTuple ℝ) x) 3 ^ 2) =
    Real.sqrt (x.re ^ 2 + x.imI ^ 2 + x.imJ ^ 2 + x.imK ^ 2)
rfl