English
For finite α, β with e: α ≃ β, signAux3((e^{-1} f e)) ht = signAux3 f hs under ht/hs membership conditions.
Русский
Для конечных множества α, β с e: α ≃ β, выполняется signAux3((e^{-1} f e)) ht = signAux3 f hs при условиях принадлежности ht/hs.
LaTeX
$$$\forall f, e, hs, ht,\ signAux3((e^{-1} f e)) ht = signAux3(f) hs$$$
Lean4
theorem signAux3_symm_trans_trans [Finite α] [DecidableEq β] [Finite β] (f : Perm α) (e : α ≃ β) {s : Multiset α}
{t : Multiset β} (hs : ∀ x, x ∈ s) (ht : ∀ x, x ∈ t) : signAux3 ((e.symm.trans f).trans e) ht = signAux3 f hs :=
by
induction t, s using Quotient.inductionOn₂
change signAux2 _ _ = signAux2 _ _
rcases Finite.exists_equiv_fin β with ⟨n, ⟨e'⟩⟩
rw [← signAux_eq_signAux2 _ _ e' fun _ _ => ht _, ← signAux_eq_signAux2 _ _ (e.trans e') fun _ _ => hs _]
exact congr_arg signAux (Equiv.ext fun x => by simp [symm_trans_apply])
