-- Mathlib/Algebra/Polynomial/Module/Basic.lean
theorem smul_apply (f : R[X]) (g : PolynomialModule R M) (n : ℕ) :
    (f • g) n = ∑ x ∈ Finset.antidiagonal n, f.coeff x.1 • g x.2

Proof state:
case h_monomial.e_f.h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
x : ℕ
⊢ (if f_n = x then f_a • g (n - x) else 0) = (if f_n = x then f_a else 0) • g (n - x)

Tactic:
split_ifs

Result:
case pos
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
x : ℕ
h✝ : f_n = x
⊢ f_a • g (n - x) = f_a • g (n - x)

case neg
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
x : ℕ
h✝ : ¬f_n = x
⊢ 0 = 0 • g (n - x)

Proof state:
case h_monomial
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
⊢ ((monomial f_n) f_a • g) n = ∑ x ∈ Finset.antidiagonal n, ((monomial f_n) f_a).coeff x.1 • g x.2

Tactic:
rw [Finset.Nat.sum_antidiagonal_eq_sum_range_succ fun i j => (monomial f_n f_a).coeff i • g j,
  monomial_smul_apply]

Result:
case h_monomial
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
⊢ (if f_n ≤ n then f_a • g (n - f_n) else 0) = ∑ k ∈ Finset.range n.succ, ((monomial f_n) f_a).coeff k • g (n - k)

Proof state:
case h_add.e_f.h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : PolynomialModule R M
n : ℕ
p q : R[X]
hp : (p • g) n = ∑ x ∈ Finset.antidiagonal n, p.coeff x.1 • g x.2
hq : (q • g) n = ∑ x ∈ Finset.antidiagonal n, q.coeff x.1 • g x.2
x✝ : ℕ × ℕ
⊢ p.coeff x✝.1 • g x✝.2 + q.coeff x✝.1 • g x✝.2 = (p + q).coeff x✝.1 • g x✝.2

Tactic:
rw [coeff_add, add_smul]

Result:
no goals

Proof state:
case h_add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : PolynomialModule R M
n : ℕ
p q : R[X]
hp : (p • g) n = ∑ x ∈ Finset.antidiagonal n, p.coeff x.1 • g x.2
hq : (q • g) n = ∑ x ∈ Finset.antidiagonal n, q.coeff x.1 • g x.2
⊢ ∑ x ∈ Finset.antidiagonal n, (p.coeff x.1 • g x.2 + q.coeff x.1 • g x.2) =
    ∑ x ∈ Finset.antidiagonal n, (p + q).coeff x.1 • g x.2

Tactic:
congr

Result:
case h_add.e_f
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : PolynomialModule R M
n : ℕ
p q : R[X]
hp : (p • g) n = ∑ x ∈ Finset.antidiagonal n, p.coeff x.1 • g x.2
hq : (q • g) n = ∑ x ∈ Finset.antidiagonal n, q.coeff x.1 • g x.2
⊢ (fun x => p.coeff x.1 • g x.2 + q.coeff x.1 • g x.2) = fun x => (p + q).coeff x.1 • g x.2

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R[X]
g : PolynomialModule R M
n : ℕ
⊢ (f • g) n = ∑ x ∈ Finset.antidiagonal n, f.coeff x.1 • g x.2

Tactic:
induction' f using Polynomial.induction_on' with p q hp hq f_n f_a

Result:
case h_add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : PolynomialModule R M
n : ℕ
p q : R[X]
hp : (p • g) n = ∑ x ∈ Finset.antidiagonal n, p.coeff x.1 • g x.2
hq : (q • g) n = ∑ x ∈ Finset.antidiagonal n, q.coeff x.1 • g x.2
⊢ ((p + q) • g) n = ∑ x ∈ Finset.antidiagonal n, (p + q).coeff x.1 • g x.2

case h_monomial
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
⊢ ((monomial f_n) f_a • g) n = ∑ x ∈ Finset.antidiagonal n, ((monomial f_n) f_a).coeff x.1 • g x.2

Proof state:
case pos
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
x : ℕ
h✝ : f_n = x
⊢ f_a • g (n - x) = f_a • g (n - x)

case neg
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
x : ℕ
h✝ : ¬f_n = x
⊢ 0 = 0 • g (n - x)

Tactic:
exacts [rfl, (zero_smul R _).symm]

Result:
no goals

Proof state:
case h_monomial.e_f
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
⊢ (fun x => if f_n = x then f_a • g (n - x) else 0) = fun x => (if f_n = x then f_a else 0) • g (n - x)

Tactic:
ext x

Result:
case h_monomial.e_f.h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
x : ℕ
⊢ (if f_n = x then f_a • g (n - x) else 0) = (if f_n = x then f_a else 0) • g (n - x)

Proof state:
case h_add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : PolynomialModule R M
n : ℕ
p q : R[X]
hp : (p • g) n = ∑ x ∈ Finset.antidiagonal n, p.coeff x.1 • g x.2
hq : (q • g) n = ∑ x ∈ Finset.antidiagonal n, q.coeff x.1 • g x.2
⊢ ((p + q) • g) n = ∑ x ∈ Finset.antidiagonal n, (p + q).coeff x.1 • g x.2

Tactic:
rw [add_smul, Finsupp.add_apply, hp, hq, ← Finset.sum_add_distrib]

Result:
case h_add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : PolynomialModule R M
n : ℕ
p q : R[X]
hp : (p • g) n = ∑ x ∈ Finset.antidiagonal n, p.coeff x.1 • g x.2
hq : (q • g) n = ∑ x ∈ Finset.antidiagonal n, q.coeff x.1 • g x.2
⊢ ∑ x ∈ Finset.antidiagonal n, (p.coeff x.1 • g x.2 + q.coeff x.1 • g x.2) =
    ∑ x ∈ Finset.antidiagonal n, (p + q).coeff x.1 • g x.2

Proof state:
case h_monomial
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
⊢ (if f_n ≤ n then f_a • g (n - f_n) else 0) = ∑ k ∈ Finset.range n.succ, ((monomial f_n) f_a).coeff k • g (n - k)

Tactic:
simp_rw [Polynomial.coeff_monomial, ← Finset.mem_range_succ_iff]

Result:
case h_monomial
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
⊢ (if f_n ∈ Finset.range n.succ then f_a • g (n - f_n) else 0) =
    ∑ x ∈ Finset.range n.succ, (if f_n = x then f_a else 0) • g (n - x)

Proof state:
case h_monomial
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
⊢ (if f_n ∈ Finset.range n.succ then f_a • g (n - f_n) else 0) =
    ∑ x ∈ Finset.range n.succ, (if f_n = x then f_a else 0) • g (n - x)

Tactic:
rw [← Finset.sum_ite_eq (Finset.range (Nat.succ n)) f_n (fun x => f_a • g (n - x))]

Result:
case h_monomial
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
⊢ (∑ x ∈ Finset.range n.succ, if f_n = x then f_a • g (n - x) else 0) =
    ∑ x ∈ Finset.range n.succ, (if f_n = x then f_a else 0) • g (n - x)

Proof state:
case h_add.e_f
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : PolynomialModule R M
n : ℕ
p q : R[X]
hp : (p • g) n = ∑ x ∈ Finset.antidiagonal n, p.coeff x.1 • g x.2
hq : (q • g) n = ∑ x ∈ Finset.antidiagonal n, q.coeff x.1 • g x.2
⊢ (fun x => p.coeff x.1 • g x.2 + q.coeff x.1 • g x.2) = fun x => (p + q).coeff x.1 • g x.2

Tactic:
ext

Result:
case h_add.e_f.h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : PolynomialModule R M
n : ℕ
p q : R[X]
hp : (p • g) n = ∑ x ∈ Finset.antidiagonal n, p.coeff x.1 • g x.2
hq : (q • g) n = ∑ x ∈ Finset.antidiagonal n, q.coeff x.1 • g x.2
x✝ : ℕ × ℕ
⊢ p.coeff x✝.1 • g x✝.2 + q.coeff x✝.1 • g x✝.2 = (p + q).coeff x✝.1 • g x✝.2