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

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

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

State before:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hT : ¬Transitive F.Rel
⊢ ¬F ⊧* 𝗟
Tactic:
simp [Transitive] at hT
State after:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hT : ∃ x x_1, F.Rel x x_1 ∧ ∃ x_2, F.Rel x_1 x_2 ∧ ¬F.Rel x x_2
⊢ ¬F ⊧* 𝗟

State before:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hT : ∃ x x_1, F.Rel x x_1 ∧ ∃ x_2, F.Rel x_1 x_2 ∧ ¬F.Rel x x_2
⊢ ¬F ⊧* 𝗟
Tactic:
obtain ⟨w₁, w₂, r₁₂, w₃, r₂₃, nr₁₃⟩ := hT
State after:
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 ⊧* 𝗟

State before:
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 ⊧* 𝗟
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.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

State before:
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
Tactic:
existsi (atom default), (λ w' _ => w' ≠ w₂ ∧ w' ≠ w₃), w₁
State after:
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₃
⊢ (∀ (w' : F.World),
      w₁ ≺ w' →
        (∀ (w'_1 : F.World),
            w' ≺ w'_1 → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w'_1 (atom default)) →
          Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)) ∧
    ∃ x, w₁ ≺ x ∧ ¬Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)

State before:
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₃
⊢ (∀ (w' : F.World),
      w₁ ≺ w' →
        (∀ (w'_1 : F.World),
            w' ≺ w'_1 → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w'_1 (atom default)) →
          Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)) ∧
    ∃ x, w₁ ≺ x ∧ ¬Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)
Tactic:
constructor
State after:
case intro.intro.intro.intro.intro.left
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₃
⊢ ∀ (w' : F.World),
    w₁ ≺ w' →
      (∀ (w'_1 : F.World),
          w' ≺ w'_1 → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w'_1 (atom default)) →
        Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)

case intro.intro.intro.intro.intro.right
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, w₁ ≺ x ∧ ¬Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)

State before:
case intro.intro.intro.intro.intro.left
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₃
⊢ ∀ (w' : F.World),
    w₁ ≺ w' →
      (∀ (w'_1 : F.World),
          w' ≺ w'_1 → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w'_1 (atom default)) →
        Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)

case intro.intro.intro.intro.intro.right
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, w₁ ≺ x ∧ ¬Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)
Tactic:
. intro x hx h;
  by_cases hx₂ : x = w₂;
  . subst hx₂; simpa [Satisfies] using h w₃ r₂₃;
  . by_cases hx₃ : x = w₃ <;> simp_all [Satisfies, hx₃];
State after:
case intro.intro.intro.intro.intro.right
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, w₁ ≺ x ∧ ¬Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)

State before:
case intro.intro.intro.intro.intro.right
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, w₁ ≺ x ∧ ¬Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)
Tactic:
. existsi w₂; simpa [Satisfies];
State after:
no goals

State before:
case intro.intro.intro.intro.intro.left
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₃
⊢ ∀ (w' : F.World),
    w₁ ≺ w' →
      (∀ (w'_1 : F.World),
          w' ≺ w'_1 → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w'_1 (atom default)) →
        Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)
Tactic:
intro x hx h
State after:
case intro.intro.intro.intro.intro.left
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 : F.World
hx : w₁ ≺ x
h : ∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)
⊢ Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)

State before:
case intro.intro.intro.intro.intro.left
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 : F.World
hx : w₁ ≺ x
h : ∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)
⊢ Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)
Tactic:
by_cases hx₂ : x = w₂
State after:
case pos
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 : F.World
hx : w₁ ≺ x
h : ∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)
hx₂ : x = w₂
⊢ Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)

case neg
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 : F.World
hx : w₁ ≺ x
h : ∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)
hx₂ : ¬x = w₂
⊢ Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)

State before:
case pos
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 : F.World
hx : w₁ ≺ x
h : ∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)
hx₂ : x = w₂
⊢ Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)

case neg
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 : F.World
hx : w₁ ≺ x
h : ∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)
hx₂ : ¬x = w₂
⊢ Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)
Tactic:
. subst hx₂; simpa [Satisfies] using h w₃ r₂₃;
State after:
case neg
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 : F.World
hx : w₁ ≺ x
h : ∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)
hx₂ : ¬x = w₂
⊢ Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)

State before:
case neg
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 : F.World
hx : w₁ ≺ x
h : ∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)
hx₂ : ¬x = w₂
⊢ Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)
Tactic:
. by_cases hx₃ : x = w₃ <;> simp_all [Satisfies, hx₃];
State after:
no goals

State before:
case pos
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 : F.World
hx : w₁ ≺ x
h : ∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)
hx₂ : x = w₂
⊢ Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)
Tactic:
subst hx₂
State after:
case pos
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₃ : F.World
nr₁₃ : ¬F.Rel w₁ w₃
x : F.World
hx : w₁ ≺ x
r₁₂ : F.Rel w₁ x
r₂₃ : F.Rel x w₃
h : ∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w' x_1 => w' ≠ x ∧ w' ≠ w₃ } w' (atom default)
⊢ Satisfies { Frame := F, Valuation := fun w' x_1 => w' ≠ x ∧ w' ≠ w₃ } x (atom default)

State before:
case pos
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₃ : F.World
nr₁₃ : ¬F.Rel w₁ w₃
x : F.World
hx : w₁ ≺ x
r₁₂ : F.Rel w₁ x
r₂₃ : F.Rel x w₃
h : ∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w' x_1 => w' ≠ x ∧ w' ≠ w₃ } w' (atom default)
⊢ Satisfies { Frame := F, Valuation := fun w' x_1 => w' ≠ x ∧ w' ≠ w₃ } x (atom default)
Tactic:
simpa [Satisfies] using h w₃ r₂₃
State after:
no goals

State before:
case neg
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 : F.World
hx : w₁ ≺ x
h : ∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)
hx₂ : ¬x = w₂
⊢ Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)
Tactic:
by_cases hx₃ : x = w₃ <;> simp_all [Satisfies, hx₃]
State after:
no goals

State before:
case intro.intro.intro.intro.intro.right
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, w₁ ≺ x ∧ ¬Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)
Tactic:
existsi w₂
State after:
case intro.intro.intro.intro.intro.right
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₃
⊢ w₁ ≺ w₂ ∧ ¬Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w₂ (atom default)

State before:
case intro.intro.intro.intro.intro.right
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₃
⊢ w₁ ≺ w₂ ∧ ¬Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w₂ (atom default)
Tactic:
simpa [Satisfies]
State after:
no goals