no goals
ι : Sort ?u.15695
α : Sort u_1
κ : ι → Sort ?u.15697
p✝ q : α → Prop
inst✝ : DecidableEq α
a : α
p : α → Prop
⊢ (p a ∧ ∀ (b : α), b ≠ a → p b) ↔ ∀ (b : α), p b
simp only [← @forall_eq _ p a, ← forall_and, ← or_imp, Decidable.em, forall_const]