-- 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₂ : j < as.length) :
    (as.set i as[j]).set j as[i] ~ as

Proof state:
α : 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] ~ as

Tactic:
if h₃ : i = j then
  simp [h₃]
else
  if h₃ : i < j then
    let j' := j - i
    have t : j = i + j' := by omega
    generalize j' = j' at t
    subst t
    exact set_set_perm' _ _ (by omega)
  else
    rw [set_comm _ _ _ (by omega)]
    let i' := i - j
    have t : i = j + i' := by omega
    generalize i' = i' at t
    subst t
    apply set_set_perm' _ _ (by omega)

Result:
no goals

Proof state:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : j < as.length
h₃ : ¬i = j
⊢ (as.set i as[j]).set j as[i] ~ as

Tactic:
if h₃ : i < j then
  let j' := j - i
  have t : j = i + j' := by omega
  generalize j' = j' at t
  subst t
  exact set_set_perm' _ _ (by omega)
else
  rw [set_comm _ _ _ (by omega)]
  let i' := i - j
  have t : i = j + i' := by omega
  generalize i' = i' at t
  subst t
  apply set_set_perm' _ _ (by omega)

Result:
no goals

Proof state:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : j < as.length
h₃✝ : ¬i = j
h₃ : ¬i < j
i'✝ : Nat := i - j
i' : Nat
t : i = j + i'
⊢ (as.set j as[i]).set i as[j] ~ as

Tactic:
subst t

Result:
α : Type u_1
as : List α
j : Nat
h₂ : j < as.length
i'✝ : Nat
h₁ : j + i'✝ < as.length
h₃✝ : ¬j + i'✝ = j
h₃ : ¬j + i'✝ < j
i' : Nat := j + i'✝ - j
⊢ (as.set j as[j + i'✝]).set (j + i'✝) as[j] ~ as

Proof state:
α : Type u_1
as : List α
i : Nat
h₁ : i < as.length
j'✝ : Nat
h₂ : i + j'✝ < as.length
h₃✝ : ¬i = i + j'✝
h₃ : i < i + j'✝
j' : Nat := i + j'✝ - i
⊢ (as.set i as[i + j'✝]).set (i + j'✝) as[i] ~ as

Tactic:
exact set_set_perm' _ _ (by omega)

Result:
no goals

Proof state:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : j < as.length
h₃✝ : ¬i = j
h₃ : ¬i < j
⊢ i ≠ j

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : j < as.length
h₃✝ : ¬i = j
h₃ : i < j
j' : Nat := j - i
⊢ j = i + j'

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
as : List α
j : Nat
h₂ : j < as.length
i'✝ : Nat
h₁ : j + i'✝ < as.length
h₃✝ : ¬j + i'✝ = j
h₃ : ¬j + i'✝ < j
i' : Nat := j + i'✝ - j
⊢ (as.set j as[j + i'✝]).set (j + i'✝) as[j] ~ as

Tactic:
apply set_set_perm' _ _ (by omega)

Result:
no goals

Proof state:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : j < as.length
h₃✝ : ¬i = j
h₃ : i < j
j' : Nat := j - i
⊢ (as.set i as[j]).set j as[i] ~ as

Tactic:
have t : j = i + j' := by omega

Result:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : j < as.length
h₃✝ : ¬i = j
h₃ : i < j
j' : Nat := j - i
t : j = i + j'
⊢ (as.set i as[j]).set j as[i] ~ as

Proof state:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : j < as.length
h₃✝ : ¬i = j
h₃ : ¬i < j
i' : Nat := i - j
t : i = j + i'
⊢ (as.set j as[i]).set i as[j] ~ as

Tactic:
generalize i' = i' at t

Result:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : j < as.length
h₃✝ : ¬i = j
h₃ : ¬i < j
i'✝ : Nat := i - j
i' : Nat
t : i = j + i'
⊢ (as.set j as[i]).set i as[j] ~ as

Proof state:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : j < as.length
h₃✝ : ¬i = j
h₃ : ¬i < j
⊢ (as.set i as[j]).set j as[i] ~ as

Tactic:
rw [set_comm _ _ _ (by omega)]

Result:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : j < as.length
h₃✝ : ¬i = j
h₃ : ¬i < j
⊢ (as.set j as[i]).set i as[j] ~ as

Proof state:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : j < as.length
h₃✝ : ¬i = j
h₃ : i < j
j' : Nat := j - i
t : j = i + j'
⊢ (as.set i as[j]).set j as[i] ~ as

Tactic:
generalize j' = j' at t

Result:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : j < as.length
h₃✝ : ¬i = j
h₃ : i < j
j'✝ : Nat := j - i
j' : Nat
t : j = i + j'
⊢ (as.set i as[j]).set j as[i] ~ as

Proof state:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : j < as.length
h₃✝ : ¬i = j
h₃ : ¬i < j
⊢ (as.set j as[i]).set i as[j] ~ as

Tactic:
let i' := i - j

Result:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : j < as.length
h₃✝ : ¬i = j
h₃ : ¬i < j
i' : Nat := i - j
⊢ (as.set j as[i]).set i as[j] ~ as

Proof state:
α : Type u_1
as : List α
i : Nat
h₁ : i < as.length
j'✝ : Nat
h₂ : i + j'✝ < as.length
h₃✝ : ¬i = i + j'✝
h₃ : i < i + j'✝
j' : Nat := i + j'✝ - i
⊢ 0 < j'✝

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : j < as.length
h₃✝ : ¬i = j
h₃ : i < j
j'✝ : Nat := j - i
j' : Nat
t : j = i + j'
⊢ (as.set i as[j]).set j as[i] ~ as

Tactic:
subst t

Result:
α : Type u_1
as : List α
i : Nat
h₁ : i < as.length
j'✝ : Nat
h₂ : i + j'✝ < as.length
h₃✝ : ¬i = i + j'✝
h₃ : i < i + j'✝
j' : Nat := i + j'✝ - i
⊢ (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₂ : j < as.length
h₃✝ : ¬i = j
h₃ : i < j
⊢ (as.set i as[j]).set j as[i] ~ as

Tactic:
let j' := j - i

Result:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : j < as.length
h₃✝ : ¬i = j
h₃ : i < j
j' : Nat := j - i
⊢ (as.set i as[j]).set j as[i] ~ as

Proof state:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : j < as.length
h₃✝ : ¬i = j
h₃ : ¬i < j
i' : Nat := i - j
⊢ (as.set j as[i]).set i as[j] ~ as

Tactic:
have t : i = j + i' := by omega

Result:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : j < as.length
h₃✝ : ¬i = j
h₃ : ¬i < j
i' : Nat := i - j
t : i = j + i'
⊢ (as.set j as[i]).set i as[j] ~ as

Proof state:
α : Type u_1
as : List α
j : Nat
h₂ : j < as.length
i'✝ : Nat
h₁ : j + i'✝ < as.length
h₃✝ : ¬j + i'✝ = j
h₃ : ¬j + i'✝ < j
i' : Nat := j + i'✝ - j
⊢ 0 < i'✝

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : j < as.length
h₃✝ : ¬i = j
h₃ : ¬i < j
i' : Nat := i - j
⊢ i = j + i'

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
as : List α
i j : Nat
h₁ : i < as.length
h₂ : j < as.length
h₃ : i = j
⊢ (as.set i as[j]).set j as[i] ~ as

Tactic:
simp [h₃]

Result:
no goals