simp only [Semantics.RealizeSet.setOf_iff, ValidOnFrame.models_iff, ValidOnFrame,
  ValidOnModel.iff_models, ValidOnModel, Satisfies.iff_models, forall_exists_index,
  forall_apply_eq_imp_iff, Satisfies.imp_def, Satisfies.box_def, not_forall, exists_prop]
case intro.intro.intro.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₂ : F.World
r₁₂ : F.Rel w₁ w₂
w₃ : F.World
r₂₃ : F.Rel w₂ w₃
nr₁₃ : ¬F.Rel w₁ w₃
⊢ ¬F ⊧* 𝗟
case intro.intro.intro.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₂ : F.World
r₁₂ : F.Rel w₁ w₂
w₃ : F.World
r₂₃ : F.Rel w₂ w₃
nr₁₃ : ¬F.Rel w₁ w₃
⊢ ∃ x x_1 x_2,
    (∀ (w' : F.World),
        x_2 ≺ w' →
          (∀ (w'_1 : F.World), w' ≺ w'_1 → Satisfies { Frame := F, Valuation := x_1 } w'_1 x) →
            Satisfies { Frame := F, Valuation := x_1 } w' x) ∧
      ∃ x_3, x_2 ≺ x_3 ∧ ¬Satisfies { Frame := F, Valuation := x_1 } x_3 x