case zero
α : Type ?u.130390
R : Type u_2
k : Type ?u.130396
S : Type ?u.130399
M : Type u_1
M₂ : Type ?u.130405
M₃ : Type ?u.130408
ι : Type ?u.130411
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : M
⊢ Nat.zero • b = ↑Nat.zero • b

case succ
α : Type ?u.130390
R : Type u_2
k : Type ?u.130396
S : Type ?u.130399
M : Type u_1
M₂ : Type ?u.130405
M₃ : Type ?u.130408
ι : Type ?u.130411
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : M
n : ℕ
ih : n • b = ↑n • b
⊢ Nat.succ n • b = ↑(Nat.succ n) • b
α : Type ?u.130390
R : Type u_2
k : Type ?u.130396
S : Type ?u.130399
M : Type u_1
M₂ : Type ?u.130405
M₃ : Type ?u.130408
ι : Type ?u.130411
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
b : M
⊢ n • b = ↑n • b
induction' n with n ih
no goals
case zero
α : Type ?u.130390
R : Type u_2
k : Type ?u.130396
S : Type ?u.130399
M : Type u_1
M₂ : Type ?u.130405
M₃ : Type ?u.130408
ι : Type ?u.130411
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : M
⊢ Nat.zero • b = ↑Nat.zero • b
rw [Nat.zero_eq, Nat.cast_zero, zero_smul, zero_smul]
no goals
case succ
α : Type ?u.130390
R : Type u_2
k : Type ?u.130396
S : Type ?u.130399
M : Type u_1
M₂ : Type ?u.130405
M₃ : Type ?u.130408
ι : Type ?u.130411
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : M
n : ℕ
ih : n • b = ↑n • b
⊢ Nat.succ n • b = ↑(Nat.succ n) • b
rw [Nat.succ_eq_add_one, Nat.cast_succ, add_smul, add_smul, one_smul, ih, one_smul]