no goals
q : ℚ
H1 : Rat.sqrt q * Rat.sqrt q = q
⊢ ↑(Rat.sqrt q) = Real.sqrt ↑q
rw [← H1, cast_mul, sqrt_mul_self (cast_nonneg.2 <| Rat.sqrt_nonneg q), sqrt_eq,
  abs_of_nonneg (Rat.sqrt_nonneg q)]
q : ℚ
H1 : ¬Rat.sqrt q * Rat.sqrt q = q
H2 : 0 ≤ q
x✝ : Real.sqrt ↑q ∈ Set.range Rat.cast
r : ℚ
hr : Real.sqrt ↑q = ↑r
⊢ 0 ≤ ↑r
q : ℚ
H1 : ¬Rat.sqrt q * Rat.sqrt q = q
H2 : 0 ≤ q
x✝ : Real.sqrt ↑q ∈ Set.range Rat.cast
r : ℚ
hr : ↑r = Real.sqrt ↑q
⊢ r * r = q
rwa [eq_comm, sqrt_eq_iff_mul_self_eq (cast_nonneg.2 H2), ← cast_mul,
      Rat.cast_inj] at hr
q : ℚ
H1 : ¬Rat.sqrt q * Rat.sqrt q = q
H2 : 0 ≤ q
x✝ : Real.sqrt ↑q ∈ Set.range Rat.cast
r : ℚ
hr : Real.sqrt ↑q = ↑r
⊢ 0 ≤ Real.sqrt ↑q
q : ℚ
H1 : ¬Rat.sqrt q * Rat.sqrt q = q
H2 : 0 ≤ q
x✝ : Real.sqrt ↑q ∈ Set.range Rat.cast
r : ℚ
hr : Real.sqrt ↑q = ↑r
⊢ 0 ≤ ↑r
rw [← hr]
no goals
q : ℚ
H1 : ¬Rat.sqrt q * Rat.sqrt q = q
H2 : 0 ≤ q
x✝ : Real.sqrt ↑q ∈ Set.range Rat.cast
r : ℚ
hr : Real.sqrt ↑q = ↑r
⊢ 0 ≤ Real.sqrt ↑q
exact Real.sqrt_nonneg _
q : ℚ
H1 : ¬Rat.sqrt q * Rat.sqrt q = q
H2 : ¬0 ≤ q
⊢ 0 = Real.sqrt ↑q
q : ℚ
H1 : ¬Rat.sqrt q * Rat.sqrt q = q
H2 : ¬0 ≤ q
⊢ ↑0 = Real.sqrt ↑q
rw [cast_zero]
no goals
q : ℚ
H1 : ¬Rat.sqrt q * Rat.sqrt q = q
H2 : ¬0 ≤ q
⊢ 0 = Real.sqrt ↑q
exact (sqrt_eq_zero_of_nonpos (Rat.cast_nonpos.2 <| le_of_not_le H2)).symm