Theorem: PartialEquiv.symm_image_isImage_of_subset_target (Matroid/ForMathlib/PartialEquiv.lean)

State before:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set β
h : s ⊆ e.target
⊢ e.IsImage (↑e.symm '' s) s
Tactic:
simpa using e.symm.image_isImage_of_subset_source (s := s) (by simpa)
State after:
no goals

State before:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set β
h : s ⊆ e.target
⊢ s ⊆ e.symm.source
Tactic:
simpa
State after:
no goals