refine (M.cl_subset_cl (subset_union_left (t := C))).trans ?_
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.cl (M.E \ K ∪ {e}) ⊆ M.cl (M.E \ K)
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.cl (M.E \ K ∪ {e} ∪ C) ⊆ M.cl (M.E \ K)