exact fun _ _ ↦ ⟨fun h ↦ M.subset_cl _ (union_subset (h.trans (M.cl_subset_ground _)) hC),
  fun h ↦ subset_union_left.trans h⟩
α : 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 : α
hC : autoParam (C ⊆ M.E) _auto✝
⊢ Disjoint F C → M.cl (F ∪ C) ⊆ F ∪ C → (F ⊆ M.cl (F ∪ C) ↔ F ∪ C ⊆ M.cl (F ∪ C))
no goals