English
If l1 is a permutation of l2, then powersetCardAux(n, l1) is a permutation of powersetCardAux(n, l2).
Русский
Если l1 является перестановкой l2, то powersetCardAux(n, l1) является перестановкой powersetCardAux(n, l2).
LaTeX
$$l1.Perm l2 → (powersetCardAux n l1).Perm (powersetCardAux n l2)$$
Lean4
theorem powersetCardAux_perm {n} {l₁ l₂ : List α} (p : l₁ ~ l₂) : powersetCardAux n l₁ ~ powersetCardAux n l₂ :=
by
induction n generalizing l₁ l₂ with
| zero => simp
| succ n IHn => ?_
induction p with
| nil => rfl
| cons _ p IH =>
simp only [powersetCardAux_cons]
exact IH.append ((IHn p).map _)
| swap a b =>
simp only [powersetCardAux_cons, append_assoc]
apply Perm.append_left
cases n
· simp [Perm.swap]
simp only [powersetCardAux_cons, map_append, List.map_map]
rw [← append_assoc, ← append_assoc, (by funext s; simp [cons_swap] : cons b ∘ cons a = cons a ∘ cons b)]
exact perm_append_comm.append_right _
| trans _ _ IH₁ IH₂ => exact IH₁.trans IH₂
