Theorem: truthLemma (Pdl/Modelgraphs.lean)

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
⊢ ∀ (X : { x // x ∈ Worlds }), ∀ P ∈ ↑X, evaluate (↑MG) X P
Tactic:
intro X P
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P : Formula
⊢ P ∈ ↑X → evaluate (↑MG) X P

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P : Formula
⊢ P ∈ ↑X → evaluate (↑MG) X P
Tactic:
have ⟨claim, _⟩ := loadedTruthLemma MG X P
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P : Formula
claim : P ∈ ↑X → evaluate (↑MG) X P
right✝ : (~P) ∈ ↑X → ¬evaluate (↑MG) X P
⊢ P ∈ ↑X → evaluate (↑MG) X P

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P : Formula
claim : P ∈ ↑X → evaluate (↑MG) X P
right✝ : (~P) ∈ ↑X → ¬evaluate (↑MG) X P
⊢ P ∈ ↑X → evaluate (↑MG) X P
Tactic:
exact claim
State after:
no goals