Theorem: List.filter_eq_filterSpec (Table/BuiltinExtensions.lean)

State before:
α✝ : Type u_1
p : α✝ → Bool
xs : List α✝
⊢ filter p xs = filterSpec p xs
Tactic:
induction xs with
| nil => simp [filter, filterSpec]
| cons x xs ih =>
  simp only [filter, filterSpec]
  cases p x with
  | true => simp only [ite_true, ih]
  | false => simp only [ite_false, ih]
State after:
no goals

State before:
case nil
α✝ : Type u_1
p : α✝ → Bool
⊢ filter p [] = filterSpec p []
Tactic:
simp [filter, filterSpec]
State after:
no goals

State before:
case cons
α✝ : Type u_1
p : α✝ → Bool
x : α✝
xs : List α✝
ih : filter p xs = filterSpec p xs
⊢ filter p (x :: xs) = filterSpec p (x :: xs)
Tactic:
simp only [filter, filterSpec]
State after:
case cons
α✝ : Type u_1
p : α✝ → Bool
x : α✝
xs : List α✝
ih : filter p xs = filterSpec p xs
⊢ (match p x with
    | true => x :: filter p xs
    | false => filter p xs) =
    if p x = true then x :: filterSpec p xs else filterSpec p xs

State before:
case cons
α✝ : Type u_1
p : α✝ → Bool
x : α✝
xs : List α✝
ih : filter p xs = filterSpec p xs
⊢ (match p x with
    | true => x :: filter p xs
    | false => filter p xs) =
    if p x = true then x :: filterSpec p xs else filterSpec p xs
Tactic:
cases p x with
| true => simp only [ite_true, ih]
| false => simp only [ite_false, ih]
State after:
no goals

State before:
case cons.true
α✝ : Type u_1
p : α✝ → Bool
x : α✝
xs : List α✝
ih : filter p xs = filterSpec p xs
⊢ (match true with
    | true => x :: filter p xs
    | false => filter p xs) =
    if true = true then x :: filterSpec p xs else filterSpec p xs
Tactic:
simp only [ite_true, ih]
State after:
no goals

State before:
case cons.false
α✝ : Type u_1
p : α✝ → Bool
x : α✝
xs : List α✝
ih : filter p xs = filterSpec p xs
⊢ (match false with
    | true => x :: filter p xs
    | false => filter p xs) =
    if false = true then x :: filterSpec p xs else filterSpec p xs
Tactic:
simp only [ite_false, ih]
State after:
no goals