Theorem: Matroid.cl_range_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)
⊢ M.cl (range φ) = M.cl X
Tactic:
simpa using M.cl_iUnion_congr (fun e ↦ {φ e}) (fun e ↦ {e.1}) (fun e ↦ (h_para e).cl_eq_cl.symm)
State after:
no goals