Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_cwf (Logic/Modal/Standard/Kripke/GL/Definability.lean)

State before:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
⊢ F ⊧* 𝗟 → ConverseWellFounded F.Rel
Tactic:
contrapose
State after:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
⊢ ¬ConverseWellFounded F.Rel → ¬F ⊧* 𝗟

State before:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
⊢ ¬ConverseWellFounded F.Rel → ¬F ⊧* 𝗟
Tactic:
intro hCF
State after:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
⊢ ¬F ⊧* 𝗟

State before:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
⊢ ¬F ⊧* 𝗟
Tactic:
obtain ⟨X, hX₁, hX₂⟩ := by simpa using ConverseWellFounded.iff_has_max.not.mp hCF;
State after:
case intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
⊢ ¬F ⊧* 𝗟

State before:
case intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
⊢ ¬F ⊧* 𝗟
Tactic:
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]
State after:
case intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
⊢ ∃ 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

State before:
case intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
⊢ ∃ 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
Tactic:
existsi (atom default), (λ w _ => w ∉ X), hX₁.some
State after:
case intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
⊢ (∀ (w' : F.World),
      hX₁.some ≺ w' →
        (∀ (w'_1 : F.World), w' ≺ w'_1 → Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w'_1 (atom default)) →
          Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w' (atom default)) ∧
    ∃ x, hX₁.some ≺ x ∧ ¬Satisfies { Frame := F, Valuation := fun w x => w ∉ X } x (atom default)

State before:
case intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
⊢ (∀ (w' : F.World),
      hX₁.some ≺ w' →
        (∀ (w'_1 : F.World), w' ≺ w'_1 → Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w'_1 (atom default)) →
          Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w' (atom default)) ∧
    ∃ x, hX₁.some ≺ x ∧ ¬Satisfies { Frame := F, Valuation := fun w x => w ∉ X } x (atom default)
Tactic:
constructor
State after:
case intro.intro.left
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
⊢ ∀ (w' : F.World),
    hX₁.some ≺ w' →
      (∀ (w'_1 : F.World), w' ≺ w'_1 → Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w'_1 (atom default)) →
        Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w' (atom default)

case intro.intro.right
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
⊢ ∃ x, hX₁.some ≺ x ∧ ¬Satisfies { Frame := F, Valuation := fun w x => w ∉ X } x (atom default)

State before:
case intro.intro.left
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
⊢ ∀ (w' : F.World),
    hX₁.some ≺ w' →
      (∀ (w'_1 : F.World), w' ≺ w'_1 → Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w'_1 (atom default)) →
        Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w' (atom default)

case intro.intro.right
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
⊢ ∃ x, hX₁.some ≺ x ∧ ¬Satisfies { Frame := F, Valuation := fun w x => w ∉ X } x (atom default)
Tactic:
. intro x _;
  by_cases hxs : x ∈ X
  . obtain ⟨y, hy₁, hy₂⟩ := hX₂ x hxs;
    intro h;
    exact h x (by simp_all only [Satisfies]);
  . aesop;
State after:
case intro.intro.right
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
⊢ ∃ x, hX₁.some ≺ x ∧ ¬Satisfies { Frame := F, Valuation := fun w x => w ∉ X } x (atom default)

State before:
case intro.intro.right
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
⊢ ∃ x, hX₁.some ≺ x ∧ ¬Satisfies { Frame := F, Valuation := fun w x => w ∉ X } x (atom default)
Tactic:
. obtain ⟨w', hw'₁, hw'₂⟩ := hX₂ hX₁.some (by apply Set.Nonempty.some_mem);
  existsi w';
  constructor;
  . simpa using hw'₂;
  . simpa [Satisfies];
State after:
no goals

State before:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
⊢ ?m.20147
Tactic:
simpa using ConverseWellFounded.iff_has_max.not.mp hCF
State after:
no goals

State before:
case intro.intro.left
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
⊢ ∀ (w' : F.World),
    hX₁.some ≺ w' →
      (∀ (w'_1 : F.World), w' ≺ w'_1 → Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w'_1 (atom default)) →
        Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w' (atom default)
Tactic:
intro x _
State after:
case intro.intro.left
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
x : F.World
a✝ : hX₁.some ≺ x
⊢ (∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w' (atom default)) →
    Satisfies { Frame := F, Valuation := fun w x => w ∉ X } x (atom default)

State before:
case intro.intro.left
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
x : F.World
a✝ : hX₁.some ≺ x
⊢ (∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w' (atom default)) →
    Satisfies { Frame := F, Valuation := fun w x => w ∉ X } x (atom default)
Tactic:
by_cases hxs : x ∈ X
State after:
case pos
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
x : F.World
a✝ : hX₁.some ≺ x
hxs : x ∈ X
⊢ (∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w' (atom default)) →
    Satisfies { Frame := F, Valuation := fun w x => w ∉ X } x (atom default)

case neg
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
x : F.World
a✝ : hX₁.some ≺ x
hxs : x ∉ X
⊢ (∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w' (atom default)) →
    Satisfies { Frame := F, Valuation := fun w x => w ∉ X } x (atom default)

State before:
case pos
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
x : F.World
a✝ : hX₁.some ≺ x
hxs : x ∈ X
⊢ (∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w' (atom default)) →
    Satisfies { Frame := F, Valuation := fun w x => w ∉ X } x (atom default)

case neg
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
x : F.World
a✝ : hX₁.some ≺ x
hxs : x ∉ X
⊢ (∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w' (atom default)) →
    Satisfies { Frame := F, Valuation := fun w x => w ∉ X } x (atom default)
Tactic:
. obtain ⟨y, hy₁, hy₂⟩ := hX₂ x hxs;
  intro h;
  exact h x (by simp_all only [Satisfies]);
State after:
case neg
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
x : F.World
a✝ : hX₁.some ≺ x
hxs : x ∉ X
⊢ (∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w' (atom default)) →
    Satisfies { Frame := F, Valuation := fun w x => w ∉ X } x (atom default)

State before:
case neg
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
x : F.World
a✝ : hX₁.some ≺ x
hxs : x ∉ X
⊢ (∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w' (atom default)) →
    Satisfies { Frame := F, Valuation := fun w x => w ∉ X } x (atom default)
Tactic:
. aesop;
State after:
no goals

State before:
case pos
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
x : F.World
a✝ : hX₁.some ≺ x
hxs : x ∈ X
⊢ (∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w' (atom default)) →
    Satisfies { Frame := F, Valuation := fun w x => w ∉ X } x (atom default)
Tactic:
obtain ⟨y, hy₁, hy₂⟩ := hX₂ x hxs
State after:
case pos.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
x : F.World
a✝ : hX₁.some ≺ x
hxs : x ∈ X
y : F.World
hy₁ : y ∈ X
hy₂ : F.Rel x y
⊢ (∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w' (atom default)) →
    Satisfies { Frame := F, Valuation := fun w x => w ∉ X } x (atom default)

State before:
case pos.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
x : F.World
a✝ : hX₁.some ≺ x
hxs : x ∈ X
y : F.World
hy₁ : y ∈ X
hy₂ : F.Rel x y
⊢ (∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w' (atom default)) →
    Satisfies { Frame := F, Valuation := fun w x => w ∉ X } x (atom default)
Tactic:
intro h
State after:
case pos.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
x : F.World
a✝ : hX₁.some ≺ x
hxs : x ∈ X
y : F.World
hy₁ : y ∈ X
hy₂ : F.Rel x y
h : ∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w' (atom default)
⊢ Satisfies { Frame := F, Valuation := fun w x => w ∉ X } x (atom default)

State before:
case pos.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
x : F.World
a✝ : hX₁.some ≺ x
hxs : x ∈ X
y : F.World
hy₁ : y ∈ X
hy₂ : F.Rel x y
h : ∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w' (atom default)
⊢ Satisfies { Frame := F, Valuation := fun w x => w ∉ X } x (atom default)
Tactic:
exact h x (by simp_all only [Satisfies])
State after:
no goals

State before:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
x : F.World
a✝ : hX₁.some ≺ x
hxs : x ∈ X
y : F.World
hy₁ : y ∈ X
hy₂ : F.Rel x y
h : ∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w' (atom default)
⊢ x ≺ x
Tactic:
simp_all only [Satisfies]
State after:
no goals

State before:
case neg
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
x : F.World
a✝ : hX₁.some ≺ x
hxs : x ∉ X
⊢ (∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w' (atom default)) →
    Satisfies { Frame := F, Valuation := fun w x => w ∉ X } x (atom default)
Tactic:
aesop
State after:
no goals

State before:
case intro.intro.right
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
⊢ ∃ x, hX₁.some ≺ x ∧ ¬Satisfies { Frame := F, Valuation := fun w x => w ∉ X } x (atom default)
Tactic:
obtain ⟨w', hw'₁, hw'₂⟩ := hX₂ hX₁.some (by apply Set.Nonempty.some_mem)
State after:
case intro.intro.right.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
w' : F.World
hw'₁ : w' ∈ X
hw'₂ : F.Rel hX₁.some w'
⊢ ∃ x, hX₁.some ≺ x ∧ ¬Satisfies { Frame := F, Valuation := fun w x => w ∉ X } x (atom default)

State before:
case intro.intro.right.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
w' : F.World
hw'₁ : w' ∈ X
hw'₂ : F.Rel hX₁.some w'
⊢ ∃ x, hX₁.some ≺ x ∧ ¬Satisfies { Frame := F, Valuation := fun w x => w ∉ X } x (atom default)
Tactic:
existsi w'
State after:
case intro.intro.right.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
w' : F.World
hw'₁ : w' ∈ X
hw'₂ : F.Rel hX₁.some w'
⊢ hX₁.some ≺ w' ∧ ¬Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w' (atom default)

State before:
case intro.intro.right.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
w' : F.World
hw'₁ : w' ∈ X
hw'₂ : F.Rel hX₁.some w'
⊢ hX₁.some ≺ w' ∧ ¬Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w' (atom default)
Tactic:
constructor
State after:
case intro.intro.right.intro.intro.left
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
w' : F.World
hw'₁ : w' ∈ X
hw'₂ : F.Rel hX₁.some w'
⊢ hX₁.some ≺ w'

case intro.intro.right.intro.intro.right
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
w' : F.World
hw'₁ : w' ∈ X
hw'₂ : F.Rel hX₁.some w'
⊢ ¬Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w' (atom default)

State before:
case intro.intro.right.intro.intro.left
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
w' : F.World
hw'₁ : w' ∈ X
hw'₂ : F.Rel hX₁.some w'
⊢ hX₁.some ≺ w'

case intro.intro.right.intro.intro.right
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
w' : F.World
hw'₁ : w' ∈ X
hw'₂ : F.Rel hX₁.some w'
⊢ ¬Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w' (atom default)
Tactic:
. simpa using hw'₂;
State after:
case intro.intro.right.intro.intro.right
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
w' : F.World
hw'₁ : w' ∈ X
hw'₂ : F.Rel hX₁.some w'
⊢ ¬Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w' (atom default)

State before:
case intro.intro.right.intro.intro.right
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
w' : F.World
hw'₁ : w' ∈ X
hw'₂ : F.Rel hX₁.some w'
⊢ ¬Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w' (atom default)
Tactic:
. simpa [Satisfies];
State after:
no goals

State before:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
⊢ hX₁.some ∈ X
Tactic:
apply Set.Nonempty.some_mem
State after:
no goals

State before:
case intro.intro.right.intro.intro.left
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
w' : F.World
hw'₁ : w' ∈ X
hw'₂ : F.Rel hX₁.some w'
⊢ hX₁.some ≺ w'
Tactic:
simpa using hw'₂
State after:
no goals

State before:
case intro.intro.right.intro.intro.right
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
w' : F.World
hw'₁ : w' ∈ X
hw'₂ : F.Rel hX₁.some w'
⊢ ¬Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w' (atom default)
Tactic:
simpa [Satisfies]
State after:
no goals