[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
