English
If l ≃ u and u is related to v by Forall₂ r, then there exists some l' with l ≃ l' and l' is related to v by Forall₂ r.
Русский
Если списки l и u эквивалентны перестановкой и u связан с v отношением Forall₂ r, то найдётся l' такой, что l ≃ l' и l' связан с v отношением Forall₂ r.
LaTeX
$$$l \\sim u \\land \\mathrm{Forall}_2(r)\\,u\\,v \\Rightarrow \\exists l',\\ l \\sim l' \\land \\mathrm{Forall}_2(r)\\,l'\\,v$$$
Lean4
theorem perm_comp_forall₂ {l u v} (hlu : Perm l u) (huv : Forall₂ r u v) : (Forall₂ r ∘r Perm) l v := by
induction hlu generalizing v with
| nil => cases huv; exact ⟨[], Forall₂.nil, Perm.nil⟩
| cons u _hlu ih =>
obtain - | ⟨hab, huv'⟩ := huv
rcases ih huv' with ⟨l₂, h₁₂, h₂₃⟩
exact ⟨_ :: l₂, Forall₂.cons hab h₁₂, h₂₃.cons _⟩
| swap a₁ a₂ h₂₃ =>
obtain - | ⟨h₁, hr₂₃⟩ := huv
obtain - | ⟨h₂, h₁₂⟩ := hr₂₃
exact ⟨_, Forall₂.cons h₂ (Forall₂.cons h₁ h₁₂), Perm.swap _ _ _⟩
| trans _ _ ih₁ ih₂ =>
rcases ih₂ huv with ⟨lb₂, hab₂, h₂₃⟩
rcases ih₁ hab₂ with ⟨lb₁, hab₁, h₁₂⟩
exact ⟨lb₁, hab₁, Perm.trans h₁₂ h₂₃⟩
