apply_fun Matroid.E at hM
case intro.intro.intro.intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K C C₁ C₂ I D : Set α
hI : M.Basis I (C ∩ M.E)
hM : M ／ C = M ／ I ＼ D
⊢ e ∈ M.cl (C ∩ M.E) \ (I ∪ D) ↔ e ∈ M.cl (C ∩ M.E) \ C
case intro.intro.intro.intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K C C₁ C₂ I D : Set α
hI : M.Basis I (C ∩ M.E)
hM : (M ／ C).E = (M ／ I ＼ D).E
⊢ e ∈ M.cl (C ∩ M.E) \ (I ∪ D) ↔ e ∈ M.cl (C ∩ M.E) \ C