[GOAL]
x y r : ℕ
hr : y * y + r = x
hle : Nat.ble r (2 * y) = true
⊢ Nat.sqrt x = y
[PROOFSTEP]
rw [← hr, ← pow_two]
[GOAL]
x y r : ℕ
hr : y * y + r = x
hle : Nat.ble r (2 * y) = true
⊢ Nat.sqrt (y ^ 2 + r) = y
[PROOFSTEP]
rw [two_mul] at hle 
[GOAL]
x y r : ℕ
hr : y * y + r = x
hle : Nat.ble r (y + y) = true
⊢ Nat.sqrt (y ^ 2 + r) = y
[PROOFSTEP]
exact Nat.sqrt_add_eq' _ (Nat.le_of_ble_eq_true hle)
