Closure finiteness descends along a finite extension `O → Oδ`: the two integral closures coincide, and finite over `Oδ` finite over `O` is finite over `O`.

import Definitions.Def_TypeDensity_Basic
import Definitions.Def_TypeDensity_Formula_LawAlgebra
import Definitions.Def_TypeDensity_Algebra_AlgebraType
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
import Mathlib.RingTheory.Henselian
set_option autoImplicit false

open TypeDensity
open scoped TensorProduct
open Polynomial IsLocalRing

theorem TypeDensity.closure_finite_descent (O Oδ L : Type) [CommRing O] [CommRing Oδ] [Algebra O Oδ]
    [Module.Finite O Oδ] [CommRing L] [Algebra O L] [Algebra Oδ L] [IsScalarTower O Oδ L]
    (h : Module.Finite Oδ (integralClosure Oδ L)) : Module.Finite O (integralClosure O L) := by sorry