case inl
z x✝ y x : ℝ
h : 0 ≤ x
⊢ sqrt x = x ^ (1 / 2)

case inr
z x✝ y x : ℝ
h : x < 0
⊢ sqrt x = x ^ (1 / 2)
z x✝ y x : ℝ
⊢ sqrt x = x ^ (1 / 2)
obtain h | h := le_or_lt 0 x
case inl
z x✝ y x : ℝ
h : 0 ≤ x
⊢ x = x ^ (1 / 2 * ↑2)
case inl
z x✝ y x : ℝ
h : 0 ≤ x
⊢ sqrt x = x ^ (1 / 2)
rw [← mul_self_inj_of_nonneg (sqrt_nonneg _) (rpow_nonneg_of_nonneg h _), mul_self_sqrt h, ← sq,
  ← rpow_nat_cast, ← rpow_mul h]
no goals
case inl
z x✝ y x : ℝ
h : 0 ≤ x
⊢ x = x ^ (1 / 2 * ↑2)
norm_num
case this
z x✝ y x : ℝ
h : x < 0
⊢ 1 / 2 * π = π / 2

case inr
z x✝ y x : ℝ
h : x < 0
this : 1 / 2 * π = π / 2
⊢ sqrt x = x ^ (1 / 2)
case inr
z x✝ y x : ℝ
h : x < 0
⊢ sqrt x = x ^ (1 / 2)
have : 1 / (2 : ℝ) * π = π / (2 : ℝ)
case inr
z x✝ y x : ℝ
h : x < 0
this : 1 / 2 * π = π / 2
⊢ sqrt x = x ^ (1 / 2)
case this
z x✝ y x : ℝ
h : x < 0
⊢ 1 / 2 * π = π / 2

case inr
z x✝ y x : ℝ
h : x < 0
this : 1 / 2 * π = π / 2
⊢ sqrt x = x ^ (1 / 2)
ring
no goals
case inr
z x✝ y x : ℝ
h : x < 0
this : 1 / 2 * π = π / 2
⊢ sqrt x = x ^ (1 / 2)
rw [sqrt_eq_zero_of_nonpos h.le, rpow_def_of_neg h, this, cos_pi_div_two, MulZeroClass.mul_zero]