have sq2_pos : (Real.sqrt 2) > 0 := by simp [Real.sqrt_pos]
two_nonneg : 2 ≥ 0
⊢ (Real.sqrt 2 ^ Real.sqrt 2) ^ Real.sqrt 2 = 2
two_nonneg : 2 ≥ 0
sq2_pos : Real.sqrt 2 > 0
⊢ (Real.sqrt 2 ^ Real.sqrt 2) ^ Real.sqrt 2 = 2