Theorem: Matroid.Indep.covBy_cl_insert (Matroid/Flat.lean)

State before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hI : M.Indep I
he : e ∈ M.E \ M.cl I
⊢ M.cl I ⋖[M] M.cl (insert e I)
Tactic:
simpa [not_mem_of_mem_diff_cl he] using
  (hI.insert_indep_iff.2 <| .inl he).cl_diff_covBy (.inl rfl)
State after:
no goals