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

State before:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set β
hs : s ⊆ e.target
⊢ ↑e.symm '' s ⊆ e.source
Tactic:
rw [← e.symm_image_target_eq_source]
State after:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set β
hs : s ⊆ e.target
⊢ ↑e.symm '' s ⊆ ↑e.symm '' e.target

State before:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set β
hs : s ⊆ e.target
⊢ ↑e.symm '' s ⊆ ↑e.symm '' e.target
Tactic:
exact image_subset _ hs
State after:
no goals