-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc :
  map (algebraMap R K) (integerNormalization R⁰ a) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) c) : K[X]) a
d : R
d0 : d ≠ 0
hd :
  map (algebraMap R K) (integerNormalization R⁰ b) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) d) : K[X]) b
hcd0 : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) (c * d) : R[X]) (0 : R[X])
h1 :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) ((C : (a : R) → R[X]) d : R[X]) * p =
    HMul.hMul (α := R[X]) (integerNormalization R⁰ a) (integerNormalization R⁰ b)
this : NormalizedGCDMonoid R
rw :
  c * d ∣ HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b)) ∧
    HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b)) ∣ c * d
rw₁ :
  Eq (α := R) ((normalize : (a : R) → R) (c * d) : R)
    ((normalize : (a : R) → R)
        (HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b))) :
      R)
rw₂ :
  HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) c : R) ((normalize : (a : R) → R) d : R) =
    (normalize : (a : R) → R)
      (HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b)))
rw₃ :
  HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) c : R) ((normalize : (a : R) → R) d : R) =
    HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) (content (integerNormalization R⁰ a)) : R)
      ((normalize : (a : R) → R) (content (integerNormalization R⁰ b)) : R)
rw₄ :
  HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) c : R) ((normalize : (a : R) → R) d : R) =
    HMul.hMul (α := R) (β := R) (content (integerNormalization R⁰ a) : R)
      ((normalize : (a : R) → R) (content (integerNormalization R⁰ b)) : R)
rw₅ :
  HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) c : R) ((normalize : (a : R) → R) d : R) =
    HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b))
rw₆ :
  HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) c : R) ((normalize : (a : R) → R) d : R) * 1 =
    HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b))
rw₇ :
  HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) c : R) ((normalize : (a : R) → R) d : R) * p.content =
    HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b))
rw₈ :
  HMul.hMul (α := R) (β := R) (content ((C : (a : R) → R[X]) c) : R) ((normalize : (a : R) → R) d : R) * p.content =
    HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b))
rw₉ :
  HMul.hMul (α := R) (content ((C : (a : R) → R[X]) c)) (content ((C : (a : R) → R[X]) d)) * p.content =
    HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b))
rw₁₀ :
  (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) ((C : (a : R) → R[X]) d : R[X])).content *
      p.content =
    HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b))
rw₁₁ :
  (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) ((C : (a : R) → R[X]) d : R[X]) * p).content =
    HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b))
rw₁₂ :
  (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) ((C : (a : R) → R[X]) d : R[X]) * p).content =
    (HMul.hMul (α := R[X]) (integerNormalization R⁰ a) (integerNormalization R⁰ b)).content
rw₁₃ rw₁₄ :
  (HMul.hMul (α := R[X]) (integerNormalization R⁰ a) (integerNormalization R⁰ b)).content =
    (HMul.hMul (α := R[X]) (integerNormalization R⁰ a) (integerNormalization R⁰ b)).content
⊢ Associated (c * d) (HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b)))

Tactic:
rw [← dvd_dvd_iff_associated, ← normalize_eq_normalize_iff, normalize.map_mul,
      normalize.map_mul, normalize_content, normalize_content, ←
      mul_one (normalize c * normalize d), ← hp.content_eq_one, ← content_C, ← content_C, ←
      content_mul, ← content_mul, ← content_mul, h1]

Premises used: HMul.hMul, normalize_eq_normalize_iff, Polynomial.IsPrimitive.content_eq_one, Polynomial.normalize_content, dvd_dvd_iff_associated, Polynomial.content_mul, Polynomial.content_C, normalize, mul_one, MonoidWithZeroHom.map_mul, DFunLike.coe