English
For all n, e ∈ Perm(Fin n), p ∈ Fin(n+1), and x ∈ Fin n, the value of decomposeFin.symm(p,e) at x.succ is the same as swapping 0 with p and then applying to (e x).succ.
Русский
Для всех n, e ∈ Perm(Fin n), p ∈ Fin(n+1) и x ∈ Fin n, значение decomposeFin.symm(p,e) на x.succ равно применению транспозиции (0 p) к (e x).succ.
LaTeX
$$$ \\mathrm{decomposeFin.symm}(p,e)(x\\.succ) = \\mathrm{swap}(0,p)\\big( (e(x)).\\mathrm{succ} \\big) \\,.$$$
Lean4
@[simp]
theorem decomposeFin_symm_apply_succ {n : ℕ} (e : Perm (Fin n)) (p : Fin (n + 1)) (x : Fin n) :
Equiv.Perm.decomposeFin.symm (p, e) x.succ = swap 0 p (e x).succ :=
by
refine Fin.cases ?_ ?_ p
· simp [Equiv.Perm.decomposeFin]
· intro i
by_cases h : i = e x
· simp [h, Equiv.Perm.decomposeFin]
· simp [Equiv.Perm.decomposeFin, swap_apply_def, Ne.symm h]
