awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : Bool
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun (b : Bool) ↦ bif b then 1 else 0) n.bits
bit : digits 2 (Nat.bit false n) = List.map (fun (b : Bool) ↦ bif b then 1 else 0) (false :: n.bits)
⊢ digits 2 (Nat.bit b n) = List.map (fun (b : Bool) ↦ bif b then 1 else 0) (b :: n.bits)
have bit₁ : digits 2 (Nat.bit true n) = List.map (fun (b : Bool) ↦ bif b then 1 else 0) (true :: n.bits)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun (b : Bool) ↦ bif b then 1 else 0) n.bits
⊢ digits 2 (bit false n) = List.map (fun (b : Bool) ↦ bif b then 1 else 0) (false :: n.bits)
have bit : bit false n % 2 :: digits 2 (bit false n / 2) = List.map (fun (b : Bool) ↦ bif b then 1 else 0) (false :: n.bits)
Tactic: rw [digits_def' one_lt_two]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun (b : Bool) ↦ bif b then 1 else 0) n.bits
bit :
  Nat.bit false n % 2 :: digits 2 (Nat.bit false n / 2) =
    List.map (fun (b : Bool) ↦ bif b then 1 else 0) (false :: n.bits)
⊢ digits 2 (Nat.bit false n) = List.map (fun (b : Bool) ↦ bif b then 1 else 0) (false :: n.bits)
have bit₁ : 0 < Nat.bit false n
Tactic: rw [digits_def' one_lt_two]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
n : ℕ
⊢ digits 2 n = List.map (fun (b : Bool) ↦ bif b then 1 else 0) n.bits
have zero : digits 2 0 = List.map (fun (b : Bool) ↦ bif b then 1 else 0) (bits 0)
Tactic: induction n using Nat.binaryRecFromOne with
  | zero => simp
  | one => simp
  | bit b n h ih =>
    rw [bits_append_bit _ _ fun hn => absurd hn h]
    cases b
    · rw [digits_def' one_lt_two]
      · simpa [Nat.bit]
      · simpa [Nat.bit, pos_iff_ne_zero]
    · simpa [Nat.bit, add_comm, digits_add 2 one_lt_two 1 n, Nat.add_mul_div_left]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
n : ℕ
zero : digits 2 0 = List.map (fun (b : Bool) ↦ bif b then 1 else 0) (bits 0)
⊢ digits 2 n = List.map (fun (b : Bool) ↦ bif b then 1 else 0) n.bits
have one : digits 2 1 = List.map (fun (b : Bool) ↦ bif b then 1 else 0) (bits 1)
Tactic: induction n using Nat.binaryRecFromOne with
  | zero => simp
  | one => simp
  | bit b n h ih =>
    rw [bits_append_bit _ _ fun hn => absurd hn h]
    cases b
    · rw [digits_def' one_lt_two]
      · simpa [Nat.bit]
      · simpa [Nat.bit, pos_iff_ne_zero]
    · simpa [Nat.bit, add_comm, digits_add 2 one_lt_two 1 n, Nat.add_mul_div_left]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
n : ℕ
zero : digits 2 0 = List.map (fun (b : Bool) ↦ bif b then 1 else 0) (bits 0)
one : digits 2 1 = List.map (fun (b : Bool) ↦ bif b then 1 else 0) (bits 1)
⊢ digits 2 n = List.map (fun (b : Bool) ↦ bif b then 1 else 0) n.bits
have bit : ∀ (b : Bool) (n : ℕ) (h : n ≠ 0) (ih : digits 2 n = List.map (fun (b : Bool) ↦ bif b then 1 else 0) n.bits),
  digits 2 (bit b n) = List.map (fun (b : Bool) ↦ bif b then 1 else 0) (bit b n).bits
Tactic: induction n using Nat.binaryRecFromOne with
  | zero => simp
  | one => simp
  | bit b n h ih =>
    rw [bits_append_bit _ _ fun hn => absurd hn h]
    cases b
    · rw [digits_def' one_lt_two]
      · simpa [Nat.bit]
      · simpa [Nat.bit, pos_iff_ne_zero]
    · simpa [Nat.bit, add_comm, digits_add 2 one_lt_two 1 n, Nat.add_mul_div_left]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
α : Type u_1
inst : CommRing α
a b k : α
h : k ∣ a - b
⊢ k ∣ ofDigits a [] - ofDigits b []
have nil : k ∣ HSub.hSub (α := α) 0 0
Tactic: change k ∣ 0 - 0
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
α : Type u_1
inst : CommRing α
a b k : α
h : k ∣ a - b
d : ℕ
L : List ℕ
ih : k ∣ ofDigits a L - ofDigits b L
⊢ k ∣ ofDigits a (d :: L) - ofDigits b (d :: L)
have cons : k ∣ a * ofDigits a L - b * ofDigits b L
Tactic: simp only [ofDigits, add_sub_add_left_eq_sub]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
α : Type u_1
inst : CommRing α
a b k : α
h : k ∣ a - b
L : List ℕ
⊢ k ∣ ofDigits a L - ofDigits b L
have nil : k ∣ ofDigits a [] - ofDigits b []
Tactic: induction L with
  | nil => change k ∣ 0 - 0; simp
  | cons d L ih =>
    simp only [ofDigits, add_sub_add_left_eq_sub]
    exact dvd_mul_sub_mul h ih
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
α : Type u_1
inst : CommRing α
a b k : α
h : k ∣ a - b
L : List ℕ
nil : k ∣ ofDigits a [] - ofDigits b []
⊢ k ∣ ofDigits a L - ofDigits b L
have cons : ∀ (d : ℕ) (L : List ℕ) (ih : k ∣ ofDigits a L - ofDigits b L), k ∣ ofDigits a (d :: L) - ofDigits b (d :: L)
Tactic: induction L with
  | nil => change k ∣ 0 - 0; simp
  | cons d L ih =>
    simp only [ofDigits, add_sub_add_left_eq_sub]
    exact dvd_mul_sub_mul h ih
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b b' k : ℕ
h : b ≡ b' [MOD k]
d : ℕ
L : List ℕ
ih : ofDigits b L ≡ ofDigits b' L [MOD k]
⊢ ofDigits b (d :: L) ≡ ofDigits b' (d :: L) [MOD k]
have cons : d + b * ofDigits b L ≡ d + b' * ofDigits b' L [MOD k]
Tactic: dsimp [ofDigits]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
| (d + b * ofDigits b L) % k
have rw : (d % k + b' % k * (ofDigits b' L % k) % k) % k
Tactic: rw [Nat.add_mod, Nat.mul_mod, h, ih]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
⊢ (d + b * ofDigits b L) % k = (d + b' * ofDigits b' L) % k
have cons : (d % k + b' % k * (ofDigits b' L % k) % k) % k = (d + b' * ofDigits b' L) % k
Tactic: conv_lhs => rw [Nat.add_mod, Nat.mul_mod, h, ih]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
| (d + b' * ofDigits b' L) % k
have rw : (d % k + b' % k * (ofDigits b' L % k) % k) % k
Tactic: rw [Nat.add_mod, Nat.mul_mod]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
⊢ (d % k + b' % k * (ofDigits b' L % k) % k) % k = (d + b' * ofDigits b' L) % k
have conv_rhs : (d % k + b' % k * (ofDigits b' L % k) % k) % k = (d + b' * ofDigits b' L) % k
Tactic: conv_rhs => rw [Nat.add_mod, Nat.mul_mod]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
conv_rhs : (d % k + b' % k * (ofDigits b' L % k) % k) % k = (d + b' * ofDigits b' L) % k
⊢ (d % k + b' % k * (ofDigits b' L % k) % k) % k = (d + b' * ofDigits b' L) % k
have cons : (d % k + b' % k * (ofDigits b' L % k) % k) % k = (d % k + b' % k * (ofDigits b' L % k) % k) % k
Tactic: conv_rhs => rw [Nat.add_mod, Nat.mul_mod]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b b' k : ℕ
h : b ≡ b' [MOD k]
L : List ℕ
⊢ ofDigits b L ≡ ofDigits b' L [MOD k]
have nil : ofDigits b [] ≡ ofDigits b' [] [MOD k]
Tactic: induction L with
  | nil => rfl
  | cons d L ih =>
    dsimp [ofDigits]
    dsimp [Nat.ModEq] at *
    conv_lhs => rw [Nat.add_mod, Nat.mul_mod, h, ih]
    conv_rhs => rw [Nat.add_mod, Nat.mul_mod]
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b b' k : ℕ
h : b ≡ b' [MOD k]
L : List ℕ
nil : ofDigits b [] ≡ ofDigits b' [] [MOD k]
⊢ ofDigits b L ≡ ofDigits b' L [MOD k]
have cons : ∀ (d : ℕ) (L : List ℕ) (ih : ofDigits b L ≡ ofDigits b' L [MOD k]), ofDigits b (d :: L) ≡ ofDigits b' (d :: L) [MOD k]
Tactic: induction L with
  | nil => rfl
  | cons d L ih =>
    dsimp [ofDigits]
    dsimp [Nat.ModEq] at *
    conv_lhs => rw [Nat.add_mod, Nat.mul_mod, h, ih]
    conv_rhs => rw [Nat.add_mod, Nat.mul_mod]
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
l : List ℕ
⊢ ofDigits b l % b = l.head! % b
have nil : ofDigits b [] % b = List.head! [] % b
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
l : List ℕ
nil : ofDigits b [] % b = List.head! [] % b
⊢ ofDigits b l % b = l.head! % b
have cons : ∀ (head : ℕ) (tail : List ℕ),
  ofDigits b tail % b = tail.head! % b → ofDigits b (head :: tail) % b = (head :: tail).head! % b
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b n : ℕ
h : b ≠ 1
⊢ (b.digits n).head! = n % b
have pos : ∀ (hb : 1 < b), (b.digits n).head! = n % b
Tactic: by_cases hb : 1 < b
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b n : ℕ
h : b ≠ 1
pos : ∀ (hb : 1 < b), (b.digits n).head! = n % b
⊢ (b.digits n).head! = n % b
have neg : ∀ (hb : ¬1 < b), (b.digits n).head! = n % b
Tactic: by_cases hb : 1 < b
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b n : ℕ
h : b ≠ 1
hb : 1 < b
⊢ (b.digits n).head! = n % b
have pos : (b.digits 0).head! = 0 % b
Tactic: rcases n with _ | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b n : ℕ
h : b ≠ 1
hb : 1 < b
pos : (b.digits 0).head! = 0 % b
⊢ (b.digits n).head! = n % b
have pos₁ : ∀ (n : ℕ), (b.digits (n + 1)).head! = (n + 1) % b
Tactic: rcases n with _ | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
h : b ≠ 1
hb : 1 < b
n : ℕ
⊢ (b.digits (n + 1)).head! = (n + 1) % b
have pos : (b.digits (n + 1)).head! = ofDigits b (b.digits (n + 1)) % b
Tactic: nth_rw 2 [← Nat.ofDigits_digits b (n + 1)]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
h : b ≠ 1
hb : 1 < b
n : ℕ
⊢ (b.digits (n + 1)).head! = ofDigits b (b.digits (n + 1)) % b
have pos : (b.digits (n + 1)).head! = (b.digits (n + 1)).head! % b
Tactic: rw [Nat.ofDigits_mod_eq_head! _ _]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b n : ℕ
h : b ≠ 1
hb : ¬1 < b
⊢ (b.digits n).head! = n % b
have neg : (b.digits 0).head! = 0 % b
Tactic: rcases n with _ | _
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b n : ℕ
h : b ≠ 1
hb : ¬1 < b
neg : (b.digits 0).head! = 0 % b
⊢ (b.digits n).head! = n % b
have neg₁ : ∀ (n : ℕ), (b.digits (n + 1)).head! = (n + 1) % b
Tactic: rcases n with _ | _
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b b' : ℤ
k : ℕ
h : b % (↑k : ℤ) = b' % (↑k : ℤ)
d : ℕ
L : List ℕ
ih : ofDigits b L % (↑k : ℤ) = ofDigits b' L % (↑k : ℤ)
| ((↑d : ℤ) + b * ofDigits b L) % (↑k : ℤ)
have rw : (HMod.hMod (α := ℤ) (↑d : ℤ) (↑k : ℤ) + b' % (↑k : ℤ) * (ofDigits b' L % (↑k : ℤ)) % (↑k : ℤ)) % (↑k : ℤ)
Tactic: rw [Int.add_emod, Int.mul_emod, h, ih]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b b' : ℤ
k : ℕ
h : b % (↑k : ℤ) = b' % (↑k : ℤ)
d : ℕ
L : List ℕ
ih : ofDigits b L % (↑k : ℤ) = ofDigits b' L % (↑k : ℤ)
⊢ ((↑d : ℤ) + b * ofDigits b L) % (↑k : ℤ) = ((↑d : ℤ) + b' * ofDigits b' L) % (↑k : ℤ)
have cons : (HMod.hMod (α := ℤ) (↑d : ℤ) (↑k : ℤ) + b' % (↑k : ℤ) * (ofDigits b' L % (↑k : ℤ)) % (↑k : ℤ)) % (↑k : ℤ) =
  ((↑d : ℤ) + b' * ofDigits b' L) % (↑k : ℤ)
Tactic: conv_lhs => rw [Int.add_emod, Int.mul_emod, h, ih]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b b' : ℤ
k : ℕ
h : b % (↑k : ℤ) = b' % (↑k : ℤ)
d : ℕ
L : List ℕ
ih : ofDigits b L % (↑k : ℤ) = ofDigits b' L % (↑k : ℤ)
| ((↑d : ℤ) + b' * ofDigits b' L) % (↑k : ℤ)
have rw : (HMod.hMod (α := ℤ) (↑d : ℤ) (↑k : ℤ) + b' % (↑k : ℤ) * (ofDigits b' L % (↑k : ℤ)) % (↑k : ℤ)) % (↑k : ℤ)
Tactic: rw [Int.add_emod, Int.mul_emod]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b b' : ℤ
k : ℕ
h : b % (↑k : ℤ) = b' % (↑k : ℤ)
d : ℕ
L : List ℕ
ih : ofDigits b L % (↑k : ℤ) = ofDigits b' L % (↑k : ℤ)
⊢ (HMod.hMod (α := ℤ) (↑d : ℤ) (↑k : ℤ) + b' % (↑k : ℤ) * (ofDigits b' L % (↑k : ℤ)) % (↑k : ℤ)) % (↑k : ℤ) =
    ((↑d : ℤ) + b' * ofDigits b' L) % (↑k : ℤ)
have conv_rhs : (HMod.hMod (α := ℤ) (↑d : ℤ) (↑k : ℤ) + b' % (↑k : ℤ) * (ofDigits b' L % (↑k : ℤ)) % (↑k : ℤ)) % (↑k : ℤ) =
  ((↑d : ℤ) + b' * ofDigits b' L) % (↑k : ℤ)
Tactic: conv_rhs => rw [Int.add_emod, Int.mul_emod]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b b' : ℤ
k : ℕ
h : b % (↑k : ℤ) = b' % (↑k : ℤ)
d : ℕ
L : List ℕ
ih : ofDigits b L % (↑k : ℤ) = ofDigits b' L % (↑k : ℤ)
conv_rhs :
  (HMod.hMod (α := ℤ) (↑d : ℤ) (↑k : ℤ) + b' % (↑k : ℤ) * (ofDigits b' L % (↑k : ℤ)) % (↑k : ℤ)) % (↑k : ℤ) =
    ((↑d : ℤ) + b' * ofDigits b' L) % (↑k : ℤ)
⊢ (HMod.hMod (α := ℤ) (↑d : ℤ) (↑k : ℤ) + b' % (↑k : ℤ) * (ofDigits b' L % (↑k : ℤ)) % (↑k : ℤ)) % (↑k : ℤ) =
    ((↑d : ℤ) + b' * ofDigits b' L) % (↑k : ℤ)
have cons : (HMod.hMod (α := ℤ) (↑d : ℤ) (↑k : ℤ) + b' % (↑k : ℤ) * (ofDigits b' L % (↑k : ℤ)) % (↑k : ℤ)) % (↑k : ℤ) =
  (HMod.hMod (α := ℤ) (↑d : ℤ) (↑k : ℤ) + b' % (↑k : ℤ) * (ofDigits b' L % (↑k : ℤ)) % (↑k : ℤ)) % (↑k : ℤ)
Tactic: conv_rhs => rw [Int.add_emod, Int.mul_emod]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b b' : ℤ
k : ℕ
h : b ≡ b' [ZMOD (↑k : ℤ)]
L : List ℕ
⊢ ofDigits b L ≡ ofDigits b' L [ZMOD (↑k : ℤ)]
have nil : ofDigits b [] ≡ ofDigits b' [] [ZMOD (↑k : ℤ)]
Tactic: induction L with
  | nil => rfl
  | cons d L ih =>
    dsimp [ofDigits]
    dsimp [Int.ModEq] at *
    conv_lhs => rw [Int.add_emod, Int.mul_emod, h, ih]
    conv_rhs => rw [Int.add_emod, Int.mul_emod]
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b b' : ℤ
k : ℕ
h : b ≡ b' [ZMOD (↑k : ℤ)]
L : List ℕ
nil : ofDigits b [] ≡ ofDigits b' [] [ZMOD (↑k : ℤ)]
⊢ ofDigits b L ≡ ofDigits b' L [ZMOD (↑k : ℤ)]
have cons : ∀ (d : ℕ) (L : List ℕ) (ih : ofDigits b L ≡ ofDigits b' L [ZMOD (↑k : ℤ)]),
  ofDigits b (d :: L) ≡ ofDigits b' (d :: L) [ZMOD (↑k : ℤ)]
Tactic: induction L with
  | nil => rfl
  | cons d L ih =>
    dsimp [ofDigits]
    dsimp [Int.ModEq] at *
    conv_lhs => rw [Int.add_emod, Int.mul_emod, h, ih]
    conv_rhs => rw [Int.add_emod, Int.mul_emod]
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ n ≡ (b'.digits n).sum [MOD b]
have rw : n ≡ ofDigits 1 (b'.digits n) [MOD b]
Tactic: rw [← ofDigits_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b b' : ℕ
h : b' % b = 1
n : ℕ
| n ≡ ofDigits 1 (b'.digits n) [MOD b]
have n₁ : b
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b b' : ℕ
h : b' % b = 1
n : ℕ
n₁ : b
| n ≡ ofDigits 1 (b'.digits n) [MOD b]
have a : n
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b b' : ℕ
h : b' % b = 1
n : ℕ
n₁ : b
a : n
| n ≡ ofDigits 1 (b'.digits n) [MOD b]
have b₁ : ofDigits 1 (b'.digits n)
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b b' : ℕ
h : b' % b = 1
n : ℕ
| n
have a : ofDigits b' (b'.digits n)
Tactic: rw [← ofDigits_digits b' n]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b b' : ℕ
h : b' % b = 1
n : ℕ
| n ≡ ofDigits 1 (b'.digits n) [MOD b]
have b₁ : ofDigits 1 (b'.digits n)
Tactic: congr
    · skip
    · rw [← ofDigits_digits b' n]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ n ≡ ofDigits 1 (b'.digits n) [MOD b]
have conv : ofDigits b' (b'.digits n) ≡ ofDigits 1 (b'.digits n) [MOD b]
Tactic: conv =>
    congr
    · skip
    · rw [← ofDigits_digits b' n]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ ofDigits b' (b'.digits n) ≡ ofDigits 1 (b'.digits n) [MOD b]
have h₁ : 1 = b' % b
Tactic: convert! ofDigits_modEq b' b (digits b' n)
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b b' : ℕ
c : ℤ
h : (↑b' : ℤ) ≡ c [ZMOD (↑b : ℤ)]
n : ℕ
| (↑n : ℤ) ≡ ofDigits c (b'.digits n) [ZMOD (↑b : ℤ)]
have n₁ : (↑b : ℤ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b b' : ℕ
c : ℤ
h : (↑b' : ℤ) ≡ c [ZMOD (↑b : ℤ)]
n : ℕ
n₁ : (↑b : ℤ)
| (↑n : ℤ) ≡ ofDigits c (b'.digits n) [ZMOD (↑b : ℤ)]
have a : (↑n : ℤ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b b' : ℕ
c : ℤ
h : (↑b' : ℤ) ≡ c [ZMOD (↑b : ℤ)]
n : ℕ
n₁ : (↑b : ℤ)
a : (↑n : ℤ)
| (↑n : ℤ) ≡ ofDigits c (b'.digits n) [ZMOD (↑b : ℤ)]
have b₁ : ofDigits c (b'.digits n)
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b b' : ℕ
c : ℤ
h : (↑b' : ℤ) ≡ c [ZMOD (↑b : ℤ)]
n : ℕ
| (↑n : ℤ)
have a : (↑(ofDigits b' (b'.digits n)) : ℤ)
Tactic: rw [← ofDigits_digits b' n]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b b' : ℕ
c : ℤ
h : (↑b' : ℤ) ≡ c [ZMOD (↑b : ℤ)]
n : ℕ
| (↑n : ℤ) ≡ ofDigits c (b'.digits n) [ZMOD (↑b : ℤ)]
have b₁ : ofDigits c (b'.digits n)
Tactic: congr
    · skip
    · rw [← ofDigits_digits b' n]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b b' : ℕ
c : ℤ
h : (↑b' : ℤ) ≡ c [ZMOD (↑b : ℤ)]
n : ℕ
⊢ (↑n : ℤ) ≡ ofDigits c (b'.digits n) [ZMOD (↑b : ℤ)]
have conv : (↑(ofDigits b' (b'.digits n)) : ℤ) ≡ ofDigits c (b'.digits n) [ZMOD (↑b : ℤ)]
Tactic: conv =>
    congr
    · skip
    · rw [← ofDigits_digits b' n]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b b' : ℕ
c : ℤ
h : (↑b' : ℤ) ≡ c [ZMOD (↑b : ℤ)]
n : ℕ
⊢ (↑(ofDigits b' (b'.digits n)) : ℤ) ≡ ofDigits c (b'.digits n) [ZMOD (↑b : ℤ)]
have rw : ofDigits (↑b' : ℤ) (b'.digits n) ≡ ofDigits c (b'.digits n) [ZMOD (↑b : ℤ)]
Tactic: rw [coe_ofDigits]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
a b : ℕ
t : List ℕ
⊢ Eq (α := ℤ) (ofDigits (-1) (a :: b :: t)) (List.alternatingSum (List.map (fun (n : ℕ) ↦ (↑n : ℤ)) (a :: b :: t)))
have simp : (↑a : ℤ) + -1 * ((↑b : ℤ) + HMul.hMul (α := ℤ) (-1) (List.alternatingSum (List.map (fun (n : ℕ) ↦ (↑n : ℤ)) t))) =
  HAdd.hAdd (α := ℤ) (↑a : ℤ) (-(↑b : ℤ)) + List.alternatingSum (List.map (fun (n : ℕ) ↦ (↑n : ℤ)) t)
Tactic: simp only [ofDigits, List.alternatingSum, List.map_cons, ofDigits_neg_one t]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
n i b : ℕ
h : 2 ≤ b
⊢ (b.digits n).getD i 0 = n / b ^ i % b
have obtain : ∀ (b : ℕ) (h : 2 ≤ b + 2), ((b + 2).digits n).getD i 0 = n / (b + 2) ^ i % (b + 2)
Tactic: obtain ⟨b, rfl⟩ := Nat.exists_eq_add_of_le' h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b n : ℕ
IH :
  ∀ m ≤ n,
    ∀ (i : ℕ),
      (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) ((b + 2).digits m) i).getD 0 =
        m / (b + 2) ^ i % (b + 2)
i : ℕ
⊢ (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) ((b + 2).digits n.succ) i).getD 0 =
    n.succ / (b + 2) ^ i % (b + 2)
have ind : (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) ((b + 2).digits n.succ) 0).getD 0 =
  n.succ / HPow.hPow (β := ℕ) (b + 2) 0 % (b + 2)
Tactic: rcases i with _ | i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b n : ℕ
IH :
  ∀ m ≤ n,
    ∀ (i : ℕ),
      (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) ((b + 2).digits m) i).getD 0 =
        m / (b + 2) ^ i % (b + 2)
i : ℕ
ind :
  (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) ((b + 2).digits n.succ) 0).getD 0 =
    n.succ / HPow.hPow (β := ℕ) (b + 2) 0 % (b + 2)
⊢ (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) ((b + 2).digits n.succ) i).getD 0 =
    n.succ / (b + 2) ^ i % (b + 2)
have ind₁ : ∀ (i : ℕ),
  (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) ((b + 2).digits n.succ) (i + 1)).getD 0 =
    n.succ / (b + 2) ^ (i + 1) % (b + 2)
Tactic: rcases i with _ | i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b n : ℕ
IH :
  ∀ m ≤ n,
    ∀ (i : ℕ),
      (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) ((b + 2).digits m) i).getD 0 =
        m / (b + 2) ^ i % (b + 2)
⊢ (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) ((b + 2).digits n.succ) 0).getD 0 =
    n.succ / HPow.hPow (β := ℕ) (b + 2) 0 % (b + 2)
have ind : n.succ % (b + 2) = n.succ / HPow.hPow (β := ℕ) (b + 2) default % (b + 2)
Tactic: rw [← List.head?_eq_getElem?, ← default_eq_zero, ← List.head!_eq_head?_getD,
        head!_digits (by grind)]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
n i b : ℕ
⊢ (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) ((b + 2).digits n) i).getD 0 =
    n / (b + 2) ^ i % (b + 2)
have zero : ∀ (i : ℕ),
  (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) ((b + 2).digits 0) i).getD 0 =
    0 / (b + 2) ^ i % (b + 2)
Tactic: induction n using Nat.caseStrongRecOn generalizing i with
  | zero => simp
  | ind n IH =>
    rcases i with _ | i
    · rw [← List.head?_eq_getElem?, ← default_eq_zero, ← List.head!_eq_head?_getD,
        head!_digits (by grind)]
      simp
    · simp [IH _ (le_of_lt_succ (div_lt_self' n b)), pow_succ', Nat.div_div_eq_div_mul]
Cleared hypotheses: n, i
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
n i b : ℕ
zero :
  ∀ (i : ℕ),
    (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) ((b + 2).digits 0) i).getD 0 =
      0 / (b + 2) ^ i % (b + 2)
⊢ (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) ((b + 2).digits n) i).getD 0 =
    n / (b + 2) ^ i % (b + 2)
have ind : ∀ (n : ℕ)
  (IH :
    ∀ m ≤ n,
      ∀ (i : ℕ),
        (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) ((b + 2).digits m) i).getD 0 =
          m / (b + 2) ^ i % (b + 2))
  (i : ℕ),
  (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) ((b + 2).digits n.succ) i).getD 0 =
    n.succ / (b + 2) ^ i % (b + 2)
Tactic: induction n using Nat.caseStrongRecOn generalizing i with
  | zero => simp
  | ind n IH =>
    rcases i with _ | i
    · rw [← List.head?_eq_getElem?, ← default_eq_zero, ← List.head!_eq_head?_getD,
        head!_digits (by grind)]
      simp
    · simp [IH _ (le_of_lt_succ (div_lt_self' n b)), pow_succ', Nat.div_div_eq_div_mul]
Cleared hypotheses: n, i
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
n b : ℕ
hb : 1 < b
l : ℕ
hn : n < b ^ l
⊢ (b.digitsAppend l n).length = l
have rw : (b.digits n).length ≤ l
Tactic: rw [digitsAppend, length_append, length_replicate, Nat.add_sub_cancel']
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (hypothesis)
Goal:
n b : ℕ
hb : 1 < b
l i : ℕ
hi : i ∈ b.digitsAppend l n
⊢ i < b
have hi₁ : i ∈ b.digits n ∨ l - (b.digits n).length ≠ 0 ∧ i = 0
Tactic: rw [digitsAppend, mem_append, mem_replicate] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
n b : ℕ
hb : 1 < b
l i : ℕ
hi : i ∈ b.digits n ∨ l - (b.digits n).length ≠ 0 ∧ i = 0
⊢ i < b
have inl : ∀ (hi : i ∈ b.digits n), i < b
Tactic: obtain hi | ⟨_, rfl⟩ := hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
n b : ℕ
hb : 1 < b
l i : ℕ
hi : i ∈ b.digits n ∨ l - (b.digits n).length ≠ 0 ∧ i = 0
inl : ∀ (hi : i ∈ b.digits n), i < b
⊢ i < b
have inr : l - (b.digits n).length ≠ 0 → 0 < b
Tactic: obtain hi | ⟨_, rfl⟩ := hi
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
n b : ℕ
hb : 1 < b
l : ℕ
left : l - (b.digits n).length ≠ 0
⊢ 0 < b
have linarith : b ≤ 0 → HMul.hMul (α := ℤ) 2 (-1) + (HAdd.hAdd (α := ℤ) 1 1 - (↑b : ℤ)) + HSub.hSub (α := ℤ) (↑b : ℤ) 0 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
n b : ℕ
hb : 1 < b
l : ℕ
left : l - (b.digits n).length ≠ 0
linarith : b ≤ 0 → HMul.hMul (α := ℤ) 2 (-1) + (HAdd.hAdd (α := ℤ) 1 1 - (↑b : ℤ)) + HSub.hSub (α := ℤ) (↑b : ℤ) 0 = 0
⊢ 0 < b
have linarith₁ : b ≤ 0 → GT.gt (α := ℤ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l x : ℕ
h : Membership.mem (γ := Set ℕ) {n : ℕ | n < b ^ l} x
⊢ (b.digitsAppend l x).length = l
have rw : l = l
Tactic: rw [length_digitsAppend hb _ h]