English
For l a list, f a permutation, e an equivalence α ≃ Fin(n) with hs guaranteeing membership by nonempty condition, one has signAux ((e⁻¹ f e)) = signAux2 l f under the hypothesis ht relating to ht and hs.
Русский
Пусть l — список, f перестановка, e эквивелентность α ≃ Fin(n) с условием hs, ht; тогда signAux((e⁻¹ f e)) = signAux2(l,f) при соответствующих предпосылках.
LaTeX
$$$\forall l,f,e,\ hs,ht,\ (\forall x, f(x) \neq x \Rightarrow x \in l) \Rightarrow signAux((e^{-1} f e)) = signAux2(l,f)$$$
Lean4
theorem signAux_eq_signAux2 {n : ℕ} :
∀ (l : List α) (f : Perm α) (e : α ≃ Fin n) (_h : ∀ x, f x ≠ x → x ∈ l),
signAux ((e.symm.trans f).trans e) = signAux2 l f
| [], f, e, h => by
have : f = 1 := Equiv.ext fun y => Classical.not_not.1 (mt (h y) List.not_mem_nil)
rw [this, one_def, Equiv.trans_refl, Equiv.symm_trans_self, ← one_def, signAux_one, signAux2]
| x :: l, f, e, h => by
rw [signAux2]
by_cases hfx : x = f x
· rw [if_pos hfx]
exact
signAux_eq_signAux2 l f _ fun y (hy : f y ≠ y) =>
List.mem_of_ne_of_mem (fun h : y = x => by simp [h, hfx.symm] at hy) (h y hy)
· have hy : ∀ y : α, (swap x (f x) * f) y ≠ y → y ∈ l := fun y hy =>
have : f y ≠ y ∧ y ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hy
List.mem_of_ne_of_mem this.2 (h _ this.1)
have : (e.symm.trans (swap x (f x) * f)).trans e = swap (e x) (e (f x)) * (e.symm.trans f).trans e :=
by
ext
rw [← Equiv.symm_trans_swap_trans, mul_def, Equiv.symm_trans_swap_trans, mul_def]
repeat (rw [trans_apply])
simp [swap, swapCore]
split_ifs <;> rfl
have hefx : e x ≠ e (f x) := mt e.injective.eq_iff.1 hfx
rw [if_neg hfx, ← signAux_eq_signAux2 _ _ e hy, this, signAux_mul, signAux_swap hefx]
simp only [neg_neg, one_mul, neg_mul]
