Theorem: MulEquiv.mem_iff_map_mem_units_of_mem_iff_map_mem (Controlbits/Submonoid.lean)

State before:
G : Type u_1
M : Type u_2
inst✝¹ : Group G
inst✝ : Monoid M
e : G ≃* Mˣ
S : Subgroup G
T : Submonoid M
h : ∀ (s : G), s ∈ S ↔ ↑(e s) ∈ T
s : G
⊢ s ∈ S ↔ e s ∈ T.units
Tactic:
simp_rw [Submonoid.mem_units_iff, ← e.map_inv, ← h, iff_self_and, inv_mem_iff, imp_self]
State after:
no goals