-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem swap_swap (a : Array α) {i j : Nat} (hi hj) :
    (a.swap i j hi hj).swap i j ((a.size_swap ..).symm ▸ hi) ((a.size_swap ..).symm ▸ hj) = a

Proof state:
case h₁
α : Type u_1
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
⊢ ((a.swap i j hi hj).swap i j ⋯ ⋯).size = a.size

Tactic:
simp only [size_swap]

Result:
no goals

Proof state:
α : Type u_1
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
⊢ (a.swap i j hi hj).swap i j ⋯ ⋯ = a

Tactic:
apply ext

Result:
case h₁
α : Type u_1
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
⊢ ((a.swap i j hi hj).swap i j ⋯ ⋯).size = a.size

case h₂
α : Type u_1
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
⊢ ∀ (i_1 : Nat) (hi₁ : i_1 < ((a.swap i j hi hj).swap i j ⋯ ⋯).size) (hi₂ : i_1 < a.size),
    ((a.swap i j hi hj).swap i j ⋯ ⋯)[i_1] = a[i_1]

Proof state:
case h₂.isTrue
α : Type u_1
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
i✝ : Nat
hi₁✝ : i✝ < ((a.swap i j hi hj).swap i j ⋯ ⋯).size
hi₂✝ : i✝ < a.size
h✝ : i✝ = i
⊢ (if j = i then a[j] else if True then a[i] else a[j]) = a[i✝]

Tactic:
simp_all

Result:
no goals

Proof state:
case h₂
α : Type u_1
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
i✝ : Nat
hi₁✝ : i✝ < ((a.swap i j hi hj).swap i j ⋯ ⋯).size
hi₂✝ : i✝ < a.size
⊢ (if i✝ = i then if j = i then a[j] else if True then a[i] else a[j]
    else
      if i✝ = j then if True then a[j] else if i = j then a[i] else a[i]
      else if i✝ = i then a[j] else if i✝ = j then a[i] else a[i✝]) =
    a[i✝]

Tactic:
split

Result:
case h₂.isTrue
α : Type u_1
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
i✝ : Nat
hi₁✝ : i✝ < ((a.swap i j hi hj).swap i j ⋯ ⋯).size
hi₂✝ : i✝ < a.size
h✝ : i✝ = i
⊢ (if j = i then a[j] else if True then a[i] else a[j]) = a[i✝]

case h₂.isFalse
α : Type u_1
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
i✝ : Nat
hi₁✝ : i✝ < ((a.swap i j hi hj).swap i j ⋯ ⋯).size
hi₂✝ : i✝ < a.size
h✝ : ¬i✝ = i
⊢ (if i✝ = j then if True then a[j] else if i = j then a[i] else a[i] else if i✝ = j then a[i] else a[i✝]) = a[i✝]

Proof state:
case h₂
α : Type u_1
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
i✝ : Nat
hi₁✝ : i✝ < ((a.swap i j hi hj).swap i j ⋯ ⋯).size
hi₂✝ : i✝ < a.size
⊢ ((a.swap i j hi hj).swap i j ⋯ ⋯)[i✝] = a[i✝]

Tactic:
simp only [getElem_swap]

Result:
case h₂
α : Type u_1
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
i✝ : Nat
hi₁✝ : i✝ < ((a.swap i j hi hj).swap i j ⋯ ⋯).size
hi₂✝ : i✝ < a.size
⊢ (if i✝ = i then if j = i then a[j] else if True then a[i] else a[j]
    else
      if i✝ = j then if True then a[j] else if i = j then a[i] else a[i]
      else if i✝ = i then a[j] else if i✝ = j then a[i] else a[i✝]) =
    a[i✝]

Proof state:
case h₂
α : Type u_1
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
⊢ ∀ (i_1 : Nat) (hi₁ : i_1 < ((a.swap i j hi hj).swap i j ⋯ ⋯).size) (hi₂ : i_1 < a.size),
    ((a.swap i j hi hj).swap i j ⋯ ⋯)[i_1] = a[i_1]

Tactic:
intros

Result:
case h₂
α : Type u_1
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
i✝ : Nat
hi₁✝ : i✝ < ((a.swap i j hi hj).swap i j ⋯ ⋯).size
hi₂✝ : i✝ < a.size
⊢ ((a.swap i j hi hj).swap i j ⋯ ⋯)[i✝] = a[i✝]

Proof state:
case h₂.isFalse
α : Type u_1
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
i✝ : Nat
hi₁✝ : i✝ < ((a.swap i j hi hj).swap i j ⋯ ⋯).size
hi₂✝ : i✝ < a.size
h✝ : ¬i✝ = i
⊢ (if i✝ = j then if True then a[j] else if i = j then a[i] else a[i] else if i✝ = j then a[i] else a[i✝]) = a[i✝]

Tactic:
split <;> simp_all

Result:
no goals