cases h₂ : p₂ x with
| false =>
  simp only [filterSpec, h₂, ite_false]
  exact ih
| true =>
  simp only [filterSpec, h₂, ite_true]
  cases h₁ : p₁ x with
  | false =>
    simp only [filterSpec, h₁, h₂, ite_false]
    exact ih
  | true =>
    simp only [filterSpec, h₁, h₂, ite_true]
    exact congrArg _ ih
case cons
α : Type u_1
p₁ p₂ : α → Bool
x : α
xs : List α
ih : filterSpec p₁ (filterSpec p₂ xs) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
⊢ filterSpec p₁ (filterSpec p₂ (x :: xs)) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) (x :: xs)
no goals