convert on_prop h
α : 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
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)