match h : Finite.all fun x => decide (p x) with
| false =>
  apply decide_eq_false
  match exists_eq_false_of_all_eq_false h with
  | ⟨x, hx⟩ =>
    intro h
    rw [decide_eq_true (h x)] at hx
    contradiction
| true =>
  apply decide_eq_true
  intro x
  apply of_decide_eq_true
  apply forall_eq_true_of_all_eq_true h
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
⊢ decide (∀ (x : α), p x) = Finite.all fun x => decide (p x)
no goals