-- Mathlib/RingTheory/Polynomial/GaussLemma.lean
theorem IsPrimitive.dvd_of_fraction_map_dvd_fraction_map {p q : R[X]} (hp : p.IsPrimitive)
    (hq : q.IsPrimitive) (h_dvd : p.map (algebraMap R K) ∣ q.map (algebraMap R K)) : p ∣ q

Proof state:
case intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
hs : map (algebraMap R K) (integerNormalization R⁰ r) = C ((algebraMap R K) s) * r
h : p ∣ q * C s
s0 : s = 0
⊢ s ∉ R⁰

Tactic:
simp [s0, mem_nonZeroDivisors_iff_ne_zero]

Result:
no goals

Proof state:
case h.a
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = C ((algebraMap R K) s) * r
⊢ map (algebraMap R K) (q * C s) = map (algebraMap R K) (p * integerNormalization R⁰ r)

Tactic:
rw [Polynomial.map_mul, Polynomial.map_mul, hs, hr, mul_assoc, mul_comm r]

Result:
case h.a
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = C ((algebraMap R K) s) * r
⊢ map (algebraMap R K) p * (map (algebraMap R K) (C s) * r) = map (algebraMap R K) p * (C ((algebraMap R K) s) * r)

Proof state:
case intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = C ((algebraMap R K) s) * r
⊢ p ∣ q

Tactic:
have h : p ∣ q * C s := by
  use integerNormalization R⁰ r
  apply map_injective (algebraMap R K) (IsFractionRing.injective _ _)
  rw [Polynomial.map_mul, Polynomial.map_mul, hs, hr, mul_assoc, mul_comm r]
  simp

Result:
case intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = C ((algebraMap R K) s) * r
h : p ∣ q * C s
⊢ p ∣ q

Proof state:
case intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = C ((algebraMap R K) s) * r
h : p ∣ q * C s
⊢ p ∣ q

Tactic:
rw [← hp.dvd_primPart_iff_dvd, primPart_mul, hq.primPart_eq, Associated.dvd_iff_dvd_right] at h

Result:
case intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = C ((algebraMap R K) s) * r
h✝ : p ∣ q * (C s).primPart
h : p ∣ ?m.82819
⊢ p ∣ q

case intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = C ((algebraMap R K) s) * r
h : p ∣ q * (C s).primPart
⊢ Associated (q * (C s).primPart) ?m.82819

R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = C ((algebraMap R K) s) * r
h : p ∣ q * (C s).primPart
⊢ R[X]

case intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = C ((algebraMap R K) s) * r
h : p ∣ (q * C s).primPart
⊢ q * C s ≠ 0

case intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = C ((algebraMap R K) s) * r
h : p ∣ q * C s
⊢ q * C s ≠ 0

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h_dvd : map (algebraMap R K) p ∣ map (algebraMap R K) q
⊢ p ∣ q

Tactic:
rcases h_dvd with ⟨r, hr⟩

Result:
case intro
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
⊢ p ∣ q

Proof state:
case intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = C ((algebraMap R K) s) * r
h : p ∣ q * (C s).primPart
⊢ Associated (q * (C s).primPart) q

Tactic:
symm

Result:
case intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = C ((algebraMap R K) s) * r
h : p ∣ q * (C s).primPart
⊢ Associated q (q * (C s).primPart)