sqrt (r : \C) * sqrt r

Stream: Is there code for X?

[Julian Berman]

Hi. Does something exist for:

import data.complex.basic
open real
lemma sqrtn {n : ℝ} {h : 0 ≤ n} : ((sqrt n : ℂ) * sqrt n) = n := begin
  ext; norm_num,
  unfold sqrt,
  simpa only [le_refl, coe_sqrt, mul_self_sqrt, max_eq_left_iff, coe_to_nnreal', or_true, le_max_iff],
end

[Yury G. Kudryashov]

Is it just exact_mod_cast sqrt_mul_self h?

[Yury G. Kudryashov]

Or rw [← of_real_mul, sqrt_mul_self h]

[Yury G. Kudryashov]

BTW, h should be an explicit argument.

[Julian Berman]

Aha, thank you! The rewrites indeed drop right in to my proof. I've never used exact_mod_cast before but seems like something I should know about too, appreciated.