-- Mathlib/Algebra/Polynomial/Div.lean
lemma eq_of_dvd_of_natDegree_le_of_leadingCoeff {p q : R[X]} (hpq : p ∣ q)
    (h₁ : q.natDegree ≤ p.natDegree) (h₂ : p.leadingCoeff = q.leadingCoeff) :
    p = q

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hpq : p ∣ q
h₁ : q.natDegree ≤ p.natDegree
h₂ : p.leadingCoeff = q.leadingCoeff
⊢ p = q

Tactic:
by_cases hq : q = 0

Result:
case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hpq : p ∣ q
h₁ : q.natDegree ≤ p.natDegree
h₂ : p.leadingCoeff = q.leadingCoeff
hq : q = 0
⊢ p = q

case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hpq : p ∣ q
h₁ : q.natDegree ≤ p.natDegree
h₂ : p.leadingCoeff = q.leadingCoeff
hq : ¬q = 0
⊢ p = q

Proof state:
case neg.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p u : R[X]
h₂ : p.leadingCoeff = (p * u).leadingCoeff
hq : ¬p * u = 0
h₁ : p.natDegree = (p * u).natDegree
⊢ p = p * u

Tactic:
replace hq := mul_ne_zero_iff.mp hq

Result:
case neg.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p u : R[X]
h₂ : p.leadingCoeff = (p * u).leadingCoeff
h₁ : p.natDegree = (p * u).natDegree
hq : p ≠ 0 ∧ u ≠ 0
⊢ p = p * u

Proof state:
case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hpq : p ∣ q
h₁ : q.natDegree ≤ p.natDegree
h₂ : p.leadingCoeff = q.leadingCoeff
hq : q = 0
⊢ p = q

Tactic:
rwa [hq, leadingCoeff_zero, leadingCoeff_eq_zero, ← hq] at h₂

Result:
no goals

Proof state:
case neg.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p u : R[X]
h₂ : p.leadingCoeff = (p * u).leadingCoeff
h₁ : p.natDegree = (p * u).natDegree
hq : p ≠ 0 ∧ u ≠ 0
⊢ p = p * u

Tactic:
rw [natDegree_mul hq.1 hq.2, self_eq_add_right] at h₁

Result:
case neg.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p u : R[X]
h₂ : p.leadingCoeff = (p * u).leadingCoeff
h₁ : u.natDegree = 0
hq : p ≠ 0 ∧ u ≠ 0
⊢ p = p * u

Proof state:
case neg.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p u : R[X]
h₂ : p.leadingCoeff = (p * u).leadingCoeff
h₁ : u.natDegree = 0
hq : p ≠ 0 ∧ u ≠ 0
⊢ p = p * u

Tactic:
rw [eq_C_of_natDegree_eq_zero h₁, leadingCoeff_mul, leadingCoeff_C,
  eq_comm, mul_eq_left₀ (leadingCoeff_ne_zero.mpr hq.1)] at h₂

Result:
case neg.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p u : R[X]
h₂ : u.coeff 0 = 1
h₁ : u.natDegree = 0
hq : p ≠ 0 ∧ u ≠ 0
⊢ p = p * u

Proof state:
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hpq : p ∣ q
h₁ : q.natDegree ≤ p.natDegree
h₂ : p.leadingCoeff = q.leadingCoeff
hq : ¬q = 0
⊢ p = q

Tactic:
replace h₁ := (natDegree_le_of_dvd hpq hq).antisymm h₁

Result:
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hpq : p ∣ q
h₂ : p.leadingCoeff = q.leadingCoeff
hq : ¬q = 0
h₁ : p.natDegree = q.natDegree
⊢ p = q

Proof state:
case neg.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p u : R[X]
h₂ : u.coeff 0 = 1
h₁ : u.natDegree = 0
hq : p ≠ 0 ∧ u ≠ 0
⊢ p = p * u

Tactic:
rw [eq_C_of_natDegree_eq_zero h₁, h₂, map_one, mul_one]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hpq : p ∣ q
h₂ : p.leadingCoeff = q.leadingCoeff
hq : ¬q = 0
h₁ : p.natDegree = q.natDegree
⊢ p = q

Tactic:
obtain ⟨u, rfl⟩ := hpq

Result:
case neg.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p u : R[X]
h₂ : p.leadingCoeff = (p * u).leadingCoeff
hq : ¬p * u = 0
h₁ : p.natDegree = (p * u).natDegree
⊢ p = p * u