Theorem: Matroid.Indep.of_image_paraMap (Matroid/Parallel.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ : α → α
hI : M.Indep (φ '' I)
hφ : InjOn φ I
h_para : ∀ e ∈ I, M.Parallel' e (φ e)
⊢ M.Indep I
Tactic:
rwa [indep_iff_range_indep_of_paraMap hφ.injective (by simpa), range_restrict]
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ : α → α
hI : M.Indep (φ '' I)
hφ : InjOn φ I
h_para : ∀ e ∈ I, M.Parallel' e (φ e)
⊢ ∀ (e : ↑I), M.Parallel' (↑e) (I.restrict φ e)
Tactic:
simpa
State after:
no goals