simp [h, M.cl_iUnion_cl_eq_cl_iUnion]
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
ι : Type u_3
Xs Ys : ι → Set α
h : ∀ (i : ι), M.cl (Xs i) = M.cl (Ys i)
⊢ M.cl (⋃ i, M.cl (Xs i)) = M.cl (⋃ i, Ys i)
no goals