awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Log
Goal:
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hm : m ≠ 0
hb : b ≤ 1
inr :
  ∀ (h : m ≠ 0 ∨ LT.lt (α := ℕ) 1 0 ∧ n ≠ 0) (hb : LE.le (α := ℕ) 0 1),
    log 0 n = m ↔ HPow.hPow (α := ℕ) 0 m ≤ n ∧ n < HPow.hPow (α := ℕ) 0 (m + 1)
inr₁ :
  ∀ (h : m ≠ 0 ∨ LT.lt (α := ℕ) 1 1 ∧ n ≠ 0) (hb : LE.le (α := ℕ) 1 1),
    log 1 n = m ↔ HPow.hPow (α := ℕ) 1 m ≤ n ∧ n < HPow.hPow (α := ℕ) 1 (m + 1)
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)

Tactic:
obtain rfl | rfl := le_one_iff_eq_zero_or_eq_one.1 hb

Premises used: Nat.le_one_iff_eq_zero_or_eq_one, Iff.mp, rfl
-- Module: Mathlib.Data.Nat.Log
Goal:
m n : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ LT.lt (α := ℕ) 1 0 ∧ n ≠ 0
hb : LE.le (α := ℕ) 0 1
⊢ 0 = m ↔ HPow.hPow (α := ℕ) 0 m ≤ n ∧ n < HPow.hPow (α := ℕ) 0 (m + 1)

Tactic:
lia
-- Module: Mathlib.Data.Nat.Log
Goal:
m n : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ LT.lt (α := ℕ) 1 1 ∧ n ≠ 0
hb : LE.le (α := ℕ) 1 1
⊢ 0 = m ↔ HPow.hPow (α := ℕ) 1 m ≤ n ∧ n < HPow.hPow (α := ℕ) 1 (m + 1)

Tactic:
lia
-- Module: Mathlib.Data.Nat.Log
Goal:
b m : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ 1 < b ∧ Ne (α := ℕ) 0 0
⊢ log b 0 = m ↔ b ^ m ≤ 0 ∧ 0 < b ^ (m + 1)

Tactic:
simp [@eq_comm _ 0, hm]

Premises used: eq_comm
-- Module: Mathlib.Data.Nat.Log
Goal:
b m n : ℕ
h₁ : b ^ m ≤ n
h₂ : n < b ^ (m + 1)
inl : ∀ (h₁ : HPow.hPow (β := ℕ) b 0 ≤ n) (h₂ : n < b ^ HAdd.hAdd (α := ℕ) 0 1), log b n = 0
inr : ∀ (hm : m ≠ 0), log b n = m
⊢ log b n = m

Tactic:
rcases eq_or_ne m 0 with (rfl | hm)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
h₁ : HPow.hPow (β := ℕ) b 0 ≤ n
h₂ : n < b ^ HAdd.hAdd (α := ℕ) 0 1
⊢ n < b

Tactic:
rw [Nat.pow_one] at h₂

Premises used: Nat.pow_one
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
h₁ : HPow.hPow (β := ℕ) b 0 ≤ n
h₂ : n < b
⊢ log b n = 0

Tactic:
log_of_lt h₂

Premises used: Nat.log_of_lt
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
h₁ : HPow.hPow (β := ℕ) b 0 ≤ n
h₂ : n < b
⊢ log b n = 0

Tactic:
exact log_of_lt h₂

Premises used: Nat.log_of_lt
-- Module: Mathlib.Data.Nat.Log
Goal:
b m n : ℕ
h₁ : b ^ m ≤ n
h₂ : n < b ^ (m + 1)
hm : m ≠ 0
⊢ log b n = m

Tactic:
(log_eq_iff (Or.inl hm)).2 ⟨h₁, h₂⟩

Premises used: Iff.mpr, Nat.log_eq_iff, And.intro, Or.inl
-- Module: Mathlib.Data.Nat.Log
Goal:
b m n : ℕ
h₁ : b ^ m ≤ n
h₂ : n < b ^ (m + 1)
hm : m ≠ 0
⊢ log b n = m

Tactic:
exact (log_eq_iff (Or.inl hm)).2 ⟨h₁, h₂⟩

Premises used: Iff.mpr, Nat.log_eq_iff, And.intro, Or.inl
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
hb : 1 < b
x : ℕ
⊢ log b (b ^ x) = x

Tactic:
log_eq_of_pow_le_of_lt_pow le_rfl (Nat.pow_lt_pow_right hb x.lt_succ_self)

Premises used: le_rfl, Nat.lt_succ_self, Nat.log_eq_of_pow_le_of_lt_pow, Nat.pow_lt_pow_right
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
rw : HPow.hPow (β := ℕ) b 1 ≤ n ∧ n < b ^ HAdd.hAdd (α := ℕ) 1 1 ↔ b ≤ n ∧ n < b * b
rw₁ : HPow.hPow (β := ℕ) b 1 ≤ n ∧ n < HPow.hPow (β := ℕ) b 1 * HPow.hPow (β := ℕ) b 1 ↔ b ≤ n ∧ n < b * b
rw₂ rw₃ : b ≤ n ∧ n < b * b ↔ b ≤ n ∧ n < b * b
⊢ log b n = 1 ↔ b ≤ n ∧ n < b * b

Tactic:
rw [log_eq_iff (Or.inl Nat.one_ne_zero), Nat.pow_add, Nat.pow_one]

Premises used: Nat.pow_add, Nat.log_eq_iff, Nat.one_ne_zero, Nat.pow_one, Or.inl
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
⊢ log b n = 1 ↔ n < b * b ∧ 1 < b ∧ b ≤ n

Tactic:
log_eq_one_iff'.trans
    ⟨fun h => ⟨h.2, lt_mul_self_iff.1 (h.1.trans_lt h.2), h.1⟩, fun h => ⟨h.2.2, h.1⟩⟩

Premises used: Nat.lt_mul_self_iff, Nat.log_eq_one_iff', And.right, And.left, And.intro, Iff.intro, Iff.mp, Iff.trans, LE.le.trans_lt
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
h₁ : b ^ (log b n + 1) ≤ n * b
h₂ : n * b < b ^ (log b n + 1 + 1)
⊢ log b (n * b) = log b n + 1

Tactic:
apply log_eq_of_pow_le_of_lt_pow

Premises used: Nat.log_eq_of_pow_le_of_lt_pow
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
h₁ : b ^ log b n * b ≤ n * b
⊢ b ^ (log b n + 1) ≤ n * b

Tactic:
rw [pow_succ', Nat.mul_comm b]

Premises used: Nat.pow_succ', Nat.mul_comm
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
h₂ : n * b < b ^ (log b n + 1) * b
⊢ n * b < b ^ (log b n + 1 + 1)

Tactic:
rw [pow_succ', Nat.mul_comm b]

Premises used: Nat.pow_succ', Nat.mul_comm
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ b ^ log b n * b ≤ n * b

Tactic:
Nat.mul_le_mul_right _ (pow_log_le_self _ hn)

Premises used: Nat.mul_le_mul_right, Nat.pow_log_le_self
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ n * b < b ^ (log b n + 1) * b

Tactic:
(Nat.mul_lt_mul_right (Nat.zero_lt_one.trans hb)).2 (lt_pow_succ_log_self hb _)

Premises used: Iff.mpr, Nat.lt_pow_succ_log_self, LT.lt.trans, Nat.mul_lt_mul_right, Nat.zero_lt_one
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ b ^ log b n * b ≤ n * b

Tactic:
exacts [Nat.mul_le_mul_right _ (pow_log_le_self _ hn),
    (Nat.mul_lt_mul_right (Nat.zero_lt_one.trans hb)).2 (lt_pow_succ_log_self hb _)]

Premises used: Iff.mpr, Nat.mul_le_mul_right, Nat.lt_pow_succ_log_self, LT.lt.trans, Nat.pow_log_le_self, Nat.mul_lt_mul_right, Nat.zero_lt_one
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
rw : HPow.hPow (β := ℕ) b 0 ≤ HAdd.hAdd (α := ℕ) 0 1
rw₁ rw₂ : LE.le (α := ℕ) 1 1
⊢ b ^ log b 0 ≤ HAdd.hAdd (α := ℕ) 0 1

Tactic:
rw [log_zero_right, Nat.pow_zero]

Premises used: Nat.log_zero_right, Nat.pow_zero
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
⊢ Monotone (log b)

Tactic:
monotone_nat_of_le_succ fun n => ?_

Premises used: monotone_nat_of_le_succ
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
refine : ∀ (n : ℕ), log b n ≤ log b (n + 1)
⊢ Monotone (log b)

Tactic:
refine monotone_nat_of_le_succ fun n => ?_

Premises used: monotone_nat_of_le_succ
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
inl : ∀ (hb : b ≤ 1), log b n ≤ log b (n + 1)
inr : ∀ (hb : 1 < b), log b n ≤ log b (n + 1)
⊢ log b n ≤ log b (n + 1)

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 : ℕ
hb : b ≤ 1
inl : 0 ≤ log b (n + 1)
⊢ log b n ≤ log b (n + 1)

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 ≤ log b (n + 1)

Tactic:
zero_le _

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

Tactic:
exact zero_le _

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

Tactic:
le_log_of_pow_le hb (pow_log_le_add_one _ _)

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

Tactic:
exact le_log_of_pow_le hb (pow_log_le_add_one _ _)

Premises used: Nat.le_log_of_pow_le, Nat.pow_log_le_add_one
-- Module: Mathlib.Data.Nat.Log
Goal:
b n m : ℕ
h : n ≤ m
⊢ log b n ≤ log b m

Tactic:
log_monotone h

Premises used: Nat.log_monotone
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b n < log b (n + 1) ↔ b ^ log b (n + 1) = n + 1

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

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

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

Tactic:
apply le_antisymm _ (Nat.lt_pow_of_log_lt hb H)

Premises used: le_antisymm
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
H : log b n < log b (n + 1)
⊢ b ^ log b (n + 1) ≤ n + 1

Tactic:
Nat.pow_log_le_self b (Ne.symm (Nat.zero_ne_add_one n))

Premises used: Ne.symm, Nat.pow_log_le_self, Nat.zero_ne_add_one
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
H : log b n < log b (n + 1)
⊢ b ^ log b (n + 1) ≤ n + 1

Tactic:
exact Nat.pow_log_le_self b (Ne.symm (Nat.zero_ne_add_one n))

Premises used: Ne.symm, Nat.pow_log_le_self, Nat.zero_ne_add_one
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
H : b ^ log b (n + 1) = n + 1
refine_2 : n < b ^ log b (n + 1)
⊢ log b n < log b (n + 1)

Tactic:
apply Nat.log_lt_of_lt_pow hn

Premises used: Nat.log_lt_of_lt_pow
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
H : b ^ log b (n + 1) = n + 1
⊢ n < b ^ log b (n + 1)

Tactic:
simp [H]
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
rw : log b n = log b (n + 1) ↔ log b (n + 1) ≤ log b n
⊢ log b n = log b (n + 1) ↔ b ^ log b (n + 1) ≠ n + 1

Tactic:
rw [ne_eq, ← log_lt_log_succ_iff hb hn, not_lt]

Premises used: ne_eq, not_lt, Nat.log_lt_log_succ_iff
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
simp : log b (n + 1) ≤ log b n → log b n ≤ log b (n + 1)
⊢ log b n = log b (n + 1) ↔ log b (n + 1) ≤ log b n

Tactic:
simp only [le_antisymm_iff, and_iff_right_iff_imp]

Premises used: le_antisymm_iff, and_iff_right_iff_imp
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b (n + 1) ≤ log b n → log b n ≤ log b (n + 1)

Tactic:
fun _ ↦ log_monotone (le_add_right n 1)

Premises used: Nat.le_add_right, OfNat.ofNat, Nat.log_monotone
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b (n + 1) ≤ log b n → log b n ≤ log b (n + 1)

Tactic:
exact fun _ ↦ log_monotone (le_add_right n 1)

Premises used: Nat.le_add_right, OfNat.ofNat, Nat.log_monotone
-- Module: Mathlib.Data.Nat.Log
Goal:
b c n : ℕ
hc : 1 < c
hb : c ≤ b
inl : log b 0 ≤ log c 0
inr : ∀ (hn : n ≠ 0), log b n ≤ log c n
⊢ log b n ≤ log c n

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Log
Goal:
b c : ℕ
hc : 1 < c
hb : c ≤ b
inl : 0 ≤ log c 0
inl₁ inl₂ : LE.le (α := ℕ) 0 0
⊢ log b 0 ≤ log c 0

Tactic:
rw [log_zero_right, log_zero_right]

Premises used: Nat.log_zero_right
-- Module: Mathlib.Data.Nat.Log
Goal:
b c n : ℕ
hc : 1 < c
hb : c ≤ b
hn : n ≠ 0
inr : c ^ log b n ≤ n
⊢ log b n ≤ log c n

Tactic:
apply le_log_of_pow_le hc

Premises used: Nat.le_log_of_pow_le
-- Module: Mathlib.Data.Nat.Log
Goal:
b c n : ℕ
hc : 1 < c
hb : c ≤ b
hn : n ≠ 0
⊢ c ^ log b n ≤ b ^ log b 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
hn : n ≠ 0
⊢ b ^ log b n ≤ n

Tactic:
pow_log_le_self _ hn

Premises used: Nat.pow_log_le_self
-- Module: Mathlib.Data.Nat.Log
Goal:
b c n : ℕ
hc : 1 < c
hb : c ≤ b
hn : n ≠ 0
⊢ c ^ log b n ≤ n

Tactic:
calc
    c ^ log b n ≤ b ^ log b n := Nat.pow_le_pow_left hb _
    _ ≤ n := pow_log_le_self _ hn

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

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

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

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

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 : ℕ
hb : b ≤ 1
inl : 0 = log b n - 1
inl₁ : 0 = HSub.hSub (α := ℕ) 0 1
inl₂ inl₃ : Eq (α := ℕ) 0 0
⊢ log b (n / b) = log b n - 1

Tactic:
rw [log_of_left_le_one hb, log_of_left_le_one hb, Nat.zero_sub]

Premises used: Nat.zero_sub, Nat.log_of_left_le_one
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
inr : ∀ (h : n < b), log b (n / b) = log b n - 1
inr₁ : ∀ (h : b ≤ n), log b (n / b) = log b n - 1
⊢ log b (n / b) = log b n - 1

Tactic:
rcases lt_or_ge n b with h | h

Premises used: lt_or_ge
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
h : n < b
inr : log b 0 = log b n - 1
inr₁ : log b 0 = HSub.hSub (α := ℕ) 0 1
inr₂ inr₃ : 0 = HSub.hSub (α := ℕ) 0 1
⊢ log b (n / b) = log b n - 1

Tactic:
rw [div_eq_of_lt h, log_of_lt h, log_zero_right]

Premises used: Nat.log_zero_right, Nat.log_of_lt, Nat.div_eq_of_lt
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
h : b ≤ n
inr : log b (n / b) = log b (n / b) + 1 - 1
inr₁ inr₂ : log b (n / b) = log b (n / b)
⊢ log b (n / b) = log b n - 1

Tactic:
rw [log_of_one_lt_of_le hb h, Nat.add_sub_cancel_right]

Premises used: Nat.add_sub_cancel_right, Nat.log_of_one_lt_of_le
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
⊢ log b (n / HPow.hPow (β := ℕ) b 0) = log b n - 0

Tactic:
grind
-- Module: Mathlib.Data.Nat.Log
Goal:
b n k : ℕ
hk : log b (n / b ^ k) = log b n - k
succ : log b (n / (b ^ k * b)) = log b n - (k + 1)
succ₁ : log b (n / b ^ k / b) = log b n - (k + 1)
succ₂ : log b (n / b ^ k) - 1 = log b n - (k + 1)
succ₃ : log b n - k - 1 = log b n - (k + 1)
succ₄ succ₅ : log b n - k - 1 = log b n - k - 1
⊢ log b (n / b ^ (k + 1)) = log b n - (k + 1)

Tactic:
rw [Nat.pow_succ, ← Nat.div_div_eq_div_mul, log_div_base, hk, sub_add_eq]

Premises used: Nat.sub_add_eq, Nat.pow_succ, Nat.log_div_base, Nat.div_div_eq_div_mul
-- Module: Mathlib.Data.Nat.Log
Goal:
b n k : ℕ
zero : log b (n / HPow.hPow (β := ℕ) b 0) = log b n - 0
succ : ∀ (k : ℕ) (hk : log b (n / b ^ k) = log b n - k), log b (n / b ^ (k + 1)) = log b n - (k + 1)
⊢ log b (n / b ^ k) = log b n - k

Tactic:
induction k with
  | zero => grind
  | succ k hk => rw [Nat.pow_succ, ← Nat.div_div_eq_div_mul, log_div_base, hk, sub_add_eq]

Premises used: Nat.sub_add_eq, Nat.pow_succ, Nat.log_div_base, Nat.zero, Nat.succ, Nat.div_div_eq_div_mul
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
inl : ∀ (hb : b ≤ 1), log b (n / b * b) = log b n
inr : ∀ (hb : 1 < b), log b (n / b * b) = log b n
⊢ log b (n / b * b) = log b n

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 : ℕ
hb : b ≤ 1
inl : 0 = log b n
inl₁ inl₂ : Eq (α := ℕ) 0 0
⊢ log b (n / b * b) = log b n

Tactic:
rw [log_of_left_le_one hb, log_of_left_le_one hb]

Premises used: Nat.log_of_left_le_one
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
inr : ∀ (h : n < b), log b (n / b * b) = log b n
inr₁ : ∀ (h : b ≤ n), log b (n / b * b) = log b n
⊢ log b (n / b * b) = log b n

Tactic:
rcases lt_or_ge n b with h | h

Premises used: lt_or_ge
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
h : n < b
inr : log b (0 * b) = log b n
inr₁ : log b 0 = log b n
inr₂ : 0 = log b n
inr₃ inr₄ : Eq (α := ℕ) 0 0
⊢ log b (n / b * b) = log b n

Tactic:
rw [div_eq_of_lt h, Nat.zero_mul, log_zero_right, log_of_lt h]

Premises used: Nat.log_zero_right, Nat.zero_mul, Nat.log_of_lt, Nat.div_eq_of_lt
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
h : b ≤ n
⊢ 0 < b

Tactic:
lia
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
h : b ≤ n
inr : log b (n / b) + 1 = log b n
inr₁ : log b n - 1 + 1 = log b n
inr₂ inr₃ : log b n = log b n
⊢ log b (n / b * b) = log b n

Tactic:
rw [log_mul_base hb (Nat.div_pos h (by lia)).ne', log_div_base,
    Nat.sub_add_cancel (succ_le_iff.2 <| log_pos hb h)]

Premises used: Iff.mpr, Nat.log_pos, Nat.log_mul_base, LT.lt.ne', Nat.log_div_base, Nat.sub_add_cancel, Nat.succ_le_iff, Nat.div_pos
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ 0 < b

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

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

Tactic:
rw [div_lt_iff_lt_mul (by lia), ← succ_le_iff, ← pred_eq_sub_one,
    succ_pred_eq_of_pos (by lia)]

Premises used: Nat.succ_pred_eq_of_pos, Nat.div_lt_iff_lt_mul, Nat.pred_eq_sub_one, Nat.succ_le_iff
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ n + b ≤ n * b

Tactic:
Nat.add_le_mul hn hb

Premises used: Nat.add_le_mul
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ n + b ≤ n * b

Tactic:
exact Nat.add_le_mul hn hb

Premises used: Nat.add_le_mul
-- Module: Mathlib.Data.Nat.Log
Goal:
b : Bool
n : ℕ
hn : n ≠ 0
rw : log 2 (bit b n / 2 * 2) = log 2 n + 1
rw₁ : log 2 (n * 2) = log 2 n + 1
rw₂ rw₃ : log 2 n + 1 = log 2 n + 1
⊢ log 2 (bit b n) = log 2 n + 1

Tactic:
rw [← log_div_mul_self, bit_div_two, log_mul_base Nat.one_lt_two hn]

Premises used: Nat.one_lt_two, Nat.log_mul_base, Nat.bit_div_two, Nat.log_div_mul_self
-- Module: Mathlib.Data.Nat.Log
Goal:
n : ℕ
inl : log2 0 = log 2 0
inr : ∀ (hn : n ≠ 0), n.log2 = log 2 n
⊢ n.log2 = log 2 n

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Log
Goal:
inl : 0 = log 2 0
inl₁ inl₂ : Eq (α := ℕ) 0 0
⊢ log2 0 = log 2 0

Tactic:
rw [log2_zero, log_zero_right]

Premises used: Nat.log_zero_right, Nat.log2_zero
-- Module: Mathlib.Data.Nat.Log
Goal:
n : ℕ
hn : n ≠ 0
inr : ∀ (c : ℕ), c ≤ n.log2 ↔ c ≤ log 2 n
⊢ n.log2 = log 2 n

Tactic:
apply eq_of_forall_le_iff

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Data.Nat.Log
Goal:
n : ℕ
hn : n ≠ 0
m : ℕ
inr : HPow.hPow (α := ℕ) 2 m ≤ n ↔ m ≤ log 2 n
inr₁ inr₂ : HPow.hPow (α := ℕ) 2 m ≤ n ↔ HPow.hPow (α := ℕ) 2 m ≤ n
⊢ m ≤ n.log2 ↔ m ≤ log 2 n

Tactic:
rw [Nat.le_log2 hn, Nat.le_log_iff_pow_le Nat.one_lt_two hn]

Premises used: Nat.one_lt_two, Nat.le_log_iff_pow_le, Nat.le_log2
-- Module: Mathlib.Data.Nat.Log
Goal:
b k n : ℕ
inl : log (b ^ k) 0 = log b 0 / k
inr : ∀ (hn : n ≠ 0), log (b ^ k) n = log b n / k
⊢ log (b ^ k) n = log b n / k

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Log
Goal:
b k : ℕ
⊢ log (b ^ k) 0 = log b 0 / k

Tactic:
simp
-- Module: Mathlib.Data.Nat.Log
Goal:
b k n : ℕ
hn : n ≠ 0
inr : log (HPow.hPow (β := ℕ) b 0) n = log b n / 0
inr₁ : ∀ (hk : k > 0), log (b ^ k) n = log b n / k
⊢ log (b ^ k) n = log b n / k

Tactic:
rcases k.eq_zero_or_pos with rfl | hk

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hn : n ≠ 0
⊢ log (HPow.hPow (β := ℕ) b 0) n = log b n / 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Log
Goal:
b k n : ℕ
hn : n ≠ 0
hk : k > 0
inr : ∀ (hb : 1 < b), log (b ^ k) n = log b n / k
inr₁ : ∀ (hb : 1 ≥ b), log (b ^ k) n = log b n / k
⊢ log (b ^ k) n = log b n / k

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 k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 < b
⊢ log (b ^ k) n = log b n / k

Tactic:
eq_of_forall_le_iff fun c ↦ ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Data.Nat.Log
Goal:
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 < b
inr : ∀ (c : ℕ), c ≤ log (b ^ k) n ↔ c ≤ log b n / k
⊢ log (b ^ k) n = log b n / k

Tactic:
refine eq_of_forall_le_iff fun c ↦ ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Data.Nat.Log
Goal:
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 < b
c : ℕ
inr : (b ^ k) ^ c ≤ n ↔ c ≤ log b n / k
inr₁ : (b ^ k) ^ c ≤ n ↔ c * k ≤ log b n
inr₂ : (b ^ k) ^ c ≤ n ↔ b ^ (c * k) ≤ n
inr₃ inr₄ : (b ^ k) ^ c ≤ n ↔ (b ^ k) ^ c ≤ n
⊢ c ≤ log (b ^ k) n ↔ c ≤ log b n / k

Tactic:
rw [le_log_iff_pow_le (Nat.one_lt_pow (Nat.ne_of_gt hk) hb) hn, Nat.le_div_iff_mul_le hk,
          le_log_iff_pow_le hb hn, Nat.pow_mul']

Premises used: Nat.one_lt_pow, Nat.le_log_iff_pow_le, Nat.le_div_iff_mul_le, Nat.pow_mul', Nat.ne_of_gt
-- Module: Mathlib.Data.Nat.Log
Goal:
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 ≥ b
inr : b ^ k ≤ 1
⊢ log (b ^ k) n = log b n / k

Tactic:
rw [log_of_left_le_one hb, Nat.zero_div, log_of_left_le_one]

Premises used: Nat.zero_div, Nat.log_of_left_le_one
-- Module: Mathlib.Data.Nat.Log
Goal:
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 ≥ b
inr inr₁ inr₂ inr₃ : b ≤ 1
⊢ b ^ k ≤ 1

Tactic:
rwa [Nat.pow_le_one_iff (Nat.ne_of_gt hk)]

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

Tactic:
grind [clog]

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

Tactic:
grind [clog]

Premises used: Nat.clog
-- Module: Mathlib.Data.Nat.Log
Goal:
n : ℕ
⊢ clog 0 n = 0

Tactic:
clog_of_left_le_one (Nat.zero_le _) _

Premises used: Nat.zero_le, Nat.clog_of_left_le_one
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
⊢ clog b 0 = 0

Tactic:
clog_of_right_le_one (Nat.zero_le _) _

Premises used: Nat.zero_le, Nat.clog_of_right_le_one
-- Module: Mathlib.Data.Nat.Log
Goal:
n : ℕ
⊢ clog 1 n = 0

Tactic:
clog_of_left_le_one le_rfl _

Premises used: le_rfl, Nat.clog_of_left_le_one
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
⊢ clog b 1 = 0

Tactic:
clog_of_right_le_one le_rfl _

Premises used: le_rfl, Nat.clog_of_right_le_one
-- Module: Mathlib.Data.Nat.Log
Goal:
n : ℕ
hn : 1 < n
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)

Tactic:
simp_all
-- 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
⊢ (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 [go]

Premises used: Nat.clog.go
-- 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
⊢ (go n (b * b) fuel).fst = (b * b) ^ ((go n (b * b) fuel).snd + 1) / n

Tactic:
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₃⟩

Premises used: _private.0.Nat.log.go_aux, Nat.le_of_lt
-- 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
⊢ (b * b) ^ (go n (b * b) fuel).snd < n

Tactic:
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₃⟩

Premises used: _private.0.Nat.log.go_aux, Nat.le_of_lt
-- 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
⊢ n ≤ (b * b) ^ ((go n (b * b) fuel).snd + 1)

Tactic:
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₃⟩

Premises used: _private.0.Nat.log.go_aux, Nat.le_of_lt