awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
n : ℕ
hn : n ≠ 0
fuel : ℕ
ih :
  ∀ {b : ℕ} (hb : 1 < b) (hfuel : n < b ^ fuel),
    (go n b fuel).fst = n / b ^ (go n b fuel).snd ∧ b ^ (go n b fuel).snd ≤ n ∧ n < b ^ ((go n b fuel).snd + 1)
b : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hnb : n ≥ b
ih₁ : (go n (HPow.hPow (β := ℕ) b 2) fuel).fst = n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd)
ih₂ : b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd) ≤ n
ih₃ : n < b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 2)
⊢ (if n < b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) then
          (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd), 2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd)
        else
          (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1),
            2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1)).fst =
      n /
        b ^
          (if n < b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) then
              (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd), 2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd)
            else
              (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1),
                2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1)).snd ∧
    b ^
          (if n < b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) then
              (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd), 2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd)
            else
              (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1),
                2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1)).snd ≤
        n ∧
      n <
        b ^
          ((if n < b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) then
                (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd), 2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd)
              else
                (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1),
                  2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1)).snd +
            1)
have succ : n < b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) →
  (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd), 2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd).fst =
      n /
        b ^ (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd), 2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd).snd ∧
    b ^ (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd), 2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd).snd ≤ n ∧
      n <
        b ^
          ((n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd), 2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd).snd +
            1)
Tactic: split
-- Lean 4 proof step from Mathlib.Data.Nat.Log (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
fuel : ℕ
ih :
  ∀ {b : ℕ} (hb : 1 < b) (hfuel : n < b ^ fuel),
    (go n b fuel).fst = n / b ^ (go n b fuel).snd ∧ 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 = n / b ^ (go n b (fuel + 1)).snd ∧
    b ^ (go n b (fuel + 1)).snd ≤ n ∧ n < b ^ ((go n b (fuel + 1)).snd + 1)
have x : n < b ∨ n ≥ b
Tactic: cases Nat.lt_or_ge n b with
    | inl hnb =>
      simp [go, hnb, one_le_iff_ne_zero, hn]
    | inr hnb =>
      rcases ih (Nat.one_mul 1 ▸ Nat.mul_lt_mul_of_lt_of_lt hb hb) (go_aux hb hfuel hnb)
        with ⟨ih₁, ih₂, ih₃⟩
      simp_all only [go, if_neg (Nat.not_lt_of_le hnb), ← Nat.pow_two, ← Nat.pow_mul,
        Nat.div_lt_iff_lt_mul, Nat.pow_pos (Nat.zero_lt_of_lt hb), Nat.div_div_eq_div_mul,
        ← Nat.pow_add_one, ← Nat.pow_add_one', Nat.mul_add_one]
      split <;> simp_all
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n fuel : ℕ
hb : 1 < b
hn : n ≠ 0
hfuel : n < b ^ fuel
⊢ (go n b fuel).fst = n / b ^ (go n b fuel).snd ∧ b ^ (go n b fuel).snd ≤ n ∧ n < b ^ ((go n b fuel).snd + 1)
have zero : ∀ {b : ℕ} (hb : 1 < b) (hfuel : n < HPow.hPow (β := ℕ) b 0),
  (go n b 0).fst = n / b ^ (go n b 0).snd ∧ b ^ (go n b 0).snd ≤ n ∧ n < b ^ ((go n b 0).snd + 1)
Tactic: induction fuel generalizing b with
  | zero => simp_all
  | succ fuel ih =>
    cases Nat.lt_or_ge n b with
    | inl hnb =>
      simp [go, hnb, one_le_iff_ne_zero, hn]
    | inr hnb =>
      rcases ih (Nat.one_mul 1 ▸ Nat.mul_lt_mul_of_lt_of_lt hb hb) (go_aux hb hfuel hnb)
        with ⟨ih₁, ih₂, ih₃⟩
      simp_all only [go, if_neg (Nat.not_lt_of_le hnb), ← Nat.pow_two, ← Nat.pow_mul,
        Nat.div_lt_iff_lt_mul, Nat.pow_pos (Nat.zero_lt_of_lt hb), Nat.div_div_eq_div_mul,
        ← Nat.pow_add_one, ← Nat.pow_add_one', Nat.mul_add_one]
      split <;> simp_all
Cleared hypotheses: b, fuel, hb, hfuel
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n fuel : ℕ
hb : 1 < b
hn : n ≠ 0
hfuel : n < b ^ fuel
zero :
  ∀ {b : ℕ} (hb : 1 < b) (hfuel : n < HPow.hPow (β := ℕ) b 0),
    (go n b 0).fst = n / b ^ (go n b 0).snd ∧ b ^ (go n b 0).snd ≤ n ∧ n < b ^ ((go n b 0).snd + 1)
⊢ (go n b fuel).fst = n / b ^ (go n b fuel).snd ∧ b ^ (go n b fuel).snd ≤ n ∧ n < b ^ ((go n b fuel).snd + 1)
have succ : ∀ (fuel : ℕ)
  (ih :
    ∀ {b : ℕ} (hb : 1 < b) (hfuel : n < b ^ fuel),
      (go n b fuel).fst = n / b ^ (go n b fuel).snd ∧ 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 = n / b ^ (go n b (fuel + 1)).snd ∧
    b ^ (go n b (fuel + 1)).snd ≤ n ∧ n < b ^ ((go n b (fuel + 1)).snd + 1)
Tactic: induction fuel generalizing b with
  | zero => simp_all
  | succ fuel ih =>
    cases Nat.lt_or_ge n b with
    | inl hnb =>
      simp [go, hnb, one_le_iff_ne_zero, hn]
    | inr hnb =>
      rcases ih (Nat.one_mul 1 ▸ Nat.mul_lt_mul_of_lt_of_lt hb hb) (go_aux hb hfuel hnb)
        with ⟨ih₁, ih₂, ih₃⟩
      simp_all only [go, if_neg (Nat.not_lt_of_le hnb), ← Nat.pow_two, ← Nat.pow_mul,
        Nat.div_lt_iff_lt_mul, Nat.pow_pos (Nat.zero_lt_of_lt hb), Nat.div_div_eq_div_mul,
        ← Nat.pow_add_one, ← Nat.pow_add_one', Nat.mul_add_one]
      split <;> simp_all
Cleared hypotheses: b, fuel, hb, hfuel
-- Lean 4 proof step from Mathlib.Data.Nat.Log (hypothesis)
Goal:
b : ℕ
hb : 1 < b
x y : ℕ
hy : y ≠ 0
⊢ log b y < x ↔ y < b ^ x
have H₁ : b ^ (log.go y b y).snd ≤ y
Tactic: rcases log.go_spec hb hy (Nat.lt_pow_self hb) with ⟨-, H₁, H₂⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Log (hypothesis)
Goal:
b : ℕ
hb : 1 < b
x y : ℕ
hy : y ≠ 0
H₁ : b ^ (log.go y b y).snd ≤ y
⊢ log b y < x ↔ y < b ^ x
have H₂ : y < b ^ ((log.go y b y).snd + 1)
Tactic: rcases log.go_spec hb hy (Nat.lt_pow_self hb) with ⟨-, H₁, H₂⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b : ℕ
hb : 1 < b
x y : ℕ
hy : y ≠ 0
H₁ : b ^ (log.go y b y).snd ≤ y
H₂ : y < b ^ ((log.go y b y).snd + 1)
⊢ log b y < x ↔ y < b ^ x
have rw : (log.go y b y).snd < x ↔ y < b ^ x
Tactic: rw [log, if_neg (Nat.not_le_of_lt hb)]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b : ℕ
hb : 1 < b
x y : ℕ
hy : y ≠ 0
H₁ : b ^ (log.go y b y).snd ≤ y
H₂ : y < b ^ ((log.go y b y).snd + 1)
h : (log.go y b y).snd ≥ x
⊢ (log.go y b y).snd < x ↔ y < b ^ x
have inr : b ^ x ≤ b ^ (log.go y b y).snd
Tactic: refine iff_of_false (Nat.not_lt_of_ge h) <| Nat.not_lt_of_ge <| Nat.le_trans ?_ H₁
-- Lean 4 proof step from Mathlib.Data.Nat.Log (hypothesis)
Goal:
b : ℕ
hb : 1 < b
x y : ℕ
hy : y ≠ 0
H₁ : b ^ (log.go y b y).snd ≤ y
H₂ : y < b ^ ((log.go y b y).snd + 1)
⊢ (log.go y b y).snd < x ↔ y < b ^ x
have x₁ : (log.go y b y).snd < x ∨ (log.go y b y).snd ≥ x
Tactic: cases Nat.lt_or_ge (log.go y b y).snd x with
  | inl h =>
    exact iff_of_true h <| Nat.lt_of_lt_of_le H₂ <| Nat.pow_le_pow_right (Nat.zero_lt_of_lt hb) h
  | inr h =>
    refine iff_of_false (Nat.not_lt_of_ge h) <| Nat.not_lt_of_ge <| Nat.le_trans ?_ H₁
    exact Nat.pow_le_pow_right (Nat.zero_lt_of_lt hb) h
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
⊢ log b n = 0 ↔ n < b ∨ b ≤ 1
have inl : ∀ (hb : 1 < b), log b n = 0 ↔ n < b ∨ b ≤ 1
Tactic: rcases Nat.lt_or_ge 1 b with hb | hb
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
inl : ∀ (hb : 1 < b), log b n = 0 ↔ n < b ∨ b ≤ 1
⊢ log b n = 0 ↔ n < b ∨ b ≤ 1
have inr : ∀ (hb : 1 ≥ b), log b n = 0 ↔ n < b ∨ b ≤ 1
Tactic: rcases Nat.lt_or_ge 1 b with hb | hb
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
⊢ log b n = 0 ↔ n < b ∨ b ≤ 1
have inl : log b 0 = 0 ↔ 0 < b ∨ b ≤ 1
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
inl : log b 0 = 0 ↔ 0 < b ∨ b ≤ 1
⊢ log b n = 0 ↔ n < b ∨ b ≤ 1
have inl₁ : ∀ (hn : n ≠ 0), log b n = 0 ↔ n < b ∨ b ≤ 1
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b n = 0 ↔ n < b ∨ b ≤ 1
have inl : log b n < 1 ↔ n < b ∨ b ≤ 1
Tactic: rw [← Nat.lt_one_iff, log_lt_iff_lt_pow hb hn, Nat.pow_one, or_iff_left (Nat.not_le_of_lt hb)]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
inl : log b n < 1 ↔ n < b ∨ b ≤ 1
⊢ log b n = 0 ↔ n < b ∨ b ≤ 1
have inl₁ : n < HPow.hPow (β := ℕ) b 1 ↔ n < b ∨ b ≤ 1
Tactic: rw [← Nat.lt_one_iff, log_lt_iff_lt_pow hb hn, Nat.pow_one, or_iff_left (Nat.not_le_of_lt hb)]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
inl : log b n < 1 ↔ n < b ∨ b ≤ 1
inl₁ : n < HPow.hPow (β := ℕ) b 1 ↔ n < b ∨ b ≤ 1
⊢ log b n = 0 ↔ n < b ∨ b ≤ 1
have inl₂ : n < b ↔ n < b ∨ b ≤ 1
Tactic: rw [← Nat.lt_one_iff, log_lt_iff_lt_pow hb hn, Nat.pow_one, or_iff_left (Nat.not_le_of_lt hb)]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
inl : log b n < 1 ↔ n < b ∨ b ≤ 1
inl₁ : n < HPow.hPow (β := ℕ) b 1 ↔ n < b ∨ b ≤ 1
inl₂ : n < b ↔ n < b ∨ b ≤ 1
⊢ log b n = 0 ↔ n < b ∨ b ≤ 1
have inl₃ : n < b ↔ n < b
Tactic: rw [← Nat.lt_one_iff, log_lt_iff_lt_pow hb hn, Nat.pow_one, or_iff_left (Nat.not_le_of_lt hb)]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
⊢ 0 < log b n ↔ b ≤ n ∧ 1 < b
have rw : log b n ≠ 0 ↔ b ≤ n ∧ 1 < b
Tactic: rw [Nat.pos_iff_ne_zero, Ne, log_eq_zero_iff, not_or, not_lt, not_le]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
rw : log b n ≠ 0 ↔ b ≤ n ∧ 1 < b
⊢ 0 < log b n ↔ b ≤ n ∧ 1 < b
have rw₁ : ¬log b n = 0 ↔ b ≤ n ∧ 1 < b
Tactic: rw [Nat.pos_iff_ne_zero, Ne, log_eq_zero_iff, not_or, not_lt, not_le]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
rw : log b n ≠ 0 ↔ b ≤ n ∧ 1 < b
rw₁ : ¬log b n = 0 ↔ b ≤ n ∧ 1 < b
⊢ 0 < log b n ↔ b ≤ n ∧ 1 < b
have rw₂ : ¬(n < b ∨ b ≤ 1) ↔ b ≤ n ∧ 1 < b
Tactic: rw [Nat.pos_iff_ne_zero, Ne, log_eq_zero_iff, not_or, not_lt, not_le]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
rw : log b n ≠ 0 ↔ b ≤ n ∧ 1 < b
rw₁ : ¬log b n = 0 ↔ b ≤ n ∧ 1 < b
rw₂ : ¬(n < b ∨ b ≤ 1) ↔ b ≤ n ∧ 1 < b
⊢ 0 < log b n ↔ b ≤ n ∧ 1 < b
have rw₃ : ¬n < b ∧ ¬b ≤ 1 ↔ b ≤ n ∧ 1 < b
Tactic: rw [Nat.pos_iff_ne_zero, Ne, log_eq_zero_iff, not_or, not_lt, not_le]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
rw : log b n ≠ 0 ↔ b ≤ n ∧ 1 < b
rw₁ : ¬log b n = 0 ↔ b ≤ n ∧ 1 < b
rw₂ : ¬(n < b ∨ b ≤ 1) ↔ b ≤ n ∧ 1 < b
rw₃ : ¬n < b ∧ ¬b ≤ 1 ↔ b ≤ n ∧ 1 < b
⊢ 0 < log b n ↔ b ≤ n ∧ 1 < b
have rw₄ : b ≤ n ∧ ¬b ≤ 1 ↔ b ≤ n ∧ 1 < b
Tactic: rw [Nat.pos_iff_ne_zero, Ne, log_eq_zero_iff, not_or, not_lt, not_le]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
rw : log b n ≠ 0 ↔ b ≤ n ∧ 1 < b
rw₁ : ¬log b n = 0 ↔ b ≤ n ∧ 1 < b
rw₂ : ¬(n < b ∨ b ≤ 1) ↔ b ≤ n ∧ 1 < b
rw₃ : ¬n < b ∧ ¬b ≤ 1 ↔ b ≤ n ∧ 1 < b
rw₄ : b ≤ n ∧ ¬b ≤ 1 ↔ b ≤ n ∧ 1 < b
⊢ 0 < log b n ↔ b ≤ n ∧ 1 < b
have rw₅ : b ≤ n ∧ 1 < b ↔ b ≤ n ∧ 1 < b
Tactic: rw [Nat.pos_iff_ne_zero, Ne, log_eq_zero_iff, not_or, not_lt, not_le]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
h : 1 < b
hn : b ≤ n
⊢ log b n = log b (n / b) + 1
have h₁ : ∀ (c : ℕ), log b n < c ↔ log b (n / b) + 1 < c
Tactic: apply eq_of_forall_gt_iff
-- Lean 4 proof step from Mathlib.Data.Nat.Log (hypothesis)
Goal:
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
⊢ log b n < c + 1 ↔ log b (n / b) + 1 < c + 1
have this : n / b ≠ 0
Tactic: have : n / b ≠ 0 := by simp [*, Nat.ne_zero_of_lt h]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ log b n < c + 1 ↔ log b (n / b) + 1 < c + 1
have h₁ : 0 < b
Tactic: rw [log_lt_iff_lt_pow, Nat.add_lt_add_iff_right, log_lt_iff_lt_pow,
      Nat.pow_add_one, Nat.div_lt_iff_lt_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
h₁ : 0 < b
h₂ : 1 < b
h₃ : n / b ≠ 0
h₄ : 1 < b
⊢ log b n < c + 1 ↔ log b (n / b) + 1 < c + 1
have h₅ : n ≠ 0
Tactic: rw [log_lt_iff_lt_pow, Nat.add_lt_add_iff_right, log_lt_iff_lt_pow,
      Nat.pow_add_one, Nat.div_lt_iff_lt_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (hypothesis)
Goal:
b x y : ℕ
hy : y ≠ 0
h : x ≤ log b y
⊢ b ^ x ≤ y
have hb : b ≤ 1
Tactic: refine (le_or_gt b 1).elim (fun hb => ?_) fun hb => (le_log_iff_pow_le hb hy).1 h
-- Lean 4 proof step from Mathlib.Data.Nat.Log (hypothesis)
Goal:
b x y : ℕ
hy : y ≠ 0
h : x ≤ log b y
hb : b ≤ 1
⊢ b ^ x ≤ y
have h₁ : x = 0
Tactic: rw [log_of_left_le_one hb, Nat.le_zero] at h
Cleared hypotheses: h, hb
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b x y : ℕ
hy : y ≠ 0
h : x = 0
hb : b ≤ 1
⊢ b ^ x ≤ y
have rwa : HPow.hPow (β := ℕ) b 0 ≤ y
Tactic: rwa [h, Nat.pow_zero, one_le_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b x y : ℕ
hy : y ≠ 0
h : x = 0
hb : b ≤ 1
rwa : HPow.hPow (β := ℕ) b 0 ≤ y
⊢ b ^ x ≤ y
have rwa₁ : 1 ≤ y
Tactic: rwa [h, Nat.pow_zero, one_le_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b x y : ℕ
hb : 1 < b
h : b ^ x ≤ y
⊢ x ≤ log b y
have inl : ∀ (hy : y ≠ 0), x ≤ log b y
Tactic: rcases ne_or_eq y 0 with (hy | rfl)
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b x y : ℕ
hb : 1 < b
h : b ^ x ≤ y
inl : ∀ (hy : y ≠ 0), x ≤ log b y
⊢ x ≤ log b y
have inr : ∀ (h : b ^ x ≤ 0), x ≤ log b 0
Tactic: rcases ne_or_eq y 0 with (hy | rfl)
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b x y : ℕ
hx : x ≠ 0
hlt : y < b ^ x
⊢ log b y < x
have inl : ∀ (hlt : 0 < b ^ x), log b 0 < x
Tactic: rcases eq_or_ne y 0 with rfl | hy
Cleared hypotheses: y, hlt
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b x y : ℕ
hx : x ≠ 0
hlt : y < b ^ x
inl : ∀ (hlt : 0 < b ^ x), log b 0 < x
⊢ log b y < x
have inr : ∀ (hy : y ≠ 0), log b y < x
Tactic: rcases eq_or_ne y 0 with rfl | hy
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
have inl : ∀ (hb : 1 < b) (hn : n ≠ 0), log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
Tactic: rcases em (1 < b ∧ n ≠ 0) with (⟨hb, hn⟩ | hbn)
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
inl : ∀ (hb : 1 < b) (hn : n ≠ 0), log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
have inr : ∀ (hbn : ¬(1 < b ∧ n ≠ 0)), log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
Tactic: rcases em (1 < b ∧ n ≠ 0) with (⟨hb, hn⟩ | hbn)
-- Lean 4 proof step from Mathlib.Data.Nat.Log (hypothesis)
Goal:
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hbn : ¬(1 < b ∧ n ≠ 0)
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
have hm : m ≠ 0
Tactic: have hm : m ≠ 0 := h.resolve_right hbn
-- Lean 4 proof step from Mathlib.Data.Nat.Log (hypothesis)
Goal:
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hbn : ¬(1 < b ∧ n ≠ 0)
hm : m ≠ 0
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
have hbn₁ : b ≤ 1 ∨ n = 0
Tactic: rw [not_and_or, not_lt, Ne, not_not] at hbn
Cleared hypotheses: hbn, hm
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hbn : b ≤ 1 ∨ n = 0
hm : m ≠ 0
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
have inr : ∀ (hb : b ≤ 1), log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
Tactic: rcases hbn with (hb | rfl)
Cleared hypotheses: hbn
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hbn : b ≤ 1 ∨ n = 0
hm : m ≠ 0
inr : ∀ (hb : b ≤ 1), log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
have inr₁ : ∀ (h : m ≠ 0 ∨ 1 < b ∧ Ne (α := ℕ) 0 0), log b 0 = m ↔ b ^ m ≤ 0 ∧ 0 < b ^ (m + 1)
Tactic: rcases hbn with (hb | rfl)
Cleared hypotheses: n, h, hbn
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hm : m ≠ 0
hb : b ≤ 1
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
have 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)
Tactic: obtain rfl | rfl := le_one_iff_eq_zero_or_eq_one.1 hb
Cleared hypotheses: b, h, hb
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
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)
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
have 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)
Tactic: obtain rfl | rfl := le_one_iff_eq_zero_or_eq_one.1 hb
Cleared hypotheses: b, h, hb
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b m n : ℕ
h₁ : b ^ m ≤ n
h₂ : n < b ^ (m + 1)
⊢ log b n = m
have inl : ∀ (h₁ : HPow.hPow (β := ℕ) b 0 ≤ n) (h₂ : n < b ^ HAdd.hAdd (α := ℕ) 0 1), log b n = 0
Tactic: rcases eq_or_ne m 0 with (rfl | hm)
Cleared hypotheses: m, h₁, h₂
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
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
⊢ log b n = m
have inr : ∀ (hm : m ≠ 0), log b n = m
Tactic: rcases eq_or_ne m 0 with (rfl | hm)
-- Lean 4 proof step from Mathlib.Data.Nat.Log (hypothesis)
Goal:
b n : ℕ
h₁ : HPow.hPow (β := ℕ) b 0 ≤ n
h₂ : n < b ^ HAdd.hAdd (α := ℕ) 0 1
⊢ log b n = 0
have h₃ : n < b
Tactic: rw [Nat.pow_one] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
⊢ log b n = 1 ↔ b ≤ n ∧ n < b * b
have rw : HPow.hPow (β := ℕ) b 1 ≤ n ∧ n < b ^ HAdd.hAdd (α := ℕ) 1 1 ↔ b ≤ n ∧ n < b * b
Tactic: rw [log_eq_iff (Or.inl Nat.one_ne_zero), Nat.pow_add, Nat.pow_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
rw : HPow.hPow (β := ℕ) b 1 ≤ n ∧ n < b ^ HAdd.hAdd (α := ℕ) 1 1 ↔ b ≤ n ∧ n < b * b
⊢ log b n = 1 ↔ b ≤ n ∧ n < b * b
have rw₁ : HPow.hPow (β := ℕ) b 1 ≤ n ∧ n < HPow.hPow (β := ℕ) b 1 * HPow.hPow (β := ℕ) b 1 ↔ b ≤ n ∧ n < b * b
Tactic: rw [log_eq_iff (Or.inl Nat.one_ne_zero), Nat.pow_add, Nat.pow_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
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
⊢ log b n = 1 ↔ b ≤ n ∧ n < b * b
have rw₂ : b ≤ n ∧ n < b * b ↔ b ≤ n ∧ n < b * b
Tactic: rw [log_eq_iff (Or.inl Nat.one_ne_zero), Nat.pow_add, Nat.pow_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b (n * b) = log b n + 1
have h₁ : b ^ (log b n + 1) ≤ n * b
Tactic: apply log_eq_of_pow_le_of_lt_pow
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
h₁ : b ^ (log b n + 1) ≤ n * b
⊢ log b (n * b) = log b n + 1
have h₂ : n * b < b ^ (log b n + 1 + 1)
Tactic: apply log_eq_of_pow_le_of_lt_pow
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ b ^ (log b n + 1) ≤ n * b
have h₁ : b ^ log b n * b ≤ n * b
Tactic: rw [pow_succ', Nat.mul_comm b]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ n * b < b ^ (log b n + 1 + 1)
have h₂ : n * b < b ^ (log b n + 1) * b
Tactic: rw [pow_succ', Nat.mul_comm b]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b : ℕ
⊢ b ^ log b 0 ≤ HAdd.hAdd (α := ℕ) 0 1
have rw : HPow.hPow (β := ℕ) b 0 ≤ HAdd.hAdd (α := ℕ) 0 1
Tactic: rw [log_zero_right, Nat.pow_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b : ℕ
rw : HPow.hPow (β := ℕ) b 0 ≤ HAdd.hAdd (α := ℕ) 0 1
⊢ b ^ log b 0 ≤ HAdd.hAdd (α := ℕ) 0 1
have rw₁ : LE.le (α := ℕ) 1 1
Tactic: rw [log_zero_right, Nat.pow_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b : ℕ
⊢ Monotone (log b)
have refine : ∀ (n : ℕ), log b n ≤ log b (n + 1)
Tactic: refine monotone_nat_of_le_succ fun n => ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
⊢ log b n ≤ log b (n + 1)
have inl : ∀ (hb : b ≤ 1), log b n ≤ log b (n + 1)
Tactic: rcases le_or_gt b 1 with hb | hb
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
inl : ∀ (hb : b ≤ 1), log b n ≤ log b (n + 1)
⊢ log b n ≤ log b (n + 1)
have inr : ∀ (hb : 1 < b), log b n ≤ log b (n + 1)
Tactic: rcases le_or_gt b 1 with hb | hb
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : b ≤ 1
⊢ log b n ≤ log b (n + 1)
have inl : 0 ≤ log b (n + 1)
Tactic: rw [log_of_left_le_one hb]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b n < log b (n + 1) ↔ b ^ log b (n + 1) = n + 1
have refine_1 : ∀ (H : log b n < log b (n + 1)), b ^ log b (n + 1) = n + 1
Tactic: refine ⟨fun H ↦ ?_, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
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
⊢ log b n < log b (n + 1) ↔ b ^ log b (n + 1) = n + 1
have refine_2 : ∀ (H : b ^ log b (n + 1) = n + 1), log b n < log b (n + 1)
Tactic: refine ⟨fun H ↦ ?_, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
H : log b n < log b (n + 1)
⊢ b ^ log b (n + 1) = n + 1
have apply : b ^ log b (n + 1) ≤ n + 1
Tactic: apply le_antisymm _ (Nat.lt_pow_of_log_lt hb H)
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
H : b ^ log b (n + 1) = n + 1
⊢ log b n < log b (n + 1)
have refine_2 : n < b ^ log b (n + 1)
Tactic: apply Nat.log_lt_of_lt_pow hn
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b n = log b (n + 1) ↔ b ^ log b (n + 1) ≠ n + 1
have rw : log b n = log b (n + 1) ↔ log b (n + 1) ≤ log b n
Tactic: rw [ne_eq, ← log_lt_log_succ_iff hb hn, not_lt]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b n = log b (n + 1) ↔ log b (n + 1) ≤ log b n
have simp : log b (n + 1) ≤ log b n → log b n ≤ log b (n + 1)
Tactic: simp only [le_antisymm_iff, and_iff_right_iff_imp]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b c n : ℕ
hc : 1 < c
hb : c ≤ b
⊢ log b n ≤ log c n
have inl : log b 0 ≤ log c 0
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b c n : ℕ
hc : 1 < c
hb : c ≤ b
inl : log b 0 ≤ log c 0
⊢ log b n ≤ log c n
have inr : ∀ (hn : n ≠ 0), log b n ≤ log c n
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b c : ℕ
hc : 1 < c
hb : c ≤ b
⊢ log b 0 ≤ log c 0
have inl : 0 ≤ log c 0
Tactic: rw [log_zero_right, log_zero_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b c : ℕ
hc : 1 < c
hb : c ≤ b
inl : 0 ≤ log c 0
⊢ log b 0 ≤ log c 0
have inl₁ : LE.le (α := ℕ) 0 0
Tactic: rw [log_zero_right, log_zero_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b c n : ℕ
hc : 1 < c
hb : c ≤ b
hn : n ≠ 0
⊢ log b n ≤ log c n
have inr : c ^ log b n ≤ n
Tactic: apply le_log_of_pow_le hc
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
⊢ log b (n / b) = log b n - 1
have inl : ∀ (hb : b ≤ 1), log b (n / b) = log b n - 1
Tactic: rcases le_or_gt b 1 with hb | hb
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
inl : ∀ (hb : b ≤ 1), log b (n / b) = log b n - 1
⊢ log b (n / b) = log b n - 1
have inr : ∀ (hb : 1 < b), log b (n / b) = log b n - 1
Tactic: rcases le_or_gt b 1 with hb | hb