exact hf.2 rfl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
f✝ x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
f : α
he : f ∈ B₁ \ B₂
he₁ : f ∈ M.cl B₂ \ B₂
h : ∀ f_1 ∈ B₂ \ B₁, f_1 ∈ M.fundCct f B₂ → ¬M.Indep (insert f_1 B₁ \ {f})
hC : M.Circuit (M.fundCct f B₂)
hCss : M.fundCct f B₂ \ {f} ⊆ B₂
hf : f ∈ M.fundCct f B₂ \ {f}
⊢ False
no goals