G✝ : Type ?u.362185
G' : Type ?u.362188
inst✝³ : Group G✝
inst✝² : Group G'
A : Type ?u.362197
inst✝¹ : AddGroup A
H K : Subgroup G✝
G : Type u_1
inst✝ : CommGroup G
⊢ ∀ (x : G), x ∈ center G
G✝ : Type ?u.362185
G' : Type ?u.362188
inst✝³ : Group G✝
inst✝² : Group G'
A : Type ?u.362197
inst✝¹ : AddGroup A
H K : Subgroup G✝
G : Type u_1
inst✝ : CommGroup G
⊢ center G = ⊤
rw [eq_top_iff']
G✝ : Type ?u.362185
G' : Type ?u.362188
inst✝³ : Group G✝
inst✝² : Group G'
A : Type ?u.362197
inst✝¹ : AddGroup A
H K : Subgroup G✝
G : Type u_1
inst✝ : CommGroup G
x y : G
⊢ y * x = x * y
G✝ : Type ?u.362185
G' : Type ?u.362188
inst✝³ : Group G✝
inst✝² : Group G'
A : Type ?u.362197
inst✝¹ : AddGroup A
H K : Subgroup G✝
G : Type u_1
inst✝ : CommGroup G
⊢ ∀ (x : G), x ∈ center G
intro x y
no goals
G✝ : Type ?u.362185
G' : Type ?u.362188
inst✝³ : Group G✝
inst✝² : Group G'
A : Type ?u.362197
inst✝¹ : AddGroup A
H K : Subgroup G✝
G : Type u_1
inst✝ : CommGroup G
x y : G
⊢ y * x = x * y
exact mul_comm y x