-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem eraseP_eq_eraseIdx {xs : List α} {p : α → Bool} :
    xs.eraseP p = match xs.findIdx? p with
    | none => xs
    | some i => xs.eraseIdx i

Proof state:
case nil
α : Type u_1
p : α → Bool
⊢ eraseP p [] =
    match findIdx? p [] with
    | none => []
    | some i => [].eraseIdx i

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  eraseP p xs =
    match findIdx? p xs with
    | none => xs
    | some i => xs.eraseIdx i
⊢ eraseP p (x :: xs) =
    match findIdx? p (x :: xs) with
    | none => x :: xs
    | some i => (x :: xs).eraseIdx i

Tactic:
rw [eraseP_cons, findIdx?_cons]

Result:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  eraseP p xs =
    match findIdx? p xs with
    | none => xs
    | some i => xs.eraseIdx i
⊢ (bif p x then xs else x :: eraseP p xs) =
    match if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs) with
    | none => x :: xs
    | some i => (x :: xs).eraseIdx i

Proof state:
case neg
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  eraseP p xs =
    match findIdx? p xs with
    | none => xs
    | some i => xs.eraseIdx i
h : ¬p x = true
⊢ (bif false then xs
    else
      x ::
        match findIdx? p xs with
        | none => xs
        | some i => xs.eraseIdx i) =
    match if false = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs) with
    | none => x :: xs
    | some i => (x :: xs).eraseIdx i

Tactic:
split <;> simp [*]

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  eraseP p xs =
    match findIdx? p xs with
    | none => xs
    | some i => xs.eraseIdx i
⊢ (bif p x then xs else x :: eraseP p xs) =
    match if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs) with
    | none => x :: xs
    | some i => (x :: xs).eraseIdx i

Tactic:
by_cases h : p x

Result:
case pos
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  eraseP p xs =
    match findIdx? p xs with
    | none => xs
    | some i => xs.eraseIdx i
h : p x = true
⊢ (bif p x then xs else x :: eraseP p xs) =
    match if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs) with
    | none => x :: xs
    | some i => (x :: xs).eraseIdx i

case neg
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  eraseP p xs =
    match findIdx? p xs with
    | none => xs
    | some i => xs.eraseIdx i
h : ¬p x = true
⊢ (bif p x then xs else x :: eraseP p xs) =
    match if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs) with
    | none => x :: xs
    | some i => (x :: xs).eraseIdx i

Proof state:
case neg
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  eraseP p xs =
    match findIdx? p xs with
    | none => xs
    | some i => xs.eraseIdx i
h : ¬p x = true
⊢ (bif p x then xs else x :: eraseP p xs) =
    match if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs) with
    | none => x :: xs
    | some i => (x :: xs).eraseIdx i

Tactic:
simp only [h]

Result:
case neg
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  eraseP p xs =
    match findIdx? p xs with
    | none => xs
    | some i => xs.eraseIdx i
h : ¬p x = true
⊢ (bif false then xs else x :: eraseP p xs) =
    match if false = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs) with
    | none => x :: xs
    | some i => (x :: xs).eraseIdx i

Proof state:
case neg
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  eraseP p xs =
    match findIdx? p xs with
    | none => xs
    | some i => xs.eraseIdx i
h : ¬p x = true
⊢ (bif false then xs else x :: eraseP p xs) =
    match if false = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs) with
    | none => x :: xs
    | some i => (x :: xs).eraseIdx i

Tactic:
rw [ih]

Result:
case neg
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  eraseP p xs =
    match findIdx? p xs with
    | none => xs
    | some i => xs.eraseIdx i
h : ¬p x = true
⊢ (bif false then xs
    else
      x ::
        match findIdx? p xs with
        | none => xs
        | some i => xs.eraseIdx i) =
    match if false = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs) with
    | none => x :: xs
    | some i => (x :: xs).eraseIdx i

Proof state:
case pos
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  eraseP p xs =
    match findIdx? p xs with
    | none => xs
    | some i => xs.eraseIdx i
h : p x = true
⊢ (bif p x then xs else x :: eraseP p xs) =
    match if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs) with
    | none => x :: xs
    | some i => (x :: xs).eraseIdx i

Tactic:
simp [h]

Result:
no goals