intros y h₄
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
leqthan : n ≤ m
l₅ : x ∈ fam m
⊢ ↑(insert x fs) ⊆ fam m
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
x : α
fs : Finset α
a✝ : ¬x ∈ fs
h₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fs ⊆ fam n
h₄✝ : ↑(insert x fs) ⊆ { x | ∃ n, x ∈ fam n }
l₁ : x ∈ { x | ∃ n, x ∈ fam n }
n : β
l₂ : x ∈ fam n
l₃ : ↑fs ⊆ { x | ∃ n, x ∈ fam n }
m : β
l₄ : ↑fs ⊆ fam m
leqthan : n ≤ m
l₅ : x ∈ fam m
y : α
h₄ : y ∈ ↑(insert x fs)
⊢ y ∈ fam m