-- Mathlib/Data/Nat/Sqrt.lean
lemma sqrt.lt_iter_succ_sq (n guess : ℕ) (hn : n < (guess + 1) * (guess + 1)) :
    n < (sqrt.iter n guess + 1) * (sqrt.iter n guess + 1)

Proof state:
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
⊢ n <
    ((if (guess + n / guess) / 2 < guess then iter n ((guess + n / guess) / 2) else guess) + 1) *
      ((if (guess + n / guess) / 2 < guess then iter n ((guess + n / guess) / 2) else guess) + 1)

Tactic:
split_ifs with h

Result:
case pos
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
⊢ n < (iter n ((guess + n / guess) / 2) + 1) * (iter n ((guess + n / guess) / 2) + 1)

case neg
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : ¬(guess + n / guess) / 2 < guess
⊢ n < (guess + 1) * (guess + 1)

Proof state:
case pos
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
aux_lemma : ∀ {a : ℕ}, a ≤ 2 * ((a + 1) / 2)
⊢ guess * guess + n < guess * (2 * ((guess + n / guess + 1 + 1) / 2))

Tactic:
refine lt_of_lt_of_le ?_ (Nat.mul_le_mul_left _ aux_lemma)

Result:
case pos
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
aux_lemma : ∀ {a : ℕ}, a ≤ 2 * ((a + 1) / 2)
⊢ guess * guess + n < guess * (guess + n / guess + 1)

Proof state:
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)

Tactic:
dsimp

Result:
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
⊢ n <
    ((if (guess + n / guess) / 2 < guess then iter n ((guess + n / guess) / 2) else guess) + 1) *
      ((if (guess + n / guess) / 2 < guess then iter n ((guess + n / guess) / 2) else guess) + 1)

Proof state:
case pos
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
⊢ n < (m + 1) * (m + 1)

Tactic:
refine Nat.lt_of_mul_lt_mul_left ?_ (a := 4 * (guess * guess))

Result:
case pos
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
⊢ 4 * (guess * guess) * n < 4 * (guess * guess) * ((m + 1) * (m + 1))

Proof state:
case pos
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
aux_lemma : ∀ {a : ℕ}, a ≤ 2 * ((a + 1) / 2)
⊢ guess * guess + n < guess * (guess + n / guess + 1)

Tactic:
rw [Nat.add_assoc, Nat.mul_add]

Result:
case pos
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
aux_lemma : ∀ {a : ℕ}, a ≤ 2 * ((a + 1) / 2)
⊢ guess * guess + n < guess * guess + guess * (n / guess + 1)

Proof state:
case pos
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
⊢ (guess * guess + n) * (guess * guess + n) < 2 * guess * (m + 1) * (2 * guess * (m + 1))

Tactic:
refine Nat.mul_self_lt_mul_self (?_ : _ < _ * ((_ / 2) + 1))

Result:
case pos
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
⊢ guess * guess + n < 2 * guess * ((guess + n / guess) / 2 + 1)

Proof state:
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
a : ℕ
⊢ a ≤ 2 * ((a + 1) / 2)

Tactic:
omega

Result:
no goals

Proof state:
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
this : n < (m + 1) * (m + 1)
⊢ n < (iter n ((guess + n / guess) / 2) + 1) * (iter n ((guess + n / guess) / 2) + 1)

Tactic:
simpa only [dif_pos h] using sqrt.lt_iter_succ_sq n m this

Result:
no goals

Proof state:
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)

Tactic:
let m := (guess + n / guess) / 2

Result:
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)

Proof state:
case pos
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
⊢ guess * guess + n < 2 * guess * ((guess + n / guess) / 2 + 1)

Tactic:
rw [← add_div_right _ (by decide), Nat.mul_comm 2, Nat.mul_assoc,
  show guess + n / guess + 2 = (guess + n / guess + 1) + 1 from rfl]

Result:
case pos
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
⊢ guess * guess + n < guess * (2 * ((guess + n / guess + 1 + 1) / 2))

Proof state:
case pos
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
⊢ (guess * guess + n) * (guess * guess + n) < 2 * 2 * (guess * guess) * ((m + 1) * (m + 1))

Tactic:
rw [Nat.mul_mul_mul_comm 2, Nat.mul_mul_mul_comm (2 * guess)]

Result:
case pos
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
⊢ (guess * guess + n) * (guess * guess + n) < 2 * guess * (m + 1) * (2 * guess * (m + 1))

Proof state:
case pos
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
⊢ (guess * guess + n) * (guess * guess + n) < 4 * (guess * guess) * ((m + 1) * (m + 1))

Tactic:
rw [show (4 : ℕ) = 2 * 2 from rfl]

Result:
case pos
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
⊢ (guess * guess + n) * (guess * guess + n) < 2 * 2 * (guess * guess) * ((m + 1) * (m + 1))

Proof state:
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
⊢ n < (iter n guess + 1) * (iter n guess + 1)

Tactic:
unfold sqrt.iter

Result:
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)

Proof state:
case pos
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
⊢ guess * guess + n < guess * (2 * ((guess + n / guess + 1 + 1) / 2))

Tactic:
have aux_lemma {a : ℕ} : a ≤ 2 * ((a + 1) / 2) := by omega

Result:
case pos
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
aux_lemma : ∀ {a : ℕ}, a ≤ 2 * ((a + 1) / 2)
⊢ guess * guess + n < guess * (2 * ((guess + n / guess + 1 + 1) / 2))

Proof state:
case pos
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
aux_lemma : ∀ {a : ℕ}, a ≤ 2 * ((a + 1) / 2)
⊢ guess * guess + n < guess * guess + guess * (n / guess + 1)

Tactic:
exact Nat.add_lt_add_left (lt_mul_div_succ _ (lt_of_le_of_lt (Nat.zero_le m) h)) _

Result:
no goals