refine subset_antisymm ?_ (singleton_subset_iff.2 ⟨M.mem_fundCocct _ _, he⟩)
α : 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
⊢ fundCocct e B ∩ B ⊆ {e}