-- Mathlib/RingTheory/DedekindDomain/Dvr.lean
theorem IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain [IsDedekindDomain A]
    {P : Ideal A} (hP : P ≠ ⊥) [pP : P.IsPrime] (Aₘ : Type*) [CommRing Aₘ] [IsDomain Aₘ]
    [Algebra A Aₘ] [IsLocalization.AtPrime Aₘ P] : IsDiscreteValuationRing Aₘ

Proof state:
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
pP : P.IsPrime
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
this : IsNoetherianRing Aₘ := isNoetherianRing P.primeCompl Aₘ IsDedekindRing.toIsNoetherian
⊢ IsDiscreteValuationRing Aₘ

Tactic:
letI : IsLocalRing Aₘ := IsLocalization.AtPrime.isLocalRing Aₘ P

Result:
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
pP : P.IsPrime
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
this✝ : IsNoetherianRing Aₘ := isNoetherianRing P.primeCompl Aₘ IsDedekindRing.toIsNoetherian
this : IsLocalRing Aₘ := isLocalRing Aₘ P
⊢ IsDiscreteValuationRing Aₘ

Proof state:
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
pP : P.IsPrime
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
⊢ IsDiscreteValuationRing Aₘ

Tactic:
letI : IsNoetherianRing Aₘ :=
  IsLocalization.isNoetherianRing P.primeCompl _ IsDedekindRing.toIsNoetherian

Result:
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
pP : P.IsPrime
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
this : IsNoetherianRing Aₘ := isNoetherianRing P.primeCompl Aₘ IsDedekindRing.toIsNoetherian
⊢ IsDiscreteValuationRing Aₘ

Proof state:
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
pP : P.IsPrime
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
this✝ : IsNoetherianRing Aₘ := isNoetherianRing P.primeCompl Aₘ IsDedekindRing.toIsNoetherian
this : IsLocalRing Aₘ := isLocalRing Aₘ P
hnf : ¬IsField Aₘ
⊢ IsDiscreteValuationRing Aₘ

Tactic:
exact
  ((IsDiscreteValuationRing.TFAE Aₘ hnf).out 0 2).mpr
    (IsLocalization.AtPrime.isDedekindDomain A P _)

Result:
no goals

Proof state:
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
pP : P.IsPrime
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
⊢ IsDiscreteValuationRing Aₘ

Tactic:
classical
letI : IsNoetherianRing Aₘ :=
  IsLocalization.isNoetherianRing P.primeCompl _ IsDedekindRing.toIsNoetherian
letI : IsLocalRing Aₘ := IsLocalization.AtPrime.isLocalRing Aₘ P
have hnf := IsLocalization.AtPrime.not_isField A hP Aₘ
exact
  ((IsDiscreteValuationRing.TFAE Aₘ hnf).out 0 2).mpr
    (IsLocalization.AtPrime.isDedekindDomain A P _)

Result:
no goals

Proof state:
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
pP : P.IsPrime
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
this✝ : IsNoetherianRing Aₘ := isNoetherianRing P.primeCompl Aₘ IsDedekindRing.toIsNoetherian
this : IsLocalRing Aₘ := isLocalRing Aₘ P
⊢ IsDiscreteValuationRing Aₘ

Tactic:
have hnf := IsLocalization.AtPrime.not_isField A hP Aₘ

Result:
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
P : Ideal A
hP : P ≠ ⊥
pP : P.IsPrime
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
this✝ : IsNoetherianRing Aₘ := isNoetherianRing P.primeCompl Aₘ IsDedekindRing.toIsNoetherian
this : IsLocalRing Aₘ := isLocalRing Aₘ P
hnf : ¬IsField Aₘ
⊢ IsDiscreteValuationRing Aₘ