rw [diff_subset_iff, singleton_union, union_subset_iff, and_iff_right hCI]
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}
⊢ (C ∪ M.fundCct e I) \ {e} ⊆ I
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}
⊢ M.fundCct e I ⊆ insert e I