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

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

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