exact subset_iUnion_of_subset x diff_subset
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝¹ y : α
ι : Type u_2
hC : M.Circuit C
x✝ : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x✝ i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x✝ i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x✝)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x✝)
hYE : Y ⊆ M.E
h₁ : range x✝ ⊆ M.cl (⋃ i, (Cs i \ {x✝ i}) \ insert z (range x✝))
x : ι
⊢ Cs x \ {x✝ x} ⊆ ⋃ x, Cs x
no goals