no goals
M : Type u_1
N : Type ?u.162461
P : Type ?u.162464
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S✝ : Submonoid M
A : Type ?u.162485
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
S : Submonoid M
⊢ (∃ x hx, { val := x, property := hx } ≠ { val := 1, property := (_ : 1 ∈ S) }) ↔ ∃ x, x ∈ S ∧ x ≠ 1
simp [Ne.def]