convert M.cl_insert_cl_eq_cl_insert e (X \ {e}) using 1
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
h : e ∈ M.cl (X \ {e})
h' : e ∈ X
⊢ M.cl (X \ {e}) = M.cl X
case h.e'_2
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
h : e ∈ M.cl (X \ {e})
h' : e ∈ X
⊢ M.cl (X \ {e}) = M.cl (insert e (M.cl (X \ {e})))

case h.e'_3
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
h : e ∈ M.cl (X \ {e})
h' : e ∈ X
⊢ M.cl X = M.cl (insert e (X \ {e}))