intros h₁
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
⊢ Monotone fam → ↑fin ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fin ⊆ fam n
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
⊢ ↑fin ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fin ⊆ fam n