-- Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean
theorem maximalIdeal_isPrincipal_of_isDedekindDomain [IsLocalRing R] [IsDomain R]
    [IsDedekindDomain R] : (maximalIdeal R).IsPrincipal

Proof state:
case neg.intro.intro.a
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
this✝¹ : (Ideal.span {a}).radical = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = n + 1
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : b ∉ Ideal.span {a}
hb₃ : ∀ m ∈ maximalIdeal R, ∃ k, k * a = b * m
hb₄ : b ≠ 0
K : Type u_1 := FractionRing R
x : K := (algebraMap R K) b / (algebraMap R K) a
M : Submodule R K := Submodule.map (Algebra.linearMap R K) (maximalIdeal R)
ha₃ : (algebraMap R K) a ≠ 0
hx : ¬∀ y ∈ M, x * y ∈ M
this : Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribMulAction.toLinearMap R K x) M) = ⊤
y : R
hy₁ : y ∈ maximalIdeal R
hy₂ : b * y = a
⊢ maximalIdeal R ≤ Submodule.span R {y}

Tactic:
intro m hm

Result:
case neg.intro.intro.a
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
this✝¹ : (Ideal.span {a}).radical = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = n + 1
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : b ∉ Ideal.span {a}
hb₃ : ∀ m ∈ maximalIdeal R, ∃ k, k * a = b * m
hb₄ : b ≠ 0
K : Type u_1 := FractionRing R
x : K := (algebraMap R K) b / (algebraMap R K) a
M : Submodule R K := Submodule.map (Algebra.linearMap R K) (maximalIdeal R)
ha₃ : (algebraMap R K) a ≠ 0
hx : ¬∀ y ∈ M, x * y ∈ M
this : Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribMulAction.toLinearMap R K x) M) = ⊤
y : R
hy₁ : y ∈ maximalIdeal R
hy₂ : b * y = a
m : R
hm : m ∈ maximalIdeal R
⊢ m ∈ Submodule.span R {y}

Proof state:
case a
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
⊢ maximalIdeal R ≤ sInf {J | Ideal.span {a} ≤ J ∧ J.IsPrime}

Tactic:
refine
  le_sInf fun I hI =>
    (eq_maximalIdeal <| hI.2.isMaximal (fun e => ha₂ ?_)).ge

Result:
case a
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
I : Ideal R
hI : I ∈ {J | Ideal.span {a} ≤ J ∧ J.IsPrime}
e : I = ⊥
⊢ a = 0

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
this✝ : (Ideal.span {a}).radical = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : maximalIdeal R ^ (n + 1) ≤ Ideal.span {a} ∧ ∀ n_1 < n + 1, ¬maximalIdeal R ^ n_1 ≤ Ideal.span {a}
h' : ∀ b ∈ maximalIdeal R ^ n, b ∈ Ideal.span {a}
⊢ False

Tactic:
exact hn.2 n n.lt_succ_self fun x hx => h' x hx

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
this✝ : (Ideal.span {a}).radical = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = n + 1
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : b ∉ Ideal.span {a}
m : R
hm : m ∈ maximalIdeal R
⊢ ∃ k, k * a = b * m

Tactic:
rw [← Ideal.mem_span_singleton']

Result:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
this✝ : (Ideal.span {a}).radical = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = n + 1
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : b ∉ Ideal.span {a}
m : R
hm : m ∈ maximalIdeal R
⊢ b * m ∈ Ideal.span {a}

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
⊢ ∃ a ∈ maximalIdeal R, a ≠ 0

Tactic:
by_contra! h'

Result:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
h' : ∀ a ∈ maximalIdeal R, a = 0
⊢ False

Proof state:
case neg.intro.intro
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
this : (Ideal.span {a}).radical = maximalIdeal R
⊢ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
have : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a} := by
  rw [← this]; apply Ideal.exists_radical_pow_le_of_fg; exact IsNoetherian.noetherian _

Result:
case neg.intro.intro
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
this✝ : (Ideal.span {a}).radical = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
⊢ Submodule.IsPrincipal (maximalIdeal R)

Proof state:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ne_bot : maximalIdeal R = ⊥
⊢ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
rw [ne_bot]

Result:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ne_bot : maximalIdeal R = ⊥
⊢ Submodule.IsPrincipal ⊥

Proof state:
case intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
this✝ : (Ideal.span {a}).radical = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = n + 1
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : b ∉ Ideal.span {a}
hb₃ : ∀ m ∈ maximalIdeal R, ∃ k, k * a = b * m
hb₄ : b ≠ 0
K : Type u_1 := FractionRing R
x : K := (algebraMap R K) b / (algebraMap R K) a
M : Submodule R K := Submodule.map (Algebra.linearMap R K) (maximalIdeal R)
ha₃ : (algebraMap R K) a ≠ 0
hx : ¬∀ y ∈ M, x * y ∈ M
h : ¬Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribMulAction.toLinearMap R K x) M) = ⊤
m : R
hm : m ∈ ↑(maximalIdeal R)
k : R
hk : k * a = b * m
⊢ x * (algebraMap R K) m ∈ M

Tactic:
have hk' : x * algebraMap R K m = algebraMap R K k := by
  rw [← mul_div_right_comm, ← map_mul, ← hk, map_mul, mul_div_cancel_right₀ _ ha₃]

Result:
case intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
hle : Ideal.span {a} ≤ maximalIdeal R
this✝ : (Ideal.span {a}).radical = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = n + 1
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : b ∉ Ideal.span {a}
hb₃ : ∀ m ∈ maximalIdeal R, ∃ k, k * a = b * m
hb₄ : b ≠ 0
K : Type u_1 := FractionRing R
x : K := (algebraMap R K) b / (algebraMap R K) a
M : Submodule R K := Submodule.map (Algebra.linearMap R K) (maximalIdeal R)
ha₃ : (algebraMap R K) a ≠ 0
hx : ¬∀ y ∈ M, x * y ∈ M
h : ¬Submodule.comap (Algebra.linearMap R K) (Submodule.map (DistribMulAction.toLinearMap R K x) M) = ⊤
m : R
hm : m ∈ ↑(maximalIdeal R)
k : R
hk : k * a = b * m
hk' : x * (algebraMap R K) m = (algebraMap R K) k
⊢ x * (algebraMap R K) m ∈ M