Theorem: singletonCompleteness (Pdl/Completeness.lean)

State before:
⊢ ∀ (φ : Formula), consistent ([φ], [], none) ↔ satisfiable φ
Tactic:
intro φ
State after:
φ : Formula
⊢ consistent ([φ], [], none) ↔ satisfiable φ

State before:
φ : Formula
⊢ consistent ([φ], [], none) ↔ satisfiable φ
Tactic:
have := completeness ⟨[φ], [], none⟩
State after:
φ : Formula
this : consistent ([φ], [], none) ↔ satisfiable ([φ], [], none)
⊢ consistent ([φ], [], none) ↔ satisfiable φ

State before:
φ : Formula
this : consistent ([φ], [], none) ↔ satisfiable ([φ], [], none)
⊢ consistent ([φ], [], none) ↔ satisfiable φ
Tactic:
simp [this,tNodeHasSat,modelCanSemImplyTNode]
State after:
no goals