case nil
ι : Type ?u.107956
α : Type ?u.107959
M : Type ?u.107962
N : Type ?u.107965
P : Type ?u.107968
M₀ : Type u_1
G : Type ?u.107974
R : Type ?u.107977
inst✝ : MonoidWithZero M₀
L : List M₀
h✝ : 0 ∈ L
h : 0 ∈ []
⊢ prod [] = 0

case cons
ι : Type ?u.107956
α : Type ?u.107959
M : Type ?u.107962
N : Type ?u.107965
P : Type ?u.107968
M₀ : Type u_1
G : Type ?u.107974
R : Type ?u.107977
inst✝ : MonoidWithZero M₀
L✝ : List M₀
h✝ : 0 ∈ L✝
a : M₀
L : List M₀
ihL : 0 ∈ L → prod L = 0
h : 0 ∈ a :: L
⊢ prod (a :: L) = 0
ι : Type ?u.107956
α : Type ?u.107959
M : Type ?u.107962
N : Type ?u.107965
P : Type ?u.107968
M₀ : Type u_1
G : Type ?u.107974
R : Type ?u.107977
inst✝ : MonoidWithZero M₀
L : List M₀
h : 0 ∈ L
⊢ prod L = 0
induction' L with a L ihL
no goals
case nil
ι : Type ?u.107956
α : Type ?u.107959
M : Type ?u.107962
N : Type ?u.107965
P : Type ?u.107968
M₀ : Type u_1
G : Type ?u.107974
R : Type ?u.107977
inst✝ : MonoidWithZero M₀
L : List M₀
h✝ : 0 ∈ L
h : 0 ∈ []
⊢ prod [] = 0
exact absurd h (not_mem_nil _)
case cons
ι : Type ?u.107956
α : Type ?u.107959
M : Type ?u.107962
N : Type ?u.107965
P : Type ?u.107968
M₀ : Type u_1
G : Type ?u.107974
R : Type ?u.107977
inst✝ : MonoidWithZero M₀
L✝ : List M₀
h✝ : 0 ∈ L✝
a : M₀
L : List M₀
ihL : 0 ∈ L → prod L = 0
h : 0 ∈ a :: L
⊢ a * prod L = 0
case cons
ι : Type ?u.107956
α : Type ?u.107959
M : Type ?u.107962
N : Type ?u.107965
P : Type ?u.107968
M₀ : Type u_1
G : Type ?u.107974
R : Type ?u.107977
inst✝ : MonoidWithZero M₀
L✝ : List M₀
h✝ : 0 ∈ L✝
a : M₀
L : List M₀
ihL : 0 ∈ L → prod L = 0
h : 0 ∈ a :: L
⊢ prod (a :: L) = 0
rw [prod_cons]
case cons.inl
ι : Type ?u.107956
α : Type ?u.107959
M : Type ?u.107962
N : Type ?u.107965
P : Type ?u.107968
M₀ : Type u_1
G : Type ?u.107974
R : Type ?u.107977
inst✝ : MonoidWithZero M₀
L✝ : List M₀
h✝ : 0 ∈ L✝
a : M₀
L : List M₀
ihL : 0 ∈ L → prod L = 0
h : 0 ∈ a :: L
ha : 0 = a
⊢ a * prod L = 0

case cons.inr
ι : Type ?u.107956
α : Type ?u.107959
M : Type ?u.107962
N : Type ?u.107965
P : Type ?u.107968
M₀ : Type u_1
G : Type ?u.107974
R : Type ?u.107977
inst✝ : MonoidWithZero M₀
L✝ : List M₀
h✝ : 0 ∈ L✝
a : M₀
L : List M₀
ihL : 0 ∈ L → prod L = 0
h : 0 ∈ a :: L
hL : 0 ∈ L
⊢ a * prod L = 0
case cons
ι : Type ?u.107956
α : Type ?u.107959
M : Type ?u.107962
N : Type ?u.107965
P : Type ?u.107968
M₀ : Type u_1
G : Type ?u.107974
R : Type ?u.107977
inst✝ : MonoidWithZero M₀
L✝ : List M₀
h✝ : 0 ∈ L✝
a : M₀
L : List M₀
ihL : 0 ∈ L → prod L = 0
h : 0 ∈ a :: L
⊢ a * prod L = 0
cases' mem_cons.1 h with ha hL
no goals
case cons.inl
ι : Type ?u.107956
α : Type ?u.107959
M : Type ?u.107962
N : Type ?u.107965
P : Type ?u.107968
M₀ : Type u_1
G : Type ?u.107974
R : Type ?u.107977
inst✝ : MonoidWithZero M₀
L✝ : List M₀
h✝ : 0 ∈ L✝
a : M₀
L : List M₀
ihL : 0 ∈ L → prod L = 0
h : 0 ∈ a :: L
ha : 0 = a
⊢ a * prod L = 0

case cons.inr
ι : Type ?u.107956
α : Type ?u.107959
M : Type ?u.107962
N : Type ?u.107965
P : Type ?u.107968
M₀ : Type u_1
G : Type ?u.107974
R : Type ?u.107977
inst✝ : MonoidWithZero M₀
L✝ : List M₀
h✝ : 0 ∈ L✝
a : M₀
L : List M₀
ihL : 0 ∈ L → prod L = 0
h : 0 ∈ a :: L
hL : 0 ∈ L
⊢ a * prod L = 0
exacts [mul_eq_zero_of_left ha.symm _, mul_eq_zero_of_right _ (ihL hL)]