rwa [hC.eq_fundCct_of_subset_insert_indep hI hCeI]
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hI : M.Indep I
he : e ∈ M.cl I \ I
h : f ∈ M.fundCct e I
C : Set α
hC : M.Circuit C
hCeI : C ⊆ insert e I
⊢ f ∈ C
no goals