rcases M_prop with ⟨i, ii, iii, iv⟩
case mk
Worlds : Set (Finset Formula)
X : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
M_prop :
  (∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X) ∧
    (fun M => ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp) M ∧
      (fun M => ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y) M ∧
        (fun M => ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y) M
⊢ P ∈ ↑X → Evaluate (↑⟨M, M_prop⟩, X) P
case mk.intro.intro.intro
Worlds : Set (Finset Formula)
X : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
⊢ P ∈ ↑X → Evaluate (↑⟨M, ⋯⟩, X) P