Theorem: Matroid.Iso.on_prop_symm (Matroid/Old/_Equiv.lean)

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
PM : Set α → Prop
PN : Set β → Prop
e : M.Iso N
on_prop : ∀ {Y : Set β}, PN Y → PM (↑e.symm.toPartialEquiv '' Y)
h : PN (↑e.toPartialEquiv '' X)
hX : autoParam (X ⊆ M.E) _auto✝
⊢ PM X
Tactic:
convert on_prop h
State after:
case h.e'_1
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
PM : Set α → Prop
PN : Set β → Prop
e : M.Iso N
on_prop : ∀ {Y : Set β}, PN Y → PM (↑e.symm.toPartialEquiv '' Y)
h : PN (↑e.toPartialEquiv '' X)
hX : autoParam (X ⊆ M.E) _auto✝
⊢ X = ↑e.symm.toPartialEquiv '' (↑e.toPartialEquiv '' X)

State before:
case h.e'_1
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
α₃ : Type u_6
M : Matroid α
N : Matroid β
B I D X Y : Set α
PM : Set α → Prop
PN : Set β → Prop
e : M.Iso N
on_prop : ∀ {Y : Set β}, PN Y → PM (↑e.symm.toPartialEquiv '' Y)
h : PN (↑e.toPartialEquiv '' X)
hX : autoParam (X ⊆ M.E) _auto✝
⊢ X = ↑e.symm.toPartialEquiv '' (↑e.toPartialEquiv '' X)
Tactic:
rw [symm_apply, symm_image_image_of_subset_source _ (e.subset_source X)]
State after:
no goals