case nil
ι : Type ?u.109197
α : Type ?u.109200
M : Type ?u.109203
N : Type ?u.109206
P : Type ?u.109209
M₀ : Type u_1
G : Type ?u.109215
R : Type ?u.109218
inst✝² : MonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
⊢ prod [] = 0 ↔ 0 ∈ []

case cons
ι : Type ?u.109197
α : Type ?u.109200
M : Type ?u.109203
N : Type ?u.109206
P : Type ?u.109209
M₀ : Type u_1
G : Type ?u.109215
R : Type ?u.109218
inst✝² : MonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
a : M₀
L : List M₀
ihL : prod L = 0 ↔ 0 ∈ L
⊢ prod (a :: L) = 0 ↔ 0 ∈ a :: L
ι : Type ?u.109197
α : Type ?u.109200
M : Type ?u.109203
N : Type ?u.109206
P : Type ?u.109209
M₀ : Type u_1
G : Type ?u.109215
R : Type ?u.109218
inst✝² : MonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
L : List M₀
⊢ prod L = 0 ↔ 0 ∈ L
induction' L with a L ihL
no goals
case nil
ι : Type ?u.109197
α : Type ?u.109200
M : Type ?u.109203
N : Type ?u.109206
P : Type ?u.109209
M₀ : Type u_1
G : Type ?u.109215
R : Type ?u.109218
inst✝² : MonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
⊢ prod [] = 0 ↔ 0 ∈ []
simp
no goals
case cons
ι : Type ?u.109197
α : Type ?u.109200
M : Type ?u.109203
N : Type ?u.109206
P : Type ?u.109209
M₀ : Type u_1
G : Type ?u.109215
R : Type ?u.109218
inst✝² : MonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
a : M₀
L : List M₀
ihL : prod L = 0 ↔ 0 ∈ L
⊢ prod (a :: L) = 0 ↔ 0 ∈ a :: L
rw [prod_cons, mul_eq_zero, ihL, mem_cons, eq_comm]