exact ⟨fun h ↦ h _ (hI.fundCct_circuit he) (fundCct_subset_insert _ _),
  fun h C hC hCeI ↦ by 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
⊢ (∀ (C : Set α), M.Circuit C → C ⊆ insert e I → f ∈ C) ↔ f ∈ M.fundCct e I
no goals