rw [insert_inter_of_mem (hC.subset_ground heC)]
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f x y : α
he : e ∉ X
x✝ : ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
C : Set α
hC : M.Circuit C
heC : e ∈ C
h : C ⊆ insert e X
⊢ insert e X ∩ M.E ⊆ insert e (X ∩ M.E)
no goals