awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ ofDigits b (b.digitsAppend l x) = x
have rw : ofDigits b (b.digits x ++ replicate (l - (b.digits x).length) 0) = x
Tactic: rw [digitsAppend, ofDigits_append_replicate_zero,
    ofDigits_digits]
-- 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
rw : ofDigits b (b.digits x ++ replicate (l - (b.digits x).length) 0) = x
⊢ ofDigits b (b.digitsAppend l x) = x
have rw₁ : ofDigits b (b.digits x) = x
Tactic: rw [digitsAppend, ofDigits_append_replicate_zero,
    ofDigits_digits]
-- 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
rw : ofDigits b (b.digits x ++ replicate (l - (b.digits x).length) 0) = x
rw₁ : ofDigits b (b.digits x) = x
⊢ ofDigits b (b.digitsAppend l x) = x
have rw₂ : x = x
Tactic: rw [digitsAppend, ofDigits_append_replicate_zero,
    ofDigits_digits]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
⊢ Set.InvOn (b.digitsAppend l) (ofDigits b) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} {n : ℕ | n < b ^ l}
have refine : ∀ (L : List ℕ) (hL : Membership.mem (γ := Set (List ℕ)) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} L),
  b.digitsAppend l (ofDigits b L) = L
Tactic: refine ⟨fun L hL ↦ ?_, fun _ _ ↦ by rw [digitsAppend, ofDigits_append_replicate_zero,
    ofDigits_digits]⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : Membership.mem (γ := Set (List ℕ)) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} L
⊢ ofDigits b (b.digitsAppend l (ofDigits b L)) = ofDigits b L
have rw : ofDigits b (b.digits (ofDigits b L) ++ replicate (l - (b.digits (ofDigits b L)).length) 0) = ofDigits b L
Tactic: rw [digitsAppend, ofDigits_append_replicate_zero, ofDigits_digits]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : Membership.mem (γ := Set (List ℕ)) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} L
rw : ofDigits b (b.digits (ofDigits b L) ++ replicate (l - (b.digits (ofDigits b L)).length) 0) = ofDigits b L
⊢ ofDigits b (b.digitsAppend l (ofDigits b L)) = ofDigits b L
have rw₁ : ofDigits b (b.digits (ofDigits b L)) = ofDigits b L
Tactic: rw [digitsAppend, ofDigits_append_replicate_zero, ofDigits_digits]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : Membership.mem (γ := Set (List ℕ)) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} L
rw : ofDigits b (b.digits (ofDigits b L) ++ replicate (l - (b.digits (ofDigits b L)).length) 0) = ofDigits b L
rw₁ : ofDigits b (b.digits (ofDigits b L)) = ofDigits b L
⊢ ofDigits b (b.digitsAppend l (ofDigits b L)) = ofDigits b L
have rw₂ : ofDigits b L = ofDigits b L
Tactic: rw [digitsAppend, ofDigits_append_replicate_zero, ofDigits_digits]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : Membership.mem (γ := Set (List ℕ)) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} L
⊢ b.digitsAppend l (ofDigits b L) = L
have refine_1 : (b.digitsAppend l (ofDigits b L)).length = l
Tactic: refine (injOn_ofDigits hb l) ⟨?_, ?_⟩ hL
    (by rw [digitsAppend, ofDigits_append_replicate_zero, ofDigits_digits])
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : Membership.mem (γ := Set (List ℕ)) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} L
refine_1 : (b.digitsAppend l (ofDigits b L)).length = l
⊢ b.digitsAppend l (ofDigits b L) = L
have refine_2 : ∀ x ∈ b.digitsAppend l (ofDigits b L), x < b
Tactic: refine (injOn_ofDigits hb l) ⟨?_, ?_⟩ hL
    (by rw [digitsAppend, ofDigits_append_replicate_zero, ofDigits_digits])
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : Membership.mem (γ := Set (List ℕ)) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} L
⊢ (b.digitsAppend l (ofDigits b L)).length = l
have refine_1 : l = l
Tactic: rw [length_digitsAppend hb _ (mapsTo_ofDigits hb _ hL)]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : Membership.mem (γ := Set (List ℕ)) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} L
⊢ (b.digits (ofDigits b L)).sum = L.sum
have nth_rewrite : (b.digits (ofDigits b L)).sum = (b.digitsAppend l (ofDigits b L)).sum
Tactic: nth_rewrite 2 [← (setInvOn_digitsAppend_ofDigits hb l).1 hL]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : Membership.mem (γ := Set (List ℕ)) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} L
⊢ (b.digits (ofDigits b L)).sum = (b.digitsAppend l (ofDigits b L)).sum
have rw : (b.digits (ofDigits b L)).sum = (b.digits (ofDigits b L) ++ replicate (l - (b.digits (ofDigits b L)).length) 0).sum
Tactic: rw [digitsAppend, List.sum_append_nat, List.sum_replicate, nsmul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : Membership.mem (γ := Set (List ℕ)) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} L
rw : (b.digits (ofDigits b L)).sum = (b.digits (ofDigits b L) ++ replicate (l - (b.digits (ofDigits b L)).length) 0).sum
⊢ (b.digits (ofDigits b L)).sum = (b.digitsAppend l (ofDigits b L)).sum
have rw₁ : (b.digits (ofDigits b L)).sum = (b.digits (ofDigits b L)).sum + sum (replicate (l - (b.digits (ofDigits b L)).length) 0)
Tactic: rw [digitsAppend, List.sum_append_nat, List.sum_replicate, nsmul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : Membership.mem (γ := Set (List ℕ)) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} L
rw : (b.digits (ofDigits b L)).sum = (b.digits (ofDigits b L) ++ replicate (l - (b.digits (ofDigits b L)).length) 0).sum
rw₁ :
  (b.digits (ofDigits b L)).sum =
    (b.digits (ofDigits b L)).sum + sum (replicate (l - (b.digits (ofDigits b L)).length) 0)
⊢ (b.digits (ofDigits b L)).sum = (b.digitsAppend l (ofDigits b L)).sum
have rw₂ : (b.digits (ofDigits b L)).sum =
  (b.digits (ofDigits b L)).sum + HSMul.hSMul (β := ℕ) (l - (b.digits (ofDigits b L)).length) 0
Tactic: rw [digitsAppend, List.sum_append_nat, List.sum_replicate, nsmul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : Membership.mem (γ := Set (List ℕ)) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} L
rw : (b.digits (ofDigits b L)).sum = (b.digits (ofDigits b L) ++ replicate (l - (b.digits (ofDigits b L)).length) 0).sum
rw₁ :
  (b.digits (ofDigits b L)).sum =
    (b.digits (ofDigits b L)).sum + sum (replicate (l - (b.digits (ofDigits b L)).length) 0)
rw₂ :
  (b.digits (ofDigits b L)).sum =
    (b.digits (ofDigits b L)).sum + HSMul.hSMul (β := ℕ) (l - (b.digits (ofDigits b L)).length) 0
⊢ (b.digits (ofDigits b L)).sum = (b.digitsAppend l (ofDigits b L)).sum
have rw₃ : (b.digits (ofDigits b L)).sum = (b.digits (ofDigits b L)).sum + 0
Tactic: rw [digitsAppend, List.sum_append_nat, List.sum_replicate, nsmul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : Membership.mem (γ := Set (List ℕ)) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} L
rw : (b.digits (ofDigits b L)).sum = (b.digits (ofDigits b L) ++ replicate (l - (b.digits (ofDigits b L)).length) 0).sum
rw₁ :
  (b.digits (ofDigits b L)).sum =
    (b.digits (ofDigits b L)).sum + sum (replicate (l - (b.digits (ofDigits b L)).length) 0)
rw₂ :
  (b.digits (ofDigits b L)).sum =
    (b.digits (ofDigits b L)).sum + HSMul.hSMul (β := ℕ) (l - (b.digits (ofDigits b L)).length) 0
rw₃ : (b.digits (ofDigits b L)).sum = (b.digits (ofDigits b L)).sum + 0
⊢ (b.digits (ofDigits b L)).sum = (b.digitsAppend l (ofDigits b L)).sum
have rw₄ : (b.digits (ofDigits b L)).sum = (b.digits (ofDigits b L)).sum
Tactic: rw [digitsAppend, List.sum_append_nat, List.sum_replicate, nsmul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
⊢ Finset (List ℕ)
have have : (this : Fintype (↑{L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} : Type)) → Finset (List ℕ)
Tactic: have : Fintype {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} :=
    Fintype.ofInjective (Set.MapsTo.restrict _ _ _ (mapsTo_ofDigits hb l))
      <| (Set.MapsTo.restrict_inj (mapsTo_ofDigits hb l)).mpr <| injOn_ofDigits hb l
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
⊢ Set.BijOn (ofDigits b) (↑(fixedLengthDigits hb l) : Set (List ℕ)) (↑(Finset.range (b ^ l)) : Set ℕ)
have rw : Set.BijOn (ofDigits b) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} (↑(Finset.range (b ^ l)) : Set ℕ)
Tactic: rw [fixedLengthDigits, Set.coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
⊢ Set.BijOn (ofDigits b) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} (↑(Finset.range (b ^ l)) : Set ℕ)
have h : (↑(Finset.range (b ^ l)) : Set ℕ) = {n : ℕ | n < b ^ l}
Tactic: convert! bijOn_ofDigits hb l
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
⊢ (↑(Finset.range (b ^ l)) : Set ℕ) = {n : ℕ | n < b ^ l}
have h : ∀ (x : ℕ), x ∈ (↑(Finset.range (b ^ l)) : Set ℕ) ↔ Membership.mem (γ := Set ℕ) {n : ℕ | n < b ^ l} x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
⊢ Set.BijOn (b.digitsAppend l) (↑(Finset.range (b ^ l)) : Set ℕ) (↑(fixedLengthDigits hb l) : Set (List ℕ))
have rw : Set.BijOn (b.digitsAppend l) (↑(Finset.range (b ^ l)) : Set ℕ) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b}
Tactic: rw [fixedLengthDigits, Set.coe_toFinset]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
⊢ Set.BijOn (b.digitsAppend l) (↑(Finset.range (b ^ l)) : Set ℕ) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b}
have h : (↑(Finset.range (b ^ l)) : Set ℕ) = {n : ℕ | n < b ^ l}
Tactic: convert! bijOn_digitsAppend hb l
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
⊢ fixedLengthDigits hb 0 = {[]}
have h : ∀ (a : List ℕ), a ∈ fixedLengthDigits hb 0 ↔ Membership.mem (γ := Finset (List ℕ)) {[]} a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
a : List ℕ
⊢ a ∈ fixedLengthDigits hb 0 ↔ Membership.mem (γ := Finset (List ℕ)) {[]} a
have h : a = [] → ∀ x ∈ a, x < b
Tactic: simp [fixedLengthDigits]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
⊢ fixedLengthDigits hb 1 = Finset.image (fun (x : ℕ) ↦ [x]) (Finset.range b)
have h : ∀ (a : List ℕ),
  a ∈ fixedLengthDigits hb 1 ↔
    Membership.mem (γ := Finset (List ℕ)) (Finset.image (fun (x : ℕ) ↦ [x]) (Finset.range b)) a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
a : List ℕ
⊢ a ∈ fixedLengthDigits hb 1 ↔
    Membership.mem (γ := Finset (List ℕ)) (Finset.image (fun (x : ℕ) ↦ [x]) (Finset.range b)) a
have h : ((∃ (a_1 : ℕ), a = [a_1]) ∧ ∀ x ∈ a, x < b) ↔
  Membership.mem (γ := Finset (List ℕ)) (Finset.image (fun (x : ℕ) ↦ [x]) (Finset.range b)) a
Tactic: rw [mem_fixedLengthDigits_iff, List.length_eq_one_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
⊢ (fixedLengthDigits hb l).card = b ^ l
have rw : (Finset.range (b ^ l)).card = b ^ l
Tactic: rw [Set.BijOn.finsetCard_eq (ofDigits b) (bijOn_ofDigits' hb l), Finset.card_range]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
rw : (Finset.range (b ^ l)).card = b ^ l
⊢ (fixedLengthDigits hb l).card = b ^ l
have rw₁ : b ^ l = b ^ l
Tactic: rw [Set.BijOn.finsetCard_eq (ofDigits b) (bijOn_ofDigits' hb l), Finset.card_range]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l d : ℕ
L : List ℕ
hL : L ∈ consFixedLengthDigits hb l d
⊢ L ≠ []
have obtain : ∀ w ∈ fixedLengthDigits hb l, ∀ (hL : d :: w ∈ consFixedLengthDigits hb l d), d :: w ≠ []
Tactic: obtain ⟨_, _, rfl⟩ := Finset.mem_image.mp hL
Cleared hypotheses: L, hL
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l d : ℕ
L : List ℕ
hL : L ∈ consFixedLengthDigits hb l d
⊢ L.head ⋯ = d
have obtain : ∀ w ∈ fixedLengthDigits hb l, ∀ (hL : d :: w ∈ consFixedLengthDigits hb l d), (d :: w).head sorry = d
Tactic: obtain ⟨_, _, rfl⟩ := Finset.mem_image.mp hL
Cleared hypotheses: L, hL
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l d : ℕ
w : List ℕ
left : w ∈ fixedLengthDigits hb l
hL : d :: w ∈ consFixedLengthDigits hb l d
⊢ (d :: w).head ⋯ = d
have rw : d = d
Tactic: rw [head_cons]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
⊢ d :: L ∈ fixedLengthDigits hb (l + 1)
have refine_1 : (d :: L).length = l + 1
Tactic: refine (mem_fixedLengthDigits_iff hb).mpr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
refine_1 : (d :: L).length = l + 1
⊢ d :: L ∈ fixedLengthDigits hb (l + 1)
have refine_2 : ∀ x ∈ d :: L, x < b
Tactic: refine (mem_fixedLengthDigits_iff hb).mpr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
x : ℕ
hx : x ∈ d :: L
⊢ x < b
have refine_2 : ∀ (hd : x < b) (hx : x ∈ x :: L), x < b
Tactic: obtain rfl | hx := mem_cons.mp hx
Cleared hypotheses: d, hd, hx
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
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
⊢ x < b
have refine_2₁ : ∀ (hx : x ∈ L), x < b
Tactic: obtain rfl | hx := mem_cons.mp hx
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
⊢ (↑(Finset.range b) : Set ℕ).PairwiseDisjoint (α := Finset (List ℕ)) fun (d : ℕ) ↦ consFixedLengthDigits hb l d
have 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
Tactic: refine Finset.pairwiseDisjoint_iff.mpr fun i _ j _ ⟨L, hL⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (hypothesis)
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
⊢ i = j
have hL₁ : L ∈ consFixedLengthDigits hb l i ∧ L ∈ consFixedLengthDigits hb l j
Tactic: rw [Finset.mem_inter] at hL
Cleared hypotheses: hL
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
⊢ fixedLengthDigits hb (l + 1) = (Finset.range b).disjiUnion (consFixedLengthDigits hb l) ⋯
have h : ∀ (L : List ℕ), L ∈ fixedLengthDigits hb (l + 1) ↔ L ∈ (Finset.range b).disjiUnion (consFixedLengthDigits hb l) sorry
Tactic: ext L
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
⊢ L ∈ fixedLengthDigits hb (l + 1) ↔ L ∈ (Finset.range b).disjiUnion (consFixedLengthDigits hb l) ⋯
have h : L ∈ fixedLengthDigits hb (l + 1) ↔ ∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L
Tactic: simp_rw [Finset.disjiUnion_eq_biUnion, Finset.mem_biUnion, Finset.mem_range,
    consFixedLengthDigits, Finset.mem_image]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
⊢ L ∈ fixedLengthDigits hb (l + 1) ↔ ∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L
have h : ∀ (hL : L ∈ fixedLengthDigits hb (l + 1)), ∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L
Tactic: refine ⟨fun hL ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
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
⊢ L ∈ fixedLengthDigits hb (l + 1) ↔ ∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L
have h₁ : (∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L) → L ∈ fixedLengthDigits hb (l + 1)
Tactic: refine ⟨fun hL ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (hypothesis)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb (l + 1)
⊢ ∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L
have hL₁ : L.length = l + 1
Tactic: have hL₁ : L.length = l + 1 := ((mem_fixedLengthDigits_iff hb).mp hL).1
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (hypothesis)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb (l + 1)
hL₁ : L.length = l + 1
⊢ ∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L
have hL₂ : ∀ x ∈ L, x < b
Tactic: have hL₂ : ∀ x ∈ L, x < b := ((mem_fixedLengthDigits_iff hb).mp hL).2
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (hypothesis)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb (l + 1)
hL₁ : L.length = l + 1
hL₂ : ∀ x ∈ L, x < b
⊢ ∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L
have hL₃ : L ≠ []
Tactic: have hL₃ : L ≠ [] := by simp [ne_nil_iff_length_pos, hL₁]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
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
have h : L.tail ∈ fixedLengthDigits hb l
Tactic: refine ⟨L.head hL₃, hL₂ _ (L.head_mem hL₃), L.tail, ?_, cons_head_tail hL₃⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
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
have h : L.tail.length = l
Tactic: refine (mem_fixedLengthDigits_iff hb).mpr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
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
⊢ L.tail ∈ fixedLengthDigits hb l
have h₁ : ∀ x ∈ L.tail, x < b
Tactic: refine (mem_fixedLengthDigits_iff hb).mpr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
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.length = l
have h : L.length - 1 = l
Tactic: rw [length_tail, hL₁, Nat.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
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
⊢ L.tail.length = l
have h₁ : l + 1 - 1 = l
Tactic: rw [length_tail, hL₁, Nat.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
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
⊢ L.tail.length = l
have h₂ : l = l
Tactic: rw [length_tail, hL₁, Nat.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
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
have pos : ∀ (hl : l = 0), ∑ L ∈ fixedLengthDigits hb (l + 1), L.sum = (l + 1) * b ^ (l + 1 - 1) * b.choose 2
Tactic: by_cases hl : l = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
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
⊢ ∑ L ∈ fixedLengthDigits hb (l + 1), L.sum = (l + 1) * b ^ (l + 1 - 1) * b.choose 2
have neg : ∀ (hl : ¬l = 0), ∑ L ∈ fixedLengthDigits hb (l + 1), L.sum = (l + 1) * b ^ (l + 1 - 1) * b.choose 2
Tactic: by_cases hl : l = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
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
have neg : ∑ i ∈ Finset.range b, ∑ x ∈ consFixedLengthDigits hb l i, x.sum = (l + 1) * b ^ (l + 1 - 1) * b.choose 2
Tactic: rw [fixedLengthDigits_succ_eq_disjiUnion, Finset.sum_disjiUnion]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ ∑ i ∈ Finset.range b, ∑ x ∈ consFixedLengthDigits hb l i, x.sum = (l + 1) * b ^ (l + 1 - 1) * b.choose 2
have neg : ∑ x ∈ Finset.range b, ∑ x_1 ∈ fixedLengthDigits hb l, (x + x_1.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]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ ∑ x ∈ Finset.range b, ∑ x_1 ∈ fixedLengthDigits hb l, (x + x_1.sum) = (l + 1) * b ^ (l + 1 - 1) * b.choose 2
have neg : ∑ y ∈ fixedLengthDigits hb l, ∑ x ∈ Finset.range b, (x + y.sum) = (l + 1) * b ^ (l + 1 - 1) * b.choose 2
Tactic: rw [Finset.sum_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ ∑ y ∈ fixedLengthDigits hb l, ∑ x ∈ Finset.range b, (x + y.sum) = (l + 1) * b ^ (l + 1 - 1) * b.choose 2
have neg : b ^ l * (b * (b - 1) / 2) + b * (l * b ^ (l - 1) * (b * (b - 1) / 2)) = (l + 1) * b ^ l * (b * (b - 1) / 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ b ^ l = b * b ^ (l - 1)
have rw : b ^ l = b ^ (l - 1).succ
Tactic: rw [← Nat.pow_succ', Nat.sub_one, Nat.succ_pred hl]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
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
⊢ b ^ l = b * b ^ (l - 1)
have rw₁ : b ^ l = b ^ l.pred.succ
Tactic: rw [← Nat.pow_succ', Nat.sub_one, Nat.succ_pred hl]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
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
⊢ b ^ l = b * b ^ (l - 1)
have rw₂ : b ^ l = b ^ l
Tactic: rw [← Nat.pow_succ', Nat.sub_one, Nat.succ_pred hl]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ b ^ l * (b * (b - 1) / 2) + b * (l * b ^ (l - 1) * (b * (b - 1) / 2)) = (l + 1) * b ^ l * (b * (b - 1) / 2)
have 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)
Tactic: rw [show b ^ l = b * b ^ (l - 1) by rw [← Nat.pow_succ', Nat.sub_one, Nat.succ_pred hl]]