rw [fundCct, inter_eq_self_of_subset_right]
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
he : e ∈ M.cl I
⊢ M.fundCct e I = insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
he : e ∈ M.cl I
⊢ ⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} ⊆ I