exact fun hss ↦ (hss ((union_subset hC hD) he)).2 he
case right
α : Type u_1
M M' : Matroid α
e✝ f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
C D : Set α
hC : C ⊆ M.E
hD : D ⊆ M.E
hCD : Disjoint C D
e : α
he : e ∈ C ∪ D
⊢ ¬M.E ⊆ M.E \ (C ∪ D)
no goals