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

State before:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
⊢ Transitive F.Rel ∧ ConverseWellFounded F.Rel → F ⊧* 𝗟
Tactic:
rintro ⟨hTrans, hWF⟩
State after:
case intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
⊢ F ⊧* 𝗟

State before:
case intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
⊢ F ⊧* 𝗟
Tactic:
simp [AxiomSet.L, Axioms.L]
State after:
case intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
⊢ ∀ (a : Formula α), ValidOnFrame F (□(□a ⟶ a) ⟶ □a)

State before:
case intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
⊢ ∀ (a : Formula α), ValidOnFrame F (□(□a ⟶ a) ⟶ □a)
Tactic:
intro p V w
State after:
case intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
⊢ w ⊧ □(□p ⟶ p) ⟶ □p

State before:
case intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
⊢ w ⊧ □(□p ⟶ p) ⟶ □p
Tactic:
simp only [Satisfies.iff_models, Satisfies.imp_def]
State after:
case intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
⊢ Satisfies { Frame := F, Valuation := V } w (□(□p ⟶ p)) → Satisfies { Frame := F, Valuation := V } w (□p)

State before:
case intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
⊢ Satisfies { Frame := F, Valuation := V } w (□(□p ⟶ p)) → Satisfies { Frame := F, Valuation := V } w (□p)
Tactic:
contrapose
State after:
case intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
⊢ ¬Satisfies { Frame := F, Valuation := V } w (□p) → ¬Satisfies { Frame := F, Valuation := V } w (□(□p ⟶ p))

State before:
case intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
⊢ ¬Satisfies { Frame := F, Valuation := V } w (□p) → ¬Satisfies { Frame := F, Valuation := V } w (□(□p ⟶ p))
Tactic:
intro h
State after:
case intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
⊢ ¬Satisfies { Frame := F, Valuation := V } w (□(□p ⟶ p))

State before:
case intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
⊢ ¬Satisfies { Frame := F, Valuation := V } w (□(□p ⟶ p))
Tactic:
obtain ⟨z, rwz, hz⟩ := by simpa using h;
State after:
case intro.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
⊢ ¬Satisfies { Frame := F, Valuation := V } w (□(□p ⟶ p))

State before:
case intro.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
⊢ ¬Satisfies { Frame := F, Valuation := V } w (□(□p ⟶ p))
Tactic:
obtain ⟨xm, ⟨hxm₁, hxm₂⟩⟩ := hWF.has_min ({ x | (F.Rel w x) ∧ ¬(Satisfies ⟨F, V⟩ x p) }) (by existsi z; simp_all)
State after:
case intro.intro.intro.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
⊢ ¬Satisfies { Frame := F, Valuation := V } w (□(□p ⟶ p))

State before:
case intro.intro.intro.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
⊢ ¬Satisfies { Frame := F, Valuation := V } w (□(□p ⟶ p))
Tactic:
simp [Satisfies.box_def]
State after:
case intro.intro.intro.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
⊢ ∃ x,
    w ≺ x ∧
      (∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := V } w' p) ∧
        ¬Satisfies { Frame := F, Valuation := V } x p

State before:
case intro.intro.intro.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
⊢ ∃ x,
    w ≺ x ∧
      (∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := V } w' p) ∧
        ¬Satisfies { Frame := F, Valuation := V } x p
Tactic:
existsi xm
State after:
case intro.intro.intro.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
⊢ w ≺ xm ∧
    (∀ (w' : F.World), xm ≺ w' → Satisfies { Frame := F, Valuation := V } w' p) ∧
      ¬Satisfies { Frame := F, Valuation := V } xm p

State before:
case intro.intro.intro.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
⊢ w ≺ xm ∧
    (∀ (w' : F.World), xm ≺ w' → Satisfies { Frame := F, Valuation := V } w' p) ∧
      ¬Satisfies { Frame := F, Valuation := V } xm p
Tactic:
have : Satisfies ⟨F, V⟩ xm (□p) := by
  by_contra hC;
  obtain ⟨y, hy₁, hy₂⟩ := by simpa using hC;
  have : ¬(xm ≺ y) := hxm₂ y ⟨(hTrans (by simp_all) hy₁), hy₂⟩;
  contradiction;
State after:
case intro.intro.intro.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
this : Satisfies { Frame := F, Valuation := V } xm (□p)
⊢ w ≺ xm ∧
    (∀ (w' : F.World), xm ≺ w' → Satisfies { Frame := F, Valuation := V } w' p) ∧
      ¬Satisfies { Frame := F, Valuation := V } xm p

State before:
case intro.intro.intro.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
this : Satisfies { Frame := F, Valuation := V } xm (□p)
⊢ w ≺ xm ∧
    (∀ (w' : F.World), xm ≺ w' → Satisfies { Frame := F, Valuation := V } w' p) ∧
      ¬Satisfies { Frame := F, Valuation := V } xm p
Tactic:
simp_all
State after:
no goals

State before:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
⊢ ?m.44125
Tactic:
simpa using h
State after:
no goals

State before:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
⊢ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}.Nonempty
Tactic:
existsi z
State after:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
⊢ z ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}

State before:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
⊢ z ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
Tactic:
simp_all
State after:
no goals

State before:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
⊢ Satisfies { Frame := F, Valuation := V } xm (□p)
Tactic:
by_contra hC
State after:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
hC : ¬Satisfies { Frame := F, Valuation := V } xm (□p)
⊢ False

State before:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
hC : ¬Satisfies { Frame := F, Valuation := V } xm (□p)
⊢ False
Tactic:
obtain ⟨y, hy₁, hy₂⟩ := by simpa using hC;
State after:
case intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
hC : ¬Satisfies { Frame := F, Valuation := V } xm (□p)
y : F.World
hy₁ : xm ≺ y
hy₂ : ¬Satisfies { Frame := F, Valuation := V } y p
⊢ False

State before:
case intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
hC : ¬Satisfies { Frame := F, Valuation := V } xm (□p)
y : F.World
hy₁ : xm ≺ y
hy₂ : ¬Satisfies { Frame := F, Valuation := V } y p
⊢ False
Tactic:
have : ¬(xm ≺ y) := hxm₂ y ⟨(hTrans (by simp_all) hy₁), hy₂⟩
State after:
case intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
hC : ¬Satisfies { Frame := F, Valuation := V } xm (□p)
y : F.World
hy₁ : xm ≺ y
hy₂ : ¬Satisfies { Frame := F, Valuation := V } y p
this : ¬xm ≺ y
⊢ False

State before:
case intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
hC : ¬Satisfies { Frame := F, Valuation := V } xm (□p)
y : F.World
hy₁ : xm ≺ y
hy₂ : ¬Satisfies { Frame := F, Valuation := V } y p
this : ¬xm ≺ y
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
hC : ¬Satisfies { Frame := F, Valuation := V } xm (□p)
⊢ ?m.80491
Tactic:
simpa using hC
State after:
no goals

State before:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
hC : ¬Satisfies { Frame := F, Valuation := V } xm (□p)
y : F.World
hy₁ : xm ≺ y
hy₂ : ¬Satisfies { Frame := F, Valuation := V } y p
⊢ F.Rel w xm
Tactic:
simp_all
State after:
no goals