obtain hdj | hndj := em (Disjoint I (M₁.cl ∅))
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
⊢ M₁.Indep (I \ M₁✶.cl ∅) ↔ M₂.Indep (I \ M₁✶.cl ∅)
case inl
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hdj : Disjoint I (M₁.cl ∅)
⊢ M₁.Indep (I \ M₁✶.cl ∅) ↔ M₂.Indep (I \ M₁✶.cl ∅)

case inr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I (M₁.cl ∅)
⊢ M₁.Indep (I \ M₁✶.cl ∅) ↔ M₂.Indep (I \ M₁✶.cl ∅)