Theorem: soundTableau (Pdl/Soundness.lean)

State before:
⊢ ∀ (φ : Formula), provable φ → ¬satisfiable {~φ}
Tactic:
intro φ prov
State after:
φ : Formula
prov : provable φ
⊢ ¬satisfiable {~φ}

State before:
φ : Formula
prov : provable φ
⊢ ¬satisfiable {~φ}
Tactic:
rcases prov with ⟨tabl⟩|⟨tabl⟩
State after:
case byTableauL
φ : Formula
tabl : ClosedTableau ([], []) ([~φ], [], none)
⊢ ¬satisfiable {~φ}

case byTableauR
φ : Formula
tabl : ClosedTableau ([], []) ([], [~φ], none)
⊢ ¬satisfiable {~φ}

State before:
case byTableauL
φ : Formula
tabl : ClosedTableau ([], []) ([~φ], [], none)
⊢ ¬satisfiable {~φ}

case byTableauR
φ : Formula
tabl : ClosedTableau ([], []) ([], [~φ], none)
⊢ ¬satisfiable {~φ}
Tactic:
exact tableauThenNotSat ([~φ], [], none) tabl
State after:
case byTableauR
φ : Formula
tabl : ClosedTableau ([], []) ([], [~φ], none)
⊢ ¬satisfiable {~φ}

State before:
case byTableauR
φ : Formula
tabl : ClosedTableau ([], []) ([], [~φ], none)
⊢ ¬satisfiable {~φ}
Tactic:
exact tableauThenNotSat ([], [~φ], none) tabl
State after:
no goals