-- Mathlib/Data/List/Basic.lean
theorem erase_getElem [DecidableEq ι] {l : List ι} {i : ℕ} (hi : i < l.length) :
    Perm (l.erase l[i]) (l.eraseIdx i)

Proof state:
ι : Type u_1
inst✝ : DecidableEq ι
a : ι
l : List ι
IH : ∀ {i : ℕ} (hi : i < l.length), l.erase l[i] ~ l.eraseIdx i
i : ℕ
hi : i + 1 < (a :: l).length
⊢ i < l.length

Tactic:
simpa using hi

Result:
no goals

Proof state:
case nil
ι : Type u_1
inst✝ : DecidableEq ι
i : ℕ
hi : i < [].length
⊢ [].erase [][i] ~ [].eraseIdx i

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : DecidableEq ι
l : List ι
i : ℕ
hi : i < l.length
⊢ l.erase l[i] ~ l.eraseIdx i

Tactic:
induction l generalizing i with
| nil => simp
| cons a l IH =>
  cases i with
  | zero => simp
  | succ i =>
    have hi' : i < l.length := by simpa using hi
    if ha : a = l[i] then
      simpa [ha] using .trans (perm_cons_erase (getElem_mem _)) (.cons _ (IH hi'))
    else
      simpa [ha] using IH hi'

Result:
no goals

Proof state:
case cons.zero
ι : Type u_1
inst✝ : DecidableEq ι
a : ι
l : List ι
IH : ∀ {i : ℕ} (hi : i < l.length), l.erase l[i] ~ l.eraseIdx i
hi : 0 < (a :: l).length
⊢ (a :: l).erase (a :: l)[0] ~ (a :: l).eraseIdx 0

Tactic:
simp

Result:
no goals

Proof state:
case cons.succ
ι : Type u_1
inst✝ : DecidableEq ι
a : ι
l : List ι
IH : ∀ {i : ℕ} (hi : i < l.length), l.erase l[i] ~ l.eraseIdx i
i : ℕ
hi : i + 1 < (a :: l).length
⊢ (a :: l).erase (a :: l)[i + 1] ~ (a :: l).eraseIdx (i + 1)

Tactic:
have hi' : i < l.length := by simpa using hi

Result:
case cons.succ
ι : Type u_1
inst✝ : DecidableEq ι
a : ι
l : List ι
IH : ∀ {i : ℕ} (hi : i < l.length), l.erase l[i] ~ l.eraseIdx i
i : ℕ
hi : i + 1 < (a :: l).length
hi' : i < l.length
⊢ (a :: l).erase (a :: l)[i + 1] ~ (a :: l).eraseIdx (i + 1)

Proof state:
ι : Type u_1
inst✝ : DecidableEq ι
a : ι
l : List ι
IH : ∀ {i : ℕ} (hi : i < l.length), l.erase l[i] ~ l.eraseIdx i
i : ℕ
hi : i + 1 < (a :: l).length
hi' : i < l.length
ha : ¬a = l[i]
⊢ (a :: l).erase (a :: l)[i + 1] ~ (a :: l).eraseIdx (i + 1)

Tactic:
simpa [ha] using IH hi'

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : DecidableEq ι
a : ι
l : List ι
IH : ∀ {i : ℕ} (hi : i < l.length), l.erase l[i] ~ l.eraseIdx i
i : ℕ
hi : i + 1 < (a :: l).length
hi' : i < l.length
ha : a = l[i]
⊢ (a :: l).erase (a :: l)[i + 1] ~ (a :: l).eraseIdx (i + 1)

Tactic:
simpa [ha] using .trans (perm_cons_erase (getElem_mem _)) (.cons _ (IH hi'))

Result:
no goals

Proof state:
case cons.succ
ι : Type u_1
inst✝ : DecidableEq ι
a : ι
l : List ι
IH : ∀ {i : ℕ} (hi : i < l.length), l.erase l[i] ~ l.eraseIdx i
i : ℕ
hi : i + 1 < (a :: l).length
hi' : i < l.length
⊢ (a :: l).erase (a :: l)[i + 1] ~ (a :: l).eraseIdx (i + 1)

Tactic:
if ha : a = l[i] then
  simpa [ha] using .trans (perm_cons_erase (getElem_mem _)) (.cons _ (IH hi'))
else
  simpa [ha] using IH hi'

Result:
no goals

Proof state:
case cons
ι : Type u_1
inst✝ : DecidableEq ι
a : ι
l : List ι
IH : ∀ {i : ℕ} (hi : i < l.length), l.erase l[i] ~ l.eraseIdx i
i : ℕ
hi : i < (a :: l).length
⊢ (a :: l).erase (a :: l)[i] ~ (a :: l).eraseIdx i

Tactic:
cases i with
| zero => simp
| succ i =>
  have hi' : i < l.length := by simpa using hi
  if ha : a = l[i] then
    simpa [ha] using .trans (perm_cons_erase (getElem_mem _)) (.cons _ (IH hi'))
  else
    simpa [ha] using IH hi'

Result:
no goals