no goals
n : ℕ
⊢ Nat.IsSqrt 0 (sqrt 0)
simp [IsSqrt]
no goals
n : ℕ
⊢ Nat.IsSqrt 1 (sqrt 1)
simp [IsSqrt]
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ Nat.IsSqrt (n + 2) (sqrt (n + 2))
n✝ n : ℕ
⊢ Nat.IsSqrt (n + 2) (sqrt (n + 2))
have h : ¬ (n + 2) ≤ 1 := by simp
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)
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ Nat.IsSqrt (n + 2) (sqrt (n + 2))
simp only [IsSqrt, sqrt, h, ite_false]
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n + 2 < ((n + 2) / 2 + 1) * ((n + 2) / 2 + 1)
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)
refine ⟨sqrt.iter_sq_le _ _, sqrt.lt_iter_succ_sq _ _ ?_⟩
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n + 2 < (n + 2) / 2 * ((n + 2) / 2) + (n + 2) / 2 + (n + 2) / 2 + 1
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n + 2 < ((n + 2) / 2 + 1) * ((n + 2) / 2 + 1)
simp only [mul_add, add_mul, one_mul, mul_one, ← add_assoc]
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n + 2 ≤ (n + 2) / 2 * ((n + 2) / 2) + (n + 2) / 2 * 2
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n + 2 < (n + 2) / 2 * ((n + 2) / 2) + (n + 2) / 2 + (n + 2) / 2 + 1
rw [lt_add_one_iff, add_assoc, ← mul_two]
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ (n + 2) / 2 * 2 + (n + 2) % 2 ≤ (n + 2) / 2 * ((n + 2) / 2) + (n + 2) / 2 * 2
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n + 2 ≤ (n + 2) / 2 * ((n + 2) / 2) + (n + 2) / 2 * 2
refine le_trans (div_add_mod' (n + 2) 2).ge ?_
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n % 2 ≤ (n + 2) / 2 * ((n + 2) / 2)
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ (n + 2) / 2 * 2 + (n + 2) % 2 ≤ (n + 2) / 2 * ((n + 2) / 2) + (n + 2) / 2 * 2
rw [add_comm, add_le_add_iff_right, add_mod_right]
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n % 2 ≤ n / 2 * (n / 2) + n / 2 + n / 2 + 1
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n % 2 ≤ (n + 2) / 2 * ((n + 2) / 2)
simp only [zero_lt_two, add_div_right, succ_mul_succ_eq]
case refine_1
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n % 2 ≤ 1

case refine_2
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ 1 ≤ n / 2 * (n / 2) + n / 2 + n / 2 + 1
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n % 2 ≤ n / 2 * (n / 2) + n / 2 + n / 2 + 1
refine le_trans (b := 1) ?_ ?_
no goals
n✝ n : ℕ
⊢ ¬n + 2 ≤ 1
simp
no goals
case refine_1
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ n % 2 ≤ 1
exact (lt_succ.1 $ mod_lt n zero_lt_two)
case refine_2
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ 0 ≤ n / 2 * (n / 2) + n / 2 + n / 2
case refine_2
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ 1 ≤ n / 2 * (n / 2) + n / 2 + n / 2 + 1
simp only [le_add_iff_nonneg_left]
no goals
case refine_2
n✝ n : ℕ
h : ¬n + 2 ≤ 1
⊢ 0 ≤ n / 2 * (n / 2) + n / 2 + n / 2
exact zero_le _