R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h : ∀ (n : ℕ) (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
⊢ content (p * q) = content p * content q

case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ ∀ (n : ℕ) (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ content (p * q) = content p * content q
suffices h :
  ∀ (n : ℕ) (p q : R[X]), (p * q).degree < n → (p * q).content = p.content * q.content
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
n : ℕ
⊢ ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ ∀ (n : ℕ) (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
intro n
case h.zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ ∀ (p q : R[X]), degree (p * q) < ↑Nat.zero → content (p * q) = content p * content q

case h.succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
⊢ ∀ (p q : R[X]), degree (p * q) < ↑(Nat.succ n) → content (p * q) = content p * content q
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
n : ℕ
⊢ ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
induction' n with n ih
case h.succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
hpq : degree (p * q) < ↑(Nat.succ n)
⊢ content (p * q) = content p * content q
case h.succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
⊢ ∀ (p q : R[X]), degree (p * q) < ↑(Nat.succ n) → content (p * q) = content p * content q
intro p q hpq
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
hpq : degree (p * q) < ↑(Nat.succ n)
p0 : p = 0
⊢ content (p * q) = content p * content q

case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
hpq : degree (p * q) < ↑(Nat.succ n)
p0 : ¬p = 0
⊢ content (p * q) = content p * content q
case h.succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
hpq : degree (p * q) < ↑(Nat.succ n)
⊢ content (p * q) = content p * content q
by_cases p0 : p = 0
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
hpq : degree (p * q) < ↑(Nat.succ n)
p0 : ¬p = 0
q0 : q = 0
⊢ content (p * q) = content p * content q

case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
hpq : degree (p * q) < ↑(Nat.succ n)
p0 : ¬p = 0
q0 : ¬q = 0
⊢ content (p * q) = content p * content q
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
hpq : degree (p * q) < ↑(Nat.succ n)
p0 : ¬p = 0
⊢ content (p * q) = content p * content q
by_cases q0 : q = 0
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
hpq : degree (p * q) < ↑n ∨ natDegree p + natDegree q = n
p0 : ¬p = 0
q0 : ¬q = 0
⊢ content (p * q) = content p * content q
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
hpq : degree (p * q) < ↑(Nat.succ n)
p0 : ¬p = 0
q0 : ¬q = 0
⊢ content (p * q) = content p * content q
rw [degree_eq_natDegree (mul_ne_zero p0 q0), Nat.cast_withBot,
  Nat.cast_withBot, WithBot.coe_lt_coe, Nat.lt_succ_iff_lt_or_eq, ←
  WithBot.coe_lt_coe, ←Nat.cast_withBot, ← degree_eq_natDegree (mul_ne_zero p0 q0),
  natDegree_mul p0 q0] at hpq
case neg.inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
hlt : degree (p * q) < ↑n
⊢ content (p * q) = content p * content q

case neg.inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : natDegree p + natDegree q = n
⊢ content (p * q) = content p * content q
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
hpq : degree (p * q) < ↑n ∨ natDegree p + natDegree q = n
p0 : ¬p = 0
q0 : ¬q = 0
⊢ content (p * q) = content p * content q
rcases hpq with (hlt | heq)
case neg.inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : degree (primPart p) + degree (primPart q) = ↑n
⊢ content (p * q) = content p * content q
case neg.inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : natDegree p + natDegree q = n
⊢ content (p * q) = content p * content q
rw [← p.natDegree_primPart, ← q.natDegree_primPart, ← WithBot.coe_eq_coe,
  WithBot.coe_add, ← Nat.cast_withBot, ←degree_eq_natDegree p.primPart_ne_zero,
  ← Nat.cast_withBot, ← degree_eq_natDegree q.primPart_ne_zero] at heq
case neg.inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : degree (primPart p) + degree (primPart q) = ↑n
⊢ content (↑C (content p) * primPart p * (↑C (content q) * primPart q)) =
    content (↑C (content p) * primPart p) * content (↑C (content q) * primPart q)
case neg.inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : degree (primPart p) + degree (primPart q) = ↑n
⊢ content (p * q) = content p * content q
rw [p.eq_C_content_mul_primPart, q.eq_C_content_mul_primPart]
case neg.inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : degree (primPart p) + degree (primPart q) = ↑n
h : content (primPart q * primPart p) = 1
⊢ content (↑C (content p) * primPart p * (↑C (content q) * primPart q)) =
    content (↑C (content p) * primPart p) * content (↑C (content q) * primPart q)

case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : degree (primPart p) + degree (primPart q) = ↑n
⊢ content (primPart q * primPart p) = 1
case neg.inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : degree (primPart p) + degree (primPart q) = ↑n
⊢ content (↑C (content p) * primPart p * (↑C (content q) * primPart q)) =
    content (↑C (content p) * primPart p) * content (↑C (content q) * primPart q)
suffices h : (q.primPart * p.primPart).content = 1
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : degree (primPart p) + degree (primPart q) = ↑n
⊢ gcd (content (eraseLead (primPart q * primPart p))) (leadingCoeff (primPart q) * leadingCoeff (primPart p)) ∣ 1
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : degree (primPart p) + degree (primPart q) = ↑n
⊢ content (primPart q * primPart p) = 1
rw [← normalize_content, normalize_eq_one, isUnit_iff_dvd_one,
  content_eq_gcd_leadingCoeff_content_eraseLead, leadingCoeff_mul, gcd_comm]
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : degree (primPart p) + degree (primPart q) = ↑n
⊢ gcd (content (eraseLead (primPart q * primPart p))) (leadingCoeff (primPart q)) *
      gcd (content (eraseLead (primPart q * primPart p))) (leadingCoeff (primPart p)) ∣
    1
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : degree (primPart p) + degree (primPart q) = ↑n
⊢ gcd (content (eraseLead (primPart q * primPart p))) (leadingCoeff (primPart q) * leadingCoeff (primPart p)) ∣ 1
apply (gcd_mul_dvd_mul_gcd _ _ _).trans
case h.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : degree (primPart p) + degree (primPart q) = ↑n
⊢ degree (eraseLead (primPart p) * primPart q) < ↑n

case h.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : degree (primPart p) + degree (primPart q) = ↑n
⊢ degree (eraseLead (primPart q) * primPart p) < ↑n
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : degree (primPart p) + degree (primPart q) = ↑n
⊢ gcd (content (eraseLead (primPart q * primPart p))) (leadingCoeff (primPart q)) *
      gcd (content (eraseLead (primPart q * primPart p))) (leadingCoeff (primPart p)) ∣
    1
rw [content_mul_aux, ih, content_primPart, mul_one, gcd_comm, ←
  content_eq_gcd_leadingCoeff_content_eraseLead, content_primPart, one_mul,
  mul_comm q.primPart, content_mul_aux, ih, content_primPart, mul_one, gcd_comm, ←
  content_eq_gcd_leadingCoeff_content_eraseLead, content_primPart]
case a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h : ∀ (n : ℕ) (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
⊢ degree (p * q) < ↑?n

case n
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h : ∀ (n : ℕ) (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
⊢ ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h : ∀ (n : ℕ) (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
⊢ content (p * q) = content p * content q
apply h
no goals
case a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h : ∀ (n : ℕ) (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
⊢ degree (p * q) < ↑?n

case n
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h : ∀ (n : ℕ) (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
⊢ ℕ
apply lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 (Nat.lt_succ_self _))
case h.zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ p q : R[X]
hpq : degree (p * q) < ↑Nat.zero
⊢ content (p * q) = content p * content q
case h.zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ ∀ (p q : R[X]), degree (p * q) < ↑Nat.zero → content (p * q) = content p * content q
intro p q hpq
case h.zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ p q : R[X]
hpq : degree (p * q) < ↑0
⊢ content (p * q) = content p * content q
case h.zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ p q : R[X]
hpq : degree (p * q) < ↑Nat.zero
⊢ content (p * q) = content p * content q
dsimp at hpq
case h.zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ p q : R[X]
hpq : p = 0 ∨ q = 0
⊢ content (p * q) = content p * content q
case h.zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ p q : R[X]
hpq : degree (p * q) < ↑0
⊢ content (p * q) = content p * content q
rw [Nat.cast_withBot, WithBot.coe_zero,
  Nat.WithBot.lt_zero_iff, degree_eq_bot, mul_eq_zero] at hpq
no goals
case h.zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ p q : R[X]
hpq : p = 0 ∨ q = 0
⊢ content (p * q) = content p * content q
rcases hpq with (rfl | rfl) <;> simp
no goals
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
hpq : degree (p * q) < ↑(Nat.succ n)
p0 : p = 0
⊢ content (p * q) = content p * content q
simp [p0]
no goals
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
hpq : degree (p * q) < ↑(Nat.succ n)
p0 : ¬p = 0
q0 : q = 0
⊢ content (p * q) = content p * content q
simp [q0]
no goals
case neg.inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
hlt : degree (p * q) < ↑n
⊢ content (p * q) = content p * content q
apply ih _ _ hlt
no goals
case neg.inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : degree (primPart p) + degree (primPart q) = ↑n
h : content (primPart q * primPart p) = 1
⊢ content (↑C (content p) * primPart p * (↑C (content q) * primPart q)) =
    content (↑C (content p) * primPart p) * content (↑C (content q) * primPart q)
rw [mul_assoc, content_C_mul, content_C_mul, mul_comm p.primPart, mul_assoc, content_C_mul,
  content_C_mul, h, mul_one, content_primPart, content_primPart, mul_one, mul_one]
case h.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : degree (primPart p) + degree (primPart q) = ↑n
⊢ degree (eraseLead (primPart p)) < degree (primPart p)

case h.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : degree (primPart p) + degree (primPart q) = ↑n
⊢ degree (primPart q) ≠ ⊥
case h.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : degree (primPart p) + degree (primPart q) = ↑n
⊢ degree (eraseLead (primPart p) * primPart q) < ↑n
rw [Nat.cast_withBot, ← heq, degree_mul, WithBot.add_lt_add_iff_right]
no goals
case h.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : degree (primPart p) + degree (primPart q) = ↑n
⊢ degree (eraseLead (primPart p)) < degree (primPart p)
apply degree_erase_lt p.primPart_ne_zero
case h.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : degree (primPart p) + degree (primPart q) = ↑n
⊢ ¬primPart q = 0
case h.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : degree (primPart p) + degree (primPart q) = ↑n
⊢ degree (primPart q) ≠ ⊥
rw [Ne.def, degree_eq_bot]
no goals
case h.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : degree (primPart p) + degree (primPart q) = ↑n
⊢ ¬primPart q = 0
apply q.primPart_ne_zero
case h.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : degree (primPart p) + degree (primPart q) = ↑n
⊢ degree (eraseLead (primPart q)) < degree (primPart q)

case h.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : degree (primPart p) + degree (primPart q) = ↑n
⊢ degree (primPart p) ≠ ⊥
case h.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : degree (primPart p) + degree (primPart q) = ↑n
⊢ degree (eraseLead (primPart q) * primPart p) < ↑n
rw [mul_comm, Nat.cast_withBot, ← heq, degree_mul, WithBot.add_lt_add_iff_left]
no goals
case h.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : degree (primPart p) + degree (primPart q) = ↑n
⊢ degree (eraseLead (primPart q)) < degree (primPart q)
apply degree_erase_lt q.primPart_ne_zero
case h.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : degree (primPart p) + degree (primPart q) = ↑n
⊢ ¬primPart p = 0
case h.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : degree (primPart p) + degree (primPart q) = ↑n
⊢ degree (primPart p) ≠ ⊥
rw [Ne.def, degree_eq_bot]
no goals
case h.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), degree (p * q) < ↑n → content (p * q) = content p * content q
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : degree (primPart p) + degree (primPart q) = ↑n
⊢ ¬primPart p = 0
apply p.primPart_ne_zero