refine (inter_subset_inter_left _ (M.fundCocct_subset_insert_compl _ _)).trans ?_
α : Type u_1
M✝ : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B✝ : Set α
M : Matroid α
B : Set α
he : e ∈ B
⊢ fundCocct e B ∩ B ⊆ {e}
α : Type u_1
M✝ : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B✝ : Set α
M : Matroid α
B : Set α
he : e ∈ B
⊢ insert e (M.E \ B) ∩ B ⊆ {e}