-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p_1 q_1 : R[X]
h_1 : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]) (hpq : (p * q).degree < (↑n : WithBot ℕ)), (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 : WithBot ℕ)
h : (q.primPart * p.primPart).content = 1
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X])
        (p.primPart * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) q.primPart)).content =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart).content *
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) q.primPart).content
rw₁ :
  HMul.hMul (α := R) ((normalize : (a : R) → R) p.content : R)
      (p.primPart * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) q.primPart).content =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart).content *
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) q.primPart).content
rw₂ :
  HMul.hMul (α := R) ((normalize : (a : R) → R) p.content : R)
      (p.primPart * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) q.primPart).content =
    HMul.hMul (α := R) ((normalize : (a : R) → R) p.content : R) p.primPart.content *
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) q.primPart).content
rw₃ :
  HMul.hMul (α := R) ((normalize : (a : R) → R) p.content : R)
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) q.primPart * p.primPart).content =
    HMul.hMul (α := R) ((normalize : (a : R) → R) p.content : R) p.primPart.content *
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) q.primPart).content
rw₄ :
  HMul.hMul (α := R) ((normalize : (a : R) → R) p.content : R)
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) (q.primPart * p.primPart)).content =
    HMul.hMul (α := R) ((normalize : (a : R) → R) p.content : R) p.primPart.content *
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) q.primPart).content
rw₅ :
  HMul.hMul (α := R) ((normalize : (a : R) → R) p.content : R)
      (HMul.hMul (α := R) ((normalize : (a : R) → R) q.content : R) (q.primPart * p.primPart).content) =
    HMul.hMul (α := R) ((normalize : (a : R) → R) p.content : R) p.primPart.content *
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) q.primPart).content
rw₆ :
  HMul.hMul (α := R) ((normalize : (a : R) → R) p.content : R)
      (HMul.hMul (α := R) ((normalize : (a : R) → R) q.content : R) (q.primPart * p.primPart).content) =
    HMul.hMul (α := R) ((normalize : (a : R) → R) p.content : R) p.primPart.content *
      HMul.hMul (α := R) ((normalize : (a : R) → R) q.content : R) q.primPart.content
rw₇ :
  HMul.hMul (α := R) ((normalize : (a : R) → R) p.content : R)
      (HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) q.content : R) (1 : R)) =
    HMul.hMul (α := R) ((normalize : (a : R) → R) p.content : R) p.primPart.content *
      HMul.hMul (α := R) ((normalize : (a : R) → R) q.content : R) q.primPart.content
rw₈ :
  HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) p.content : R) ((normalize : (a : R) → R) q.content : R) =
    HMul.hMul (α := R) ((normalize : (a : R) → R) p.content : R) p.primPart.content *
      HMul.hMul (α := R) ((normalize : (a : R) → R) q.content : R) q.primPart.content
rw₉ :
  HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) p.content : R) ((normalize : (a : R) → R) q.content : R) =
    HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) p.content : R) (1 : R) *
      HMul.hMul (α := R) ((normalize : (a : R) → R) q.content : R) q.primPart.content
rw₁₀ :
  HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) p.content : R) ((normalize : (a : R) → R) q.content : R) =
    HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) p.content : R) (1 : R) *
      HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) q.content : R) (1 : R)
rw₁₁ :
  HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) p.content : R) ((normalize : (a : R) → R) q.content : R) =
    HMul.hMul (α := R) ((normalize : (a : R) → R) p.content : R)
      (HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) q.content : R) (1 : R))
rw₁₂ rw₁₃ :
  HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) p.content : R) ((normalize : (a : R) → R) q.content : R) =
    HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) p.content : R) ((normalize : (a : R) → R) q.content : R)
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart *
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) q.primPart).content =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart).content *
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) q.primPart).content

Tactic:
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]

Premises used: mul_assoc, Polynomial.content_C_mul, Polynomial.primPart, mul_comm, Polynomial.content_primPart, mul_one