theorem isFiniteUnramifiedSubext_integralClosure_isUnramifiedDVR (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (L : Type u_3) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra A L] [IsScalarTower A K L] (E : IntermediateField K L) (hE : IsFiniteUnramifiedSubext A K L E) [IsDomain ↥(integralClosure A ↥E)] [IsDiscreteValuationRing ↥(integralClosure A ↥E)] [IsLocalHom (algebraMap A ↥(integralClosure A ↥E))] [Module.Finite A ↥(integralClosure A ↥E)] : IsUnramifiedDVRExtension A ↥(integralClosure A ↥E)