Theorem: Tutorial.mem_of_eq_one (Tutorial/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:
sorry
State after:
no goals