no goals
α✝ : Type u_1
p : α✝ → Bool
l : List α✝
⊢ filter p l = l ↔ ∀ (a : α✝), a ∈ l → p a = true
induction l with simp
| cons a l ih =>
  cases h : p a <;> simp [*]
  intro h; exact Nat.lt_irrefl _ (h ▸ length_filter_le p l)
case cons.false
α✝ : Type u_1
p : α✝ → Bool
a : α✝
l : List α✝
ih : filter p l = l ↔ ∀ (a : α✝), a ∈ l → p a = true
h : p a = false
⊢ ¬filter p l = a :: l
case cons
α✝ : Type u_1
p : α✝ → Bool
a : α✝
l : List α✝
ih : filter p l = l ↔ ∀ (a : α✝), a ∈ l → p a = true
⊢ filter p (a :: l) = a :: l ↔ p a = true ∧ ∀ (a : α✝), a ∈ l → p a = true
cases h : p a <;> simp [*]
case cons.false
α✝ : Type u_1
p : α✝ → Bool
a : α✝
l : List α✝
ih : filter p l = l ↔ ∀ (a : α✝), a ∈ l → p a = true
h✝ : p a = false
h : filter p l = a :: l
⊢ False
case cons.false
α✝ : Type u_1
p : α✝ → Bool
a : α✝
l : List α✝
ih : filter p l = l ↔ ∀ (a : α✝), a ∈ l → p a = true
h : p a = false
⊢ ¬filter p l = a :: l
intro h
no goals
case cons.false
α✝ : Type u_1
p : α✝ → Bool
a : α✝
l : List α✝
ih : filter p l = l ↔ ∀ (a : α✝), a ∈ l → p a = true
h✝ : p a = false
h : filter p l = a :: l
⊢ False
exact Nat.lt_irrefl _ (h ▸ length_filter_le p l)