-- Mathlib/RingTheory/DedekindDomain/Dvr.lean
theorem Ring.DimensionLEOne.localization {R : Type*} (Rₘ : Type*) [CommRing R] [IsDomain R]
    [CommRing Rₘ] [Algebra R Rₘ] {M : Submonoid R} [IsLocalization M Rₘ] (hM : M ≤ R⁰)
    [h : Ring.DimensionLEOne R] : Ring.DimensionLEOne Rₘ := ⟨by
  intro p hp0 hpp
  refine Ideal.isMaximal_def.mpr ⟨hpp.ne_top, Ideal.maximal_of_no_maximal fun P hpP hPm => ?_⟩
  have hpP' : (⟨p, hpp⟩ : { p : Ideal Rₘ // p.IsPrime }) < ⟨P, hPm.isPrime⟩ := hpP
  rw [← (IsLocalization.orderIsoOfPrime M Rₘ).lt_iff_lt] at hpP'
  haveI : Ideal.IsPrime (Ideal.comap (algebraMap R Rₘ) p) :=
    ((IsLocalization.orderIsoOfPrime M Rₘ) ⟨p, hpp⟩).2.1
  haveI : Ideal.IsPrime (Ideal.comap (algebraMap R Rₘ) P) :=
    ((IsLocalization.orderIsoOfPrime M Rₘ) ⟨P, hPm.isPrime⟩).2.1
  have hlt : Ideal.comap (algebraMap R Rₘ) p < Ideal.comap (algebraMap R Rₘ) P := hpP'
  refine h.not_lt_lt ⊥ (Ideal.comap _ _) (Ideal.comap _ _) ⟨?_, hlt⟩
  exact IsLocalization.bot_lt_comap_prime _ _ hM _ hp0⟩

Proof state:
R : Type u_2
Rₘ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : p.IsPrime
P : Ideal Rₘ
hpP : p < P
hPm : P.IsMaximal
hpP' : (IsLocalization.orderIsoOfPrime M Rₘ) ⟨p, hpp⟩ < (IsLocalization.orderIsoOfPrime M Rₘ) ⟨P, ⋯⟩
this✝ : (Ideal.comap (algebraMap R Rₘ) p).IsPrime
this : (Ideal.comap (algebraMap R Rₘ) P).IsPrime
⊢ False

Tactic:
have hlt : Ideal.comap (algebraMap R Rₘ) p < Ideal.comap (algebraMap R Rₘ) P := hpP'

Result:
R : Type u_2
Rₘ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : p.IsPrime
P : Ideal Rₘ
hpP : p < P
hPm : P.IsMaximal
hpP' : (IsLocalization.orderIsoOfPrime M Rₘ) ⟨p, hpp⟩ < (IsLocalization.orderIsoOfPrime M Rₘ) ⟨P, ⋯⟩
this✝ : (Ideal.comap (algebraMap R Rₘ) p).IsPrime
this : (Ideal.comap (algebraMap R Rₘ) P).IsPrime
hlt : Ideal.comap (algebraMap R Rₘ) p < Ideal.comap (algebraMap R Rₘ) P
⊢ False

Proof state:
R : Type u_2
Rₘ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : p.IsPrime
P : Ideal Rₘ
hpP : p < P
hPm : P.IsMaximal
hpP' : (IsLocalization.orderIsoOfPrime M Rₘ) ⟨p, hpp⟩ < (IsLocalization.orderIsoOfPrime M Rₘ) ⟨P, ⋯⟩
⊢ False

Tactic:
haveI : Ideal.IsPrime (Ideal.comap (algebraMap R Rₘ) p) :=
  ((IsLocalization.orderIsoOfPrime M Rₘ) ⟨p, hpp⟩).2.1

Result:
R : Type u_2
Rₘ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : p.IsPrime
P : Ideal Rₘ
hpP : p < P
hPm : P.IsMaximal
hpP' : (IsLocalization.orderIsoOfPrime M Rₘ) ⟨p, hpp⟩ < (IsLocalization.orderIsoOfPrime M Rₘ) ⟨P, ⋯⟩
this : (Ideal.comap (algebraMap R Rₘ) p).IsPrime
⊢ False

Proof state:
R : Type u_2
Rₘ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : p.IsPrime
P : Ideal Rₘ
hpP : p < P
hPm : P.IsMaximal
hpP' : (IsLocalization.orderIsoOfPrime M Rₘ) ⟨p, hpp⟩ < (IsLocalization.orderIsoOfPrime M Rₘ) ⟨P, ⋯⟩
this✝ : (Ideal.comap (algebraMap R Rₘ) p).IsPrime
this : (Ideal.comap (algebraMap R Rₘ) P).IsPrime
hlt : Ideal.comap (algebraMap R Rₘ) p < Ideal.comap (algebraMap R Rₘ) P
⊢ ⊥ < Ideal.comap (algebraMap R Rₘ) p

Tactic:
exact IsLocalization.bot_lt_comap_prime _ _ hM _ hp0

Result:
no goals

Proof state:
R : Type u_2
Rₘ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : p.IsPrime
P : Ideal Rₘ
hpP : p < P
hPm : P.IsMaximal
hpP' : (IsLocalization.orderIsoOfPrime M Rₘ) ⟨p, hpp⟩ < (IsLocalization.orderIsoOfPrime M Rₘ) ⟨P, ⋯⟩
this✝ : (Ideal.comap (algebraMap R Rₘ) p).IsPrime
this : (Ideal.comap (algebraMap R Rₘ) P).IsPrime
hlt : Ideal.comap (algebraMap R Rₘ) p < Ideal.comap (algebraMap R Rₘ) P
⊢ False

Tactic:
refine h.not_lt_lt ⊥ (Ideal.comap _ _) (Ideal.comap _ _) ⟨?_, hlt⟩

Result:
R : Type u_2
Rₘ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : p.IsPrime
P : Ideal Rₘ
hpP : p < P
hPm : P.IsMaximal
hpP' : (IsLocalization.orderIsoOfPrime M Rₘ) ⟨p, hpp⟩ < (IsLocalization.orderIsoOfPrime M Rₘ) ⟨P, ⋯⟩
this✝ : (Ideal.comap (algebraMap R Rₘ) p).IsPrime
this : (Ideal.comap (algebraMap R Rₘ) P).IsPrime
hlt : Ideal.comap (algebraMap R Rₘ) p < Ideal.comap (algebraMap R Rₘ) P
⊢ ⊥ < Ideal.comap (algebraMap R Rₘ) p

Proof state:
R : Type u_2
Rₘ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : p.IsPrime
P : Ideal Rₘ
hpP : p < P
hPm : P.IsMaximal
hpP' : (IsLocalization.orderIsoOfPrime M Rₘ) ⟨p, hpp⟩ < (IsLocalization.orderIsoOfPrime M Rₘ) ⟨P, ⋯⟩
this : (Ideal.comap (algebraMap R Rₘ) p).IsPrime
⊢ False

Tactic:
haveI : Ideal.IsPrime (Ideal.comap (algebraMap R Rₘ) P) :=
  ((IsLocalization.orderIsoOfPrime M Rₘ) ⟨P, hPm.isPrime⟩).2.1

Result:
R : Type u_2
Rₘ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : p.IsPrime
P : Ideal Rₘ
hpP : p < P
hPm : P.IsMaximal
hpP' : (IsLocalization.orderIsoOfPrime M Rₘ) ⟨p, hpp⟩ < (IsLocalization.orderIsoOfPrime M Rₘ) ⟨P, ⋯⟩
this✝ : (Ideal.comap (algebraMap R Rₘ) p).IsPrime
this : (Ideal.comap (algebraMap R Rₘ) P).IsPrime
⊢ False

Proof state:
R : Type u_2
Rₘ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : p.IsPrime
P : Ideal Rₘ
hpP : p < P
hPm : P.IsMaximal
⊢ False

Tactic:
have hpP' : (⟨p, hpp⟩ : { p : Ideal Rₘ // p.IsPrime }) < ⟨P, hPm.isPrime⟩ := hpP

Result:
R : Type u_2
Rₘ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : p.IsPrime
P : Ideal Rₘ
hpP : p < P
hPm : P.IsMaximal
hpP' : ⟨p, hpp⟩ < ⟨P, ⋯⟩
⊢ False

Proof state:
R : Type u_2
Rₘ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : p.IsPrime
P : Ideal Rₘ
hpP : p < P
hPm : P.IsMaximal
hpP' : ⟨p, hpp⟩ < ⟨P, ⋯⟩
⊢ False

Tactic:
rw [← (IsLocalization.orderIsoOfPrime M Rₘ).lt_iff_lt] at hpP'

Result:
R : Type u_2
Rₘ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : p.IsPrime
P : Ideal Rₘ
hpP : p < P
hPm : P.IsMaximal
hpP' : (IsLocalization.orderIsoOfPrime M Rₘ) ⟨p, hpp⟩ < (IsLocalization.orderIsoOfPrime M Rₘ) ⟨P, ⋯⟩
⊢ False