Theorem: loadedTruthLemma (Pdl/Modelgraphs.lean)

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
⊢ ∀ (P : Formula), (P ∈ ↑X → evaluate (↑MG) X P) ∧ ((~P) ∈ ↑X → ¬evaluate (↑MG) X P)
Tactic:
intro P
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P : Formula
⊢ (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
⊢ (P ∈ ↑X → evaluate (↑MG) X P) ∧ ((~P) ∈ ↑X → ¬evaluate (↑MG) X P)
Tactic:
cases P
State after:
case bottom
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
⊢ (bottom ∈ ↑X → evaluate (↑MG) X bottom) ∧ ((~bottom) ∈ ↑X → ¬evaluate (↑MG) X bottom)

case atom_prop
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a✝ : ℕ
⊢ ((·a✝) ∈ ↑X → evaluate (↑MG) X (·a✝)) ∧ ((~·a✝) ∈ ↑X → ¬evaluate (↑MG) X (·a✝))

case neg
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a✝ : Formula
⊢ ((~a✝) ∈ ↑X → evaluate (↑MG) X (~a✝)) ∧ ((~~a✝) ∈ ↑X → ¬evaluate (↑MG) X (~a✝))

case and
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a✝¹ a✝ : Formula
⊢ (a✝¹⋀a✝ ∈ ↑X → evaluate (↑MG) X (a✝¹⋀a✝)) ∧ ((~a✝¹⋀a✝) ∈ ↑X → ¬evaluate (↑MG) X (a✝¹⋀a✝))

case box
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a✝¹ : Program
a✝ : Formula
⊢ ((⌈a✝¹⌉a✝) ∈ ↑X → evaluate (↑MG) X (⌈a✝¹⌉a✝)) ∧ ((~⌈a✝¹⌉a✝) ∈ ↑X → ¬evaluate (↑MG) X (⌈a✝¹⌉a✝))

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
⊢ (bottom ∈ ↑X → evaluate (↑MG) X bottom) ∧ ((~bottom) ∈ ↑X → ¬evaluate (↑MG) X bottom)
Tactic:
repeat' constructor
State after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
⊢ bottom ∈ ↑X → evaluate (↑MG) X bottom

case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
⊢ (~bottom) ∈ ↑X → ¬evaluate (↑MG) X bottom

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
⊢ (bottom ∈ ↑X → evaluate (↑MG) X bottom) ∧ ((~bottom) ∈ ↑X → ¬evaluate (↑MG) X bottom)
Tactic:
constructor
State after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
⊢ bottom ∈ ↑X → evaluate (↑MG) X bottom

case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
⊢ (~bottom) ∈ ↑X → ¬evaluate (↑MG) X bottom

State before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
⊢ bottom ∈ ↑X → evaluate (↑MG) X bottom
Tactic:
intro P_in_X
State after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P_in_X : bottom ∈ ↑X
⊢ evaluate (↑MG) X bottom

State before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P_in_X : bottom ∈ ↑X
⊢ evaluate (↑MG) X bottom
Tactic:
apply absurd P_in_X
State after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P_in_X : bottom ∈ ↑X
⊢ bottom ∉ ↑X

State before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P_in_X : bottom ∈ ↑X
⊢ bottom ∉ ↑X
Tactic:
have ⟨_,⟨i,_,_,_⟩⟩ := MG
State after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P_in_X : bottom ∈ ↑X
val✝ : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝¹ : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) val✝
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) val✝
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) val✝
⊢ bottom ∉ ↑X

State before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P_in_X : bottom ∈ ↑X
val✝ : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝¹ : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) val✝
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) val✝
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) val✝
⊢ bottom ∉ ↑X
Tactic:
specialize i X
State after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P_in_X : bottom ∈ ↑X
val✝ : KripkeModel { x // x ∈ Worlds }
left✝¹ : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) val✝
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) val✝
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) val✝
i : saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
⊢ bottom ∉ ↑X

State before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P_in_X : bottom ∈ ↑X
val✝ : KripkeModel { x // x ∈ Worlds }
left✝¹ : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) val✝
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) val✝
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) val✝
i : saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
⊢ bottom ∉ ↑X
Tactic:
tauto
State after:
no goals

State before:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
⊢ (~bottom) ∈ ↑X → ¬evaluate (↑MG) X bottom
Tactic:
simp only [instBot, evaluate, not_false_eq_true, implies_true]
State after:
no goals

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
⊢ ((·pp) ∈ ↑X → evaluate (↑MG) X (·pp)) ∧ ((~·pp) ∈ ↑X → ¬evaluate (↑MG) X (·pp))
Tactic:
have ⟨M,⟨i,ii,_,_⟩⟩ := MG
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
⊢ ((·pp) ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X (·pp)) ∧ ((~·pp) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X (·pp))

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
⊢ ((·pp) ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X (·pp)) ∧ ((~·pp) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X (·pp))
Tactic:
repeat' constructor
State after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
⊢ (·pp) ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X (·pp)

case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
⊢ (~·pp) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X (·pp)

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
⊢ ((·pp) ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X (·pp)) ∧ ((~·pp) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X (·pp))
Tactic:
constructor
State after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
⊢ (·pp) ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X (·pp)

case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
⊢ (~·pp) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X (·pp)

State before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
⊢ (·pp) ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X (·pp)
Tactic:
intro P_in_X
State after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
P_in_X : (·pp) ∈ ↑X
⊢ evaluate (↑⟨M, ⋯⟩) X (·pp)

State before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
P_in_X : (·pp) ∈ ↑X
⊢ evaluate (↑⟨M, ⋯⟩) X (·pp)
Tactic:
simp only [evaluate]
State after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
P_in_X : (·pp) ∈ ↑X
⊢ M.val X pp

State before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
P_in_X : (·pp) ∈ ↑X
⊢ M.val X pp
Tactic:
rw [ii X pp] at P_in_X
State after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
P_in_X : M.val X pp
⊢ M.val X pp

State before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
P_in_X : M.val X pp
⊢ M.val X pp
Tactic:
exact P_in_X
State after:
no goals

State before:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
⊢ (~·pp) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X (·pp)
Tactic:
intro notP_in_X
State after:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
notP_in_X : (~·pp) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X (·pp)

State before:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
notP_in_X : (~·pp) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X (·pp)
Tactic:
simp only [evaluate]
State after:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
notP_in_X : (~·pp) ∈ ↑X
⊢ ¬M.val X pp

State before:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
notP_in_X : (~·pp) ∈ ↑X
⊢ ¬M.val X pp
Tactic:
rw [← ii X pp]
State after:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
notP_in_X : (~·pp) ∈ ↑X
⊢ (·pp) ∉ ↑X

State before:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
notP_in_X : (~·pp) ∈ ↑X
⊢ (·pp) ∉ ↑X
Tactic:
rcases i X with ⟨_, _, P_in_then_notP_not_in⟩
State after:
case right.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
left✝² : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
notP_in_X : (~·pp) ∈ ↑X
left✝¹ : saturated ↑X
left✝ : ⊥ ∉ ↑X
P_in_then_notP_not_in : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
⊢ (·pp) ∉ ↑X

State before:
case right.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
left✝² : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
notP_in_X : (~·pp) ∈ ↑X
left✝¹ : saturated ↑X
left✝ : ⊥ ∉ ↑X
P_in_then_notP_not_in : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
⊢ (·pp) ∉ ↑X
Tactic:
specialize P_in_then_notP_not_in pp
State after:
case right.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
left✝² : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
notP_in_X : (~·pp) ∈ ↑X
left✝¹ : saturated ↑X
left✝ : ⊥ ∉ ↑X
P_in_then_notP_not_in : (·pp) ∈ ↑X → (~·pp) ∉ ↑X
⊢ (·pp) ∉ ↑X

State before:
case right.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
pp : ℕ
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
left✝² : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
notP_in_X : (~·pp) ∈ ↑X
left✝¹ : saturated ↑X
left✝ : ⊥ ∉ ↑X
P_in_then_notP_not_in : (·pp) ∈ ↑X → (~·pp) ∉ ↑X
⊢ (·pp) ∉ ↑X
Tactic:
tauto
State after:
no goals

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
⊢ ((~Q) ∈ ↑X → evaluate (↑MG) X (~Q)) ∧ ((~~Q) ∈ ↑X → ¬evaluate (↑MG) X (~Q))
Tactic:
have ⟨plus,minus⟩ := loadedTruthLemma MG X Q
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
⊢ ((~Q) ∈ ↑X → evaluate (↑MG) X (~Q)) ∧ ((~~Q) ∈ ↑X → ¬evaluate (↑MG) X (~Q))

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
⊢ ((~Q) ∈ ↑X → evaluate (↑MG) X (~Q)) ∧ ((~~Q) ∈ ↑X → ¬evaluate (↑MG) X (~Q))
Tactic:
repeat' constructor
State after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
⊢ (~Q) ∈ ↑X → evaluate (↑MG) X (~Q)

case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
⊢ (~~Q) ∈ ↑X → ¬evaluate (↑MG) X (~Q)

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
⊢ ((~Q) ∈ ↑X → evaluate (↑MG) X (~Q)) ∧ ((~~Q) ∈ ↑X → ¬evaluate (↑MG) X (~Q))
Tactic:
constructor
State after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
⊢ (~Q) ∈ ↑X → evaluate (↑MG) X (~Q)

case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
⊢ (~~Q) ∈ ↑X → ¬evaluate (↑MG) X (~Q)

State before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
⊢ (~Q) ∈ ↑X → evaluate (↑MG) X (~Q)
Tactic:
intro notQ_in_X
State after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
notQ_in_X : (~Q) ∈ ↑X
⊢ evaluate (↑MG) X (~Q)

State before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
notQ_in_X : (~Q) ∈ ↑X
⊢ evaluate (↑MG) X (~Q)
Tactic:
simp only [evaluate]
State after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
notQ_in_X : (~Q) ∈ ↑X
⊢ ¬evaluate (↑MG) X Q

State before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
notQ_in_X : (~Q) ∈ ↑X
⊢ ¬evaluate (↑MG) X Q
Tactic:
exact minus notQ_in_X
State after:
no goals

State before:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
⊢ (~~Q) ∈ ↑X → ¬evaluate (↑MG) X (~Q)
Tactic:
intro notnotQ_in_X
State after:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
notnotQ_in_X : (~~Q) ∈ ↑X
⊢ ¬evaluate (↑MG) X (~Q)

State before:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
notnotQ_in_X : (~~Q) ∈ ↑X
⊢ ¬evaluate (↑MG) X (~Q)
Tactic:
simp only [instBot, evaluate, not_not]
State after:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
notnotQ_in_X : (~~Q) ∈ ↑X
⊢ evaluate (↑MG) X Q

State before:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
plus : Q ∈ ↑X → evaluate (↑MG) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
notnotQ_in_X : (~~Q) ∈ ↑X
⊢ evaluate (↑MG) X Q
Tactic:
have ⟨M,⟨i,_,_,_⟩⟩ := MG
State after:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
notnotQ_in_X : (~~Q) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝¹ : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
left✝ : ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y
right✝ : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
⊢ evaluate (↑⟨M, ⋯⟩) X Q

State before:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
notnotQ_in_X : (~~Q) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝¹ : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
left✝ : ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y
right✝ : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
⊢ evaluate (↑⟨M, ⋯⟩) X Q
Tactic:
rcases i X with ⟨X_saturated, _, _⟩
State after:
case right.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
notnotQ_in_X : (~~Q) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
left✝¹ : ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y
right✝¹ : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
X_saturated : saturated ↑X
left✝ : ⊥ ∉ ↑X
right✝ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
⊢ evaluate (↑⟨M, ⋯⟩) X Q

State before:
case right.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
notnotQ_in_X : (~~Q) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
left✝¹ : ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y
right✝¹ : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
X_saturated : saturated ↑X
left✝ : ⊥ ∉ ↑X
right✝ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
⊢ evaluate (↑⟨M, ⋯⟩) X Q
Tactic:
exact plus ((X_saturated Q Q (?'Q)).1 notnotQ_in_X)
State after:
no goals

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
⊢ (Q⋀R ∈ ↑X → evaluate (↑MG) X (Q⋀R)) ∧ ((~Q⋀R) ∈ ↑X → ¬evaluate (↑MG) X (Q⋀R))
Tactic:
have ⟨plus_Q, minus_Q⟩ := loadedTruthLemma MG X Q
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
plus_Q : Q ∈ ↑X → evaluate (↑MG) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
⊢ (Q⋀R ∈ ↑X → evaluate (↑MG) X (Q⋀R)) ∧ ((~Q⋀R) ∈ ↑X → ¬evaluate (↑MG) X (Q⋀R))

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
plus_Q : Q ∈ ↑X → evaluate (↑MG) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
⊢ (Q⋀R ∈ ↑X → evaluate (↑MG) X (Q⋀R)) ∧ ((~Q⋀R) ∈ ↑X → ¬evaluate (↑MG) X (Q⋀R))
Tactic:
have ⟨plus_R, minus_R⟩ := loadedTruthLemma MG X R
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
plus_Q : Q ∈ ↑X → evaluate (↑MG) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
plus_R : R ∈ ↑X → evaluate (↑MG) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑MG) X R
⊢ (Q⋀R ∈ ↑X → evaluate (↑MG) X (Q⋀R)) ∧ ((~Q⋀R) ∈ ↑X → ¬evaluate (↑MG) X (Q⋀R))

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
plus_Q : Q ∈ ↑X → evaluate (↑MG) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑MG) X Q
plus_R : R ∈ ↑X → evaluate (↑MG) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑MG) X R
⊢ (Q⋀R ∈ ↑X → evaluate (↑MG) X (Q⋀R)) ∧ ((~Q⋀R) ∈ ↑X → ¬evaluate (↑MG) X (Q⋀R))
Tactic:
have ⟨M,⟨i,_,iii,_⟩⟩ := MG
State after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
⊢ (Q⋀R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X (Q⋀R)) ∧ ((~Q⋀R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X (Q⋀R))

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝ : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
⊢ (Q⋀R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X (Q⋀R)) ∧ ((~Q⋀R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X (Q⋀R))
Tactic:
rcases i X with ⟨X_saturated, _, _⟩
State after:
case intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝¹ : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝¹ : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝ : ⊥ ∉ ↑X
right✝ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
⊢ (Q⋀R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X (Q⋀R)) ∧ ((~Q⋀R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X (Q⋀R))

State before:
case intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝¹ : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝¹ : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝ : ⊥ ∉ ↑X
right✝ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
⊢ (Q⋀R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X (Q⋀R)) ∧ ((~Q⋀R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X (Q⋀R))
Tactic:
rcases X_saturated Q R (?'Q) with ⟨_, ⟨andSplit, ⟨notAndSplit, _⟩⟩⟩
State after:
case intro.intro.intro.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
⊢ (Q⋀R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X (Q⋀R)) ∧ ((~Q⋀R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X (Q⋀R))

State before:
case intro.intro.intro.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
⊢ (Q⋀R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X (Q⋀R)) ∧ ((~Q⋀R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X (Q⋀R))
Tactic:
repeat' constructor
State after:
case intro.intro.intro.intro.intro.left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
⊢ Q⋀R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X (Q⋀R)

case intro.intro.intro.intro.intro.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
⊢ (~Q⋀R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X (Q⋀R)

State before:
case intro.intro.intro.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
⊢ (Q⋀R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X (Q⋀R)) ∧ ((~Q⋀R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X (Q⋀R))
Tactic:
constructor
State after:
case intro.intro.intro.intro.intro.left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
⊢ Q⋀R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X (Q⋀R)

case intro.intro.intro.intro.intro.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
⊢ (~Q⋀R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X (Q⋀R)

State before:
case intro.intro.intro.intro.intro.left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
⊢ Q⋀R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X (Q⋀R)
Tactic:
intro QandR_in_X
State after:
case intro.intro.intro.intro.intro.left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
QandR_in_X : Q⋀R ∈ ↑X
⊢ evaluate (↑⟨M, ⋯⟩) X (Q⋀R)

State before:
case intro.intro.intro.intro.intro.left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
QandR_in_X : Q⋀R ∈ ↑X
⊢ evaluate (↑⟨M, ⋯⟩) X (Q⋀R)
Tactic:
specialize andSplit QandR_in_X
State after:
case intro.intro.intro.intro.intro.left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
QandR_in_X : Q⋀R ∈ ↑X
andSplit : Q ∈ ↑X ∧ R ∈ ↑X
⊢ evaluate (↑⟨M, ⋯⟩) X (Q⋀R)

State before:
case intro.intro.intro.intro.intro.left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
QandR_in_X : Q⋀R ∈ ↑X
andSplit : Q ∈ ↑X ∧ R ∈ ↑X
⊢ evaluate (↑⟨M, ⋯⟩) X (Q⋀R)
Tactic:
cases' andSplit with Q_in_X R_in_X
State after:
case intro.intro.intro.intro.intro.left.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
QandR_in_X : Q⋀R ∈ ↑X
Q_in_X : Q ∈ ↑X
R_in_X : R ∈ ↑X
⊢ evaluate (↑⟨M, ⋯⟩) X (Q⋀R)

State before:
case intro.intro.intro.intro.intro.left.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
QandR_in_X : Q⋀R ∈ ↑X
Q_in_X : Q ∈ ↑X
R_in_X : R ∈ ↑X
⊢ evaluate (↑⟨M, ⋯⟩) X (Q⋀R)
Tactic:
simp only [evaluate]
State after:
case intro.intro.intro.intro.intro.left.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
QandR_in_X : Q⋀R ∈ ↑X
Q_in_X : Q ∈ ↑X
R_in_X : R ∈ ↑X
⊢ evaluate M X Q ∧ evaluate M X R

State before:
case intro.intro.intro.intro.intro.left.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
QandR_in_X : Q⋀R ∈ ↑X
Q_in_X : Q ∈ ↑X
R_in_X : R ∈ ↑X
⊢ evaluate M X Q ∧ evaluate M X R
Tactic:
constructor
State after:
case intro.intro.intro.intro.intro.left.intro.left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
QandR_in_X : Q⋀R ∈ ↑X
Q_in_X : Q ∈ ↑X
R_in_X : R ∈ ↑X
⊢ evaluate M X Q

case intro.intro.intro.intro.intro.left.intro.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
QandR_in_X : Q⋀R ∈ ↑X
Q_in_X : Q ∈ ↑X
R_in_X : R ∈ ↑X
⊢ evaluate M X R

State before:
case intro.intro.intro.intro.intro.left.intro.left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
QandR_in_X : Q⋀R ∈ ↑X
Q_in_X : Q ∈ ↑X
R_in_X : R ∈ ↑X
⊢ evaluate M X Q
Tactic:
exact plus_Q Q_in_X
State after:
no goals

State before:
case intro.intro.intro.intro.intro.left.intro.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
QandR_in_X : Q⋀R ∈ ↑X
Q_in_X : Q ∈ ↑X
R_in_X : R ∈ ↑X
⊢ evaluate M X R
Tactic:
exact plus_R R_in_X
State after:
no goals

State before:
case intro.intro.intro.intro.intro.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
⊢ (~Q⋀R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X (Q⋀R)
Tactic:
intro notQandR_in_X
State after:
case intro.intro.intro.intro.intro.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X (Q⋀R)

State before:
case intro.intro.intro.intro.intro.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X (Q⋀R)
Tactic:
unfold evaluate
State after:
case intro.intro.intro.intro.intro.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
⊢ ¬(evaluate (↑⟨M, ⋯⟩) X Q ∧ evaluate (↑⟨M, ⋯⟩) X R)

State before:
case intro.intro.intro.intro.intro.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
⊢ ¬(evaluate (↑⟨M, ⋯⟩) X Q ∧ evaluate (↑⟨M, ⋯⟩) X R)
Tactic:
rw [not_and_or]
State after:
case intro.intro.intro.intro.intro.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X Q ∨ ¬evaluate (↑⟨M, ⋯⟩) X R

State before:
case intro.intro.intro.intro.intro.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X Q ∨ ¬evaluate (↑⟨M, ⋯⟩) X R
Tactic:
specialize notAndSplit notQandR_in_X
State after:
case intro.intro.intro.intro.intro.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
notAndSplit : (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X Q ∨ ¬evaluate (↑⟨M, ⋯⟩) X R

State before:
case intro.intro.intro.intro.intro.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
notAndSplit : (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X Q ∨ ¬evaluate (↑⟨M, ⋯⟩) X R
Tactic:
cases' notAndSplit with notQ_in_X notR_in_X
State after:
case intro.intro.intro.intro.intro.right.inl
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
notQ_in_X : (~Q) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X Q ∨ ¬evaluate (↑⟨M, ⋯⟩) X R

case intro.intro.intro.intro.intro.right.inr
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
notR_in_X : (~R) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X Q ∨ ¬evaluate (↑⟨M, ⋯⟩) X R

State before:
case intro.intro.intro.intro.intro.right.inl
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
notQ_in_X : (~Q) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X Q ∨ ¬evaluate (↑⟨M, ⋯⟩) X R
Tactic:
left
State after:
case intro.intro.intro.intro.intro.right.inl.h
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
notQ_in_X : (~Q) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X Q

State before:
case intro.intro.intro.intro.intro.right.inl.h
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
notQ_in_X : (~Q) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X Q
Tactic:
exact minus_Q notQ_in_X
State after:
no goals

State before:
case intro.intro.intro.intro.intro.right.inr
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
notR_in_X : (~R) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X Q ∨ ¬evaluate (↑⟨M, ⋯⟩) X R
Tactic:
right
State after:
case intro.intro.intro.intro.intro.right.inr.h
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
notR_in_X : (~R) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X R

State before:
case intro.intro.intro.intro.intro.right.inr.h
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
notR_in_X : (~R) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X R
Tactic:
exact minus_R notR_in_X
State after:
no goals

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ ((⌈a⌉P) ∈ ↑X → evaluate (↑MG) X (⌈a⌉P)) ∧ ((~⌈a⌉P) ∈ ↑X → ¬evaluate (↑MG) X (⌈a⌉P))
Tactic:
repeat' constructor
State after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ (⌈a⌉P) ∈ ↑X → evaluate (↑MG) X (⌈a⌉P)

case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ (~⌈a⌉P) ∈ ↑X → ¬evaluate (↑MG) X (⌈a⌉P)

State before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ (⌈a⌉P) ∈ ↑X → evaluate (↑MG) X (⌈a⌉P)

case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ (~⌈a⌉P) ∈ ↑X → ¬evaluate (↑MG) X (⌈a⌉P)
Tactic:
all_goals simp
State after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ (⌈a⌉P) ∈ ↑X → ∀ (a_2 : Finset Formula) (b : a_2 ∈ Worlds), relate (↑MG) a X ⟨a_2, b⟩ → evaluate ↑MG ⟨a_2, b⟩ P

case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ (~⌈a⌉P) ∈ ↑X → ∃ x, ∃ (h : x ∈ Worlds), relate (↑MG) a X ⟨x, ⋯⟩ ∧ ¬evaluate ↑MG ⟨x, ⋯⟩ P

State before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ ((⌈a⌉P) ∈ ↑X → evaluate (↑MG) X (⌈a⌉P)) ∧ ((~⌈a⌉P) ∈ ↑X → ¬evaluate (↑MG) X (⌈a⌉P))
Tactic:
constructor
State after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ (⌈a⌉P) ∈ ↑X → evaluate (↑MG) X (⌈a⌉P)

case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ (~⌈a⌉P) ∈ ↑X → ¬evaluate (↑MG) X (⌈a⌉P)

State before:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ (~⌈a⌉P) ∈ ↑X → ¬evaluate (↑MG) X (⌈a⌉P)
Tactic:
simp
State after:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ (~⌈a⌉P) ∈ ↑X → ∃ x, ∃ (h : x ∈ Worlds), relate (↑MG) a X ⟨x, ⋯⟩ ∧ ¬evaluate ↑MG ⟨x, ⋯⟩ P

State before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ (⌈a⌉P) ∈ ↑X → ∀ (a_2 : Finset Formula) (b : a_2 ∈ Worlds), relate (↑MG) a X ⟨a_2, b⟩ → evaluate ↑MG ⟨a_2, b⟩ P
Tactic:
intro boxP_in_X
State after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
boxP_in_X : (⌈a⌉P) ∈ ↑X
⊢ ∀ (a_1 : Finset Formula) (b : a_1 ∈ Worlds), relate (↑MG) a X ⟨a_1, b⟩ → evaluate ↑MG ⟨a_1, b⟩ P

State before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
boxP_in_X : (⌈a⌉P) ∈ ↑X
⊢ ∀ (a_1 : Finset Formula) (b : a_1 ∈ Worlds), relate (↑MG) a X ⟨a_1, b⟩ → evaluate ↑MG ⟨a_1, b⟩ P
Tactic:
intro Y Y_in X_rel_Y
State after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
boxP_in_X : (⌈a⌉P) ∈ ↑X
Y : Finset Formula
Y_in : Y ∈ Worlds
X_rel_Y : relate (↑MG) a X ⟨Y, Y_in⟩
⊢ evaluate ↑MG ⟨Y, Y_in⟩ P

State before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
boxP_in_X : (⌈a⌉P) ∈ ↑X
Y : Finset Formula
Y_in : Y ∈ Worlds
X_rel_Y : relate (↑MG) a X ⟨Y, Y_in⟩
⊢ evaluate ↑MG ⟨Y, Y_in⟩ P
Tactic:
have ⟨plus_Y, _⟩ := loadedTruthLemma MG ⟨Y, Y_in⟩ P
State after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
boxP_in_X : (⌈a⌉P) ∈ ↑X
Y : Finset Formula
Y_in : Y ∈ Worlds
X_rel_Y : relate (↑MG) a X ⟨Y, Y_in⟩
plus_Y : P ∈ ↑⟨Y, Y_in⟩ → evaluate ↑MG ⟨Y, Y_in⟩ P
right✝ : (~P) ∈ ↑⟨Y, Y_in⟩ → ¬evaluate ↑MG ⟨Y, Y_in⟩ P
⊢ evaluate ↑MG ⟨Y, Y_in⟩ P

State before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
boxP_in_X : (⌈a⌉P) ∈ ↑X
Y : Finset Formula
Y_in : Y ∈ Worlds
X_rel_Y : relate (↑MG) a X ⟨Y, Y_in⟩
plus_Y : P ∈ ↑⟨Y, Y_in⟩ → evaluate ↑MG ⟨Y, Y_in⟩ P
right✝ : (~P) ∈ ↑⟨Y, Y_in⟩ → ¬evaluate ↑MG ⟨Y, Y_in⟩ P
⊢ evaluate ↑MG ⟨Y, Y_in⟩ P
Tactic:
have oh_a := loadedTruthLemmaProg MG a X
State after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
boxP_in_X : (⌈a⌉P) ∈ ↑X
Y : Finset Formula
Y_in : Y ∈ Worlds
X_rel_Y : relate (↑MG) a X ⟨Y, Y_in⟩
plus_Y : P ∈ ↑⟨Y, Y_in⟩ → evaluate ↑MG ⟨Y, Y_in⟩ P
right✝ : (~P) ∈ ↑⟨Y, Y_in⟩ → ¬evaluate ↑MG ⟨Y, Y_in⟩ P
oh_a : ∀ (φ : Formula), (⌈a⌉φ) ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), relate (↑MG) a X Y → φ ∈ ↑Y
⊢ evaluate ↑MG ⟨Y, Y_in⟩ P

State before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
boxP_in_X : (⌈a⌉P) ∈ ↑X
Y : Finset Formula
Y_in : Y ∈ Worlds
X_rel_Y : relate (↑MG) a X ⟨Y, Y_in⟩
plus_Y : P ∈ ↑⟨Y, Y_in⟩ → evaluate ↑MG ⟨Y, Y_in⟩ P
right✝ : (~P) ∈ ↑⟨Y, Y_in⟩ → ¬evaluate ↑MG ⟨Y, Y_in⟩ P
oh_a : ∀ (φ : Formula), (⌈a⌉φ) ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), relate (↑MG) a X Y → φ ∈ ↑Y
⊢ evaluate ↑MG ⟨Y, Y_in⟩ P
Tactic:
apply plus_Y
State after:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
boxP_in_X : (⌈a⌉P) ∈ ↑X
Y : Finset Formula
Y_in : Y ∈ Worlds
X_rel_Y : relate (↑MG) a X ⟨Y, Y_in⟩
plus_Y : P ∈ ↑⟨Y, Y_in⟩ → evaluate ↑MG ⟨Y, Y_in⟩ P
right✝ : (~P) ∈ ↑⟨Y, Y_in⟩ → ¬evaluate ↑MG ⟨Y, Y_in⟩ P
oh_a : ∀ (φ : Formula), (⌈a⌉φ) ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), relate (↑MG) a X Y → φ ∈ ↑Y
⊢ P ∈ ↑⟨Y, Y_in⟩

State before:
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
boxP_in_X : (⌈a⌉P) ∈ ↑X
Y : Finset Formula
Y_in : Y ∈ Worlds
X_rel_Y : relate (↑MG) a X ⟨Y, Y_in⟩
plus_Y : P ∈ ↑⟨Y, Y_in⟩ → evaluate ↑MG ⟨Y, Y_in⟩ P
right✝ : (~P) ∈ ↑⟨Y, Y_in⟩ → ¬evaluate ↑MG ⟨Y, Y_in⟩ P
oh_a : ∀ (φ : Formula), (⌈a⌉φ) ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), relate (↑MG) a X Y → φ ∈ ↑Y
⊢ P ∈ ↑⟨Y, Y_in⟩
Tactic:
apply oh_a P boxP_in_X ⟨Y,Y_in⟩ X_rel_Y
State after:
no goals

State before:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ (~⌈a⌉P) ∈ ↑X → ∃ x, ∃ (h : x ∈ Worlds), relate (↑MG) a X ⟨x, ⋯⟩ ∧ ¬evaluate ↑MG ⟨x, ⋯⟩ P
Tactic:
intro notBoxP_in_X
State after:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
⊢ ∃ x, ∃ (h : x ∈ Worlds), relate (↑MG) a X ⟨x, ⋯⟩ ∧ ¬evaluate ↑MG ⟨x, ⋯⟩ P

State before:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
⊢ ∃ x, ∃ (h : x ∈ Worlds), relate (↑MG) a X ⟨x, ⋯⟩ ∧ ¬evaluate ↑MG ⟨x, ⋯⟩ P
Tactic:
have ⟨M,⟨i,ii,iii,iv⟩⟩ := MG
State after:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
⊢ ∃ x, ∃ (h : x ∈ Worlds), relate (↑⟨M, ⋯⟩) a X ⟨x, ⋯⟩ ∧ ¬evaluate ↑⟨M, ⋯⟩ ⟨x, ⋯⟩ P

State before:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
⊢ ∃ x, ∃ (h : x ∈ Worlds), relate (↑⟨M, ⋯⟩) a X ⟨x, ⋯⟩ ∧ ¬evaluate ↑⟨M, ⋯⟩ ⟨x, ⋯⟩ P
Tactic:
have my_iv := iv X a P notBoxP_in_X
State after:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
my_iv : ∃ Y, Q M.Rel a X Y ∧ (~P) ∈ ↑Y
⊢ ∃ x, ∃ (h : x ∈ Worlds), relate (↑⟨M, ⋯⟩) a X ⟨x, ⋯⟩ ∧ ¬evaluate ↑⟨M, ⋯⟩ ⟨x, ⋯⟩ P

State before:
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
my_iv : ∃ Y, Q M.Rel a X Y ∧ (~P) ∈ ↑Y
⊢ ∃ x, ∃ (h : x ∈ Worlds), relate (↑⟨M, ⋯⟩) a X ⟨x, ⋯⟩ ∧ ¬evaluate ↑⟨M, ⋯⟩ ⟨x, ⋯⟩ P
Tactic:
rcases my_iv with ⟨⟨Y, Y_in⟩, X_a_Y, nP_in_Y⟩
State after:
case right.intro.mk.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
Y : Finset Formula
Y_in : Y ∈ Worlds
X_a_Y : Q M.Rel a X ⟨Y, Y_in⟩
nP_in_Y : (~P) ∈ ↑⟨Y, Y_in⟩
⊢ ∃ x, ∃ (h : x ∈ Worlds), relate (↑⟨M, ⋯⟩) a X ⟨x, ⋯⟩ ∧ ¬evaluate ↑⟨M, ⋯⟩ ⟨x, ⋯⟩ P

State before:
case right.intro.mk.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
Y : Finset Formula
Y_in : Y ∈ Worlds
X_a_Y : Q M.Rel a X ⟨Y, Y_in⟩
nP_in_Y : (~P) ∈ ↑⟨Y, Y_in⟩
⊢ ∃ x, ∃ (h : x ∈ Worlds), relate (↑⟨M, ⋯⟩) a X ⟨x, ⋯⟩ ∧ ¬evaluate ↑⟨M, ⋯⟩ ⟨x, ⋯⟩ P
Tactic:
use Y, Y_in
State after:
case h
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
Y : Finset Formula
Y_in : Y ∈ Worlds
X_a_Y : Q M.Rel a X ⟨Y, Y_in⟩
nP_in_Y : (~P) ∈ ↑⟨Y, Y_in⟩
⊢ relate (↑⟨M, ⋯⟩) a X ⟨Y, ⋯⟩ ∧ ¬evaluate ↑⟨M, ⋯⟩ ⟨Y, ⋯⟩ P

State before:
case h
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
Y : Finset Formula
Y_in : Y ∈ Worlds
X_a_Y : Q M.Rel a X ⟨Y, Y_in⟩
nP_in_Y : (~P) ∈ ↑⟨Y, Y_in⟩
⊢ relate (↑⟨M, ⋯⟩) a X ⟨Y, ⋯⟩ ∧ ¬evaluate ↑⟨M, ⋯⟩ ⟨Y, ⋯⟩ P
Tactic:
constructor
State after:
case h.left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
Y : Finset Formula
Y_in : Y ∈ Worlds
X_a_Y : Q M.Rel a X ⟨Y, Y_in⟩
nP_in_Y : (~P) ∈ ↑⟨Y, Y_in⟩
⊢ relate (↑⟨M, ⋯⟩) a X ⟨Y, ⋯⟩

case h.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
Y : Finset Formula
Y_in : Y ∈ Worlds
X_a_Y : Q M.Rel a X ⟨Y, Y_in⟩
nP_in_Y : (~P) ∈ ↑⟨Y, Y_in⟩
⊢ ¬evaluate ↑⟨M, ⋯⟩ ⟨Y, ⋯⟩ P

State before:
case h.left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
Y : Finset Formula
Y_in : Y ∈ Worlds
X_a_Y : Q M.Rel a X ⟨Y, Y_in⟩
nP_in_Y : (~P) ∈ ↑⟨Y, Y_in⟩
⊢ relate (↑⟨M, ⋯⟩) a X ⟨Y, ⋯⟩
Tactic:
exact Q_then_relate ⟨M,⟨i,ii,iii,iv⟩⟩ a X ⟨Y,Y_in⟩ X_a_Y
State after:
no goals

State before:
case h.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
Y : Finset Formula
Y_in : Y ∈ Worlds
X_a_Y : Q M.Rel a X ⟨Y, Y_in⟩
nP_in_Y : (~P) ∈ ↑⟨Y, Y_in⟩
⊢ ¬evaluate ↑⟨M, ⋯⟩ ⟨Y, ⋯⟩ P
Tactic:
have ⟨_, minus_Y⟩ := loadedTruthLemma ⟨M,⟨i,ii,iii,iv⟩⟩ ⟨Y, Y_in⟩ P
State after:
case h.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
Y : Finset Formula
Y_in : Y ∈ Worlds
X_a_Y : Q M.Rel a X ⟨Y, Y_in⟩
nP_in_Y : (~P) ∈ ↑⟨Y, Y_in⟩
left✝ : P ∈ ↑⟨Y, Y_in⟩ → evaluate ↑⟨M, ⋯⟩ ⟨Y, Y_in⟩ P
minus_Y : (~P) ∈ ↑⟨Y, Y_in⟩ → ¬evaluate ↑⟨M, ⋯⟩ ⟨Y, Y_in⟩ P
⊢ ¬evaluate ↑⟨M, ⋯⟩ ⟨Y, ⋯⟩ P

State before:
case h.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
Y : Finset Formula
Y_in : Y ∈ Worlds
X_a_Y : Q M.Rel a X ⟨Y, Y_in⟩
nP_in_Y : (~P) ∈ ↑⟨Y, Y_in⟩
left✝ : P ∈ ↑⟨Y, Y_in⟩ → evaluate ↑⟨M, ⋯⟩ ⟨Y, Y_in⟩ P
minus_Y : (~P) ∈ ↑⟨Y, Y_in⟩ → ¬evaluate ↑⟨M, ⋯⟩ ⟨Y, Y_in⟩ P
⊢ ¬evaluate ↑⟨M, ⋯⟩ ⟨Y, ⋯⟩ P
Tactic:
simp only at minus_Y
State after:
case h.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
Y : Finset Formula
Y_in : Y ∈ Worlds
X_a_Y : Q M.Rel a X ⟨Y, Y_in⟩
nP_in_Y : (~P) ∈ ↑⟨Y, Y_in⟩
left✝ : P ∈ ↑⟨Y, Y_in⟩ → evaluate ↑⟨M, ⋯⟩ ⟨Y, Y_in⟩ P
minus_Y : (~P) ∈ Y → ¬evaluate M ⟨Y, Y_in⟩ P
⊢ ¬evaluate ↑⟨M, ⋯⟩ ⟨Y, ⋯⟩ P

State before:
case h.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
Y : Finset Formula
Y_in : Y ∈ Worlds
X_a_Y : Q M.Rel a X ⟨Y, Y_in⟩
nP_in_Y : (~P) ∈ ↑⟨Y, Y_in⟩
left✝ : P ∈ ↑⟨Y, Y_in⟩ → evaluate ↑⟨M, ⋯⟩ ⟨Y, Y_in⟩ P
minus_Y : (~P) ∈ Y → ¬evaluate M ⟨Y, Y_in⟩ P
⊢ ¬evaluate ↑⟨M, ⋯⟩ ⟨Y, ⋯⟩ P
Tactic:
specialize minus_Y nP_in_Y
State after:
case h.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
Y : Finset Formula
Y_in : Y ∈ Worlds
X_a_Y : Q M.Rel a X ⟨Y, Y_in⟩
nP_in_Y : (~P) ∈ ↑⟨Y, Y_in⟩
left✝ : P ∈ ↑⟨Y, Y_in⟩ → evaluate ↑⟨M, ⋯⟩ ⟨Y, Y_in⟩ P
minus_Y : ¬evaluate M ⟨Y, Y_in⟩ P
⊢ ¬evaluate ↑⟨M, ⋯⟩ ⟨Y, ⋯⟩ P

State before:
case h.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
notBoxP_in_X : (~⌈a⌉P) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) M
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
iv : (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) M
Y : Finset Formula
Y_in : Y ∈ Worlds
X_a_Y : Q M.Rel a X ⟨Y, Y_in⟩
nP_in_Y : (~P) ∈ ↑⟨Y, Y_in⟩
left✝ : P ∈ ↑⟨Y, Y_in⟩ → evaluate ↑⟨M, ⋯⟩ ⟨Y, Y_in⟩ P
minus_Y : ¬evaluate M ⟨Y, Y_in⟩ P
⊢ ¬evaluate ↑⟨M, ⋯⟩ ⟨Y, ⋯⟩ P
Tactic:
convert minus_Y
State after:
no goals