case zero
α : Type ?u.8662
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
⊢ Nat.zero • 0 = 0

case succ
α : Type ?u.8662
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
n : ℕ
ih : n • 0 = 0
⊢ Nat.succ n • 0 = 0
α : Type ?u.8662
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
n : ℕ
⊢ n • 0 = 0
induction' n with n ih
no goals
case zero
α : Type ?u.8662
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
⊢ Nat.zero • 0 = 0
exact zero_nsmul _
no goals
case succ
α : Type ?u.8662
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
n : ℕ
ih : n • 0 = 0
⊢ Nat.succ n • 0 = 0
rw [succ_nsmul, ih, add_zero]