a : ℕ
⊢ ↑(Nat.sqrt a) ^ 2 ≤ ↑a
a : ℕ
⊢ ↑(Nat.sqrt a) ≤ sqrt ↑a
rw [Real.le_sqrt (Nat.cast_nonneg _) (Nat.cast_nonneg _)]
a : ℕ
⊢ Nat.sqrt a ^ 2 ≤ a
a : ℕ
⊢ ↑(Nat.sqrt a) ^ 2 ≤ ↑a
norm_cast
no goals
a : ℕ
⊢ Nat.sqrt a ^ 2 ≤ a
exact Nat.sqrt_le' a