awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l d : ℕ
w : List ℕ
left : w ∈ fixedLengthDigits hb l
hL : d :: w ∈ consFixedLengthDigits hb l d
rw rw₁ : d = d
⊢ (d :: w).head ⋯ = d

Tactic:
rw [head_cons]

Premises used: List.head_cons
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
⊢ d :: L ∈ fixedLengthDigits hb (l + 1)

Tactic:
(mem_fixedLengthDigits_iff hb).mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, And.intro, List.mem_fixedLengthDigits_iff
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
refine_1 : (d :: L).length = l + 1
refine_2 : ∀ x ∈ d :: L, x < b
⊢ d :: L ∈ fixedLengthDigits hb (l + 1)

Tactic:
refine (mem_fixedLengthDigits_iff hb).mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, And.intro, List.mem_fixedLengthDigits_iff
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
⊢ (d :: L).length = l + 1

Tactic:
simpa using ((mem_fixedLengthDigits_iff hb).mp hL).1

Premises used: And.left, Iff.mp, List.mem_fixedLengthDigits_iff
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
x : ℕ
hx : x ∈ d :: L
refine_2 : ∀ (hd : x < b) (hx : x ∈ x :: L), x < b
refine_2₁ : ∀ (hx : x ∈ L), x < b
⊢ x < b

Tactic:
obtain rfl | hx := mem_cons.mp hx

Premises used: Iff.mp, List.mem_cons, rfl
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
x : ℕ
hd : x < b
hx : x ∈ x :: L
⊢ x < b

Tactic:
hd
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
x : ℕ
hd : x < b
hx : x ∈ x :: L
⊢ x < b

Tactic:
exact hd
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
x : ℕ
hx_1 : x ∈ d :: L
hx : x ∈ L
⊢ x < b

Tactic:
((mem_fixedLengthDigits_iff hb).mp hL).2 _ hx

Premises used: And.right, Iff.mp, List.mem_fixedLengthDigits_iff
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
x : ℕ
hx_1 : x ∈ d :: L
hx : x ∈ L
⊢ x < b

Tactic:
exact ((mem_fixedLengthDigits_iff hb).mp hL).2 _ hx

Premises used: And.right, Iff.mp, List.mem_fixedLengthDigits_iff
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
⊢ (↑(Finset.range b) : Set ℕ).PairwiseDisjoint (α := Finset (List ℕ)) fun (d : ℕ) ↦ consFixedLengthDigits hb l d

Tactic:
Finset.pairwiseDisjoint_iff.mpr fun i _ j _ ⟨L, hL⟩ ↦ ?_

Premises used: Iff.mpr, Finset.pairwiseDisjoint_iff, _private.0.List.pairwiseDisjoint_consFixedLengthDigits.match_1, Eq
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
refine :
  ∀ i ∈ (↑(Finset.range b) : Set ℕ),
    ∀ j ∈ (↑(Finset.range b) : Set ℕ),
      (consFixedLengthDigits hb l i ∩ consFixedLengthDigits hb l j).Nonempty →
        ∀ (L : List ℕ) (hL : L ∈ consFixedLengthDigits hb l i ∩ consFixedLengthDigits hb l j), i = j
⊢ (↑(Finset.range b) : Set ℕ).PairwiseDisjoint (α := Finset (List ℕ)) fun (d : ℕ) ↦ consFixedLengthDigits hb l d

Tactic:
refine Finset.pairwiseDisjoint_iff.mpr fun i _ j _ ⟨L, hL⟩ ↦ ?_

Premises used: Iff.mpr, Finset.pairwiseDisjoint_iff
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l i : ℕ
h : i ∈ (↑(Finset.range b) : Set ℕ)
j : ℕ
h_1 : j ∈ (↑(Finset.range b) : Set ℕ)
h_2 : (consFixedLengthDigits hb l i ∩ consFixedLengthDigits hb l j).Nonempty
L : List ℕ
hL : L ∈ consFixedLengthDigits hb l i ∩ consFixedLengthDigits hb l j
⊢ L ∈ consFixedLengthDigits hb l i ∧ L ∈ consFixedLengthDigits hb l j

Tactic:
rw [Finset.mem_inter] at hL

Premises used: Finset.mem_inter
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l i : ℕ
h : i ∈ (↑(Finset.range b) : Set ℕ)
j : ℕ
h_1 : j ∈ (↑(Finset.range b) : Set ℕ)
h_2 : (consFixedLengthDigits hb l i ∩ consFixedLengthDigits hb l j).Nonempty
L : List ℕ
hL : L ∈ consFixedLengthDigits hb l i ∧ L ∈ consFixedLengthDigits hb l j
⊢ i = j

Tactic:
(consFixedLengthDigits_head hb hL.1).symm.trans (consFixedLengthDigits_head hb hL.2)

Premises used: List.consFixedLengthDigits_head, And.right, And.left, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l i : ℕ
h : i ∈ (↑(Finset.range b) : Set ℕ)
j : ℕ
h_1 : j ∈ (↑(Finset.range b) : Set ℕ)
h_2 : (consFixedLengthDigits hb l i ∩ consFixedLengthDigits hb l j).Nonempty
L : List ℕ
hL : L ∈ consFixedLengthDigits hb l i ∧ L ∈ consFixedLengthDigits hb l j
⊢ i = j

Tactic:
exact (consFixedLengthDigits_head hb hL.1).symm.trans (consFixedLengthDigits_head hb hL.2)

Premises used: List.consFixedLengthDigits_head, And.right, And.left, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
h : ∀ (L : List ℕ), L ∈ fixedLengthDigits hb (l + 1) ↔ L ∈ (Finset.range b).disjiUnion (consFixedLengthDigits hb l) ⋯
⊢ fixedLengthDigits hb (l + 1) = (Finset.range b).disjiUnion (consFixedLengthDigits hb l) ⋯

Tactic:
ext L
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
h : L ∈ fixedLengthDigits hb (l + 1) ↔ ∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L
⊢ L ∈ fixedLengthDigits hb (l + 1) ↔ L ∈ (Finset.range b).disjiUnion (consFixedLengthDigits hb l) ⋯

Tactic:
simp_rw [Finset.disjiUnion_eq_biUnion, Finset.mem_biUnion, Finset.mem_range,
    consFixedLengthDigits, Finset.mem_image]

Premises used: Finset.disjiUnion_eq_biUnion, Finset.mem_image, Finset.mem_range, List.consFixedLengthDigits, Finset.mem_biUnion
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
⊢ L ∈ fixedLengthDigits hb (l + 1) ↔ ∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L

Tactic:
⟨fun hL ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
h : ∀ (hL : L ∈ fixedLengthDigits hb (l + 1)), ∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L
h₁ : (∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L) → L ∈ fixedLengthDigits hb (l + 1)
⊢ L ∈ fixedLengthDigits hb (l + 1) ↔ ∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L

Tactic:
refine ⟨fun hL ↦ ?_, ?_⟩
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb (l + 1)
⊢ L.length = l + 1

Tactic:
have hL₁ : L.length = l + 1 := ((mem_fixedLengthDigits_iff hb).mp hL).1
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb (l + 1)
hL₁ : L.length = l + 1
⊢ ∀ x ∈ L, x < b

Tactic:
have hL₂ : ∀ x ∈ L, x < b := ((mem_fixedLengthDigits_iff hb).mp hL).2
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb (l + 1)
hL₁ : L.length = l + 1
hL₂ : ∀ x ∈ L, x < b
⊢ L ≠ []

Tactic:
simp [ne_nil_iff_length_pos, hL₁]

Premises used: List.ne_nil_iff_length_pos
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb (l + 1)
hL₁ : L.length = l + 1
hL₂ : ∀ x ∈ L, x < b
⊢ L ≠ []

Tactic:
have hL₃ : L ≠ [] := by simp [ne_nil_iff_length_pos, hL₁]
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb (l + 1)
hL₁ : L.length = l + 1
hL₂ : ∀ x ∈ L, x < b
hL₃ : L ≠ []
⊢ ∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L

Tactic:
⟨L.head hL₃, hL₂ _ (L.head_mem hL₃), L.tail, ?_, cons_head_tail hL₃⟩

Premises used: List.head, List.cons_head_tail, List.head_mem, List.tail, And.intro, Exists.intro
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb (l + 1)
hL₁ : L.length = l + 1
hL₂ : ∀ x ∈ L, x < b
hL₃ : L ≠ []
h : L.tail ∈ fixedLengthDigits hb l
⊢ ∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L

Tactic:
refine ⟨L.head hL₃, hL₂ _ (L.head_mem hL₃), L.tail, ?_, cons_head_tail hL₃⟩
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb (l + 1)
hL₁ : L.length = l + 1
hL₂ : ∀ x ∈ L, x < b
hL₃ : L ≠ []
⊢ L.tail ∈ fixedLengthDigits hb l

Tactic:
(mem_fixedLengthDigits_iff hb).mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, And.intro, List.mem_fixedLengthDigits_iff
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb (l + 1)
hL₁ : L.length = l + 1
hL₂ : ∀ x ∈ L, x < b
hL₃ : L ≠ []
h : L.tail.length = l
h₁ : ∀ x ∈ L.tail, x < b
⊢ L.tail ∈ fixedLengthDigits hb l

Tactic:
refine (mem_fixedLengthDigits_iff hb).mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, And.intro, List.mem_fixedLengthDigits_iff
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb (l + 1)
hL₁ : L.length = l + 1
hL₂ : ∀ x ∈ L, x < b
hL₃ : L ≠ []
h : L.length - 1 = l
h₁ : l + 1 - 1 = l
h₂ h₃ : l = l
⊢ L.tail.length = l

Tactic:
rw [length_tail, hL₁, Nat.add_sub_cancel_right]

Premises used: Nat.add_sub_cancel_right, List.length_tail
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb (l + 1)
hL₁ : L.length = l + 1
hL₂ : ∀ x ∈ L, x < b
hL₃ : L ≠ []
⊢ ∀ x ∈ L.tail, x < b

Tactic:
fun x hx ↦ hL₂ _ <| mem_of_mem_tail hx

Premises used: List.mem_of_mem_tail
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb (l + 1)
hL₁ : L.length = l + 1
hL₂ : ∀ x ∈ L, x < b
hL₃ : L ≠ []
⊢ ∀ x ∈ L.tail, x < b

Tactic:
exact fun x hx ↦ hL₂ _ <| mem_of_mem_tail hx

Premises used: List.mem_of_mem_tail
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l d : ℕ
hd₁ : d < b
T : List ℕ
hT : T ∈ fixedLengthDigits hb l
⊢ d :: T ∈ fixedLengthDigits hb (l + 1)

Tactic:
cons_mem_fixedLengthDigits_succ hb l d hd₁ hT

Premises used: List.cons_mem_fixedLengthDigits_succ
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l d : ℕ
hd₁ : d < b
T : List ℕ
hT : T ∈ fixedLengthDigits hb l
⊢ d :: T ∈ fixedLengthDigits hb (l + 1)

Tactic:
exact cons_mem_fixedLengthDigits_succ hb l d hd₁ hT

Premises used: List.cons_mem_fixedLengthDigits_succ
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
⊢ ∑ L ∈ fixedLengthDigits hb 0, L.sum = 0 * b ^ HSub.hSub (α := ℕ) 0 1 * b.choose 2

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
pos : ∀ (hl : l = 0), ∑ L ∈ fixedLengthDigits hb (l + 1), L.sum = (l + 1) * b ^ (l + 1 - 1) * b.choose 2
neg : ∀ (hl : ¬l = 0), ∑ L ∈ fixedLengthDigits hb (l + 1), L.sum = (l + 1) * b ^ (l + 1 - 1) * b.choose 2
⊢ ∑ L ∈ fixedLengthDigits hb (l + 1), L.sum = (l + 1) * b ^ (l + 1 - 1) * b.choose 2

Tactic:
by_cases hl : l = 0
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : l = 0
⊢ ∑ L ∈ fixedLengthDigits hb (l + 1), L.sum = (l + 1) * b ^ (l + 1 - 1) * b.choose 2

Tactic:
simp [hl, fixedLengthDigits_one, Finset.sum_range_id, choose_two_right]

Premises used: List.fixedLengthDigits_one, Nat.choose_two_right, Finset.sum_range_id
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
neg : ∑ i ∈ Finset.range b, ∑ x ∈ consFixedLengthDigits hb l i, x.sum = (l + 1) * b ^ (l + 1 - 1) * b.choose 2
⊢ ∑ L ∈ fixedLengthDigits hb (l + 1), L.sum = (l + 1) * b ^ (l + 1 - 1) * b.choose 2

Tactic:
rw [fixedLengthDigits_succ_eq_disjiUnion, Finset.sum_disjiUnion]

Premises used: List.fixedLengthDigits_succ_eq_disjiUnion, Finset.sum_disjiUnion
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
neg : ∑ x ∈ Finset.range b, ∑ x_1 ∈ fixedLengthDigits hb l, (x + x_1.sum) = (l + 1) * b ^ (l + 1 - 1) * b.choose 2
⊢ ∑ i ∈ Finset.range b, ∑ x ∈ consFixedLengthDigits hb l i, x.sum = (l + 1) * b ^ (l + 1 - 1) * b.choose 2

Tactic:
simp only [consFixedLengthDigits, cons.injEq, true_and, implies_true, Set.injOn_of_eq_iff_eq,
        Finset.sum_image, sum_cons]

Premises used: Set.injOn_of_eq_iff_eq, List.cons.injEq, List.sum_cons, List.consFixedLengthDigits, Finset.sum_image, implies_true, true_and
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
neg : ∑ y ∈ fixedLengthDigits hb l, ∑ x ∈ Finset.range b, (x + y.sum) = (l + 1) * b ^ (l + 1 - 1) * b.choose 2
⊢ ∑ x ∈ Finset.range b, ∑ x_1 ∈ fixedLengthDigits hb l, (x + x_1.sum) = (l + 1) * b ^ (l + 1 - 1) * b.choose 2

Tactic:
rw [Finset.sum_comm]

Premises used: Finset.sum_comm
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
neg : b ^ l * (b * (b - 1) / 2) + b * (l * b ^ (l - 1) * (b * (b - 1) / 2)) = (l + 1) * b ^ l * (b * (b - 1) / 2)
⊢ ∑ y ∈ fixedLengthDigits hb l, ∑ x ∈ Finset.range b, (x + y.sum) = (l + 1) * b ^ (l + 1 - 1) * b.choose 2

Tactic:
simp_rw [Finset.sum_add_distrib, Finset.sum_const, Finset.sum_nsmul, Finset.sum_range_id, hr,
        nsmul_eq_mul, Finset.card_range, add_tsub_cancel_right, cast_id, card_fixedLengthDigits,
        choose_two_right]

Premises used: Finset.sum_nsmul, List.card_fixedLengthDigits, Nat.cast_id, Finset.sum_add_distrib, Nat.choose_two_right, Finset.card_range, nsmul_eq_mul, Finset.sum_range_id, add_tsub_cancel_right, Finset.sum_const
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
rw : b ^ l = b ^ (l - 1).succ
rw₁ : b ^ l = b ^ l.pred.succ
rw₂ rw₃ : b ^ l = b ^ l
⊢ b ^ l = b * b ^ (l - 1)

Tactic:
rw [← Nat.pow_succ', Nat.sub_one, Nat.succ_pred hl]

Premises used: Nat.pow_succ', Nat.succ_pred, Nat.sub_one
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
neg :
  b * b ^ (l - 1) * (b * (b - 1) / 2) + b * (l * b ^ (l - 1) * (b * (b - 1) / 2)) =
    (l + 1) * (b * b ^ (l - 1)) * (b * (b - 1) / 2)
⊢ b ^ l * (b * (b - 1) / 2) + b * (l * b ^ (l - 1) * (b * (b - 1) / 2)) = (l + 1) * b ^ l * (b * (b - 1) / 2)

Tactic:
rw [show b ^ l = b * b ^ (l - 1) by rw [← Nat.pow_succ', Nat.sub_one, Nat.succ_pred hl]]
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ b * b ^ (l - 1) * (b * (b - 1) / 2) + b * (l * b ^ (l - 1) * (b * (b - 1) / 2)) =
    (l + 1) * (b * b ^ (l - 1)) * (b * (b - 1) / 2)

Tactic:
ring
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
zero : ∑ L ∈ fixedLengthDigits hb 0, L.sum = 0 * b ^ HSub.hSub (α := ℕ) 0 1 * b.choose 2
succ :
  ∀ (l : ℕ) (hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2),
    ∑ L ∈ fixedLengthDigits hb (l + 1), L.sum = (l + 1) * b ^ (l + 1 - 1) * b.choose 2
⊢ ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2

Tactic:
induction l with
  | zero => simp
  | succ l hr =>
      by_cases hl : l = 0
      · simp [hl, fixedLengthDigits_one, Finset.sum_range_id, choose_two_right]
      rw [fixedLengthDigits_succ_eq_disjiUnion, Finset.sum_disjiUnion]
      simp only [consFixedLengthDigits, cons.injEq, true_and, implies_true, Set.injOn_of_eq_iff_eq,
        Finset.sum_image, sum_cons]
      rw [Finset.sum_comm]
      simp_rw [Finset.sum_add_distrib, Finset.sum_const, Finset.sum_nsmul, Finset.sum_range_id, hr,
        nsmul_eq_mul, Finset.card_range, add_tsub_cancel_right, cast_id, card_fixedLengthDigits,
        choose_two_right]
      rw [show b ^ l = b * b ^ (l - 1) by rw [← Nat.pow_succ', Nat.sub_one, Nat.succ_pred hl]]
      ring

Premises used: Finset.sum_nsmul, List.card_fixedLengthDigits, Nat.cast_id, Finset.sum_add_distrib, List.fixedLengthDigits_succ_eq_disjiUnion, List.fixedLengthDigits_one, Nat.choose_two_right, Finset.card_range, Set.injOn_of_eq_iff_eq, List.cons.injEq, List.sum_cons, nsmul_eq_mul, List.consFixedLengthDigits, Nat.zero, Finset.sum_image, Finset.sum_range_id, implies_true, add_tsub_cancel_right, Finset.sum_comm, Nat.succ, Finset.sum_disjiUnion, true_and, Finset.sum_const
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
rw : Eq (α := ℕ) (∑ x ∈ Finset.range (b ^ l), (b.digits x).sum) (∑ L ∈ List.fixedLengthDigits hb l, L.sum)
⊢ ∑ x ∈ Finset.range (b ^ l), (b.digits x).sum = l * b ^ (l - 1) * b.choose 2

Tactic:
rw [← List.sum_fixedLengthDigits_sum hb]

Premises used: List.sum_fixedLengthDigits_sum
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
⊢ ∀ a ∈ List.fixedLengthDigits hb l, ofDigits b a ∈ Finset.range (b ^ l)

Tactic:
(bijOn_ofDigits' hb l).1

Premises used: Nat.bijOn_ofDigits', And.left, Set.MapsTo
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
⊢ ∀ a ∈ List.fixedLengthDigits hb l, ofDigits b a ∈ Finset.range (b ^ l)

Tactic:
exact (bijOn_ofDigits' hb l).1

Premises used: Nat.bijOn_ofDigits', And.left
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
refine : ∀ (L : List ℕ) (hL : L ∈ List.fixedLengthDigits hb l), L.sum = (b.digits (ofDigits b L)).sum
⊢ Eq (α := ℕ) (∑ x ∈ Finset.range (b ^ l), (b.digits x).sum) (∑ L ∈ List.fixedLengthDigits hb l, L.sum)

Tactic:
refine (Finset.sum_nbij (ofDigits b) (by exact (bijOn_ofDigits' hb l).1)
    (bijOn_ofDigits' hb l).2.1 (bijOn_ofDigits' hb l).2.2 fun L hL ↦ ?_).symm

Premises used: Finset.sum_nbij, Nat.ofDigits, Nat.bijOn_ofDigits', And.right, And.left, Eq.symm
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ List.fixedLengthDigits hb l
rw rw₁ : L.sum = L.sum
⊢ L.sum = (b.digits (ofDigits b L)).sum

Tactic:
rw [sum_digits_ofDigits_eq_sum hb ((List.mem_fixedLengthDigits_iff hb).mp hL)]

Premises used: Nat.sum_digits_ofDigits_eq_sum, Iff.mp, List.mem_fixedLengthDigits_iff
-- Module: Mathlib.Data.Nat.Dist
Goal:
n m : ℕ
⊢ n.dist m = m.dist n

Tactic:
simp [dist, add_comm]

Premises used: Nat.dist, add_comm
-- Module: Mathlib.Data.Nat.Dist
Goal:
n : ℕ
⊢ n.dist n = 0

Tactic:
simp [dist, tsub_self]

Premises used: Nat.dist, tsub_self
-- Module: Mathlib.Data.Nat.Dist
Goal:
n m : ℕ
h : n - m + (m - n) = 0
⊢ n = m

Tactic:
lia
-- Module: Mathlib.Data.Nat.Dist
Goal:
n m : ℕ
h : n = m
⊢ n - m + (m - n) = 0

Tactic:
lia
-- Module: Mathlib.Data.Nat.Dist
Goal:
n m : ℕ
h : n ≤ m
⊢ n - m + (m - n) = m - n

Tactic:
lia
-- Module: Mathlib.Data.Nat.Dist
Goal:
n m : ℕ
h : m ≤ n
⊢ n - m + (m - n) = n - m

Tactic:
lia
-- Module: Mathlib.Data.Nat.Dist
Goal:
n m : ℕ
⊢ m ≤ n - m + (m - n) + n

Tactic:
lia
-- Module: Mathlib.Data.Nat.Dist
Goal:
n m : ℕ
⊢ m ≤ n + (n - m + (m - n))

Tactic:
lia
-- Module: Mathlib.Data.Nat.Dist
Goal:
n m : ℕ
⊢ n ≤ n - m + (m - n) + m

Tactic:
lia
-- Module: Mathlib.Data.Nat.Dist
Goal:
n m : ℕ
⊢ n ≤ m + (n - m + (m - n))

Tactic:
lia
-- Module: Mathlib.Data.Nat.Dist
Goal:
n : ℕ
⊢ n - 0 + (0 - n) = n

Tactic:
lia
-- Module: Mathlib.Data.Nat.Dist
Goal:
n : ℕ
⊢ 0 - n + (n - 0) = n

Tactic:
lia
-- Module: Mathlib.Data.Nat.Dist
Goal:
n k m : ℕ
⊢ n + k - (m + k) + (m + k - (n + k)) = n - m + (m - n)

Tactic:
lia
-- Module: Mathlib.Data.Nat.Dist
Goal:
k n m : ℕ
⊢ k + n - (k + m) + (k + m - (k + n)) = n - m + (m - n)

Tactic:
lia
-- Module: Mathlib.Data.Nat.Dist
Goal:
n m k l : ℕ
h : n + m = k + l
⊢ n - k + (k - n) = l - m + (m - l)

Tactic:
lia
-- Module: Mathlib.Data.Nat.Dist
Goal:
n m k : ℕ
⊢ n - k + (k - n) ≤ n - m + (m - n) + (m - k + (k - m))

Tactic:
lia
-- Module: Mathlib.Data.Nat.Dist
Goal:
n k m : ℕ
rw : n * k - m * k + (m * k - n * k) = n.dist m * k
rw₁ : n * k - m * k + (m * k - n * k) = (n - m + (m - n)) * k
rw₂ : n * k - m * k + (m * k - n * k) = (n - m) * k + (m - n) * k
rw₃ : n * k - m * k + (m * k - n * k) = n * k - m * k + (m - n) * k
rw₄ rw₅ : n * k - m * k + (m * k - n * k) = n * k - m * k + (m * k - n * k)
⊢ (n * k).dist (m * k) = n.dist m * k

Tactic:
rw [dist, dist, right_distrib, tsub_mul n, tsub_mul m]

Premises used: Nat.dist, right_distrib, tsub_mul
-- Module: Mathlib.Data.Nat.Dist
Goal:
k n m : ℕ
rw : (n * k).dist (k * m) = k * n.dist m
rw₁ : (n * k).dist (m * k) = k * n.dist m
rw₂ : n.dist m * k = k * n.dist m
rw₃ rw₄ : k * n.dist m = k * n.dist m
⊢ (k * n).dist (k * m) = k * n.dist m

Tactic:
rw [mul_comm k n, mul_comm k m, dist_mul_right, mul_comm]

Premises used: mul_comm, Nat.dist_mul_right
-- Module: Mathlib.Data.Nat.Dist
Goal:
i j : ℕ
inl : i ≤ j → i.dist j = max i j - min i j
inr : j ≤ i → i.dist j = max i j - min i j
⊢ i.dist j = max i j - min i j

Tactic:
cases le_total i j

Premises used: le_total
-- Module: Mathlib.Data.Nat.Dist
Goal:
i j : ℕ
h : i ≤ j
⊢ i.dist j = max i j - min i j

Tactic:
simp [Nat.dist, *]

Premises used: Nat.dist
-- Module: Mathlib.Data.Nat.Dist
Goal:
i j : ℕ
h : j ≤ i
⊢ i.dist j = max i j - min i j

Tactic:
simp [Nat.dist, *]

Premises used: Nat.dist
-- Module: Mathlib.Data.Nat.Dist
Goal:
i j : ℕ
⊢ i.succ - j.succ + (j.succ - i.succ) = i - j + (j - i)

Tactic:
lia
-- Module: Mathlib.Data.Nat.Dist
Goal:
i j : ℕ
h : i ≠ j
⊢ 0 < i - j + (j - i)

Tactic:
lia
-- Module: Mathlib.Data.Nat.EvenOddRec
Goal:
P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
⊢ evenOddRec (P := fun (x : ℕ) ↦ P x) h0 h_even h_odd 0 = h0

Tactic:
binaryRec_zero _ _

Premises used: Nat.binaryRec_zero, Nat.evenOddRec
-- Module: Mathlib.Data.Nat.EvenOddRec
Goal:
P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
n : ℕ
apply :
  (match (motive := (x : Bool) → (x_1 : ℕ) → P x_1 → (fun (x : ℕ) ↦ P x) (bit x x_1)) false, 0, h0 with
      | false, i, hi => h_even i hi
      | true, i, hi => h_odd i hi) =
      h0 ∨
    (n = 0 → false = true)
⊢ evenOddRec (P := fun (x : ℕ) ↦ P x) h0 h_even h_odd (2 * n) =
    h_even n (evenOddRec (P := fun (x : ℕ) ↦ P x) h0 h_even h_odd n)

Tactic:
apply binaryRec_eq false n

Premises used: Bool.false, Nat.binaryRec_eq
-- Module: Mathlib.Data.Nat.EvenOddRec
Goal:
P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
n : ℕ
⊢ (match (motive := (x : Bool) → (x_1 : ℕ) → P x_1 → (fun (x : ℕ) ↦ P x) (bit x x_1)) false, 0, h0 with
      | false, i, hi => h_even i hi
      | true, i, hi => h_odd i hi) =
      h0 ∨
    (n = 0 → false = true)

Tactic:
simp [H]
-- Module: Mathlib.Data.Nat.EvenOddRec
Goal:
P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
n : ℕ
apply :
  (match (motive := (x : Bool) → (x_1 : ℕ) → P x_1 → (fun (x : ℕ) ↦ P x) (bit x x_1)) false, 0, h0 with
      | false, i, hi => h_even i hi
      | true, i, hi => h_odd i hi) =
      h0 ∨
    (n = 0 → true = true)
⊢ evenOddRec (P := fun (x : ℕ) ↦ P x) h0 h_even h_odd (2 * n + 1) =
    h_odd n (evenOddRec (P := fun (x : ℕ) ↦ P x) h0 h_even h_odd n)

Tactic:
apply binaryRec_eq true n

Premises used: Bool.true, Nat.binaryRec_eq
-- Module: Mathlib.Data.Nat.EvenOddRec
Goal:
P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
n : ℕ
⊢ (match (motive := (x : Bool) → (x_1 : ℕ) → P x_1 → (fun (x : ℕ) ↦ P x) (bit x x_1)) false, 0, h0 with
      | false, i, hi => h_even i hi
      | true, i, hi => h_odd i hi) =
      h0 ∨
    (n = 0 → true = true)

Tactic:
simp [H]
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
⊢ 0! = 1

Tactic:
rfl

Premises used: Nat.factorial, rfl
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
⊢ (n + 1)! = (n + 1) * n !

Tactic:
rfl

Premises used: Nat.factorial, rfl
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
⊢ 1! = 1

Tactic:
rfl

Premises used: Nat.factorial, rfl
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
⊢ 2! = 2

Tactic:
rfl

Premises used: Nat.factorial, rfl
-- Module: Mathlib.Data.Nat.Factorial.Basic
Goal:
n : ℕ
hn : n ≠ 0
⊢ n * (n - 1)! = n !

Tactic:
Nat.sub_add_cancel (one_le_iff_ne_zero.mpr hn) ▸ rfl

Premises used: Iff.mpr, Eq.rec, Nat.sub_add_cancel, Nat.one_le_iff_ne_zero, rfl