-- 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
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
⊢ (l.toArray.swap (i + 1) i h✝ h).toList.length - (i + 1) < l.length - i

Tactic:
rename_i h

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
⊢ (l.toArray.swap (i + 1) i h h✝).toList.length - (i + 1) < l.length - i

Proof state:
α : Type u_1
l : List α
i : Nat
h : i < l.length
h' : l.length ≤ i + 1
⊢ i = l.length - 1

Tactic:
omega

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
⊢ (l.toArray.swap (i + 1) i h h✝).toList.length - (i + 1) < l.length - i

Tactic:
simp at h

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.toArray.swap (i + 1) i h✝ h✝¹).toList.length - (i + 1) < l.length - i

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

Tactic:
simp [t]

Result:
no goals