rw [fundCct, ← union_singleton, union_eq_right]
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ I
⊢ M.fundCct e I = {e}
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ I
⊢ I ∩ ⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} ⊆ {e}