English
Map after applying g and g' to the appropriate components preserves the snd part of permutationsAux2.
Русский
Применение функций g и g' к компонентам permutationsAux2 сохраняет вторую компоненту (snd).
LaTeX
$$$\forall {\alpha,\beta,\alpha',\beta'} (g:\alpha \to \alpha') (g' : \beta \to \beta') (t: \alpha) (ts ys : List\;\alpha) (r : List\beta) (f : List\alpha \to \beta) (f' : List\alpha' \to \beta'),\; (\forall a, g'(f a) = f'(List.map g a)) \\Rightarrow \, List.map g' (List.permutationsAux2 t ts r ys f).2 = (List.permutationsAux2 (g t) (List.map g ts) (List.map g' r) (List.map g ys) f').2$$$
Lean4
theorem map_permutationsAux2' {α' β'} (g : α → α') (g' : β → β') (t : α) (ts ys : List α) (r : List β) (f : List α → β)
(f' : List α' → β') (H : ∀ a, g' (f a) = f' (map g a)) :
map g' (permutationsAux2 t ts r ys f).2 = (permutationsAux2 (g t) (map g ts) (map g' r) (map g ys) f').2 := by
induction ys generalizing f f' with
| nil => simp
| cons ys_hd _ ys_ih =>
simp only [map, permutationsAux2_snd_cons, cons_append, cons.injEq]
rw [ys_ih]
· refine ⟨?_, rfl⟩
simp only [← map_cons, ← map_append]; apply H
· intro a; apply H
