awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Log
Goal:
n : ℕ
hn : 1 < n
fuel : ℕ
ih :
  ∀ {b : ℕ} (hb : 1 < b) (hfuel : n < b ^ fuel),
    (go n b fuel).fst = b ^ ((go n b fuel).snd + 1) / n ∧ b ^ (go n b fuel).snd < n ∧ n ≤ b ^ ((go n b fuel).snd + 1)
b : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b < n
ih₁ : (go n (b * b) fuel).fst = (b * b) ^ ((go n (b * b) fuel).snd + 1) / n
ih₂ : (b * b) ^ (go n (b * b) fuel).snd < n
ih₃ : n ≤ (b * b) ^ ((go n (b * b) fuel).snd + 1)
succ :
  ∀ (ih₁ : (go n (HPow.hPow (β := ℕ) b 2) fuel).fst = b * b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n)
    (ih₂ : b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd) < n)
    (ih₃ : n ≤ b * b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1)),
    (if b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) < n then
            (b * b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
              2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1)
          else
            (b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
              2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd)).fst =
        b ^
            ((if b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) < n then
                  (b * b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
                    2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1)
                else
                  (b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
                    2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd)).snd +
              1) /
          n ∧
      b ^
            (if b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) < n then
                (b * b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
                  2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1)
              else
                (b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
                  2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd)).snd <
          n ∧
        n ≤
          b ^
            ((if b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) < n then
                  (b * b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
                    2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1)
                else
                  (b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
                    2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd)).snd +
              1)
⊢ (go n b (fuel + 1)).fst = b ^ ((go n b (fuel + 1)).snd + 1) / n ∧
    b ^ (go n b (fuel + 1)).snd < n ∧ n ≤ b ^ ((go n b (fuel + 1)).snd + 1)

Tactic:
simp_all only [go, if_neg (Nat.not_le_of_gt hbn), ← Nat.pow_two, ← Nat.pow_mul,
        Nat.div_lt_iff_lt_mul (Nat.zero_lt_of_lt hbn), Nat.div_div_eq_div_mul,
        Nat.mul_comm n b, Nat.mul_add_one, @Nat.pow_add_one' _ (2 * _ + 1),
        Nat.mul_lt_mul_left, Nat.mul_div_mul_left, Nat.zero_lt_of_lt hb]

Premises used: Nat.pow_mul, Nat.zero_lt_of_lt, Nat.clog.go, Nat.mul_div_mul_left, Nat.pow_two, Nat.mul_comm, Nat.div_lt_iff_lt_mul, Nat.mul_lt_mul_left, Nat.not_le_of_gt, Nat.mul_add_one, Nat.pow_add_one', if_neg, Nat.div_div_eq_div_mul
-- Module: Mathlib.Data.Nat.Log
Goal:
n : ℕ
hn : 1 < n
fuel : ℕ
ih :
  ∀ {b : ℕ} (hb : 1 < b) (hfuel : n < b ^ fuel),
    (go n b fuel).fst = b ^ ((go n b fuel).snd + 1) / n ∧ b ^ (go n b fuel).snd < n ∧ n ≤ b ^ ((go n b fuel).snd + 1)
b : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b < n
ih₁ : (go n (HPow.hPow (β := ℕ) b 2) fuel).fst = b * b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n
ih₂ : b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd) < n
ih₃ : n ≤ b * b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1)
h : b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) < n
⊢ (b * b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
          2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1).fst =
      b ^
          ((b * b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
                2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1).snd +
            1) /
        n ∧
    b ^
          (b * b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
              2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1).snd <
        n ∧
      n ≤
        b ^
          ((b * b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
                2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1).snd +
            1)

Tactic:
simp_all [Nat.mul_add_one, Nat.pow_add_one']

Premises used: Nat.mul_add_one, Nat.pow_add_one'
-- Module: Mathlib.Data.Nat.Log
Goal:
n : ℕ
hn : 1 < n
fuel : ℕ
ih :
  ∀ {b : ℕ} (hb : 1 < b) (hfuel : n < b ^ fuel),
    (go n b fuel).fst = b ^ ((go n b fuel).snd + 1) / n ∧ b ^ (go n b fuel).snd < n ∧ n ≤ b ^ ((go n b fuel).snd + 1)
b : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b < n
ih₁ : (go n (HPow.hPow (β := ℕ) b 2) fuel).fst = b * b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n
ih₂ : b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd) < n
ih₃ : n ≤ b * b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1)
h : ¬b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) < n
⊢ (b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n, 2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd).fst =
      b ^
          ((b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
                2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd).snd +
            1) /
        n ∧
    b ^ (b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n, 2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd).snd <
        n ∧
      n ≤
        b ^
          ((b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
                2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd).snd +
            1)

Tactic:
simp_all [Nat.mul_add_one, Nat.pow_add_one']

Premises used: Nat.mul_add_one, Nat.pow_add_one'
-- Module: Mathlib.Data.Nat.Log
Goal:
n : ℕ
hn : 1 < n
fuel : ℕ
ih :
  ∀ {b : ℕ} (hb : 1 < b) (hfuel : n < b ^ fuel),
    (go n b fuel).fst = b ^ ((go n b fuel).snd + 1) / n ∧ b ^ (go n b fuel).snd < n ∧ n ≤ b ^ ((go n b fuel).snd + 1)
b : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
⊢ b < n ∨ b ≥ n

Tactic:
cases Nat.lt_or_ge b n with
    | inr hbn => simp_all [go]
    | inl hbn =>
      rcases ih (Nat.one_mul 1 ▸ Nat.mul_lt_mul_of_lt_of_lt hb hb)
        (log.go_aux hb hfuel (Nat.le_of_lt hbn)) with ⟨ih₁, ih₂, ih₃⟩
      simp_all only [go, if_neg (Nat.not_le_of_gt hbn), ← Nat.pow_two, ← Nat.pow_mul,
        Nat.div_lt_iff_lt_mul (Nat.zero_lt_of_lt hbn), Nat.div_div_eq_div_mul,
        Nat.mul_comm n b, Nat.mul_add_one, @Nat.pow_add_one' _ (2 * _ + 1),
        Nat.mul_lt_mul_left, Nat.mul_div_mul_left, Nat.zero_lt_of_lt hb]
      split <;> simp_all [Nat.mul_add_one, Nat.pow_add_one']

Premises used: Nat.pow_mul, Nat.zero_lt_of_lt, Nat.clog.go, Nat.mul_div_mul_left, Nat.pow_two, Nat.mul_comm, Nat.mul_lt_mul_left, Nat.mul_add_one, Nat.lt_or_ge, Nat.pow_add_one', Nat.div_div_eq_div_mul
-- Module: Mathlib.Data.Nat.Log
Goal:
n b fuel : ℕ
hn : 1 < n
hb : 1 < b
hfuel : n < b ^ fuel
zero :
  ∀ {b : ℕ} (hb : 1 < b) (hfuel : n < HPow.hPow (β := ℕ) b 0),
    (go n b 0).fst = b ^ ((go n b 0).snd + 1) / n ∧ b ^ (go n b 0).snd < n ∧ n ≤ b ^ ((go n b 0).snd + 1)
succ :
  ∀ (fuel : ℕ)
    (ih :
      ∀ {b : ℕ} (hb : 1 < b) (hfuel : n < b ^ fuel),
        (go n b fuel).fst = b ^ ((go n b fuel).snd + 1) / n ∧
          b ^ (go n b fuel).snd < n ∧ n ≤ b ^ ((go n b fuel).snd + 1))
    {b : ℕ} (hb : 1 < b) (hfuel : n < b ^ (fuel + 1)),
    (go n b (fuel + 1)).fst = b ^ ((go n b (fuel + 1)).snd + 1) / n ∧
      b ^ (go n b (fuel + 1)).snd < n ∧ n ≤ b ^ ((go n b (fuel + 1)).snd + 1)
⊢ (go n b fuel).fst = b ^ ((go n b fuel).snd + 1) / n ∧ b ^ (go n b fuel).snd < n ∧ n ≤ b ^ ((go n b fuel).snd + 1)

Tactic:
induction fuel generalizing b with
  | zero => simp_all
  | succ fuel ih =>
    cases Nat.lt_or_ge b n with
    | inr hbn => simp_all [go]
    | inl hbn =>
      rcases ih (Nat.one_mul 1 ▸ Nat.mul_lt_mul_of_lt_of_lt hb hb)
        (log.go_aux hb hfuel (Nat.le_of_lt hbn)) with ⟨ih₁, ih₂, ih₃⟩
      simp_all only [go, if_neg (Nat.not_le_of_gt hbn), ← Nat.pow_two, ← Nat.pow_mul,
        Nat.div_lt_iff_lt_mul (Nat.zero_lt_of_lt hbn), Nat.div_div_eq_div_mul,
        Nat.mul_comm n b, Nat.mul_add_one, @Nat.pow_add_one' _ (2 * _ + 1),
        Nat.mul_lt_mul_left, Nat.mul_div_mul_left, Nat.zero_lt_of_lt hb]
      split <;> simp_all [Nat.mul_add_one, Nat.pow_add_one']

Premises used: Nat.pow_mul, Nat.zero_lt_of_lt, Nat.clog.go, Nat.mul_div_mul_left, Nat.pow_two, Nat.mul_comm, Nat.mul_lt_mul_left, Nat.mul_add_one, Nat.lt_or_ge, Nat.zero, Nat.pow_add_one', Nat.succ, Nat.div_div_eq_div_mul
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
hb : 1 < b
x y : ℕ
h : 1 < b ∧ 1 < x
⊢ b ^ (clog.go x b x).snd < x

Tactic:
rcases clog.go_spec h.2 hb (Nat.lt_pow_self hb) with ⟨-, H₁, H₂⟩

Premises used: Nat.lt_pow_self, Nat.clog.go_spec, And.right
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
hb : 1 < b
x y : ℕ
h : 1 < b ∧ 1 < x
H₁ : b ^ (clog.go x b x).snd < x
⊢ x ≤ b ^ ((clog.go x b x).snd + 1)

Tactic:
rcases clog.go_spec h.2 hb (Nat.lt_pow_self hb) with ⟨-, H₁, H₂⟩

Premises used: Nat.lt_pow_self, Nat.clog.go_spec, And.right
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
hb : 1 < b
x y : ℕ
h : 1 < b ∧ 1 < x
H₁ : b ^ (clog.go x b x).snd < x
H₂ : x ≤ b ^ ((clog.go x b x).snd + 1)
hy : (clog.go x b x).snd < y
⊢ (clog.go x b x).snd + 1 ≤ y

Tactic:
rw [← Nat.add_one_le_iff] at hy

Premises used: Nat.add_one_le_iff
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
hb : 1 < b
x y : ℕ
h : 1 < b ∧ 1 < x
H₁ : b ^ (clog.go x b x).snd < x
H₂ : x ≤ b ^ ((clog.go x b x).snd + 1)
hy : (clog.go x b x).snd + 1 ≤ y
⊢ (clog.go x b x).snd + 1 ≤ y ↔ x ≤ b ^ y

Tactic:
iff_of_true hy <| Nat.le_trans H₂ <| Nat.pow_le_pow_right (Nat.zero_lt_of_lt hb) hy

Premises used: Nat.zero_lt_of_lt, Nat.pow_le_pow_right, iff_of_true, Nat.le_trans
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
hb : 1 < b
x y : ℕ
h : 1 < b ∧ 1 < x
H₁ : b ^ (clog.go x b x).snd < x
H₂ : x ≤ b ^ ((clog.go x b x).snd + 1)
hy : (clog.go x b x).snd + 1 ≤ y
⊢ (clog.go x b x).snd + 1 ≤ y ↔ x ≤ b ^ y

Tactic:
exact iff_of_true hy <| Nat.le_trans H₂ <| Nat.pow_le_pow_right (Nat.zero_lt_of_lt hb) hy

Premises used: Nat.zero_lt_of_lt, Nat.pow_le_pow_right, iff_of_true, Nat.le_trans
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
hb : 1 < b
x y : ℕ
h : 1 < b ∧ 1 < x
H₁ : b ^ (clog.go x b x).snd < x
H₂ : x ≤ b ^ ((clog.go x b x).snd + 1)
hy : (clog.go x b x).snd ≥ y
case1 : x > b ^ y
⊢ (clog.go x b x).snd + 1 ≤ y ↔ x ≤ b ^ y

Tactic:
apply_rules [iff_of_false, Nat.not_le_of_gt, Nat.lt_add_one_of_le]

Premises used: Nat.lt_add_one_of_le, iff_of_false, Nat.not_le_of_gt
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
hb : 1 < b
x y : ℕ
h : 1 < b ∧ 1 < x
H₁ : b ^ (clog.go x b x).snd < x
H₂ : x ≤ b ^ ((clog.go x b x).snd + 1)
hy : (clog.go x b x).snd ≥ y
⊢ x > b ^ y

Tactic:
Nat.lt_of_le_of_lt (Nat.pow_le_pow_right (Nat.zero_lt_of_lt hb) hy) H₁

Premises used: Nat.zero_lt_of_lt, Nat.lt_of_le_of_lt, Nat.pow_le_pow_right
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
hb : 1 < b
x y : ℕ
h : 1 < b ∧ 1 < x
H₁ : b ^ (clog.go x b x).snd < x
H₂ : x ≤ b ^ ((clog.go x b x).snd + 1)
hy : (clog.go x b x).snd ≥ y
⊢ x > b ^ y

Tactic:
exact Nat.lt_of_le_of_lt (Nat.pow_le_pow_right (Nat.zero_lt_of_lt hb) hy) H₁

Premises used: Nat.zero_lt_of_lt, Nat.lt_of_le_of_lt, Nat.pow_le_pow_right
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
hb : 1 < b
x y : ℕ
h : 1 < b ∧ 1 < x
H₁ : b ^ (clog.go x b x).snd < x
H₂ : x ≤ b ^ ((clog.go x b x).snd + 1)
⊢ (clog.go x b x).snd < y ∨ (clog.go x b x).snd ≥ y

Tactic:
cases Nat.lt_or_ge (clog.go x b x).2 y with
    | inl hy =>
      rw [← Nat.add_one_le_iff] at hy
      exact iff_of_true hy <| Nat.le_trans H₂ <| Nat.pow_le_pow_right (Nat.zero_lt_of_lt hb) hy
    | inr hy =>
      apply_rules [iff_of_false, Nat.not_le_of_gt, Nat.lt_add_one_of_le]
      exact Nat.lt_of_le_of_lt (Nat.pow_le_pow_right (Nat.zero_lt_of_lt hb) hy) H₁

Premises used: Nat.clog.go, Nat.lt_add_one_of_le, iff_of_false, Nat.add_one_le_iff, Nat.le_trans, Nat.not_le_of_gt, Nat.lt_or_ge, Prod.snd
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
hb : 1 < b
x y : ℕ
h : ¬(1 < b ∧ 1 < x)
⊢ 0 ≤ y ↔ x ≤ b ^ y

Tactic:
grind [Nat.one_le_pow]

Premises used: Nat.one_le_pow
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
hb : 1 < b
x y : ℕ
case1 : ∀ (h : 1 < b ∧ 1 < x), (clog.go x b x).snd + 1 ≤ y ↔ x ≤ b ^ y
case2 : ∀ (h : ¬(1 < b ∧ 1 < x)), 0 ≤ y ↔ x ≤ b ^ y
⊢ clog b x ≤ y ↔ x ≤ b ^ y

Tactic:
fun_cases clog with
  | case1 h =>
    rcases clog.go_spec h.2 hb (Nat.lt_pow_self hb) with ⟨-, H₁, H₂⟩
    cases Nat.lt_or_ge (clog.go x b x).2 y with
    | inl hy =>
      rw [← Nat.add_one_le_iff] at hy
      exact iff_of_true hy <| Nat.le_trans H₂ <| Nat.pow_le_pow_right (Nat.zero_lt_of_lt hb) hy
    | inr hy =>
      apply_rules [iff_of_false, Nat.not_le_of_gt, Nat.lt_add_one_of_le]
      exact Nat.lt_of_le_of_lt (Nat.pow_le_pow_right (Nat.zero_lt_of_lt hb) hy) H₁
  | case2 h => grind [Nat.one_le_pow]

Premises used: Nat.clog.go, Nat.lt_add_one_of_le, iff_of_false, Nat.add_one_le_iff, Nat.one_le_pow, Nat.not_le_of_gt, Nat.lt_or_ge, Nat.clog, Prod.snd
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
hn : 1 < n
rw : 0 < (clog.go n b n).snd + 1
hc : 1 < b ∧ 1 < n
⊢ 0 < clog b n

Tactic:
rw [clog, if_pos]

Premises used: if_pos, Nat.clog
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
hn : 1 < n
⊢ 0 < (clog.go n b n).snd + 1

Tactic:
Nat.succ_pos _

Premises used: Nat.succ_pos
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
hn : 1 < n
⊢ 1 < b ∧ 1 < n

Tactic:
⟨hb, hn⟩

Premises used: And.intro
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
hn : 1 < n
⊢ 0 < (clog.go n b n).snd + 1

Tactic:
exacts [Nat.succ_pos _, ⟨hb, hn⟩]

Premises used: Nat.succ_pos
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
hn : 1 < n
H : ∀ (c : ℕ), clog b n ≤ c ↔ clog b ((n + b - 1) / b) + 1 ≤ c
⊢ clog b n = clog b ((n + b - 1) / b) + 1

Tactic:
apply eq_of_forall_ge_iff

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
hn : 1 < n
⊢ clog b n ≤ 0 ↔ clog b ((n + b - 1) / b) + 1 ≤ 0

Tactic:
simp [Nat.ne_of_gt <| clog_pos hb hn]

Premises used: Nat.clog_pos, Nat.ne_of_gt
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
hn : 1 < n
c : ℕ
H : n ≤ b ^ c * b ↔ n + b - 1 ≤ b ^ c * b + b - 1
⊢ clog b n ≤ c + 1 ↔ clog b ((n + b - 1) / b) + 1 ≤ c + 1

Tactic:
simp only [clog_le_iff_le_pow, Nat.pow_add_one, Nat.add_le_add_iff_right, Nat.zero_lt_of_lt hb,
      div_le_iff_le_mul, hb]

Premises used: Nat.add_le_add_iff_right, Nat.pow_add_one, Nat.clog_le_iff_le_pow, Nat.zero_lt_of_lt, Nat.div_le_iff_le_mul
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
hn : 1 < n
c : ℕ
⊢ n ≤ b ^ c * b ↔ n + b - 1 ≤ b ^ c * b + b - 1

Tactic:
grind
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ clog b n = clog b ((n + b - 1) / b) + 1

Tactic:
clog_of_one_lt hb hn

Premises used: Nat.clog_of_one_lt
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
hn₁ : (n + b - 1) / b ≤ 1
⊢ clog b n = 1

Tactic:
rw [clog_of_two_le (hn.trans h) hn, clog_of_right_le_one]

Premises used: Nat.clog_of_right_le_one, Nat.clog_of_two_le, LE.le.trans
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
hn₁ : n + b - 1 < succ 1 * b
hn₂ : 0 < b
⊢ (n + b - 1) / b ≤ 1

Tactic:
rw [← Nat.lt_succ_iff, Nat.div_lt_iff_lt_mul]

Premises used: Nat.div_lt_iff_lt_mul, Nat.lt_succ_iff
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ n + b - 1 < succ 1 * b

Tactic:
lia
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ 0 < b

Tactic:
lia
-- Module: Mathlib.Data.Nat.Log
Goal:
b x y : ℕ
h : x ≤ b ^ y
inl : ∀ (hb : 1 < b), clog b x ≤ y
inr : ∀ (hb : 1 ≥ b), clog b x ≤ y
⊢ clog b x ≤ y

Tactic:
rcases Nat.lt_or_ge 1 b with hb | hb

Premises used: Nat.lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Log
Goal:
b x y : ℕ
h : x ≤ b ^ y
hb : 1 < b
inl inl₁ inl₂ inl₃ : x ≤ b ^ y
⊢ clog b x ≤ y

Tactic:
rwa [clog_le_iff_le_pow hb]

Premises used: Nat.clog_le_iff_le_pow
-- Module: Mathlib.Data.Nat.Log
Goal:
b x y : ℕ
h : x ≤ b ^ y
hb : 1 ≥ b
⊢ clog b x ≤ y

Tactic:
grind [clog_of_left_le_one]

Premises used: Nat.clog_of_left_le_one
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
hb : 1 < b
x y : ℕ
⊢ y < clog b x ↔ b ^ y < x

Tactic:
lt_iff_lt_of_le_iff_le (clog_le_iff_le_pow hb)

Premises used: Nat.clog_le_iff_le_pow, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Data.Nat.Log
Goal:
b x y : ℕ
h : y < clog b x
⊢ b ^ y < x

Tactic:
lt_imp_lt_of_le_imp_le clog_le_of_le_pow h

Premises used: lt_imp_lt_of_le_imp_le, Nat.clog_le_of_le_pow
-- Module: Mathlib.Data.Nat.Log
Goal:
b x : ℕ
hb : 1 < b
z : ℕ
rw : b ^ x ≤ b ^ z ↔ x ≤ z
rw₁ rw₂ : x ≤ z ↔ x ≤ z
⊢ clog b (b ^ x) ≤ z ↔ x ≤ z

Tactic:
rw [clog_le_iff_le_pow hb, Nat.pow_le_pow_iff_right hb]

Premises used: Nat.clog_le_iff_le_pow, Nat.pow_le_pow_iff_right
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
hb : 1 < b
x : ℕ
hx : 1 < x
rw : (clog b x).pred < clog b x
⊢ b ^ (clog b x).pred < x

Tactic:
rw [← lt_clog_iff_pow_lt hb]

Premises used: Nat.lt_clog_iff_pow_lt
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
hb : 1 < b
x : ℕ
hx : 1 < x
⊢ (clog b x).pred < clog b x

Tactic:
pred_lt (clog_pos hb hx).ne'

Premises used: LT.lt.ne', Nat.pred_lt, Nat.clog_pos
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
hb : 1 < b
x : ℕ
hx : 1 < x
⊢ (clog b x).pred < clog b x

Tactic:
exact pred_lt (clog_pos hb hx).ne'

Premises used: LT.lt.ne', Nat.pred_lt, Nat.clog_pos
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
hb : 1 < b
x : ℕ
⊢ x ≤ b ^ clog b x

Tactic:
(clog_le_iff_le_pow hb).1 le_rfl

Premises used: le_rfl, Nat.clog_le_iff_le_pow, Iff.mp
-- Module: Mathlib.Data.Nat.Log
Goal:
b n m : ℕ
h : n ≤ m
inl : ∀ (hb : b ≤ 1), clog b n ≤ clog b m
inr : ∀ (hb : 1 < b), clog b n ≤ clog b m
⊢ clog b n ≤ clog b m

Tactic:
rcases le_or_gt b 1 with hb | hb

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Log
Goal:
b n m : ℕ
h : n ≤ m
hb : b ≤ 1
inl : 0 ≤ clog b m
⊢ clog b n ≤ clog b m

Tactic:
rw [clog_of_left_le_one hb]

Premises used: Nat.clog_of_left_le_one
-- Module: Mathlib.Data.Nat.Log
Goal:
b n m : ℕ
h : n ≤ m
hb : b ≤ 1
⊢ 0 ≤ clog b m

Tactic:
zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Nat.Log
Goal:
b n m : ℕ
h : n ≤ m
hb : b ≤ 1
⊢ 0 ≤ clog b m

Tactic:
exact zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Nat.Log
Goal:
b n m : ℕ
h : n ≤ m
hb : 1 < b
inr : n ≤ b ^ clog b m
⊢ clog b n ≤ clog b m

Tactic:
rw [clog_le_iff_le_pow hb]

Premises used: Nat.clog_le_iff_le_pow
-- Module: Mathlib.Data.Nat.Log
Goal:
b n m : ℕ
h : n ≤ m
hb : 1 < b
⊢ n ≤ b ^ clog b m

Tactic:
h.trans (le_pow_clog hb _)

Premises used: Nat.le_pow_clog, LE.le.trans
-- Module: Mathlib.Data.Nat.Log
Goal:
b n m : ℕ
h : n ≤ m
hb : 1 < b
⊢ n ≤ b ^ clog b m

Tactic:
exact h.trans (le_pow_clog hb _)

Premises used: Nat.le_pow_clog, LE.le.trans
-- Module: Mathlib.Data.Nat.Log
Goal:
b c n : ℕ
hc : 1 < c
hb : c ≤ b
rw : n ≤ b ^ clog c n
⊢ clog b n ≤ clog c n

Tactic:
rw [clog_le_iff_le_pow (lt_of_lt_of_le hc hb)]

Premises used: Nat.clog_le_iff_le_pow, lt_of_lt_of_le
-- Module: Mathlib.Data.Nat.Log
Goal:
b c n : ℕ
hc : 1 < c
hb : c ≤ b
⊢ n ≤ c ^ clog c n

Tactic:
le_pow_clog hc _

Premises used: Nat.le_pow_clog
-- Module: Mathlib.Data.Nat.Log
Goal:
b c n : ℕ
hc : 1 < c
hb : c ≤ b
⊢ c ^ clog c n ≤ b ^ clog c n

Tactic:
Nat.pow_le_pow_left hb _

Premises used: Nat.pow_le_pow_left
-- Module: Mathlib.Data.Nat.Log
Goal:
b c n : ℕ
hc : 1 < c
hb : c ≤ b
⊢ n ≤ b ^ clog c n

Tactic:
calc
    n ≤ c ^ clog c n := le_pow_clog hc _
    _ ≤ b ^ clog c n := Nat.pow_le_pow_left hb _

Premises used: Nat.le_pow_clog, Nat.clog, Nat.pow_le_pow_left
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
⊢ Monotone (clog b)

Tactic:
fun _ _ => clog_mono_right _

Premises used: Monotone, Nat.clog_mono_right
-- Module: Mathlib.Data.Nat.Log
Goal:
n : ℕ
⊢ AntitoneOn (β := ℕ) (fun (b : ℕ) ↦ clog b n) (Set.Ioi 1)

Tactic:
fun _ hc _ _ hb => clog_anti_left (Set.mem_Iio.1 hc) hb

Premises used: Set.mem_Iio, Iff.mp, AntitoneOn, Nat.clog_anti_left
-- Module: Mathlib.Data.Nat.Log
Goal:
b c m n : ℕ
hc : 1 < c
hb : c ≤ b
hmn : m ≤ n
⊢ clog c m ≤ clog c n

Tactic:
gcongr
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
inl : ∀ (hb : b ≤ 1), log b n ≤ clog b n
inr : ∀ (hb : 1 < b), log b n ≤ clog b n
⊢ log b n ≤ clog b n

Tactic:
obtain hb | hb := le_or_gt b 1

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : b ≤ 1
inl : 0 ≤ clog b n
⊢ log b n ≤ clog b n

Tactic:
rw [log_of_left_le_one hb]

Premises used: Nat.log_of_left_le_one
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : b ≤ 1
⊢ 0 ≤ clog b n

Tactic:
zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : b ≤ 1
⊢ 0 ≤ clog b n

Tactic:
exact zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
hb : 1 < b
inr : 0 ≤ clog b 0
⊢ log b 0 ≤ clog b 0

Tactic:
rw [log_zero_right]

Premises used: Nat.log_zero_right
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
hb : 1 < b
⊢ 0 ≤ clog b 0

Tactic:
zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
hb : 1 < b
⊢ 0 ≤ clog b 0

Tactic:
exact zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
hb : 1 < b
n : ℕ
⊢ log b (n + 1) ≤ clog b (n + 1)

Tactic:
(Nat.pow_le_pow_iff_right hb).1
      ((pow_log_le_self b n.succ_ne_zero).trans <| le_pow_clog hb _)

Premises used: Nat.le_pow_clog, Nat.succ_ne_zero, Iff.mp, Nat.pow_le_pow_iff_right, LE.le.trans, Nat.pow_log_le_self
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
hb : 1 < b
n : ℕ
⊢ log b (n + 1) ≤ clog b (n + 1)

Tactic:
exact (Nat.pow_le_pow_iff_right hb).1
      ((pow_log_le_self b n.succ_ne_zero).trans <| le_pow_clog hb _)

Premises used: Nat.le_pow_clog, Nat.succ_ne_zero, Iff.mp, Nat.pow_le_pow_iff_right, LE.le.trans, Nat.pow_log_le_self
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
inr : log b 0 ≤ clog b 0
inr₁ : ∀ (n : ℕ), log b (n + 1) ≤ clog b (n + 1)
⊢ log b n ≤ clog b n

Tactic:
cases n with
  | zero =>
    rw [log_zero_right]
    exact zero_le _
  | succ n =>
    exact (Nat.pow_le_pow_iff_right hb).1
      ((pow_log_le_self b n.succ_ne_zero).trans <| le_pow_clog hb _)

Premises used: Nat.zero_le, Nat.log_zero_right, Nat.le_pow_clog, Nat.succ_ne_zero, Iff.mp, Nat.pow_le_pow_iff_right, Nat.zero, LE.le.trans, Nat.succ, Nat.pow_log_le_self
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
⊢ clog b n < clog b (n + 1) ↔ b ^ clog b n = n

Tactic:
⟨fun H ↦ ?_, fun H ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
refine_1 : ∀ (H : clog b n < clog b (n + 1)), b ^ clog b n = n
refine_2 : ∀ (H : b ^ clog b n = n), clog b n < clog b (n + 1)
⊢ clog b n < clog b (n + 1) ↔ b ^ clog b n = n

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ ?_⟩
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
H : clog b n < clog b (n + 1)
apply : b ^ clog b n ≤ n
⊢ b ^ clog b n = n

Tactic:
apply le_antisymm _ (le_pow_clog hb n)

Premises used: Nat.le_pow_clog, le_antisymm
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
H : clog b n < clog b (n + 1)
a : b ^ clog b n < n.succ
⊢ b ^ clog b n ≤ n

Tactic:
apply le_of_lt_succ

Premises used: Nat.le_of_lt_succ
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
H : clog b n < clog b (n + 1)
⊢ b ^ clog b n < n.succ

Tactic:
(lt_clog_iff_pow_lt hb).mp H

Premises used: Nat.lt_clog_iff_pow_lt, Iff.mp
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
H : clog b n < clog b (n + 1)
⊢ b ^ clog b n < n.succ

Tactic:
exact (lt_clog_iff_pow_lt hb).mp H

Premises used: Nat.lt_clog_iff_pow_lt, Iff.mp
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
H : b ^ clog b n = n
refine_2 : n < n + 1
⊢ clog b n < clog b (n + 1)

Tactic:
rw [lt_clog_iff_pow_lt hb, H]

Premises used: Nat.lt_clog_iff_pow_lt
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
H : b ^ clog b n = n
⊢ n < n + 1

Tactic:
n.lt_add_one

Premises used: Nat.lt_add_one
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
H : b ^ clog b n = n
⊢ n < n + 1

Tactic:
exact n.lt_add_one

Premises used: Nat.lt_add_one
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
rw : clog b n = clog b (n + 1) ↔ clog b (n + 1) ≤ clog b n
⊢ clog b n = clog b (n + 1) ↔ b ^ clog b n ≠ n

Tactic:
rw [ne_eq, ← clog_lt_clog_succ_iff hb, not_lt]

Premises used: ne_eq, not_lt, Nat.clog_lt_clog_succ_iff