no goals
M : Type u_1
N : Type ?u.19160
A : Type ?u.19163
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
h : Subsingleton M
x y : Submonoid M
i : M
⊢ 1 ∈ x ↔ 1 ∈ y
simp [Submonoid.one_mem]