[GOAL]
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
⊢ coeff (map (mk P) f) n = coeff (↑C (↑(mk P) (leadingCoeff f)) * X ^ natDegree f) n
[PROOFSTEP]
by_cases hf0 : f = 0
[GOAL]
case pos
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
hf0 : f = 0
⊢ coeff (map (mk P) f) n = coeff (↑C (↑(mk P) (leadingCoeff f)) * X ^ natDegree f) n
[PROOFSTEP]
simp [hf0]
[GOAL]
case neg
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
hf0 : ¬f = 0
⊢ coeff (map (mk P) f) n = coeff (↑C (↑(mk P) (leadingCoeff f)) * X ^ natDegree f) n
[PROOFSTEP]
rcases lt_trichotomy (n : WithBot ℕ) (degree f) with (h | h | h)
[GOAL]
case neg.inl
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
hf0 : ¬f = 0
h : ↑n < degree f
⊢ coeff (map (mk P) f) n = coeff (↑C (↑(mk P) (leadingCoeff f)) * X ^ natDegree f) n
[PROOFSTEP]
erw [coeff_map, eq_zero_iff_mem.2 (hfP n h), coeff_C_mul, coeff_X_pow, if_neg, mul_zero]
[GOAL]
case neg.inl.hnc
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
hf0 : ¬f = 0
h : ↑n < degree f
⊢ ¬n = natDegree f
[PROOFSTEP]
rintro rfl
[GOAL]
case neg.inl.hnc
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
hf0 : ¬f = 0
h : ↑(natDegree f) < degree f
⊢ False
[PROOFSTEP]
exact not_lt_of_ge degree_le_natDegree h
[GOAL]
case neg.inr.inl
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
hf0 : ¬f = 0
h : ↑n = degree f
⊢ coeff (map (mk P) f) n = coeff (↑C (↑(mk P) (leadingCoeff f)) * X ^ natDegree f) n
[PROOFSTEP]
have : natDegree f = n := natDegree_eq_of_degree_eq_some h.symm
[GOAL]
case neg.inr.inl
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
hf0 : ¬f = 0
h : ↑n = degree f
this : natDegree f = n
⊢ coeff (map (mk P) f) n = coeff (↑C (↑(mk P) (leadingCoeff f)) * X ^ natDegree f) n
[PROOFSTEP]
rw [coeff_C_mul, coeff_X_pow, if_pos this.symm, mul_one, leadingCoeff, this, coeff_map]
[GOAL]
case neg.inr.inr
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
hf0 : ¬f = 0
h : degree f < ↑n
⊢ coeff (map (mk P) f) n = coeff (↑C (↑(mk P) (leadingCoeff f)) * X ^ natDegree f) n
[PROOFSTEP]
rw [coeff_eq_zero_of_degree_lt, coeff_eq_zero_of_degree_lt]
[GOAL]
case neg.inr.inr
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
hf0 : ¬f = 0
h : degree f < ↑n
⊢ degree (↑C (↑(mk P) (leadingCoeff f)) * X ^ natDegree f) < ↑n
[PROOFSTEP]
refine' lt_of_le_of_lt (degree_C_mul_X_pow_le _ _) _
[GOAL]
case neg.inr.inr
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
hf0 : ¬f = 0
h : degree f < ↑n
⊢ ↑(natDegree f) < ↑n
[PROOFSTEP]
rwa [← degree_eq_natDegree hf0]
[GOAL]
case neg.inr.inr
R : Type u_1
inst✝ : CommRing R
f : R[X]
P : Ideal R
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
n : ℕ
hf0 : ¬f = 0
h : degree f < ↑n
⊢ degree (map (mk P) f) < ↑n
[PROOFSTEP]
exact lt_of_le_of_lt (degree_map_le _ _) h
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
P : Ideal R
hP : Ideal.IsPrime P
q : R[X]
c : (R ⧸ P)[X]
hq : map (mk P) q = c * X ^ n
hc0 : degree c = 0
⊢ ↑n = degree (map (mk P) q)
[PROOFSTEP]
rw [hq, degree_mul, hc0, zero_add, degree_pow, degree_X, nsmul_one, Nat.cast_withBot]
[GOAL]
R : Type u_1
inst✝ : CommRing R
n : ℕ
P : Ideal R
q : R[X]
c : (R ⧸ P)[X]
hq : map (mk P) q = c * X ^ n
hn0 : 0 < n
⊢ eval 0 q ∈ P
[PROOFSTEP]
rw [← coeff_zero_eq_eval_zero, ← eq_zero_iff_mem, ← coeff_map, hq,
  --Porting note: why is this lemma required twice?coeff_zero_eq_eval_zero, coeff_zero_eq_eval_zero, eval_mul, eval_pow,
  eval_X, zero_pow hn0, mul_zero]
[GOAL]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hu : IsPrimitive (p * q)
hpm : natDegree p = 0
⊢ IsUnit p
[PROOFSTEP]
rw [eq_C_of_degree_le_zero (natDegree_eq_zero_iff_degree_le_zero.1 hpm), isUnit_C]
[GOAL]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hu : IsPrimitive (p * q)
hpm : natDegree p = 0
⊢ IsUnit (coeff p 0)
[PROOFSTEP]
refine' hu _ _
[GOAL]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hu : IsPrimitive (p * q)
hpm : natDegree p = 0
⊢ ↑C (coeff p 0) ∣ p * q
[PROOFSTEP]
rw [← eq_C_of_degree_le_zero (natDegree_eq_zero_iff_degree_le_zero.1 hpm)]
[GOAL]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hu : IsPrimitive (p * q)
hpm : natDegree p = 0
⊢ p ∣ p * q
[PROOFSTEP]
exact dvd_mul_right _ _
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : Ideal.IsPrime P
hfl : ¬leadingCoeff f ∈ P
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
hfd0 : 0 < degree f
h0 : ¬coeff f 0 ∈ P ^ 2
hu : IsPrimitive f
x✝ : f = 0
⊢ False
[PROOFSTEP]
simp_all only [not_true, Submodule.zero_mem, coeff_zero]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : Ideal.IsPrime P
hfl : ¬leadingCoeff f ∈ P
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
hfd0✝ : 0 < degree f
h0 : ¬coeff f 0 ∈ P ^ 2
hu : IsPrimitive f
hf0 : f ≠ 0
hf : map (mk P) f = ↑C (↑(mk P) (leadingCoeff f)) * X ^ natDegree f
hfd0 : 0 < natDegree f
h : degree f = 0
⊢ False
[PROOFSTEP]
simp_all only [lt_irrefl]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : Ideal.IsPrime P
hfl : ¬leadingCoeff f ∈ P
hfP : ∀ (n : ℕ), ↑n < degree f → coeff f n ∈ P
hfd0✝ : 0 < degree f
h0 : ¬coeff f 0 ∈ P ^ 2
hu : IsPrimitive f
hf0 : f ≠ 0
hf : map (mk P) f = ↑C (↑(mk P) (leadingCoeff f)) * X ^ natDegree f
hfd0 : 0 < natDegree f
⊢ ∀ (a b : R[X]), f = a * b → IsUnit a ∨ IsUnit b
[PROOFSTEP]
rintro p q rfl
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) (p * q) = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
⊢ IsUnit p ∨ IsUnit q
[PROOFSTEP]
rw [Polynomial.map_mul] at hf
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
⊢ IsUnit p ∨ IsUnit q
[PROOFSTEP]
rcases mul_eq_mul_prime_pow (show Prime (X : Polynomial (R ⧸ P)) from monic_X.prime_of_degree_eq_one degree_X) hf with
  ⟨m, n, b, c, hmnd, hbc, hp, hq⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
m n : ℕ
b c : (R ⧸ P)[X]
hmnd : m + n = natDegree (p * q)
hbc : ↑C (↑(mk P) (leadingCoeff (p * q))) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
⊢ IsUnit p ∨ IsUnit q
[PROOFSTEP]
have hmn : 0 < m → 0 < n → False := by
  intro hm0 hn0
  refine' h0 _
  rw [coeff_zero_eq_eval_zero, eval_mul, sq]
  exact Ideal.mul_mem_mul (eval_zero_mem_ideal_of_eq_mul_X_pow hp hm0) (eval_zero_mem_ideal_of_eq_mul_X_pow hq hn0)
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
m n : ℕ
b c : (R ⧸ P)[X]
hmnd : m + n = natDegree (p * q)
hbc : ↑C (↑(mk P) (leadingCoeff (p * q))) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
⊢ 0 < m → 0 < n → False
[PROOFSTEP]
intro hm0 hn0
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
m n : ℕ
b c : (R ⧸ P)[X]
hmnd : m + n = natDegree (p * q)
hbc : ↑C (↑(mk P) (leadingCoeff (p * q))) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hm0 : 0 < m
hn0 : 0 < n
⊢ False
[PROOFSTEP]
refine' h0 _
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
m n : ℕ
b c : (R ⧸ P)[X]
hmnd : m + n = natDegree (p * q)
hbc : ↑C (↑(mk P) (leadingCoeff (p * q))) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hm0 : 0 < m
hn0 : 0 < n
⊢ coeff (p * q) 0 ∈ P ^ 2
[PROOFSTEP]
rw [coeff_zero_eq_eval_zero, eval_mul, sq]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
m n : ℕ
b c : (R ⧸ P)[X]
hmnd : m + n = natDegree (p * q)
hbc : ↑C (↑(mk P) (leadingCoeff (p * q))) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hm0 : 0 < m
hn0 : 0 < n
⊢ eval 0 p * eval 0 q ∈ P * P
[PROOFSTEP]
exact Ideal.mul_mem_mul (eval_zero_mem_ideal_of_eq_mul_X_pow hp hm0) (eval_zero_mem_ideal_of_eq_mul_X_pow hq hn0)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
m n : ℕ
b c : (R ⧸ P)[X]
hmnd : m + n = natDegree (p * q)
hbc : ↑C (↑(mk P) (leadingCoeff (p * q))) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hmn : 0 < m → 0 < n → False
⊢ IsUnit p ∨ IsUnit q
[PROOFSTEP]
have hpql0 : (mk P) (p * q).leadingCoeff ≠ 0 := by rwa [Ne.def, eq_zero_iff_mem]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
m n : ℕ
b c : (R ⧸ P)[X]
hmnd : m + n = natDegree (p * q)
hbc : ↑C (↑(mk P) (leadingCoeff (p * q))) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hmn : 0 < m → 0 < n → False
⊢ ↑(mk P) (leadingCoeff (p * q)) ≠ 0
[PROOFSTEP]
rwa [Ne.def, eq_zero_iff_mem]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
m n : ℕ
b c : (R ⧸ P)[X]
hmnd : m + n = natDegree (p * q)
hbc : ↑C (↑(mk P) (leadingCoeff (p * q))) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hmn : 0 < m → 0 < n → False
hpql0 : ↑(mk P) (leadingCoeff (p * q)) ≠ 0
⊢ IsUnit p ∨ IsUnit q
[PROOFSTEP]
have hp0 : p ≠ 0 := fun h => by simp_all only [zero_mul, eq_self_iff_true, not_true, Ne.def]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
m n : ℕ
b c : (R ⧸ P)[X]
hmnd : m + n = natDegree (p * q)
hbc : ↑C (↑(mk P) (leadingCoeff (p * q))) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hmn : 0 < m → 0 < n → False
hpql0 : ↑(mk P) (leadingCoeff (p * q)) ≠ 0
h : p = 0
⊢ False
[PROOFSTEP]
simp_all only [zero_mul, eq_self_iff_true, not_true, Ne.def]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
m n : ℕ
b c : (R ⧸ P)[X]
hmnd : m + n = natDegree (p * q)
hbc : ↑C (↑(mk P) (leadingCoeff (p * q))) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hmn : 0 < m → 0 < n → False
hpql0 : ↑(mk P) (leadingCoeff (p * q)) ≠ 0
hp0 : p ≠ 0
⊢ IsUnit p ∨ IsUnit q
[PROOFSTEP]
have hq0 : q ≠ 0 := fun h => by simp_all only [eq_self_iff_true, not_true, Ne.def, mul_zero]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
m n : ℕ
b c : (R ⧸ P)[X]
hmnd : m + n = natDegree (p * q)
hbc : ↑C (↑(mk P) (leadingCoeff (p * q))) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hmn : 0 < m → 0 < n → False
hpql0 : ↑(mk P) (leadingCoeff (p * q)) ≠ 0
hp0 : p ≠ 0
h : q = 0
⊢ False
[PROOFSTEP]
simp_all only [eq_self_iff_true, not_true, Ne.def, mul_zero]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
m n : ℕ
b c : (R ⧸ P)[X]
hmnd : m + n = natDegree (p * q)
hbc : ↑C (↑(mk P) (leadingCoeff (p * q))) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hmn : 0 < m → 0 < n → False
hpql0 : ↑(mk P) (leadingCoeff (p * q)) ≠ 0
hp0 : p ≠ 0
hq0 : q ≠ 0
⊢ IsUnit p ∨ IsUnit q
[PROOFSTEP]
have hbc0 : degree b = 0 ∧ degree c = 0 := by
  apply_fun degree at hbc
  rwa [degree_C hpql0, degree_mul, eq_comm, Nat.WithBot.add_eq_zero_iff] at hbc
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
m n : ℕ
b c : (R ⧸ P)[X]
hmnd : m + n = natDegree (p * q)
hbc : ↑C (↑(mk P) (leadingCoeff (p * q))) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hmn : 0 < m → 0 < n → False
hpql0 : ↑(mk P) (leadingCoeff (p * q)) ≠ 0
hp0 : p ≠ 0
hq0 : q ≠ 0
⊢ degree b = 0 ∧ degree c = 0
[PROOFSTEP]
apply_fun degree at hbc
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
m n : ℕ
b c : (R ⧸ P)[X]
hmnd : m + n = natDegree (p * q)
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hmn : 0 < m → 0 < n → False
hpql0 : ↑(mk P) (leadingCoeff (p * q)) ≠ 0
hp0 : p ≠ 0
hq0 : q ≠ 0
hbc : degree (↑C (↑(mk P) (leadingCoeff (p * q)))) = degree (b * c)
⊢ degree b = 0 ∧ degree c = 0
[PROOFSTEP]
rwa [degree_C hpql0, degree_mul, eq_comm, Nat.WithBot.add_eq_zero_iff] at hbc
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
m n : ℕ
b c : (R ⧸ P)[X]
hmnd : m + n = natDegree (p * q)
hbc : ↑C (↑(mk P) (leadingCoeff (p * q))) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hmn : 0 < m → 0 < n → False
hpql0 : ↑(mk P) (leadingCoeff (p * q)) ≠ 0
hp0 : p ≠ 0
hq0 : q ≠ 0
hbc0 : degree b = 0 ∧ degree c = 0
⊢ IsUnit p ∨ IsUnit q
[PROOFSTEP]
have hmp : m ≤ natDegree p := le_natDegree_of_map_eq_mul_X_pow hP hp hbc0.1
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
m n : ℕ
b c : (R ⧸ P)[X]
hmnd : m + n = natDegree (p * q)
hbc : ↑C (↑(mk P) (leadingCoeff (p * q))) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hmn : 0 < m → 0 < n → False
hpql0 : ↑(mk P) (leadingCoeff (p * q)) ≠ 0
hp0 : p ≠ 0
hq0 : q ≠ 0
hbc0 : degree b = 0 ∧ degree c = 0
hmp : m ≤ natDegree p
⊢ IsUnit p ∨ IsUnit q
[PROOFSTEP]
have hnq : n ≤ natDegree q := le_natDegree_of_map_eq_mul_X_pow hP hq hbc0.2
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
m n : ℕ
b c : (R ⧸ P)[X]
hmnd : m + n = natDegree (p * q)
hbc : ↑C (↑(mk P) (leadingCoeff (p * q))) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hmn : 0 < m → 0 < n → False
hpql0 : ↑(mk P) (leadingCoeff (p * q)) ≠ 0
hp0 : p ≠ 0
hq0 : q ≠ 0
hbc0 : degree b = 0 ∧ degree c = 0
hmp : m ≤ natDegree p
hnq : n ≤ natDegree q
⊢ IsUnit p ∨ IsUnit q
[PROOFSTEP]
have hpmqn : p.natDegree = m ∧ q.natDegree = n :=
  by
  rw [natDegree_mul hp0 hq0] at hmnd
  contrapose hmnd
  apply ne_of_lt
  rw [not_and_or] at hmnd
  cases' hmnd with hmnd hmnd
  · exact add_lt_add_of_lt_of_le (lt_of_le_of_ne hmp (Ne.symm hmnd)) hnq
  · exact add_lt_add_of_le_of_lt hmp (lt_of_le_of_ne hnq (Ne.symm hmnd))
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
m n : ℕ
b c : (R ⧸ P)[X]
hmnd : m + n = natDegree (p * q)
hbc : ↑C (↑(mk P) (leadingCoeff (p * q))) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hmn : 0 < m → 0 < n → False
hpql0 : ↑(mk P) (leadingCoeff (p * q)) ≠ 0
hp0 : p ≠ 0
hq0 : q ≠ 0
hbc0 : degree b = 0 ∧ degree c = 0
hmp : m ≤ natDegree p
hnq : n ≤ natDegree q
⊢ natDegree p = m ∧ natDegree q = n
[PROOFSTEP]
rw [natDegree_mul hp0 hq0] at hmnd
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
m n : ℕ
b c : (R ⧸ P)[X]
hmnd : m + n = natDegree p + natDegree q
hbc : ↑C (↑(mk P) (leadingCoeff (p * q))) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hmn : 0 < m → 0 < n → False
hpql0 : ↑(mk P) (leadingCoeff (p * q)) ≠ 0
hp0 : p ≠ 0
hq0 : q ≠ 0
hbc0 : degree b = 0 ∧ degree c = 0
hmp : m ≤ natDegree p
hnq : n ≤ natDegree q
⊢ natDegree p = m ∧ natDegree q = n
[PROOFSTEP]
contrapose hmnd
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
m n : ℕ
b c : (R ⧸ P)[X]
hbc : ↑C (↑(mk P) (leadingCoeff (p * q))) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hmn : 0 < m → 0 < n → False
hpql0 : ↑(mk P) (leadingCoeff (p * q)) ≠ 0
hp0 : p ≠ 0
hq0 : q ≠ 0
hbc0 : degree b = 0 ∧ degree c = 0
hmp : m ≤ natDegree p
hnq : n ≤ natDegree q
hmnd : ¬(natDegree p = m ∧ natDegree q = n)
⊢ ¬m + n = natDegree p + natDegree q
[PROOFSTEP]
apply ne_of_lt
[GOAL]
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
m n : ℕ
b c : (R ⧸ P)[X]
hbc : ↑C (↑(mk P) (leadingCoeff (p * q))) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hmn : 0 < m → 0 < n → False
hpql0 : ↑(mk P) (leadingCoeff (p * q)) ≠ 0
hp0 : p ≠ 0
hq0 : q ≠ 0
hbc0 : degree b = 0 ∧ degree c = 0
hmp : m ≤ natDegree p
hnq : n ≤ natDegree q
hmnd : ¬(natDegree p = m ∧ natDegree q = n)
⊢ m + n < natDegree p + natDegree q
[PROOFSTEP]
rw [not_and_or] at hmnd
[GOAL]
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
m n : ℕ
b c : (R ⧸ P)[X]
hbc : ↑C (↑(mk P) (leadingCoeff (p * q))) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hmn : 0 < m → 0 < n → False
hpql0 : ↑(mk P) (leadingCoeff (p * q)) ≠ 0
hp0 : p ≠ 0
hq0 : q ≠ 0
hbc0 : degree b = 0 ∧ degree c = 0
hmp : m ≤ natDegree p
hnq : n ≤ natDegree q
hmnd : ¬natDegree p = m ∨ ¬natDegree q = n
⊢ m + n < natDegree p + natDegree q
[PROOFSTEP]
cases' hmnd with hmnd hmnd
[GOAL]
case h.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
m n : ℕ
b c : (R ⧸ P)[X]
hbc : ↑C (↑(mk P) (leadingCoeff (p * q))) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hmn : 0 < m → 0 < n → False
hpql0 : ↑(mk P) (leadingCoeff (p * q)) ≠ 0
hp0 : p ≠ 0
hq0 : q ≠ 0
hbc0 : degree b = 0 ∧ degree c = 0
hmp : m ≤ natDegree p
hnq : n ≤ natDegree q
hmnd : ¬natDegree p = m
⊢ m + n < natDegree p + natDegree q
[PROOFSTEP]
exact add_lt_add_of_lt_of_le (lt_of_le_of_ne hmp (Ne.symm hmnd)) hnq
[GOAL]
case h.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
m n : ℕ
b c : (R ⧸ P)[X]
hbc : ↑C (↑(mk P) (leadingCoeff (p * q))) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hmn : 0 < m → 0 < n → False
hpql0 : ↑(mk P) (leadingCoeff (p * q)) ≠ 0
hp0 : p ≠ 0
hq0 : q ≠ 0
hbc0 : degree b = 0 ∧ degree c = 0
hmp : m ≤ natDegree p
hnq : n ≤ natDegree q
hmnd : ¬natDegree q = n
⊢ m + n < natDegree p + natDegree q
[PROOFSTEP]
exact add_lt_add_of_le_of_lt hmp (lt_of_le_of_ne hnq (Ne.symm hmnd))
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
m n : ℕ
b c : (R ⧸ P)[X]
hmnd : m + n = natDegree (p * q)
hbc : ↑C (↑(mk P) (leadingCoeff (p * q))) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hmn : 0 < m → 0 < n → False
hpql0 : ↑(mk P) (leadingCoeff (p * q)) ≠ 0
hp0 : p ≠ 0
hq0 : q ≠ 0
hbc0 : degree b = 0 ∧ degree c = 0
hmp : m ≤ natDegree p
hnq : n ≤ natDegree q
hpmqn : natDegree p = m ∧ natDegree q = n
⊢ IsUnit p ∨ IsUnit q
[PROOFSTEP]
obtain rfl | rfl : m = 0 ∨ n = 0 := by
  rwa [pos_iff_ne_zero, pos_iff_ne_zero, imp_false, Classical.not_not, ← or_iff_not_imp_left] at hmn
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
m n : ℕ
b c : (R ⧸ P)[X]
hmnd : m + n = natDegree (p * q)
hbc : ↑C (↑(mk P) (leadingCoeff (p * q))) = b * c
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hmn : 0 < m → 0 < n → False
hpql0 : ↑(mk P) (leadingCoeff (p * q)) ≠ 0
hp0 : p ≠ 0
hq0 : q ≠ 0
hbc0 : degree b = 0 ∧ degree c = 0
hmp : m ≤ natDegree p
hnq : n ≤ natDegree q
hpmqn : natDegree p = m ∧ natDegree q = n
⊢ m = 0 ∨ n = 0
[PROOFSTEP]
rwa [pos_iff_ne_zero, pos_iff_ne_zero, imp_false, Classical.not_not, ← or_iff_not_imp_left] at hmn
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
n : ℕ
b c : (R ⧸ P)[X]
hbc : ↑C (↑(mk P) (leadingCoeff (p * q))) = b * c
hq : map (mk P) q = c * X ^ n
hpql0 : ↑(mk P) (leadingCoeff (p * q)) ≠ 0
hp0 : p ≠ 0
hq0 : q ≠ 0
hbc0 : degree b = 0 ∧ degree c = 0
hnq : n ≤ natDegree q
hmnd : 0 + n = natDegree (p * q)
hp : map (mk P) p = b * X ^ 0
hmn : 0 < 0 → 0 < n → False
hmp : 0 ≤ natDegree p
hpmqn : natDegree p = 0 ∧ natDegree q = n
⊢ IsUnit p ∨ IsUnit q
[PROOFSTEP]
exact Or.inl (isUnit_of_natDegree_eq_zero_of_isPrimitive hu hpmqn.1)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
m : ℕ
b c : (R ⧸ P)[X]
hbc : ↑C (↑(mk P) (leadingCoeff (p * q))) = b * c
hp : map (mk P) p = b * X ^ m
hpql0 : ↑(mk P) (leadingCoeff (p * q)) ≠ 0
hp0 : p ≠ 0
hq0 : q ≠ 0
hbc0 : degree b = 0 ∧ degree c = 0
hmp : m ≤ natDegree p
hmnd : m + 0 = natDegree (p * q)
hq : map (mk P) q = c * X ^ 0
hmn : 0 < m → 0 < 0 → False
hnq : 0 ≤ natDegree q
hpmqn : natDegree p = m ∧ natDegree q = 0
⊢ IsUnit p ∨ IsUnit q
[PROOFSTEP]
exact
  Or.inr (isUnit_of_natDegree_eq_zero_of_isPrimitive (show IsPrimitive (q * p) by simpa [mul_comm] using hu) hpmqn.2)
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : Ideal.IsPrime P
p q : R[X]
hfl : ¬leadingCoeff (p * q) ∈ P
hfP : ∀ (n : ℕ), ↑n < degree (p * q) → coeff (p * q) n ∈ P
hfd0✝ : 0 < degree (p * q)
h0 : ¬coeff (p * q) 0 ∈ P ^ 2
hu : IsPrimitive (p * q)
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = ↑C (↑(mk P) (leadingCoeff (p * q))) * X ^ natDegree (p * q)
hfd0 : 0 < natDegree (p * q)
m : ℕ
b c : (R ⧸ P)[X]
hbc : ↑C (↑(mk P) (leadingCoeff (p * q))) = b * c
hp : map (mk P) p = b * X ^ m
hpql0 : ↑(mk P) (leadingCoeff (p * q)) ≠ 0
hp0 : p ≠ 0
hq0 : q ≠ 0
hbc0 : degree b = 0 ∧ degree c = 0
hmp : m ≤ natDegree p
hmnd : m + 0 = natDegree (p * q)
hq : map (mk P) q = c * X ^ 0
hmn : 0 < m → 0 < 0 → False
hnq : 0 ≤ natDegree q
hpmqn : natDegree p = m ∧ natDegree q = 0
⊢ IsPrimitive (q * p)
[PROOFSTEP]
simpa [mul_comm] using hu


[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
x : R
hx : x ∈ jacobson I
y : R
hxy : I ⊔ span {y * x + 1} = ⊤
p : R
hpi : p ∈ I
q : R
hq : q ∈ span {y * x + 1}
hpq : p + q = 1
r : R
hr : r * (y * x + 1) = q
⊢ r * y * x + r - 1 ∈ I
[PROOFSTEP]
rw [mul_assoc, ← mul_add_one r (y * x), hr, ← hpq, ← neg_sub, add_sub_cancel]
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
x : R
hx : x ∈ jacobson I
y : R
hxy : I ⊔ span {y * x + 1} = ⊤
p : R
hpi : p ∈ I
q : R
hq : q ∈ span {y * x + 1}
hpq : p + q = 1
r : R
hr : r * (y * x + 1) = q
⊢ -p ∈ I
[PROOFSTEP]
exact I.neg_mem hpi
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
x : R
hx : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
M : Ideal R
x✝ : M ∈ {J | I ≤ J ∧ IsMaximal J}
him : I ≤ M
hm : IsMaximal M
hxm : ¬x ∈ M
y i : R
hi : i ∈ M
df : y * x + i = 1
z : R
hz : z * -y * x + z - 1 ∈ I
⊢ z * -y * x + z ∈ M
[PROOFSTEP]
rw [mul_assoc, ← mul_add_one z, neg_mul, ← sub_eq_iff_eq_add.mpr df.symm, neg_sub, sub_add_cancel]
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
x : R
hx : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
M : Ideal R
x✝ : M ∈ {J | I ≤ J ∧ IsMaximal J}
him : I ≤ M
hm : IsMaximal M
hxm : ¬x ∈ M
y i : R
hi : i ∈ M
df : y * x + i = 1
z : R
hz : z * -y * x + z - 1 ∈ I
⊢ z * i ∈ M
[PROOFSTEP]
exact M.mul_mem_left _ hi
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I : Ideal R
r : R
h : r - 1 ∈ jacobson I
⊢ ∃ s, s * r - 1 ∈ I
[PROOFSTEP]
cases' mem_jacobson_iff.1 h 1 with s hs
[GOAL]
case intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I : Ideal R
r : R
h : r - 1 ∈ jacobson I
s : R
hs : s * 1 * (r - 1) + s - 1 ∈ I
⊢ ∃ s, s * r - 1 ∈ I
[PROOFSTEP]
use s
[GOAL]
case h
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I : Ideal R
r : R
h : r - 1 ∈ jacobson I
s : R
hs : s * 1 * (r - 1) + s - 1 ∈ I
⊢ s * r - 1 ∈ I
[PROOFSTEP]
simpa [mul_sub] using hs
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
⊢ jacobson I = I ↔ ∃ M, (∀ (J : Ideal R), J ∈ M → IsMaximal J ∨ J = ⊤) ∧ I = sInf M
[PROOFSTEP]
use fun hI => ⟨{J : Ideal R | I ≤ J ∧ J.IsMaximal}, ⟨fun _ hJ => Or.inl hJ.right, hI.symm⟩⟩
[GOAL]
case mpr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
⊢ (∃ M, (∀ (J : Ideal R), J ∈ M → IsMaximal J ∨ J = ⊤) ∧ I = sInf M) → jacobson I = I
[PROOFSTEP]
rintro ⟨M, hM, hInf⟩
[GOAL]
case mpr.intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
M : Set (Ideal R)
hM : ∀ (J : Ideal R), J ∈ M → IsMaximal J ∨ J = ⊤
hInf : I = sInf M
⊢ jacobson I = I
[PROOFSTEP]
refine le_antisymm (fun x hx => ?_) le_jacobson
[GOAL]
case mpr.intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
M : Set (Ideal R)
hM : ∀ (J : Ideal R), J ∈ M → IsMaximal J ∨ J = ⊤
hInf : I = sInf M
x : R
hx : x ∈ jacobson I
⊢ x ∈ I
[PROOFSTEP]
rw [hInf, mem_sInf]
[GOAL]
case mpr.intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
M : Set (Ideal R)
hM : ∀ (J : Ideal R), J ∈ M → IsMaximal J ∨ J = ⊤
hInf : I = sInf M
x : R
hx : x ∈ jacobson I
⊢ ∀ ⦃I : Ideal R⦄, I ∈ M → x ∈ I
[PROOFSTEP]
intro I hI
[GOAL]
case mpr.intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ : Ideal R
M : Set (Ideal R)
hM : ∀ (J : Ideal R), J ∈ M → IsMaximal J ∨ J = ⊤
hInf : I✝ = sInf M
x : R
hx : x ∈ jacobson I✝
I : Ideal R
hI : I ∈ M
⊢ x ∈ I
[PROOFSTEP]
cases' hM I hI with is_max is_top
[GOAL]
case mpr.intro.intro.inl
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ : Ideal R
M : Set (Ideal R)
hM : ∀ (J : Ideal R), J ∈ M → IsMaximal J ∨ J = ⊤
hInf : I✝ = sInf M
x : R
hx : x ∈ jacobson I✝
I : Ideal R
hI : I ∈ M
is_max : IsMaximal I
⊢ x ∈ I
[PROOFSTEP]
exact (mem_sInf.1 hx) ⟨le_sInf_iff.1 (le_of_eq hInf) I hI, is_max⟩
[GOAL]
case mpr.intro.intro.inr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ : Ideal R
M : Set (Ideal R)
hM : ∀ (J : Ideal R), J ∈ M → IsMaximal J ∨ J = ⊤
hInf : I✝ = sInf M
x : R
hx : x ∈ jacobson I✝
I : Ideal R
hI : I ∈ M
is_top : I = ⊤
⊢ x ∈ I
[PROOFSTEP]
exact is_top.symm ▸ Submodule.mem_top
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
⊢ jacobson I = I ↔ ∀ (x : R), ¬x ∈ I → ∃ M, (I ≤ M ∧ IsMaximal M) ∧ ¬x ∈ M
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
⊢ jacobson I = I → ∀ (x : R), ¬x ∈ I → ∃ M, (I ≤ M ∧ IsMaximal M) ∧ ¬x ∈ M
[PROOFSTEP]
intro h x hx
[GOAL]
case mp
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
h : jacobson I = I
x : R
hx : ¬x ∈ I
⊢ ∃ M, (I ≤ M ∧ IsMaximal M) ∧ ¬x ∈ M
[PROOFSTEP]
erw [← h, mem_sInf] at hx
[GOAL]
case mp
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
h : jacobson I = I
x : R
hx : ¬∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ IsMaximal J} → x ∈ I_1
⊢ ∃ M, (I ≤ M ∧ IsMaximal M) ∧ ¬x ∈ M
[PROOFSTEP]
push_neg at hx
[GOAL]
case mp
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
h : jacobson I = I
x : R
hx : Exists fun ⦃I_1⦄ => I_1 ∈ {J | I ≤ J ∧ IsMaximal J} ∧ ¬x ∈ I_1
⊢ ∃ M, (I ≤ M ∧ IsMaximal M) ∧ ¬x ∈ M
[PROOFSTEP]
exact hx
[GOAL]
case mpr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
⊢ (∀ (x : R), ¬x ∈ I → ∃ M, (I ≤ M ∧ IsMaximal M) ∧ ¬x ∈ M) → jacobson I = I
[PROOFSTEP]
refine fun h => le_antisymm (fun x hx => ?_) le_jacobson
[GOAL]
case mpr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
h : ∀ (x : R), ¬x ∈ I → ∃ M, (I ≤ M ∧ IsMaximal M) ∧ ¬x ∈ M
x : R
hx : x ∈ jacobson I
⊢ x ∈ I
[PROOFSTEP]
contrapose hx
[GOAL]
case mpr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
h : ∀ (x : R), ¬x ∈ I → ∃ M, (I ≤ M ∧ IsMaximal M) ∧ ¬x ∈ M
x : R
hx : ¬x ∈ I
⊢ ¬x ∈ jacobson I
[PROOFSTEP]
erw [mem_sInf]
[GOAL]
case mpr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
h : ∀ (x : R), ¬x ∈ I → ∃ M, (I ≤ M ∧ IsMaximal M) ∧ ¬x ∈ M
x : R
hx : ¬x ∈ I
⊢ ¬∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ IsMaximal J} → x ∈ I_1
[PROOFSTEP]
push_neg
[GOAL]
case mpr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
h : ∀ (x : R), ¬x ∈ I → ∃ M, (I ≤ M ∧ IsMaximal M) ∧ ¬x ∈ M
x : R
hx : ¬x ∈ I
⊢ Exists fun ⦃I_1⦄ => I_1 ∈ {J | I ≤ J ∧ IsMaximal J} ∧ ¬x ∈ I_1
[PROOFSTEP]
exact h x hx
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
⊢ RingHom.ker f ≤ I → map f (jacobson I) = jacobson (map f I)
[PROOFSTEP]
intro h
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
⊢ map f (jacobson I) = jacobson (map f I)
[PROOFSTEP]
unfold Ideal.jacobson
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
⊢ map f (sInf {J | I ≤ J ∧ IsMaximal J}) = sInf {J | map f I ≤ J ∧ IsMaximal J}
[PROOFSTEP]
have : ∀ J ∈ {J : Ideal R | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J := fun J hJ => le_trans h hJ.left
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsMaximal J} → RingHom.ker f ≤ J
⊢ map f (sInf {J | I ≤ J ∧ IsMaximal J}) = sInf {J | map f I ≤ J ∧ IsMaximal J}
[PROOFSTEP]
refine Trans.trans (map_sInf hf this) (le_antisymm ?_ ?_)
[GOAL]
case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsMaximal J} → RingHom.ker f ≤ J
⊢ sInf (map f '' {J | I ≤ J ∧ IsMaximal J}) ≤ sInf {J | map f I ≤ J ∧ IsMaximal J}
[PROOFSTEP]
refine' sInf_le_sInf fun J hJ => ⟨comap f J, ⟨⟨le_comap_of_map_le hJ.1, _⟩, map_comap_of_surjective f hf J⟩⟩
[GOAL]
case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsMaximal J} → RingHom.ker f ≤ J
J : Ideal S
hJ : J ∈ {J | map f I ≤ J ∧ IsMaximal J}
⊢ IsMaximal (comap f J)
[PROOFSTEP]
haveI : J.IsMaximal := hJ.right
[GOAL]
case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
this✝ : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsMaximal J} → RingHom.ker f ≤ J
J : Ideal S
hJ : J ∈ {J | map f I ≤ J ∧ IsMaximal J}
this : IsMaximal J
⊢ IsMaximal (comap f J)
[PROOFSTEP]
exact comap_isMaximal_of_surjective f hf
[GOAL]
case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsMaximal J} → RingHom.ker f ≤ J
⊢ sInf {J | map f I ≤ J ∧ IsMaximal J} ≤ sInf (map f '' {J | I ≤ J ∧ IsMaximal J})
[PROOFSTEP]
refine' sInf_le_sInf_of_subset_insert_top fun j hj => hj.recOn fun J hJ => _
[GOAL]
case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsMaximal J} → RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' {J | I ≤ J ∧ IsMaximal J}
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ IsMaximal J} ∧ map f J = j
⊢ j ∈ insert ⊤ {J | map f I ≤ J ∧ IsMaximal J}
[PROOFSTEP]
rw [← hJ.2]
[GOAL]
case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsMaximal J} → RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' {J | I ≤ J ∧ IsMaximal J}
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ IsMaximal J} ∧ map f J = j
⊢ map f J ∈ insert ⊤ {J | map f I ≤ J ∧ IsMaximal J}
[PROOFSTEP]
cases' map_eq_top_or_isMaximal_of_surjective f hf hJ.left.right with htop hmax
[GOAL]
case refine_2.inl
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsMaximal J} → RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' {J | I ≤ J ∧ IsMaximal J}
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ IsMaximal J} ∧ map f J = j
htop : map f J = ⊤
⊢ map f J ∈ insert ⊤ {J | map f I ≤ J ∧ IsMaximal J}
[PROOFSTEP]
exact htop.symm ▸ Set.mem_insert ⊤ _
[GOAL]
case refine_2.inr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), J ∈ {J | I ≤ J ∧ IsMaximal J} → RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' {J | I ≤ J ∧ IsMaximal J}
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ IsMaximal J} ∧ map f J = j
hmax : IsMaximal (map f J)
⊢ map f J ∈ insert ⊤ {J | map f I ≤ J ∧ IsMaximal J}
[PROOFSTEP]
exact Set.mem_insert_of_mem ⊤ ⟨map_mono hJ.1.1, hmax⟩
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
K : Ideal S
⊢ comap f (jacobson K) = jacobson (comap f K)
[PROOFSTEP]
unfold Ideal.jacobson
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
K : Ideal S
⊢ comap f (sInf {J | K ≤ J ∧ IsMaximal J}) = sInf {J | comap f K ≤ J ∧ IsMaximal J}
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
K : Ideal S
⊢ comap f (sInf {J | K ≤ J ∧ IsMaximal J}) ≤ sInf {J | comap f K ≤ J ∧ IsMaximal J}
[PROOFSTEP]
refine le_trans (comap_mono (le_of_eq (Trans.trans top_inf_eq.symm sInf_insert.symm))) ?_
[GOAL]
case refine'_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
K : Ideal S
⊢ comap f (sInf (insert ⊤ {J | K ≤ J ∧ IsMaximal J})) ≤ sInf {J | comap f K ≤ J ∧ IsMaximal J}
[PROOFSTEP]
rw [comap_sInf', sInf_eq_iInf]
[GOAL]
case refine'_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
K : Ideal S
⊢ ⨅ (I : Ideal R) (_ : I ∈ comap f '' insert ⊤ {J | K ≤ J ∧ IsMaximal J}), I ≤
    ⨅ (a : Ideal R) (_ : a ∈ {J | comap f K ≤ J ∧ IsMaximal J}), a
[PROOFSTEP]
refine' iInf_le_iInf_of_subset fun J hJ => _
[GOAL]
case refine'_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
K : Ideal S
J : Ideal R
hJ : J ∈ {J | comap f K ≤ J ∧ IsMaximal J}
⊢ J ∈ comap f '' insert ⊤ {J | K ≤ J ∧ IsMaximal J}
[PROOFSTEP]
have : comap f (map f J) = J :=
  Trans.trans (comap_map_of_surjective f hf J)
    (le_antisymm (sup_le_iff.2 ⟨le_of_eq rfl, le_trans (comap_mono bot_le) hJ.left⟩) le_sup_left)
[GOAL]
case refine'_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
K : Ideal S
J : Ideal R
hJ : J ∈ {J | comap f K ≤ J ∧ IsMaximal J}
this : comap f (map f J) = J
⊢ J ∈ comap f '' insert ⊤ {J | K ≤ J ∧ IsMaximal J}
[PROOFSTEP]
cases' map_eq_top_or_isMaximal_of_surjective _ hf hJ.right with htop hmax
[GOAL]
case refine'_1.inl
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
K : Ideal S
J : Ideal R
hJ : J ∈ {J | comap f K ≤ J ∧ IsMaximal J}
this : comap f (map f J) = J
htop : map f J = ⊤
⊢ J ∈ comap f '' insert ⊤ {J | K ≤ J ∧ IsMaximal J}
[PROOFSTEP]
exact ⟨⊤, ⟨Set.mem_insert ⊤ _, htop ▸ this⟩⟩
[GOAL]
case refine'_1.inr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
K : Ideal S
J : Ideal R
hJ : J ∈ {J | comap f K ≤ J ∧ IsMaximal J}
this : comap f (map f J) = J
hmax : IsMaximal (map f J)
⊢ J ∈ comap f '' insert ⊤ {J | K ≤ J ∧ IsMaximal J}
[PROOFSTEP]
exact ⟨map f J, ⟨Set.mem_insert_of_mem _ ⟨le_map_of_comap_le_of_surjective f hf hJ.1, hmax⟩, this⟩⟩
[GOAL]
case refine'_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
K : Ideal S
⊢ sInf {J | comap f K ≤ J ∧ IsMaximal J} ≤ comap f (sInf {J | K ≤ J ∧ IsMaximal J})
[PROOFSTEP]
rw [comap_sInf]
[GOAL]
case refine'_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
K : Ideal S
⊢ sInf {J | comap f K ≤ J ∧ IsMaximal J} ≤ ⨅ (I : Ideal S) (_ : I ∈ {J | K ≤ J ∧ IsMaximal J}), comap f I
[PROOFSTEP]
refine' le_iInf_iff.2 fun J => le_iInf_iff.2 fun hJ => _
[GOAL]
case refine'_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
K J : Ideal S
hJ : J ∈ {J | K ≤ J ∧ IsMaximal J}
⊢ sInf {J | comap f K ≤ J ∧ IsMaximal J} ≤ comap f J
[PROOFSTEP]
haveI : J.IsMaximal := hJ.right
[GOAL]
case refine'_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ↑f
K J : Ideal S
hJ : J ∈ {J | K ≤ J ∧ IsMaximal J}
this : IsMaximal J
⊢ sInf {J | comap f K ≤ J ∧ IsMaximal J} ≤ comap f J
[PROOFSTEP]
refine' sInf_le ⟨comap_mono hJ.left, comap_isMaximal_of_surjective _ hf⟩
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I J : Ideal R
⊢ I ≤ J → jacobson I ≤ jacobson J
[PROOFSTEP]
intro h x hx
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I J : Ideal R
h : I ≤ J
x : R
hx : x ∈ jacobson I
⊢ x ∈ jacobson J
[PROOFSTEP]
erw [mem_sInf] at hx ⊢
[GOAL]
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I J : Ideal R
h : I ≤ J
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ IsMaximal J} → x ∈ I_1
⊢ ∀ ⦃I : Ideal R⦄, I ∈ {J_1 | J ≤ J_1 ∧ IsMaximal J_1} → x ∈ I
[PROOFSTEP]
exact fun K ⟨hK, hK_max⟩ => hx ⟨Trans.trans h hK, hK_max⟩
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
r : R
h : r - 1 ∈ jacobson ⊥
⊢ IsUnit r
[PROOFSTEP]
cases' exists_mul_sub_mem_of_sub_one_mem_jacobson r h with s hs
[GOAL]
case intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
r : R
h : r - 1 ∈ jacobson ⊥
s : R
hs : s * r - 1 ∈ ⊥
⊢ IsUnit r
[PROOFSTEP]
rw [mem_bot, sub_eq_zero, mul_comm] at hs
[GOAL]
case intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
r : R
h : r - 1 ∈ jacobson ⊥
s : R
hs : r * s = 1
⊢ IsUnit r
[PROOFSTEP]
exact isUnit_of_mul_eq_one _ _ hs
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
x : R
hx : x ∈ jacobson ⊥
y z : R
hz : z * y * x + z - 1 ∈ ⊥
⊢ (x * y + 1) * z = 1
[PROOFSTEP]
rwa [add_mul, one_mul, ← sub_eq_zero, mul_right_comm, mul_comm _ z, mul_right_comm]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
x : R
h : ∀ (y : R), IsUnit (x * y + 1)
y b : R
hb : (x * y + 1) * b = 1
⊢ b * y * x + b - (x * y + 1) * b = 0
[PROOFSTEP]
ring
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
⊢ jacobson I = I ↔ jacobson ⊥ = ⊥
[PROOFSTEP]
have hf : Function.Surjective (Ideal.Quotient.mk I) := Submodule.Quotient.mk_surjective I
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
⊢ jacobson I = I ↔ jacobson ⊥ = ⊥
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
⊢ jacobson I = I → jacobson ⊥ = ⊥
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : jacobson I = I
⊢ jacobson ⊥ = ⊥
[PROOFSTEP]
replace h := congr_arg (Ideal.map (Ideal.Quotient.mk I)) h
[GOAL]
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : map (Quotient.mk I) (jacobson I) = map (Quotient.mk I) I
⊢ jacobson ⊥ = ⊥
[PROOFSTEP]
rw [map_jacobson_of_surjective hf (le_of_eq mk_ker)] at h
[GOAL]
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : jacobson (map (Quotient.mk I) I) = map (Quotient.mk I) I
⊢ jacobson ⊥ = ⊥
[PROOFSTEP]
simpa using h
[GOAL]
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
⊢ jacobson ⊥ = ⊥ → jacobson I = I
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : jacobson ⊥ = ⊥
⊢ jacobson I = I
[PROOFSTEP]
replace h := congr_arg (comap (Ideal.Quotient.mk I)) h
[GOAL]
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : comap (Quotient.mk I) (jacobson ⊥) = comap (Quotient.mk I) ⊥
⊢ jacobson I = I
[PROOFSTEP]
rw [comap_jacobson_of_surjective hf, ← RingHom.ker_eq_comap_bot (Ideal.Quotient.mk I)] at h
[GOAL]
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : jacobson (RingHom.ker (Quotient.mk I)) = RingHom.ker (Quotient.mk I)
⊢ jacobson I = I
[PROOFSTEP]
simpa using h
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
⊢ radical I = jacobson I ↔ radical ⊥ = jacobson ⊥
[PROOFSTEP]
have hf : Function.Surjective (Ideal.Quotient.mk I) := Submodule.Quotient.mk_surjective I
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
⊢ radical I = jacobson I ↔ radical ⊥ = jacobson ⊥
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
⊢ radical I = jacobson I → radical ⊥ = jacobson ⊥
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : radical I = jacobson I
⊢ radical ⊥ = jacobson ⊥
[PROOFSTEP]
have := congr_arg (map (Ideal.Quotient.mk I)) h
[GOAL]
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : radical I = jacobson I
this : map (Quotient.mk I) (radical I) = map (Quotient.mk I) (jacobson I)
⊢ radical ⊥ = jacobson ⊥
[PROOFSTEP]
rw [map_radical_of_surjective hf (le_of_eq mk_ker), map_jacobson_of_surjective hf (le_of_eq mk_ker)] at this
[GOAL]
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : radical I = jacobson I
this : radical (map (Quotient.mk I) I) = jacobson (map (Quotient.mk I) I)
⊢ radical ⊥ = jacobson ⊥
[PROOFSTEP]
simpa using this
[GOAL]
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
⊢ radical ⊥ = jacobson ⊥ → radical I = jacobson I
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : radical ⊥ = jacobson ⊥
⊢ radical I = jacobson I
[PROOFSTEP]
have := congr_arg (comap (Ideal.Quotient.mk I)) h
[GOAL]
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : radical ⊥ = jacobson ⊥
this : comap (Quotient.mk I) (radical ⊥) = comap (Quotient.mk I) (jacobson ⊥)
⊢ radical I = jacobson I
[PROOFSTEP]
rw [comap_radical, comap_jacobson_of_surjective hf, ← RingHom.ker_eq_comap_bot (Ideal.Quotient.mk I)] at this
[GOAL]
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hf : Function.Surjective ↑(Quotient.mk I)
h : radical ⊥ = jacobson ⊥
this : radical (RingHom.ker (Quotient.mk I)) = jacobson (RingHom.ker (Quotient.mk I))
⊢ radical I = jacobson I
[PROOFSTEP]
simpa using this
[GOAL]
R : Type u
S : Type v
inst✝ : CommRing R
⊢ jacobson ⊥ ≤ sInf (map C '' {J | IsMaximal J})
[PROOFSTEP]
refine' le_sInf fun J => exists_imp.2 fun j hj => _
[GOAL]
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
⊢ jacobson ⊥ ≤ J
[PROOFSTEP]
haveI : j.IsMaximal := hj.1
[GOAL]
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
⊢ jacobson ⊥ ≤ J
[PROOFSTEP]
refine' Trans.trans (jacobson_mono bot_le) (le_of_eq _ : J.jacobson ≤ J)
[GOAL]
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
⊢ jacobson J = J
[PROOFSTEP]
suffices t : (⊥ : Ideal (Polynomial (R ⧸ j))).jacobson = ⊥
  by
  rw [← hj.2, jacobson_eq_iff_jacobson_quotient_eq_bot]
  replace t := congr_arg (map (polynomialQuotientEquivQuotientPolynomial j).toRingHom) t
  rwa [map_jacobson_of_bijective _, map_bot] at t
  exact RingEquiv.bijective (polynomialQuotientEquivQuotientPolynomial j)
[GOAL]
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
t : jacobson ⊥ = ⊥
⊢ jacobson J = J
[PROOFSTEP]
rw [← hj.2, jacobson_eq_iff_jacobson_quotient_eq_bot]
[GOAL]
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
t : jacobson ⊥ = ⊥
⊢ jacobson ⊥ = ⊥
[PROOFSTEP]
replace t := congr_arg (map (polynomialQuotientEquivQuotientPolynomial j).toRingHom) t
[GOAL]
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
t :
  map (RingEquiv.toRingHom (polynomialQuotientEquivQuotientPolynomial j)) (jacobson ⊥) =
    map (RingEquiv.toRingHom (polynomialQuotientEquivQuotientPolynomial j)) ⊥
⊢ jacobson ⊥ = ⊥
[PROOFSTEP]
rwa [map_jacobson_of_bijective _, map_bot] at t
[GOAL]
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
t :
  map (RingEquiv.toRingHom (polynomialQuotientEquivQuotientPolynomial j)) (jacobson ⊥) =
    map (RingEquiv.toRingHom (polynomialQuotientEquivQuotientPolynomial j)) ⊥
⊢ Function.Bijective ↑(RingEquiv.toRingHom (polynomialQuotientEquivQuotientPolynomial j))
[PROOFSTEP]
exact RingEquiv.bijective (polynomialQuotientEquivQuotientPolynomial j)
[GOAL]
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
⊢ jacobson ⊥ = ⊥
[PROOFSTEP]
refine' eq_bot_iff.2 fun f hf => _
[GOAL]
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
f : (R ⧸ j)[X]
hf : f ∈ jacobson ⊥
⊢ f ∈ ⊥
[PROOFSTEP]
have r1 : (X : (R ⧸ j)[X]) ≠ 0 := fun hX =>
  by
  replace hX := congr_arg (fun f => coeff f 1) hX
  simp only [coeff_X_one, coeff_zero] at hX
  exact zero_ne_one hX.symm
[GOAL]
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
f : (R ⧸ j)[X]
hf : f ∈ jacobson ⊥
hX : X = 0
⊢ False
[PROOFSTEP]
replace hX := congr_arg (fun f => coeff f 1) hX
[GOAL]
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
f : (R ⧸ j)[X]
hf : f ∈ jacobson ⊥
hX : (fun f => coeff f 1) X = (fun f => coeff f 1) 0
⊢ False
[PROOFSTEP]
simp only [coeff_X_one, coeff_zero] at hX
[GOAL]
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
f : (R ⧸ j)[X]
hf : f ∈ jacobson ⊥
hX : 1 = 0
⊢ False
[PROOFSTEP]
exact zero_ne_one hX.symm
[GOAL]
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
f : (R ⧸ j)[X]
hf : f ∈ jacobson ⊥
r1 : X ≠ 0
⊢ f ∈ ⊥
[PROOFSTEP]
have r2 := eq_C_of_degree_eq_zero (degree_eq_zero_of_isUnit ((mem_jacobson_bot.1 hf) X))
[GOAL]
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
f : (R ⧸ j)[X]
hf : f ∈ jacobson ⊥
r1 : X ≠ 0
r2 : f * X + 1 = ↑C (coeff (f * X + 1) 0)
⊢ f ∈ ⊥
[PROOFSTEP]
simp only [coeff_add, mul_coeff_zero, coeff_X_zero, mul_zero, coeff_one_zero, zero_add] at r2
[GOAL]
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
f : (R ⧸ j)[X]
hf : f ∈ jacobson ⊥
r1 : X ≠ 0
r2 : f * X + 1 = ↑C 1
⊢ f ∈ ⊥
[PROOFSTEP]
erw [add_left_eq_self] at r2
[GOAL]
R : Type u
S : Type v
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | IsMaximal J} ∧ map C j = J
this : IsMaximal j
f : (R ⧸ j)[X]
hf : f ∈ jacobson ⊥
r1 : X ≠ 0
r2 : f * X = 0
⊢ f ∈ ⊥
[PROOFSTEP]
simpa using (mul_eq_zero.mp r2).resolve_right r1
[GOAL]
R : Type u
S : Type v
inst✝ : CommRing R
h : jacobson ⊥ = ⊥
⊢ jacobson ⊥ = ⊥
[PROOFSTEP]
refine' eq_bot_iff.2 (le_trans jacobson_bot_polynomial_le_sInf_map_maximal _)
[GOAL]
R : Type u
S : Type v
inst✝ : CommRing R
h : jacobson ⊥ = ⊥
⊢ sInf (map C '' {J | IsMaximal J}) ≤ ⊥
[PROOFSTEP]
refine' fun f hf =>
  (Submodule.mem_bot R[X]).2 <| Polynomial.ext fun n => Trans.trans (?_ : coeff f n = 0) (coeff_zero n).symm
[GOAL]
R : Type u
S : Type v
inst✝ : CommRing R
h : jacobson ⊥ = ⊥
f : R[X]
hf : f ∈ sInf (map C '' {J | IsMaximal J})
n : ℕ
⊢ coeff f n = 0
[PROOFSTEP]
suffices f.coeff n ∈ Ideal.jacobson ⊥ by rwa [h, Submodule.mem_bot] at this
[GOAL]
R : Type u
S : Type v
inst✝ : CommRing R
h : jacobson ⊥ = ⊥
f : R[X]
hf : f ∈ sInf (map C '' {J | IsMaximal J})
n : ℕ
this : coeff f n ∈ jacobson ⊥
⊢ coeff f n = 0
[PROOFSTEP]
rwa [h, Submodule.mem_bot] at this
[GOAL]
R : Type u
S : Type v
inst✝ : CommRing R
h : jacobson ⊥ = ⊥
f : R[X]
hf : f ∈ sInf (map C '' {J | IsMaximal J})
n : ℕ
⊢ coeff f n ∈ jacobson ⊥
[PROOFSTEP]
exact mem_sInf.2 fun j hj => (mem_map_C_iff.1 ((mem_sInf.1 hf) ⟨j, ⟨hj.2, rfl⟩⟩)) n
[GOAL]
R : Type u
S : Type v
inst✝ : CommRing R
I : Ideal R
hi : IsLocal I
x : R
h : I ⊔ span {x} = ⊤
p : R
hpi : p ∈ I
q : R
hq : q ∈ span {x}
hpq : p + q = 1
r : R
hr : q = x * r
⊢ r * x - 1 ∈ I
[PROOFSTEP]
rw [← hpq, mul_comm, ← hr, ← neg_sub, add_sub_cancel]
[GOAL]
R : Type u
S : Type v
inst✝ : CommRing R
I : Ideal R
hi : IsLocal I
x : R
h : I ⊔ span {x} = ⊤
p : R
hpi : p ∈ I
q : R
hq : q ∈ span {x}
hpq : p + q = 1
r : R
hr : q = x * r
⊢ -p ∈ I
[PROOFSTEP]
exact I.neg_mem hpi
[GOAL]
R : Type u
S : Type v
inst✝ : CommRing R
I : Ideal R
hi : IsMaximal (radical I)
this : radical I = jacobson I
x y : R
hxy : x * y ∈ I
x✝ : ∃ y_1, y_1 * y - 1 ∈ I
z : R
hz : z * y - 1 ∈ I
⊢ x ∈ I
[PROOFSTEP]
rw [← mul_one x, ← sub_sub_cancel (z * y) 1, mul_sub, mul_left_comm]
[GOAL]
R : Type u
S : Type v
inst✝ : CommRing R
I : Ideal R
hi : IsMaximal (radical I)
this : radical I = jacobson I
x y : R
hxy : x * y ∈ I
x✝ : ∃ y_1, y_1 * y - 1 ∈ I
z : R
hz : z * y - 1 ∈ I
⊢ z * (x * y) - x * (z * y - 1) ∈ I
[PROOFSTEP]
exact I.sub_mem (I.mul_mem_left _ hxy) (I.mul_mem_left _ hz)