Theorem: Misc.not_forall (LeanSAT/Util/Misc.lean)

State before:
α : Sort u_1
p : α → Prop
⊢ (¬∀ (x : α), p x) ↔ ∃ x, ¬p x
Tactic:
have em := Classical.propDecidable
State after:
α : Sort u_1
p : α → Prop
em : (a : Prop) → Decidable a
⊢ (¬∀ (x : α), p x) ↔ ∃ x, ¬p x

State before:
α : Sort u_1
p : α → Prop
em : (a : Prop) → Decidable a
⊢ (¬∀ (x : α), p x) ↔ ∃ x, ¬p x
Tactic:
apply Decidable.not_forall
State after:
no goals