awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p : ℕ
L : List ℕ
h_nonempty : L ≠ []
h_ne_zero : L.getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ L, l < p
h : 1 < p
inl :
  ∀ {h_nonempty : Ne (α := List ℕ) [] []} (h_ne_zero : List.getLast [] h_nonempty ≠ 0)
    (h_lt : ∀ (l : ℕ), Membership.mem (γ := List ℕ) [] l → l < p),
    (p - 1) * ∑ i ∈ range (List.length (α := ℕ) []), ofDigits p [] / p ^ i.succ = ofDigits p [] - List.sum []
inl₁ :
  ∀ (hd : ℕ) (tl : List ℕ)
    (ih :
      ∀ {h_nonempty : tl ≠ []} (h_ne_zero : tl.getLast h_nonempty ≠ 0) (h_lt : ∀ l ∈ tl, l < p),
        (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum)
    {h_nonempty : hd :: tl ≠ []} (h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0) (h_lt : ∀ l ∈ hd :: tl, l < p),
    (p - 1) * ∑ i ∈ range (hd :: tl).length, ofDigits p (hd :: tl) / p ^ i.succ = ofDigits p (hd :: tl) - (hd :: tl).sum
⊢ (p - 1) * ∑ i ∈ range L.length, ofDigits p L / p ^ i.succ = ofDigits p L - L.sum

Tactic:
induction L with
    | nil => simp [ofDigits]
    | cons hd tl ih =>
      simp only [List.length_cons, List.sum_cons, self_div_pow_eq_ofDigits_drop _ _ h,
          digits_ofDigits p h (hd :: tl) h_lt (fun _ => h_ne_zero)]
      simp only [ofDigits]
      rw [sum_range_succ, Nat.cast_id]
      simp only [List.drop, List.drop_length]
      obtain rfl | h' := em <| tl = []
      · simp [ofDigits]
      · have w₁' := fun l hl ↦ h_lt l <| List.mem_cons_of_mem hd hl
        have w₂' := fun (h : tl ≠ []) ↦ (List.getLast_cons h) ▸ h_ne_zero
        have ih := ih (w₂' h') w₁'
        simp only [self_div_pow_eq_ofDigits_drop _ _ h, digits_ofDigits p h tl w₁' w₂',
          ← Nat.one_add] at ih
        have := sum_singleton (fun x ↦ ofDigits p <| tl.drop x) tl.length
        rw [← Ico_succ_singleton, List.drop_length, ofDigits] at this
        have h₁ : 1 ≤ tl.length := List.length_pos_iff.mpr h'
        rw [← sum_range_add_sum_Ico _ <| h₁, ← add_zero (∑ x ∈ Ico _ _, ofDigits p (tl.drop x)),
            ← this, sum_Ico_consecutive _ h₁ <| (le_add_right tl.length 1),
            ← sum_Ico_add _ 0 tl.length 1,
            Ico_zero_eq_range, mul_add, mul_add, ih, range_one, sum_singleton, List.drop, ofDigits,
            mul_zero, add_zero, ← Nat.add_sub_assoc <| sum_le_ofDigits _ <| Nat.le_of_lt h]
        nth_rw 2 [← one_mul <| ofDigits p tl]
        rw [← add_mul, Nat.sub_add_cancel (one_le_of_lt h), Nat.add_sub_add_left]

Premises used: add_mul, Finset.sum_range_add_sum_Ico, Nat.cast_id, Nat.sum_le_ofDigits, Finset.cons, List.length_cons, Nat.ofDigits, Nat.add_sub_assoc, Nat.add_sub_add_left, em, Nat.one_le_of_lt, Nat.le_of_lt, MulZeroClass.mul_zero, Finset.sum_singleton, Nat.sub_add_cancel, List.drop, List.sum_cons, Nat.Ico_zero_eq_range, Nat.Ico_succ_singleton, mul_add, Finset.range_one, add_zero, Nat.one_add, Finset.sum_range_succ, one_mul, rfl, Nat.self_div_pow_eq_ofDigits_drop, List.drop_length
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
L : List ℕ
h_nonempty : L ≠ []
h_ne_zero : L.getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ L, l < 1
⊢ HSub.hSub (α := ℕ) 1 1 * ∑ i ∈ range L.length, ofDigits 1 L / HPow.hPow (α := ℕ) 1 i.succ = ofDigits 1 L - L.sum

Tactic:
simp [ofDigits_one]

Premises used: Nat.ofDigits_one
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p : ℕ
L : List ℕ
h_nonempty : L ≠ []
h_ne_zero : L.getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ L, l < p
h : p < 1
inr : 0 = ofDigits 0 L - L.sum
⊢ (p - 1) * ∑ i ∈ range L.length, ofDigits p L / p ^ i.succ = ofDigits p L - L.sum

Tactic:
simp [lt_one_iff.mp h]

Premises used: Nat.lt_one_iff, Iff.mp
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p : ℕ
L : List ℕ
h_nonempty : L ≠ []
h_ne_zero : L.getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ L, l < p
h : p < 1
inr :
  ∀ {h_nonempty : Ne (α := List ℕ) [] []} (h_ne_zero : List.getLast [] h_nonempty ≠ 0)
    (h_lt : ∀ (l : ℕ), Membership.mem (γ := List ℕ) [] l → l < p), 0 = HSub.hSub (α := ℕ) (ofDigits 0 []) (List.sum [])
inr₁ :
  ∀ (head : ℕ) (tail : List ℕ) {h_nonempty : head :: tail ≠ []} (h_ne_zero : (head :: tail).getLast h_nonempty ≠ 0)
    (h_lt : ∀ l ∈ head :: tail, l < p), 0 = ofDigits 0 (head :: tail) - (head :: tail).sum
⊢ 0 = ofDigits 0 L - L.sum

Tactic:
cases L
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p : ℕ
h : p < 1
h_nonempty : Ne (α := List ℕ) [] []
h_ne_zero : List.getLast [] h_nonempty ≠ 0
h_lt : ∀ (l : ℕ), Membership.mem (γ := List ℕ) [] l → l < p
⊢ 0 = HSub.hSub (α := ℕ) (ofDigits 0 []) (List.sum [])

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p : ℕ
h : p < 1
head : ℕ
tail : List ℕ
h_nonempty : head :: tail ≠ []
h_ne_zero : (head :: tail).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ head :: tail, l < p
⊢ 0 = ofDigits 0 (head :: tail) - (head :: tail).sum

Tactic:
simp [ofDigits]

Premises used: Nat.ofDigits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p n : ℕ
⊢ 1 < p ∨ 1 = p ∨ p < 1

Tactic:
trichotomous 1 p

Premises used: trichotomous, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p n : ℕ
inl : ∀ (h : 1 < p), (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum
inr : HSub.hSub (α := ℕ) 1 1 * ∑ i ∈ range (log 1 n).succ, n / HPow.hPow (α := ℕ) 1 i.succ = n - (digits 1 n).sum
inr₁ : ∀ (h : p < 1), (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum

Tactic:
obtain h | rfl | h : 1 < p ∨ 1 = p ∨ p < 1 := trichotomous 1 p

Premises used: trichotomous, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p n : ℕ
h : 1 < p
inl : (p - 1) * ∑ i ∈ range (log p 0).succ, 0 / p ^ i.succ = 0 - (p.digits 0).sum
inl₁ : ∀ (hn : n ≠ 0), (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p : ℕ
h : 1 < p
⊢ (p - 1) * ∑ i ∈ range (log p 0).succ, 0 / p ^ i.succ = 0 - (p.digits 0).sum

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p n : ℕ
h : 1 < p
hn : n ≠ 0
⊢ (p - 1) * ∑ i ∈ range (p.digits n).length, ofDigits p (p.digits n) / p ^ i.succ =
    ofDigits p (p.digits n) - (p.digits n).sum

Tactic:
sub_one_mul_sum_div_pow_eq_sub_sum_digits (p.digits n) (getLast_digit_ne_zero p hn) <|
        (fun l a ↦ digits_lt_base h a)

Premises used: Nat.digits_lt_base, Nat.getLast_digit_ne_zero, Nat.sub_one_mul_sum_div_pow_eq_sub_sum_digits, Nat.digits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p n : ℕ
h : 1 < p
hn : n ≠ 0
h₁ : (log p n).succ = (p.digits n).length
h₂ : ∀ x ∈ range (p.digits n).length, n = ofDigits p (p.digits n)
h₃ : n = ofDigits p (p.digits n)
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum

Tactic:
convert!
      sub_one_mul_sum_div_pow_eq_sub_sum_digits (p.digits n) (getLast_digit_ne_zero p hn) <|
        (fun l a ↦ digits_lt_base h a)

Premises used: Nat.digits_lt_base, Nat.getLast_digit_ne_zero, Nat.sub_one_mul_sum_div_pow_eq_sub_sum_digits, Nat.digits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p n : ℕ
h : 1 < p
hn : n ≠ 0
⊢ (log p n).succ = (p.digits n).length

Tactic:
(length_digits p n h hn).symm

Premises used: Nat.length_digits, Eq.symm
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p n : ℕ
h : 1 < p
hn : n ≠ 0
⊢ (log p n).succ = (p.digits n).length

Tactic:
refine (length_digits p n h hn).symm

Premises used: Nat.length_digits, Eq.symm
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p n : ℕ
h : 1 < p
hn : n ≠ 0
x : ℕ
h_1 : x ∈ range (p.digits n).length
⊢ n = ofDigits p (p.digits n)

Tactic:
(ofDigits_digits p n).symm

Premises used: Eq.symm, Nat.ofDigits_digits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p n : ℕ
h : 1 < p
hn : n ≠ 0
x : ℕ
h_1 : x ∈ range (p.digits n).length
⊢ n = ofDigits p (p.digits n)

Tactic:
exact (ofDigits_digits p n).symm

Premises used: Eq.symm, Nat.ofDigits_digits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p n : ℕ
h : 1 < p
hn : n ≠ 0
⊢ n = ofDigits p (p.digits n)

Tactic:
(ofDigits_digits p n).symm

Premises used: Eq.symm, Nat.ofDigits_digits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p n : ℕ
h : 1 < p
hn : n ≠ 0
⊢ n = ofDigits p (p.digits n)

Tactic:
exact (ofDigits_digits p n).symm

Premises used: Eq.symm, Nat.ofDigits_digits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
n : ℕ
⊢ HSub.hSub (α := ℕ) 1 1 * ∑ i ∈ range (log 1 n).succ, n / HPow.hPow (α := ℕ) 1 i.succ = n - (digits 1 n).sum

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p n : ℕ
h : p < 1
inr : 0 = n - (digits 0 n).sum
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum

Tactic:
simp [lt_one_iff.mp h]

Premises used: Nat.lt_one_iff, Iff.mp
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p n : ℕ
h : p < 1
inr : 0 = 0 - (digits 0 0).sum
inr₁ : ∀ (n : ℕ), 0 = n + 1 - (digits 0 (n + 1)).sum
⊢ 0 = n - (digits 0 n).sum

Tactic:
cases n
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p : ℕ
h : p < 1
⊢ 0 = 0 - (digits 0 0).sum

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p : ℕ
h : p < 1
n : ℕ
⊢ 0 = n + 1 - (digits 0 (n + 1)).sum

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
⊢ digits 2 0 = List.map (fun (b : Bool) ↦ bif b then 1 else 0) (bits 0)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
⊢ digits 2 1 = List.map (fun (b : Bool) ↦ bif b then 1 else 0) (bits 1)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Lemmas
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 b n) = List.map (fun (b : Bool) ↦ bif b then 1 else 0) (b :: n.bits)
⊢ digits 2 (Nat.bit b n) = List.map (fun (b : Bool) ↦ bif b then 1 else 0) (Nat.bit b n).bits

Tactic:
rw [bits_append_bit _ _ fun hn => absurd hn h]

Premises used: Nat.bits_append_bit, absurd
-- Module: Mathlib.Data.Nat.Digits.Lemmas
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)
bit₁ : digits 2 (Nat.bit true n) = List.map (fun (b : Bool) ↦ bif b then 1 else 0) (true :: n.bits)
⊢ digits 2 (Nat.bit b n) = List.map (fun (b : Bool) ↦ bif b then 1 else 0) (b :: n.bits)

Tactic:
cases b
-- Module: Mathlib.Data.Nat.Digits.Lemmas
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)
bit₁ : 0 < Nat.bit false n
⊢ digits 2 (Nat.bit false n) = List.map (fun (b : Bool) ↦ bif b then 1 else 0) (false :: n.bits)

Tactic:
rw [digits_def' one_lt_two]

Premises used: one_lt_two, Nat.digits_def'
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun (b : Bool) ↦ bif b then 1 else 0) n.bits
⊢ 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:
simpa [Nat.bit]

Premises used: Nat.bit
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun (b : Bool) ↦ bif b then 1 else 0) n.bits
⊢ 0 < bit false n

Tactic:
simpa [Nat.bit, pos_iff_ne_zero]

Premises used: Nat.bit, pos_iff_ne_zero
-- Module: Mathlib.Data.Nat.Digits.Lemmas
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 true n) = List.map (fun (b : Bool) ↦ bif b then 1 else 0) (true :: n.bits)

Tactic:
simpa [Nat.bit, add_comm, digits_add 2 one_lt_two 1 n, Nat.add_mul_div_left]

Premises used: Nat.bit, Nat.digits_add, add_comm, one_lt_two, Nat.add_mul_div_left, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Digits.Lemmas
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)
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 (Nat.bit b n) = List.map (fun (b : Bool) ↦ bif b then 1 else 0) (Nat.bit b n).bits
⊢ digits 2 n = List.map (fun (b : Bool) ↦ bif b then 1 else 0) 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]

Premises used: Nat.bit, Nat.digits_add, add_comm, one_lt_two, Nat.digits_def', Nat.zero, Nat.add_mul_div_left, OfNat.ofNat, pos_iff_ne_zero
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
α : Type u_1
inst : CommRing α
a b k : α
h : k ∣ a - b
nil : k ∣ HSub.hSub (α := α) 0 0
⊢ k ∣ ofDigits a [] - ofDigits b []

Tactic:
change k ∣ 0 - 0
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
α : Type u_1
inst : CommRing α
a b k : α
h : k ∣ a - b
⊢ k ∣ HSub.hSub (α := α) 0 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
α : Type u_1
inst : CommRing α
a b k : α
h : k ∣ a - b
d : ℕ
L : List ℕ
ih : k ∣ ofDigits a L - ofDigits b L
cons : k ∣ a * ofDigits a L - b * ofDigits b L
⊢ k ∣ ofDigits a (d :: L) - ofDigits b (d :: L)

Tactic:
simp only [ofDigits, add_sub_add_left_eq_sub]

Premises used: Nat.ofDigits, add_sub_add_left_eq_sub
-- Module: Mathlib.Data.Nat.Digits.Lemmas
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 ∣ a * ofDigits a L - b * ofDigits b L

Tactic:
dvd_mul_sub_mul h ih

Premises used: dvd_mul_sub_mul
-- Module: Mathlib.Data.Nat.Digits.Lemmas
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 ∣ a * ofDigits a L - b * ofDigits b L

Tactic:
exact dvd_mul_sub_mul h ih

Premises used: dvd_mul_sub_mul
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
α : Type u_1
inst : CommRing α
a b k : α
h : k ∣ a - b
L : List ℕ
nil : k ∣ ofDigits a [] - ofDigits b []
cons : ∀ (d : ℕ) (L : List ℕ) (ih : k ∣ ofDigits a L - ofDigits b L), k ∣ ofDigits a (d :: L) - ofDigits b (d :: L)
⊢ k ∣ ofDigits a L - ofDigits b 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

Premises used: Finset.cons, Nat.ofDigits, add_sub_add_left_eq_sub
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b b' k : ℕ
h : b ≡ b' [MOD k]
⊢ ofDigits b [] ≡ ofDigits b' [] [MOD k]

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b b' k : ℕ
h : b ≡ b' [MOD k]
d : ℕ
L : List ℕ
ih : ofDigits b L ≡ ofDigits b' L [MOD k]
cons : d + b * ofDigits b L ≡ d + b' * ofDigits b' L [MOD k]
⊢ ofDigits b (d :: L) ≡ ofDigits b' (d :: L) [MOD k]

Tactic:
dsimp [ofDigits]

Premises used: Nat.ofDigits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
rw : (d % k + b' % k * (ofDigits b' L % k) % k) % k
| (d + b * ofDigits b L) % k

Tactic:
rw [Nat.add_mod, Nat.mul_mod, h, ih]

Premises used: Nat.mul_mod, Nat.add_mod
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
cons : (d % k + b' % k * (ofDigits b' L % k) % k) % k = (d + b' * ofDigits b' L) % k
⊢ (d + b * ofDigits b L) % k = (d + b' * ofDigits b' L) % k

Tactic:
conv_lhs => rw [Nat.add_mod, Nat.mul_mod, h, ih]

Premises used: Nat.mul_mod, Nat.add_mod
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
rw : (d % k + b' % k * (ofDigits b' L % k) % k) % k
| (d + b' * ofDigits b' L) % k

Tactic:
rw [Nat.add_mod, Nat.mul_mod]

Premises used: Nat.mul_mod, Nat.add_mod
-- Module: Mathlib.Data.Nat.Digits.Lemmas
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
cons : (d % k + b' % k * (ofDigits b' L % k) % k) % k = (d % k + b' % k * (ofDigits b' L % k) % k) % k
⊢ (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]

Premises used: Nat.mul_mod, Nat.add_mod
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b b' k : ℕ
h : b ≡ b' [MOD k]
L : List ℕ
nil : ofDigits b [] ≡ ofDigits b' [] [MOD k]
cons :
  ∀ (d : ℕ) (L : List ℕ) (ih : ofDigits b L ≡ ofDigits b' L [MOD k]), ofDigits b (d :: L) ≡ ofDigits b' (d :: L) [MOD k]
⊢ ofDigits b L ≡ ofDigits b' 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]

Premises used: Finset.cons, Nat.ofDigits, Nat.mul_mod, Nat.ModEq, Nat.add_mod
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b k : ℕ
L : List ℕ
⊢ ofDigits b L ≡ ofDigits (b % k) L [MOD k]

Tactic:
ofDigits_modEq' b (b % k) k (b.mod_modEq k).symm L

Premises used: Nat.mod_modEq, HMod.hMod, Nat.ModEq.symm, Nat.ofDigits_modEq'
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b k : ℕ
L : List ℕ
⊢ ofDigits b L % k = ofDigits (b % k) L % k

Tactic:
ofDigits_modEq b k L

Premises used: Nat.ModEq, Nat.ofDigits_modEq
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
l : List ℕ
nil : ofDigits b [] % b = List.head! [] % b
cons :
  ∀ (head : ℕ) (tail : List ℕ),
    ofDigits b tail % b = tail.head! % b → ofDigits b (head :: tail) % b = (head :: tail).head! % b
⊢ ofDigits b l % b = l.head! % b

Tactic:
induction l
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
⊢ ofDigits b [] % b = List.head! [] % b

Tactic:
simp [Nat.ofDigits]

Premises used: Nat.ofDigits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b head : ℕ
tail : List ℕ
tail_ih : ofDigits b tail % b = tail.head! % b
⊢ ofDigits b (head :: tail) % b = (head :: tail).head! % b

Tactic:
simp [Nat.ofDigits]

Premises used: Nat.ofDigits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b n : ℕ
h : b ≠ 1
pos : ∀ (hb : 1 < b), (b.digits n).head! = n % b
neg : ∀ (hb : ¬1 < b), (b.digits n).head! = n % b
⊢ (b.digits n).head! = n % b

Tactic:
by_cases hb : 1 < b
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b n : ℕ
h : b ≠ 1
hb : 1 < b
pos : (b.digits 0).head! = 0 % b
pos₁ : ∀ (n : ℕ), (b.digits (n + 1)).head! = (n + 1) % b
⊢ (b.digits n).head! = n % b

Tactic:
rcases n with _ | n
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
h : b ≠ 1
hb : 1 < b
⊢ (b.digits 0).head! = 0 % b

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
h : b ≠ 1
hb : 1 < b
n : ℕ
pos : (b.digits (n + 1)).head! = ofDigits b (b.digits (n + 1)) % b
⊢ (b.digits (n + 1)).head! = (n + 1) % b

Tactic:
nth_rw 2 [← Nat.ofDigits_digits b (n + 1)]

Premises used: HAdd.hAdd, OfNat.ofNat, Nat.ofDigits_digits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
h : b ≠ 1
hb : 1 < b
n : ℕ
pos : (b.digits (n + 1)).head! = (b.digits (n + 1)).head! % b
⊢ (b.digits (n + 1)).head! = ofDigits b (b.digits (n + 1)) % b

Tactic:
rw [Nat.ofDigits_mod_eq_head! _ _]

Premises used: Nat.ofDigits_mod_eq_head!
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
h : b ≠ 1
hb : 1 < b
n : ℕ
⊢ (b.digits (n + 1)).head! = (b.digits (n + 1)).head! % b

Tactic:
(Nat.mod_eq_of_lt (Nat.digits_lt_base hb <| List.head!_mem_self <|
          Nat.digits_ne_nil_iff_ne_zero.mpr <| Nat.succ_ne_zero n)).symm

Premises used: Iff.mpr, List.head!_mem_self, Nat.digits_lt_base, Nat.mod_eq_of_lt, Nat.succ_ne_zero, Nat.digits_ne_nil_iff_ne_zero, Eq.symm
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
h : b ≠ 1
hb : 1 < b
n : ℕ
⊢ (b.digits (n + 1)).head! = (b.digits (n + 1)).head! % b

Tactic:
exact (Nat.mod_eq_of_lt (Nat.digits_lt_base hb <| List.head!_mem_self <|
          Nat.digits_ne_nil_iff_ne_zero.mpr <| Nat.succ_ne_zero n)).symm

Premises used: Iff.mpr, List.head!_mem_self, Nat.digits_lt_base, Nat.mod_eq_of_lt, Nat.succ_ne_zero, Nat.digits_ne_nil_iff_ne_zero, Eq.symm
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b n : ℕ
h : b ≠ 1
hb : ¬1 < b
neg : (b.digits 0).head! = 0 % b
neg₁ : ∀ (n : ℕ), (b.digits (n + 1)).head! = (n + 1) % b
⊢ (b.digits n).head! = n % b

Tactic:
rcases n with _ | _
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
h : b ≠ 1
hb : ¬1 < b
⊢ b = 0

Tactic:
lia
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
h : b ≠ 1
hb : ¬1 < b
⊢ (b.digits 0).head! = 0 % b

Tactic:
simp_all [show b = 0 by lia]
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
h : b ≠ 1
hb : ¬1 < b
n : ℕ
⊢ b = 0

Tactic:
lia
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
h : b ≠ 1
hb : ¬1 < b
n : ℕ
⊢ (b.digits (n + 1)).head! = (n + 1) % b

Tactic:
simp_all [show b = 0 by lia]
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b b' : ℤ
k : ℕ
h : b ≡ b' [ZMOD (↑k : ℤ)]
⊢ ofDigits b [] ≡ ofDigits b' [] [ZMOD (↑k : ℤ)]

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b b' : ℤ
k : ℕ
h : b % (↑k : ℤ) = b' % (↑k : ℤ)
d : ℕ
L : List ℕ
ih : ofDigits b L % (↑k : ℤ) = ofDigits b' L % (↑k : ℤ)
rw : (HMod.hMod (α := ℤ) (↑d : ℤ) (↑k : ℤ) + b' % (↑k : ℤ) * (ofDigits b' L % (↑k : ℤ)) % (↑k : ℤ)) % (↑k : ℤ)
| ((↑d : ℤ) + b * ofDigits b L) % (↑k : ℤ)

Tactic:
rw [Int.add_emod, Int.mul_emod, h, ih]

Premises used: Int.mul_emod, Int.add_emod
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b b' : ℤ
k : ℕ
h : b % (↑k : ℤ) = b' % (↑k : ℤ)
d : ℕ
L : List ℕ
ih : ofDigits b L % (↑k : ℤ) = ofDigits b' L % (↑k : ℤ)
cons :
  (HMod.hMod (α := ℤ) (↑d : ℤ) (↑k : ℤ) + b' % (↑k : ℤ) * (ofDigits b' L % (↑k : ℤ)) % (↑k : ℤ)) % (↑k : ℤ) =
    ((↑d : ℤ) + b' * ofDigits b' L) % (↑k : ℤ)
⊢ ((↑d : ℤ) + b * ofDigits b L) % (↑k : ℤ) = ((↑d : ℤ) + b' * ofDigits b' L) % (↑k : ℤ)

Tactic:
conv_lhs => rw [Int.add_emod, Int.mul_emod, h, ih]

Premises used: Int.mul_emod, Int.add_emod
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b b' : ℤ
k : ℕ
h : b % (↑k : ℤ) = b' % (↑k : ℤ)
d : ℕ
L : List ℕ
ih : ofDigits b L % (↑k : ℤ) = ofDigits b' L % (↑k : ℤ)
rw : (HMod.hMod (α := ℤ) (↑d : ℤ) (↑k : ℤ) + b' % (↑k : ℤ) * (ofDigits b' L % (↑k : ℤ)) % (↑k : ℤ)) % (↑k : ℤ)
| ((↑d : ℤ) + b' * ofDigits b' L) % (↑k : ℤ)

Tactic:
rw [Int.add_emod, Int.mul_emod]

Premises used: Int.mul_emod, Int.add_emod
-- Module: Mathlib.Data.Nat.Digits.Lemmas
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 : ℤ)
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 : ℤ)
⊢ (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]

Premises used: Int.mul_emod, Int.add_emod
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b b' : ℤ
k : ℕ
h : b ≡ b' [ZMOD (↑k : ℤ)]
L : List ℕ
nil : ofDigits b [] ≡ ofDigits b' [] [ZMOD (↑k : ℤ)]
cons :
  ∀ (d : ℕ) (L : List ℕ) (ih : ofDigits b L ≡ ofDigits b' L [ZMOD (↑k : ℤ)]),
    ofDigits b (d :: L) ≡ ofDigits b' (d :: L) [ZMOD (↑k : ℤ)]
⊢ ofDigits b L ≡ ofDigits b' 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]

Premises used: Finset.cons, Nat.ofDigits, Int.ModEq, Int.mul_emod, Int.add_emod
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℤ
k : ℕ
L : List ℕ
⊢ ofDigits b L ≡ ofDigits (b % (↑k : ℤ)) L [ZMOD (↑k : ℤ)]

Tactic:
ofDigits_zmodeq' b (b % k) k (b.mod_modEq ↑k).symm L

Premises used: Int.ModEq.symm, Nat.cast, HMod.hMod, Nat.ofDigits_zmodeq', Int.mod_modEq
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℤ
k : ℕ
L : List ℕ
⊢ ofDigits b L % (↑k : ℤ) = ofDigits (b % (↑k : ℤ)) L % (↑k : ℤ)

Tactic:
ofDigits_zmodeq b k L

Premises used: Nat.ofDigits_zmodeq, Int.ModEq