-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem coeff_mul_monomial' (m) (s : σ →₀ ℕ) (r : R) (p : MvPolynomial σ R) :
    coeff m (p * monomial s r) = if s ≤ m then coeff (m - s) p * r else 0

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : m ∈ (p * (monomial s) r).support
⊢ ∃ j ∈ p.support, j + s = m

Tactic:
simpa [Finset.mem_add]
  using Finset.add_subset_add_left support_monomial_subset <| support_mul _ _ h

Result:
no goals

Proof state:
case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : m ∈ (p * (monomial s) r).support
⊢ s ≤ m

Tactic:
obtain ⟨j, -, rfl⟩ : ∃ j ∈ support p, j + s = m := by
  simpa [Finset.mem_add]
    using Finset.add_subset_add_left support_monomial_subset <| support_mul _ _ h

Result:
case neg.intro.intro
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
j : σ →₀ ℕ
h : j + s ∈ (p * (monomial s) r).support
⊢ s ≤ j + s

Proof state:
case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : coeff m (p * (monomial s) r) ≠ 0
⊢ s ≤ m

Tactic:
rw [← mem_support_iff] at h

Result:
case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : m ∈ (p * (monomial s) r).support
⊢ s ≤ m

Proof state:
case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : ¬s ≤ m
⊢ coeff m (p * (monomial s) r) = 0

Tactic:
contrapose! h

Result:
case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : coeff m (p * (monomial s) r) ≠ 0
⊢ s ≤ m

Proof state:
case pos.e_m.h
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : s ≤ m
t : σ
⊢ m t = (m - s + s) t

Tactic:
rw [tsub_add_cancel_of_le h]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
⊢ coeff m (p * (monomial s) r) = if s ≤ m then coeff (m - s) p * r else 0

Tactic:
split_ifs with h

Result:
case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : s ≤ m
⊢ coeff m (p * (monomial s) r) = coeff (m - s) p * r

case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : ¬s ≤ m
⊢ coeff m (p * (monomial s) r) = 0

Proof state:
case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : s ≤ m
⊢ coeff m (p * (monomial s) r) = coeff (m - s) p * r

Tactic:
conv_rhs => rw [← coeff_mul_monomial _ s]

Result:
case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : s ≤ m
⊢ coeff m (p * (monomial s) r) = coeff (m - s + s) (p * (monomial s) r)

Proof state:
case neg.intro.intro
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
j : σ →₀ ℕ
h : j + s ∈ (p * (monomial s) r).support
⊢ s ≤ j + s

Tactic:
exact le_add_left le_rfl

Result:
no goals

Proof state:
case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : s ≤ m
⊢ coeff m (p * (monomial s) r) = coeff (m - s + s) (p * (monomial s) r)

Tactic:
congr with t

Result:
case pos.e_m.h
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : s ≤ m
t : σ
⊢ m t = (m - s + s) t