α : Type u_1
p q : α → Bool
a : α
l : List α
h : (p a = true ↔ q a = true) ∧ ∀ (x : α), x ∈ l → (p x = true ↔ q x = true)
⊢ filter p (a :: l) = filter q (a :: l)
α : Type u_1
p q : α → Bool
a : α
l : List α
h : ∀ (x : α), x ∈ a :: l → (p x = true ↔ q x = true)
⊢ filter p (a :: l) = filter q (a :: l)
rw [forall_mem_cons] at h
case pos
α : Type u_1
p q : α → Bool
a : α
l : List α
h : (p a = true ↔ q a = true) ∧ ∀ (x : α), x ∈ l → (p x = true ↔ q x = true)
pa : p a = true
⊢ filter p (a :: l) = filter q (a :: l)

case neg
α : Type u_1
p q : α → Bool
a : α
l : List α
h : (p a = true ↔ q a = true) ∧ ∀ (x : α), x ∈ l → (p x = true ↔ q x = true)
pa : ¬p a = true
⊢ filter p (a :: l) = filter q (a :: l)
α : Type u_1
p q : α → Bool
a : α
l : List α
h : (p a = true ↔ q a = true) ∧ ∀ (x : α), x ∈ l → (p x = true ↔ q x = true)
⊢ filter p (a :: l) = filter q (a :: l)
by_cases pa : p a
no goals
case pos
α : Type u_1
p q : α → Bool
a : α
l : List α
h : (p a = true ↔ q a = true) ∧ ∀ (x : α), x ∈ l → (p x = true ↔ q x = true)
pa : p a = true
⊢ filter p (a :: l) = filter q (a :: l)
simp [pa, h.1.1 pa, filter_congr' h.2]
no goals
case neg
α : Type u_1
p q : α → Bool
a : α
l : List α
h : (p a = true ↔ q a = true) ∧ ∀ (x : α), x ∈ l → (p x = true ↔ q x = true)
pa : ¬p a = true
⊢ filter p (a :: l) = filter q (a :: l)
simp [pa, mt h.1.2 pa, filter_congr' h.2]