awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Size
Goal:
n : ℕ
zero : 0 < HPow.hPow (α := ℕ) 2 (size 0)
bit :
  ∀ (b : Bool) (n : ℕ) (h : n = 0 → b = true) (IH : n < HPow.hPow (α := ℕ) 2 n.size),
    Nat.bit b n < HPow.hPow (α := ℕ) 2 (Nat.bit b n).size
⊢ n < HPow.hPow (α := ℕ) 2 n.size

Tactic:
induction n using binaryRec' with
  | zero => simp
  | bit b n h IH =>
    rw [← Nat.bit_ne_zero_iff] at h
    rwa [size_bit h, bit_lt_two_pow_succ_iff]

Premises used: Nat.bit, Nat.zero, Nat.bit_lt_two_pow_succ_iff, Nat.bit_ne_zero_iff
-- Module: Mathlib.Data.Nat.Size
Goal:
m n : ℕ
h : m.size ≤ n
⊢ GT.gt (α := ℕ) 2 0

Tactic:
decide
-- Module: Mathlib.Data.Nat.Size
Goal:
n : ℕ
h : 0 < HPow.hPow (α := ℕ) 2 n
⊢ size 0 ≤ n

Tactic:
simp
-- Module: Mathlib.Data.Nat.Size
Goal:
b : Bool
m : ℕ
e : m = 0 → b = true
IH : ∀ {n : ℕ} (h : m < HPow.hPow (α := ℕ) 2 n), m.size ≤ n
n : ℕ
h : Nat.bit b m < HPow.hPow (α := ℕ) 2 n
bit :
  ∀ (e : Nat.bit b m ≠ 0) (IH : ∀ {n : ℕ} (h : m < HPow.hPow (α := ℕ) 2 n), m.size ≤ n) {n : ℕ}
    (h : Nat.bit b m < HPow.hPow (α := ℕ) 2 n), (Nat.bit b m).size ≤ n
⊢ (Nat.bit b m).size ≤ n

Tactic:
rw [← Nat.bit_ne_zero_iff] at e

Premises used: Nat.bit_ne_zero_iff
-- Module: Mathlib.Data.Nat.Size
Goal:
b : Bool
m : ℕ
e : Nat.bit b m ≠ 0
IH : ∀ {n : ℕ} (h : m < HPow.hPow (α := ℕ) 2 n), m.size ≤ n
n : ℕ
h : Nat.bit b m < HPow.hPow (α := ℕ) 2 n
bit : m.size.succ ≤ n
⊢ (Nat.bit b m).size ≤ n

Tactic:
rw [size_bit e]

Premises used: Nat.size_bit
-- Module: Mathlib.Data.Nat.Size
Goal:
b : Bool
m : ℕ
e : bit b m ≠ 0
IH : ∀ {n : ℕ} (h : m < HPow.hPow (α := ℕ) 2 n), m.size ≤ n
h : bit b m < HPow.hPow (α := ℕ) (β := ℕ) 2 0
⊢ m.size.succ ≤ 0

Tactic:
(e (Nat.lt_one_iff.mp h)).elim

Premises used: False.elim, Nat.lt_one_iff, Iff.mp
-- Module: Mathlib.Data.Nat.Size
Goal:
b : Bool
m : ℕ
e : bit b m ≠ 0
IH : ∀ {n : ℕ} (h : m < HPow.hPow (α := ℕ) 2 n), m.size ≤ n
h : bit b m < HPow.hPow (α := ℕ) (β := ℕ) 2 0
⊢ m.size.succ ≤ 0

Tactic:
exact (e (Nat.lt_one_iff.mp h)).elim

Premises used: False.elim, Nat.lt_one_iff, Iff.mp
-- Module: Mathlib.Data.Nat.Size
Goal:
b : Bool
m : ℕ
e : bit b m ≠ 0
IH : ∀ {n : ℕ} (h : m < HPow.hPow (α := ℕ) 2 n), m.size ≤ n
n : ℕ
h : bit b m < HPow.hPow (α := ℕ) 2 (n + 1)
⊢ m.size.succ ≤ n + 1

Tactic:
succ_le_succ (IH (bit_lt_two_pow_succ_iff.mp h))

Premises used: Iff.mp, Nat.bit_lt_two_pow_succ_iff, Nat.succ_le_succ
-- Module: Mathlib.Data.Nat.Size
Goal:
b : Bool
m : ℕ
e : bit b m ≠ 0
IH : ∀ {n : ℕ} (h : m < HPow.hPow (α := ℕ) 2 n), m.size ≤ n
n : ℕ
h : bit b m < HPow.hPow (α := ℕ) 2 (n + 1)
⊢ m.size.succ ≤ n + 1

Tactic:
exact succ_le_succ (IH (bit_lt_two_pow_succ_iff.mp h))

Premises used: Iff.mp, Nat.bit_lt_two_pow_succ_iff, Nat.succ_le_succ
-- Module: Mathlib.Data.Nat.Size
Goal:
b : Bool
m : ℕ
e : Nat.bit b m ≠ 0
IH : ∀ {n : ℕ} (h : m < HPow.hPow (α := ℕ) 2 n), m.size ≤ n
n : ℕ
h : Nat.bit b m < HPow.hPow (α := ℕ) 2 n
bit : ∀ (h : Nat.bit b m < HPow.hPow (α := ℕ) (β := ℕ) 2 0), m.size.succ ≤ 0
bit₁ : ∀ (n : ℕ) (h : Nat.bit b m < HPow.hPow (α := ℕ) 2 (n + 1)), m.size.succ ≤ n + 1
⊢ m.size.succ ≤ n

Tactic:
cases n with
      | zero => exact (e (Nat.lt_one_iff.mp h)).elim
      | succ n => exact succ_le_succ (IH (bit_lt_two_pow_succ_iff.mp h))

Premises used: Iff.mp, Nat.zero, Nat.bit_lt_two_pow_succ_iff, Nat.succ, Nat.succ_le_succ
-- Module: Mathlib.Data.Nat.Size
Goal:
m n : ℕ
h : m < HPow.hPow (α := ℕ) 2 n
zero : ∀ {n : ℕ} (h : 0 < HPow.hPow (α := ℕ) 2 n), size 0 ≤ n
bit :
  ∀ (b : Bool) (m : ℕ) (e : m = 0 → b = true) (IH : ∀ {n : ℕ} (h : m < HPow.hPow (α := ℕ) 2 n), m.size ≤ n) {n : ℕ}
    (h : Nat.bit b m < HPow.hPow (α := ℕ) 2 n), (Nat.bit b m).size ≤ n
⊢ m.size ≤ n

Tactic:
induction m using binaryRec' generalizing n with
    | zero => simp
    | bit b m e IH =>
      rw [← Nat.bit_ne_zero_iff] at e
      rw [size_bit e]
      cases n with
      | zero => exact (e (Nat.lt_one_iff.mp h)).elim
      | succ n => exact succ_le_succ (IH (bit_lt_two_pow_succ_iff.mp h))

Premises used: Nat.bit, Nat.zero, Nat.bit_ne_zero_iff, Nat.succ
-- Module: Mathlib.Data.Nat.Size
Goal:
m n : ℕ
rw : m < n.size ↔ ¬n < HPow.hPow (α := ℕ) 2 m
rw₁ : n < HPow.hPow (α := ℕ) 2 m ↔ ¬m < n.size
rw₂ : n < HPow.hPow (α := ℕ) 2 m ↔ n.size ≤ m
rw₃ rw₄ : n < HPow.hPow (α := ℕ) 2 m ↔ n < HPow.hPow (α := ℕ) 2 m
⊢ m < n.size ↔ HPow.hPow (α := ℕ) 2 m ≤ n

Tactic:
rw [← Nat.not_lt, Decidable.iff_not_comm, Nat.not_lt, size_le]

Premises used: Nat.not_lt, Decidable.iff_not_comm, Nat.size_le
-- Module: Mathlib.Data.Nat.Size
Goal:
n : ℕ
rw : HPow.hPow (α := ℕ) (β := ℕ) 2 0 ≤ n ↔ 0 < n
⊢ 0 < n.size ↔ 0 < n

Tactic:
rw [lt_size]

Premises used: Nat.lt_size
-- Module: Mathlib.Data.Nat.Size
Goal:
n : ℕ
⊢ HPow.hPow (α := ℕ) (β := ℕ) 2 0 ≤ n ↔ 0 < n

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Size
Goal:
n : ℕ
⊢ n.size = 0 ↔ n = 0

Tactic:
simpa [Nat.pos_iff_ne_zero, Decidable.not_iff_not] using size_pos

Premises used: Nat.pos_iff_ne_zero, Decidable.not_iff_not, Nat.size_pos
-- Module: Mathlib.Data.Nat.Size
Goal:
n : ℕ
⊢ Ne (α := ℕ) 1 0

Tactic:
decide
-- Module: Mathlib.Data.Nat.Size
Goal:
n : ℕ
⊢ (HPow.hPow (α := ℕ) 2 n).size = n + 1

Tactic:
simpa [shiftLeft_eq, Nat.add_comm] using size_shiftLeft (m := 1) (by decide) n

Premises used: Nat.shiftLeft_eq, Nat.size_shiftLeft, Nat.add_comm
-- Module: Mathlib.Data.Nat.Size
Goal:
m n : ℕ
h : m ≤ n
⊢ m.size ≤ n.size

Tactic:
size_le.2 <| Nat.lt_of_le_of_lt h (lt_size_self _)

Premises used: Iff.mpr, Nat.lt_of_le_of_lt, Nat.lt_size_self, Nat.size_le
-- Module: Mathlib.Data.Nat.Size
Goal:
⊢ (bits 0).length = size 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Size
Goal:
b : Bool
n : ℕ
h : n = 0 → b = true
ih : n.bits.length = n.size
bit : (b :: n.bits).length = n.size.succ
bit₁ : Nat.bit b n ≠ 0
⊢ (Nat.bit b n).bits.length = (Nat.bit b n).size

Tactic:
rw [size_bit, bits_append_bit _ _ h]

Premises used: Nat.size_bit, Nat.bits_append_bit
-- Module: Mathlib.Data.Nat.Size
Goal:
b : Bool
n : ℕ
h : n = 0 → b = true
ih : n.bits.length = n.size
⊢ (b :: n.bits).length = n.size.succ

Tactic:
simp [ih]
-- Module: Mathlib.Data.Nat.Size
Goal:
b : Bool
n : ℕ
h : n = 0 → b = true
ih : n.bits.length = n.size
⊢ bit b n ≠ 0

Tactic:
simpa [bit_eq_zero_iff]

Premises used: Nat.bit_eq_zero_iff
-- Module: Mathlib.Data.Nat.Size
Goal:
n : ℕ
zero : (bits 0).length = size 0
bit :
  ∀ (b : Bool) (n : ℕ) (h : n = 0 → b = true) (ih : n.bits.length = n.size),
    (Nat.bit b n).bits.length = (Nat.bit b n).size
⊢ n.bits.length = n.size

Tactic:
induction n using Nat.binaryRec' with
  | zero => simp
  | bit _ _ h ih =>
    rw [size_bit, bits_append_bit _ _ h]
    · simp [ih]
    · simpa [bit_eq_zero_iff]

Premises used: Nat.bit, Nat.bit_eq_zero_iff, Nat.size_bit, Nat.zero
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n k : ℕ
iter_next : (n guess : ℕ) → ℕ := fun (n guess : ℕ) ↦ (guess + n / guess) / 2
unfold :
  (have next := (k + n / k) / 2;
    if _h : next < k then sqrt.iter n next else k) ≤
    iter_next n
      (have next := (k + n / k) / 2;
      if _h : next < k then sqrt.iter n next else k)
⊢ sqrt.iter n k ≤ iter_next n (sqrt.iter n k)

Tactic:
unfold sqrt.iter

Premises used: Nat.sqrt.iter
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n k : ℕ
iter_next : (n guess : ℕ) → ℕ := fun (n guess : ℕ) ↦ (guess + n / guess) / 2
h : (k + n / k) / 2 < k
⊢ (have next := (k + n / k) / 2;
    if _h : next < k then sqrt.iter n next else k) ≤
    iter_next n
      (have next := (k + n / k) / 2;
      if _h : next < k then sqrt.iter n next else k)

Tactic:
simpa [if_pos h] using iter_fp_bound _ _

Premises used: if_pos
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n k : ℕ
iter_next : (n guess : ℕ) → ℕ := fun (n guess : ℕ) ↦ (guess + n / guess) / 2
h : ¬(k + n / k) / 2 < k
⊢ (have next := (k + n / k) / 2;
    if _h : next < k then sqrt.iter n next else k) ≤
    iter_next n
      (have next := (k + n / k) / 2;
      if _h : next < k then sqrt.iter n next else k)

Tactic:
grind
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n k : ℕ
iter_next : (n guess : ℕ) → ℕ := fun (n guess : ℕ) ↦ (guess + n / guess) / 2
if :
  ∀ (h : (k + n / k) / 2 < k),
    (have next := (k + n / k) / 2;
      if _h : next < k then sqrt.iter n next else k) ≤
      iter_next n
        (have next := (k + n / k) / 2;
        if _h : next < k then sqrt.iter n next else k)
if₁ :
  ∀ (h : ¬(k + n / k) / 2 < k),
    (have next := (k + n / k) / 2;
      if _h : next < k then sqrt.iter n next else k) ≤
      iter_next n
        (have next := (k + n / k) / 2;
        if _h : next < k then sqrt.iter n next else k)
if₂ :
  ∀ (h : (k + n / k) / 2 < k),
    (have next := (k + n / k) / 2;
      if _h : next < k then sqrt.iter n next else k) ≤
      iter_next n
        (have next := (k + n / k) / 2;
        if _h : next < k then sqrt.iter n next else k)
if₃ if₄ :
  ∀ (h : ¬(k + n / k) / 2 < k),
    (have next := (k + n / k) / 2;
      if _h : next < k then sqrt.iter n next else k) ≤
      iter_next n
        (have next := (k + n / k) / 2;
        if _h : next < k then sqrt.iter n next else k)
⊢ (have next := (k + n / k) / 2;
    if _h : next < k then sqrt.iter n next else k) ≤
    iter_next n
      (have next := (k + n / k) / 2;
      if _h : next < k then sqrt.iter n next else k)

Tactic:
if h : (k + n / k) / 2 < k then
    simpa [if_pos h] using iter_fp_bound _ _
  else
    grind

Premises used: HDiv.hDiv, HAdd.hAdd
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
x : ℕ
rw : 0 ≤ (0 + x) * (0 + x)
⊢ HMul.hMul (α := ℕ) 4 0 * x ≤ (0 + x) * (0 + x)

Tactic:
rw [Nat.mul_zero, Nat.zero_mul]

Premises used: Nat.zero_mul, Nat.mul_zero
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
x : ℕ
⊢ 0 ≤ (0 + x) * (0 + x)

Tactic:
zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
x : ℕ
⊢ 0 ≤ (0 + x) * (0 + x)

Tactic:
exact zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
x : ℕ
⊢ 0 ≤ (x + 0) * (x + 0)

Tactic:
zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
x : ℕ
⊢ 0 ≤ (x + 0) * (x + 0)

Tactic:
exact zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
a b : ℕ
⊢ 4 * (a + 1) * (b + 1) ≤ (a + 1 + (b + 1)) * (a + 1 + (b + 1))

Tactic:
simpa only [Nat.mul_add, Nat.add_mul, show (4 : ℕ) = 1 + 1 + 1 + 1 from rfl, Nat.one_mul,
      Nat.mul_one, Nat.add_assoc, Nat.add_left_comm, Nat.add_le_add_iff_left]
      using Nat.add_le_add_right (@AM_GM a b) 4

Premises used: Nat.mul_one, Nat.add_le_add_right, Nat.add_left_comm, Nat.add_le_add_iff_left, Nat.add_assoc, OfNat.ofNat, Nat.mul_add, Nat.one_mul, Nat.add_mul, rfl
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n guess : ℕ
unfold :
  HMul.hMul (α := ℕ)
      (have next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess)
      (have next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) ≤
    n
⊢ iter n guess * iter n guess ≤ n

Tactic:
unfold sqrt.iter

Premises used: Nat.sqrt.iter
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : next < guess
⊢ HMul.hMul (α := ℕ)
      (have next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess)
      (have next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) ≤
    n

Tactic:
simpa only [next, dif_pos h] using sqrt.iter_sq_le n next

Premises used: dif_pos
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
h₁ :
  (have next := (guess + n / guess) / 2;
    if _h : next < guess then iter n next else guess) ≤
    n /
      have next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess
⊢ HMul.hMul (α := ℕ)
      (have next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess)
      (have next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) ≤
    n

Tactic:
apply Nat.mul_le_of_le_div

Premises used: Nat.mul_le_of_le_div
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
⊢ (have next := (guess + n / guess) / 2;
    if _h : next < guess then iter n next else guess) ≤
    n /
      have next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess

Tactic:
grind
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
if :
  ∀ (h : next < guess),
    HMul.hMul (α := ℕ)
        (have next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess)
        (have next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) ≤
      n
if₁ :
  ∀ (h : ¬next < guess),
    HMul.hMul (α := ℕ)
        (have next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess)
        (have next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) ≤
      n
if₂ :
  ∀ (h : next < guess),
    HMul.hMul (α := ℕ)
        (have next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess)
        (have next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) ≤
      n
if₃ if₄ :
  ∀ (h : ¬next < guess),
    HMul.hMul (α := ℕ)
        (have next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess)
        (have next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess) ≤
      n
⊢ HMul.hMul (α := ℕ)
      (have next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess)
      (have next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) ≤
    n

Tactic:
if h : next < guess then
    simpa only [next, dif_pos h] using sqrt.iter_sq_le n next
  else
    apply Nat.mul_le_of_le_div
    grind

Premises used: Nat.mul_le_of_le_div
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
unfold :
  n <
    HAdd.hAdd (α := ℕ)
        (have next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess)
        1 *
      HAdd.hAdd (α := ℕ)
        (have next := (guess + n / guess) / 2;
        if _h : next < guess then iter n next else guess)
        1
⊢ n < (iter n guess + 1) * (iter n guess + 1)

Tactic:
unfold sqrt.iter

Premises used: Nat.sqrt.iter
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
pos :
  ∀ (h : (guess + n / guess) / 2 < guess),
    n < (iter n ((guess + n / guess) / 2) + 1) * (iter n ((guess + n / guess) / 2) + 1)
neg : ∀ (h : ¬(guess + n / guess) / 2 < guess), n < (guess + 1) * (guess + 1)
⊢ 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
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
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

Premises used: dif_pos
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
pos : n < (m + 1) * (m + 1)
⊢ n < (iter n ((guess + n / guess) / 2) + 1) * (iter n ((guess + n / guess) / 2) + 1)

Tactic:
suffices n < (m + 1) * (m + 1) by
      simpa only [dif_pos h] using sqrt.lt_iter_succ_sq n m this
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
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:
Nat.lt_of_mul_lt_mul_left ?_ (a := 4 * (guess * guess))

Premises used: Nat.lt_of_mul_lt_mul_left
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
pos : 4 * (guess * guess) * n < 4 * (guess * guess) * ((m + 1) * (m + 1))
⊢ n < (m + 1) * (m + 1)

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

Premises used: Nat.lt_of_mul_lt_mul_left
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
pos : (guess * guess + n) * (guess * guess + n) < 4 * (guess * guess) * ((m + 1) * (m + 1))
⊢ 4 * (guess * guess) * n < 4 * (guess * guess) * ((m + 1) * (m + 1))

Tactic:
apply Nat.lt_of_le_of_lt AM_GM

Premises used: Nat.lt_of_le_of_lt, _private.0.Nat.AM_GM
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
pos : (guess * guess + n) * (guess * guess + n) < 2 * guess * (m + 1) * (2 * guess * (m + 1))
⊢ (guess * guess + n) * (guess * guess + n) < HMul.hMul (α := ℕ) 2 2 * (guess * guess) * ((m + 1) * (m + 1))

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

Premises used: HMul.hMul, Nat.mul_mul_mul_comm, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
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:
Nat.mul_self_lt_mul_self (?_ : _ < _ * ((_ / 2) + 1))

Premises used: Nat.mul_self_lt_mul_self
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
pos : guess * guess + n < 2 * guess * ((guess + n / guess) / 2 + 1)
⊢ (guess * guess + n) * (guess * guess + n) < 2 * guess * (m + 1) * (2 * guess * (m + 1))

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

Premises used: Nat.mul_self_lt_mul_self
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
⊢ LT.lt (α := ℕ) 0 2

Tactic:
decide
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
pos : guess * guess + n < guess * (2 * ((guess + n / guess + 1 + 1) / 2))
⊢ 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]

Premises used: Nat.mul_comm, Nat.mul_assoc, Nat.add_div_right, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
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:
lia
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
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:
have aux_lemma {a : ℕ} : a ≤ 2 * ((a + 1) / 2) := by lia
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
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:
lt_of_lt_of_le ?_ (Nat.mul_le_mul_left _ aux_lemma)

Premises used: Nat.mul_le_mul_left, lt_of_lt_of_le
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
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)
pos : guess * guess + n < guess * (guess + n / guess + 1)
⊢ 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)

Premises used: Nat.mul_le_mul_left, lt_of_lt_of_le
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
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)
pos : guess * guess + n < guess * guess + guess * (n / guess + 1)
⊢ guess * guess + n < guess * (guess + n / guess + 1)

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

Premises used: Nat.add_assoc, Nat.mul_add
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
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:
Nat.add_lt_add_left (lt_mul_div_succ _ (lt_of_le_of_lt (Nat.zero_le m) h)) _

Premises used: Nat.zero_le, lt_of_le_of_lt, Nat.lt_mul_div_succ, Nat.add_lt_add_left
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
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)) _

Premises used: Nat.zero_le, lt_of_le_of_lt, Nat.lt_mul_div_succ, Nat.add_lt_add_left
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : ¬(guess + n / guess) / 2 < guess
⊢ n < (guess + 1) * (guess + 1)

Tactic:
hn
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : ¬(guess + n / guess) / 2 < guess
⊢ n < (guess + 1) * (guess + 1)

Tactic:
exact hn
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n : ℕ
⊢ IsSqrt 0 (sqrt 0)

Tactic:
simp [IsSqrt, sqrt]

Premises used: Nat.sqrt, _private.0.Nat.IsSqrt
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n : ℕ
⊢ IsSqrt 1 (sqrt 1)

Tactic:
simp [IsSqrt, sqrt]

Premises used: Nat.sqrt, _private.0.Nat.IsSqrt
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n_1 n : ℕ
⊢ ¬n + 2 ≤ 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n_1 n : ℕ
⊢ ¬n + 2 ≤ 1

Tactic:
have h : ¬ (n + 2) ≤ 1 := by simp
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n_1 n : ℕ
h : ¬n + 2 ≤ 1
⊢ sqrt.iter (n + 2) (1 <<< ((n + 2).log2 / 2 + 1)) * sqrt.iter (n + 2) (1 <<< ((n + 2).log2 / 2 + 1)) ≤ n + 2 ∧
    n + 2 <
      (sqrt.iter (n + 2) (1 <<< ((n + 2).log2 / 2 + 1)) + 1) * (sqrt.iter (n + 2) (1 <<< ((n + 2).log2 / 2 + 1)) + 1)

Tactic:
⟨sqrt.iter_sq_le _ _, sqrt.lt_iter_succ_sq _ _ ?_⟩

Premises used: Nat.sqrt.iter_sq_le, And.intro, Nat.sqrt.lt_iter_succ_sq
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n_1 n : ℕ
h : ¬n + 2 ≤ 1
refine : n + 2 < (1 <<< ((n + 2).log2 / 2 + 1) + 1) * (1 <<< ((n + 2).log2 / 2 + 1) + 1)
⊢ sqrt.iter (n + 2) (1 <<< ((n + 2).log2 / 2 + 1)) * sqrt.iter (n + 2) (1 <<< ((n + 2).log2 / 2 + 1)) ≤ n + 2 ∧
    n + 2 <
      (sqrt.iter (n + 2) (1 <<< ((n + 2).log2 / 2 + 1)) + 1) * (sqrt.iter (n + 2) (1 <<< ((n + 2).log2 / 2 + 1)) + 1)

Tactic:
refine ⟨sqrt.iter_sq_le _ _, sqrt.lt_iter_succ_sq _ _ ?_⟩
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n_1 n : ℕ
h : ¬n + 2 ≤ 1
simp :
  n + 2 <
    1 <<< ((n + 2).log2 / 2 + 1) * 1 <<< ((n + 2).log2 / 2 + 1) + 1 <<< ((n + 2).log2 / 2 + 1) +
        1 <<< ((n + 2).log2 / 2 + 1) +
      1
⊢ n + 2 < (1 <<< ((n + 2).log2 / 2 + 1) + 1) * (1 <<< ((n + 2).log2 / 2 + 1) + 1)

Tactic:
simp only [Nat.mul_add, Nat.add_mul, Nat.one_mul, Nat.mul_one, ← Nat.add_assoc]

Premises used: Nat.mul_one, Nat.add_assoc, Nat.mul_add, Nat.one_mul, Nat.add_mul
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n_1 n : ℕ
h : ¬n + 2 ≤ 1
rw : n + 2 ≤ 1 <<< ((n + 2).log2 / 2 + 1) * 1 <<< ((n + 2).log2 / 2 + 1) + 1 <<< ((n + 2).log2 / 2 + 1) * 2
⊢ n + 2 <
    1 <<< ((n + 2).log2 / 2 + 1) * 1 <<< ((n + 2).log2 / 2 + 1) + 1 <<< ((n + 2).log2 / 2 + 1) +
        1 <<< ((n + 2).log2 / 2 + 1) +
      1

Tactic:
rw [Nat.lt_add_one_iff, Nat.add_assoc, ← Nat.mul_two]

Premises used: Nat.lt_add_one_iff, Nat.add_assoc, Nat.mul_two
-- Module: Mathlib.Data.Nat.Sqrt
Goal:
n_1 n : ℕ
h : ¬n + 2 ≤ 1
⊢ n + 2 ≤ 1 <<< ((n + 2).log2 / 2 + 1) * 1 <<< ((n + 2).log2 / 2 + 1) + 1 <<< ((n + 2).log2 / 2 + 1) * 2

Tactic:
le_trans (Nat.le_of_eq (div_add_mod' (n + 2) 2).symm) ?_

Premises used: Nat.div_add_mod', Nat.le_of_eq, HAdd.hAdd, OfNat.ofNat, Eq.symm, le_trans