-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toList_reverse (a : Array α) : a.reverse.toList = a.toList.reverse

Proof state:
case isTrue.H.isFalse
α : Type u_1
a as : Array α
i j✝ : Nat
h₂✝ : as.size = a.size
k✝ j : Nat
hj : j + 1 < as.size
h : i + (j + 1) + 1 = a.size
H : ∀ (k : Nat), as.toList[k]? = if i ≤ k ∧ k ≤ j + 1 then a.toList[k]? else a.toList.reverse[k]?
h₁ : i < j + 1
k : Nat
h₂ : ¬j + 1 = k
⊢ (if i = k then if True ∧ j + 1 ≤ j + 1 then a.toList[j + 1]? else a.toList.reverse[j + 1]?
    else if i ≤ k ∧ k ≤ j + 1 then a.toList[k]? else a.toList.reverse[k]?) =
    if i + 1 ≤ k ∧ k ≤ j then a.toList[k]? else a.toList.reverse[k]?

Tactic:
split <;> rename_i h₃

Result:
case isTrue.H.isFalse.isTrue
α : Type u_1
a as : Array α
i j✝ : Nat
h₂✝ : as.size = a.size
k✝ j : Nat
hj : j + 1 < as.size
h : i + (j + 1) + 1 = a.size
H : ∀ (k : Nat), as.toList[k]? = if i ≤ k ∧ k ≤ j + 1 then a.toList[k]? else a.toList.reverse[k]?
h₁ : i < j + 1
k : Nat
h₂ : ¬j + 1 = k
h₃ : i = k
⊢ (if True ∧ j + 1 ≤ j + 1 then a.toList[j + 1]? else a.toList.reverse[j + 1]?) =
    if i + 1 ≤ k ∧ k ≤ j then a.toList[k]? else a.toList.reverse[k]?

case isTrue.H.isFalse.isFalse
α : Type u_1
a as : Array α
i j✝ : Nat
h₂✝ : as.size = a.size
k✝ j : Nat
hj : j + 1 < as.size
h : i + (j + 1) + 1 = a.size
H : ∀ (k : Nat), as.toList[k]? = if i ≤ k ∧ k ≤ j + 1 then a.toList[k]? else a.toList.reverse[k]?
h₁ : i < j + 1
k : Nat
h₂ : ¬j + 1 = k
h₃ : ¬i = k
⊢ (if i ≤ k ∧ k ≤ j + 1 then a.toList[k]? else a.toList.reverse[k]?) =
    if i + 1 ≤ k ∧ k ≤ j then a.toList[k]? else a.toList.reverse[k]?

Proof state:
case isFalse
α : Type u_1
a : Array α
h✝ : ¬a.size ≤ 1
this : a.size - 1 + 1 = a.size
⊢ (reverse.loop a 0 ⟨a.size - 1, ⋯⟩).toList = a.toList.reverse

Tactic:
refine List.ext_getElem? <| go _ _ _ _ (by simp [this]) rfl fun k => ?_

Result:
case isFalse
α : Type u_1
a : Array α
h✝ : ¬a.size ≤ 1
this : a.size - 1 + 1 = a.size
k : Nat
⊢ a.toList[k]? = if 0 ≤ k ∧ k ≤ a.size - 1 then a.toList[k]? else a.toList.reverse[k]?

Proof state:
case isTrue.H.isFalse.isTrue
α : Type u_1
a as : Array α
i j✝ : Nat
h₂✝ : as.size = a.size
k✝ j : Nat
hj : j + 1 < as.size
h : i + (j + 1) + 1 = a.size
H : ∀ (k : Nat), as.toList[k]? = if i ≤ k ∧ k ≤ j + 1 then a.toList[k]? else a.toList.reverse[k]?
h₁ : i < j + 1
k : Nat
h₂ : ¬j + 1 = k
h₃ : i = k
⊢ (if True ∧ True then a.toList[j + 1]? else a.toList.reverse[j + 1]?) =
    if False then a.toList[i]? else a.toList.reverse[i]?

Tactic:
exact (List.getElem?_reverse' i (j+1) (Eq.trans (by simp_arith) h)).symm

Result:
no goals

Proof state:
case isTrue.H.isFalse.isFalse
α : Type u_1
a as : Array α
i j✝ : Nat
h₂✝ : as.size = a.size
k✝ j : Nat
hj : j + 1 < as.size
h : i + (j + 1) + 1 = a.size
H : ∀ (k : Nat), as.toList[k]? = if i ≤ k ∧ k ≤ j + 1 then a.toList[k]? else a.toList.reverse[k]?
h₁ : i < j + 1
k : Nat
h₂ : ¬j + 1 = k
h₃ : ¬i = k
⊢ (if i ≤ k ∧ k ≤ j + 1 then a.toList[k]? else a.toList.reverse[k]?) =
    if i + 1 ≤ k ∧ k ≤ j then a.toList[k]? else a.toList.reverse[k]?

Tactic:
simp only [Nat.succ_le, Nat.lt_iff_le_and_ne.trans (and_iff_left h₃),
  Nat.lt_succ.symm.trans (Nat.lt_iff_le_and_ne.trans (and_iff_left (Ne.symm h₂)))]

Result:
no goals

Proof state:
case isFalse
α : Type u_1
a : Array α
h✝ : ¬a.size ≤ 1
⊢ (reverse.loop a 0 ⟨a.size - 1, ⋯⟩).toList = a.toList.reverse

Tactic:
have := Nat.sub_add_cancel (Nat.le_of_not_le ‹_›)

Result:
case isFalse
α : Type u_1
a : Array α
h✝ : ¬a.size ≤ 1
this : a.size - 1 + 1 = a.size
⊢ (reverse.loop a 0 ⟨a.size - 1, ⋯⟩).toList = a.toList.reverse

Proof state:
case isTrue
α : Type u_1
a : Array α
h✝ : a.size ≤ 1
⊢ a.toList = a.toList.reverse

Tactic:
match a with | ⟨[]⟩ | ⟨[_]⟩ => rfl

Result:
no goals

Proof state:
case isTrue.H
α : Type u_1
a as : Array α
i j✝ : Nat
h₂ : as.size = a.size
k✝ j : Nat
hj : j + 1 < as.size
h : i + (j + 1) + 1 = a.size
H : ∀ (k : Nat), as.toList[k]? = if i ≤ k ∧ k ≤ j + 1 then a.toList[k]? else a.toList.reverse[k]?
h₁ : i < j + 1
k : Nat
⊢ (as.swap i (j + 1) ⋯ ⋯).toList[k]? = if i + 1 ≤ k ∧ k ≤ j then a.toList[k]? else a.toList.reverse[k]?

Tactic:
rw [getElem?_toList, getElem?_swap]

Result:
case isTrue.H
α : Type u_1
a as : Array α
i j✝ : Nat
h₂ : as.size = a.size
k✝ j : Nat
hj : j + 1 < as.size
h : i + (j + 1) + 1 = a.size
H : ∀ (k : Nat), as.toList[k]? = if i ≤ k ∧ k ≤ j + 1 then a.toList[k]? else a.toList.reverse[k]?
h₁ : i < j + 1
k : Nat
⊢ (if j + 1 = k then some as[i] else if i = k then some as[j + 1] else as[k]?) =
    if i + 1 ≤ k ∧ k ≤ j then a.toList[k]? else a.toList.reverse[k]?

Proof state:
case isTrue.H
α : Type u_1
a as : Array α
i j✝ : Nat
h₂ : as.size = a.size
k✝ j : Nat
hj : j + 1 < as.size
h : i + (j + 1) + 1 = a.size
H : ∀ (k : Nat), as.toList[k]? = if i ≤ k ∧ k ≤ j + 1 then a.toList[k]? else a.toList.reverse[k]?
h₁ : i < j + 1
k : Nat
⊢ (if j + 1 = k then some as[i] else if i = k then some as[j + 1] else as[k]?) =
    if i + 1 ≤ k ∧ k ≤ j then a.toList[k]? else a.toList.reverse[k]?

Tactic:
simp only [H, ← getElem_toList, ← List.getElem?_eq_getElem, Nat.le_of_lt h₁,
  ← getElem?_toList]

Result:
case isTrue.H
α : Type u_1
a as : Array α
i j✝ : Nat
h₂ : as.size = a.size
k✝ j : Nat
hj : j + 1 < as.size
h : i + (j + 1) + 1 = a.size
H : ∀ (k : Nat), as.toList[k]? = if i ≤ k ∧ k ≤ j + 1 then a.toList[k]? else a.toList.reverse[k]?
h₁ : i < j + 1
k : Nat
⊢ (if j + 1 = k then if i ≤ i ∧ True then a.toList[i]? else a.toList.reverse[i]?
    else
      if i = k then if True ∧ j + 1 ≤ j + 1 then a.toList[j + 1]? else a.toList.reverse[j + 1]?
      else if i ≤ k ∧ k ≤ j + 1 then a.toList[k]? else a.toList.reverse[k]?) =
    if i + 1 ≤ k ∧ k ≤ j then a.toList[k]? else a.toList.reverse[k]?

Proof state:
case isTrue
α : Type u_1
a as : Array α
i j✝ : Nat
h₂ : as.size = a.size
k j : Nat
hj : j + 1 < as.size
h : i + (j + 1) + 1 = a.size
H : ∀ (k : Nat), as.toList[k]? = if i ≤ k ∧ k ≤ j + 1 then a.toList[k]? else a.toList.reverse[k]?
h₁ : i < j + 1
⊢ (reverse.loop (as.swap i (j + 1) ⋯ ⋯) (i + 1) ⟨j + 1 - 1, ⋯⟩).toList[k]? = a.toList.reverse[k]?

Tactic:
simp only [Nat.add_sub_cancel]

Result:
case isTrue
α : Type u_1
a as : Array α
i j✝ : Nat
h₂ : as.size = a.size
k j : Nat
hj : j + 1 < as.size
h : i + (j + 1) + 1 = a.size
H : ∀ (k : Nat), as.toList[k]? = if i ≤ k ∧ k ≤ j + 1 then a.toList[k]? else a.toList.reverse[k]?
h₁ : i < j + 1
⊢ (reverse.loop (as.swap i (j + 1) ⋯ ⋯) (i + 1) ⟨j, ⋯⟩).toList[k]? = a.toList.reverse[k]?

Proof state:
case isTrue
α : Type u_1
a as : Array α
i j : Nat
hj : j < as.size
h : i + j + 1 = a.size
h₂ : as.size = a.size
H : ∀ (k : Nat), as.toList[k]? = if i ≤ k ∧ k ≤ j then a.toList[k]? else a.toList.reverse[k]?
k : Nat
h₁ : i < j
⊢ (reverse.loop (as.swap i j ⋯ ⋯) (i + 1) ⟨j - 1, ⋯⟩).toList[k]? = a.toList.reverse[k]?

Tactic:
match j with | j+1 => ?_

Result:
case isTrue
α : Type u_1
a as : Array α
i j✝ : Nat
h₂ : as.size = a.size
k j : Nat
hj : j + 1 < as.size
h : i + (j + 1) + 1 = a.size
H : ∀ (k : Nat), as.toList[k]? = if i ≤ k ∧ k ≤ j + 1 then a.toList[k]? else a.toList.reverse[k]?
h₁ : i < j + 1
⊢ (reverse.loop (as.swap i (j + 1) ⋯ ⋯) (i + 1) ⟨j + 1 - 1, ⋯⟩).toList[k]? = a.toList.reverse[k]?

Proof state:
α : Type u_1
a as : Array α
i j✝ : Nat
h₂✝ : as.size = a.size
k✝ j : Nat
hj : j + 1 < as.size
h : i + (j + 1) + 1 = a.size
H : ∀ (k : Nat), as.toList[k]? = if i ≤ k ∧ k ≤ j + 1 then a.toList[k]? else a.toList.reverse[k]?
h₁ : i < j + 1
k : Nat
h₂ : j + 1 = k
⊢ j + 1 + i + 1 = i + (j + 1) + 1

Tactic:
simp_arith

Result:
no goals

Proof state:
case isTrue.h₂
α : Type u_1
a as : Array α
i j✝ : Nat
h₂ : as.size = a.size
k j : Nat
hj : j + 1 < as.size
h : i + (j + 1) + 1 = a.size
H : ∀ (k : Nat), as.toList[k]? = if i ≤ k ∧ k ≤ j + 1 then a.toList[k]? else a.toList.reverse[k]?
h₁ : i < j + 1
⊢ (as.swap i (j + 1) ⋯ ⋯).size = a.size

Tactic:
simp [size_swap, h₂]

Result:
no goals