convert M.cl_biUnion_congr (fun e : X ↦ {φ e}) (fun e ↦ {e.1}) Y
  (fun e _ ↦ (h_para e).cl_eq_cl.symm) <;> aesop
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D X : Set α
φ : ↑X → α
h_para : ∀ (e : ↑X), M.Parallel' (↑e) (φ e)
Y : Set ↑X
⊢ M.cl (φ '' Y) = M.cl ↑Y
no goals