Theorem: soundness (Pdl/Soundness.lean)

State before:
⊢ ∀ (φ : Formula), provable φ → tautology φ
Tactic:
intro φ prov
State after:
φ : Formula
prov : provable φ
⊢ tautology φ

State before:
φ : Formula
prov : provable φ
⊢ tautology φ
Tactic:
apply notsatisfnotThenTaut
State after:
case a
φ : Formula
prov : provable φ
⊢ ¬satisfiable (~φ)

State before:
case a
φ : Formula
prov : provable φ
⊢ ¬satisfiable (~φ)
Tactic:
rw [← singletonSat_iff_sat]
State after:
case a
φ : Formula
prov : provable φ
⊢ ¬satisfiable {~φ}

State before:
case a
φ : Formula
prov : provable φ
⊢ ¬satisfiable {~φ}
Tactic:
apply soundTableau
State after:
case a.a
φ : Formula
prov : provable φ
⊢ provable φ

State before:
case a.a
φ : Formula
prov : provable φ
⊢ provable φ
Tactic:
exact prov
State after:
no goals