Theorem: Matroid.cl_biUnion_cl_eq_cl_sUnion (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 : α
M : Matroid α
Xs : Set (Set α)
⊢ M.cl (⋃ X ∈ Xs, M.cl X) = M.cl (⋃₀ Xs)
Tactic:
rw [sUnion_eq_iUnion, biUnion_eq_iUnion, cl_iUnion_cl_eq_cl_iUnion]
State after:
no goals