Theorem: Matroid.Indep.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_para : ∀ e ∈ I, M.Parallel' e (φ e)
⊢ M.Indep (φ '' I)
Tactic:
convert hI.indep_range_paraMap (fun e ↦ φ e) (by simpa)
State after:
case h.e'_3
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ : α → α
hI : M.Indep I
h_para : ∀ e ∈ I, M.Parallel' e (φ e)
⊢ φ '' I = range fun e => φ ↑e

State before:
case h.e'_3
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
φ : α → α
hI : M.Indep I
h_para : ∀ e ∈ I, M.Parallel' e (φ e)
⊢ φ '' I = range fun e => φ ↑e
Tactic:
simp [Set.ext_iff]
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_para : ∀ e ∈ I, M.Parallel' e (φ e)
⊢ ∀ (e : ↑I), M.Parallel' (↑e) ((fun e => φ ↑e) e)
Tactic:
simpa
State after:
no goals