-- Mathlib/Algebra/Polynomial/Monic.lean
theorem isUnit_leadingCoeff_mul_right_eq_zero_iff (h : IsUnit p.leadingCoeff) {q : R[X]} :
    p * q = 0 ↔ q = 0

Proof state:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ p * q = 0 → q = 0

Tactic:
intro hp

Result:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : p * q = 0
⊢ q = 0

Proof state:
case mp.h
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • p * q = 0
this : h.unit⁻¹ • (p * q) = h.unit⁻¹ • p * q
⊢ (h.unit⁻¹ • p).Monic

Tactic:
exact monic_of_isUnit_leadingCoeff_inv_smul _

Result:
no goals

Proof state:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
⊢ q = 0

Tactic:
have : h.unit⁻¹ • (p * q) = h.unit⁻¹ • p * q := by
  ext
  simp only [Units.smul_def, coeff_smul, coeff_mul, smul_eq_mul, mul_sum]
  refine sum_congr rfl fun x _ => ?_
  rw [← mul_assoc]

Result:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
this : h.unit⁻¹ • (p * q) = h.unit⁻¹ • p * q
⊢ q = 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ p * q = 0 ↔ q = 0

Tactic:
constructor

Result:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ p * q = 0 → q = 0

case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ q = 0 → p * q = 0

Proof state:
case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ q = 0 → p * q = 0

Tactic:
rintro rfl

Result:
case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
⊢ p * 0 = 0

Proof state:
case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
⊢ p * 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
n✝ : ℕ
⊢ (h.unit⁻¹ • (p * q)).coeff n✝ = (h.unit⁻¹ • p * q).coeff n✝

Tactic:
simp only [Units.smul_def, coeff_smul, coeff_mul, smul_eq_mul, mul_sum]

Result:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
n✝ : ℕ
⊢ ∑ i ∈ antidiagonal n✝, ↑h.unit⁻¹ * (p.coeff i.1 * q.coeff i.2) =
    ∑ x ∈ antidiagonal n✝, ↑h.unit⁻¹ * p.coeff x.1 * q.coeff x.2

Proof state:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
n✝ : ℕ
x : ℕ × ℕ
x✝ : x ∈ antidiagonal n✝
⊢ ↑h.unit⁻¹ * (p.coeff x.1 * q.coeff x.2) = ↑h.unit⁻¹ * p.coeff x.1 * q.coeff x.2

Tactic:
rw [← mul_assoc]

Result:
no goals

Proof state:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
this : h.unit⁻¹ • (p * q) = h.unit⁻¹ • p * q
⊢ q = 0

Tactic:
rwa [this, Monic.mul_right_eq_zero_iff] at hp

Result:
case mp.h
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • p * q = 0
this : h.unit⁻¹ • (p * q) = h.unit⁻¹ • p * q
⊢ (h.unit⁻¹ • p).Monic

Proof state:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : p * q = 0
⊢ q = 0

Tactic:
rw [← smul_eq_zero_iff_eq h.unit⁻¹] at hp

Result:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
⊢ q = 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
⊢ h.unit⁻¹ • (p * q) = h.unit⁻¹ • p * q

Tactic:
ext

Result:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
n✝ : ℕ
⊢ (h.unit⁻¹ • (p * q)).coeff n✝ = (h.unit⁻¹ • p * q).coeff n✝

Proof state:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
n✝ : ℕ
⊢ ∑ i ∈ antidiagonal n✝, ↑h.unit⁻¹ * (p.coeff i.1 * q.coeff i.2) =
    ∑ x ∈ antidiagonal n✝, ↑h.unit⁻¹ * p.coeff x.1 * q.coeff x.2

Tactic:
refine sum_congr rfl fun x _ => ?_

Result:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : h.unit⁻¹ • (p * q) = 0
n✝ : ℕ
x : ℕ × ℕ
x✝ : x ∈ antidiagonal n✝
⊢ ↑h.unit⁻¹ * (p.coeff x.1 * q.coeff x.2) = ↑h.unit⁻¹ * p.coeff x.1 * q.coeff x.2