-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem eraseIdx_toArray (l : List α) (i : Nat) (h : i < l.toArray.size) :
    l.toArray.eraseIdx i h = (l.eraseIdx i).toArray

Proof state:
α : Type u_1
l : List α
i : Nat
h : i < l.toArray.size
⊢ (if h' : i + 1 < l.toArray.size then
      let a' := l.toArray.swap (i + 1) i h' h;
      a'.eraseIdx (i + 1) ⋯
    else l.toArray.pop) =
    (l.eraseIdx i).toArray

Tactic:
split <;> rename_i h'

Result:
case isTrue
α : Type u_1
l : List α
i : Nat
h : i < l.toArray.size
h' : i + 1 < l.toArray.size
⊢ (let a' := l.toArray.swap (i + 1) i h' h;
    a'.eraseIdx (i + 1) ⋯) =
    (l.eraseIdx i).toArray

case isFalse
α : Type u_1
l : List α
i : Nat
h : i < l.toArray.size
h' : ¬i + 1 < l.toArray.size
⊢ l.toArray.pop = (l.eraseIdx i).toArray

Proof state:
α : Type u_1
x✝ : (l : List α) ×' (i : Nat) ×' i < l.toArray.size
a✝² :
  ∀ (y : (l : List α) ×' (i : Nat) ×' i < l.toArray.size),
    (invImage (fun x => PSigma.casesOn x fun l i => PSigma.casesOn i fun i h => l.length - i)
            instWellFoundedRelationOfSizeOf).1
        y x✝ →
      y.1.toArray.eraseIdx y.2.1 ⋯ = (y.1.eraseIdx y.2.1).toArray
l : List α
i✝ : (i : Nat) ×' i < l.toArray.size
a✝¹ :
  ∀ (y : (l : List α) ×' (i : Nat) ×' i < l.toArray.size),
    (invImage (fun x => PSigma.casesOn x fun l i => PSigma.casesOn i fun i h => l.length - i)
            instWellFoundedRelationOfSizeOf).1
        y ⟨l, i✝⟩ →
      y.1.toArray.eraseIdx y.2.1 ⋯ = (y.1.eraseIdx y.2.1).toArray
i : Nat
h✝¹ : i < l.toArray.size
a✝ :
  ∀ (y : (l : List α) ×' (i : Nat) ×' i < l.toArray.size),
    (invImage (fun x => PSigma.casesOn x fun l i => PSigma.casesOn i fun i h => l.length - i)
            instWellFoundedRelationOfSizeOf).1
        y ⟨l, ⟨i, h✝¹⟩⟩ →
      y.1.toArray.eraseIdx y.2.1 ⋯ = (y.1.eraseIdx y.2.1).toArray
h✝ : i + 1 < l.toArray.size
h : i + 1 < l.length
⊢ (l.toArray.swap (i + 1) i h✝ h✝¹).toList.length - (i + 1) < l.length - i

Tactic:
simp

Result:
α : Type u_1
x✝ : (l : List α) ×' (i : Nat) ×' i < l.toArray.size
a✝² :
  ∀ (y : (l : List α) ×' (i : Nat) ×' i < l.toArray.size),
    (invImage (fun x => PSigma.casesOn x fun l i => PSigma.casesOn i fun i h => l.length - i)
            instWellFoundedRelationOfSizeOf).1
        y x✝ →
      y.1.toArray.eraseIdx y.2.1 ⋯ = (y.1.eraseIdx y.2.1).toArray
l : List α
i✝ : (i : Nat) ×' i < l.toArray.size
a✝¹ :
  ∀ (y : (l : List α) ×' (i : Nat) ×' i < l.toArray.size),
    (invImage (fun x => PSigma.casesOn x fun l i => PSigma.casesOn i fun i h => l.length - i)
            instWellFoundedRelationOfSizeOf).1
        y ⟨l, i✝⟩ →
      y.1.toArray.eraseIdx y.2.1 ⋯ = (y.1.eraseIdx y.2.1).toArray
i : Nat
h✝¹ : i < l.toArray.size
a✝ :
  ∀ (y : (l : List α) ×' (i : Nat) ×' i < l.toArray.size),
    (invImage (fun x => PSigma.casesOn x fun l i => PSigma.casesOn i fun i h => l.length - i)
            instWellFoundedRelationOfSizeOf).1
        y ⟨l, ⟨i, h✝¹⟩⟩ →
      y.1.toArray.eraseIdx y.2.1 ⋯ = (y.1.eraseIdx y.2.1).toArray
h✝ : i + 1 < l.toArray.size
h : i + 1 < l.length
⊢ l.length - (i + 1) < l.length - i

Proof state:
case isFalse
α : Type u_1
l : List α
i : Nat
h : i < l.toArray.size
h' : ¬i + 1 < l.toArray.size
⊢ l.toArray.pop = (l.eraseIdx i).toArray

Tactic:
simp at h h'

Result:
case isFalse
α : Type u_1
l : List α
i : Nat
h : i < l.length
h' : l.length ≤ i + 1
⊢ l.toArray.pop = (l.eraseIdx i).toArray

Proof state:
case isTrue
α : Type u_1
l : List α
i : Nat
h : i < l.toArray.size
h' : i + 1 < l.toArray.size
⊢ (let a' := l.toArray.swap (i + 1) i h' h;
    a'.eraseIdx (i + 1) ⋯) =
    (l.eraseIdx i).toArray

Tactic:
rw [eraseIdx_toArray]

Result:
case isTrue
α : Type u_1
l : List α
i : Nat
h : i < l.toArray.size
h' : i + 1 < l.toArray.size
⊢ ((l.toArray.swap (i + 1) i h' h).toList.eraseIdx (i + 1)).toArray = (l.eraseIdx i).toArray

Proof state:
case isFalse
α : Type u_1
l : List α
i : Nat
h : i < l.length
h' : l.length ≤ i + 1
⊢ l.toArray.pop = (l.eraseIdx i).toArray

Tactic:
have t : i = l.length - 1 := by omega

Result:
case isFalse
α : Type u_1
l : List α
i : Nat
h : i < l.length
h' : l.length ≤ i + 1
t : i = l.length - 1
⊢ l.toArray.pop = (l.eraseIdx i).toArray

Proof state:
case isTrue
α : Type u_1
l : List α
i : Nat
h : i < l.toArray.size
h' : i + 1 < l.toArray.size
⊢ ((l.set (i + 1) l[i]).set i l[i + 1]).eraseIdx (i + 1) = l.eraseIdx i

Tactic:
rw [eraseIdx_set_gt (by simp), eraseIdx_set_eq]

Result:
case isTrue
α : Type u_1
l : List α
i : Nat
h : i < l.toArray.size
h' : i + 1 < l.toArray.size
⊢ (l.eraseIdx (i + 1)).set i l[i + 1] = l.eraseIdx i

Proof state:
α : Type u_1
l : List α
i : Nat
h : i < l.toArray.size
⊢ l.toArray.eraseIdx i h = (l.eraseIdx i).toArray

Tactic:
rw [Array.eraseIdx]

Result:
α : Type u_1
l : List α
i : Nat
h : i < l.toArray.size
⊢ (if h' : i + 1 < l.toArray.size then
      let a' := l.toArray.swap (i + 1) i h' h;
      a'.eraseIdx (i + 1) ⋯
    else l.toArray.pop) =
    (l.eraseIdx i).toArray

Proof state:
α : Type u_1
l : List α
i : Nat
h : i < l.toArray.size
h' : i + 1 < l.toArray.size
⊢ i < i + 1

Tactic:
simp

Result:
no goals

Proof state:
case isTrue
α : Type u_1
l : List α
i : Nat
h : i < l.toArray.size
h' : i + 1 < l.toArray.size
⊢ (l.eraseIdx (i + 1)).set i l[i + 1] = l.eraseIdx i

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
x✝ : (l : List α) ×' (i : Nat) ×' i < l.toArray.size
a✝² :
  ∀ (y : (l : List α) ×' (i : Nat) ×' i < l.toArray.size),
    (invImage (fun x => PSigma.casesOn x fun l i => PSigma.casesOn i fun i h => l.length - i)
            instWellFoundedRelationOfSizeOf).1
        y x✝ →
      y.1.toArray.eraseIdx y.2.1 ⋯ = (y.1.eraseIdx y.2.1).toArray
l : List α
i✝ : (i : Nat) ×' i < l.toArray.size
a✝¹ :
  ∀ (y : (l : List α) ×' (i : Nat) ×' i < l.toArray.size),
    (invImage (fun x => PSigma.casesOn x fun l i => PSigma.casesOn i fun i h => l.length - i)
            instWellFoundedRelationOfSizeOf).1
        y ⟨l, i✝⟩ →
      y.1.toArray.eraseIdx y.2.1 ⋯ = (y.1.eraseIdx y.2.1).toArray
i : Nat
h✝¹ : i < l.toArray.size
a✝ :
  ∀ (y : (l : List α) ×' (i : Nat) ×' i < l.toArray.size),
    (invImage (fun x => PSigma.casesOn x fun l i => PSigma.casesOn i fun i h => l.length - i)
            instWellFoundedRelationOfSizeOf).1
        y ⟨l, ⟨i, h✝¹⟩⟩ →
      y.1.toArray.eraseIdx y.2.1 ⋯ = (y.1.eraseIdx y.2.1).toArray
h✝ : i + 1 < l.toArray.size
h : i + 1 < l.length
⊢ l.length - (i + 1) < l.length - i

Tactic:
omega

Result:
no goals

Proof state:
case isTrue
α : Type u_1
l : List α
i : Nat
h : i < l.toArray.size
h' : i + 1 < l.toArray.size
⊢ ((l.toArray.swap (i + 1) i h' h).toList.eraseIdx (i + 1)).toArray = (l.eraseIdx i).toArray

Tactic:
simp only [swap_toArray, Fin.getElem_fin, toList_toArray, mk.injEq]

Result:
case isTrue
α : Type u_1
l : List α
i : Nat
h : i < l.toArray.size
h' : i + 1 < l.toArray.size
⊢ ((l.set (i + 1) l[i]).set i l[i + 1]).eraseIdx (i + 1) = l.eraseIdx i