have hIR : I ⊆ R := hI.indep.subset_ground
case h.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
I : Set α
hI : (M ↾ R).Basis I (X ∩ R)
hI' : M.Basis I (X ∩ R ∩ M.E)
⊢ ¬M.Indep (insert e I) ∧ e ∈ R ∨ e ∈ I ↔ (¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E
case h.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
I : Set α
hI : (M ↾ R).Basis I (X ∩ R)
hI' : M.Basis I (X ∩ R ∩ M.E)
hIR : I ⊆ R
⊢ ¬M.Indep (insert e I) ∧ e ∈ R ∨ e ∈ I ↔ (¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E