[GOAL]
k x y : ℕ
h : x ≤ y / k
⊢ x * k ≤ y
[PROOFSTEP]
by_cases hk : k = 0
[GOAL]
case pos
k x y : ℕ
h : x ≤ y / k
hk : k = 0
⊢ x * k ≤ y
case neg k x y : ℕ h : x ≤ y / k hk : ¬k = 0 ⊢ x * k ≤ y
[PROOFSTEP]
case pos => rw [hk, mul_zero]; exact zero_le _
[GOAL]
k x y : ℕ
h : x ≤ y / k
hk : k = 0
⊢ x * k ≤ y
[PROOFSTEP]
case pos => rw [hk, mul_zero]; exact zero_le _
[GOAL]
k x y : ℕ
h : x ≤ y / k
hk : k = 0
⊢ x * k ≤ y
[PROOFSTEP]
rw [hk, mul_zero]
[GOAL]
k x y : ℕ
h : x ≤ y / k
hk : k = 0
⊢ 0 ≤ y
[PROOFSTEP]
exact zero_le _
[GOAL]
case neg
k x y : ℕ
h : x ≤ y / k
hk : ¬k = 0
⊢ x * k ≤ y
[PROOFSTEP]
case neg => rwa [← le_div_iff_mul_le (pos_iff_ne_zero.2 hk)]
[GOAL]
k x y : ℕ
h : x ≤ y / k
hk : ¬k = 0
⊢ x * k ≤ y
[PROOFSTEP]
case neg => rwa [← le_div_iff_mul_le (pos_iff_ne_zero.2 hk)]
[GOAL]
k x y : ℕ
h : x ≤ y / k
hk : ¬k = 0
⊢ x * k ≤ y
[PROOFSTEP]
rwa [← le_div_iff_mul_le (pos_iff_ne_zero.2 hk)]
[GOAL]
a b c d : ℕ
⊢ a / b * (c / d) ≤ a * c / (b * d)
[PROOFSTEP]
by_cases hb : b = 0
[GOAL]
case pos
a b c d : ℕ
hb : b = 0
⊢ a / b * (c / d) ≤ a * c / (b * d)
case neg a b c d : ℕ hb : ¬b = 0 ⊢ a / b * (c / d) ≤ a * c / (b * d)
[PROOFSTEP]
case pos => simp [hb]
[GOAL]
a b c d : ℕ
hb : b = 0
⊢ a / b * (c / d) ≤ a * c / (b * d)
[PROOFSTEP]
case pos => simp [hb]
[GOAL]
a b c d : ℕ
hb : b = 0
⊢ a / b * (c / d) ≤ a * c / (b * d)
[PROOFSTEP]
simp [hb]
[GOAL]
case neg
a b c d : ℕ
hb : ¬b = 0
⊢ a / b * (c / d) ≤ a * c / (b * d)
[PROOFSTEP]
by_cases hd : d = 0
[GOAL]
case pos
a b c d : ℕ
hb : ¬b = 0
hd : d = 0
⊢ a / b * (c / d) ≤ a * c / (b * d)
case neg a b c d : ℕ hb : ¬b = 0 hd : ¬d = 0 ⊢ a / b * (c / d) ≤ a * c / (b * d)
[PROOFSTEP]
case pos => simp [hd]
[GOAL]
a b c d : ℕ
hb : ¬b = 0
hd : d = 0
⊢ a / b * (c / d) ≤ a * c / (b * d)
[PROOFSTEP]
case pos => simp [hd]
[GOAL]
a b c d : ℕ
hb : ¬b = 0
hd : d = 0
⊢ a / b * (c / d) ≤ a * c / (b * d)
[PROOFSTEP]
simp [hd]
[GOAL]
case neg
a b c d : ℕ
hb : ¬b = 0
hd : ¬d = 0
⊢ a / b * (c / d) ≤ a * c / (b * d)
[PROOFSTEP]
have hbd : b * d ≠ 0 := mul_ne_zero hb hd
[GOAL]
case neg
a b c d : ℕ
hb : ¬b = 0
hd : ¬d = 0
hbd : b * d ≠ 0
⊢ a / b * (c / d) ≤ a * c / (b * d)
[PROOFSTEP]
rw [le_div_iff_mul_le (Nat.pos_of_ne_zero hbd)]
[GOAL]
case neg
a b c d : ℕ
hb : ¬b = 0
hd : ¬d = 0
hbd : b * d ≠ 0
⊢ a / b * (c / d) * (b * d) ≤ a * c
[PROOFSTEP]
transitivity ((a / b) * b) * ((c / d) * d)
[GOAL]
case neg.a
a b c d : ℕ
hb : ¬b = 0
hd : ¬d = 0
hbd : b * d ≠ 0
⊢ a / b * (c / d) * (b * d) ≤ a / b * b * (c / d * d)
[PROOFSTEP]
apply le_of_eq
[GOAL]
case neg.a.a
a b c d : ℕ
hb : ¬b = 0
hd : ¬d = 0
hbd : b * d ≠ 0
⊢ a / b * (c / d) * (b * d) = a / b * b * (c / d * d)
[PROOFSTEP]
simp only [mul_assoc, mul_left_comm]
[GOAL]
case neg.a
a b c d : ℕ
hb : ¬b = 0
hd : ¬d = 0
hbd : b * d ≠ 0
⊢ a / b * b * (c / d * d) ≤ a * c
[PROOFSTEP]
apply Nat.mul_le_mul
[GOAL]
case neg.a.h₁
a b c d : ℕ
hb : ¬b = 0
hd : ¬d = 0
hbd : b * d ≠ 0
⊢ a / b * b ≤ a
[PROOFSTEP]
apply div_mul_le_self
[GOAL]
case neg.a.h₂
a b c d : ℕ
hb : ¬b = 0
hd : ¬d = 0
hbd : b * d ≠ 0
⊢ c / d * d ≤ c
[PROOFSTEP]
apply div_mul_le_self
[GOAL]
n k : ℕ
⊢ let iter_next := fun n guess => (guess + n / guess) / 2;
  sqrt.iter n k ≤ iter_next n (sqrt.iter n k)
[PROOFSTEP]
intro iter_next
[GOAL]
n k : ℕ
iter_next : ℕ → ℕ → ℕ := fun n guess => (guess + n / guess) / 2
⊢ sqrt.iter n k ≤ iter_next n (sqrt.iter n k)
[PROOFSTEP]
unfold sqrt.iter
[GOAL]
n k : ℕ
iter_next : ℕ → ℕ → ℕ := fun n guess => (guess + n / guess) / 2
⊢ (let next := (k + n / k) / 2;
    if _h : next < k then sqrt.iter n next else k) ≤
    iter_next n
      (let next := (k + n / k) / 2;
      if _h : next < k then sqrt.iter n next else k)
[PROOFSTEP]
by_cases h : (k + n / k) / 2 < k
[GOAL]
case pos
n k : ℕ
iter_next : ℕ → ℕ → ℕ := fun n guess => (guess + n / guess) / 2
h : (k + n / k) / 2 < k
⊢ (let next := (k + n / k) / 2;
    if _h : next < k then sqrt.iter n next else k) ≤
    iter_next n
      (let next := (k + n / k) / 2;
      if _h : next < k then sqrt.iter n next else k)
case neg
n k : ℕ
iter_next : ℕ → ℕ → ℕ := fun n guess => (guess + n / guess) / 2
h : ¬(k + n / k) / 2 < k
⊢ (let next := (k + n / k) / 2;
    if _h : next < k then sqrt.iter n next else k) ≤
    iter_next n
      (let next := (k + n / k) / 2;
      if _h : next < k then sqrt.iter n next else k)
[PROOFSTEP]
case pos => simp [if_pos h]; exact iter_fp_bound _ _
[GOAL]
n k : ℕ
iter_next : ℕ → ℕ → ℕ := fun n guess => (guess + n / guess) / 2
h : (k + n / k) / 2 < k
⊢ (let next := (k + n / k) / 2;
    if _h : next < k then sqrt.iter n next else k) ≤
    iter_next n
      (let next := (k + n / k) / 2;
      if _h : next < k then sqrt.iter n next else k)
[PROOFSTEP]
case pos => simp [if_pos h]; exact iter_fp_bound _ _
[GOAL]
n k : ℕ
iter_next : ℕ → ℕ → ℕ := fun n guess => (guess + n / guess) / 2
h : (k + n / k) / 2 < k
⊢ (let next := (k + n / k) / 2;
    if _h : next < k then sqrt.iter n next else k) ≤
    iter_next n
      (let next := (k + n / k) / 2;
      if _h : next < k then sqrt.iter n next else k)
[PROOFSTEP]
simp [if_pos h]
[GOAL]
n k : ℕ
iter_next : ℕ → ℕ → ℕ := fun n guess => (guess + n / guess) / 2
h : (k + n / k) / 2 < k
⊢ sqrt.iter n ((k + n / k) / 2) ≤ (sqrt.iter n ((k + n / k) / 2) + n / sqrt.iter n ((k + n / k) / 2)) / 2
[PROOFSTEP]
exact iter_fp_bound _ _
[GOAL]
case neg
n k : ℕ
iter_next : ℕ → ℕ → ℕ := fun n guess => (guess + n / guess) / 2
h : ¬(k + n / k) / 2 < k
⊢ (let next := (k + n / k) / 2;
    if _h : next < k then sqrt.iter n next else k) ≤
    iter_next n
      (let next := (k + n / k) / 2;
      if _h : next < k then sqrt.iter n next else k)
[PROOFSTEP]
case neg => simp [if_neg h]; exact Nat.le_of_not_lt h
[GOAL]
n k : ℕ
iter_next : ℕ → ℕ → ℕ := fun n guess => (guess + n / guess) / 2
h : ¬(k + n / k) / 2 < k
⊢ (let next := (k + n / k) / 2;
    if _h : next < k then sqrt.iter n next else k) ≤
    iter_next n
      (let next := (k + n / k) / 2;
      if _h : next < k then sqrt.iter n next else k)
[PROOFSTEP]
case neg => simp [if_neg h]; exact Nat.le_of_not_lt h
[GOAL]
n k : ℕ
iter_next : ℕ → ℕ → ℕ := fun n guess => (guess + n / guess) / 2
h : ¬(k + n / k) / 2 < k
⊢ (let next := (k + n / k) / 2;
    if _h : next < k then sqrt.iter n next else k) ≤
    iter_next n
      (let next := (k + n / k) / 2;
      if _h : next < k then sqrt.iter n next else k)
[PROOFSTEP]
simp [if_neg h]
[GOAL]
n k : ℕ
iter_next : ℕ → ℕ → ℕ := fun n guess => (guess + n / guess) / 2
h : ¬(k + n / k) / 2 < k
⊢ k ≤ (k + n / k) / 2
[PROOFSTEP]
exact Nat.le_of_not_lt h
[GOAL]
x✝ : ℕ
⊢ 4 * 0 * x✝ ≤ (0 + x✝) * (0 + x✝)
[PROOFSTEP]
rw [mul_zero, zero_mul]
[GOAL]
x✝ : ℕ
⊢ 0 ≤ (0 + x✝) * (0 + x✝)
[PROOFSTEP]
exact zero_le _
[GOAL]
x✝ : ℕ
⊢ 4 * x✝ * 0 ≤ (x✝ + 0) * (x✝ + 0)
[PROOFSTEP]
rw [mul_zero]
[GOAL]
x✝ : ℕ
⊢ 0 ≤ (x✝ + 0) * (x✝ + 0)
[PROOFSTEP]
exact zero_le _
[GOAL]
a b : ℕ
⊢ 4 * (a + 1) * (b + 1) ≤ (a + 1 + (b + 1)) * (a + 1 + (b + 1))
[PROOFSTEP]
have ih := add_le_add_right (@AM_GM a b) 4
[GOAL]
a b : ℕ
ih : 4 * a * b + 4 ≤ (a + b) * (a + b) + 4
⊢ 4 * (a + 1) * (b + 1) ≤ (a + 1 + (b + 1)) * (a + 1 + (b + 1))
[PROOFSTEP]
simp only [mul_add, add_mul, show (4 : ℕ) = 1 + 1 + 1 + 1 from rfl, one_mul, mul_one] at ih ⊢
[GOAL]
a b : ℕ
ih : a * b + a * b + a * b + a * b + (1 + 1 + 1 + 1) ≤ a * a + b * a + (a * b + b * b) + (1 + 1 + 1 + 1)
⊢ a * b + a * b + a * b + a * b + (b + b + b + b) + (a + a + a + a + (1 + 1 + 1 + 1)) ≤
    a * a + a + (b * a + a) + (a + 1 + (b + 1)) + (a * b + b + (b * b + b) + (a + 1 + (b + 1)))
[PROOFSTEP]
simp only [add_assoc, add_left_comm, add_le_add_iff_left] at ih ⊢
[GOAL]
a b : ℕ
ih :
  a * b + (a * b + (a * b + (a * b + (1 + (1 + (1 + 1)))))) ≤ a * a + (a * b + (b * a + (b * b + (1 + (1 + (1 + 1))))))
⊢ a * b + (a * b + (a * b + (a * b + (1 + (1 + (1 + 1)))))) ≤ a * a + (a * b + (b * a + (b * b + (1 + (1 + (1 + 1))))))
[PROOFSTEP]
exact ih
[GOAL]
n guess : ℕ
⊢ iter n guess * iter n guess ≤ n
[PROOFSTEP]
unfold sqrt.iter
[GOAL]
n guess : ℕ
⊢ ((let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) *
      let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) ≤
    n
[PROOFSTEP]
let next := (guess + n / guess) / 2
[GOAL]
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
⊢ ((let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) *
      let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) ≤
    n
[PROOFSTEP]
by_cases h : next < guess
[GOAL]
case pos
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : next < guess
⊢ ((let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) *
      let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) ≤
    n
case neg
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
⊢ ((let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) *
      let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) ≤
    n
[PROOFSTEP]
case pos => simpa only [dif_pos h] using sqrt.iter_sq_le n next
[GOAL]
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : next < guess
⊢ ((let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) *
      let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) ≤
    n
[PROOFSTEP]
case pos => simpa only [dif_pos h] using sqrt.iter_sq_le n next
[GOAL]
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : next < guess
⊢ ((let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) *
      let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) ≤
    n
[PROOFSTEP]
simpa only [dif_pos h] using sqrt.iter_sq_le n next
[GOAL]
case neg
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
⊢ ((let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) *
      let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) ≤
    n
[PROOFSTEP]
case neg =>
  simp only [dif_neg h]
  apply Nat.mul_le_of_le_div
  apply le_of_add_le_add_left (a := guess)
  rw [← mul_two, ← le_div_iff_mul_le]
  · exact le_of_not_lt h
  · exact zero_lt_two
[GOAL]
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
⊢ ((let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) *
      let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) ≤
    n
[PROOFSTEP]
case neg =>
  simp only [dif_neg h]
  apply Nat.mul_le_of_le_div
  apply le_of_add_le_add_left (a := guess)
  rw [← mul_two, ← le_div_iff_mul_le]
  · exact le_of_not_lt h
  · exact zero_lt_two
[GOAL]
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
⊢ ((let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) *
      let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) ≤
    n
[PROOFSTEP]
simp only [dif_neg h]
[GOAL]
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
⊢ guess * guess ≤ n
[PROOFSTEP]
apply Nat.mul_le_of_le_div
[GOAL]
case h
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
⊢ guess ≤ n / guess
[PROOFSTEP]
apply le_of_add_le_add_left (a := guess)
[GOAL]
case h
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
⊢ guess + guess ≤ guess + n / guess
[PROOFSTEP]
rw [← mul_two, ← le_div_iff_mul_le]
[GOAL]
case h
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
⊢ guess ≤ (guess + n / guess) / 2
[PROOFSTEP]
exact le_of_not_lt h
[GOAL]
case h
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
⊢ 0 < 2
[PROOFSTEP]
exact zero_lt_two
[GOAL]
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
⊢ n < (iter n guess + 1) * (iter n guess + 1)
[PROOFSTEP]
unfold sqrt.iter
[GOAL]
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
⊢ n <
    ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1) *
      ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1)
[PROOFSTEP]
let m := (guess + n / guess) / 2
[GOAL]
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
⊢ n <
    ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1) *
      ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1)
[PROOFSTEP]
by_cases h : m < guess
[GOAL]
case pos
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
⊢ n <
    ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1) *
      ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1)
case neg
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : ¬m < guess
⊢ n <
    ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1) *
      ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1)
[PROOFSTEP]
case pos =>
  suffices : n < (m + 1) * (m + 1)
  · simpa only [dif_pos h] using sqrt.lt_iter_succ_sq n m this
  refine lt_of_mul_lt_mul_left ?_ (4 * (guess * guess)).zero_le
  apply lt_of_le_of_lt AM_GM
  rw [show (4 : ℕ) = 2 * 2 from rfl]
  rw [mul_mul_mul_comm 2, mul_mul_mul_comm (2 * guess)]
  refine mul_self_lt_mul_self (?_ : _ < _ * succ (_ / 2))
  rw [← add_div_right _ (by decide), mul_comm 2, mul_assoc,
    show guess + n / guess + 2 = (guess + n / guess + 1) + 1 from rfl]
  have aux_lemma {a : ℕ} : a ≤ 2 * ((a + 1) / 2) := by
    rw [mul_comm]
    exact (add_le_add_iff_right 2).1 $ succ_le_of_lt $ @lt_div_mul_add (a + 1) 2 zero_lt_two
  refine lt_of_lt_of_le ?_ (act_rel_act_of_rel _ aux_lemma)
  rw [add_assoc, mul_add]
  exact add_lt_add_left (lt_mul_div_succ _ (lt_of_le_of_lt (Nat.zero_le m) h)) _
[GOAL]
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
⊢ n <
    ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1) *
      ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1)
[PROOFSTEP]
case pos =>
  suffices : n < (m + 1) * (m + 1)
  · simpa only [dif_pos h] using sqrt.lt_iter_succ_sq n m this
  refine lt_of_mul_lt_mul_left ?_ (4 * (guess * guess)).zero_le
  apply lt_of_le_of_lt AM_GM
  rw [show (4 : ℕ) = 2 * 2 from rfl]
  rw [mul_mul_mul_comm 2, mul_mul_mul_comm (2 * guess)]
  refine mul_self_lt_mul_self (?_ : _ < _ * succ (_ / 2))
  rw [← add_div_right _ (by decide), mul_comm 2, mul_assoc,
    show guess + n / guess + 2 = (guess + n / guess + 1) + 1 from rfl]
  have aux_lemma {a : ℕ} : a ≤ 2 * ((a + 1) / 2) := by
    rw [mul_comm]
    exact (add_le_add_iff_right 2).1 $ succ_le_of_lt $ @lt_div_mul_add (a + 1) 2 zero_lt_two
  refine lt_of_lt_of_le ?_ (act_rel_act_of_rel _ aux_lemma)
  rw [add_assoc, mul_add]
  exact add_lt_add_left (lt_mul_div_succ _ (lt_of_le_of_lt (Nat.zero_le m) h)) _
[GOAL]
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
⊢ n <
    ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1) *
      ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1)
[PROOFSTEP]
suffices : n < (m + 1) * (m + 1)
[GOAL]
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
this : n < (m + 1) * (m + 1)
⊢ n <
    ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1) *
      ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1)
[PROOFSTEP]
simpa only [dif_pos h] using sqrt.lt_iter_succ_sq n m this
[GOAL]
case this
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
⊢ n < (m + 1) * (m + 1)
[PROOFSTEP]
refine lt_of_mul_lt_mul_left ?_ (4 * (guess * guess)).zero_le
[GOAL]
case this
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
⊢ 4 * (guess * guess) * n < 4 * (guess * guess) * ((m + 1) * (m + 1))
[PROOFSTEP]
apply lt_of_le_of_lt AM_GM
[GOAL]
case this
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
⊢ (guess * guess + n) * (guess * guess + n) < 4 * (guess * guess) * ((m + 1) * (m + 1))
[PROOFSTEP]
rw [show (4 : ℕ) = 2 * 2 from rfl]
[GOAL]
case this
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
⊢ (guess * guess + n) * (guess * guess + n) < 2 * 2 * (guess * guess) * ((m + 1) * (m + 1))
[PROOFSTEP]
rw [mul_mul_mul_comm 2, mul_mul_mul_comm (2 * guess)]
[GOAL]
case this
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
⊢ (guess * guess + n) * (guess * guess + n) < 2 * guess * (m + 1) * (2 * guess * (m + 1))
[PROOFSTEP]
refine mul_self_lt_mul_self (?_ : _ < _ * succ (_ / 2))
[GOAL]
case this
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
⊢ guess * guess + n < 2 * guess * succ ((guess + n / guess) / 2)
[PROOFSTEP]
rw [← add_div_right _ (by decide), mul_comm 2, mul_assoc,
  show guess + n / guess + 2 = (guess + n / guess + 1) + 1 from rfl]
[GOAL]
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
case this
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
⊢ guess * guess + n < guess * (2 * ((guess + n / guess + 1 + 1) / 2))
[PROOFSTEP]
have aux_lemma {a : ℕ} : a ≤ 2 * ((a + 1) / 2) := by
  rw [mul_comm]
  exact (add_le_add_iff_right 2).1 $ succ_le_of_lt $ @lt_div_mul_add (a + 1) 2 zero_lt_two
[GOAL]
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
a : ℕ
⊢ a ≤ 2 * ((a + 1) / 2)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
a : ℕ
⊢ a ≤ (a + 1) / 2 * 2
[PROOFSTEP]
exact (add_le_add_iff_right 2).1 $ succ_le_of_lt $ @lt_div_mul_add (a + 1) 2 zero_lt_two
[GOAL]
case this
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
aux_lemma : ∀ {a : ℕ}, a ≤ 2 * ((a + 1) / 2)
⊢ guess * guess + n < guess * (2 * ((guess + n / guess + 1 + 1) / 2))
[PROOFSTEP]
refine lt_of_lt_of_le ?_ (act_rel_act_of_rel _ aux_lemma)
[GOAL]
case this
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
aux_lemma : ∀ {a : ℕ}, a ≤ 2 * ((a + 1) / 2)
⊢ guess * guess + n < guess * (guess + n / guess + 1)
[PROOFSTEP]
rw [add_assoc, mul_add]
[GOAL]
case this
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : m < guess
aux_lemma : ∀ {a : ℕ}, a ≤ 2 * ((a + 1) / 2)
⊢ guess * guess + n < guess * guess + guess * (n / guess + 1)
[PROOFSTEP]
exact add_lt_add_left (lt_mul_div_succ _ (lt_of_le_of_lt (Nat.zero_le m) h)) _
[GOAL]
case neg
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : ¬m < guess
⊢ n <
    ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1) *
      ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1)
[PROOFSTEP]
case neg => simpa only [dif_neg h] using hn
[GOAL]
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : ¬m < guess
⊢ n <
    ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1) *
      ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1)
[PROOFSTEP]
case neg => simpa only [dif_neg h] using hn
[GOAL]
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : ¬m < guess
⊢ n <
    ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1) *
      ((let next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) +
        1)
[PROOFSTEP]
simpa only [dif_neg h] using hn
