Theorem: PartialEquiv.IsImage.restr_eq_restr_set (Matroid/ForMathlib/PartialEquiv.lean)

State before:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
h : e.IsImage s t
⊢ h.restr = e.restr s
Tactic:
ext <;> simp
State after:
no goals