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

Proof state:
α : 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
⊢ (if h : i < j then reverse.loop (as.swap i j ⋯ ⋯) (i + 1) ⟨j - 1, ⋯⟩ else as).toList[k]? = a.toList.reverse[k]?

Tactic:
split <;> rename_i h₁

Result:
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]?

case isFalse
α : 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
⊢ as.toList[k]? = a.toList.reverse[k]?

Proof state:
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]?

Tactic:
split

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

case isFalse.isFalse
α : Type u_1
a : Array α
h✝¹ : ¬a.size ≤ 1
this : a.size - 1 + 1 = a.size
k : Nat
h✝ : ¬(0 ≤ k ∧ k ≤ a.size - 1)
⊢ a.toList[k]? = 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
⊢ i + 1 + j + 1 = a.size

Tactic:
rwa [Nat.add_right_comm i]

Result:
no goals

Proof state:
case isFalse.isFalse
α : Type u_1
a : Array α
h✝¹ : ¬a.size ≤ 1
this : a.size - 1 + 1 = a.size
k : Nat
h✝ : ¬(0 ≤ k ∧ k ≤ a.size - 1)
⊢ a.toList[k]? = a.toList.reverse[k]?

Tactic:
rename_i h

Result:
case isFalse.isFalse
α : Type u_1
a : Array α
h✝ : ¬a.size ≤ 1
this : a.size - 1 + 1 = a.size
k : Nat
h : ¬(0 ≤ k ∧ k ≤ a.size - 1)
⊢ a.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
h₃ : i = k
⊢ i + (j + 1) + 1 = i + (j + 1) + 1

Tactic:
simp_arith

Result:
no goals

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

Tactic:
exact (List.getElem?_reverse' _ _ h).symm

Result:
no goals

Proof state:
case isTrue.H.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
⊢ (if True ∧ True then a.toList[i]? else a.toList.reverse[i]?) =
    if False then a.toList[j + 1]? else a.toList.reverse[j + 1]?

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

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:
intro k

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
⊢ (as.swap i (j + 1) ⋯ ⋯).toList[k]? = if i + 1 ≤ k ∧ k ≤ j then a.toList[k]? else a.toList.reverse[k]?

Proof state:
α : Type u_1
a : Array α
⊢ a.reverse.toList = a.toList.reverse

Tactic:
simp only [reverse]

Result:
α : Type u_1
a : Array α
⊢ (if h : a.size ≤ 1 then a else reverse.loop a 0 ⟨a.size - 1, ⋯⟩).toList = a.toList.reverse

Proof state:
α : Type u_1
a : Array α
h✝ : ¬a.size ≤ 1
this : a.size - 1 + 1 = a.size
⊢ 0 + (a.size - 1) + 1 = a.size

Tactic:
simp [this]

Result:
no goals

Proof state:
α : Type u_1
a : Array α
⊢ (if h : a.size ≤ 1 then a else reverse.loop a 0 ⟨a.size - 1, ⋯⟩).toList = a.toList.reverse

Tactic:
split

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

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

Proof state:
case isFalse.isFalse
α : 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
h₂ : ¬(i ≤ k ∧ k ≤ j)
⊢ a.toList.reverse[k]? = a.toList.reverse[k]?

Tactic:
rfl

Result:
no goals

Proof state:
case isFalse.isFalse
α : Type u_1
a : Array α
h✝ : ¬a.size ≤ 1
this : a.size - 1 + 1 = a.size
k : Nat
h : ¬(0 ≤ k ∧ k ≤ a.size - 1)
⊢ a.toList[k]? = a.toList.reverse[k]?

Tactic:
simp only [← show k < _ + 1 ↔ _ from Nat.lt_succ (n := a.size - 1), this, Nat.zero_le,
  true_and, Nat.not_lt] at h

Result:
case isFalse.isFalse
α : Type u_1
a : Array α
h✝ : ¬a.size ≤ 1
this : a.size - 1 + 1 = a.size
k : Nat
h : a.size ≤ k
⊢ a.toList[k]? = 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 ∧ 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]?

Tactic:
simp only [← h₃, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, false_and]

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 ∧ True then a.toList[j + 1]? else a.toList.reverse[j + 1]?) =
    if False then a.toList[i]? else a.toList.reverse[i]?

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

Tactic:
cases Nat.le_antisymm h₂.1 h₂.2

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

Proof state:
α : Type u_1
a : Array α
head✝ : α
h✝ : { toList := [head✝] }.size ≤ 1
⊢ { toList := [head✝] }.toList = { toList := [head✝] }.toList.reverse

Tactic:
rfl

Result:
no goals