-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem erase_eq_eraseIdx (l : List α) (a : α) :
    l.erase a = match l.idxOf? a with
    | none => l
    | some i => l.eraseIdx i

Proof state:
case cons
α : Type u_1
inst✝ : BEq α
a x : α
xs : List α
ih :
  xs.erase a =
    match idxOf? a xs with
    | none => xs
    | some i => xs.eraseIdx i
⊢ (if (x == a) = true then xs else x :: xs.erase a) =
    match if (x == a) = true then some 0 else Option.map (fun x => x + 1) (idxOf? a xs) with
    | none => x :: xs
    | some i => (x :: xs).eraseIdx i

Tactic:
split

Result:
case cons.isTrue
α : Type u_1
inst✝ : BEq α
a x : α
xs : List α
ih :
  xs.erase a =
    match idxOf? a xs with
    | none => xs
    | some i => xs.eraseIdx i
h✝ : (x == a) = true
⊢ xs =
    match some 0 with
    | none => x :: xs
    | some i => (x :: xs).eraseIdx i

case cons.isFalse
α : Type u_1
inst✝ : BEq α
a x : α
xs : List α
ih :
  xs.erase a =
    match idxOf? a xs with
    | none => xs
    | some i => xs.eraseIdx i
h✝ : ¬(x == a) = true
⊢ x :: xs.erase a =
    match Option.map (fun x => x + 1) (idxOf? a xs) with
    | none => x :: xs
    | some i => (x :: xs).eraseIdx i

Proof state:
case cons.isTrue
α : Type u_1
inst✝ : BEq α
a x : α
xs : List α
ih :
  xs.erase a =
    match idxOf? a xs with
    | none => xs
    | some i => xs.eraseIdx i
h✝ : (x == a) = true
⊢ xs =
    match some 0 with
    | none => x :: xs
    | some i => (x :: xs).eraseIdx i

Tactic:
simp

Result:
no goals

Proof state:
case cons.isFalse
α : Type u_1
inst✝ : BEq α
a x : α
xs : List α
ih :
  xs.erase a =
    match idxOf? a xs with
    | none => xs
    | some i => xs.eraseIdx i
h✝ : ¬(x == a) = true
⊢ x :: xs.erase a =
    match Option.map (fun x => x + 1) (idxOf? a xs) with
    | none => x :: xs
    | some i => (x :: xs).eraseIdx i

Tactic:
simp [ih]

Result:
case cons.isFalse
α : Type u_1
inst✝ : BEq α
a x : α
xs : List α
ih :
  xs.erase a =
    match idxOf? a xs with
    | none => xs
    | some i => xs.eraseIdx i
h✝ : ¬(x == a) = true
⊢ (x ::
      match idxOf? a xs with
      | none => xs
      | some i => xs.eraseIdx i) =
    match Option.map (fun x => x + 1) (idxOf? a xs) with
    | none => x :: xs
    | some i => (x :: xs).eraseIdx i

Proof state:
case nil
α : Type u_1
inst✝ : BEq α
a : α
⊢ [].erase a =
    match idxOf? a [] with
    | none => []
    | some i => [].eraseIdx i

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : BEq α
a x : α
xs : List α
ih :
  xs.erase a =
    match idxOf? a xs with
    | none => xs
    | some i => xs.eraseIdx i
⊢ (x :: xs).erase a =
    match idxOf? a (x :: xs) with
    | none => x :: xs
    | some i => (x :: xs).eraseIdx i

Tactic:
rw [erase_cons, idxOf?_cons]

Result:
case cons
α : Type u_1
inst✝ : BEq α
a x : α
xs : List α
ih :
  xs.erase a =
    match idxOf? a xs with
    | none => xs
    | some i => xs.eraseIdx i
⊢ (if (x == a) = true then xs else x :: xs.erase a) =
    match if (x == a) = true then some 0 else Option.map (fun x => x + 1) (idxOf? a xs) with
    | none => x :: xs
    | some i => (x :: xs).eraseIdx i

Proof state:
case cons.isFalse
α : Type u_1
inst✝ : BEq α
a x : α
xs : List α
ih :
  xs.erase a =
    match idxOf? a xs with
    | none => xs
    | some i => xs.eraseIdx i
h✝ : ¬(x == a) = true
⊢ (x ::
      match idxOf? a xs with
      | none => xs
      | some i => xs.eraseIdx i) =
    match Option.map (fun x => x + 1) (idxOf? a xs) with
    | none => x :: xs
    | some i => (x :: xs).eraseIdx i

Tactic:
split <;> simp [*]

Result:
no goals