awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
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)
⊢ (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)
have 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)
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']
Cleared hypotheses: b, fuel, hb, hfuel
-- Lean 4 proof step from Mathlib.Data.Nat.Log (hypothesis)
Goal:
b : ℕ
hb : 1 < b
x y : ℕ
h : 1 < b ∧ 1 < x
⊢ (clog.go x b x).snd + 1 ≤ y ↔ x ≤ b ^ y
have H₁ : b ^ (clog.go x b x).snd < x
Tactic: rcases clog.go_spec h.2 hb (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 : ℕ
h : 1 < b ∧ 1 < x
H₁ : b ^ (clog.go x b x).snd < x
⊢ (clog.go x b x).snd + 1 ≤ y ↔ x ≤ b ^ y
have H₂ : 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₂⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Log (hypothesis)
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 ↔ x ≤ b ^ y
have hy₁ : (clog.go x b x).snd + 1 ≤ y
Tactic: rw [← Nat.add_one_le_iff] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
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 ↔ x ≤ b ^ y
have case1 : x > b ^ y
Tactic: apply_rules [iff_of_false, Nat.not_le_of_gt, Nat.lt_add_one_of_le]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (hypothesis)
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 + 1 ≤ y ↔ x ≤ b ^ y
have x₁ : (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₁
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b : ℕ
hb : 1 < b
x y : ℕ
⊢ clog b x ≤ y ↔ x ≤ b ^ y
have case1 : ∀ (h : 1 < b ∧ 1 < x), (clog.go x b x).snd + 1 ≤ 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b : ℕ
hb : 1 < b
x y : ℕ
case1 : ∀ (h : 1 < b ∧ 1 < x), (clog.go x b x).snd + 1 ≤ y ↔ x ≤ b ^ y
⊢ clog b x ≤ y ↔ x ≤ b ^ y
have case2 : ∀ (h : ¬(1 < b ∧ 1 < x)), 0 ≤ 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
hn : 1 < n
⊢ 0 < clog b n
have rw : 0 < (clog.go n b n).snd + 1
Tactic: rw [clog, if_pos]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
hn : 1 < n
rw : 0 < (clog.go n b n).snd + 1
⊢ 0 < clog b n
have hc : 1 < b ∧ 1 < n
Tactic: rw [clog, if_pos]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
hn : 1 < n
⊢ clog b n = clog b ((n + b - 1) / b) + 1
have H : ∀ (c : ℕ), clog b n ≤ c ↔ clog b ((n + b - 1) / b) + 1 ≤ c
Tactic: apply eq_of_forall_ge_iff
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
hn : 1 < n
c : ℕ
⊢ clog b n ≤ c + 1 ↔ clog b ((n + b - 1) / b) + 1 ≤ c + 1
have H : n ≤ b ^ c * b ↔ n + b - 1 ≤ b ^ c * b + b - 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ clog b n = 1
have hn₁ : (n + b - 1) / b ≤ 1
Tactic: rw [clog_of_two_le (hn.trans h) hn, clog_of_right_le_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ (n + b - 1) / b ≤ 1
have hn₁ : n + b - 1 < succ 1 * b
Tactic: rw [← Nat.lt_succ_iff, Nat.div_lt_iff_lt_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
hn₁ : n + b - 1 < succ 1 * b
⊢ (n + b - 1) / b ≤ 1
have hn₂ : 0 < b
Tactic: rw [← Nat.lt_succ_iff, Nat.div_lt_iff_lt_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b x y : ℕ
h : x ≤ b ^ y
⊢ clog b x ≤ y
have inl : ∀ (hb : 1 < b), clog b x ≤ y
Tactic: rcases Nat.lt_or_ge 1 b with hb | hb
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b x y : ℕ
h : x ≤ b ^ y
inl : ∀ (hb : 1 < b), clog b x ≤ y
⊢ clog b x ≤ y
have inr : ∀ (hb : 1 ≥ b), clog b x ≤ y
Tactic: rcases Nat.lt_or_ge 1 b with hb | hb
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b x : ℕ
hb : 1 < b
z : ℕ
⊢ clog b (b ^ x) ≤ z ↔ x ≤ z
have rw : b ^ x ≤ b ^ z ↔ x ≤ z
Tactic: rw [clog_le_iff_le_pow hb, Nat.pow_le_pow_iff_right hb]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b x : ℕ
hb : 1 < b
z : ℕ
rw : b ^ x ≤ b ^ z ↔ x ≤ z
⊢ clog b (b ^ x) ≤ z ↔ x ≤ z
have rw₁ : x ≤ z ↔ x ≤ z
Tactic: rw [clog_le_iff_le_pow hb, Nat.pow_le_pow_iff_right hb]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b : ℕ
hb : 1 < b
x : ℕ
hx : 1 < x
⊢ b ^ (clog b x).pred < x
have rw : (clog b x).pred < clog b x
Tactic: rw [← lt_clog_iff_pow_lt hb]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n m : ℕ
h : n ≤ m
⊢ clog b n ≤ clog b m
have inl : ∀ (hb : b ≤ 1), clog b n ≤ clog b m
Tactic: rcases le_or_gt b 1 with hb | hb
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n m : ℕ
h : n ≤ m
inl : ∀ (hb : b ≤ 1), clog b n ≤ clog b m
⊢ clog b n ≤ clog b m
have inr : ∀ (hb : 1 < b), clog b n ≤ clog b m
Tactic: rcases le_or_gt b 1 with hb | hb
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n m : ℕ
h : n ≤ m
hb : b ≤ 1
⊢ clog b n ≤ clog b m
have inl : 0 ≤ clog b m
Tactic: rw [clog_of_left_le_one hb]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n m : ℕ
h : n ≤ m
hb : 1 < b
⊢ clog b n ≤ clog b m
have inr : n ≤ b ^ clog b m
Tactic: rw [clog_le_iff_le_pow hb]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b c n : ℕ
hc : 1 < c
hb : c ≤ b
⊢ clog b n ≤ clog c n
have rw : n ≤ b ^ clog c n
Tactic: rw [clog_le_iff_le_pow (lt_of_lt_of_le hc hb)]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
⊢ log b n ≤ clog b n
have inl : ∀ (hb : b ≤ 1), log b n ≤ clog b n
Tactic: obtain hb | hb := le_or_gt b 1
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
inl : ∀ (hb : b ≤ 1), log b n ≤ clog b n
⊢ log b n ≤ clog b n
have inr : ∀ (hb : 1 < b), log b n ≤ clog b n
Tactic: obtain hb | hb := le_or_gt b 1
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : b ≤ 1
⊢ log b n ≤ clog b n
have inl : 0 ≤ clog b n
Tactic: rw [log_of_left_le_one hb]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b : ℕ
hb : 1 < b
⊢ log b 0 ≤ clog b 0
have inr : 0 ≤ clog b 0
Tactic: rw [log_zero_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
⊢ log b n ≤ clog b n
have inr : log b 0 ≤ clog b 0
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 _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
inr : log b 0 ≤ clog b 0
⊢ log b n ≤ clog b n
have inr₁ : ∀ (n : ℕ), log b (n + 1) ≤ clog b (n + 1)
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 _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
⊢ clog b n < clog b (n + 1) ↔ b ^ clog b n = n
have refine_1 : ∀ (H : clog b n < clog b (n + 1)), b ^ clog b n = n
Tactic: refine ⟨fun H ↦ ?_, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
refine_1 : ∀ (H : clog b n < clog b (n + 1)), b ^ clog b n = n
⊢ clog b n < clog b (n + 1) ↔ b ^ clog b n = n
have refine_2 : ∀ (H : b ^ clog b n = n), clog b n < clog 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
H : clog b n < clog b (n + 1)
⊢ b ^ clog b n = n
have apply : b ^ clog b n ≤ n
Tactic: apply le_antisymm _ (le_pow_clog hb n)
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
H : clog b n < clog b (n + 1)
⊢ b ^ clog b n ≤ n
have a : b ^ clog b n < n.succ
Tactic: apply le_of_lt_succ
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
H : b ^ clog b n = n
⊢ clog b n < clog b (n + 1)
have refine_2 : n < n + 1
Tactic: rw [lt_clog_iff_pow_lt hb, H]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
⊢ clog b n = clog b (n + 1) ↔ b ^ clog b n ≠ n
have rw : clog b n = clog b (n + 1) ↔ clog b (n + 1) ≤ clog b n
Tactic: rw [ne_eq, ← clog_lt_clog_succ_iff hb, not_lt]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
⊢ clog b n = clog b (n + 1) ↔ clog b (n + 1) ≤ clog b n
have simp : clog b (n + 1) ≤ clog b n → clog b n ≤ clog 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 k n : ℕ
⊢ clog (b ^ k) n = (clog b n + (k - 1)) / k
have inl : clog (HPow.hPow (β := ℕ) b 0) n = (clog b n + HSub.hSub (α := ℕ) 0 1) / 0
Tactic: rcases k.eq_zero_or_pos with rfl | hk
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b k n : ℕ
inl : clog (HPow.hPow (β := ℕ) b 0) n = (clog b n + HSub.hSub (α := ℕ) 0 1) / 0
⊢ clog (b ^ k) n = (clog b n + (k - 1)) / k
have inr : ∀ (hk : k > 0), clog (b ^ k) n = (clog b n + (k - 1)) / k
Tactic: rcases k.eq_zero_or_pos with rfl | hk
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b k n : ℕ
hk : k > 0
⊢ clog (b ^ k) n = (clog b n + (k - 1)) / k
have inr : ∀ (hb : 1 < b), clog (b ^ k) n = (clog b n + (k - 1)) / k
Tactic: rcases Nat.lt_or_ge 1 b with hb | hb
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b k n : ℕ
hk : k > 0
inr : ∀ (hb : 1 < b), clog (b ^ k) n = (clog b n + (k - 1)) / k
⊢ clog (b ^ k) n = (clog b n + (k - 1)) / k
have inr₁ : ∀ (hb : 1 ≥ b), clog (b ^ k) n = (clog b n + (k - 1)) / k
Tactic: rcases Nat.lt_or_ge 1 b with hb | hb
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b k n : ℕ
hk : k > 0
hb : 1 < b
⊢ clog (b ^ k) n = (clog b n + (k - 1)) / k
have inr : ∀ (c : ℕ), c < clog (b ^ k) n ↔ c < (clog b n + (k - 1)) / k
Tactic: refine eq_of_forall_lt_iff fun c ↦ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b k n : ℕ
hk : k > 0
hb : 1 < b
c : ℕ
⊢ c < clog (b ^ k) n ↔ c < (clog b n + (k - 1)) / k
have inr : (b ^ k) ^ c < n ↔ c < (clog b n + (k - 1)) / k
Tactic: rw [lt_clog_iff_pow_lt (Nat.one_lt_pow (Nat.ne_of_gt hk) hb), Nat.lt_div_iff_mul_lt hk,
        Nat.add_sub_cancel, lt_clog_iff_pow_lt hb, Nat.pow_mul']
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b k n : ℕ
hk : k > 0
hb : 1 < b
c : ℕ
inr : (b ^ k) ^ c < n ↔ c < (clog b n + (k - 1)) / k
⊢ c < clog (b ^ k) n ↔ c < (clog b n + (k - 1)) / k
have inr₁ : (b ^ k) ^ c < n ↔ c * k < clog b n + (k - 1) - (k - 1)
Tactic: rw [lt_clog_iff_pow_lt (Nat.one_lt_pow (Nat.ne_of_gt hk) hb), Nat.lt_div_iff_mul_lt hk,
        Nat.add_sub_cancel, lt_clog_iff_pow_lt hb, Nat.pow_mul']
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b k n : ℕ
hk : k > 0
hb : 1 < b
c : ℕ
inr : (b ^ k) ^ c < n ↔ c < (clog b n + (k - 1)) / k
inr₁ : (b ^ k) ^ c < n ↔ c * k < clog b n + (k - 1) - (k - 1)
⊢ c < clog (b ^ k) n ↔ c < (clog b n + (k - 1)) / k
have inr₂ : (b ^ k) ^ c < n ↔ c * k < clog b n
Tactic: rw [lt_clog_iff_pow_lt (Nat.one_lt_pow (Nat.ne_of_gt hk) hb), Nat.lt_div_iff_mul_lt hk,
        Nat.add_sub_cancel, lt_clog_iff_pow_lt hb, Nat.pow_mul']
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b k n : ℕ
hk : k > 0
hb : 1 < b
c : ℕ
inr : (b ^ k) ^ c < n ↔ c < (clog b n + (k - 1)) / k
inr₁ : (b ^ k) ^ c < n ↔ c * k < clog b n + (k - 1) - (k - 1)
inr₂ : (b ^ k) ^ c < n ↔ c * k < clog b n
⊢ c < clog (b ^ k) n ↔ c < (clog b n + (k - 1)) / k
have inr₃ : (b ^ k) ^ c < n ↔ b ^ (c * k) < n
Tactic: rw [lt_clog_iff_pow_lt (Nat.one_lt_pow (Nat.ne_of_gt hk) hb), Nat.lt_div_iff_mul_lt hk,
        Nat.add_sub_cancel, lt_clog_iff_pow_lt hb, Nat.pow_mul']
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b k n : ℕ
hk : k > 0
hb : 1 < b
c : ℕ
inr : (b ^ k) ^ c < n ↔ c < (clog b n + (k - 1)) / k
inr₁ : (b ^ k) ^ c < n ↔ c * k < clog b n + (k - 1) - (k - 1)
inr₂ : (b ^ k) ^ c < n ↔ c * k < clog b n
inr₃ : (b ^ k) ^ c < n ↔ b ^ (c * k) < n
⊢ c < clog (b ^ k) n ↔ c < (clog b n + (k - 1)) / k
have inr₄ : (b ^ k) ^ c < n ↔ (b ^ k) ^ c < n
Tactic: rw [lt_clog_iff_pow_lt (Nat.one_lt_pow (Nat.ne_of_gt hk) hb), Nat.lt_div_iff_mul_lt hk,
        Nat.add_sub_cancel, lt_clog_iff_pow_lt hb, Nat.pow_mul']
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b k n : ℕ
hk : k > 0
hb : 1 ≥ b
⊢ clog (b ^ k) n = (clog b n + (k - 1)) / k
have inr : (k - 1) / k = 0
Tactic: suffices (k - 1) / k = 0 by grind [clog_of_left_le_one, Nat.pow_le_one_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b k n : ℕ
hk : k > 0
hb : 1 ≥ b
⊢ (k - 1) / k = 0
have inr : k - 1 < k
Tactic: apply Nat.div_eq_of_lt
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (hypothesis)
Goal:
n p : ℕ
hp : 1 < p ∧ n ≠ 0
hmod : n % p = 0
⊢ n / (p * p) < n / p
have hmod₁ : p ∣ n
Tactic: rw [← Nat.dvd_iff_mod_eq_zero] at hmod
Cleared hypotheses: hmod
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
n p : ℕ
hp : 1 < p ∧ n ≠ 0
hmod : p ∣ n
⊢ n / (p * p) < n / p
have rcases : ∀ (m : ℕ) (hp : 1 < p ∧ p * m ≠ 0), p * m / (p * p) < p * m / p
Tactic: rcases hmod with ⟨m, rfl⟩
Cleared hypotheses: n, hp, hmod
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (hypothesis)
Goal:
p m : ℕ
hp : 1 < p ∧ p * m ≠ 0
⊢ p * m / (p * p) < p * m / p
have hp₀ : 0 < p
Tactic: have hp₀ : 0 < p := Nat.lt_trans Nat.one_pos hp.1
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
p m : ℕ
hp : 1 < p ∧ p * m ≠ 0
hp₀ : 0 < p
⊢ p * m / (p * p) < p * m / p
have rw : m / p < m
Tactic: rw [Nat.mul_div_mul_left _ _ hp₀, Nat.mul_div_cancel_left _ hp₀]
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
n p : ℕ
hp : 1 < p ∧ n ≠ 0
hmod : n % p = 0
⊢ n / (p * p) < n / p
have rw : ∀ (hmod : p ∣ n), n / (p * p) < n / p
Tactic: decreasing_by
    rw [← Nat.dvd_iff_mod_eq_zero] at hmod
    rcases hmod with ⟨m, rfl⟩
    have hp₀ : 0 < p := Nat.lt_trans Nat.one_pos hp.1
    rw [Nat.mul_div_mul_left _ _ hp₀, Nat.mul_div_cancel_left _ hp₀]
    exact Nat.div_lt_self (by grind) hp.1
Cleared hypotheses: hmod
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
n p : ℕ
hp : 1 < p ∧ n ≠ 0
hmod : n % p = 0
rw rw₁ rw₂ : ∀ (hmod : p ∣ n), n / (p * p) < n / p
⊢ n / (p * p) < n / p
have rw₃ : ∀ (m : ℕ) (hp : 1 < p ∧ p * m ≠ 0), p * m / (p * p) < p * m / p
Tactic: decreasing_by
    rw [← Nat.dvd_iff_mod_eq_zero] at hmod
    rcases hmod with ⟨m, rfl⟩
    have hp₀ : 0 < p := Nat.lt_trans Nat.one_pos hp.1
    rw [Nat.mul_div_mul_left _ _ hp₀, Nat.mul_div_cancel_left _ hp₀]
    exact Nat.div_lt_self (by grind) hp.1
Cleared hypotheses: n, hp, hmod
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
n p : ℕ
hp : 1 < p ∧ n ≠ 0
hmod : n % p = 0
rw rw₁ rw₂ : ∀ (hmod : p ∣ n), n / (p * p) < n / p
rw₃ : ∀ (m : ℕ) (hp : 1 < p ∧ p * m ≠ 0), p * m / (p * p) < p * m / p
⊢ n / (p * p) < n / p
have rw₄ : ∀ (m : ℕ) (hp : 1 < p ∧ p * m ≠ 0) (hp₀ : 0 < p), p * m / (p * p) < p * m / p
Tactic: decreasing_by
    rw [← Nat.dvd_iff_mod_eq_zero] at hmod
    rcases hmod with ⟨m, rfl⟩
    have hp₀ : 0 < p := Nat.lt_trans Nat.one_pos hp.1
    rw [Nat.mul_div_mul_left _ _ hp₀, Nat.mul_div_cancel_left _ hp₀]
    exact Nat.div_lt_self (by grind) hp.1
Cleared hypotheses: n, hp, hmod
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
n p : ℕ
hp : 1 < p ∧ n ≠ 0
hmod : n % p = 0
rw rw₁ rw₂ : ∀ (hmod : p ∣ n), n / (p * p) < n / p
rw₃ : ∀ (m : ℕ) (hp : 1 < p ∧ p * m ≠ 0), p * m / (p * p) < p * m / p
rw₄ : ∀ (m : ℕ) (hp : 1 < p ∧ p * m ≠ 0) (hp₀ : 0 < p), p * m / (p * p) < p * m / p
⊢ n / (p * p) < n / p
have rw₅ : ∀ (m : ℕ) (hp : 1 < p ∧ p * m ≠ 0) (hp₀ : 0 < p), m / p < m
Tactic: decreasing_by
    rw [← Nat.dvd_iff_mod_eq_zero] at hmod
    rcases hmod with ⟨m, rfl⟩
    have hp₀ : 0 < p := Nat.lt_trans Nat.one_pos hp.1
    rw [Nat.mul_div_mul_left _ _ hp₀, Nat.mul_div_cancel_left _ hp₀]
    exact Nat.div_lt_self (by grind) hp.1
Cleared hypotheses: n, hp, hmod
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (hypothesis)
Goal:
n p_1 p : ℕ
hp : 1 < p ∧ n ≠ 0
hmod : n % p = 0
e q : ℕ
heq : go n (p * p) ⋯ = (e, q)
hqp : q % p = 0
ih : (go n (p * p) ⋯).snd * (p * p) ^ (go n (p * p) ⋯).fst = n ∧ ¬p * p ∣ (go n (p * p) ⋯).snd
⊢ (2 * e + 1, q / p).snd * p ^ (2 * e + 1, q / p).fst = n ∧ ¬p ∣ (2 * e + 1, q / p).snd
have ih₁ : (e, q).snd * (p * p) ^ (e, q).fst = n ∧ ¬p * p ∣ (e, q).snd
Tactic: rw [heq] at ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
n p_1 p : ℕ
hp : 1 < p ∧ n ≠ 0
hmod : n % p = 0
e q : ℕ
heq : go n (p * p) ⋯ = (e, q)
hqp : q % p = 0
ih : (e, q).snd * (p * p) ^ (e, q).fst = n ∧ ¬p * p ∣ (e, q).snd
⊢ (2 * e + 1, q / p).snd * p ^ (2 * e + 1, q / p).fst = n ∧ ¬p ∣ (2 * e + 1, q / p).snd
have case1 : ∀ (hdvd : ¬p * p ∣ (e, q).snd) (hp : 1 < p ∧ (e, q).snd * (p * p) ^ (e, q).fst ≠ 0)
  (hmod : (e, q).snd * (p * p) ^ (e, q).fst % p = 0) (heq : go ((e, q).snd * (p * p) ^ (e, q).fst) (p * p) sorry = (e, q)),
  (2 * e + 1, q / p).snd * p ^ (2 * e + 1, q / p).fst = (e, q).snd * (p * p) ^ (e, q).fst ∧ ¬p ∣ (2 * e + 1, q / p).snd
Tactic: rcases ih with ⟨rfl, hdvd⟩
Cleared hypotheses: n, hp, hmod, heq, ih
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (hypothesis)
Goal:
p_1 p e q : ℕ
hqp : q % p = 0
hdvd : ¬p * p ∣ (e, q).snd
hp : 1 < p ∧ (e, q).snd * (p * p) ^ (e, q).fst ≠ 0
hmod : (e, q).snd * (p * p) ^ (e, q).fst % p = 0
heq : go ((e, q).snd * (p * p) ^ (e, q).fst) (p * p) ⋯ = (e, q)
⊢ (2 * e + 1, q / p).snd * p ^ (2 * e + 1, q / p).fst = (e, q).snd * (p * p) ^ (e, q).fst ∧ ¬p ∣ (2 * e + 1, q / p).snd
have hp₀ : 0 < p
Tactic: have hp₀ : 0 < p := Nat.lt_trans Nat.one_pos hp.1
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (hypothesis)
Goal:
n p_1 p : ℕ
hp : 1 < p ∧ n ≠ 0
hmod : n % p = 0
e q : ℕ
heq : go n (p * p) ⋯ = (e, q)
hqp : ¬q % p = 0
ih : (go n (p * p) ⋯).snd * (p * p) ^ (go n (p * p) ⋯).fst = n ∧ ¬p * p ∣ (go n (p * p) ⋯).snd
⊢ (2 * e, q).snd * p ^ (2 * e, q).fst = n ∧ ¬p ∣ (2 * e, q).snd
have ih₁ : (e, q).snd * (p * p) ^ (e, q).fst = n ∧ ¬p * p ∣ (e, q).snd
Tactic: rw [heq] at ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
n p_1 p : ℕ
hp : 1 < p ∧ n ≠ 0
hmod : n % p = 0
e q : ℕ
heq : go n (p * p) ⋯ = (e, q)
hqp : ¬q % p = 0
ih : (e, q).snd * (p * p) ^ (e, q).fst = n ∧ ¬p * p ∣ (e, q).snd
⊢ (2 * e, q).snd * p ^ (2 * e, q).fst = n ∧ ¬p ∣ (2 * e, q).snd
have case2 : ∀ (hdvd : ¬p * p ∣ (e, q).snd) (hp : 1 < p ∧ (e, q).snd * (p * p) ^ (e, q).fst ≠ 0)
  (hmod : (e, q).snd * (p * p) ^ (e, q).fst % p = 0) (heq : go ((e, q).snd * (p * p) ^ (e, q).fst) (p * p) sorry = (e, q)),
  (2 * e, q).snd * p ^ (2 * e, q).fst = (e, q).snd * (p * p) ^ (e, q).fst ∧ ¬p ∣ (2 * e, q).snd
Tactic: rcases ih with ⟨rfl, hdvd⟩
Cleared hypotheses: n, hp, hmod, heq, ih
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
n p : ℕ
hnp : 1 < p ∧ n ≠ 0
⊢ (go n p hnp).snd * p ^ (go n p hnp).fst = n ∧ ¬p ∣ (go n p hnp).snd
have case1 : ∀ (p : ℕ) (hp : 1 < p ∧ n ≠ 0) (hmod : n % p = 0) (e q : ℕ) (heq : go n (p * p) sorry = (e, q)) (hqp : q % p = 0)
  (ih : (go n (p * p) sorry).snd * (p * p) ^ (go n (p * p) sorry).fst = n ∧ ¬p * p ∣ (go n (p * p) sorry).snd),
  (2 * e + 1, q / p).snd * p ^ (2 * e + 1, q / p).fst = n ∧ ¬p ∣ (2 * e + 1, q / p).snd
Tactic: fun_induction go with
  | case1 p hp hmod e q heq hqp ih =>
    rw [heq] at ih
    rcases ih with ⟨rfl, hdvd⟩
    have hp₀ : 0 < p := Nat.lt_trans Nat.one_pos hp.1
    simp_all [← Nat.dvd_iff_mod_eq_zero, Nat.pow_add', ← Nat.mul_assoc, Nat.div_mul_cancel,
      Nat.two_mul, Nat.mul_pow]
  | case2 p hp hmod e q heq hqp ih =>
    rw [heq] at ih
    rcases ih with ⟨rfl, hdvd⟩
    simp_all [Nat.dvd_iff_mod_eq_zero, Nat.two_mul, Nat.mul_pow, Nat.pow_add]
  | case3 =>
    simp_all [Nat.dvd_iff_mod_eq_zero]
Cleared hypotheses: hnp
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
n p : ℕ
hnp : 1 < p ∧ n ≠ 0
case1 :
  ∀ (p : ℕ) (hp : 1 < p ∧ n ≠ 0) (hmod : n % p = 0) (e q : ℕ) (heq : go n (p * p) ⋯ = (e, q)) (hqp : q % p = 0)
    (ih : (go n (p * p) ⋯).snd * (p * p) ^ (go n (p * p) ⋯).fst = n ∧ ¬p * p ∣ (go n (p * p) ⋯).snd),
    (2 * e + 1, q / p).snd * p ^ (2 * e + 1, q / p).fst = n ∧ ¬p ∣ (2 * e + 1, q / p).snd
⊢ (go n p hnp).snd * p ^ (go n p hnp).fst = n ∧ ¬p ∣ (go n p hnp).snd
have case2 : ∀ (p : ℕ) (hp : 1 < p ∧ n ≠ 0) (hmod : n % p = 0) (e q : ℕ) (heq : go n (p * p) sorry = (e, q)) (hqp : ¬q % p = 0)
  (ih : (go n (p * p) sorry).snd * (p * p) ^ (go n (p * p) sorry).fst = n ∧ ¬p * p ∣ (go n (p * p) sorry).snd),
  (2 * e, q).snd * p ^ (2 * e, q).fst = n ∧ ¬p ∣ (2 * e, q).snd
Tactic: fun_induction go with
  | case1 p hp hmod e q heq hqp ih =>
    rw [heq] at ih
    rcases ih with ⟨rfl, hdvd⟩
    have hp₀ : 0 < p := Nat.lt_trans Nat.one_pos hp.1
    simp_all [← Nat.dvd_iff_mod_eq_zero, Nat.pow_add', ← Nat.mul_assoc, Nat.div_mul_cancel,
      Nat.two_mul, Nat.mul_pow]
  | case2 p hp hmod e q heq hqp ih =>
    rw [heq] at ih
    rcases ih with ⟨rfl, hdvd⟩
    simp_all [Nat.dvd_iff_mod_eq_zero, Nat.two_mul, Nat.mul_pow, Nat.pow_add]
  | case3 =>
    simp_all [Nat.dvd_iff_mod_eq_zero]
Cleared hypotheses: hnp