no goals
α : Type u_1
β : Type ?u.331102
γ : Type ?u.331105
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
⊢ filter p {a} = if p a then {a} else ∅
classical
  ext x
  simp
  split_ifs with h <;> by_cases h' : x = a <;> simp [h, h']
case a
α : Type u_1
β : Type ?u.331102
γ : Type ?u.331105
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a x : α
⊢ x ∈ filter p {a} ↔ x ∈ if p a then {a} else ∅
α : Type u_1
β : Type ?u.331102
γ : Type ?u.331105
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
⊢ filter p {a} = if p a then {a} else ∅
ext x
case a
α : Type u_1
β : Type ?u.331102
γ : Type ?u.331105
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a x : α
⊢ x = a ∧ p x ↔ x ∈ if p a then {a} else ∅
case a
α : Type u_1
β : Type ?u.331102
γ : Type ?u.331105
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a x : α
⊢ x ∈ filter p {a} ↔ x ∈ if p a then {a} else ∅
simp
no goals
case a
α : Type u_1
β : Type ?u.331102
γ : Type ?u.331105
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a x : α
⊢ x = a ∧ p x ↔ x ∈ if p a then {a} else ∅
split_ifs with h <;> by_cases h' : x = a <;> simp [h, h']