Theorem: Matroid.cl_image_of_forall_parallel'_subtype (Matroid/Parallel.lean)

State before:
α : 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
Tactic:
convert M.cl_biUnion_congr (fun e : X ↦ {φ e}) (fun e ↦ {e.1}) Y
  (fun e _ ↦ (h_para e).cl_eq_cl.symm) <;> aesop
State after:
no goals