-- Mathlib/GroupTheory/Subgroup/Center.lean
theorem mk_bijOn (G : Type*) [Group G] :
    Set.BijOn ConjClasses.mk (↑(Subgroup.center G)) (noncenter G)ᶜ

Proof state:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : Quot.mk (⇑(IsConj.setoid G)) g ∈ (noncenter G)ᶜ
⊢ Quot.mk (⇑(IsConj.setoid G)) g ∈ ConjClasses.mk '' ↑(Subgroup.center G)

Tactic:
refine ⟨g, ?_, rfl⟩

Result:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : Quot.mk (⇑(IsConj.setoid G)) g ∈ (noncenter G)ᶜ
⊢ g ∈ ↑(Subgroup.center G)

Proof state:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
h : G
⊢ IsConj (h * g * h⁻¹) g

Tactic:
rw [isConj_comm, isConj_iff]

Result:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
h : G
⊢ ∃ c, c * g * c⁻¹ = h * g * h⁻¹

Proof state:
case refine_3
G : Type u_2
inst✝ : Group G
⊢ Set.SurjOn ConjClasses.mk (↑(Subgroup.center G)) (noncenter G)ᶜ

Tactic:
rintro ⟨g⟩ hg

Result:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : Quot.mk (⇑(IsConj.setoid G)) g ∈ (noncenter G)ᶜ
⊢ Quot.mk (⇑(IsConj.setoid G)) g ∈ ConjClasses.mk '' ↑(Subgroup.center G)

Proof state:
case refine_1
G : Type u_2
inst✝ : Group G
g : G
hg : g ∈ ↑(Subgroup.center G)
⊢ ConjClasses.mk g ∈ (noncenter G)ᶜ

Tactic:
simp only [mem_noncenter, Set.compl_def, Set.mem_setOf, Set.not_nontrivial_iff]

Result:
case refine_1
G : Type u_2
inst✝ : Group G
g : G
hg : g ∈ ↑(Subgroup.center G)
⊢ (ConjClasses.mk g).carrier.Subsingleton

Proof state:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
⊢ ∀ (g_1 : G), g_1 * g = g * g_1

Tactic:
intro h

Result:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
h : G
⊢ h * g = g * h

Proof state:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : Quot.mk (⇑(IsConj.setoid G)) g ∈ (noncenter G)ᶜ
⊢ g ∈ ↑(Subgroup.center G)

Tactic:
simp only [mem_noncenter, Set.compl_def, Set.mem_setOf, Set.not_nontrivial_iff] at hg

Result:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
⊢ g ∈ ↑(Subgroup.center G)

Proof state:
case refine_1
G : Type u_2
inst✝ : Group G
g : G
hg : g ∈ ↑(Subgroup.center G)
⊢ (ConjClasses.mk g).carrier.Subsingleton

Tactic:
intro x hx y hy

Result:
case refine_1
G : Type u_2
inst✝ : Group G
g : G
hg : g ∈ ↑(Subgroup.center G)
x : G
hx : x ∈ (ConjClasses.mk g).carrier
y : G
hy : y ∈ (ConjClasses.mk g).carrier
⊢ x = y

Proof state:
case refine_2
G : Type u_2
inst✝ : Group G
x : G
hx : x ∈ ↑(Subgroup.center G)
y : G
x✝ : y ∈ ↑(Subgroup.center G)
H : ConjClasses.mk x = ConjClasses.mk y
⊢ x = y

Tactic:
rw [mk_eq_mk_iff_isConj] at H

Result:
case refine_2
G : Type u_2
inst✝ : Group G
x : G
hx : x ∈ ↑(Subgroup.center G)
y : G
x✝ : y ∈ ↑(Subgroup.center G)
H : IsConj x y
⊢ x = y

Proof state:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
⊢ g ∈ ↑(Subgroup.center G)

Tactic:
rw [SetLike.mem_coe, Subgroup.mem_center_iff]

Result:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
⊢ ∀ (g_1 : G), g_1 * g = g * g_1

Proof state:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
h : G
⊢ h * g = g * h

Tactic:
rw [← mul_inv_eq_iff_eq_mul]

Result:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
h : G
⊢ h * g * h⁻¹ = g

Proof state:
case refine_2
G : Type u_2
inst✝ : Group G
x : G
hx : x ∈ ↑(Subgroup.center G)
y : G
x✝ : y ∈ ↑(Subgroup.center G)
H : IsConj x y
⊢ x = y

Tactic:
exact H.eq_of_left_mem_center hx

Result:
no goals

Proof state:
G : Type u_2
inst✝ : Group G
⊢ Set.BijOn ConjClasses.mk (↑(Subgroup.center G)) (noncenter G)ᶜ

Tactic:
refine ⟨fun g hg ↦ ?_, fun x hx y _ H ↦ ?_, ?_⟩

Result:
case refine_1
G : Type u_2
inst✝ : Group G
g : G
hg : g ∈ ↑(Subgroup.center G)
⊢ ConjClasses.mk g ∈ (noncenter G)ᶜ

case refine_2
G : Type u_2
inst✝ : Group G
x : G
hx : x ∈ ↑(Subgroup.center G)
y : G
x✝ : y ∈ ↑(Subgroup.center G)
H : ConjClasses.mk x = ConjClasses.mk y
⊢ x = y

case refine_3
G : Type u_2
inst✝ : Group G
⊢ Set.SurjOn ConjClasses.mk (↑(Subgroup.center G)) (noncenter G)ᶜ

Proof state:
case refine_1
G : Type u_2
inst✝ : Group G
g : G
hg : g ∈ ↑(Subgroup.center G)
x : G
hx : x ∈ (ConjClasses.mk g).carrier
y : G
hy : y ∈ (ConjClasses.mk g).carrier
⊢ x = y

Tactic:
simp only [mem_carrier_iff_mk_eq, mk_eq_mk_iff_isConj] at hx hy

Result:
case refine_1
G : Type u_2
inst✝ : Group G
g : G
hg : g ∈ ↑(Subgroup.center G)
x y : G
hx : IsConj x g
hy : IsConj y g
⊢ x = y

Proof state:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
h : G
⊢ ConjClasses.mk (h * g * h⁻¹) = Quot.mk (⇑(IsConj.setoid G)) g

Tactic:
apply mk_eq_mk_iff_isConj.mpr

Result:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
h : G
⊢ IsConj (h * g * h⁻¹) g

Proof state:
case refine_1
G : Type u_2
inst✝ : Group G
g : G
hg : g ∈ ↑(Subgroup.center G)
x y : G
hx : IsConj x g
hy : IsConj y g
⊢ x = y

Tactic:
rw [hx.eq_of_right_mem_center hg, hy.eq_of_right_mem_center hg]

Result:
no goals

Proof state:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
h : G
⊢ h * g * h⁻¹ = g

Tactic:
refine hg ?_ mem_carrier_mk

Result:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
h : G
⊢ h * g * h⁻¹ ∈ carrier (Quot.mk (⇑(IsConj.setoid G)) g)

Proof state:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
h : G
⊢ h * g * h⁻¹ ∈ carrier (Quot.mk (⇑(IsConj.setoid G)) g)

Tactic:
rw [mem_carrier_iff_mk_eq]

Result:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
h : G
⊢ ConjClasses.mk (h * g * h⁻¹) = Quot.mk (⇑(IsConj.setoid G)) g

Proof state:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
h : G
⊢ ∃ c, c * g * c⁻¹ = h * g * h⁻¹

Tactic:
exact ⟨h, rfl⟩

Result:
no goals