have hCss : M.fundCct e B₂ \ {e} ⊆ B₂ := by
  rw [diff_subset_iff, singleton_union]; exact fundCct_subset_insert _ _
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
⊢ False
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
hCss : M.fundCct e B₂ \ {e} ⊆ B₂
⊢ False