no goals
α : Type ?u.9319
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : A
m n : ℕ
⊢ (m + n) • a = m • a + n • a
induction m with
| zero => rw [Nat.zero_add, zero_nsmul, zero_add]
| succ m ih => rw [Nat.succ_add, Nat.succ_eq_add_one, succ_nsmul, ih, succ_nsmul, add_assoc]
no goals
case zero
α : Type ?u.9319
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : A
n : ℕ
⊢ (Nat.zero + n) • a = Nat.zero • a + n • a
rw [Nat.zero_add, zero_nsmul, zero_add]
no goals
case succ
α : Type ?u.9319
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝¹ : Monoid M
inst✝ : AddMonoid A
a : A
n m : ℕ
ih : (m + n) • a = m • a + n • a
⊢ (Nat.succ m + n) • a = Nat.succ m • a + n • a
rw [Nat.succ_add, Nat.succ_eq_add_one, succ_nsmul, ih, succ_nsmul, add_assoc]