simp [Matroid.sigmaDisjoint, h.sigmaSubtypeEmbedding_preimage]
α : Type u_1
β : Type u_2
ι : Type u_3
M : ι → Matroid α
h : univ.PairwiseDisjoint fun i => (M i).E
I : Set α
⊢ (Matroid.sigmaDisjoint M h).Indep I ↔ (∀ (i : ι), (M i).Indep (I ∩ (M i).E)) ∧ I ⊆ ⋃ i, (M i).E
no goals