[GOAL]
α✝ : Type u
β : Type v
inst✝² : Monoid α✝
inst✝¹ : Monoid β
α : Type u_1
inst✝ : CommMonoid α
a b : α
x✝ : IsConj a b
c : αˣ
hc : SemiconjBy (↑c) a b
⊢ a = b
[PROOFSTEP]
rw [SemiconjBy, mul_comm, ← Units.mul_inv_eq_iff_eq_mul, mul_assoc, c.mul_inv, mul_one] at hc 
[GOAL]
α✝ : Type u
β : Type v
inst✝² : Monoid α✝
inst✝¹ : Monoid β
α : Type u_1
inst✝ : CommMonoid α
a b : α
x✝ : IsConj a b
c : αˣ
hc : a = b
⊢ a = b
[PROOFSTEP]
exact hc
[GOAL]
α✝ : Type u
β : Type v
inst✝² : Monoid α✝
inst✝¹ : Monoid β
α : Type u_1
inst✝ : CommMonoid α
a b : α
h : a = b
⊢ IsConj a b
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
a b : α
c : αˣ
hc : SemiconjBy (↑c) a b
⊢ SemiconjBy (↑(↑(Units.map f) c)) (↑f a) (↑f b)
[PROOFSTEP]
rw [Units.coe_map, SemiconjBy, ← f.map_mul, hc.eq, f.map_mul]
[GOAL]
α : Type u
β : Type v
inst✝ : CancelMonoid α
a : α
h : a = 1
⊢ IsConj 1 a
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u
β : Type v
inst✝ : Group α
i : ℕ
a b : α
⊢ (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹
[PROOFSTEP]
induction' i with i hi
[GOAL]
case zero
α : Type u
β : Type v
inst✝ : Group α
a b : α
⊢ (a * b * a⁻¹) ^ Nat.zero = a * b ^ Nat.zero * a⁻¹
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u
β : Type v
inst✝ : Group α
a b : α
i : ℕ
hi : (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹
⊢ (a * b * a⁻¹) ^ Nat.succ i = a * b ^ Nat.succ i * a⁻¹
[PROOFSTEP]
simp [pow_succ, hi]
[GOAL]
α : Type u
β : Type v
inst✝ : Group α
i : ℤ
a b : α
⊢ (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹
[PROOFSTEP]
induction' i
[GOAL]
case ofNat
α : Type u
β : Type v
inst✝ : Group α
a b : α
a✝ : ℕ
⊢ (a * b * a⁻¹) ^ Int.ofNat a✝ = a * b ^ Int.ofNat a✝ * a⁻¹
[PROOFSTEP]
change (a * b * a⁻¹) ^ (_ : ℤ) = a * b ^ (_ : ℤ) * a⁻¹
[GOAL]
case ofNat
α : Type u
β : Type v
inst✝ : Group α
a b : α
a✝ : ℕ
⊢ (a * b * a⁻¹) ^ Int.ofNat a✝ = a * b ^ Int.ofNat a✝ * a⁻¹
[PROOFSTEP]
simp [zpow_ofNat]
[GOAL]
case negSucc
α : Type u
β : Type v
inst✝ : Group α
a b : α
a✝ : ℕ
⊢ (a * b * a⁻¹) ^ Int.negSucc a✝ = a * b ^ Int.negSucc a✝ * a⁻¹
[PROOFSTEP]
simp [zpow_negSucc, conj_pow]
[GOAL]
case negSucc
α : Type u
β : Type v
inst✝ : Group α
a b : α
a✝ : ℕ
⊢ a * ((b ^ (a✝ + 1))⁻¹ * a⁻¹) = a * (b ^ (a✝ + 1))⁻¹ * a⁻¹
[PROOFSTEP]
rw [mul_assoc]
  -- Porting note: Added `change`, `zpow_ofNat`, and `rw`.
[GOAL]
α : Type u
β : Type v
inst✝ : GroupWithZero α
a b : α
x✝ : IsConj a b
c : αˣ
hc : SemiconjBy (↑c) a b
⊢ ↑c ≠ 0 ∧ ↑c * a * (↑c)⁻¹ = b
[PROOFSTEP]
rw [← Units.val_inv_eq_inv_val, Units.mul_inv_eq_iff_eq_mul]
[GOAL]
α : Type u
β : Type v
inst✝ : GroupWithZero α
a b : α
x✝ : IsConj a b
c : αˣ
hc : SemiconjBy (↑c) a b
⊢ ↑c ≠ 0 ∧ ↑c * a = b * ↑c
[PROOFSTEP]
exact ⟨c.ne_zero, hc⟩
[GOAL]
α : Type u
β : Type v
inst✝ : GroupWithZero α
a b : α
x✝ : ∃ c, c ≠ 0 ∧ c * a * c⁻¹ = b
c : α
c0 : c ≠ 0
hc : c * a * c⁻¹ = b
⊢ SemiconjBy (↑(Units.mk0 c c0)) a b
[PROOFSTEP]
rw [SemiconjBy, ← Units.mul_inv_eq_iff_eq_mul, Units.val_inv_eq_inv_val, Units.val_mk0]
[GOAL]
α : Type u
β : Type v
inst✝ : GroupWithZero α
a b : α
x✝ : ∃ c, c ≠ 0 ∧ c * a * c⁻¹ = b
c : α
c0 : c ≠ 0
hc : c * a * c⁻¹ = b
⊢ c * a * c⁻¹ = b
[PROOFSTEP]
exact hc
[GOAL]
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
hf : Function.Surjective ↑f
⊢ Function.Surjective (map f)
[PROOFSTEP]
intro b
[GOAL]
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
hf : Function.Surjective ↑f
b : ConjClasses β
⊢ ∃ a, map f a = b
[PROOFSTEP]
obtain ⟨b, rfl⟩ := ConjClasses.mk_surjective b
[GOAL]
case intro
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
hf : Function.Surjective ↑f
b : β
⊢ ∃ a, map f a = ConjClasses.mk b
[PROOFSTEP]
obtain ⟨a, rfl⟩ := hf b
[GOAL]
case intro.intro
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
hf : Function.Surjective ↑f
a : α
⊢ ∃ a_1, map f a_1 = ConjClasses.mk (↑f a)
[PROOFSTEP]
exact ⟨ConjClasses.mk a, rfl⟩
[GOAL]
α : Type u
β : Type v
inst✝ : CommMonoid α
⊢ Function.RightInverse (Quotient.lift id (_ : ∀ (a b : α), IsConj a b → a = b)) ConjClasses.mk
[PROOFSTEP]
rw [Function.RightInverse, Function.LeftInverse, forall_isConj]
[GOAL]
α : Type u
β : Type v
inst✝ : CommMonoid α
⊢ ∀ (a : α),
    ConjClasses.mk (Quotient.lift id (_ : ∀ (a b : α), IsConj a b → a = b) (ConjClasses.mk a)) = ConjClasses.mk a
[PROOFSTEP]
intro x
[GOAL]
α : Type u
β : Type v
inst✝ : CommMonoid α
x : α
⊢ ConjClasses.mk (Quotient.lift id (_ : ∀ (a b : α), IsConj a b → a = b) (ConjClasses.mk x)) = ConjClasses.mk x
[PROOFSTEP]
rw [← quotient_mk_eq_mk, ← quotient_mk_eq_mk, Quotient.lift_mk, id.def]
[GOAL]
α : Type u
β : Type v
inst✝ : Monoid α
a b : α
h : conjugatesOf a = conjugatesOf b
⊢ IsConj a b
[PROOFSTEP]
have ha := @mem_conjugatesOf_self _ _ b
[GOAL]
α : Type u
β : Type v
inst✝ : Monoid α
a b : α
h : conjugatesOf a = conjugatesOf b
ha : b ∈ conjugatesOf b
⊢ IsConj a b
[PROOFSTEP]
rwa [← h] at ha 
[GOAL]
α : Type u
β : Type v
inst✝ : Monoid α
a : α
b : ConjClasses α
⊢ a ∈ carrier b ↔ ConjClasses.mk a = b
[PROOFSTEP]
revert b
[GOAL]
α : Type u
β : Type v
inst✝ : Monoid α
a : α
⊢ ∀ {b : ConjClasses α}, a ∈ carrier b ↔ ConjClasses.mk a = b
[PROOFSTEP]
rw [forall_isConj]
[GOAL]
α : Type u
β : Type v
inst✝ : Monoid α
a : α
⊢ ∀ (a_1 : α), a ∈ carrier (ConjClasses.mk a_1) ↔ ConjClasses.mk a = ConjClasses.mk a_1
[PROOFSTEP]
intro b
[GOAL]
α : Type u
β : Type v
inst✝ : Monoid α
a b : α
⊢ a ∈ carrier (ConjClasses.mk b) ↔ ConjClasses.mk a = ConjClasses.mk b
[PROOFSTEP]
rw [carrier, eq_comm, mk_eq_mk_iff_isConj, ← quotient_mk_eq_mk, Quotient.lift_mk]
[GOAL]
α : Type u
β : Type v
inst✝ : Monoid α
a b : α
⊢ a ∈ conjugatesOf b ↔ IsConj b a
[PROOFSTEP]
rfl
