R : Type u_2
M : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.189821
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S 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)
R : Type u_2
M : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.189821
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
j : ℕ
m : M
⊢ ↑(monomial i) r • ↑(single R j) m = ↑(single R (i + j)) (r • m)
simp only [LinearMap.mul_apply, Polynomial.aeval_monomial, LinearMap.pow_apply,
  Module.algebraMap_end_apply, modulePolynomialOfEndo_smul_def]
no goals
R : Type u_2
M : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.189821
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S 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)
induction i generalizing r j m with
| zero =>
  rw [Nat.zero_eq, Function.iterate_zero, zero_add]
  exact Finsupp.smul_single r j m
| succ n hn =>
  rw [Function.iterate_succ, Function.comp_apply, Nat.succ_eq_add_one, add_assoc, ← hn]
  congr 2
  rw [← Nat.succ_eq_one_add]
  exact Finsupp.mapDomain_single
case zero
R : Type u_2
M : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.189821
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
r : R
j : ℕ
m : M
⊢ r • id (↑(single R j) m) = ↑(single R j) (r • m)
case zero
R : Type u_2
M : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.189821
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
r : R
j : ℕ
m : M
⊢ r • (↑(Finsupp.lmapDomain M R Nat.succ)^[Nat.zero]) (↑(single R j) m) = ↑(single R (Nat.zero + j)) (r • m)
rw [Nat.zero_eq, Function.iterate_zero, zero_add]
no goals
case zero
R : Type u_2
M : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.189821
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
r : R
j : ℕ
m : M
⊢ r • id (↑(single R j) m) = ↑(single R j) (r • m)
exact Finsupp.smul_single r j m
case succ
R : Type u_2
M : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.189821
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S 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)
case succ
R : Type u_2
M : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.189821
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S 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)^[Nat.succ n]) (↑(single R j) m) = ↑(single R (Nat.succ n + j)) (r • m)
rw [Function.iterate_succ, Function.comp_apply, Nat.succ_eq_add_one, add_assoc, ← hn]
case succ.e_a.e_a
R : Type u_2
M : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.189821
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S 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
case succ
R : Type u_2
M : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.189821
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S 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)
congr 2
case succ.e_a.e_a
R : Type u_2
M : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.189821
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S 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 (Nat.succ j)) m
case succ.e_a.e_a
R : Type u_2
M : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.189821
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S 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
rw [← Nat.succ_eq_one_add]
no goals
case succ.e_a.e_a
R : Type u_2
M : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.189821
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S 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 (Nat.succ j)) m
exact Finsupp.mapDomain_single