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

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D : Set α
φ : α → α
h_para : ∀ (e : α), M.Parallel' e (φ e)
X : Set α
⊢ M.cl (φ '' X) = M.cl X
Tactic:
rw [← cl_range_of_forall_parallel'_subtype (fun x : X ↦ φ x) (fun x ↦ h_para x), image_eq_range]
State after:
no goals