refine hK.ssubset_indep <| (union_subset hI.1.1 hC.subset).ssubset_of_ne ?_
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K C C₁ C₂ : Set α
hK : M.Circuit K
hC : C ⊂ K
hCi : M.Indep C
I : Set α
hI : (I ⊆ K ∧ Disjoint I C) ∧ ¬K ⊆ I ∪ C
⊢ M.Indep (I ∪ C)
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K C C₁ C₂ : Set α
hK : M.Circuit K
hC : C ⊂ K
hCi : M.Indep C
I : Set α
hI : (I ⊆ K ∧ Disjoint I C) ∧ ¬K ⊆ I ∪ C
⊢ I ∪ C ≠ K