case pos
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ne_bot : maximalIdeal R = ⊥
⊢ Submodule.IsPrincipal (maximalIdeal R)

case neg
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
⊢ Submodule.IsPrincipal (maximalIdeal R)
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
⊢ Submodule.IsPrincipal (maximalIdeal R)
by_cases ne_bot : maximalIdeal R = ⊥
case neg.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
⊢ Submodule.IsPrincipal (maximalIdeal R)
case neg
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
⊢ Submodule.IsPrincipal (maximalIdeal R)
obtain ⟨a, ha₁, ha₂⟩ : ∃ a ∈ maximalIdeal R, a ≠ (0 : R) := by
  by_contra' h'; apply ne_bot; rwa [eq_bot_iff]
case neg.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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
⊢ Submodule.IsPrincipal (maximalIdeal R)
case neg.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
⊢ Submodule.IsPrincipal (maximalIdeal R)
have hle : Ideal.span {a} ≤ maximalIdeal R := by rwa [Ideal.span_le, Set.singleton_subset_iff]
case neg.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
⊢ Submodule.IsPrincipal (maximalIdeal R)
case neg.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
⊢ Submodule.IsPrincipal (maximalIdeal R)
have : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a} := by
  rw [← this]; apply Ideal.exists_radical_pow_le_of_fg; exact IsNoetherian.noetherian _
case neg.intro.intro.zero
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
hn : Nat.find this = Nat.zero
⊢ Submodule.IsPrincipal (maximalIdeal R)

case neg.intro.intro.succ
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
⊢ Submodule.IsPrincipal (maximalIdeal R)
case neg.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
⊢ Submodule.IsPrincipal (maximalIdeal R)
cases' hn : Nat.find this with n
case neg.intro.intro.succ.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
⊢ Submodule.IsPrincipal (maximalIdeal R)
case neg.intro.intro.succ
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
⊢ Submodule.IsPrincipal (maximalIdeal R)
obtain ⟨b, hb₁, hb₂⟩ : ∃ b ∈ maximalIdeal R ^ n, ¬b ∈ Ideal.span {a} := by
  by_contra' h'; rw [Nat.find_eq_iff] at hn ; exact hn.2 n n.lt_succ_self fun x hx => h' x hx
case neg.intro.intro.succ.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), m ∈ maximalIdeal R → ∃ k, k * a = b * m
⊢ Submodule.IsPrincipal (maximalIdeal R)
case neg.intro.intro.succ.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
⊢ Submodule.IsPrincipal (maximalIdeal R)
have hb₃ : ∀ m ∈ maximalIdeal R, ∃ k : R, k * a = b * m := by
  intro m hm; rw [← Ideal.mem_span_singleton']; apply Nat.find_spec this
  rw [hn, pow_succ']; exact Ideal.mul_mem_mul hb₁ hm
case neg.intro.intro.succ.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), m ∈ maximalIdeal R → ∃ k, k * a = b * m
hb₄ : b ≠ 0
⊢ Submodule.IsPrincipal (maximalIdeal R)
case neg.intro.intro.succ.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), m ∈ maximalIdeal R → ∃ k, k * a = b * m
⊢ Submodule.IsPrincipal (maximalIdeal R)
have hb₄ : b ≠ 0 := by rintro rfl; apply hb₂; exact zero_mem _
case neg.intro.intro.succ.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), m ∈ maximalIdeal R → ∃ k, k * a = b * m
hb₄ : b ≠ 0
K : Type u_1 := FractionRing R
⊢ Submodule.IsPrincipal (maximalIdeal R)
case neg.intro.intro.succ.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), m ∈ maximalIdeal R → ∃ k, k * a = b * m
hb₄ : b ≠ 0
⊢ Submodule.IsPrincipal (maximalIdeal R)
let K := FractionRing R
case neg.intro.intro.succ.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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
⊢ Submodule.IsPrincipal (maximalIdeal R)
case neg.intro.intro.succ.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), m ∈ maximalIdeal R → ∃ k, k * a = b * m
hb₄ : b ≠ 0
K : Type u_1 := FractionRing R
⊢ Submodule.IsPrincipal (maximalIdeal R)
let x : K := algebraMap R K b / algebraMap R K a
case neg.intro.intro.succ.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
⊢ Submodule.IsPrincipal (maximalIdeal R)
case neg.intro.intro.succ.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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
⊢ Submodule.IsPrincipal (maximalIdeal R)
let M := Submodule.map (Algebra.ofId R K).toLinearMap (maximalIdeal R)
case neg.intro.intro.succ.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
⊢ Submodule.IsPrincipal (maximalIdeal R)
case neg.intro.intro.succ.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
⊢ Submodule.IsPrincipal (maximalIdeal R)
have ha₃ : algebraMap R K a ≠ 0 := IsFractionRing.to_map_eq_zero_iff.not.mpr ha₂
case pos
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ∀ (y : K), y ∈ M → x * y ∈ M
⊢ Submodule.IsPrincipal (maximalIdeal R)

case neg
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
⊢ Submodule.IsPrincipal (maximalIdeal R)
case neg.intro.intro.succ.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
⊢ Submodule.IsPrincipal (maximalIdeal R)
by_cases hx : ∀ y ∈ M, x * y ∈ M
case pos
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ne_bot : maximalIdeal R = ⊥
⊢ Submodule.IsPrincipal ⊥
case pos
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ne_bot : maximalIdeal R = ⊥
⊢ Submodule.IsPrincipal (maximalIdeal R)
rw [ne_bot]
no goals
case pos
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ne_bot : maximalIdeal R = ⊥
⊢ Submodule.IsPrincipal ⊥
infer_instance
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
h' : ∀ (a : R), a ∈ maximalIdeal R → a = 0
⊢ False
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
⊢ ∃ a, a ∈ maximalIdeal R ∧ a ≠ 0
by_contra' h'
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
h' : ∀ (a : R), a ∈ maximalIdeal R → a = 0
⊢ maximalIdeal R = ⊥
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
h' : ∀ (a : R), a ∈ maximalIdeal R → a = 0
⊢ False
apply ne_bot
no goals
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
h' : ∀ (a : R), a ∈ maximalIdeal R → a = 0
⊢ maximalIdeal R = ⊥
rwa [eq_bot_iff]
no goals
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ne_bot : ¬maximalIdeal R = ⊥
a : R
ha₁ : a ∈ maximalIdeal R
ha₂ : a ≠ 0
⊢ Ideal.span {a} ≤ maximalIdeal R
rwa [Ideal.span_le, Set.singleton_subset_iff]
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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
⊢ sInf {J | Ideal.span {a} ≤ J ∧ Ideal.IsPrime J} = maximalIdeal R
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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
⊢ Ideal.radical (Ideal.span {a}) = maximalIdeal R
rw [Ideal.radical_eq_sInf]
case a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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
⊢ sInf {J | Ideal.span {a} ≤ J ∧ Ideal.IsPrime J} ≤ maximalIdeal R

case a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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 ∧ Ideal.IsPrime J}
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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
⊢ sInf {J | Ideal.span {a} ≤ J ∧ Ideal.IsPrime J} = maximalIdeal R
apply le_antisymm
no goals
case a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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
⊢ sInf {J | Ideal.span {a} ≤ J ∧ Ideal.IsPrime J} ≤ maximalIdeal R
exact sInf_le ⟨hle, inferInstance⟩
case a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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 ∧ Ideal.IsPrime J}
e : I = ⊥
⊢ a = 0
case a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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 ∧ Ideal.IsPrime J}
refine'
  le_sInf fun I hI =>
    (eq_maximalIdeal <| IsDedekindDomain.dimensionLEOne _ (fun e => ha₂ _) hI.2).ge
case a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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 ∧ Ideal.IsPrime J}
e : I = ⊥
⊢ Ideal.span {a} ≤ I
case a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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 ∧ Ideal.IsPrime J}
e : I = ⊥
⊢ a = 0
rw [← Ideal.span_singleton_eq_bot, eq_bot_iff, ← e]
no goals
case a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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 ∧ Ideal.IsPrime J}
e : I = ⊥
⊢ Ideal.span {a} ≤ I
exact hI.1
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
⊢ ∃ n, Ideal.radical (Ideal.span {a}) ^ n ≤ Ideal.span {a}
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
⊢ ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
rw [← this]
case h
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
⊢ Ideal.FG (Ideal.radical (Ideal.span {a}))
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
⊢ ∃ n, Ideal.radical (Ideal.span {a}) ^ n ≤ Ideal.span {a}
apply Ideal.exists_radical_pow_le_of_fg
no goals
case h
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
⊢ Ideal.FG (Ideal.radical (Ideal.span {a}))
exact IsNoetherian.noetherian _
case neg.intro.intro.zero
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
hn : Nat.find this✝ = Nat.zero
this : maximalIdeal R ^ Nat.find this✝ ≤ Ideal.span {a}
⊢ Submodule.IsPrincipal (maximalIdeal R)
case neg.intro.intro.zero
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
hn : Nat.find this = Nat.zero
⊢ Submodule.IsPrincipal (maximalIdeal R)
have := Nat.find_spec this
case neg.intro.intro.zero
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
hn : Nat.find this✝ = Nat.zero
this : ⊤ ≤ Ideal.span {a}
⊢ Submodule.IsPrincipal (maximalIdeal R)
case neg.intro.intro.zero
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
hn : Nat.find this✝ = Nat.zero
this : maximalIdeal R ^ Nat.find this✝ ≤ Ideal.span {a}
⊢ Submodule.IsPrincipal (maximalIdeal R)
rw [hn, pow_zero, Ideal.one_eq_top] at this
no goals
case neg.intro.intro.zero
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
hn : Nat.find this✝ = Nat.zero
this : ⊤ ≤ Ideal.span {a}
⊢ Submodule.IsPrincipal (maximalIdeal R)
exact (Ideal.IsMaximal.ne_top inferInstance (eq_top_iff.mpr <| this.trans hle)).elim
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
h' : ∀ (b : R), b ∈ maximalIdeal R ^ n → b ∈ Ideal.span {a}
⊢ False
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
⊢ ∃ b, b ∈ maximalIdeal R ^ n ∧ ¬b ∈ Ideal.span {a}
by_contra' h'
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn :
  maximalIdeal R ^ Nat.succ n ≤ Ideal.span {a} ∧ ∀ (n_1 : ℕ), n_1 < Nat.succ n → ¬maximalIdeal R ^ n_1 ≤ Ideal.span {a}
h' : ∀ (b : R), b ∈ maximalIdeal R ^ n → b ∈ Ideal.span {a}
⊢ False
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
h' : ∀ (b : R), b ∈ maximalIdeal R ^ n → b ∈ Ideal.span {a}
⊢ False
rw [Nat.find_eq_iff] at hn
no goals
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn :
  maximalIdeal R ^ Nat.succ n ≤ Ideal.span {a} ∧ ∀ (n_1 : ℕ), n_1 < Nat.succ n → ¬maximalIdeal R ^ n_1 ≤ Ideal.span {a}
h' : ∀ (b : R), b ∈ maximalIdeal R ^ n → b ∈ Ideal.span {a}
⊢ False
exact hn.2 n n.lt_succ_self fun x hx => h' x hx
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
m : R
hm : m ∈ maximalIdeal R
⊢ ∃ k, k * a = b * m
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
⊢ ∀ (m : R), m ∈ maximalIdeal R → ∃ k, k * a = b * m
intro m hm
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
m : R
hm : m ∈ maximalIdeal R
⊢ b * m ∈ Ideal.span {a}
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
m : R
hm : m ∈ maximalIdeal R
⊢ ∃ k, k * a = b * m
rw [← Ideal.mem_span_singleton']
case a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
m : R
hm : m ∈ maximalIdeal R
⊢ b * m ∈ maximalIdeal R ^ Nat.find this
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
m : R
hm : m ∈ maximalIdeal R
⊢ b * m ∈ Ideal.span {a}
apply Nat.find_spec this
case a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
m : R
hm : m ∈ maximalIdeal R
⊢ b * m ∈ maximalIdeal R ^ n * maximalIdeal R
case a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
m : R
hm : m ∈ maximalIdeal R
⊢ b * m ∈ maximalIdeal R ^ Nat.find this
rw [hn, pow_succ']
no goals
case a
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
m : R
hm : m ∈ maximalIdeal R
⊢ b * m ∈ maximalIdeal R ^ n * maximalIdeal R
exact Ideal.mul_mem_mul hb₁ hm
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
hb₁ : 0 ∈ maximalIdeal R ^ n
hb₂ : ¬0 ∈ Ideal.span {a}
hb₃ : ∀ (m : R), m ∈ maximalIdeal R → ∃ k, k * a = 0 * m
⊢ False
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), m ∈ maximalIdeal R → ∃ k, k * a = b * m
⊢ b ≠ 0
rintro rfl
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
hb₁ : 0 ∈ maximalIdeal R ^ n
hb₂ : ¬0 ∈ Ideal.span {a}
hb₃ : ∀ (m : R), m ∈ maximalIdeal R → ∃ k, k * a = 0 * m
⊢ 0 ∈ Ideal.span {a}
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
hb₁ : 0 ∈ maximalIdeal R ^ n
hb₂ : ¬0 ∈ Ideal.span {a}
hb₃ : ∀ (m : R), m ∈ maximalIdeal R → ∃ k, k * a = 0 * m
⊢ False
apply hb₂
no goals
R : Type u_1
inst✝⁶ : CommRing R
K : Type ?u.14279
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
hb₁ : 0 ∈ maximalIdeal R ^ n
hb₂ : ¬0 ∈ Ideal.span {a}
hb₃ : ∀ (m : R), m ∈ maximalIdeal R → ∃ k, k * a = 0 * m
⊢ 0 ∈ Ideal.span {a}
exact zero_mem _
case pos.refine_3
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ∀ (y : K), y ∈ M → x * y ∈ M
this : IsIntegral R x
⊢ Submodule.IsPrincipal (maximalIdeal R)

case pos.refine_1
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ∀ (y : K), y ∈ M → x * y ∈ M
⊢ M ≠ ⊥

case pos.refine_2
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ∀ (y : K), y ∈ M → x * y ∈ M
⊢ Submodule.FG M
case pos
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ∀ (y : K), y ∈ M → x * y ∈ M
⊢ Submodule.IsPrincipal (maximalIdeal R)
have := isIntegral_of_smul_mem_submodule M ?_ ?_ x hx
case pos.refine_3.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ∀ (y : K), y ∈ M → x * y ∈ M
this : IsIntegral R x
y : R
e : ↑(algebraMap R (FractionRing R)) y = x
⊢ Submodule.IsPrincipal (maximalIdeal R)
case pos.refine_3
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ∀ (y : K), y ∈ M → x * y ∈ M
this : IsIntegral R x
⊢ Submodule.IsPrincipal (maximalIdeal R)
obtain ⟨y, e⟩ := IsIntegrallyClosed.algebraMap_eq_of_integral this
case pos.refine_3.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ∀ (y : K), y ∈ M → x * y ∈ M
this : IsIntegral R x
y : R
e : ↑(algebraMap R (FractionRing R)) y = x
⊢ y * a = b
case pos.refine_3.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ∀ (y : K), y ∈ M → x * y ∈ M
this : IsIntegral R x
y : R
e : ↑(algebraMap R (FractionRing R)) y = x
⊢ Submodule.IsPrincipal (maximalIdeal R)
refine' (hb₂ (Ideal.mem_span_singleton'.mpr ⟨y, _⟩)).elim
case pos.refine_3.intro.a
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ∀ (y : K), y ∈ M → x * y ∈ M
this : IsIntegral R x
y : R
e : ↑(algebraMap R (FractionRing R)) y = x
⊢ ↑(algebraMap R K) (y * a) = ↑(algebraMap R K) b
case pos.refine_3.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ∀ (y : K), y ∈ M → x * y ∈ M
this : IsIntegral R x
y : R
e : ↑(algebraMap R (FractionRing R)) y = x
⊢ y * a = b
apply IsFractionRing.injective R K
no goals
case pos.refine_3.intro.a
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ∀ (y : K), y ∈ M → x * y ∈ M
this : IsIntegral R x
y : R
e : ↑(algebraMap R (FractionRing R)) y = x
⊢ ↑(algebraMap R K) (y * a) = ↑(algebraMap R K) b
rw [map_mul, e, div_mul_cancel _ ha₃]
case pos.refine_1
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ∀ (y : K), y ∈ M → x * y ∈ M
⊢ ∃ x, x ∈ M ∧ x ≠ 0
case pos.refine_1
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ∀ (y : K), y ∈ M → x * y ∈ M
⊢ M ≠ ⊥
rw [Submodule.ne_bot_iff]
case pos.refine_1
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ∀ (y : K), y ∈ M → x * y ∈ M
⊢ ↑(AlgHom.toLinearMap (Algebra.ofId R K)) a ≠ 0
case pos.refine_1
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ∀ (y : K), y ∈ M → x * y ∈ M
⊢ ∃ x, x ∈ M ∧ x ≠ 0
refine' ⟨_, ⟨a, ha₁, rfl⟩, _⟩
no goals
case pos.refine_1
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ∀ (y : K), y ∈ M → x * y ∈ M
⊢ ↑(AlgHom.toLinearMap (Algebra.ofId R K)) a ≠ 0
exact (IsFractionRing.to_map_eq_zero_iff (K := K)).not.mpr ha₂
case pos.refine_2.hs
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ∀ (y : K), y ∈ M → x * y ∈ M
⊢ Submodule.FG (maximalIdeal R)
case pos.refine_2
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ∀ (y : K), y ∈ M → x * y ∈ M
⊢ Submodule.FG M
apply Submodule.FG.map
no goals
case pos.refine_2.hs
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ∀ (y : K), y ∈ M → x * y ∈ M
⊢ Submodule.FG (maximalIdeal R)
exact IsNoetherian.noetherian _
case neg
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
this :
  Submodule.comap (AlgHom.toLinearMap (Algebra.ofId R K)) (Submodule.map (DistribMulAction.toLinearMap R K x) M) = ⊤
⊢ Submodule.IsPrincipal (maximalIdeal R)
case neg
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
⊢ Submodule.IsPrincipal (maximalIdeal R)
have :
    (M.map (DistribMulAction.toLinearMap R K x)).comap (Algebra.ofId R K).toLinearMap = ⊤ := by
  by_contra h; apply hx
  rintro m' ⟨m, hm, rfl : algebraMap R K m = m'⟩
  obtain ⟨k, hk⟩ := hb₃ m hm
  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 _ ha₃]
  exact ⟨k, le_maximalIdeal h ⟨_, ⟨_, hm, rfl⟩, hk'⟩, hk'.symm⟩
case neg.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
this :
  Submodule.comap (AlgHom.toLinearMap (Algebra.ofId R K)) (Submodule.map (DistribMulAction.toLinearMap R K x) M) = ⊤
y : R
hy₁ : y ∈ maximalIdeal R
hy₂ : b * y = a
⊢ Submodule.IsPrincipal (maximalIdeal R)
case neg
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
this :
  Submodule.comap (AlgHom.toLinearMap (Algebra.ofId R K)) (Submodule.map (DistribMulAction.toLinearMap R K x) M) = ⊤
⊢ Submodule.IsPrincipal (maximalIdeal R)
obtain ⟨y, hy₁, hy₂⟩ : ∃ y ∈ maximalIdeal R, b * y = a := by
  rw [Ideal.eq_top_iff_one, Submodule.mem_comap] at this
  obtain ⟨_, ⟨y, hy, rfl⟩, hy' : x * algebraMap R K y = algebraMap R K 1⟩ := this
  rw [map_one, ← mul_div_right_comm, div_eq_one_iff_eq ha₃, ← map_mul] at hy'
  exact ⟨y, hy, IsFractionRing.injective R K hy'⟩
case neg.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
this :
  Submodule.comap (AlgHom.toLinearMap (Algebra.ofId 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}
case neg.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
this :
  Submodule.comap (AlgHom.toLinearMap (Algebra.ofId R K)) (Submodule.map (DistribMulAction.toLinearMap R K x) M) = ⊤
y : R
hy₁ : y ∈ maximalIdeal R
hy₂ : b * y = a
⊢ Submodule.IsPrincipal (maximalIdeal R)
refine' ⟨⟨y, _⟩⟩
case neg.intro.intro.a
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
this :
  Submodule.comap (AlgHom.toLinearMap (Algebra.ofId 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}

case neg.intro.intro.a
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
this :
  Submodule.comap (AlgHom.toLinearMap (Algebra.ofId R K)) (Submodule.map (DistribMulAction.toLinearMap R K x) M) = ⊤
y : R
hy₁ : y ∈ maximalIdeal R
hy₂ : b * y = a
⊢ Submodule.span R {y} ≤ maximalIdeal R
case neg.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
this :
  Submodule.comap (AlgHom.toLinearMap (Algebra.ofId 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}
apply le_antisymm
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
h : ¬Submodule.comap (AlgHom.toLinearMap (Algebra.ofId R K)) (Submodule.map (DistribMulAction.toLinearMap R K x) M) = ⊤
⊢ False
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
⊢ Submodule.comap (AlgHom.toLinearMap (Algebra.ofId R K)) (Submodule.map (DistribMulAction.toLinearMap R K x) M) = ⊤
by_contra h
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
h : ¬Submodule.comap (AlgHom.toLinearMap (Algebra.ofId R K)) (Submodule.map (DistribMulAction.toLinearMap R K x) M) = ⊤
⊢ ∀ (y : K), y ∈ M → x * y ∈ M
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
h : ¬Submodule.comap (AlgHom.toLinearMap (Algebra.ofId R K)) (Submodule.map (DistribMulAction.toLinearMap R K x) M) = ⊤
⊢ False
apply hx
case intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
h : ¬Submodule.comap (AlgHom.toLinearMap (Algebra.ofId R K)) (Submodule.map (DistribMulAction.toLinearMap R K x) M) = ⊤
m : R
hm : m ∈ ↑(maximalIdeal R)
⊢ x * ↑(algebraMap R K) m ∈ M
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
h : ¬Submodule.comap (AlgHom.toLinearMap (Algebra.ofId R K)) (Submodule.map (DistribMulAction.toLinearMap R K x) M) = ⊤
⊢ ∀ (y : K), y ∈ M → x * y ∈ M
rintro m' ⟨m, hm, rfl : algebraMap R K m = m'⟩
case intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
h : ¬Submodule.comap (AlgHom.toLinearMap (Algebra.ofId 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
case intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
h : ¬Submodule.comap (AlgHom.toLinearMap (Algebra.ofId R K)) (Submodule.map (DistribMulAction.toLinearMap R K x) M) = ⊤
m : R
hm : m ∈ ↑(maximalIdeal R)
⊢ x * ↑(algebraMap R K) m ∈ M
obtain ⟨k, hk⟩ := hb₃ m hm
case intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
h : ¬Submodule.comap (AlgHom.toLinearMap (Algebra.ofId 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
case intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
h : ¬Submodule.comap (AlgHom.toLinearMap (Algebra.ofId 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
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 _ ha₃]
no goals
case intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
h : ¬Submodule.comap (AlgHom.toLinearMap (Algebra.ofId 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
exact ⟨k, le_maximalIdeal h ⟨_, ⟨_, hm, rfl⟩, hk'⟩, hk'.symm⟩
no goals
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
h : ¬Submodule.comap (AlgHom.toLinearMap (Algebra.ofId 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 = ↑(algebraMap R K) k
rw [← mul_div_right_comm, ← map_mul, ← hk, map_mul, mul_div_cancel _ ha₃]
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
this : ↑(AlgHom.toLinearMap (Algebra.ofId R K)) 1 ∈ Submodule.map (DistribMulAction.toLinearMap R K x) M
⊢ ∃ y, y ∈ maximalIdeal R ∧ b * y = a
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
this :
  Submodule.comap (AlgHom.toLinearMap (Algebra.ofId R K)) (Submodule.map (DistribMulAction.toLinearMap R K x) M) = ⊤
⊢ ∃ y, y ∈ maximalIdeal R ∧ b * y = a
rw [Ideal.eq_top_iff_one, Submodule.mem_comap] at this
case intro.intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
y : R
hy : y ∈ ↑(maximalIdeal R)
hy' : x * ↑(algebraMap R K) y = ↑(algebraMap R K) 1
⊢ ∃ y, y ∈ maximalIdeal R ∧ b * y = a
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
this : ↑(AlgHom.toLinearMap (Algebra.ofId R K)) 1 ∈ Submodule.map (DistribMulAction.toLinearMap R K x) M
⊢ ∃ y, y ∈ maximalIdeal R ∧ b * y = a
obtain ⟨_, ⟨y, hy, rfl⟩, hy' : x * algebraMap R K y = algebraMap R K 1⟩ := this
case intro.intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
y : R
hy : y ∈ ↑(maximalIdeal R)
hy' : ↑(algebraMap R K) (b * y) = ↑(algebraMap R K) a
⊢ ∃ y, y ∈ maximalIdeal R ∧ b * y = a
case intro.intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
y : R
hy : y ∈ ↑(maximalIdeal R)
hy' : x * ↑(algebraMap R K) y = ↑(algebraMap R K) 1
⊢ ∃ y, y ∈ maximalIdeal R ∧ b * y = a
rw [map_one, ← mul_div_right_comm, div_eq_one_iff_eq ha₃, ← map_mul] at hy'
no goals
case intro.intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
y : R
hy : y ∈ ↑(maximalIdeal R)
hy' : ↑(algebraMap R K) (b * y) = ↑(algebraMap R K) a
⊢ ∃ y, y ∈ maximalIdeal R ∧ b * y = a
exact ⟨y, hy, IsFractionRing.injective R K hy'⟩
case neg.intro.intro.a
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
this :
  Submodule.comap (AlgHom.toLinearMap (Algebra.ofId 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}
case neg.intro.intro.a
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
this :
  Submodule.comap (AlgHom.toLinearMap (Algebra.ofId 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}
intro m hm
case neg.intro.intro.a.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
this :
  Submodule.comap (AlgHom.toLinearMap (Algebra.ofId 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
k : R
hk : k * a = b * m
⊢ m ∈ Submodule.span R {y}
case neg.intro.intro.a
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
this :
  Submodule.comap (AlgHom.toLinearMap (Algebra.ofId 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}
obtain ⟨k, hk⟩ := hb₃ m hm
case neg.intro.intro.a.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
this :
  Submodule.comap (AlgHom.toLinearMap (Algebra.ofId 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
k : R
hk : b * (y * k) = b * m
⊢ m ∈ Submodule.span R {y}
case neg.intro.intro.a.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
this :
  Submodule.comap (AlgHom.toLinearMap (Algebra.ofId 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
k : R
hk : k * a = b * m
⊢ m ∈ Submodule.span R {y}
rw [← hy₂, mul_comm, mul_assoc] at hk
case neg.intro.intro.a.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
this :
  Submodule.comap (AlgHom.toLinearMap (Algebra.ofId 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
k : R
hk : b * (y * k) = b * m
⊢ k * y ∈ Submodule.span R {y}
case neg.intro.intro.a.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
this :
  Submodule.comap (AlgHom.toLinearMap (Algebra.ofId 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
k : R
hk : b * (y * k) = b * m
⊢ m ∈ Submodule.span R {y}
rw [← mul_left_cancel₀ hb₄ hk, mul_comm]
no goals
case neg.intro.intro.a.intro
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
this :
  Submodule.comap (AlgHom.toLinearMap (Algebra.ofId 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
k : R
hk : b * (y * k) = b * m
⊢ k * y ∈ Submodule.span R {y}
exact Ideal.mem_span_singleton'.mpr ⟨_, rfl⟩
no goals
case neg.intro.intro.a
R : Type u_1
inst✝⁶ : CommRing R
K✝ : Type ?u.14279
inst✝⁵ : Field K✝
inst✝⁴ : Algebra R K✝
inst✝³ : IsFractionRing R K✝
inst✝² : LocalRing 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.radical (Ideal.span {a}) = maximalIdeal R
this✝ : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a}
n : ℕ
hn : Nat.find this✝ = Nat.succ n
b : R
hb₁ : b ∈ maximalIdeal R ^ n
hb₂ : ¬b ∈ Ideal.span {a}
hb₃ : ∀ (m : R), 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 (AlgHom.toLinearMap (Algebra.ofId R K)) (maximalIdeal R)
ha₃ : ↑(algebraMap R K) a ≠ 0
hx : ¬∀ (y : K), y ∈ M → x * y ∈ M
this :
  Submodule.comap (AlgHom.toLinearMap (Algebra.ofId R K)) (Submodule.map (DistribMulAction.toLinearMap R K x) M) = ⊤
y : R
hy₁ : y ∈ maximalIdeal R
hy₂ : b * y = a
⊢ Submodule.span R {y} ≤ maximalIdeal R
rwa [Submodule.span_le, Set.singleton_subset_iff]