[GOAL]
M : Type u_1
inst✝² : Monoid M
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
m : M
⊢ HSMul.hSMul m = map (MulSemiringAction.toRingHom M R m)
[PROOFSTEP]
suffices DistribMulAction.toAddMonoidHom R[X] m = (mapRingHom (MulSemiringAction.toRingHom M R m)).toAddMonoidHom
  by
  ext1 r
  exact FunLike.congr_fun this r
[GOAL]
M : Type u_1
inst✝² : Monoid M
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
m : M
this : DistribMulAction.toAddMonoidHom R[X] m = RingHom.toAddMonoidHom (mapRingHom (MulSemiringAction.toRingHom M R m))
⊢ HSMul.hSMul m = map (MulSemiringAction.toRingHom M R m)
[PROOFSTEP]
ext1 r
[GOAL]
case h
M : Type u_1
inst✝² : Monoid M
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
m : M
this : DistribMulAction.toAddMonoidHom R[X] m = RingHom.toAddMonoidHom (mapRingHom (MulSemiringAction.toRingHom M R m))
r : R[X]
⊢ m • r = map (MulSemiringAction.toRingHom M R m) r
[PROOFSTEP]
exact FunLike.congr_fun this r
[GOAL]
M : Type u_1
inst✝² : Monoid M
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
m : M
⊢ DistribMulAction.toAddMonoidHom R[X] m = RingHom.toAddMonoidHom (mapRingHom (MulSemiringAction.toRingHom M R m))
[PROOFSTEP]
ext n r : 2
[GOAL]
case h.h
M : Type u_1
inst✝² : Monoid M
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
m : M
n : ℕ
r : R
⊢ ↑(AddMonoidHom.comp (DistribMulAction.toAddMonoidHom R[X] m) (LinearMap.toAddMonoidHom (monomial n))) r =
    ↑(AddMonoidHom.comp (RingHom.toAddMonoidHom (mapRingHom (MulSemiringAction.toRingHom M R m)))
          (LinearMap.toAddMonoidHom (monomial n)))
      r
[PROOFSTEP]
change m • monomial n r = map (MulSemiringAction.toRingHom M R m) (monomial n r)
[GOAL]
case h.h
M : Type u_1
inst✝² : Monoid M
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
m : M
n : ℕ
r : R
⊢ m • ↑(monomial n) r = map (MulSemiringAction.toRingHom M R m) (↑(monomial n) r)
[PROOFSTEP]
rw [Polynomial.map_monomial, Polynomial.smul_monomial, MulSemiringAction.toRingHom_apply]
[GOAL]
M : Type u_1
inst✝⁴ : Monoid M
R : Type u_2
inst✝³ : Semiring R
inst✝² : MulSemiringAction M R
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : MulSemiringAction M S
m : M
f : S[X]
x r : S
⊢ eval (m • x) (m • ↑C r) = m • eval x (↑C r)
[PROOFSTEP]
rw [smul_C, eval_C, eval_C]
[GOAL]
M : Type u_1
inst✝⁴ : Monoid M
R : Type u_2
inst✝³ : Semiring R
inst✝² : MulSemiringAction M R
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : MulSemiringAction M S
m : M
f✝ : S[X]
x : S
f g : S[X]
ihf : eval (m • x) (m • f) = m • eval x f
ihg : eval (m • x) (m • g) = m • eval x g
⊢ eval (m • x) (m • (f + g)) = m • eval x (f + g)
[PROOFSTEP]
rw [smul_add, eval_add, ihf, ihg, eval_add, smul_add]
[GOAL]
M : Type u_1
inst✝⁴ : Monoid M
R : Type u_2
inst✝³ : Semiring R
inst✝² : MulSemiringAction M R
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : MulSemiringAction M S
m : M
f : S[X]
x : S
n : ℕ
r : S
x✝ : eval (m • x) (m • (↑C r * X ^ n)) = m • eval x (↑C r * X ^ n)
⊢ eval (m • x) (m • (↑C r * X ^ (n + 1))) = m • eval x (↑C r * X ^ (n + 1))
[PROOFSTEP]
rw [smul_mul', smul_pow', smul_C, smul_X, eval_mul, eval_C, eval_pow, eval_X, eval_mul, eval_C, eval_pow, eval_X,
  smul_mul', smul_pow']
[GOAL]
M : Type u_1
inst✝⁶ : Monoid M
R : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : MulSemiringAction M R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : MulSemiringAction M S
G : Type u_4
inst✝¹ : Group G
inst✝ : MulSemiringAction G S
g : G
f : S[X]
x : S
⊢ eval (g • x) f = g • eval x (g⁻¹ • f)
[PROOFSTEP]
rw [← smul_eval_smul, smul_inv_smul]
[GOAL]
M : Type u_1
inst✝⁶ : Monoid M
R : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : MulSemiringAction M R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : MulSemiringAction M S
G : Type u_4
inst✝¹ : Group G
inst✝ : MulSemiringAction G S
g : G
f : S[X]
x : S
⊢ eval x (g • f) = g • eval (g⁻¹ • x) f
[PROOFSTEP]
rw [← smul_eval_smul, smul_inv_smul]
[GOAL]
M : Type u_1
inst✝⁴ : Monoid M
G : Type u_2
inst✝³ : Group G
inst✝² : Fintype G
R : Type u_3
inst✝¹ : CommRing R
inst✝ : MulSemiringAction G R
x : R
⊢ ↑↑↑(aeval x) (X - ↑C (ofQuotientStabilizer G x ↑1)) = 0
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
inst✝⁴ : Monoid M
G : Type u_2
inst✝³ : Group G
inst✝² : Fintype G
R : Type u_3
inst✝¹ : CommRing R
inst✝ : MulSemiringAction G R
x : R
g : G
g' : G ⧸ stabilizer G x
⊢ g • (X - ↑C (ofQuotientStabilizer G x g')) = X - ↑C (ofQuotientStabilizer G x ((fun x_1 x_2 => x_1 • x_2) g g'))
[PROOFSTEP]
rw [ofQuotientStabilizer_smul, smul_sub, Polynomial.smul_X, Polynomial.smul_C]
[GOAL]
M : Type u_1
inst✝⁴ : Monoid M
G : Type u_2
inst✝³ : Group G
inst✝² : Fintype G
R : Type u_3
inst✝¹ : CommRing R
inst✝ : MulSemiringAction G R
x : R
g : G
n : ℕ
⊢ g • Polynomial.coeff (prodXSubSmul G R x) n = Polynomial.coeff (prodXSubSmul G R x) n
[PROOFSTEP]
rw [← Polynomial.coeff_smul, prodXSubSmul.smul]
[GOAL]
M : Type u_1
inst✝⁴ : Monoid M
P : Type u_2
inst✝³ : CommSemiring P
inst✝² : MulSemiringAction M P
Q : Type u_3
inst✝¹ : CommSemiring Q
inst✝ : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p : P[X]
b : P
⊢ map (↑g) (m • ↑C b) = m • map (↑g) (↑C b)
[PROOFSTEP]
rw [smul_C, map_C, coe_fn_coe, g.map_smul, map_C, coe_fn_coe, smul_C]
[GOAL]
M : Type u_1
inst✝⁴ : Monoid M
P : Type u_2
inst✝³ : CommSemiring P
inst✝² : MulSemiringAction M P
Q : Type u_3
inst✝¹ : CommSemiring Q
inst✝ : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p✝ p q : P[X]
ihp : map (↑g) (m • p) = m • map (↑g) p
ihq : map (↑g) (m • q) = m • map (↑g) q
⊢ map (↑g) (m • (p + q)) = m • map (↑g) (p + q)
[PROOFSTEP]
rw [smul_add, Polynomial.map_add, ihp, ihq, Polynomial.map_add, smul_add]
[GOAL]
M : Type u_1
inst✝⁴ : Monoid M
P : Type u_2
inst✝³ : CommSemiring P
inst✝² : MulSemiringAction M P
Q : Type u_3
inst✝¹ : CommSemiring Q
inst✝ : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p : P[X]
n : ℕ
b : P
x✝ : map (↑g) (m • (↑C b * X ^ n)) = m • map (↑g) (↑C b * X ^ n)
⊢ map (↑g) (m • (↑C b * X ^ (n + 1))) = m • map (↑g) (↑C b * X ^ (n + 1))
[PROOFSTEP]
rw [smul_mul', smul_C, smul_pow', smul_X, Polynomial.map_mul, map_C, Polynomial.map_pow, map_X, coe_fn_coe, g.map_smul,
  Polynomial.map_mul, map_C, Polynomial.map_pow, map_X, smul_mul', smul_C, smul_pow', smul_X, coe_fn_coe]
  -- porting note: added `.toRingHom`
