English
For any l1,l2 and n,a, (l1.insertIdx n a) ~ (l2.insertIdx n a) iff l1 ~ l2.
Русский
Для любых l1, l2 и n,a, (l1.insertIdx n a) ~ (l2.insertIdx n a) эквивалентно l1 ~ l2.
LaTeX
$$$\\forall {l_1 l_2} {n} {a}, (l_1.insertIdx n a) \\sim (l_2.insertIdx n a) \\iff l_1 \\sim l_2.$$$
Lean4
@[simp]
theorem perm_insertIdx_iff {l₁ l₂ : List α} {n : ℕ} {a : α} : l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂ :=
by
wlog hle : length l₁ ≤ length l₂ generalizing l₁ l₂
· rw [perm_comm, this (le_of_not_ge hle), perm_comm]
cases Nat.lt_or_ge (length l₁) n with
| inl hn₁ =>
rw [insertIdx_of_length_lt hn₁]
cases Nat.lt_or_ge (length l₂) n with
| inl hn₂ => rw [insertIdx_of_length_lt hn₂]
| inr hn₂ =>
apply iff_of_false
· intro h
rw [h.length_eq] at hn₁
exact (hn₁.trans_le hn₂).not_ge (length_le_length_insertIdx ..)
· exact fun h ↦ (hn₁.trans_le hn₂).not_ge h.length_eq.ge
| inr hn₁ => exact perm_insertIdx_iff_of_le hn₁ (le_trans hn₁ hle) _
