awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Log
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
⊢ (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:
simp [go, hnb, one_le_iff_ne_zero, hn]

Premises used: Nat.one_le_iff_ne_zero, Nat.log.go
-- Module: Mathlib.Data.Nat.Log
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
⊢ (go n (b * b) fuel).fst = n / (b * b) ^ (go n (b * b) fuel).snd

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

Premises used: _private.0.Nat.log.go_aux
-- Module: Mathlib.Data.Nat.Log
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 (b * b) fuel).fst = n / (b * b) ^ (go n (b * b) fuel).snd
⊢ (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) (go_aux hb hfuel hnb)
        with ⟨ih₁, ih₂, ih₃⟩

Premises used: _private.0.Nat.log.go_aux
-- Module: Mathlib.Data.Nat.Log
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 (b * b) fuel).fst = n / (b * b) ^ (go n (b * b) fuel).snd
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) (go_aux hb hfuel hnb)
        with ⟨ih₁, ih₂, ih₃⟩

Premises used: _private.0.Nat.log.go_aux
-- Module: Mathlib.Data.Nat.Log
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 (b * b) fuel).fst = n / (b * b) ^ (go n (b * b) fuel).snd
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 = 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)
⊢ (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:
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]

Premises used: Nat.pow_mul, Nat.not_lt_of_le, Nat.pow_add_one, Nat.zero_lt_of_lt, Nat.pow_two, Nat.div_lt_iff_lt_mul, Nat.mul_add_one, Nat.pow_pos, Nat.pow_add_one', if_neg, Nat.div_div_eq_div_mul, Nat.log.go
-- Module: Mathlib.Data.Nat.Log
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)
h : 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:
simp_all
-- Module: Mathlib.Data.Nat.Log
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)
h : ¬n < b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1)
⊢ (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 ^
          (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1),
              2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1).snd ∧
    b ^
          (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 ^
          ((n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1),
                2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1).snd +
            1)

Tactic:
simp_all
-- Module: Mathlib.Data.Nat.Log
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)
⊢ 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

Premises used: Nat.pow_mul, Nat.pow_add_one, Nat.zero_lt_of_lt, Nat.pow_two, Nat.div_lt_iff_lt_mul, Nat.mul_add_one, Nat.lt_or_ge, Nat.one_le_iff_ne_zero, Nat.pow_pos, Nat.pow_add_one', Nat.div_div_eq_div_mul, Nat.log.go
-- Module: Mathlib.Data.Nat.Log
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)
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)
⊢ (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)

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

Premises used: Nat.pow_mul, Nat.pow_add_one, Nat.zero_lt_of_lt, Nat.pow_two, Nat.div_lt_iff_lt_mul, Nat.mul_add_one, Nat.lt_or_ge, Nat.zero, Nat.one_le_iff_ne_zero, Nat.pow_pos, Nat.pow_add_one', Nat.succ, Nat.div_div_eq_div_mul, Nat.log.go
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
hb : 1 < b
x y : ℕ
hy : y ≠ 0
⊢ b ^ (log.go y b y).snd ≤ y

Tactic:
rcases log.go_spec hb hy (Nat.lt_pow_self hb) with ⟨-, H₁, H₂⟩

Premises used: Nat.lt_pow_self, Nat.log.go_spec
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
hb : 1 < b
x y : ℕ
hy : y ≠ 0
H₁ : b ^ (log.go y b y).snd ≤ y
⊢ y < b ^ ((log.go y b y).snd + 1)

Tactic:
rcases log.go_spec hb hy (Nat.lt_pow_self hb) with ⟨-, H₁, H₂⟩

Premises used: Nat.lt_pow_self, Nat.log.go_spec
-- Module: Mathlib.Data.Nat.Log
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)
rw : (log.go y b y).snd < x ↔ y < b ^ x
⊢ log b y < x ↔ y < b ^ x

Tactic:
rw [log, if_neg (Nat.not_le_of_lt hb)]

Premises used: Nat.not_le_of_lt, Nat.log, if_neg
-- Module: Mathlib.Data.Nat.Log
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

Tactic:
iff_of_true h <| Nat.lt_of_lt_of_le H₂ <| Nat.pow_le_pow_right (Nat.zero_lt_of_lt hb) h

Premises used: Nat.zero_lt_of_lt, Nat.pow_le_pow_right, iff_of_true, Nat.lt_of_lt_of_le
-- Module: Mathlib.Data.Nat.Log
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

Tactic:
exact iff_of_true h <| Nat.lt_of_lt_of_le H₂ <| Nat.pow_le_pow_right (Nat.zero_lt_of_lt hb) h

Premises used: Nat.zero_lt_of_lt, Nat.pow_le_pow_right, iff_of_true, Nat.lt_of_lt_of_le
-- Module: Mathlib.Data.Nat.Log
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

Tactic:
iff_of_false (Nat.not_lt_of_ge h) <| Nat.not_lt_of_ge <| Nat.le_trans ?_ H₁

Premises used: iff_of_false, Nat.le_trans, Nat.not_lt_of_ge
-- Module: Mathlib.Data.Nat.Log
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
inr : b ^ x ≤ b ^ (log.go y b y).snd
⊢ (log.go y b y).snd < x ↔ y < b ^ x

Tactic:
refine iff_of_false (Nat.not_lt_of_ge h) <| Nat.not_lt_of_ge <| Nat.le_trans ?_ H₁

Premises used: iff_of_false, Nat.le_trans, Nat.not_lt_of_ge
-- Module: Mathlib.Data.Nat.Log
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
⊢ b ^ x ≤ b ^ (log.go y b y).snd

Tactic:
Nat.pow_le_pow_right (Nat.zero_lt_of_lt hb) h

Premises used: Nat.zero_lt_of_lt, Nat.pow_le_pow_right
-- Module: Mathlib.Data.Nat.Log
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
⊢ b ^ x ≤ b ^ (log.go y b y).snd

Tactic:
exact Nat.pow_le_pow_right (Nat.zero_lt_of_lt hb) h

Premises used: Nat.zero_lt_of_lt, Nat.pow_le_pow_right
-- Module: Mathlib.Data.Nat.Log
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 ∨ (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

Premises used: Nat.le_trans, Nat.lt_or_ge, Nat.not_lt_of_ge, Prod.snd, Nat.lt_of_lt_of_le, Nat.log.go
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
inl : ∀ (hb : 1 < b), log b n = 0 ↔ n < b ∨ b ≤ 1
inr : ∀ (hb : 1 ≥ b), log b n = 0 ↔ n < b ∨ b ≤ 1
⊢ log b n = 0 ↔ n < b ∨ b ≤ 1

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 n : ℕ
hb : 1 < b
inl : log b 0 = 0 ↔ 0 < b ∨ b ≤ 1
inl₁ : ∀ (hn : n ≠ 0), log b n = 0 ↔ n < b ∨ b ≤ 1
⊢ log b n = 0 ↔ n < b ∨ b ≤ 1

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 : ℕ
hb : 1 < b
⊢ log b 0 = 0 ↔ 0 < b ∨ b ≤ 1

Tactic:
grind [log_of_lt]

Premises used: Nat.log_of_lt
-- Module: Mathlib.Data.Nat.Log
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
inl₃ inl₄ : n < b ↔ n < b
⊢ log b n = 0 ↔ 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)]

Premises used: Nat.log_lt_iff_lt_pow, Nat.not_le_of_lt, Nat.lt_one_iff, Nat.pow_one, or_iff_left
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 ≥ b
⊢ log b n = 0 ↔ n < b ∨ b ≤ 1

Tactic:
simp [hb, log_of_left_le_one]

Premises used: Nat.log_of_left_le_one
-- Module: Mathlib.Data.Nat.Log
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
rw₅ rw₆ : b ≤ n ∧ 1 < b ↔ b ≤ n ∧ 1 < b
⊢ 0 < log b n ↔ b ≤ n ∧ 1 < b

Tactic:
rw [Nat.pos_iff_ne_zero, Ne, log_eq_zero_iff, not_or, not_lt, not_le]

Premises used: not_le, Nat.pos_iff_ne_zero, Nat.log_eq_zero_iff, Ne, not_or, not_lt
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
hbn : b ≤ n
⊢ 0 < log b n

Tactic:
log_pos_iff.2 ⟨hbn, hb⟩

Premises used: Iff.mpr, And.intro, Nat.log_pos_iff
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
h : 1 < b
hn : b ≤ n
h₁ : ∀ (c : ℕ), log b n < c ↔ log b (n / b) + 1 < c
⊢ log b n = log b (n / b) + 1

Tactic:
apply eq_of_forall_gt_iff

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

Tactic:
simp
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
⊢ n / b ≠ 0

Tactic:
simp [*, Nat.ne_zero_of_lt h]

Premises used: Nat.ne_zero_of_lt
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
⊢ n / b ≠ 0

Tactic:
have : n / b ≠ 0 := by simp [*, Nat.ne_zero_of_lt h]
-- Module: Mathlib.Data.Nat.Log
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
h₅ : n ≠ 0
⊢ log b n < c + 1 ↔ log b (n / b) + 1 < c + 1

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]

Premises used: Nat.log_lt_iff_lt_pow, Nat.pow_add_one, Nat.div_lt_iff_lt_mul, Nat.add_lt_add_iff_right
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ 0 < b

Tactic:
grind
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ 1 < b

Tactic:
grind
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ n / b ≠ 0

Tactic:
grind
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ n ≠ 0

Tactic:
grind
-- Module: Mathlib.Data.Nat.Log
Goal:
⊢ ∀ (n : ℕ), log 0 n = 0

Tactic:
log_of_left_le_one <| Nat.zero_le _

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

Tactic:
log_eq_zero_iff.2 (le_total 1 b)

Premises used: Iff.mpr, Nat.log_eq_zero_iff, le_total, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Log
Goal:
⊢ ∀ (n : ℕ), log 1 n = 0

Tactic:
log_of_left_le_one le_rfl

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

Tactic:
log_eq_zero_iff.2 (lt_or_ge _ _)

Premises used: Iff.mpr, Nat.log_eq_zero_iff, lt_or_ge
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
hb : 1 < b
x y : ℕ
hy : y ≠ 0
⊢ x ≤ log b y ↔ b ^ x ≤ y

Tactic:
le_iff_le_iff_lt_iff_lt.mpr <| log_lt_iff_lt_pow hb hy

Premises used: Iff.mpr, Nat.log_lt_iff_lt_pow, le_iff_le_iff_lt_iff_lt
-- Module: Mathlib.Data.Nat.Log
Goal:
b x y : ℕ
hy : y ≠ 0
h : x ≤ log b y
⊢ b ^ x ≤ y

Tactic:
(le_or_gt b 1).elim (fun hb => ?_) fun hb => (le_log_iff_pow_le hb hy).1 h

Premises used: le_or_gt, Nat.le_log_iff_pow_le, Iff.mp, Or.elim, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Log
Goal:
b x y : ℕ
hy : y ≠ 0
h : x ≤ log b y
⊢ b ≤ 1

Tactic:
refine (le_or_gt b 1).elim (fun hb => ?_) fun hb => (le_log_iff_pow_le hb hy).1 h

Premises used: le_or_gt, Nat.le_log_iff_pow_le, Iff.mp, Or.elim, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Log
Goal:
b x y : ℕ
hy : y ≠ 0
h : x ≤ log b y
hb : b ≤ 1
⊢ x = 0

Tactic:
rw [log_of_left_le_one hb, Nat.le_zero] at h

Premises used: Nat.le_zero, Nat.log_of_left_le_one
-- Module: Mathlib.Data.Nat.Log
Goal:
b x y : ℕ
hy : y ≠ 0
h : x ≤ log b y
hb : b ≤ 1
h₁ : x = 0
⊢ b ≤ 1

Tactic:
rw [log_of_left_le_one hb, Nat.le_zero] at h

Premises used: Nat.le_zero, Nat.log_of_left_le_one
-- Module: Mathlib.Data.Nat.Log
Goal:
b x y : ℕ
hy : y ≠ 0
h : x = 0
hb : b ≤ 1
rwa : HPow.hPow (β := ℕ) b 0 ≤ y
rwa₁ : 1 ≤ y
rwa₂ rwa₃ rwa₄ rwa₅ : y ≠ 0
⊢ b ^ x ≤ y

Tactic:
rwa [h, Nat.pow_zero, one_le_iff_ne_zero]

Premises used: Nat.pow_zero, Nat.one_le_iff_ne_zero
-- Module: Mathlib.Data.Nat.Log
Goal:
b x y : ℕ
hb : 1 < b
h : b ^ x ≤ y
inl : ∀ (hy : y ≠ 0), x ≤ log b y
inr : ∀ (h : b ^ x ≤ 0), x ≤ log b 0
⊢ x ≤ log b y

Tactic:
rcases ne_or_eq y 0 with (hy | rfl)

Premises used: ne_or_eq, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Log
Goal:
b x y : ℕ
hb : 1 < b
h : b ^ x ≤ y
hy : y ≠ 0
⊢ x ≤ log b y

Tactic:
(le_log_iff_pow_le hb hy).2 h

Premises used: Iff.mpr, Nat.le_log_iff_pow_le
-- Module: Mathlib.Data.Nat.Log
Goal:
b x : ℕ
hb : 1 < b
h : b ^ x ≤ 0
⊢ x ≤ log b 0

Tactic:
(h.not_gt (Nat.pow_pos (Nat.zero_lt_one.trans hb))).elim

Premises used: False.elim, LE.le.not_gt, LT.lt.trans, Nat.pow_pos, Nat.zero_lt_one
-- Module: Mathlib.Data.Nat.Log
Goal:
b x y : ℕ
hb : 1 < b
h : b ^ x ≤ y
hy : y ≠ 0
⊢ x ≤ log b y

Tactic:
exacts [(le_log_iff_pow_le hb hy).2 h, (h.not_gt (Nat.pow_pos (Nat.zero_lt_one.trans hb))).elim]

Premises used: Iff.mpr, False.elim, LE.le.not_gt, Nat.le_log_iff_pow_le
-- Module: Mathlib.Data.Nat.Log
Goal:
b x : ℕ
hx : x ≠ 0
⊢ b ^ log b x ≤ x

Tactic:
pow_le_of_le_log hx le_rfl

Premises used: le_rfl, Nat.pow_le_of_le_log
-- Module: Mathlib.Data.Nat.Log
Goal:
b x y : ℕ
hy : y ≠ 0
⊢ y < b ^ x → log b y < x

Tactic:
lt_imp_lt_of_le_imp_le (pow_le_of_le_log hy)

Premises used: Nat.pow_le_of_le_log, lt_imp_lt_of_le_imp_le
-- Module: Mathlib.Data.Nat.Log
Goal:
b x y : ℕ
hx : x ≠ 0
hlt : y < b ^ x
inl : ∀ (hlt : 0 < b ^ x), log b 0 < x
inr : ∀ (hy : y ≠ 0), log b y < x
⊢ log b y < x

Tactic:
rcases eq_or_ne y 0 with rfl | hy

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Log
Goal:
b x : ℕ
hx : x ≠ 0
hlt : 0 < b ^ x
⊢ log b 0 < x

Tactic:
grind [log_zero_right]

Premises used: Nat.log_zero_right
-- Module: Mathlib.Data.Nat.Log
Goal:
b x y : ℕ
hx : x ≠ 0
hlt : y < b ^ x
hy : y ≠ 0
⊢ log b y < x

Tactic:
log_lt_of_lt_pow hy hlt

Premises used: Nat.log_lt_of_lt_pow
-- Module: Mathlib.Data.Nat.Log
Goal:
b x y : ℕ
hx : x ≠ 0
hlt : y < b ^ x
hy : y ≠ 0
⊢ log b y < x

Tactic:
exact log_lt_of_lt_pow hy hlt

Premises used: Nat.log_lt_of_lt_pow
-- Module: Mathlib.Data.Nat.Log
Goal:
b x y : ℕ
hb : 1 < b
⊢ log b y < x → y < b ^ x

Tactic:
lt_imp_lt_of_le_imp_le (le_log_of_pow_le hb)

Premises used: Nat.le_log_of_pow_le, lt_imp_lt_of_le_imp_le
-- Module: Mathlib.Data.Nat.Log
Goal:
b x : ℕ
hx : x ≠ 0
⊢ log b x < x

Tactic:
match le_or_gt b 1 with
  | .inl h => log_of_left_le_one h x ▸ Nat.pos_iff_ne_zero.2 hx
  | .inr h => log_lt_of_lt_pow hx <| Nat.lt_pow_self h

Premises used: Nat.lt_pow_self, Iff.mpr, Nat.pos_iff_ne_zero, _private.0.Nat.log_lt_self.match_1, Eq.rec, le_or_gt, LT.lt, Nat.log_of_left_le_one, Nat.log, OfNat.ofNat, Eq.symm, Nat.log_lt_of_lt_pow
-- Module: Mathlib.Data.Nat.Log
Goal:
b x : ℕ
hx : x = 0
⊢ log b x ≤ x

Tactic:
simp [hx]
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
hb : 1 < b
x : ℕ
⊢ x < b ^ (log b x).succ

Tactic:
lt_pow_of_log_lt hb (lt_succ_self _)

Premises used: Nat.lt_succ_self, Nat.lt_pow_of_log_lt
-- Module: Mathlib.Data.Nat.Log
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)
inr : ∀ (hbn : ¬(1 < b ∧ n ≠ 0)), log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)

Tactic:
rcases em (1 < b ∧ n ≠ 0) with (⟨hb, hn⟩ | hbn)

Premises used: em, Ne, And, LT.lt, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Log
Goal:
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
inl : 1 < b
inl₁ : n ≠ 0
inl₂ : 1 < b
inl₃ : n ≠ 0
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)

Tactic:
rw [le_antisymm_iff, ← Nat.lt_succ_iff, le_log_iff_pow_le, log_lt_iff_lt_pow,
      and_comm]

Premises used: Nat.log_lt_iff_lt_pow, and_comm, Nat.lt_succ_iff, le_antisymm_iff, Nat.le_log_iff_pow_le
-- Module: Mathlib.Data.Nat.Log
Goal:
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ 1 < b

Tactic:
assumption
-- Module: Mathlib.Data.Nat.Log
Goal:
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ n ≠ 0

Tactic:
assumption
-- Module: Mathlib.Data.Nat.Log
Goal:
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hbn : ¬(1 < b ∧ n ≠ 0)
⊢ m ≠ 0

Tactic:
have hm : m ≠ 0 := h.resolve_right hbn
-- Module: Mathlib.Data.Nat.Log
Goal:
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hbn : ¬(1 < b ∧ n ≠ 0)
hm : m ≠ 0
⊢ b ≤ 1 ∨ n = 0

Tactic:
rw [not_and_or, not_lt, Ne, not_not] at hbn

Premises used: Classical.not_not, Ne, not_lt, not_and_or
-- Module: Mathlib.Data.Nat.Log
Goal:
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hbn : ¬(1 < b ∧ n ≠ 0)
hm : m ≠ 0
hbn₁ : b ≤ 1 ∨ n = 0
⊢ m ≠ 0

Tactic:
rw [not_and_or, not_lt, Ne, not_not] at hbn

Premises used: Classical.not_not, Ne, not_lt, not_and_or
-- Module: Mathlib.Data.Nat.Log
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)
inr₁ : ∀ (h : m ≠ 0 ∨ 1 < b ∧ Ne (α := ℕ) 0 0), log b 0 = m ↔ b ^ m ≤ 0 ∧ 0 < b ^ (m + 1)
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)

Tactic:
rcases hbn with (hb | rfl)

Premises used: rfl