-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Perm.lean
theorem set_set_perm' {as : List α} {i j : Nat} (h₁ : i < as.length) (h₂ : i + j < as.length)
    (hj : 0 < j) :
    (as.set i as[i + j]).set (i + j) as[i] ~ as

Proof state:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : i + j < as.length
hj : 0 < j
this : as = take i as ++ as[i] :: drop (i + 1) (take (i + j) as) ++ as[i + j] :: drop (i + j + 1) as
⊢ (as.set i as[i + j]).set (i + j) as[i] ~ as

Tactic:
conv => lhs; congr; congr; rw [this]

Result:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : i + j < as.length
hj : 0 < j
this : as = take i as ++ as[i] :: drop (i + 1) (take (i + j) as) ++ as[i + j] :: drop (i + j + 1) as
⊢ ((take i as ++ as[i] :: drop (i + 1) (take (i + j) as) ++ as[i + j] :: drop (i + j + 1) as).set i as[i + j]).set
      (i + j) as[i] ~
    as

Proof state:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : i + j < as.length
hj : 0 < j
this : as = take i as ++ as[i] :: drop (i + 1) (take (i + j) as) ++ as[i + j] :: drop (i + j + 1) as
⊢ ((take i as ++ as[i] :: drop (i + 1) (take (i + j) as)).set i as[i + j]).length ≤ i + j

Tactic:
simp

Result:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : i + j < as.length
hj : 0 < j
this : as = take i as ++ as[i] :: drop (i + 1) (take (i + j) as) ++ as[i + j] :: drop (i + j + 1) as
⊢ min i as.length + (min (i + j) as.length - (i + 1) + 1) ≤ i + j

Proof state:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : i + j < as.length
hj : 0 < j
this : as = take i as ++ as[i] :: drop (i + 1) (take (i + j) as) ++ as[i + j] :: drop (i + j + 1) as
⊢ i - min i as.length = 0

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : i + j < as.length
hj : 0 < j
this : as = take i as ++ as[i] :: drop (i + 1) (take (i + j) as) ++ as[i + j] :: drop (i + j + 1) as
⊢ ((take i as ++ as[i] :: drop (i + 1) (take (i + j) as)).set i as[i + j] ++ as[i + j] :: drop (i + j + 1) as).set
      (i + j) as[i] ~
    take i as ++ as[i] :: drop (i + 1) (take (i + j) as) ++ as[i + j] :: drop (i + j + 1) as

Tactic:
rw [set_append_right _ _ (by simp; omega)]

Result:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : i + j < as.length
hj : 0 < j
this : as = take i as ++ as[i] :: drop (i + 1) (take (i + j) as) ++ as[i + j] :: drop (i + j + 1) as
⊢ (take i as ++ as[i] :: drop (i + 1) (take (i + j) as)).set i as[i + j] ++
      (as[i + j] :: drop (i + j + 1) as).set
        (i + j - ((take i as ++ as[i] :: drop (i + 1) (take (i + j) as)).set i as[i + j]).length) as[i] ~
    take i as ++ as[i] :: drop (i + 1) (take (i + j) as) ++ as[i + j] :: drop (i + j + 1) as

Proof state:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : i + j < as.length
hj : 0 < j
this : as = take i as ++ as[i] :: drop (i + 1) (take (i + j) as) ++ as[i + j] :: drop (i + j + 1) as
⊢ take i as ++ as[i + j] :: drop (i + 1) (take (i + j) as) ++ as[i] :: drop (i + j + 1) as ~
    take i as ++ as[i] :: drop (i + 1) (take (i + j) as) ++ as[i + j] :: drop (i + j + 1) as

Tactic:
simp only [append_assoc]

Result:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : i + j < as.length
hj : 0 < j
this : as = take i as ++ as[i] :: drop (i + 1) (take (i + j) as) ++ as[i + j] :: drop (i + j + 1) as
⊢ take i as ++ (as[i + j] :: drop (i + 1) (take (i + j) as) ++ as[i] :: drop (i + j + 1) as) ~
    take i as ++ (as[i] :: drop (i + 1) (take (i + j) as) ++ as[i + j] :: drop (i + j + 1) as)

Proof state:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : i + j < as.length
hj : 0 < j
⊢ i + 1 ≤ (take (i + j) as).length

Tactic:
simp

Result:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : i + j < as.length
hj : 0 < j
⊢ i + 1 ≤ min (i + j) as.length

Proof state:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : i + j < as.length
hj : 0 < j
this : as = take i as ++ as[i] :: drop (i + 1) (take (i + j) as) ++ as[i + j] :: drop (i + j + 1) as
⊢ min i as.length + (min (i + j) as.length - (i + 1) + 1) ≤ i + j

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : i + j < as.length
hj : 0 < j
⊢ as = take i as ++ as[i] :: drop (i + 1) (take (i + j) as) ++ as[i + j] :: drop (i + j + 1) as

Tactic:
simp only [getElem_cons_drop, append_assoc, cons_append]

Result:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : i + j < as.length
hj : 0 < j
⊢ as = take i as ++ as[i] :: (drop (i + 1) (take (i + j) as) ++ drop (i + j) as)

Proof state:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : i + j < as.length
hj : 0 < j
this : as = take i as ++ as[i] :: drop (i + 1) (take (i + j) as) ++ as[i + j] :: drop (i + j + 1) as
⊢ i < min i as.length + (min (i + j) as.length - (i + 1) + 1)

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : i + j < as.length
hj : 0 < j
⊢ i + 1 ≤ min (i + j) as.length

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : i + j < as.length
hj : 0 < j
this : as = take i as ++ as[i] :: drop (i + 1) (take (i + j) as) ++ as[i + j] :: drop (i + j + 1) as
⊢ take i as ++ (as[i] :: drop (i + 1) (take (i + j) as)).set (i - (take i as).length) as[i + j] ++
      (as[i + j] :: drop (i + j + 1) as).set
        (i + j - (take i as ++ (as[i] :: drop (i + 1) (take (i + j) as)).set (i - (take i as).length) as[i + j]).length)
        as[i] ~
    take i as ++ as[i] :: drop (i + 1) (take (i + j) as) ++ as[i + j] :: drop (i + j + 1) as

Tactic:
simp only [length_append, length_take, length_set, length_cons, length_drop]

Result:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : i + j < as.length
hj : 0 < j
this : as = take i as ++ as[i] :: drop (i + 1) (take (i + j) as) ++ as[i + j] :: drop (i + j + 1) as
⊢ take i as ++ (as[i] :: drop (i + 1) (take (i + j) as)).set (i - min i as.length) as[i + j] ++
      (as[i + j] :: drop (i + j + 1) as).set (i + j - (min i as.length + (min (i + j) as.length - (i + 1) + 1))) as[i] ~
    take i as ++ as[i] :: drop (i + 1) (take (i + j) as) ++ as[i + j] :: drop (i + j + 1) as

Proof state:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : i + j < as.length
hj : 0 < j
this : as = take i as ++ as[i] :: drop (i + 1) (take (i + j) as) ++ as[i + j] :: drop (i + j + 1) as
⊢ (take i as ++ as[i] :: drop (i + 1) (take (i + j) as)).set i as[i + j] ++
      (as[i + j] :: drop (i + j + 1) as).set
        (i + j - ((take i as ++ as[i] :: drop (i + 1) (take (i + j) as)).set i as[i + j]).length) as[i] ~
    take i as ++ as[i] :: drop (i + 1) (take (i + j) as) ++ as[i + j] :: drop (i + j + 1) as

Tactic:
rw [set_append_right _ _ (by simp; omega)]

Result:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : i + j < as.length
hj : 0 < j
this : as = take i as ++ as[i] :: drop (i + 1) (take (i + j) as) ++ as[i + j] :: drop (i + j + 1) as
⊢ take i as ++ (as[i] :: drop (i + 1) (take (i + j) as)).set (i - (take i as).length) as[i + j] ++
      (as[i + j] :: drop (i + j + 1) as).set
        (i + j - (take i as ++ (as[i] :: drop (i + 1) (take (i + j) as)).set (i - (take i as).length) as[i + j]).length)
        as[i] ~
    take i as ++ as[i] :: drop (i + 1) (take (i + j) as) ++ as[i + j] :: drop (i + j + 1) as