-- Mathlib/Algebra/Polynomial/Module/Basic.lean
theorem smul_single_apply (i : ℕ) (f : R[X]) (m : M) (n : ℕ) :
    (f • single R i m) n = ite (i ≤ n) (f.coeff (n - i) • m) 0

Proof state:
case neg.hnc
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
m : M
n n✝ : ℕ
a✝ : R
h : ¬i ≤ n
⊢ ¬n✝ + i = n

Tactic:
omega

Result:
no goals

Proof state:
case pos
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
m : M
n : ℕ
p q : R[X]
hp : (p • (single R i) m) n = if i ≤ n then p.coeff (n - i) • m else 0
hq : (q • (single R i) m) n = if i ≤ n then q.coeff (n - i) • m else 0
h✝ : i ≤ n
⊢ p.coeff (n - i) • m + q.coeff (n - i) • m = p.coeff (n - i) • m + q.coeff (n - i) • m

case neg
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
m : M
n : ℕ
p q : R[X]
hp : (p • (single R i) m) n = if i ≤ n then p.coeff (n - i) • m else 0
hq : (q • (single R i) m) n = if i ≤ n then q.coeff (n - i) • m else 0
h✝ : ¬i ≤ n
⊢ 0 + 0 = 0

Tactic:
exacts [rfl, zero_add 0]

Result:
no goals

Proof state:
case h_monomial
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
m : M
n n✝ : ℕ
a✝ : R
⊢ (if n✝ + i = n then a✝ • m else 0) = if i ≤ n then if n✝ = n - i then a✝ • m else 0 else 0

Tactic:
by_cases h : i ≤ n

Result:
case pos
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
m : M
n n✝ : ℕ
a✝ : R
h : i ≤ n
⊢ (if n✝ + i = n then a✝ • m else 0) = if i ≤ n then if n✝ = n - i then a✝ • m else 0 else 0

case neg
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
m : M
n n✝ : ℕ
a✝ : R
h : ¬i ≤ n
⊢ (if n✝ + i = n then a✝ • m else 0) = if i ≤ n then if n✝ = n - i then a✝ • m else 0 else 0

Proof state:
case pos
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
m : M
n n✝ : ℕ
a✝ : R
h : i ≤ n
⊢ (if n✝ + i = n then a✝ • m else 0) = if i ≤ n then if n✝ = n - i then a✝ • m else 0 else 0

Tactic:
simp_rw [eq_tsub_iff_add_eq_of_le h, if_pos h]

Result:
no goals

Proof state:
case neg
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
m : M
n n✝ : ℕ
a✝ : R
h : ¬i ≤ n
⊢ (if n✝ + i = n then a✝ • m else 0) = if i ≤ n then if n✝ = n - i then a✝ • m else 0 else 0

Tactic:
rw [if_neg h, if_neg]

Result:
case neg.hnc
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
m : M
n n✝ : ℕ
a✝ : R
h : ¬i ≤ n
⊢ ¬n✝ + i = n

Proof state:
case h_add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
m : M
n : ℕ
p q : R[X]
hp : (p • (single R i) m) n = if i ≤ n then p.coeff (n - i) • m else 0
hq : (q • (single R i) m) n = if i ≤ n then q.coeff (n - i) • m else 0
⊢ ((if i ≤ n then p.coeff (n - i) • m else 0) + if i ≤ n then q.coeff (n - i) • m else 0) =
    if i ≤ n then p.coeff (n - i) • m + q.coeff (n - i) • m else 0

Tactic:
split_ifs

Result:
case pos
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
m : M
n : ℕ
p q : R[X]
hp : (p • (single R i) m) n = if i ≤ n then p.coeff (n - i) • m else 0
hq : (q • (single R i) m) n = if i ≤ n then q.coeff (n - i) • m else 0
h✝ : i ≤ n
⊢ p.coeff (n - i) • m + q.coeff (n - i) • m = p.coeff (n - i) • m + q.coeff (n - i) • m

case neg
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
m : M
n : ℕ
p q : R[X]
hp : (p • (single R i) m) n = if i ≤ n then p.coeff (n - i) • m else 0
hq : (q • (single R i) m) n = if i ≤ n then q.coeff (n - i) • m else 0
h✝ : ¬i ≤ n
⊢ 0 + 0 = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
f : R[X]
m : M
n : ℕ
⊢ (f • (single R i) m) n = if i ≤ n then f.coeff (n - i) • m else 0

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

Result:
case h_add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
m : M
n : ℕ
p q : R[X]
hp : (p • (single R i) m) n = if i ≤ n then p.coeff (n - i) • m else 0
hq : (q • (single R i) m) n = if i ≤ n then q.coeff (n - i) • m else 0
⊢ ((p + q) • (single R i) m) n = if i ≤ n then (p + q).coeff (n - i) • m else 0

case h_monomial
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
m : M
n n✝ : ℕ
a✝ : R
⊢ ((monomial n✝) a✝ • (single R i) m) n = if i ≤ n then ((monomial n✝) a✝).coeff (n - i) • m else 0

Proof state:
case h_monomial
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
m : M
n n✝ : ℕ
a✝ : R
⊢ ((monomial n✝) a✝ • (single R i) m) n = if i ≤ n then ((monomial n✝) a✝).coeff (n - i) • m else 0

Tactic:
rw [monomial_smul_single, single_apply, coeff_monomial, ite_smul, zero_smul]

Result:
case h_monomial
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
m : M
n n✝ : ℕ
a✝ : R
⊢ (if n✝ + i = n then a✝ • m else 0) = if i ≤ n then if n✝ = n - i then a✝ • m else 0 else 0

Proof state:
case h_add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
m : M
n : ℕ
p q : R[X]
hp : (p • (single R i) m) n = if i ≤ n then p.coeff (n - i) • m else 0
hq : (q • (single R i) m) n = if i ≤ n then q.coeff (n - i) • m else 0
⊢ ((p + q) • (single R i) m) n = if i ≤ n then (p + q).coeff (n - i) • m else 0

Tactic:
rw [add_smul, Finsupp.add_apply, hp, hq, coeff_add, add_smul]

Result:
case h_add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
m : M
n : ℕ
p q : R[X]
hp : (p • (single R i) m) n = if i ≤ n then p.coeff (n - i) • m else 0
hq : (q • (single R i) m) n = if i ≤ n then q.coeff (n - i) • m else 0
⊢ ((if i ≤ n then p.coeff (n - i) • m else 0) + if i ≤ n then q.coeff (n - i) • m else 0) =
    if i ≤ n then p.coeff (n - i) • m + q.coeff (n - i) • m else 0