no goals
α : Type u_1
β : Type u_2
γ : Type ?u.115242
δ : Type ?u.115245
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
e : LocalHomeomorph α β
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
⊢ (subtypeRestr e s).toLocalEquiv.source = Subtype.val ⁻¹' e.source
simp only [subtypeRestr_def, mfld_simps]