no goals
M' : Type ?u.267738
X : Type ?u.267741
inst✝²³ : SMul M' X
Y : Type ?u.267748
inst✝²² : SMul M' Y
Z : Type ?u.267755
inst✝²¹ : SMul M' Z
M : Type u_1
inst✝²⁰ : Monoid M
A : Type ?u.267768
inst✝¹⁹ : AddMonoid A
inst✝¹⁸ : DistribMulAction M A
A' : Type ?u.267796
inst✝¹⁷ : AddGroup A'
inst✝¹⁶ : DistribMulAction M A'
B : Type ?u.268072
inst✝¹⁵ : AddMonoid B
inst✝¹⁴ : DistribMulAction M B
B' : Type ?u.268098
inst✝¹³ : AddGroup B'
inst✝¹² : DistribMulAction M B'
C : Type ?u.268374
inst✝¹¹ : AddMonoid C
inst✝¹⁰ : DistribMulAction M C
R : Type u_2
inst✝⁹ : Semiring R
inst✝⁸ : MulSemiringAction M R
R' : Type ?u.268427
inst✝⁷ : Ring R'
inst✝⁶ : MulSemiringAction M R'
S : Type u_3
inst✝⁵ : Semiring S
inst✝⁴ : MulSemiringAction M S
S' : Type ?u.268650
inst✝³ : Ring S'
inst✝² : MulSemiringAction M S'
T : Type ?u.268846
inst✝¹ : Semiring T
inst✝ : MulSemiringAction M T
f : R →+*[M] S
x : R
⊢ ↑(comp (MulSemiringActionHom.id M) f) x = ↑f x
rw [comp_apply, id_apply]