[GOAL]
n : ℕ
⊢ Nat.IsSqrt n (sqrt n)
[PROOFSTEP]
match n with
| 0 => simp [IsSqrt]
| 1 => simp [IsSqrt]
| n + 2 =>
  have h : ¬(n + 2) ≤ 1 := by simp
  simp only [IsSqrt, sqrt, h, ite_false]
  refine ⟨sqrt.iter_sq_le _ _, sqrt.lt_iter_succ_sq _ _ ?_⟩
  simp only [mul_add, add_mul, one_mul, mul_one, ← add_assoc]
  rw [lt_add_one_iff, add_assoc, ← mul_two]
  refine le_trans (div_add_mod' (n + 2) 2).ge ?_
  rw [add_comm, add_le_add_iff_right, add_mod_right]
  simp only [zero_lt_two, add_div_right, succ_mul_succ_eq]
  refine le_trans (b := 1) ?_ ?_
  · exact (lt_succ.1 $ mod_lt n zero_lt_two)
  · simp only [le_add_iff_nonneg_left]; exact zero_le _
[GOAL]
n : ℕ
⊢ Nat.IsSqrt 0 (sqrt 0)
[PROOFSTEP]
simp [IsSqrt]
[GOAL]
n : ℕ
⊢ Nat.IsSqrt 1 (sqrt 1)
[PROOFSTEP]
simp [IsSqrt]
[GOAL]
n✝ n : ℕ
⊢ Nat.IsSqrt (n + 2) (sqrt (n + 2))
[PROOFSTEP]
have h : ¬(n + 2) ≤ 1 := by simp
[GOAL]
n✝ n : ℕ
⊢ ¬n + 2 ≤ 1
[PROOFSTEP]
simp
[GOAL]
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ Nat.IsSqrt (n + 2) (sqrt (n + 2))
[PROOFSTEP]
simp only [IsSqrt, sqrt, h, ite_false]
[GOAL]
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ sqrt.iter (n + 2) ((n + 2) / 2) * sqrt.iter (n + 2) ((n + 2) / 2) ≤ n + 2 ∧
    n + 2 < (sqrt.iter (n + 2) ((n + 2) / 2) + 1) * (sqrt.iter (n + 2) ((n + 2) / 2) + 1)
[PROOFSTEP]
refine ⟨sqrt.iter_sq_le _ _, sqrt.lt_iter_succ_sq _ _ ?_⟩
[GOAL]
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n + 2 < ((n + 2) / 2 + 1) * ((n + 2) / 2 + 1)
[PROOFSTEP]
simp only [mul_add, add_mul, one_mul, mul_one, ← add_assoc]
[GOAL]
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n + 2 < (n + 2) / 2 * ((n + 2) / 2) + (n + 2) / 2 + (n + 2) / 2 + 1
[PROOFSTEP]
rw [lt_add_one_iff, add_assoc, ← mul_two]
[GOAL]
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n + 2 ≤ (n + 2) / 2 * ((n + 2) / 2) + (n + 2) / 2 * 2
[PROOFSTEP]
refine le_trans (div_add_mod' (n + 2) 2).ge ?_
[GOAL]
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ (n + 2) / 2 * 2 + (n + 2) % 2 ≤ (n + 2) / 2 * ((n + 2) / 2) + (n + 2) / 2 * 2
[PROOFSTEP]
rw [add_comm, add_le_add_iff_right, add_mod_right]
[GOAL]
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n % 2 ≤ (n + 2) / 2 * ((n + 2) / 2)
[PROOFSTEP]
simp only [zero_lt_two, add_div_right, succ_mul_succ_eq]
[GOAL]
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n % 2 ≤ n / 2 * (n / 2) + n / 2 + n / 2 + 1
[PROOFSTEP]
refine le_trans (b := 1) ?_ ?_
[GOAL]
case refine_1
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n % 2 ≤ 1
[PROOFSTEP]
exact (lt_succ.1 $ mod_lt n zero_lt_two)
[GOAL]
case refine_2
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ 1 ≤ n / 2 * (n / 2) + n / 2 + n / 2 + 1
[PROOFSTEP]
simp only [le_add_iff_nonneg_left]
[GOAL]
case refine_2
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ 0 ≤ n / 2 * (n / 2) + n / 2 + n / 2
[PROOFSTEP]
exact zero_le _
[GOAL]
n : ℕ
⊢ n ≤ sqrt n * sqrt n + sqrt n + sqrt n
[PROOFSTEP]
rw [← succ_mul]
[GOAL]
n : ℕ
⊢ n ≤ succ (sqrt n) * sqrt n + sqrt n
[PROOFSTEP]
exact le_of_lt_succ (lt_succ_sqrt n)
[GOAL]
m n : ℕ
⊢ m ≤ sqrt n ↔ m ^ 2 ≤ n
[PROOFSTEP]
simpa only [pow_two] using le_sqrt
[GOAL]
n : ℕ
h : sqrt n = 0
⊢ sqrt n < 1
[PROOFSTEP]
rw [h]
[GOAL]
n : ℕ
h : sqrt n = 0
⊢ 0 < 1
[PROOFSTEP]
decide
[GOAL]
n : ℕ
⊢ n = 0 → sqrt n = 0
[PROOFSTEP]
rintro rfl
[GOAL]
⊢ sqrt 0 = 0
[PROOFSTEP]
simp
[GOAL]
n q : ℕ
⊢ q = sqrt n ↔ q ^ 2 ≤ n ∧ n < (q + 1) ^ 2
[PROOFSTEP]
simpa only [pow_two] using eq_sqrt
[GOAL]
n : ℕ
h : sqrt n = 1
⊢ sqrt n < 2
[PROOFSTEP]
rw [h]
[GOAL]
n : ℕ
h : sqrt n = 1
⊢ 1 < 2
[PROOFSTEP]
decide
[GOAL]
n : ℕ
h : 1 < n
⊢ n < n * n
[PROOFSTEP]
have := Nat.mul_lt_mul_of_pos_left h (lt_of_succ_lt h)
[GOAL]
n : ℕ
h : 1 < n
this : n * 1 < n * n
⊢ n < n * n
[PROOFSTEP]
rwa [mul_one] at this 
[GOAL]
n a : ℕ
h : a ≤ n + n
⊢ n * n + a < succ n * succ n
[PROOFSTEP]
rw [succ_mul, mul_succ, add_succ, add_assoc]
[GOAL]
n a : ℕ
h : a ≤ n + n
⊢ n * n + a < succ (n * n + (n + n))
[PROOFSTEP]
exact lt_succ_of_le (Nat.add_le_add_left h _)
[GOAL]
n : ℕ
⊢ sqrt n * sqrt n + sqrt n ≤ Nat.mul (succ (succ (sqrt n))) (succ (sqrt n))
[PROOFSTEP]
refine' add_le_add (Nat.mul_le_mul_right _ _) _
[GOAL]
case refine'_1
n : ℕ
⊢ sqrt n ≤ succ (succ (sqrt n))
[PROOFSTEP]
exact Nat.le_add_right _ 2
[GOAL]
case refine'_2
n : ℕ
⊢ sqrt n ≤ succ (succ (sqrt n))
[PROOFSTEP]
exact Nat.le_add_right _ 2
[GOAL]
x : ℕ
x✝ : ∃ n, n * n = x
n : ℕ
hn : n * n = x
⊢ sqrt x * sqrt x = x
[PROOFSTEP]
rw [← hn, sqrt_eq]
[GOAL]
x : ℕ
⊢ (∃ n, n ^ 2 = x) ↔ sqrt x ^ 2 = x
[PROOFSTEP]
simpa only [pow_two] using exists_mul_self x
[GOAL]
n m : ℕ
hl : m * m < n
hr : n < (m + 1) * (m + 1)
⊢ ¬∃ t, t * t = n
[PROOFSTEP]
rintro ⟨t, rfl⟩
[GOAL]
case intro
m t : ℕ
hl : m * m < t * t
hr : t * t < (m + 1) * (m + 1)
⊢ False
[PROOFSTEP]
have h1 : m < t := Nat.mul_self_lt_mul_self_iff.mpr hl
[GOAL]
case intro
m t : ℕ
hl : m * m < t * t
hr : t * t < (m + 1) * (m + 1)
h1 : m < t
⊢ False
[PROOFSTEP]
have h2 : t < m + 1 := Nat.mul_self_lt_mul_self_iff.mpr hr
[GOAL]
case intro
m t : ℕ
hl : m * m < t * t
hr : t * t < (m + 1) * (m + 1)
h1 : m < t
h2 : t < m + 1
⊢ False
[PROOFSTEP]
exact (not_lt_of_ge <| le_of_lt_succ h2) h1
[GOAL]
n m : ℕ
hl : m ^ 2 < n
hr : n < (m + 1) ^ 2
⊢ ¬∃ t, t ^ 2 = n
[PROOFSTEP]
simpa only [pow_two] using not_exists_sq (by simpa only [pow_two] using hl) (by simpa only [pow_two] using hr)
[GOAL]
n m : ℕ
hl : m ^ 2 < n
hr : n < (m + 1) ^ 2
⊢ ?m.11228 * ?m.11228 < n
[PROOFSTEP]
simpa only [pow_two] using hl
[GOAL]
n m : ℕ
hl : m ^ 2 < n
hr : n < (m + 1) ^ 2
⊢ n < (m + 1) * (m + 1)
[PROOFSTEP]
simpa only [pow_two] using hr
