rw [symm_apply, image_symm_image_of_subset_target _ ((hN h).trans_eq e.target_eq.symm)]
case refine'_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
hN : ∀ {Y : Set β}, PN Y → Y ⊆ N.E
hMN : ∀ {X : Set α}, PM X → PN (↑e.toPartialEquiv '' X)
hNM : ∀ {Y : Set β}, PN Y → PM (↑e.symm.toPartialEquiv '' Y)
Y : Set β
h : Y ∈ setOf PN
⊢ ↑e.toPartialEquiv '' (↑e.symm.toPartialEquiv '' Y) = Y
no goals