English
There is a finite type instance for the set of pairs (a,i) with a ∈ α and i < m.count a.
Русский
Существует конечный тип для множества пар (a,i) с a ∈ α и i < m.count a.
LaTeX
$$$\text{Fintype}\{ p = (a,i) ∈ \alpha \times \mathbb{N} \mid i < \mathrm{count}(a, m) \}$$$
Lean4
/-- The digits in the base b+2 expansion of n are all less than b+2 -/
theorem digits_lt_base' {b m : ℕ} : ∀ {d}, d ∈ digits (b + 2) m → d < b + 2 :=
by
induction m using Nat.strongRecOn with
| ind n IH => ?_
intro d hd
rcases n with - | n
· rw [digits_zero] at hd
cases hd
rw [digits_add_two_add_one] at hd
cases hd
· exact n.succ.mod_lt (by linarith)
· apply IH ((n + 1) / (b + 2))
· apply Nat.div_lt_self <;> omega
· assumption
