Theorem: notsatisfnotThenTaut (Pdl/Semantics.lean)

State before:
⊢ ∀ (φ : Formula), ¬satisfiable (~φ) → tautology φ
Tactic:
intro phi
State after:
phi : Formula
⊢ ¬satisfiable (~phi) → tautology phi

State before:
phi : Formula
⊢ ¬satisfiable (~phi) → tautology phi
Tactic:
unfold satisfiable
State after:
phi : Formula
⊢ ¬formHasSat.1 (~phi) → tautology phi

State before:
phi : Formula
⊢ ¬formHasSat.1 (~phi) → tautology phi
Tactic:
unfold tautology
State after:
phi : Formula
⊢ ¬formHasSat.1 (~phi) → ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w phi

State before:
phi : Formula
⊢ ¬formHasSat.1 (~phi) → ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w phi
Tactic:
simp
State after:
no goals