M✝ : Type ?u.38952
N : Type ?u.38955
A : Type ?u.38958
inst✝² : Monoid M✝
inst✝¹ : Monoid N
s : Set M✝
M : Type u_1
inst✝ : Monoid M
a : M
⊢ a ∈ setOf IsUnit ↔ IsUnit a
M✝ : Type ?u.38952
N : Type ?u.38955
A : Type ?u.38958
inst✝² : Monoid M✝
inst✝¹ : Monoid N
s : Set M✝
M : Type u_1
inst✝ : Monoid M
a : M
⊢ a ∈ submonoid M ↔ IsUnit a
change a ∈ setOf IsUnit ↔ IsUnit a
no goals
M✝ : Type ?u.38952
N : Type ?u.38955
A : Type ?u.38958
inst✝² : Monoid M✝
inst✝¹ : Monoid N
s : Set M✝
M : Type u_1
inst✝ : Monoid M
a : M
⊢ a ∈ setOf IsUnit ↔ IsUnit a
rw [Set.mem_setOf_eq]