no goals
case nil
α✝ : Type u_1
x : α✝
p : α✝ → Bool
⊢ x ∈ filter p [] ↔ x ∈ [] ∧ p x = true
simp [filter]
case pos
α✝ : Type u_1
x : α✝
p : α✝ → Bool
a : α✝
as : List α✝
ih : x ∈ filter p as ↔ x ∈ as ∧ p x = true
h : p a = true
⊢ x = a ∨ x ∈ as ∧ p x = true ↔ x = a ∧ p x = true ∨ x ∈ as ∧ p x = true

case neg
α✝ : Type u_1
x : α✝
p : α✝ → Bool
a : α✝
as : List α✝
ih : x ∈ filter p as ↔ x ∈ as ∧ p x = true
h : ¬p a = true
⊢ x ∈ as ∧ p x = true ↔ x = a ∧ p x = true ∨ x ∈ as ∧ p x = true
case cons
α✝ : Type u_1
x : α✝
p : α✝ → Bool
a : α✝
as : List α✝
ih : x ∈ filter p as ↔ x ∈ as ∧ p x = true
⊢ x ∈ filter p (a :: as) ↔ x ∈ a :: as ∧ p x = true
by_cases h : p a <;> simp [*, or_and_right]
no goals
case pos
α✝ : Type u_1
x : α✝
p : α✝ → Bool
a : α✝
as : List α✝
ih : x ∈ filter p as ↔ x ∈ as ∧ p x = true
h : p a = true
⊢ x = a ∨ x ∈ as ∧ p x = true ↔ x = a ∧ p x = true ∨ x ∈ as ∧ p x = true
exact or_congr_left (and_iff_left_of_imp fun | rfl => h).symm
no goals
case neg
α✝ : Type u_1
x : α✝
p : α✝ → Bool
a : α✝
as : List α✝
ih : x ∈ filter p as ↔ x ∈ as ∧ p x = true
h : ¬p a = true
⊢ x ∈ as ∧ p x = true ↔ x = a ∧ p x = true ∨ x ∈ as ∧ p x = true
exact (or_iff_right fun ⟨rfl, h'⟩ => h h').symm