Theorem: LO.Propositional.Superintuitionistic.notClassicalValid_of_exists_ClassicalValuation (Logic/Propositional/Superintuitionistic/Kripke/Classical.lean)

State before:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
⊢ (∃ V, ¬V ⊧ p) → ¬𝔽(Ax(𝐂𝐥)) ⊧ p
Tactic:
contrapose
State after:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
⊢ ¬¬𝔽(Ax(𝐂𝐥)) ⊧ p → ¬∃ V, ¬V ⊧ p

State before:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
⊢ ¬¬𝔽(Ax(𝐂𝐥)) ⊧ p → ¬∃ V, ¬V ⊧ p
Tactic:
push_neg
State after:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
⊢ 𝔽(Ax(𝐂𝐥)) ⊧ p → ∀ (V : ClassicalValuation α), V ⊧ p

State before:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
⊢ 𝔽(Ax(𝐂𝐥)) ⊧ p → ∀ (V : ClassicalValuation α), V ⊧ p
Tactic:
apply Formula.Kripke.ValidOnClassicalFrame_iff
State after:
no goals