-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem dimensionLEOne : DimensionLEOne A := ⟨by
  -- We're going to show that `P` is maximal because any (maximal) ideal `M`
  -- that is strictly larger would be `⊤`.
  rintro P P_ne hP
  refine Ideal.isMaximal_def.mpr ⟨hP.ne_top, fun M hM => ?_⟩
  -- We may assume `P` and `M` (as fractional ideals) are nonzero.
  have P'_ne : (P : FractionalIdeal A⁰ (FractionRing A)) ≠ 0 := coeIdeal_ne_zero.mpr P_ne
  have M'_ne : (M : FractionalIdeal A⁰ (FractionRing A)) ≠ 0 := coeIdeal_ne_zero.mpr hM.ne_bot
  -- In particular, we'll show `M⁻¹ * P ≤ P`
  suffices (M⁻¹ : FractionalIdeal A⁰ (FractionRing A)) * P ≤ P by
    rw [eq_top_iff, ← coeIdeal_le_coeIdeal (FractionRing A), coeIdeal_top]
    calc
      (1 : FractionalIdeal A⁰ (FractionRing A)) = _ * _ * _ := ?_
      _ ≤ _ * _ := mul_right_mono
        ((P : FractionalIdeal A⁰ (FractionRing A))⁻¹ * M : FractionalIdeal A⁰ (FractionRing A)) this
      _ = M := ?_
    · rw [mul_assoc, ← mul_assoc (P : FractionalIdeal A⁰ (FractionRing A)), h.mul_inv_eq_one P'_ne,
      one_mul, h.inv_mul_eq_one M'_ne]
    · rw [← mul_assoc (P : FractionalIdeal A⁰ (FractionRing A)), h.mul_inv_eq_one P'_ne, one_mul]
  -- Suppose we have `x ∈ M⁻¹ * P`, then in fact `x = algebraMap _ _ y` for some `y`.
  intro x hx
  have le_one : (M⁻¹ : FractionalIdeal A⁰ (FractionRing A)) * P ≤ 1

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : ↑P ≠ 0
M'_ne : ↑M ≠ 0
⊢ (↑M)⁻¹ * ↑P ≤ ↑P

Tactic:
intro x hx

Result:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : ↑P ≠ 0
M'_ne : ↑M ≠ 0
x : FractionRing A
hx : x ∈ (fun a => ↑a) ((↑M)⁻¹ * ↑P)
⊢ x ∈ (fun a => ↑a) ↑P

Proof state:
case intro.intro.intro.intro.intro.intro
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : ↑P ≠ 0
M'_ne : ↑M ≠ 0
le_one : (↑M)⁻¹ * ↑P ≤ 1
y : A
_hy : y ∈ ⊤
hx : (algebraMap A (FractionRing A)) y ∈ (fun a => ↑a) ((↑M)⁻¹ * ↑P)
z : A
hzM : z ∈ M
hzp : z ∉ P
zy_mem : (algebraMap A (FractionRing A)) (z * y) ∈ ↑P
zy : A
hzy : zy ∈ P
zy_eq : (algebraMap A (FractionRing A)) zy = (algebraMap A (FractionRing A)) (z * y)
⊢ (algebraMap A (FractionRing A)) y ∈ (fun a => ↑a) ↑P

Tactic:
rw [IsFractionRing.injective A (FractionRing A) zy_eq] at hzy

Result:
case intro.intro.intro.intro.intro.intro
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : ↑P ≠ 0
M'_ne : ↑M ≠ 0
le_one : (↑M)⁻¹ * ↑P ≤ 1
y : A
_hy : y ∈ ⊤
hx : (algebraMap A (FractionRing A)) y ∈ (fun a => ↑a) ((↑M)⁻¹ * ↑P)
z : A
hzM : z ∈ M
hzp : z ∉ P
zy_mem : (algebraMap A (FractionRing A)) (z * y) ∈ ↑P
zy : A
hzy : z * y ∈ P
zy_eq : (algebraMap A (FractionRing A)) zy = (algebraMap A (FractionRing A)) (z * y)
⊢ (algebraMap A (FractionRing A)) y ∈ (fun a => ↑a) ↑P

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
⊢ P.IsMaximal

Tactic:
refine Ideal.isMaximal_def.mpr ⟨hP.ne_top, fun M hM => ?_⟩

Result:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
⊢ M = ⊤

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : ↑P ≠ 0
M'_ne : ↑M ≠ 0
x : FractionRing A
hx : x ∈ (fun a => ↑a) ((↑M)⁻¹ * ↑P)
⊢ (↑M)⁻¹ * ↑P ≤ (↑M)⁻¹ * ↑M

Tactic:
exact mul_left_mono _ ((coeIdeal_le_coeIdeal (FractionRing A)).mpr hM.le)

Result:
no goals

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : ↑P ≠ 0
M'_ne : ↑M ≠ 0
this : (↑M)⁻¹ * ↑P ≤ ↑P
⊢ M = ⊤

Tactic:
rw [eq_top_iff, ← coeIdeal_le_coeIdeal (FractionRing A), coeIdeal_top]

Result:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : ↑P ≠ 0
M'_ne : ↑M ≠ 0
this : (↑M)⁻¹ * ↑P ≤ ↑P
⊢ 1 ≤ ↑M

Proof state:
case calc_2
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : ↑P ≠ 0
M'_ne : ↑M ≠ 0
this : (↑M)⁻¹ * ↑P ≤ ↑P
⊢ ↑P * ((↑P)⁻¹ * ↑M) = ↑M

Tactic:
rw [← mul_assoc (P : FractionalIdeal A⁰ (FractionRing A)), h.mul_inv_eq_one P'_ne, one_mul]

Result:
no goals

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : ↑P ≠ 0
⊢ M = ⊤

Tactic:
have M'_ne : (M : FractionalIdeal A⁰ (FractionRing A)) ≠ 0 := coeIdeal_ne_zero.mpr hM.ne_bot

Result:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : ↑P ≠ 0
M'_ne : ↑M ≠ 0
⊢ M = ⊤

Proof state:
case intro.intro.intro.intro.intro.intro
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : ↑P ≠ 0
M'_ne : ↑M ≠ 0
le_one : (↑M)⁻¹ * ↑P ≤ 1
y : A
_hy : y ∈ ⊤
hx : (algebraMap A (FractionRing A)) y ∈ (fun a => ↑a) ((↑M)⁻¹ * ↑P)
z : A
hzM : z ∈ M
hzp : z ∉ P
zy_mem : (algebraMap A (FractionRing A)) (z * y) ∈ ↑P
zy : A
hzy : z * y ∈ P
zy_eq : (algebraMap A (FractionRing A)) zy = (algebraMap A (FractionRing A)) (z * y)
⊢ (algebraMap A (FractionRing A)) y ∈ (fun a => ↑a) ↑P

Tactic:
exact mem_coeIdeal_of_mem A⁰ (Or.resolve_left (hP.mem_or_mem hzy) hzp)

Result:
no goals

Proof state:
case calc_1
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : ↑P ≠ 0
M'_ne : ↑M ≠ 0
this : (↑M)⁻¹ * ↑P ≤ ↑P
⊢ 1 = (↑M)⁻¹ * ↑P * ((↑P)⁻¹ * ↑M)

Tactic:
rw [mul_assoc, ← mul_assoc (P : FractionalIdeal A⁰ (FractionRing A)), h.mul_inv_eq_one P'_ne,
one_mul, h.inv_mul_eq_one M'_ne]

Result:
no goals

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
⊢ ∀ {p : Ideal A}, p ≠ ⊥ → p.IsPrime → p.IsMaximal

Tactic:
rintro P P_ne hP

Result:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
⊢ P.IsMaximal

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : ↑P ≠ 0
M'_ne : ↑M ≠ 0
x : FractionRing A
hx : x ∈ (fun a => ↑a) ((↑M)⁻¹ * ↑P)
⊢ x ∈ (fun a => ↑a) ↑P

Tactic:
have le_one : (M⁻¹ : FractionalIdeal A⁰ (FractionRing A)) * P ≤ 1 := by
  rw [← h.inv_mul_eq_one M'_ne]
  exact mul_left_mono _ ((coeIdeal_le_coeIdeal (FractionRing A)).mpr hM.le)

Result:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : ↑P ≠ 0
M'_ne : ↑M ≠ 0
x : FractionRing A
hx : x ∈ (fun a => ↑a) ((↑M)⁻¹ * ↑P)
le_one : (↑M)⁻¹ * ↑P ≤ 1
⊢ x ∈ (fun a => ↑a) ↑P

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
⊢ M = ⊤

Tactic:
have P'_ne : (P : FractionalIdeal A⁰ (FractionRing A)) ≠ 0 := coeIdeal_ne_zero.mpr P_ne

Result:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : ↑P ≠ 0
⊢ M = ⊤