rw [← cl_inter_ground, mem_cl_iff_mem_or_exists_circuit, mem_inter_iff, iff_false_intro he,
  false_and_iff, false_or_iff]
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
he : e ∉ X
⊢ e ∈ M.cl X ↔ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
he : e ∉ X
⊢ (∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e (X ∩ M.E)) ↔ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X