Theorem: truthImply_then_satImply (Pdl/Semantics.lean)

State before:
X Y : List Formula
⊢ X⊨Y → satisfiable X → satisfiable Y
Tactic:
intro X_Y
State after:
X Y : List Formula
X_Y : X⊨Y
⊢ satisfiable X → satisfiable Y

State before:
X Y : List Formula
X_Y : X⊨Y
⊢ satisfiable X → satisfiable Y
Tactic:
intro satX
State after:
X Y : List Formula
X_Y : X⊨Y
satX : satisfiable X
⊢ satisfiable Y

State before:
X Y : List Formula
X_Y : X⊨Y
satX : satisfiable X
⊢ satisfiable Y
Tactic:
rcases satX with ⟨W,M,w,v_X⟩
State after:
case intro.intro.intro
X Y : List Formula
X_Y : X⊨Y
W : Type
M : KripkeModel W
w : W
v_X : ∀ φ ∈ X, evaluate M w φ
⊢ satisfiable Y

State before:
case intro.intro.intro
X Y : List Formula
X_Y : X⊨Y
W : Type
M : KripkeModel W
w : W
v_X : ∀ φ ∈ X, evaluate M w φ
⊢ satisfiable Y
Tactic:
specialize X_Y W M w v_X
State after:
case intro.intro.intro
X Y : List Formula
W : Type
M : KripkeModel W
w : W
v_X : ∀ φ ∈ X, evaluate M w φ
X_Y : ∀ ψ ∈ Y, evaluate M w ψ
⊢ satisfiable Y

State before:
case intro.intro.intro
X Y : List Formula
W : Type
M : KripkeModel W
w : W
v_X : ∀ φ ∈ X, evaluate M w φ
X_Y : ∀ ψ ∈ Y, evaluate M w ψ
⊢ satisfiable Y
Tactic:
use W, M, w
State after:
no goals