Theorem: Matroid.sigma'_indep_iff (Matroid/Constructions/DirectSum.lean)

State before:
α : 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
Tactic:
simp [Matroid.sigmaDisjoint, h.sigmaSubtypeEmbedding_preimage]
State after:
no goals