no goals
ι : Type ?u.145057
α : Type ?u.145060
M : Type u_1
N : Type ?u.145066
P : Type ?u.145069
M₀ : Type ?u.145072
G : Type ?u.145075
R : Type ?u.145078
inst✝ : Monoid M
l : List M
h : prod l ≠ 1
⊢ ∃ x, x ∈ l ∧ x ≠ 1
simpa only [not_forall, exists_prop] using mt prod_eq_one h