trimming permutations?

Stream: Is there code for X?

[Kim Morrison]

Does anyone have code for:

namespace List

theorem take_perm {l₁ l₂ : List α} (h : l₁ ~ l₂) (n : Nat) (w : ∀ i, n ≤ i → l₁[i]? = l₂[i]?) :
    (l₁.take n) ~ (l₂.take n) := by
  sorry

theorem drop_perm {l₁ l₂ : List α} (h : l₁ ~ l₂) (n : Nat) (w : ∀ i, i < n → l₁[i]? = l₂[i]?) :
    (l₁.drop n) ~ (l₂.drop n) := by
  sorry

end List

?

[Kim Morrison]

Ah, a better question (and answer) is

theorem take_perm {l₁ l₂ : List α} (h : l₁ ~ l₂) {n : Nat} (w : l₁.drop n = l₂.drop n) :
    (l₁.take n) ~ (l₂.take n) := by
  rwa [← List.take_append_drop n l₁, ← List.take_append_drop n l₂, w, perm_append_right_iff] at h

theorem drop_perm {l₁ l₂ : List α} (h : l₁ ~ l₂) {n : Nat} (w : l₂.take n = l₁.take n) :
    (l₁.drop n) ~ (l₂.drop n) := by
  rwa [← List.take_append_drop n l₁, ← List.take_append_drop n l₂, w, perm_append_left_iff] at h

[Aaron Liu]

Here's something slightly more general, but I needed multisets to prove this version:

import Mathlib.Data.Multiset.AddSub

namespace List

theorem take_perm {l₁ l₂ : List α} (h : l₁ ~ l₂) {n : Nat} (w : l₁.drop n ~ l₂.drop n) :
    (l₁.take n) ~ (l₂.take n) := by
  rwa [← List.take_append_drop n l₁, ← List.take_append_drop n l₂, ← Multiset.coe_eq_coe,
    ← Multiset.coe_add, Multiset.coe_eq_coe.mpr w, Multiset.coe_add, Multiset.coe_eq_coe,
    perm_append_right_iff] at h

theorem drop_perm {l₁ l₂ : List α} (h : l₁ ~ l₂) {n : Nat} (w : l₁.take n ~ l₂.take n) :
    (l₁.drop n) ~ (l₂.drop n) := by
  rwa [← List.take_append_drop n l₁, ← List.take_append_drop n l₂, ← Multiset.coe_eq_coe,
    ← Multiset.coe_add, Multiset.coe_eq_coe.mpr w, Multiset.coe_add, Multiset.coe_eq_coe,
    perm_append_left_iff] at h

[Kim Morrison]

Ah, nice. Probably perm_iff_count can get there without multisets.

[Bhavik Mehta]

For completeness, here's the proof of the generalised version using only bits from core:

import Init.Data.List.Perm

namespace List

theorem take_perm {l₁ l₂ : List α} (h : l₁ ~ l₂) {n : Nat} (w : l₁.drop n ~ l₂.drop n) :
    (l₁.take n) ~ (l₂.take n) := by
  classical
  rw [perm_iff_count] at h w ⊢
  rw [← take_append_drop n l₁, ← take_append_drop n l₂] at h
  simpa only [count_append, w, Nat.add_right_cancel_iff] using h

theorem drop_perm {l₁ l₂ : List α} (h : l₁ ~ l₂) {n : Nat} (w : l₁.take n ~ l₂.take n) :
    (l₁.drop n) ~ (l₂.drop n) := by
  classical
  rw [perm_iff_count] at h w ⊢
  rw [← take_append_drop n l₁, ← take_append_drop n l₂] at h
  simpa only [count_append, w, Nat.add_left_cancel_iff] using h

[Kim Morrison]

Thanks: #7936