The image of a measurable set under a map that is continuous and injective on a closed subset of a compact space (into a Hausdorff space) is measurable.

import Definitions.Def_TypeDensity_Basic
import Definitions.Def_TypeDensity_Formula_LawAlgebra
import Mathlib.FieldTheory.RatFunc.Basic
import Mathlib.MeasureTheory.Measure.Haar.Unique
import Mathlib.NumberTheory.ArithmeticFunction.Moebius
import Mathlib.NumberTheory.Padics.PadicIntegers
import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
import Mathlib.RingTheory.MvPowerSeries.Basic
import Mathlib.RingTheory.RamificationInertia.Basic
import Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
import Mathlib.FieldTheory.Finite.GaloisField
import Mathlib.RingTheory.AdicCompletion.Algebra
import Mathlib.RingTheory.RegularLocalRing.Defs
set_option autoImplicit false

open TypeDensity
open scoped BigOperators ENNReal

theorem TypeDensity.image_measurable_of_continuousOn_injOn_compact (X Y : Type) [TopologicalSpace X]
    [CompactSpace X] [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y] [T2Space Y]
    [MeasurableSpace Y] [BorelSpace Y] (f : X → Y) (C : Set X) (hC : IsClosed C)
    (hf : ContinuousOn f C) (hinj : Set.InjOn f C) (U : Set X) (hU : MeasurableSet U) :
    MeasurableSet (f '' (U ∩ C)) := by sorry