Theorem: Matroid.Indep.cl_iInter_eq_biInter_cl_of_forall_subset (Matroid/Closure.lean)

State before:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
ι : Type u_3
hι : Nonempty ι
Js : ι → Set α
hI : M.Indep I
hJs : ∀ (i : ι), Js i ⊆ I
⊢ ⋃ i, Js i ⊆ I
Tactic:
simpa
State after:
no goals