awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : b ≤ 1
⊢ log b (n / b) = log b n - 1
have inl : 0 = log b n - 1
Tactic: rw [log_of_left_le_one hb, log_of_left_le_one hb, Nat.zero_sub]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : b ≤ 1
inl : 0 = log b n - 1
⊢ log b (n / b) = log b n - 1
have inl₁ : 0 = HSub.hSub (α := ℕ) 0 1
Tactic: rw [log_of_left_le_one hb, log_of_left_le_one hb, Nat.zero_sub]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
⊢ log b (n / b) = log b n - 1
have inr : ∀ (h : n < b), log b (n / b) = log b n - 1
Tactic: rcases lt_or_ge n b with h | h
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
inr : ∀ (h : n < b), log b (n / b) = log b n - 1
⊢ log b (n / b) = log b n - 1
have inr₁ : ∀ (h : b ≤ n), log b (n / b) = log b n - 1
Tactic: rcases lt_or_ge n b with h | h
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
h : n < b
⊢ log b (n / b) = log b n - 1
have inr : log b 0 = log b n - 1
Tactic: rw [div_eq_of_lt h, log_of_lt h, log_zero_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
h : n < b
inr : log b 0 = log b n - 1
⊢ log b (n / b) = log b n - 1
have inr₁ : log b 0 = HSub.hSub (α := ℕ) 0 1
Tactic: rw [div_eq_of_lt h, log_of_lt h, log_zero_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
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
⊢ log b (n / b) = log b n - 1
have inr₂ : 0 = HSub.hSub (α := ℕ) 0 1
Tactic: rw [div_eq_of_lt h, log_of_lt h, log_zero_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
h : b ≤ n
⊢ log b (n / b) = log b n - 1
have inr : log b (n / b) = log b (n / b) + 1 - 1
Tactic: rw [log_of_one_lt_of_le hb h, Nat.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
h : b ≤ n
inr : log b (n / b) = log b (n / b) + 1 - 1
⊢ log b (n / b) = log b n - 1
have inr₁ : log b (n / b) = log b (n / b)
Tactic: rw [log_of_one_lt_of_le hb h, Nat.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n k : ℕ
hk : log b (n / b ^ k) = log b n - k
⊢ log b (n / b ^ (k + 1)) = log b n - (k + 1)
have succ : log b (n / (b ^ k * b)) = log b n - (k + 1)
Tactic: rw [Nat.pow_succ, ← Nat.div_div_eq_div_mul, log_div_base, hk, sub_add_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
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)
⊢ log b (n / b ^ (k + 1)) = log b n - (k + 1)
have succ₁ : log b (n / b ^ k / b) = log b n - (k + 1)
Tactic: rw [Nat.pow_succ, ← Nat.div_div_eq_div_mul, log_div_base, hk, sub_add_eq]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
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)
⊢ log b (n / b ^ (k + 1)) = log b n - (k + 1)
have succ₂ : 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
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)
⊢ log b (n / b ^ (k + 1)) = log b n - (k + 1)
have succ₃ : log b n - 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
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)
⊢ log b (n / b ^ (k + 1)) = log b n - (k + 1)
have succ₄ : log b n - 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n k : ℕ
⊢ log b (n / b ^ k) = log b n - k
have zero : log b (n / HPow.hPow (β := ℕ) b 0) = log b n - 0
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]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n k : ℕ
zero : log b (n / HPow.hPow (β := ℕ) b 0) = log b n - 0
⊢ log b (n / b ^ k) = log b n - k
have succ : ∀ (k : ℕ) (hk : log b (n / b ^ k) = log b n - k), log b (n / b ^ (k + 1)) = log b n - (k + 1)
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]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
⊢ log b (n / b * b) = log b n
have inl : ∀ (hb : b ≤ 1), log b (n / b * b) = log b n
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 * b) = log b n
⊢ log b (n / b * b) = log b n
have inr : ∀ (hb : 1 < b), log b (n / b * b) = log b n
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 / b * b) = log b n
have inl : 0 = log b n
Tactic: rw [log_of_left_le_one hb, log_of_left_le_one hb]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : b ≤ 1
inl : 0 = log b n
⊢ log b (n / b * b) = log b n
have inl₁ : Eq (α := ℕ) 0 0
Tactic: rw [log_of_left_le_one hb, log_of_left_le_one hb]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
⊢ log b (n / b * b) = log b n
have inr : ∀ (h : n < b), log b (n / b * b) = log b n
Tactic: rcases lt_or_ge n b with h | h
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
inr : ∀ (h : n < b), log b (n / b * b) = log b n
⊢ log b (n / b * b) = log b n
have inr₁ : ∀ (h : b ≤ n), log b (n / b * b) = log b n
Tactic: rcases lt_or_ge n b with h | h
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
h : n < b
⊢ log b (n / b * b) = log b n
have inr : log b (0 * b) = log b n
Tactic: rw [div_eq_of_lt h, Nat.zero_mul, log_zero_right, log_of_lt h]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
h : n < b
inr : log b (0 * b) = log b n
⊢ log b (n / b * b) = log b n
have inr₁ : log b 0 = log b n
Tactic: rw [div_eq_of_lt h, Nat.zero_mul, log_zero_right, log_of_lt h]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
h : n < b
inr : log b (0 * b) = log b n
inr₁ : log b 0 = log b n
⊢ log b (n / b * b) = log b n
have inr₂ : 0 = log b n
Tactic: rw [div_eq_of_lt h, Nat.zero_mul, log_zero_right, log_of_lt h]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
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
⊢ log b (n / b * b) = log b n
have inr₃ : Eq (α := ℕ) 0 0
Tactic: rw [div_eq_of_lt h, Nat.zero_mul, log_zero_right, log_of_lt h]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
h : b ≤ n
⊢ log b (n / b * b) = log b n
have inr : log b (n / b) + 1 = 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)]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
h : b ≤ n
inr : log b (n / b) + 1 = log b n
⊢ log b (n / b * b) = log b n
have inr₁ : log b n - 1 + 1 = 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)]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
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
⊢ log b (n / b * b) = log b n
have inr₂ : log b n = 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)]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ (n + b - 1) / b < n
have rw : n + b ≤ n * b
Tactic: rw [div_lt_iff_lt_mul (by lia), ← succ_le_iff, ← pred_eq_sub_one,
    succ_pred_eq_of_pos (by lia)]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b : Bool
n : ℕ
hn : n ≠ 0
⊢ log 2 (bit b n) = log 2 n + 1
have rw : log 2 (bit b n / 2 * 2) = log 2 n + 1
Tactic: rw [← log_div_mul_self, bit_div_two, log_mul_base Nat.one_lt_two hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b : Bool
n : ℕ
hn : n ≠ 0
rw : log 2 (bit b n / 2 * 2) = log 2 n + 1
⊢ log 2 (bit b n) = log 2 n + 1
have rw₁ : log 2 (n * 2) = log 2 n + 1
Tactic: rw [← log_div_mul_self, bit_div_two, log_mul_base Nat.one_lt_two hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
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
⊢ log 2 (bit b n) = log 2 n + 1
have rw₂ : log 2 n + 1 = log 2 n + 1
Tactic: rw [← log_div_mul_self, bit_div_two, log_mul_base Nat.one_lt_two hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
n : ℕ
⊢ n.log2 = log 2 n
have inl : log2 0 = log 2 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:
n : ℕ
inl : log2 0 = log 2 0
⊢ n.log2 = log 2 n
have inr : ∀ (hn : n ≠ 0), n.log2 = log 2 n
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
⊢ log2 0 = log 2 0
have inl : 0 = log 2 0
Tactic: rw [log2_zero, log_zero_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
inl : 0 = log 2 0
⊢ log2 0 = log 2 0
have inl₁ : Eq (α := ℕ) 0 0
Tactic: rw [log2_zero, log_zero_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ n.log2 = log 2 n
have inr : ∀ (c : ℕ), c ≤ n.log2 ↔ c ≤ log 2 n
Tactic: apply eq_of_forall_le_iff
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
n : ℕ
hn : n ≠ 0
m : ℕ
⊢ m ≤ n.log2 ↔ m ≤ log 2 n
have inr : HPow.hPow (α := ℕ) 2 m ≤ n ↔ m ≤ log 2 n
Tactic: rw [Nat.le_log2 hn, Nat.le_log_iff_pow_le Nat.one_lt_two hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
n : ℕ
hn : n ≠ 0
m : ℕ
inr : HPow.hPow (α := ℕ) 2 m ≤ n ↔ m ≤ log 2 n
⊢ m ≤ n.log2 ↔ m ≤ log 2 n
have inr₁ : HPow.hPow (α := ℕ) 2 m ≤ n ↔ HPow.hPow (α := ℕ) 2 m ≤ n
Tactic: rw [Nat.le_log2 hn, Nat.le_log_iff_pow_le Nat.one_lt_two hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b k n : ℕ
⊢ log (b ^ k) n = log b n / k
have inl : log (b ^ k) 0 = log b 0 / k
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 k n : ℕ
inl : log (b ^ k) 0 = log b 0 / k
⊢ log (b ^ k) n = log b n / k
have inr : ∀ (hn : n ≠ 0), log (b ^ k) n = log b n / k
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b k n : ℕ
hn : n ≠ 0
⊢ log (b ^ k) n = log b n / k
have inr : log (HPow.hPow (β := ℕ) b 0) n = log b n / 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 : ℕ
hn : n ≠ 0
inr : log (HPow.hPow (β := ℕ) b 0) n = log b n / 0
⊢ log (b ^ k) n = log b n / k
have inr₁ : ∀ (hk : k > 0), log (b ^ k) n = log b n / 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 : ℕ
hn : n ≠ 0
hk : k > 0
⊢ log (b ^ k) n = log b n / k
have inr : ∀ (hb : 1 < b), log (b ^ k) n = log b n / 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 : ℕ
hn : n ≠ 0
hk : k > 0
inr : ∀ (hb : 1 < b), log (b ^ k) n = log b n / k
⊢ log (b ^ k) n = log b n / k
have inr₁ : ∀ (hb : 1 ≥ b), log (b ^ k) n = log b n / 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 : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 < b
⊢ log (b ^ k) n = log b n / k
have inr : ∀ (c : ℕ), c ≤ log (b ^ k) n ↔ c ≤ log b n / k
Tactic: refine eq_of_forall_le_iff fun c ↦ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 < b
c : ℕ
⊢ c ≤ log (b ^ k) n ↔ c ≤ log b n / k
have inr : (b ^ k) ^ c ≤ 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']
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 < b
c : ℕ
inr : (b ^ k) ^ c ≤ n ↔ c ≤ log b n / k
⊢ c ≤ log (b ^ k) n ↔ c ≤ log b n / k
have inr₁ : (b ^ k) ^ c ≤ n ↔ c * k ≤ log b n
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']
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
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
⊢ c ≤ log (b ^ k) n ↔ c ≤ log b n / k
have inr₂ : (b ^ k) ^ c ≤ n ↔ b ^ (c * k) ≤ n
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']
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
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
⊢ c ≤ log (b ^ k) n ↔ c ≤ log b n / k
have inr₃ : (b ^ k) ^ c ≤ n ↔ (b ^ k) ^ c ≤ n
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']
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 ≥ b
⊢ log (b ^ k) n = log b n / k
have inr : b ^ k ≤ 1
Tactic: rw [log_of_left_le_one hb, Nat.zero_div, log_of_left_le_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 ≥ b
⊢ b ^ k ≤ 1
have inr : b ≤ 1
Tactic: rwa [Nat.pow_le_one_iff (Nat.ne_of_gt hk)]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (hypothesis)
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)
have ih₁ : (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₃⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Log (hypothesis)
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
⊢ (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)
have ih₂ : (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₃⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Log (hypothesis)
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
⊢ (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)
have ih₃ : 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₃⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
n : ℕ
hn : 1 < n
fuel : ℕ
ih :
  ∀ {b : ℕ} (hb : 1 < b) (hfuel : n < b ^ fuel),
    (go n b fuel).fst = b ^ ((go n b fuel).snd + 1) / n ∧ b ^ (go n b fuel).snd < n ∧ n ≤ b ^ ((go n b fuel).snd + 1)
b : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b < n
ih₁ : (go n (b * b) fuel).fst = (b * b) ^ ((go n (b * b) fuel).snd + 1) / n
ih₂ : (b * b) ^ (go n (b * b) fuel).snd < n
ih₃ : n ≤ (b * b) ^ ((go n (b * b) fuel).snd + 1)
⊢ (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)
have succ : ∀ (ih₁ : (go n (HPow.hPow (β := ℕ) b 2) fuel).fst = b * b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n)
  (ih₂ : b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd) < n)
  (ih₃ : n ≤ b * b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1)),
  (if b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) < n then
          (b * b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
            2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1)
        else
          (b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
            2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd)).fst =
      b ^
          ((if b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) < n then
                (b * b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
                  2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1)
              else
                (b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
                  2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd)).snd +
            1) /
        n ∧
    b ^
          (if b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) < n then
              (b * b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
                2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1)
            else
              (b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
                2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd)).snd <
        n ∧
      n ≤
        b ^
          ((if b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) < n then
                (b * b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
                  2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1)
              else
                (b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
                  2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd)).snd +
            1)
Tactic: simp_all only [go, if_neg (Nat.not_le_of_gt hbn), ← Nat.pow_two, ← Nat.pow_mul,
        Nat.div_lt_iff_lt_mul (Nat.zero_lt_of_lt hbn), Nat.div_div_eq_div_mul,
        Nat.mul_comm n b, Nat.mul_add_one, @Nat.pow_add_one' _ (2 * _ + 1),
        Nat.mul_lt_mul_left, Nat.mul_div_mul_left, Nat.zero_lt_of_lt hb]
Cleared hypotheses: ih₁, ih₂, ih₃
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
n : ℕ
hn : 1 < n
fuel : ℕ
ih :
  ∀ {b : ℕ} (hb : 1 < b) (hfuel : n < b ^ fuel),
    (go n b fuel).fst = b ^ ((go n b fuel).snd + 1) / n ∧ b ^ (go n b fuel).snd < n ∧ n ≤ b ^ ((go n b fuel).snd + 1)
b : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b < n
ih₁ : (go n (HPow.hPow (β := ℕ) b 2) fuel).fst = b * b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n
ih₂ : b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd) < n
ih₃ : n ≤ b * b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1)
⊢ (if b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) < n then
          (b * b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
            2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1)
        else
          (b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
            2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd)).fst =
      b ^
          ((if b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) < n then
                (b * b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
                  2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1)
              else
                (b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
                  2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd)).snd +
            1) /
        n ∧
    b ^
          (if b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) < n then
              (b * b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
                2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1)
            else
              (b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
                2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd)).snd <
        n ∧
      n ≤
        b ^
          ((if b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) < n then
                (b * b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
                  2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1)
              else
                (b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
                  2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd)).snd +
            1)
have succ : b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) < n →
  (b * b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
          2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1).fst =
      b ^
          ((b * b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
                2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1).snd +
            1) /
        n ∧
    b ^
          (b * b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
              2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1).snd <
        n ∧
      n ≤
        b ^
          ((b * b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) / n,
                2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1).snd +
            1)
Tactic: split
-- Lean 4 proof step from Mathlib.Data.Nat.Log (hypothesis)
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)
⊢ (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)
have x : b < n ∨ b ≥ n
Tactic: cases Nat.lt_or_ge b n with
    | inr hbn => simp_all [go]
    | inl hbn =>
      rcases ih (Nat.one_mul 1 ▸ Nat.mul_lt_mul_of_lt_of_lt hb hb)
        (log.go_aux hb hfuel (Nat.le_of_lt hbn)) with ⟨ih₁, ih₂, ih₃⟩
      simp_all only [go, if_neg (Nat.not_le_of_gt hbn), ← Nat.pow_two, ← Nat.pow_mul,
        Nat.div_lt_iff_lt_mul (Nat.zero_lt_of_lt hbn), Nat.div_div_eq_div_mul,
        Nat.mul_comm n b, Nat.mul_add_one, @Nat.pow_add_one' _ (2 * _ + 1),
        Nat.mul_lt_mul_left, Nat.mul_div_mul_left, Nat.zero_lt_of_lt hb]
      split <;> simp_all [Nat.mul_add_one, Nat.pow_add_one']
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
n b fuel : ℕ
hn : 1 < n
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)
have 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)
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