Theorem: not_forall (SetTheory/Formula.lean)

State before:
V : Type ?u.5314
inst✝ : SetTheory V
α : Sort u_1
p : α → Prop
⊢ (¬∀ (x : α), p x) ↔ ∃ x, ¬p x
Tactic:
constructor
State after:
case mp
V : Type ?u.5314
inst✝ : SetTheory V
α : Sort u_1
p : α → Prop
⊢ (¬∀ (x : α), p x) → ∃ x, ¬p x

case mpr
V : Type ?u.5314
inst✝ : SetTheory V
α : Sort u_1
p : α → Prop
⊢ (∃ x, ¬p x) → ¬∀ (x : α), p x

State before:
case mp
V : Type ?u.5314
inst✝ : SetTheory V
α : Sort u_1
p : α → Prop
⊢ (¬∀ (x : α), p x) → ∃ x, ¬p x
Tactic:
by_contra
State after:
case mp
V : Type ?u.5314
inst✝ : SetTheory V
α : Sort u_1
p : α → Prop
x✝ : ¬((¬∀ (x : α), p x) → ∃ x, ¬p x)
⊢ False

State before:
case mp
V : Type ?u.5314
inst✝ : SetTheory V
α : Sort u_1
p : α → Prop
x✝ : ¬((¬∀ (x : α), p x) → ∃ x, ¬p x)
⊢ False
Tactic:
aesop
State after:
no goals

State before:
case mpr
V : Type ?u.5314
inst✝ : SetTheory V
α : Sort u_1
p : α → Prop
⊢ (∃ x, ¬p x) → ¬∀ (x : α), p x
Tactic:
aesop
State after:
no goals