case zero
R : Type ?u.18144
S : Type ?u.18147
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : NoZeroDivisors M
x : M
n : ℕ
H✝ : x ^ n = 0
H : x ^ Nat.zero = 0
⊢ x = 0

case succ
R : Type ?u.18144
S : Type ?u.18147
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : NoZeroDivisors M
x : M
n✝ : ℕ
H✝ : x ^ n✝ = 0
n : ℕ
ih : x ^ n = 0 → x = 0
H : x ^ Nat.succ n = 0
⊢ x = 0
R : Type ?u.18144
S : Type ?u.18147
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : NoZeroDivisors M
x : M
n : ℕ
H : x ^ n = 0
⊢ x = 0
induction' n with n ih
case zero
R : Type ?u.18144
S : Type ?u.18147
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : NoZeroDivisors M
x : M
n : ℕ
H✝ : x ^ n = 0
H : 1 = 0
⊢ x = 0
case zero
R : Type ?u.18144
S : Type ?u.18147
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : NoZeroDivisors M
x : M
n : ℕ
H✝ : x ^ n = 0
H : x ^ Nat.zero = 0
⊢ x = 0
rw [pow_zero] at H
no goals
case zero
R : Type ?u.18144
S : Type ?u.18147
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : NoZeroDivisors M
x : M
n : ℕ
H✝ : x ^ n = 0
H : 1 = 0
⊢ x = 0
rw [← mul_one x, H, mul_zero]
case succ
R : Type ?u.18144
S : Type ?u.18147
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : NoZeroDivisors M
x : M
n✝ : ℕ
H✝ : x ^ n✝ = 0
n : ℕ
ih : x ^ n = 0 → x = 0
H : x * x ^ n = 0
⊢ x = 0
case succ
R : Type ?u.18144
S : Type ?u.18147
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : NoZeroDivisors M
x : M
n✝ : ℕ
H✝ : x ^ n✝ = 0
n : ℕ
ih : x ^ n = 0 → x = 0
H : x ^ Nat.succ n = 0
⊢ x = 0
rw [pow_succ] at H
no goals
case succ
R : Type ?u.18144
S : Type ?u.18147
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : NoZeroDivisors M
x : M
n✝ : ℕ
H✝ : x ^ n✝ = 0
n : ℕ
ih : x ^ n = 0 → x = 0
H : x * x ^ n = 0
⊢ x = 0
exact Or.casesOn (mul_eq_zero.1 H) id ih