Theorem: List.finite_length_le (LeanCamCombi/Mathlib/Data/Set/Finite.lean)

State before:
α : Type u_1
inst✝ : Finite α
n : ℕ
⊢ {l | l.length ≤ n}.Finite
Tactic:
simpa [Nat.lt_succ_iff] using finite_length_lt α (n + 1)
State after:
no goals