have sq2_nonneg : (Real.sqrt 2) ≥ 0 := by
  apply Real.sqrt_nonneg
two_nonneg : 2 ≥ 0
sq2_pos : 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 ^ Real.sqrt 2) ^ Real.sqrt 2 = 2