I think the definition of ps_inv is not very appropriate."ps_mul_left_inv" can be proved like this.

[chenjulang]

Let's talk in here if you have time: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20Rubik's.20cube.20associative.20law.3F

def ps_inv {p o : ℕ+} : PieceState p o → PieceState p o := fun ps => { permute := ps.permute⁻¹ -- 0 1 2 -- 举例:如果原方向增加量orient为(1,2,...)，那么逆操作应该是(-1,-2,...) , 也就是(+2,+1,...) -- 比如 a:F { -- permute: Perm (Fin 8) := (1=>2,2=>6,3,4,5=>1,6=>5,7,8) -- 有8项 -- orient : Vector (Fin 3) 8 := (2,1,0,0,1,2,0,0) -- 有8项 --} -- 那么 -a:F' { -- permute: Perm (Fin 8) := (1<=2,2<=6,3,4,5<=1,6<=5,7,8) -- 有8项 -- orient : Vector (Fin 3) 8 := (2,1,0,0,1,2,0,0) -- 有8项 --} --todo -- 定义应该找位置2还是找位置5??? -- 关键是经过a操作增量后，再经过a'增量，应该为0 -- 也就是需要满足 ps_mul a a' = {orient:0} -- a'.orient ∘ a.permute.invFun + a.orient = 0 -- 因此 a'.orient ∘ a.permute.invFun = -a.orient

-- orient := fun x => - ps.orient (ps.permute⁻¹ x)
orient := (-ps.orient) ∘ ps.permute

}

lemma ps_mul_left_inv {p o : ℕ+} : ∀ (a : PieceState p o), ps_mul (ps_inv a) a = {permute := 1, orient := 0} -- 比如 a:F { -- permute: Perm (Fin 8) := (1=>2,2=>6,3,4,5=>1,6=>5,7,8) -- 有8项 -- orient : Vector (Fin 3) 8 := (2,1,0,0,1,2,0,0) -- 有8项 --} -- 那么 -a:F' { -- permute: Perm (Fin 8) := (1<=2,2<=6,3,4,5<=1,6<=5,7,8) -- 有8项 -- orient : Vector (Fin 3) 8 := (2,1,0,0,1,2,0,0) -- 有8项 --} := by intro a simp only [ps_inv] simp only [ps_mul] simp only [mul_left_inv] simp only [invFun_as_coe, PieceState.mk.injEq, true_and] exact neg_eq_iff_add_eq_zero.mp rfl

[chenjulang]

I made a mistake...Forget it