Theorem: Matroid.sigmaDisjoint_ground_eq (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
⊢ (Matroid.sigmaDisjoint M h).E = ⋃ i, (M i).E
Tactic:
ext
State after:
case h
α : Type u_1
β : Type u_2
ι : Type u_3
M : ι → Matroid α
h : univ.PairwiseDisjoint fun i => (M i).E
x✝ : α
⊢ x✝ ∈ (Matroid.sigmaDisjoint M h).E ↔ x✝ ∈ ⋃ i, (M i).E

State before:
case h
α : Type u_1
β : Type u_2
ι : Type u_3
M : ι → Matroid α
h : univ.PairwiseDisjoint fun i => (M i).E
x✝ : α
⊢ x✝ ∈ (Matroid.sigmaDisjoint M h).E ↔ x✝ ∈ ⋃ i, (M i).E
Tactic:
simp [Matroid.sigmaDisjoint, mapEmbedding, restrictSubtype]
State after:
no goals