English
If l1 is permuted to l2 by a permutation p, then applying lookmap f to both lists yields another permutation: lookmap f l1 ~ lookmap f l2, provided H encodes the appropriate compatibility between f values on corresponding elements.
Русский
Если l1 приводится к l2 перестановкой p, то применение lookmap f к обоим спискам дает другую перестановку: lookmap f l1 ~ lookmap f l2, при условии совместимости f на соответствующих элементах, зафиксированном в H.
LaTeX
$$$H:\\mathrm{Pairwise}\\ (\\lambda a\\, b\\, \\forall c\\in f(a),\\forall d\\in f(b),\, a=b\\wedge c=d)\\ l_1\\ \\Rightarrow\\ l_1\\sim l_2\\ \\Rightarrow\\ \\operatorname{lookmap} f\\ l_1 \\sim \\operatorname{lookmap} f\\ l_2$$$
Lean4
theorem perm_lookmap (f : α → Option α) {l₁ l₂ : List α}
(H : Pairwise (fun a b => ∀ c ∈ f a, ∀ d ∈ f b, a = b ∧ c = d) l₁) (p : l₁ ~ l₂) : lookmap f l₁ ~ lookmap f l₂ := by
induction p with
| nil => simp
| cons a p IH =>
cases h : f a
· simpa [h] using IH (pairwise_cons.1 H).2
· simp [lookmap_cons_some _ _ h, p]
| swap a b l =>
rcases h₁ : f a with - | c <;> rcases h₂ : f b with - | d
· simpa [h₁, h₂] using swap _ _ _
· simpa [h₁, lookmap_cons_some _ _ h₂] using swap _ _ _
· simpa [lookmap_cons_some _ _ h₁, h₂] using swap _ _ _
· rcases (pairwise_cons.1 H).1 _ (mem_cons.2 (Or.inl rfl)) _ h₂ _ h₁ with ⟨rfl, rfl⟩
exact Perm.refl _
| trans p₁ _ IH₁ IH₂ =>
refine (IH₁ H).trans (IH₂ ((p₁.pairwise_iff ?_).1 H))
grind
