Theorem: Set.Finite.subset_iUnion_mono_iff (Matroid/ForMathlib/Data/Set/Finite.lean)

State before:
α : Type u_1
s : Set α
ι : Type u_2
inst✝² : LE ι
inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1
inst✝ : Nonempty ι
v : ι → Set α
hs : s.Finite
hv : ∀ ⦃i j : ι⦄, i ≤ j → v i ⊆ v j
⊢ s ⊆ ⋃ i, v i ↔ ∃ i, s ⊆ v i
Tactic:
simp [← biUnion_univ, hs.subset_biUnion_mono_iff directedOn_univ univ_nonempty hv]
State after:
no goals