Theorem: Invariance of domain

Wikipedia, Zulip 1 2

import Mathlib

-- useful notation from `PoincareConjecture.lean`
local macro:max "ℝ" noWs n:superscript(term) : term => `(EuclideanSpace ℝ (Fin $(⟨n.raw[0]⟩)))

theorem invariance_of_domain {n : ℕ} (U : Set ℝⁿ) (hU : IsOpen U) (f : C(U, ℝⁿ))
    (hf : f.toFun.Injective) : IsOpenMap f := by
  sorry

-- A cool corollary (described in the Wikipedia page):
theorem Real.homeomorph_eq {m n : ℕ} (f : ℝᵐ ≃ₜ ℝⁿ) : m = n := by
  sorry

Note that this theorem does not appear on the 100 theorems list nor on the 1000 theorems list.

Start with the provided Lean declarations and read the linked Wikipedia and Zulip discussions for the intended mathematical route. Replace the sorry in invariance_of_domain with a proof that establishes the stated IsOpenMap result, then prove Real.homeomorph_eq as the stated corollary and verify both declarations compile with import Mathlib.