Theorem: Tutorial.mem_of_eq_one (Solution/Advanced/Algebra/Lecture5.lean)

State before:
G : Type
inst✝¹ : Group G
N : Subgroup G
inst✝ : Subgroup.Normal N
a : G
⊢ LeftQuotient.mk a = 1 ↔ a ∈ N
Tactic:
simp [N.inv_mem_iff]
State after:
no goals