-- 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
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)

Tactic:
rcases isUnit_primPart_C s with ⟨u, hu⟩

Result:
case intro.intro.mk.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
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
u : R[X]ˣ
hu : ↑u = (C s).primPart
⊢ Associated q (q * (C s).primPart)

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
⊢ ¬s = 0

Tactic:
contrapose! s0

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
hs : map (algebraMap R K) (integerNormalization R⁰ r) = C ((algebraMap R K) s) * r
h : p ∣ q * C s
s0 : s = 0
⊢ s ∉ R⁰

Proof state:
case h
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
⊢ q * C s = p * integerNormalization R⁰ r

Tactic:
apply map_injective (algebraMap R K) (IsFractionRing.injective _ _)

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) (q * C s) = map (algebraMap R K) (p * integerNormalization R⁰ 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
h : p ∣ q * C s
⊢ C s ≠ 0

Tactic:
rw [Ne, C_eq_zero]

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
⊢ ¬s = 0

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) = ↑⟨s, s0⟩ • r
⊢ p ∣ q

Tactic:
rw [Subtype.coe_mk, Algebra.smul_def, algebraMap_apply] at hs

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
⊢ p ∣ q

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) p * (map (algebraMap R K) (C s) * r) = map (algebraMap R K) p * (C ((algebraMap R K) s) * r)

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro.mk.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
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
u : R[X]ˣ
hu : ↑u = (C s).primPart
⊢ Associated q (q * (C s).primPart)

Tactic:
use u

Result:
case h
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
u : R[X]ˣ
hu : ↑u = (C s).primPart
⊢ q * ↑u = q * (C s).primPart

Proof state:
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

Tactic:
obtain ⟨⟨s, s0⟩, hs⟩ := integerNormalization_map_to_map R⁰ r

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) = ↑⟨s, s0⟩ • r
⊢ p ∣ q