obtain he' | ⟨C, hC, heC, hCss⟩ := (mem_cl_iff_mem_or_exists_circuit
  (union_subset (M.cl_subset_ground _) (hK.trans (M✶.cl_subset_ground _)))).1 he
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f : α
B L L' I X✝ Y Z F C K X : Set α
hK : K ⊆ M✶.cl ∅
e : α
he : e ∈ M.cl (M.cl X ∪ K)
⊢ e ∈ M.cl X ∪ K
case inl
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f : α
B L L' I X✝ Y Z F C K X : Set α
hK : K ⊆ M✶.cl ∅
e : α
he : e ∈ M.cl (M.cl X ∪ K)
he' : e ∈ M.cl X ∪ K
⊢ e ∈ M.cl X ∪ K

case inr.intro.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f : α
B L L' I X✝ Y Z F C✝ K X : Set α
hK : K ⊆ M✶.cl ∅
e : α
he : e ∈ M.cl (M.cl X ∪ K)
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCss : C ⊆ insert e (M.cl X ∪ K)
⊢ e ∈ M.cl X ∪ K