-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
theorem eq_zero_of_mul_eq_zero_of_smul (P : R[X]) (h : ∀ r : R, r • P = 0 → r = 0) (Q : R[X])
    (hQ : P * Q = 0) : Q = 0

Proof state:
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
i j : ℕ
hij : i + j = l + m
H : i = l → ¬j = m
⊢ P.coeff i * Q.coeff j = 0

Tactic:
obtain hi|rfl|hi := lt_trichotomy i l

Result:
case inl
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
i j : ℕ
hij : i + j = l + m
H : i = l → ¬j = m
hi : i < l
⊢ P.coeff i * Q.coeff j = 0

case inr.inl
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
m : ℕ := Q.natDegree
i j : ℕ
IH : ∀ m > i, P.coeff m • Q = 0
hl : (P.coeff i • Q).natDegree = Q.natDegree
hij : i + j = i + m
H : i = i → ¬j = m
⊢ P.coeff i * Q.coeff j = 0

case inr.inr
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
i j : ℕ
hij : i + j = l + m
H : i = l → ¬j = m
hi : l < i
⊢ P.coeff i * Q.coeff j = 0

Proof state:
case inr.inl
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
m : ℕ := Q.natDegree
i j : ℕ
IH : ∀ m > i, P.coeff m • Q = 0
hl : (P.coeff i • Q).natDegree = Q.natDegree
hij : i + j = i + m
H : i = i → ¬j = m
⊢ P.coeff i * Q.coeff j = 0

Tactic:
omega

Result:
no goals

Proof state:
case inr.inr
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
i j : ℕ
hij : i + j = l + m
H : i = l → ¬j = m
hi : l < i
⊢ P.coeff i * Q.coeff j = 0

Tactic:
rw [← coeff_C_mul, ← smul_eq_C_mul, IH _ hi, coeff_zero]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
⊢ ∀ b ∈ antidiagonal (l + m), b ≠ (l, m) → P.coeff b.1 * Q.coeff b.2 = 0

Tactic:
simp only [Finset.mem_antidiagonal, ne_eq, Prod.forall, Prod.mk.injEq, not_and]

Result:
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
⊢ ∀ (a b : ℕ), a + b = l + m → (a = l → ¬b = m) → P.coeff a * Q.coeff b = 0

Proof state:
case step.inr
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
⊢ P.coeff l • Q = 0

Tactic:
suffices P.coeff l * Q.leadingCoeff = 0 by
  rwa [← leadingCoeff_eq_zero, ← coeff_natDegree, coeff_smul, hl, coeff_natDegree, smul_eq_mul]

Result:
case step.inr
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
⊢ P.coeff l * Q.leadingCoeff = 0

Proof state:
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
⊢ ∀ (a b : ℕ), a + b = l + m → (a = l → ¬b = m) → P.coeff a * Q.coeff b = 0

Tactic:
intro i j hij H

Result:
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
i j : ℕ
hij : i + j = l + m
H : i = l → ¬j = m
⊢ P.coeff i * Q.coeff j = 0

Proof state:
case base
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
⊢ ∃ n, ∀ m > n, P.coeff m • Q = 0

Tactic:
use P.natDegree

Result:
case h
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
⊢ ∀ m > P.natDegree, P.coeff m • Q = 0

Proof state:
case step.inr
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
⊢ ∑ x ∈ antidiagonal (l + m), P.coeff x.1 * Q.coeff x.2 = P.coeff l * Q.leadingCoeff

Tactic:
apply Finset.sum_eq_single (l, m) _ (by simp)

Result:
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
⊢ ∀ b ∈ antidiagonal (l + m), b ≠ (l, m) → P.coeff b.1 * Q.coeff b.2 = 0

Proof state:
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
this : ∀ (i : ℕ), P.coeff i • Q = 0
⊢ Q = 0

Tactic:
rw [← leadingCoeff_eq_zero]

Result:
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
this : ∀ (i : ℕ), P.coeff i • Q = 0
⊢ Q.leadingCoeff = 0

Proof state:
case inl
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
i j : ℕ
hij : i + j = l + m
H : i = l → ¬j = m
hi : i < l
⊢ P.coeff i * Q.coeff j = 0

Tactic:
have hj : m < j := by omega

Result:
case inl
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
i j : ℕ
hij : i + j = l + m
H : i = l → ¬j = m
hi : i < l
hj : m < j
⊢ P.coeff i * Q.coeff j = 0

Proof state:
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
this : (P * Q).coeff (l + m) = P.coeff l * Q.leadingCoeff
⊢ P.coeff l * Q.leadingCoeff = 0

Tactic:
rw [← this, hQ, coeff_zero]

Result:
no goals