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

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).size = (a.swap j i hj hi).size

Tactic:
simp only [size_swap]

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).size
hi₂✝ : i✝ < (a.swap j i hj hi).size
⊢ (if i✝ = i then a[j] else if i✝ = j then a[i] else a[i✝]) = if i✝ = j then a[i] else if i✝ = i then a[j] else 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).size
hi₂✝ : i✝ < (a.swap j i hj hi).size
h✝ : i✝ = i
⊢ a[j] = if i✝ = j then a[i] else a[j]

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).size
hi₂✝ : i✝ < (a.swap j i hj hi).size
h✝ : ¬i✝ = i
⊢ (if i✝ = j then a[i] else a[i✝]) = if i✝ = j then a[i] else a[i✝]

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).size
hi₂✝ : i✝ < (a.swap j i hj hi).size
h✝ : i✝ = i
⊢ a[j] = if i✝ = j then a[i] else a[j]

Tactic:
split <;> 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).size
hi₂✝ : i✝ < (a.swap j i hj hi).size
⊢ (a.swap i j hi hj)[i✝] = (a.swap j i hj hi)[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).size
hi₂✝ : i✝ < (a.swap j i hj hi).size
⊢ (if i✝ = i then a[j] else if i✝ = j then a[i] else a[i✝]) = if i✝ = j then a[i] else if i✝ = i then a[j] else 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).size) (hi₂ : i_1 < (a.swap j i hj hi).size),
    (a.swap i j hi hj)[i_1] = (a.swap j i hj hi)[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).size
hi₂✝ : i✝ < (a.swap j i hj hi).size
⊢ (a.swap i j hi hj)[i✝] = (a.swap j i hj hi)[i✝]

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

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).size = (a.swap j i hj hi).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).size) (hi₂ : i_1 < (a.swap j i hj hi).size),
    (a.swap i j hi hj)[i_1] = (a.swap j i hj hi)[i_1]

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).size
hi₂✝ : i✝ < (a.swap j i hj hi).size
h✝ : ¬i✝ = i
⊢ (if i✝ = j then a[i] else a[i✝]) = if i✝ = j then a[i] else a[i✝]

Tactic:
split <;> simp_all

Result:
no goals