case h
α : Type ?u.77795
M : Type ?u.77798
G : Type u_1
G₀ : Type ?u.77804
R : Type ?u.77807
K : Type ?u.77810
inst✝ : Group G
x : G
⊢ x ∈ fixedPoints (ConjAct G) G ↔ x ∈ ↑(center G)
α : Type ?u.77795
M : Type ?u.77798
G : Type u_1
G₀ : Type ?u.77804
R : Type ?u.77807
K : Type ?u.77810
inst✝ : Group G
⊢ fixedPoints (ConjAct G) G = ↑(center G)
ext x
no goals
case h
α : Type ?u.77795
M : Type ?u.77798
G : Type u_1
G₀ : Type ?u.77804
R : Type ?u.77807
K : Type ?u.77810
inst✝ : Group G
x : G
⊢ x ∈ fixedPoints (ConjAct G) G ↔ x ∈ ↑(center G)
simp [mem_center_iff, smul_def, mul_inv_eq_iff_eq_mul]