exact SkewFamily.iUnion_indep_subset_indep h (Is := fun i ↦ bif i then I else J)
  (Bool.rec (by simpa) (by simpa)) (Bool.rec (by simpa) (by simpa))
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.Skew X Y
hI : M.Indep I
hIX : I ⊆ X
hJ : M.Indep J
hJY : J ⊆ Y
⊢ M.Indep (⋃ b, bif b then I else J)
no goals