Lean4
/-- Restrict an open partial homeomorphism to the subsets of the source and target
that consist of points `x ∈ f.source`, `y = f x ∈ f.target`
such that `f` is `C^n` at `x` and `f.symm` is `C^n` at `y`.
Note that `n` is a natural number or `ω`, but not `∞`,
because the set of points of `C^∞`-smoothness of `f` is not guaranteed to be open. -/
@[simps! apply symm_apply source target]
def restrContDiff (f : OpenPartialHomeomorph E F) (n : WithTop ℕ∞) (hn : n ≠ ∞) : OpenPartialHomeomorph E F :=
haveI H :
f.IsImage {x | ContDiffAt 𝕜 n f x ∧ ContDiffAt 𝕜 n f.symm (f x)}
{y | ContDiffAt 𝕜 n f.symm y ∧ ContDiffAt 𝕜 n f (f.symm y)} :=
fun x hx ↦ by simp [hx, and_comm]
H.restr <|
isOpen_iff_mem_nhds.2 fun _ ⟨hxs, hxf, hxf'⟩ ↦
inter_mem (f.open_source.mem_nhds hxs) <| (hxf.eventually hn).and <| f.continuousAt hxs (hxf'.eventually hn)
