-- Mathlib/Algebra/Star/Center.lean
theorem Set.star_mem_center (ha : a ∈ Set.center R) : star a ∈ Set.center R where
  comm

Proof state:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ star a * star (star c * star b) = star (star c * star b * a)

Tactic:
rw [← star_mul]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ star (star c * star (b * star a)) = star (star c * (a * star b))

Tactic:
rw [star_mul b, star_star]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ b * star (a * star c) = b * (c * star a)

Tactic:
rw [star_mul, star_star]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
a : R
ha : a ∈ center R
⊢ ∀ (a_1 : R), star a * a_1 = a_1 * star a

Tactic:
simpa only [star_mul, star_star] using fun g =>
congr_arg star ((mem_center_iff.1 ha).comm <| star g).symm

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ star (star c * star b * a) = star (star c * (star b * a))

Tactic:
rw [ha.right_assoc]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ b * star a * c = star (star c * star (b * star a))

Tactic:
rw [← star_mul, star_star]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ star a * (b * c) = star a * (star (star b) * star (star c))

Tactic:
rw [star_star, star_star]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ star (star b * a) * c = star a * b * c

Tactic:
rw [star_mul, star_star]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ star (a * (star c * star b)) = star (a * star c * star b)

Tactic:
rw [ha.left_assoc]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ star (star c * a * star b) = b * (star a * c)

Tactic:
rw [star_mul, star_star, star_mul (star c), star_star]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ b * c * star a = star (a * star (b * c))

Tactic:
rw [star_mul, star_star]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ star (star c * (star b * a)) = star (star b * a) * c

Tactic:
rw [star_mul, star_star]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ star a * (star (star b) * star (star c)) = star a * star (star c * star b)

Tactic:
rw [star_mul]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ star (a * star (b * c)) = star (a * (star c * star b))

Tactic:
rw [star_mul b]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ star (star c * (a * star b)) = star (star c * a * star b)

Tactic:
rw [ha.mid_assoc]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ star (a * star c * star b) = b * star (a * star c)

Tactic:
rw [star_mul, star_star]

Result:
no goals