Theorem: Matroid.isoOfMapParallelBijOn_apply_image (Matroid/Parallel.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D : Set α
φ : α → α
hφ : BijOn φ M.E M.E
h_para : ∀ e ∈ M.E, M.Parallel' e (φ e)
X : Set ↑M.E
⊢ ↑(⇑(isoOfMapParallelBijOn hφ h_para) '' X) = φ '' ↑X
Tactic:
suffices ∀ (x y : α) (h : y ∈ M.E), ⟨y, h⟩ ∈ X → φ y = x → x ∈ M.E by simpa [Set.ext_iff]
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D : Set α
φ : α → α
hφ : BijOn φ M.E M.E
h_para : ∀ e ∈ M.E, M.Parallel' e (φ e)
X : Set ↑M.E
⊢ ∀ (x y : α) (h : y ∈ M.E), ⟨y, h⟩ ∈ X → φ y = x → x ∈ M.E

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D : Set α
φ : α → α
hφ : BijOn φ M.E M.E
h_para : ∀ e ∈ M.E, M.Parallel' e (φ e)
X : Set ↑M.E
⊢ ∀ (x y : α) (h : y ∈ M.E), ⟨y, h⟩ ∈ X → φ y = x → x ∈ M.E
Tactic:
rintro x y h - rfl
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D : Set α
φ : α → α
hφ : BijOn φ M.E M.E
h_para : ∀ e ∈ M.E, M.Parallel' e (φ e)
X : Set ↑M.E
y : α
h : y ∈ M.E
⊢ φ y ∈ M.E

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D : Set α
φ : α → α
hφ : BijOn φ M.E M.E
h_para : ∀ e ∈ M.E, M.Parallel' e (φ e)
X : Set ↑M.E
y : α
h : y ∈ M.E
⊢ φ y ∈ M.E
Tactic:
exact (h_para y h).mem_ground_right
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D : Set α
φ : α → α
hφ : BijOn φ M.E M.E
h_para : ∀ e ∈ M.E, M.Parallel' e (φ e)
X : Set ↑M.E
this : ∀ (x y : α) (h : y ∈ M.E), ⟨y, h⟩ ∈ X → φ y = x → x ∈ M.E
⊢ ↑(⇑(isoOfMapParallelBijOn hφ h_para) '' X) = φ '' ↑X
Tactic:
simpa [Set.ext_iff]
State after:
no goals