-- Mathlib/RingTheory/Polynomial/Content.lean
theorem content_mul {p q : R[X]} : (p * q).content = p.content * q.content

Proof state:
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]), (p * q).degree < ↑n → (p * q).content = p.content * q.content
p q : R[X]
hpq : (p * q).degree < ↑n ∨ p.natDegree + q.natDegree = n
p0 : ¬p = 0
q0 : ¬q = 0
⊢ (p * q).content = p.content * q.content

Tactic:
rcases hpq with (hlt | heq)

Result:
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]), (p * q).degree < ↑n → (p * q).content = p.content * q.content
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
hlt : (p * q).degree < ↑n
⊢ (p * q).content = p.content * q.content

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]), (p * q).degree < ↑n → (p * q).content = p.content * q.content
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.natDegree + q.natDegree = n
⊢ (p * q).content = p.content * q.content

Proof state:
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]), (p * q).degree < ↑n → (p * q).content = p.content * q.content
p q : R[X]
hpq : (p * q).degree < ↑(n + 1)
p0 : ¬p = 0
q0 : q = 0
⊢ (p * q).content = p.content * q.content

Tactic:
simp [q0]

Result:
no goals

Proof state:
case neg.inr.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → (p * q).content = p.content * q.content
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ q.primPart.eraseLead.degree < q.primPart.degree

Tactic:
apply degree_erase_lt q.primPart_ne_zero

Result:
no goals

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

Tactic:
induction' n with n ih

Result:
case zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ ∀ (p q : R[X]), (p * q).degree < ↑0 → (p * q).content = p.content * q.content

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

Proof state:
case neg.inr.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → (p * q).content = p.content * q.content
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ ¬q.primPart = 0

Tactic:
apply q.primPart_ne_zero

Result:
no goals

Proof state:
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]), (p * q).degree < ↑n → (p * q).content = p.content * q.content
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.natDegree + q.natDegree = n
⊢ (p * q).content = p.content * q.content

Tactic:
rw [← p.natDegree_primPart, ← q.natDegree_primPart, ← Nat.cast_inj (R := WithBot ℕ),
  Nat.cast_add, ← degree_eq_natDegree p.primPart_ne_zero,
  ← degree_eq_natDegree q.primPart_ne_zero] at heq

Result:
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]), (p * q).degree < ↑n → (p * q).content = p.content * q.content
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ (p * q).content = p.content * q.content

Proof state:
case neg.inr.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → (p * q).content = p.content * q.content
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ p.primPart.degree ≠ ⊥

Tactic:
rw [Ne, degree_eq_bot]

Result:
case neg.inr.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → (p * q).content = p.content * q.content
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ ¬p.primPart = 0

Proof state:
case succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → (p * q).content = p.content * q.content
⊢ ∀ (p q : R[X]), (p * q).degree < ↑(n + 1) → (p * q).content = p.content * q.content

Tactic:
intro p q hpq

Result:
case succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → (p * q).content = p.content * q.content
p q : R[X]
hpq : (p * q).degree < ↑(n + 1)
⊢ (p * q).content = p.content * q.content

Proof state:
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]), (p * q).degree < ↑n → (p * q).content = p.content * q.content
p q : R[X]
hpq : (p * q).degree < ↑(n + 1)
p0 : p = 0
⊢ (p * q).content = p.content * q.content

Tactic:
simp [p0]

Result:
no goals

Proof state:
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]), (p * q).degree < ↑n → (p * q).content = p.content * q.content
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ (C p.content * p.primPart * (C q.content * q.primPart)).content =
    (C p.content * p.primPart).content * (C q.content * q.primPart).content

Tactic:
suffices h : (q.primPart * p.primPart).content = 1 by
  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]

Result:
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]), (p * q).degree < ↑n → (p * q).content = p.content * q.content
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ (q.primPart * p.primPart).content = 1

Proof state:
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]), (p * q).degree < ↑n → (p * q).content = p.content * q.content
⊢ (p * q).degree < ↑?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]), (p * q).degree < ↑n → (p * q).content = p.content * q.content
⊢ ℕ

Tactic:
apply lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 (Nat.lt_succ_self _))

Result:
no goals

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

Tactic:
intro n

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