-- Mathlib/Algebra/Polynomial/Module/Basic.lean
theorem monomial_smul_single (i : ℕ) (r : R) (j : ℕ) (m : M) :
    monomial i r • single R j m = single R (i + j) (r • m)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
j : ℕ
m : M
⊢ r • (⇑(Finsupp.lmapDomain M R Nat.succ))^[i] ((single R j) m) = (single R (i + j)) (r • m)

Tactic:
induction i generalizing r j m with
| zero =>
  rw [Function.iterate_zero, zero_add]
  exact Finsupp.smul_single r j m
| succ n hn =>
  rw [Function.iterate_succ, Function.comp_apply, add_assoc, ← hn]
  congr 2
  rw [Nat.one_add]
  exact Finsupp.mapDomain_single

Result:
no goals

Proof state:
case succ
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M), r • (⇑(Finsupp.lmapDomain M R Nat.succ))^[n] ((single R j) m) = (single R (n + j)) (r • m)
r : R
j : ℕ
m : M
⊢ r • (⇑(Finsupp.lmapDomain M R Nat.succ))^[n] ((Finsupp.lmapDomain M R Nat.succ) ((single R j) m)) =
    r • (⇑(Finsupp.lmapDomain M R Nat.succ))^[n] ((single R (1 + j)) m)

Tactic:
congr 2

Result:
case succ.e_a.e_a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M), r • (⇑(Finsupp.lmapDomain M R Nat.succ))^[n] ((single R j) m) = (single R (n + j)) (r • m)
r : R
j : ℕ
m : M
⊢ (Finsupp.lmapDomain M R Nat.succ) ((single R j) m) = (single R (1 + j)) m

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
j : ℕ
m : M
⊢ (monomial i) r • (single R j) m = (single R (i + j)) (r • m)

Tactic:
simp only [LinearMap.mul_apply, Polynomial.aeval_monomial, LinearMap.pow_apply,
  Module.algebraMap_end_apply, smul_def]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
j : ℕ
m : M
⊢ r • (⇑(Finsupp.lmapDomain M R Nat.succ))^[i] ((single R j) m) = (single R (i + j)) (r • m)

Proof state:
case succ
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M), r • (⇑(Finsupp.lmapDomain M R Nat.succ))^[n] ((single R j) m) = (single R (n + j)) (r • m)
r : R
j : ℕ
m : M
⊢ r • (⇑(Finsupp.lmapDomain M R Nat.succ))^[n + 1] ((single R j) m) = (single R (n + 1 + j)) (r • m)

Tactic:
rw [Function.iterate_succ, Function.comp_apply, add_assoc, ← hn]

Result:
case succ
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M), r • (⇑(Finsupp.lmapDomain M R Nat.succ))^[n] ((single R j) m) = (single R (n + j)) (r • m)
r : R
j : ℕ
m : M
⊢ r • (⇑(Finsupp.lmapDomain M R Nat.succ))^[n] ((Finsupp.lmapDomain M R Nat.succ) ((single R j) m)) =
    r • (⇑(Finsupp.lmapDomain M R Nat.succ))^[n] ((single R (1 + j)) m)

Proof state:
case succ.e_a.e_a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M), r • (⇑(Finsupp.lmapDomain M R Nat.succ))^[n] ((single R j) m) = (single R (n + j)) (r • m)
r : R
j : ℕ
m : M
⊢ (Finsupp.lmapDomain M R Nat.succ) ((single R j) m) = (single R j.succ) m

Tactic:
exact Finsupp.mapDomain_single

Result:
no goals

Proof state:
case zero
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
j : ℕ
m : M
⊢ r • id ((single R j) m) = (single R j) (r • m)

Tactic:
exact Finsupp.smul_single r j m

Result:
no goals

Proof state:
case succ.e_a.e_a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M), r • (⇑(Finsupp.lmapDomain M R Nat.succ))^[n] ((single R j) m) = (single R (n + j)) (r • m)
r : R
j : ℕ
m : M
⊢ (Finsupp.lmapDomain M R Nat.succ) ((single R j) m) = (single R (1 + j)) m

Tactic:
rw [Nat.one_add]

Result:
case succ.e_a.e_a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M), r • (⇑(Finsupp.lmapDomain M R Nat.succ))^[n] ((single R j) m) = (single R (n + j)) (r • m)
r : R
j : ℕ
m : M
⊢ (Finsupp.lmapDomain M R Nat.succ) ((single R j) m) = (single R j.succ) m

Proof state:
case zero
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
j : ℕ
m : M
⊢ r • (⇑(Finsupp.lmapDomain M R Nat.succ))^[0] ((single R j) m) = (single R (0 + j)) (r • m)

Tactic:
rw [Function.iterate_zero, zero_add]

Result:
case zero
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
j : ℕ
m : M
⊢ r • id ((single R j) m) = (single R j) (r • m)