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))
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)
suffices DistribMulAction.toAddMonoidHom R[X] m =
    (mapRingHom (MulSemiringAction.toRingHom M R m)).toAddMonoidHom by
  ext1 r
  exact FunLike.congr_fun this r
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
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))
ext (n r) : 2
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)
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
change m • monomial n r = map (MulSemiringAction.toRingHom M R m) (monomial n r)
no goals
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)
rw [Polynomial.map_monomial, Polynomial.smul_monomial, MulSemiringAction.toRingHom_apply]
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
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)
ext1 r
no goals
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
exact FunLike.congr_fun this r