α : Type u
β : Type v
inst✝ : Monoid α
a : α
⊢ ∀ {b : ConjClasses α}, a ∈ carrier b ↔ ConjClasses.mk a = b
α : Type u
β : Type v
inst✝ : Monoid α
a : α
b : ConjClasses α
⊢ a ∈ carrier b ↔ ConjClasses.mk a = b
revert b
α : Type u
β : Type v
inst✝ : Monoid α
a : α
⊢ ∀ (a_1 : α), a ∈ carrier (ConjClasses.mk a_1) ↔ ConjClasses.mk a = ConjClasses.mk a_1
α : Type u
β : Type v
inst✝ : Monoid α
a : α
⊢ ∀ {b : ConjClasses α}, a ∈ carrier b ↔ ConjClasses.mk a = b
rw [forall_isConj]
α : Type u
β : Type v
inst✝ : Monoid α
a b : α
⊢ a ∈ carrier (ConjClasses.mk b) ↔ ConjClasses.mk a = ConjClasses.mk b
α : Type u
β : Type v
inst✝ : Monoid α
a : α
⊢ ∀ (a_1 : α), a ∈ carrier (ConjClasses.mk a_1) ↔ ConjClasses.mk a = ConjClasses.mk a_1
intro b
α : Type u
β : Type v
inst✝ : Monoid α
a b : α
⊢ a ∈ conjugatesOf b ↔ IsConj b a
α : Type u
β : Type v
inst✝ : Monoid α
a b : α
⊢ a ∈ carrier (ConjClasses.mk b) ↔ ConjClasses.mk a = ConjClasses.mk b
rw [carrier, eq_comm, mk_eq_mk_iff_isConj, ← quotient_mk_eq_mk, Quotient.lift_mk]
no goals
α : Type u
β : Type v
inst✝ : Monoid α
a b : α
⊢ a ∈ conjugatesOf b ↔ IsConj b a
rfl