a : ℕ
⊢ 0 ≤ ↑(Nat.sqrt a) + 1 ∧ ↑a ≤ (↑(Nat.sqrt a) + 1) ^ 2
a : ℕ
⊢ sqrt ↑a ≤ ↑(Nat.sqrt a) + 1
rw [Real.sqrt_le_iff]
case left
a : ℕ
⊢ 0 ≤ ↑(Nat.sqrt a) + 1

case right
a : ℕ
⊢ ↑a ≤ (↑(Nat.sqrt a) + 1) ^ 2
a : ℕ
⊢ 0 ≤ ↑(Nat.sqrt a) + 1 ∧ ↑a ≤ (↑(Nat.sqrt a) + 1) ^ 2
constructor
case left
a : ℕ
⊢ 0 ≤ Nat.sqrt a + 1
case left
a : ℕ
⊢ 0 ≤ ↑(Nat.sqrt a) + 1
norm_cast
no goals
case left
a : ℕ
⊢ 0 ≤ Nat.sqrt a + 1
apply zero_le
case right
a : ℕ
⊢ a ≤ (Nat.sqrt a + 1) ^ 2
case right
a : ℕ
⊢ ↑a ≤ (↑(Nat.sqrt a) + 1) ^ 2
norm_cast
no goals
case right
a : ℕ
⊢ a ≤ (Nat.sqrt a + 1) ^ 2
exact le_of_lt (Nat.lt_succ_sqrt' a)