theorem List.set_set_perm {α : Type u_1} {as : List α} {i j : Nat} (h₁ : i < as.length) (h₂ : j < as.length) : ((as.set i as[j]).set j as[i]).Perm as

theorem List.Perm.take_of_getElem? {α : Type u_1} {l₁ l₂ : List α} (h : l₁.Perm l₂) {i : Nat} (w : ∀ (j : Nat), i ≤ j → l₁[j]? = l₂[j]?) : (List.take i l₁).Perm (List.take i l₂)

Variant of List.Perm.take specifying the the permutation is constant after i elementwise.

theorem List.Perm.drop_of_getElem? {α : Type u_1} {l₁ l₂ : List α} (h : l₁.Perm l₂) {i : Nat} (w : ∀ (j : Nat), j < i → l₁[j]? = l₂[j]?) : (List.drop i l₁).Perm (List.drop i l₂)

Variant of List.Perm.drop specifying the the permutation is constant before i elementwise.