rw [Nat.le_sqrt]
n : ℕ
hn : 100 ≤ n
hn' : 1 ≤ (n + 1).sqrt
h₁ : (n + 1).sqrt ^ 2 ≤ n + 1
h₂ : n + 1 + 1 ≤ ((n + 1).sqrt + 1) ^ 2
⊢ 10 ≤ (n + 1).sqrt
n : ℕ
hn : 100 ≤ n
hn' : 1 ≤ (n + 1).sqrt
h₁ : (n + 1).sqrt ^ 2 ≤ n + 1
h₂ : n + 1 + 1 ≤ ((n + 1).sqrt + 1) ^ 2
⊢ 10 * 10 ≤ n + 1