apply @Finset.induction_on α (λfs => ↑fs ⊆ {x : α | ∃n : β, x ∈ fam n } → ∃n : β, ↑fs ⊆ fam n) instDec fin
α : 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
case empty
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
⊢ ↑∅ ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑∅ ⊆ fam n

case insert
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    ¬a ∈ s →
      (↑s ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑s ⊆ fam n) →
        ↑(insert a s) ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑(insert a s) ⊆ fam n