-- Mathlib/Data/Vector/Basic.lean
theorem eraseIdx_insertIdx' {v : Vector α (n + 1)} :
    ∀ {i : Fin (n + 1)} {j : Fin (n + 2)},
      eraseIdx (j.succAbove i) (insertIdx a j v) = insertIdx a (i.predAbove j) (eraseIdx i v)
  | ⟨i, hi⟩, ⟨j, hj⟩ => by
    dsimp [insertIdx, eraseIdx, Fin.succAbove, Fin.predAbove]
    rw [Subtype.mk_eq_mk]
    simp only [Fin.lt_iff_val_lt_val]
    split_ifs with hij
    · rcases Nat.exists_eq_succ_of_ne_zero
        (Nat.pos_iff_ne_zero.1 (lt_of_le_of_lt (Nat.zero_le _) hij)) with ⟨j, rfl⟩
      rw [← List.insertIdx_eraseIdx_of_ge]
      · simp; rfl
      · simpa
      · simpa [Nat.lt_succ_iff] using hij
    · dsimp
      rw [← List.insertIdx_eraseIdx_of_le i j _ _ _]
      · rfl
      · simpa
      · simpa [not_lt] using hij

Proof state:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
⊢ (List.insertIdx j a ↑v).eraseIdx ↑(if i < j then ⟨i, ⋯⟩ else ⟨i + 1, ⋯⟩) =
    List.insertIdx (↑(if h : i < j then ⟨j, hj⟩.pred ⋯ else ⟨j, hj⟩.castPred ⋯)) a
      ↑(match v with
        | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)

Tactic:
split_ifs with hij

Result:
case pos
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : i < j
⊢ (List.insertIdx j a ↑v).eraseIdx ↑⟨i, ⋯⟩ =
    List.insertIdx (↑(⟨j, hj⟩.pred ⋯)) a
      ↑(match v with
        | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)

case neg
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ (List.insertIdx j a ↑v).eraseIdx ↑⟨i + 1, ⋯⟩ =
    List.insertIdx (↑(⟨j, hj⟩.castPred ⋯)) a
      ↑(match v with
        | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)

Proof state:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
⊢ eraseIdx (⟨j, hj⟩.succAbove ⟨i, hi⟩) (insertIdx a ⟨j, hj⟩ v) =
    insertIdx a (⟨i, hi⟩.predAbove ⟨j, hj⟩) (eraseIdx ⟨i, hi⟩ v)

Tactic:
dsimp [insertIdx, eraseIdx, Fin.succAbove, Fin.predAbove]

Result:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
⊢ ⟨(List.insertIdx j a ↑v).eraseIdx ↑(if ⟨i, ⋯⟩ < ⟨j, hj⟩ then ⟨i, ⋯⟩ else ⟨i + 1, ⋯⟩), ⋯⟩ =
    ⟨List.insertIdx (↑(if h : ⟨i, ⋯⟩ < ⟨j, hj⟩ then ⟨j, hj⟩.pred ⋯ else ⟨j, hj⟩.castPred ⋯)) a
        ↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩),
      ⋯⟩

Proof state:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ j ≤ i

Tactic:
simpa [not_lt] using hij

Result:
no goals

Proof state:
case pos.intro
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ (List.insertIdx j.succ a ↑v).eraseIdx ↑⟨i, ⋯⟩ =
    List.insertIdx (↑(⟨j.succ, hj⟩.pred ⋯)) a
      ↑(match v with
        | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)

Tactic:
rw [← List.insertIdx_eraseIdx_of_ge]

Result:
case pos.intro
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ List.insertIdx j a ((↑v).eraseIdx ↑⟨i, ⋯⟩) =
    List.insertIdx (↑(⟨j.succ, hj⟩.pred ⋯)) a
      ↑(match v with
        | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)

case pos.intro.a
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ ↑⟨i, ⋯⟩ < (↑v).length

case pos.intro.a
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ ↑⟨i, ⋯⟩ ≤ j

Proof state:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
⊢ (List.insertIdx j a ↑v).eraseIdx ↑(if ⟨i, ⋯⟩ < ⟨j, hj⟩ then ⟨i, ⋯⟩ else ⟨i + 1, ⋯⟩) =
    List.insertIdx (↑(if h : ⟨i, ⋯⟩ < ⟨j, hj⟩ then ⟨j, hj⟩.pred ⋯ else ⟨j, hj⟩.castPred ⋯)) a
      ↑(match v with
        | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)

Tactic:
simp only [Fin.lt_iff_val_lt_val]

Result:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
⊢ (List.insertIdx j a ↑v).eraseIdx ↑(if i < j then ⟨i, ⋯⟩ else ⟨i + 1, ⋯⟩) =
    List.insertIdx (↑(if h : i < j then ⟨j, hj⟩.pred ⋯ else ⟨j, hj⟩.castPred ⋯)) a
      ↑(match v with
        | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)

Proof state:
case pos.intro.a
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ ↑⟨i, ⋯⟩ ≤ j

Tactic:
simpa [Nat.lt_succ_iff] using hij

Result:
no goals

Proof state:
case pos.intro.a
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ ↑⟨i, ⋯⟩ < (↑v).length

Tactic:
simpa

Result:
no goals

Proof state:
case neg
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ List.insertIdx j a ((↑v).eraseIdx i) =
    List.insertIdx j a
      ↑(match v with
        | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)

Tactic:
rfl

Result:
no goals

Proof state:
case pos.intro
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ List.insertIdx j a ((↑v).eraseIdx i) =
    List.insertIdx j a
      ↑(match v with
        | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ i < (↑v).length

Tactic:
simpa

Result:
no goals

Proof state:
case pos
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : i < j
⊢ (List.insertIdx j a ↑v).eraseIdx ↑⟨i, ⋯⟩ =
    List.insertIdx (↑(⟨j, hj⟩.pred ⋯)) a
      ↑(match v with
        | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)

Tactic:
rcases Nat.exists_eq_succ_of_ne_zero
  (Nat.pos_iff_ne_zero.1 (lt_of_le_of_lt (Nat.zero_le _) hij)) with ⟨j, rfl⟩

Result:
case pos.intro
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ (List.insertIdx j.succ a ↑v).eraseIdx ↑⟨i, ⋯⟩ =
    List.insertIdx (↑(⟨j.succ, hj⟩.pred ⋯)) a
      ↑(match v with
        | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)

Proof state:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
⊢ ⟨(List.insertIdx j a ↑v).eraseIdx ↑(if ⟨i, ⋯⟩ < ⟨j, hj⟩ then ⟨i, ⋯⟩ else ⟨i + 1, ⋯⟩), ⋯⟩ =
    ⟨List.insertIdx (↑(if h : ⟨i, ⋯⟩ < ⟨j, hj⟩ then ⟨j, hj⟩.pred ⋯ else ⟨j, hj⟩.castPred ⋯)) a
        ↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩),
      ⋯⟩

Tactic:
rw [Subtype.mk_eq_mk]

Result:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
⊢ (List.insertIdx j a ↑v).eraseIdx ↑(if ⟨i, ⋯⟩ < ⟨j, hj⟩ then ⟨i, ⋯⟩ else ⟨i + 1, ⋯⟩) =
    List.insertIdx (↑(if h : ⟨i, ⋯⟩ < ⟨j, hj⟩ then ⟨j, hj⟩.pred ⋯ else ⟨j, hj⟩.castPred ⋯)) a
      ↑(match v with
        | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)

Proof state:
case neg
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ (List.insertIdx j a ↑v).eraseIdx (i + 1) =
    List.insertIdx j a
      ↑(match v with
        | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)

Tactic:
rw [← List.insertIdx_eraseIdx_of_le i j _ _ _]

Result:
case neg
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ List.insertIdx j a ((↑v).eraseIdx i) =
    List.insertIdx j a
      ↑(match v with
        | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)

α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ i < (↑v).length

α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ j ≤ i