obtain ⟨Cf, hCf, hCfss⟩ := hC.elimination (hI.fundCct_circuit ⟨he,heI⟩) hne e
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
he : e ∈ M.cl I
hne : C ≠ M.fundCct e I
⊢ False
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
he : e ∈ M.cl I
hne : C ≠ M.fundCct e I
Cf : Set α
hCf : M.Circuit Cf
hCfss : Cf ⊆ (C ∪ M.fundCct e I) \ {e}
⊢ False