no goals
G : Type u_1
H : Type ?u.40911
A : Type ?u.40914
a a₁ a₂ b c : G
inst✝ : Group G
⊢ 1 ∈ center G
simp [center]
no goals
G : Type u_1
H : Type ?u.40911
A : Type ?u.40914
a a₁ a₂ b c : G
inst✝ : Group G
a✝ b✝ : G
ha : a✝ ∈ center G
hb : b✝ ∈ center G
g : G
⊢ g * (a✝ * b✝) = a✝ * b✝ * g
rw [← mul_assoc, mem_center.2 ha g, mul_assoc, mem_center.2 hb g, ← mul_assoc]
no goals
G : Type u_1
H : Type ?u.40911
A : Type ?u.40914
a✝ a₁ a₂ b c : G
inst✝ : Group G
a : G
ha : a ∈ center G
g : G
⊢ g * a⁻¹ = a⁻¹ * (g * a) * a⁻¹
simp [ha g]
G : Type u_1
H : Type ?u.40911
A : Type ?u.40914
a✝ a₁ a₂ b c : G
inst✝ : Group G
a : G
ha : a ∈ center G
g : G
⊢ a⁻¹ * g * (a * a⁻¹) = a⁻¹ * g
G : Type u_1
H : Type ?u.40911
A : Type ?u.40914
a✝ a₁ a₂ b c : G
inst✝ : Group G
a : G
ha : a ∈ center G
g : G
⊢ a⁻¹ * (g * a) * a⁻¹ = a⁻¹ * g
rw [← mul_assoc, mul_assoc]
no goals
G : Type u_1
H : Type ?u.40911
A : Type ?u.40914
a✝ a₁ a₂ b c : G
inst✝ : Group G
a : G
ha : a ∈ center G
g : G
⊢ a⁻¹ * g * (a * a⁻¹) = a⁻¹ * g
simp
no goals
G : Type u_1
H : Type ?u.40911
A : Type ?u.40914
a a₁ a₂ b c : G
inst✝ : Group G
n : G
ha : n ∈ center G
g h : G
⊢ h * (g * n * g⁻¹) = h * n
simp [ha g, mul_assoc]
G : Type u_1
H : Type ?u.40911
A : Type ?u.40914
a a₁ a₂ b c : G
inst✝ : Group G
n : G
ha : n ∈ center G
g h : G
⊢ n * h = g * g⁻¹ * n * h
G : Type u_1
H : Type ?u.40911
A : Type ?u.40914
a a₁ a₂ b c : G
inst✝ : Group G
n : G
ha : n ∈ center G
g h : G
⊢ h * n = g * g⁻¹ * n * h
rw [ha h]
no goals
G : Type u_1
H : Type ?u.40911
A : Type ?u.40914
a a₁ a₂ b c : G
inst✝ : Group G
n : G
ha : n ∈ center G
g h : G
⊢ n * h = g * g⁻¹ * n * h
simp
no goals
G : Type u_1
H : Type ?u.40911
A : Type ?u.40914
a a₁ a₂ b c : G
inst✝ : Group G
n : G
ha : n ∈ center G
g h : G
⊢ g * g⁻¹ * n * h = g * n * g⁻¹ * h
rw [mul_assoc g, ha g⁻¹, ← mul_assoc]