The ascent step: let `O → Oδ` be finite, `K = Frac O`, and `Kδ/K` finite separable (with compatible structures).

import Definitions.Def_TypeDensity_Basic
import Definitions.Def_TypeDensity_Formula_LawAlgebra
import Definitions.Def_TypeDensity_Algebra_AlgebraType
import Theorems.Thm_TypeDensity_closure_finite_ascent
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_ascent_root (O Oδ K Kδ : Type) [CommRing O] [IsDomain O]
    [IsDiscreteValuationRing O] [CommRing Oδ] [Algebra O Oδ] [Module.Finite O Oδ]
    [Field K] [Algebra O K] [IsFractionRing O K] [Field Kδ] [Algebra K Kδ] [Algebra O Kδ]
    [Algebra Oδ Kδ] [IsScalarTower O K Kδ] [IsScalarTower O Oδ Kδ] [FiniteDimensional K Kδ]
    [Algebra.IsSeparable K Kδ] (g : K[X]) (hgm : g.Monic) (hgi : Irreducible g)
    (hfin : Module.Finite O (integralClosure O (AdjoinRoot g)))
    (h : Kδ[X]) (hhi : Irreducible h) (hdvd : h ∣ g.map (algebraMap K Kδ)) :
    Module.Finite Oδ (integralClosure Oδ (AdjoinRoot h)) := by sorry