awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Size (hypothesis)
Goal:
m n : ℕ
IH : ∀ (h : shiftLeft' true m n ≠ 0), (shiftLeft' true m n).size = m.size + n
h : ¬bit true 0 = 0
s0 : shiftLeft' true m n = 0
⊢ (size 0).succ = (m.size + n).succ
have this : shiftLeft' true m n + 1 = 1
Tactic: have : shiftLeft' true m n + 1 = 1 := congr_arg (· + 1) s0
-- Lean 4 proof step from Mathlib.Data.Nat.Size (hypothesis)
Goal:
m n : ℕ
IH : ∀ (h : shiftLeft' true m n ≠ 0), (shiftLeft' true m n).size = m.size + n
h : ¬bit true 0 = 0
s0 : shiftLeft' true m n = 0
this : shiftLeft' true m n + 1 = 1
⊢ (size 0).succ = (m.size + n).succ
have this₁ : (m + 1) * HPow.hPow (α := ℕ) 2 n = 1
Tactic: rw [shiftLeft'_true_eq_mul_pow] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
m n : ℕ
IH : ∀ (h : shiftLeft' true m n ≠ 0), (shiftLeft' true m n).size = m.size + n
h : ¬bit true 0 = 0
s0 : shiftLeft' true m n = 0
this : (m + 1) * HPow.hPow (α := ℕ) 2 n = 1
⊢ (size 0).succ = (m.size + n).succ
have pos : ∀ (IH : ∀ (h : shiftLeft' true 0 n ≠ 0), (shiftLeft' true 0 n).size = size 0 + n) (s0 : shiftLeft' true 0 n = 0)
  (this : HAdd.hAdd (α := ℕ) 0 1 * HPow.hPow (α := ℕ) 2 n = 1), (size 0).succ = (size 0 + n).succ
Tactic: obtain rfl := succ.inj (eq_one_of_dvd_one ⟨_, this.symm⟩)
Cleared hypotheses: m, IH, s0, this
-- Lean 4 proof step from Mathlib.Data.Nat.Size (hypothesis)
Goal:
n : ℕ
h : ¬bit true 0 = 0
IH : ∀ (h : shiftLeft' true 0 n ≠ 0), (shiftLeft' true 0 n).size = size 0 + n
s0 : shiftLeft' true 0 n = 0
this : HAdd.hAdd (α := ℕ) 0 1 * HPow.hPow (α := ℕ) 2 n = 1
⊢ (size 0).succ = (size 0 + n).succ
have this₁ : n = 0
Tactic: simp only [Nat.zero_add, Nat.one_mul, Nat.pow_eq_one, succ_ne_self, false_or] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
n : ℕ
h : ¬bit true 0 = 0
IH : ∀ (h : shiftLeft' true 0 n ≠ 0), (shiftLeft' true 0 n).size = size 0 + n
s0 : shiftLeft' true 0 n = 0
this : n = 0
⊢ (size 0).succ = (size 0 + n).succ
have pos : (size 0).succ = (size 0 + 0).succ
Tactic: rw [this, Nat.add_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
b : Bool
m n : ℕ
h : shiftLeft' b m n ≠ 0
⊢ (shiftLeft' b m n).size = m.size + n
have zero : ∀ (h : shiftLeft' b m 0 ≠ 0), (shiftLeft' b m 0).size = m.size + 0
Tactic: induction n with
  | zero => simp [shiftLeft']
  | succ n IH =>
    simp only [shiftLeft', ne_eq] at h ⊢
    rw [size_bit h, Nat.add_succ]
    by_cases s0 : shiftLeft' b m n = 0
    case neg => rw [IH s0]
    rw [s0] at h ⊢
    cases b; · exact absurd rfl h
    have : shiftLeft' true m n + 1 = 1 := congr_arg (· + 1) s0
    rw [shiftLeft'_true_eq_mul_pow] at this
    obtain rfl := succ.inj (eq_one_of_dvd_one ⟨_, this.symm⟩)
    simp only [Nat.zero_add, Nat.one_mul, Nat.pow_eq_one, succ_ne_self, false_or] at this
    rw [this, Nat.add_zero]
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
b : Bool
m n : ℕ
h : shiftLeft' b m n ≠ 0
zero : ∀ (h : shiftLeft' b m 0 ≠ 0), (shiftLeft' b m 0).size = m.size + 0
⊢ (shiftLeft' b m n).size = m.size + n
have succ : ∀ (n : ℕ) (IH : ∀ (h : shiftLeft' b m n ≠ 0), (shiftLeft' b m n).size = m.size + n) (h : shiftLeft' b m (n + 1) ≠ 0),
  (shiftLeft' b m (n + 1)).size = m.size + (n + 1)
Tactic: induction n with
  | zero => simp [shiftLeft']
  | succ n IH =>
    simp only [shiftLeft', ne_eq] at h ⊢
    rw [size_bit h, Nat.add_succ]
    by_cases s0 : shiftLeft' b m n = 0
    case neg => rw [IH s0]
    rw [s0] at h ⊢
    cases b; · exact absurd rfl h
    have : shiftLeft' true m n + 1 = 1 := congr_arg (· + 1) s0
    rw [shiftLeft'_true_eq_mul_pow] at this
    obtain rfl := succ.inj (eq_one_of_dvd_one ⟨_, this.symm⟩)
    simp only [Nat.zero_add, Nat.one_mul, Nat.pow_eq_one, succ_ne_self, false_or] at this
    rw [this, Nat.add_zero]
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Nat.Size (hypothesis)
Goal:
b : Bool
n : ℕ
h : n = 0 → b = true
IH : n < HPow.hPow (α := ℕ) 2 n.size
⊢ bit b n < HPow.hPow (α := ℕ) 2 (bit b n).size
have h₁ : bit b n ≠ 0
Tactic: rw [← Nat.bit_ne_zero_iff] at h
Cleared hypotheses: h, IH
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
b : Bool
n : ℕ
h : bit b n ≠ 0
IH : n < HPow.hPow (α := ℕ) 2 n.size
⊢ bit b n < HPow.hPow (α := ℕ) 2 (bit b n).size
have bit : bit b n < HPow.hPow (α := ℕ) 2 n.size.succ
Tactic: rwa [size_bit h, bit_lt_two_pow_succ_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
n : ℕ
⊢ n < HPow.hPow (α := ℕ) 2 n.size
have zero : 0 < HPow.hPow (α := ℕ) 2 (size 0)
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
n : ℕ
zero : 0 < HPow.hPow (α := ℕ) 2 (size 0)
⊢ n < HPow.hPow (α := ℕ) 2 n.size
have bit : ∀ (b : Bool) (n : ℕ) (h : n = 0 → b = true) (IH : n < HPow.hPow (α := ℕ) 2 n.size),
  bit b n < HPow.hPow (α := ℕ) 2 (bit b 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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
b : Bool
m : ℕ
e : m = 0 → b = true
IH : ∀ {n : ℕ} (h : m < HPow.hPow (α := ℕ) 2 n), m.size ≤ n
n : ℕ
h : bit b m < HPow.hPow (α := ℕ) 2 n
⊢ (bit b m).size ≤ n
have bit : ∀ (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), (bit b m).size ≤ n
Tactic: rw [← Nat.bit_ne_zero_iff] at e
Cleared hypotheses: e, IH, n, h
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
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
⊢ (bit b m).size ≤ n
have bit : m.size.succ ≤ n
Tactic: rw [size_bit e]
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
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
⊢ m.size.succ ≤ n
have bit : ∀ (h : bit b m < HPow.hPow (α := ℕ) (β := ℕ) 2 0), m.size.succ ≤ 0
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))
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
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
⊢ m.size.succ ≤ n
have bit₁ : ∀ (n : ℕ) (h : Nat.bit b m < HPow.hPow (α := ℕ) 2 (n + 1)), m.size.succ ≤ n + 1
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))
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
m n : ℕ
h : m < HPow.hPow (α := ℕ) 2 n
⊢ m.size ≤ n
have zero : ∀ {n : ℕ} (h : 0 < HPow.hPow (α := ℕ) 2 n), size 0 ≤ 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))
Cleared hypotheses: m, n, h
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
m n : ℕ
h : m < HPow.hPow (α := ℕ) 2 n
zero : ∀ {n : ℕ} (h : 0 < HPow.hPow (α := ℕ) 2 n), size 0 ≤ n
⊢ m.size ≤ n
have bit : ∀ (b : Bool) (m : ℕ) (e : m = 0 → b = true) (IH : ∀ {n : ℕ} (h : m < HPow.hPow (α := ℕ) 2 n), m.size ≤ n) {n : ℕ}
  (h : bit b m < HPow.hPow (α := ℕ) 2 n), (bit b 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))
Cleared hypotheses: m, n, h
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
m n : ℕ
⊢ m < n.size ↔ HPow.hPow (α := ℕ) 2 m ≤ n
have rw : m < n.size ↔ ¬n < HPow.hPow (α := ℕ) 2 m
Tactic: rw [← Nat.not_lt, Decidable.iff_not_comm, Nat.not_lt, size_le]
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
m n : ℕ
rw : m < n.size ↔ ¬n < HPow.hPow (α := ℕ) 2 m
⊢ m < n.size ↔ HPow.hPow (α := ℕ) 2 m ≤ n
have rw₁ : n < HPow.hPow (α := ℕ) 2 m ↔ ¬m < n.size
Tactic: rw [← Nat.not_lt, Decidable.iff_not_comm, Nat.not_lt, size_le]
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
m n : ℕ
rw : m < n.size ↔ ¬n < HPow.hPow (α := ℕ) 2 m
rw₁ : n < HPow.hPow (α := ℕ) 2 m ↔ ¬m < n.size
⊢ m < n.size ↔ HPow.hPow (α := ℕ) 2 m ≤ n
have rw₂ : n < HPow.hPow (α := ℕ) 2 m ↔ n.size ≤ m
Tactic: rw [← Nat.not_lt, Decidable.iff_not_comm, Nat.not_lt, size_le]
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
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
⊢ m < n.size ↔ HPow.hPow (α := ℕ) 2 m ≤ n
have rw₃ : n < HPow.hPow (α := ℕ) 2 m ↔ n < HPow.hPow (α := ℕ) 2 m
Tactic: rw [← Nat.not_lt, Decidable.iff_not_comm, Nat.not_lt, size_le]
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
n : ℕ
⊢ 0 < n.size ↔ 0 < n
have rw : HPow.hPow (α := ℕ) (β := ℕ) 2 0 ≤ n ↔ 0 < n
Tactic: rw [lt_size]
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
b : Bool
n : ℕ
h : n = 0 → b = true
ih : n.bits.length = n.size
⊢ (bit b n).bits.length = (bit b n).size
have bit : (b :: n.bits).length = n.size.succ
Tactic: rw [size_bit, bits_append_bit _ _ h]
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
b : Bool
n : ℕ
h : n = 0 → b = true
ih : n.bits.length = n.size
bit : (b :: n.bits).length = n.size.succ
⊢ (Nat.bit b n).bits.length = (Nat.bit b n).size
have bit₁ : Nat.bit b n ≠ 0
Tactic: rw [size_bit, bits_append_bit _ _ h]
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
n : ℕ
⊢ n.bits.length = n.size
have zero : (bits 0).length = size 0
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Size (goal)
Goal:
n : ℕ
zero : (bits 0).length = size 0
⊢ n.bits.length = n.size
have bit : ∀ (b : Bool) (n : ℕ) (h : n = 0 → b = true) (ih : n.bits.length = n.size), (bit b n).bits.length = (bit b 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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
Goal:
n k : ℕ
iter_next : (n guess : ℕ) → ℕ := fun (n guess : ℕ) ↦ (guess + n / guess) / 2
⊢ sqrt.iter n k ≤ iter_next n (sqrt.iter n k)
have 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)
Tactic: unfold sqrt.iter
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
Goal:
n k : ℕ
iter_next : (n guess : ℕ) → ℕ := fun (n guess : ℕ) ↦ (guess + n / guess) / 2
⊢ (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 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)
Tactic: if h : (k + n / k) / 2 < k then
    simpa [if_pos h] using iter_fp_bound _ _
  else
    grind
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
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)
⊢ (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 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)
Tactic: if h : (k + n / k) / 2 < k then
    simpa [if_pos h] using iter_fp_bound _ _
  else
    grind
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
Goal:
x : ℕ
⊢ HMul.hMul (α := ℕ) 4 0 * x ≤ (0 + x) * (0 + x)
have rw : 0 ≤ (0 + x) * (0 + x)
Tactic: rw [Nat.mul_zero, Nat.zero_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
Goal:
n guess : ℕ
⊢ iter n guess * iter n guess ≤ n
have 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
Tactic: unfold sqrt.iter
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
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
have 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
Tactic: apply Nat.mul_le_of_le_div
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
Goal:
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
⊢ 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
have 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
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
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
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
⊢ 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
have 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
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
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
Goal:
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
⊢ n < (iter n guess + 1) * (iter n guess + 1)
have 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
Tactic: unfold sqrt.iter
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
Goal:
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)
have pos : ∀ (h : (guess + n / guess) / 2 < guess),
  n < (iter n ((guess + n / guess) / 2) + 1) * (iter n ((guess + n / guess) / 2) + 1)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
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)
⊢ 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)
have neg : ∀ (h : ¬(guess + n / guess) / 2 < guess), n < (guess + 1) * (guess + 1)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
Goal:
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)
have pos : n < (m + 1) * (m + 1)
Tactic: suffices n < (m + 1) * (m + 1) by
      simpa only [dif_pos h] using sqrt.lt_iter_succ_sq n m this
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
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)
have pos : 4 * (guess * guess) * n < 4 * (guess * guess) * ((m + 1) * (m + 1))
Tactic: refine Nat.lt_of_mul_lt_mul_left ?_ (a := 4 * (guess * guess))
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
Goal:
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))
have pos : (guess * guess + n) * (guess * guess + n) < 4 * (guess * guess) * ((m + 1) * (m + 1))
Tactic: apply Nat.lt_of_le_of_lt AM_GM
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
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) < HMul.hMul (α := ℕ) 2 2 * (guess * guess) * ((m + 1) * (m + 1))
have pos : (guess * guess + n) * (guess * guess + n) < 2 * guess * (m + 1) * (2 * guess * (m + 1))
Tactic: rw [Nat.mul_mul_mul_comm 2, Nat.mul_mul_mul_comm (2 * guess)]
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
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))
have pos : guess * guess + n < 2 * guess * ((guess + n / guess) / 2 + 1)
Tactic: refine Nat.mul_self_lt_mul_self (?_ : _ < _ * ((_ / 2) + 1))
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
Goal:
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)
have pos : guess * guess + n < guess * (2 * ((guess + n / guess + 1 + 1) / 2))
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]
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (hypothesis)
Goal:
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))
have aux_lemma : ∀ {a : ℕ}, a ≤ 2 * ((a + 1) / 2)
Tactic: have aux_lemma {a : ℕ} : a ≤ 2 * ((a + 1) / 2) := by lia
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
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))
have pos : guess * guess + n < guess * (guess + n / guess + 1)
Tactic: refine lt_of_lt_of_le ?_ (Nat.mul_le_mul_left _ aux_lemma)
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
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 + n / guess + 1)
have pos : guess * guess + n < guess * guess + guess * (n / guess + 1)
Tactic: rw [Nat.add_assoc, Nat.mul_add]
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (hypothesis)
Goal:
n_1 n : ℕ
⊢ (n + 2).IsSqrt (n + 2).sqrt
have h : ¬n + 2 ≤ 1
Tactic: have h : ¬ (n + 2) ≤ 1 := by simp
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
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)
have refine : n + 2 < (1 <<< ((n + 2).log2 / 2 + 1) + 1) * (1 <<< ((n + 2).log2 / 2 + 1) + 1)
Tactic: refine ⟨sqrt.iter_sq_le _ _, sqrt.lt_iter_succ_sq _ _ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
Goal:
n_1 n : ℕ
h : ¬n + 2 ≤ 1
⊢ n + 2 < (1 <<< ((n + 2).log2 / 2 + 1) + 1) * (1 <<< ((n + 2).log2 / 2 + 1) + 1)
have 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
Tactic: simp only [Nat.mul_add, Nat.add_mul, Nat.one_mul, Nat.mul_one, ← Nat.add_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
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) +
        1 <<< ((n + 2).log2 / 2 + 1) +
      1
have rw : n + 2 ≤ 1 <<< ((n + 2).log2 / 2 + 1) * 1 <<< ((n + 2).log2 / 2 + 1) + 1 <<< ((n + 2).log2 / 2 + 1) * 2
Tactic: rw [Nat.lt_add_one_iff, Nat.add_assoc, ← Nat.mul_two]
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
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
have refine : (n + 2) / 2 * 2 + (n + 2) % 2 ≤
  1 <<< ((n + 2).log2 / 2 + 1) * 1 <<< ((n + 2).log2 / 2 + 1) + 1 <<< ((n + 2).log2 / 2 + 1) * 2
Tactic: refine le_trans (Nat.le_of_eq (div_add_mod' (n + 2) 2).symm) ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
Goal:
n_1 n : ℕ
h : ¬n + 2 ≤ 1
⊢ (n + 2) / 2 * 2 + (n + 2) % 2 ≤
    1 <<< ((n + 2).log2 / 2 + 1) * 1 <<< ((n + 2).log2 / 2 + 1) + 1 <<< ((n + 2).log2 / 2 + 1) * 2
have rw : n + 2 ≤ 1 <<< ((n + 2).log2 / 2 + 1) * 1 <<< ((n + 2).log2 / 2 + 1) + 1 <<< ((n + 2).log2 / 2 + 1) * 2
Tactic: rw [show (n + 2) / 2 * 2 + (n + 2) % 2 = n + 2 by grind]
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
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
have simp : n + 2 ≤
  HPow.hPow (α := ℕ) 2 ((n + 2).log2 / 2 + 1) * HPow.hPow (α := ℕ) 2 ((n + 2).log2 / 2 + 1) +
    HPow.hPow (α := ℕ) 2 ((n + 2).log2 / 2 + 1) * 2
Tactic: simp only [shiftLeft_eq, Nat.one_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Sqrt (goal)
Goal:
n_1 n : ℕ
h : ¬n + 2 ≤ 1
⊢ n + 2 ≤
    HPow.hPow (α := ℕ) 2 ((n + 2).log2 / 2 + 1) * HPow.hPow (α := ℕ) 2 ((n + 2).log2 / 2 + 1) +
      HPow.hPow (α := ℕ) 2 ((n + 2).log2 / 2 + 1) * 2
have refine : HPow.hPow (α := ℕ) 2 ((n + 2).log2 + 1) ≤
  HPow.hPow (α := ℕ) 2 ((n + 2).log2 / 2 + 1) * HPow.hPow (α := ℕ) 2 ((n + 2).log2 / 2 + 1)
Tactic: refine Nat.le_of_lt (Nat.le_trans lt_log2_self (le_add_right_of_le ?_))