Theorem: Matroid.Indep.modularPair_of_union (Matroid/Modular.lean)

State before:
ι : 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 : α
hi : M.Indep (I ∪ J)
⊢ M.ModularPair I J
Tactic:
simpa only [iUnion_subset_iff, Bool.forall_bool, cond_false, subset_union_right, cond_true,
  subset_union_left, and_self, forall_true_left] using
  hi.modularFamily_of_subsets (Js := fun i ↦ bif i then I else J)
State after:
no goals