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

State before:
α : Type u_1
inst✝ : Finite α
n : ℕ
⊢ {l | l.length < n}.Finite
Tactic:
convert (Finset.range n).finite_toSet.biUnion fun i _ ↦ finite_length_eq α i
State after:
case h.e'_2
α : Type u_1
inst✝ : Finite α
n : ℕ
⊢ {l | l.length < n} = ⋃ i ∈ ↑(Finset.range n), {l | l.length = i}

State before:
case h.e'_2
α : Type u_1
inst✝ : Finite α
n : ℕ
⊢ {l | l.length < n} = ⋃ i ∈ ↑(Finset.range n), {l | l.length = i}
Tactic:
ext
State after:
case h.e'_2.h
α : Type u_1
inst✝ : Finite α
n : ℕ
x✝ : List α
⊢ x✝ ∈ {l | l.length < n} ↔ x✝ ∈ ⋃ i ∈ ↑(Finset.range n), {l | l.length = i}

State before:
case h.e'_2.h
α : Type u_1
inst✝ : Finite α
n : ℕ
x✝ : List α
⊢ x✝ ∈ {l | l.length < n} ↔ x✝ ∈ ⋃ i ∈ ↑(Finset.range n), {l | l.length = i}
Tactic:
simp
State after:
no goals