Theorem: image_interior (Sard/ObsoleteHelpers.lean)

State before:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
e : PartialHomeomorph α β
s : Set α
⊢ e.target ∩ ↑e '' interior s = ↑e '' (e.source ∩ interior s)
Tactic:
sorry
State after:
no goals