case h1
α : Type ?u.146146
R : Type u_2
k : Type ?u.146152
S : Type ?u.146155
M : Type u_1
M₂ : Type ?u.146161
M₃ : Type ?u.146164
ι : Type ?u.146167
inst✝⁴ : Semiring S
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module S M
inst✝ : Module R M
n : ℤ
b : M
⊢ ↑(↑(AddMonoidHom.flip (smulAddHom ℤ M)) b) 1 =
    ↑(AddMonoidHom.comp (↑(AddMonoidHom.flip (smulAddHom R M)) b) (Int.castAddHom R)) 1
α : Type ?u.146146
R : Type u_2
k : Type ?u.146152
S : Type ?u.146155
M : Type u_1
M₂ : Type ?u.146161
M₃ : Type ?u.146164
ι : Type ?u.146167
inst✝⁴ : Semiring S
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module S M
inst✝ : Module R M
n : ℤ
b : M
⊢ ↑(AddMonoidHom.flip (smulAddHom ℤ M)) b =
    AddMonoidHom.comp (↑(AddMonoidHom.flip (smulAddHom R M)) b) (Int.castAddHom R)
apply AddMonoidHom.ext_int
no goals
case h1
α : Type ?u.146146
R : Type u_2
k : Type ?u.146152
S : Type ?u.146155
M : Type u_1
M₂ : Type ?u.146161
M₃ : Type ?u.146164
ι : Type ?u.146167
inst✝⁴ : Semiring S
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module S M
inst✝ : Module R M
n : ℤ
b : M
⊢ ↑(↑(AddMonoidHom.flip (smulAddHom ℤ M)) b) 1 =
    ↑(AddMonoidHom.comp (↑(AddMonoidHom.flip (smulAddHom R M)) b) (Int.castAddHom R)) 1
simp