-- 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
⊢ 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:
apply Perm.append_left

Result:
case a
α : 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[i + j] :: drop (i + 1) (take (i + j) as) ++ as[i] :: drop (i + j + 1) 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).length ≤ i

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 ≤ i

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) ++ as[i + j] :: drop (i + j + 1) as).set i as[i + j]).set
      (i + j) as[i] ~
    as

Tactic:
conv => rhs; 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] ~
    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) ++ as[i + j] :: drop (i + j + 1) as).set i as[i + j]).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_left _ _ (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) 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 0 as[i + j] ++
      (as[i + j] :: drop (i + j + 1) as).set 0 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 [set_cons_zero]

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
this : as = take i as ++ as[i] :: drop (i + 1) (take (i + j) as) ++ as[i + j] :: drop (i + j + 1) as
⊢ i + j - (min i as.length + (min (i + j) as.length - (i + 1) + 1)) = 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 - 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

Tactic:
rw [(show i - min i as.length = 0 by 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 0 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
⊢ as = take i as ++ as[i] :: (drop (i + 1) (take (i + j) as) ++ drop (i + j) as)

Tactic:
rw [← drop_append_of_le_length]

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)

α : 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

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 < (take i as ++ as[i] :: drop (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
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)

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 ≤ i

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 0 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

Tactic:
rw [(show i + j - (min i as.length + (min (i + j) as.length - (i + 1) + 1)) = 0 by 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 0 as[i + j] ++
      (as[i + j] :: drop (i + j + 1) as).set 0 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
⊢ as = take i as ++ as[i] :: drop (i + 1) (take (i + j) as ++ drop (i + j) as)

Tactic:
simp

Result:
no goals