Theorem: Matroid.disjointSum_ground_eq (Matroid/Constructions/DirectSum.lean)

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
M N : Matroid α
h : Disjoint M.E N.E
⊢ (M.disjointSum N h).E = M.E ∪ N.E
Tactic:
simp [disjointSum, restrictSubtype, mapEmbedding]
State after:
no goals