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

State before:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
h : s ⊆ e.source
⊢ e.IsImage s (↑e '' s)
Tactic:
apply PartialEquiv.IsImage.of_image_eq
State after:
case h
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
h : s ⊆ e.source
⊢ ↑e '' (e.source ∩ s) = e.target ∩ ↑e '' s

State before:
case h
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
h : s ⊆ e.source
⊢ ↑e '' (e.source ∩ s) = e.target ∩ ↑e '' s
Tactic:
rw [inter_eq_self_of_subset_right h, eq_comm, inter_eq_right]
State after:
case h
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
h : s ⊆ e.source
⊢ ↑e '' s ⊆ e.target

State before:
case h
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
h : s ⊆ e.source
⊢ ↑e '' s ⊆ e.target
Tactic:
exact image_subset_target e h
State after:
no goals