R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
⊢ ∃ r, IsPrimitive r ∧ ∀ (s : R[X]), p ∣ s ∧ q ∣ s ↔ r ∣ s
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
⊢ ∃ r, IsPrimitive r ∧ ∀ (s : R[X]), p ∣ s ∧ q ∣ s ↔ r ∣ s
have h : ∃ (n : ℕ)(r : R[X]), r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r :=
  ⟨(p * q).natDegree, p * q, rfl, hp.mul hq, dvd_mul_right _ _, dvd_mul_left _ _⟩
case intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
⊢ ∃ r, IsPrimitive r ∧ ∀ (s : R[X]), p ∣ s ∧ q ∣ s ↔ r ∣ s
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
⊢ ∃ r, IsPrimitive r ∧ ∀ (s : R[X]), p ∣ s ∧ q ∣ s ↔ r ∣ s
rcases Nat.find_spec h with ⟨r, rdeg, rprim, pr, qr⟩
case intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
s : R[X]
⊢ p ∣ s ∧ q ∣ s → r ∣ s
case intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
⊢ ∃ r, IsPrimitive r ∧ ∀ (s : R[X]), p ∣ s ∧ q ∣ s ↔ r ∣ s
refine' ⟨r, rprim, fun s => ⟨_, fun rs => ⟨pr.trans rs, qr.trans rs⟩⟩⟩
case intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
s : R[X]
hs : ∀ (n : ℕ) (s : R[X]), natDegree s = n → p ∣ s ∧ q ∣ s → r ∣ s
⊢ p ∣ s ∧ q ∣ s → r ∣ s

case hs
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
s : R[X]
⊢ ∀ (n : ℕ) (s : R[X]), natDegree s = n → p ∣ s ∧ q ∣ s → r ∣ s
case intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
s : R[X]
⊢ p ∣ s ∧ q ∣ s → r ∣ s
suffices hs : ∀ (n : ℕ) (s : R[X]), s.natDegree = n → p ∣ s ∧ q ∣ s → r ∣ s
case hs
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
⊢ ∀ (n : ℕ) (s : R[X]), natDegree s = n → p ∣ s ∧ q ∣ s → r ∣ s
case hs
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
s : R[X]
⊢ ∀ (n : ℕ) (s : R[X]), natDegree s = n → p ∣ s ∧ q ∣ s → r ∣ s
clear s
case hs
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
⊢ False
case hs
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
⊢ ∀ (n : ℕ) (s : R[X]), natDegree s = n → p ∣ s ∧ q ∣ s → r ∣ s
by_contra' con
case hs.intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
⊢ False
case hs
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
⊢ False
rcases Nat.find_spec con with ⟨s, sdeg, ⟨ps, qs⟩, rs⟩
case hs.intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
⊢ False
case hs.intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
⊢ False
have s0 : s ≠ 0 := by
  contrapose! rs
  simp [rs]
case hs.intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : Nat.find h ≤ natDegree s
⊢ False
case hs.intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
⊢ False
have hs :=
  Nat.find_min' h
    ⟨_, s.natDegree_primPart, s.isPrimitive_primPart, (hp.dvd_primPart_iff_dvd s0).2 ps,
      (hq.dvd_primPart_iff_dvd s0).2 qs⟩
case hs.intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
⊢ False
case hs.intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : Nat.find h ≤ natDegree s
⊢ False
rw [← rdeg] at hs
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : natDegree s ≤ 0
⊢ False

case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : ¬natDegree s ≤ 0
⊢ False
case hs.intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
⊢ False
by_cases sC : s.natDegree ≤ 0
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : ¬natDegree s ≤ 0
hcancel : natDegree (cancelLeads r s) < natDegree s
⊢ False
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : ¬natDegree s ≤ 0
⊢ False
have hcancel := natDegree_cancelLeads_lt_of_natDegree_le_natDegree hs (lt_of_not_ge sC)
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : ¬natDegree s ≤ 0
hcancel : natDegree (cancelLeads r s) < Nat.find con
⊢ False
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : ¬natDegree s ≤ 0
hcancel : natDegree (cancelLeads r s) < natDegree s
⊢ False
rw [sdeg] at hcancel
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : ¬natDegree s ≤ 0
hcancel : natDegree (cancelLeads r s) < Nat.find con
⊢ ∃ s_1, natDegree s_1 = natDegree (cancelLeads r s) ∧ (p ∣ s_1 ∧ q ∣ s_1) ∧ ¬r ∣ s_1
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : ¬natDegree s ≤ 0
hcancel : natDegree (cancelLeads r s) < Nat.find con
⊢ False
apply Nat.find_min con hcancel
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : ¬natDegree s ≤ 0
hcancel : natDegree (cancelLeads r s) < Nat.find con
rcs : r ∣ cancelLeads r s
⊢ r ∣ s
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : ¬natDegree s ≤ 0
hcancel : natDegree (cancelLeads r s) < Nat.find con
⊢ ∃ s_1, natDegree s_1 = natDegree (cancelLeads r s) ∧ (p ∣ s_1 ∧ q ∣ s_1) ∧ ¬r ∣ s_1
refine'
  ⟨_, rfl, ⟨dvd_cancelLeads_of_dvd_of_dvd pr ps, dvd_cancelLeads_of_dvd_of_dvd qr qs⟩,
    fun rcs => rs _⟩
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : ¬natDegree s ≤ 0
hcancel : natDegree (cancelLeads r s) < Nat.find con
rcs : r ∣ cancelLeads r s
⊢ r ∣ primPart s
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : ¬natDegree s ≤ 0
hcancel : natDegree (cancelLeads r s) < Nat.find con
rcs : r ∣ cancelLeads r s
⊢ r ∣ s
rw [← rprim.dvd_primPart_iff_dvd s0]
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : ¬natDegree s ≤ 0
hcancel : natDegree (cancelLeads r s) < Nat.find con
rcs : r ∣ ↑C (leadingCoeff r) * s - ↑C (leadingCoeff s) * X ^ (natDegree s - natDegree r) * r
⊢ r ∣ primPart s
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : ¬natDegree s ≤ 0
hcancel : natDegree (cancelLeads r s) < Nat.find con
rcs : r ∣ cancelLeads r s
⊢ r ∣ primPart s
rw [cancelLeads, tsub_eq_zero_iff_le.mpr hs, pow_zero, mul_one] at rcs
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h✝ : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h✝
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : ¬natDegree s ≤ 0
hcancel : natDegree (cancelLeads r s) < Nat.find con
rcs : r ∣ ↑C (leadingCoeff r) * s - ↑C (leadingCoeff s) * X ^ (natDegree s - natDegree r) * r
h :
  r ∣
    ↑C (leadingCoeff r) * s - ↑C (leadingCoeff s) * X ^ (natDegree s - natDegree r) * r +
      ↑C (leadingCoeff s) * X ^ (natDegree s - natDegree r) * r
⊢ r ∣ primPart s
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : ¬natDegree s ≤ 0
hcancel : natDegree (cancelLeads r s) < Nat.find con
rcs : r ∣ ↑C (leadingCoeff r) * s - ↑C (leadingCoeff s) * X ^ (natDegree s - natDegree r) * r
⊢ r ∣ primPart s
have h :=
  dvd_add rcs (Dvd.intro_left (C (leadingCoeff s) * X ^ (natDegree s - natDegree r)) rfl)
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h✝ : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h✝
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : ¬natDegree s ≤ 0
hcancel : natDegree (cancelLeads r s) < Nat.find con
rcs : r ∣ ↑C (leadingCoeff r) * s - ↑C (leadingCoeff s) * X ^ (natDegree s - natDegree r) * r
h :
  r ∣
    ↑C (leadingCoeff r) * s - ↑C (leadingCoeff s) * X ^ (natDegree s - natDegree r) * r +
      ↑C (leadingCoeff s) * X ^ (natDegree s - natDegree r) * r
hC0 : r ≠ 0
⊢ r ∣ primPart s
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h✝ : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h✝
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : ¬natDegree s ≤ 0
hcancel : natDegree (cancelLeads r s) < Nat.find con
rcs : r ∣ ↑C (leadingCoeff r) * s - ↑C (leadingCoeff s) * X ^ (natDegree s - natDegree r) * r
h :
  r ∣
    ↑C (leadingCoeff r) * s - ↑C (leadingCoeff s) * X ^ (natDegree s - natDegree r) * r +
      ↑C (leadingCoeff s) * X ^ (natDegree s - natDegree r) * r
⊢ r ∣ primPart s
have hC0 := rprim.ne_zero
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h✝ : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h✝
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : ¬natDegree s ≤ 0
hcancel : natDegree (cancelLeads r s) < Nat.find con
rcs : r ∣ ↑C (leadingCoeff r) * s - ↑C (leadingCoeff s) * X ^ (natDegree s - natDegree r) * r
h :
  r ∣
    ↑C (leadingCoeff r) * s - ↑C (leadingCoeff s) * X ^ (natDegree s - natDegree r) * r +
      ↑C (leadingCoeff s) * X ^ (natDegree s - natDegree r) * r
hC0 : ¬↑C (leadingCoeff r) = 0
⊢ r ∣ primPart s
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h✝ : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h✝
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : ¬natDegree s ≤ 0
hcancel : natDegree (cancelLeads r s) < Nat.find con
rcs : r ∣ ↑C (leadingCoeff r) * s - ↑C (leadingCoeff s) * X ^ (natDegree s - natDegree r) * r
h :
  r ∣
    ↑C (leadingCoeff r) * s - ↑C (leadingCoeff s) * X ^ (natDegree s - natDegree r) * r +
      ↑C (leadingCoeff s) * X ^ (natDegree s - natDegree r) * r
hC0 : r ≠ 0
⊢ r ∣ primPart s
rw [Ne.def, ← leadingCoeff_eq_zero, ← C_eq_zero] at hC0
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h✝ : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h✝
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : ¬natDegree s ≤ 0
hcancel : natDegree (cancelLeads r s) < Nat.find con
rcs : r ∣ ↑C (leadingCoeff r) * s - ↑C (leadingCoeff s) * X ^ (natDegree s - natDegree r) * r
h : r ∣ primPart (↑C (leadingCoeff r) * s)
hC0 : ¬↑C (leadingCoeff r) = 0
⊢ r ∣ primPart s
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h✝ : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h✝
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : ¬natDegree s ≤ 0
hcancel : natDegree (cancelLeads r s) < Nat.find con
rcs : r ∣ ↑C (leadingCoeff r) * s - ↑C (leadingCoeff s) * X ^ (natDegree s - natDegree r) * r
h :
  r ∣
    ↑C (leadingCoeff r) * s - ↑C (leadingCoeff s) * X ^ (natDegree s - natDegree r) * r +
      ↑C (leadingCoeff s) * X ^ (natDegree s - natDegree r) * r
hC0 : ¬↑C (leadingCoeff r) = 0
⊢ r ∣ primPart s
rw [sub_add_cancel, ← rprim.dvd_primPart_iff_dvd (mul_ne_zero hC0 s0)] at h
case neg.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h✝ : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h✝
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : ¬natDegree s ≤ 0
hcancel : natDegree (cancelLeads r s) < Nat.find con
rcs : r ∣ ↑C (leadingCoeff r) * s - ↑C (leadingCoeff s) * X ^ (natDegree s - natDegree r) * r
h : r ∣ primPart (↑C (leadingCoeff r) * s)
hC0 : ¬↑C (leadingCoeff r) = 0
u : R[X]ˣ
hu : ↑u = primPart (↑C (leadingCoeff r))
⊢ r ∣ primPart s
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h✝ : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h✝
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : ¬natDegree s ≤ 0
hcancel : natDegree (cancelLeads r s) < Nat.find con
rcs : r ∣ ↑C (leadingCoeff r) * s - ↑C (leadingCoeff s) * X ^ (natDegree s - natDegree r) * r
h : r ∣ primPart (↑C (leadingCoeff r) * s)
hC0 : ¬↑C (leadingCoeff r) = 0
⊢ r ∣ primPart s
rcases isUnit_primPart_C r.leadingCoeff with ⟨u, hu⟩
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h✝ : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h✝
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : ¬natDegree s ≤ 0
hcancel : natDegree (cancelLeads r s) < Nat.find con
rcs : r ∣ ↑C (leadingCoeff r) * s - ↑C (leadingCoeff s) * X ^ (natDegree s - natDegree r) * r
h : r ∣ primPart (↑C (leadingCoeff r) * s)
hC0 : ¬↑C (leadingCoeff r) = 0
u : R[X]ˣ
hu : ↑u = primPart (↑C (leadingCoeff r))
⊢ primPart s * ↑u = primPart (↑C (leadingCoeff r) * s)
case neg.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h✝ : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h✝
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : ¬natDegree s ≤ 0
hcancel : natDegree (cancelLeads r s) < Nat.find con
rcs : r ∣ ↑C (leadingCoeff r) * s - ↑C (leadingCoeff s) * X ^ (natDegree s - natDegree r) * r
h : r ∣ primPart (↑C (leadingCoeff r) * s)
hC0 : ¬↑C (leadingCoeff r) = 0
u : R[X]ˣ
hu : ↑u = primPart (↑C (leadingCoeff r))
⊢ r ∣ primPart s
apply h.trans (Associated.symm ⟨u, _⟩).dvd
no goals
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h✝ : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h✝
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : ¬natDegree s ≤ 0
hcancel : natDegree (cancelLeads r s) < Nat.find con
rcs : r ∣ ↑C (leadingCoeff r) * s - ↑C (leadingCoeff s) * X ^ (natDegree s - natDegree r) * r
h : r ∣ primPart (↑C (leadingCoeff r) * s)
hC0 : ¬↑C (leadingCoeff r) = 0
u : R[X]ˣ
hu : ↑u = primPart (↑C (leadingCoeff r))
⊢ primPart s * ↑u = primPart (↑C (leadingCoeff r) * s)
rw [primPart_mul (mul_ne_zero hC0 s0), hu, mul_comm]
no goals
case intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
s : R[X]
hs : ∀ (n : ℕ) (s : R[X]), natDegree s = n → p ∣ s ∧ q ∣ s → r ∣ s
⊢ p ∣ s ∧ q ∣ s → r ∣ s
apply hs s.natDegree s rfl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
ps : p ∣ s
qs : q ∣ s
rs : s = 0
⊢ r ∣ s
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
⊢ s ≠ 0
contrapose! rs
no goals
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
ps : p ∣ s
qs : q ∣ s
rs : s = 0
⊢ r ∣ s
simp [rs]
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim✝ : IsPrimitive (↑C (coeff r 0))
rprim : IsUnit (coeff r 0)
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : natDegree s ≤ 0
⊢ False
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim : IsPrimitive r
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : natDegree s ≤ 0
⊢ False
rw [eq_C_of_natDegree_le_zero (le_trans hs sC), isPrimitive_iff_content_eq_one, content_C,
  normalize_eq_one] at rprim
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim✝ : IsPrimitive (↑C (coeff r 0))
rprim : IsUnit (coeff r 0)
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs✝ : ¬↑C (coeff r 0) ∣ s
rs : ¬coeff r 0 ∣ content s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : natDegree s ≤ 0
⊢ False
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim✝ : IsPrimitive (↑C (coeff r 0))
rprim : IsUnit (coeff r 0)
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : natDegree s ≤ 0
⊢ False
rw [eq_C_of_natDegree_le_zero (le_trans hs sC), ← dvd_content_iff_C_dvd] at rs
no goals
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h : ∃ n r, natDegree r = n ∧ IsPrimitive r ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : natDegree r = Nat.find h
rprim✝ : IsPrimitive (↑C (coeff r 0))
rprim : IsUnit (coeff r 0)
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, natDegree s = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : natDegree s = Nat.find con
rs✝ : ¬↑C (coeff r 0) ∣ s
rs : ¬coeff r 0 ∣ content s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : natDegree r ≤ natDegree s
sC : natDegree s ≤ 0
⊢ False
apply rs rprim.dvd