refine ⟨M.fundCocct e B, fundCocct_cocircuit (hIB heI) hB, ?_⟩
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
⊢ ∃ K, M.Cocircuit K ∧ K ∩ 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 = {e}