rw [← Real.rpow_mul sq2_nonneg, Real.mul_self_sqrt two_nonneg]
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
sq2_nonneg : Real.sqrt 2 ≥ 0
⊢ (Real.sqrt 2 ^ Real.sqrt 2) ^ Real.sqrt 2 = 2
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
sq2_nonneg : Real.sqrt 2 ≥ 0
⊢ Real.sqrt 2 ^ 2 = 2