rw [subset_antisymm_iff, subset_inter_iff, singleton_subset_iff, and_iff_right
  (mem_fundCocct _ _ _), singleton_subset_iff, and_iff_left heI, ← M.fundCocct_inter_eq (hIB heI)]
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B✝ : Set α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ fundCocct e B ∩ I = {e}
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B✝ : Set α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ fundCocct e B ∩ I ⊆ fundCocct e B ∩ B