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

State before:
α : Type u_1
p₁ p₂ : α → Bool
xs : List α
⊢ filter p₁ (filter p₂ xs) = filter (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
Tactic:
rw [filter_eq_filterSpec, filter_eq_filterSpec, filter_eq_filterSpec]
State after:
α : Type u_1
p₁ p₂ : α → Bool
xs : List α
⊢ filterSpec p₁ (filterSpec p₂ xs) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs

State before:
α : Type u_1
p₁ p₂ : α → Bool
xs : List α
⊢ filterSpec p₁ (filterSpec p₂ xs) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
Tactic:
induction xs with
| nil => simp [filterSpec]
| cons x xs ih =>
  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
State after:
no goals

State before:
case nil
α : Type u_1
p₁ p₂ : α → Bool
⊢ filterSpec p₁ (filterSpec p₂ []) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) []
Tactic:
simp [filterSpec]
State after:
no goals

State before:
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)
Tactic:
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
State after:
no goals

State before:
case cons.false
α : 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
h₂ : p₂ x = false
⊢ filterSpec p₁ (filterSpec p₂ (x :: xs)) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) (x :: xs)
Tactic:
simp only [filterSpec, h₂, ite_false]
State after:
case cons.false
α : 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
h₂ : p₂ x = false
⊢ filterSpec p₁ (filterSpec p₂ xs) =
    if decide (False ∧ p₁ x = true) = true then x :: filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
    else filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs

State before:
case cons.false
α : 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
h₂ : p₂ x = false
⊢ filterSpec p₁ (filterSpec p₂ xs) =
    if decide (False ∧ p₁ x = true) = true then x :: filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
    else filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
Tactic:
exact ih
State after:
no goals

State before:
case cons.true
α : 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
h₂ : p₂ x = true
⊢ filterSpec p₁ (filterSpec p₂ (x :: xs)) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) (x :: xs)
Tactic:
simp only [filterSpec, h₂, ite_true]
State after:
case cons.true
α : 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
h₂ : p₂ x = true
⊢ (if p₁ x = true then x :: filterSpec p₁ (filterSpec p₂ xs) else filterSpec p₁ (filterSpec p₂ xs)) =
    if decide (True ∧ p₁ x = true) = true then x :: filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
    else filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs

State before:
case cons.true
α : 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
h₂ : p₂ x = true
⊢ (if p₁ x = true then x :: filterSpec p₁ (filterSpec p₂ xs) else filterSpec p₁ (filterSpec p₂ xs)) =
    if decide (True ∧ p₁ x = true) = true then x :: filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
    else filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
Tactic:
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
State after:
no goals

State before:
case cons.true.false
α : 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
h₂ : p₂ x = true
h₁ : p₁ x = false
⊢ (if false = true then x :: filterSpec p₁ (filterSpec p₂ xs) else filterSpec p₁ (filterSpec p₂ xs)) =
    if decide (True ∧ false = true) = true then x :: filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
    else filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
Tactic:
simp only [filterSpec, h₁, h₂, ite_false]
State after:
case cons.true.false
α : 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
h₂ : p₂ x = true
h₁ : p₁ x = false
⊢ filterSpec p₁ (filterSpec p₂ xs) =
    if decide (True ∧ False) = true then x :: filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
    else filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs

State before:
case cons.true.false
α : 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
h₂ : p₂ x = true
h₁ : p₁ x = false
⊢ filterSpec p₁ (filterSpec p₂ xs) =
    if decide (True ∧ False) = true then x :: filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
    else filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
Tactic:
exact ih
State after:
no goals

State before:
case cons.true.true
α : 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
h₂ : p₂ x = true
h₁ : p₁ x = true
⊢ (if true = true then x :: filterSpec p₁ (filterSpec p₂ xs) else filterSpec p₁ (filterSpec p₂ xs)) =
    if decide (True ∧ true = true) = true then x :: filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
    else filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
Tactic:
simp only [filterSpec, h₁, h₂, ite_true]
State after:
case cons.true.true
α : 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
h₂ : p₂ x = true
h₁ : p₁ x = true
⊢ x :: filterSpec p₁ (filterSpec p₂ xs) =
    if decide (True ∧ True) = true then x :: filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
    else filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs

State before:
case cons.true.true
α : 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
h₂ : p₂ x = true
h₁ : p₁ x = true
⊢ x :: filterSpec p₁ (filterSpec p₂ xs) =
    if decide (True ∧ True) = true then x :: filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
    else filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
Tactic:
exact congrArg _ ih
State after:
no goals