internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_transitive
Proof 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₂
Proof 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)
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_transitive
Proof 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]
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_cwf
Proof state before:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
⊢ F ⊧* 𝗟 → ConverseWellFounded F.Rel
Tactic:
contrapose
Proof state after:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
⊢ ¬ConverseWellFounded F.Rel → ¬F ⊧* 𝗟
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_cwf
Proof state before:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
⊢ ¬ConverseWellFounded F.Rel → ¬F ⊧* 𝗟
Tactic:
intro hCF
Proof state after:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
⊢ ¬F ⊧* 𝗟
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_cwf
Proof 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;
Proof 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 ⊧* 𝗟
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_cwf
Proof 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]
Proof 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
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_cwf
Proof 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
Proof 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)
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_cwf
Proof 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
Proof 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)
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_cwf
Proof 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;
Proof 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)
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_cwf
Proof 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];
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_cwf
Proof 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
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_cwf
Proof 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 _
Proof 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)
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_cwf
Proof 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
Proof 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)
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_cwf
Proof 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]);
Proof 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)
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_cwf
Proof 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;
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_cwf
Proof 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
Proof 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)
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_cwf
Proof 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
Proof 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)
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_cwf
Proof 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])
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_cwf
Proof 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]
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_cwf
Proof 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
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_cwf
Proof 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)
Proof 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)
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_cwf
Proof 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'
Proof 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)
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_cwf
Proof 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
Proof 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)
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_cwf
Proof 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'₂;
Proof 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)
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_cwf
Proof 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];
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_cwf
Proof 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
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_cwf
Proof 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'₂
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.L.definability.implies_cwf
Proof 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]
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.L.definability.impliedby
Proof state before:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
⊢ Transitive F.Rel ∧ ConverseWellFounded F.Rel → F ⊧* 𝗟
Tactic:
rintro ⟨hTrans, hWF⟩
Proof state after:
case intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
⊢ F ⊧* 𝗟
Theorem: LO.Modal.Standard.AxiomSet.L.definability.impliedby
Proof 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]
Proof 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)
Theorem: LO.Modal.Standard.AxiomSet.L.definability.impliedby
Proof 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
Proof 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
Theorem: LO.Modal.Standard.AxiomSet.L.definability.impliedby
Proof 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]
Proof 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)
Theorem: LO.Modal.Standard.AxiomSet.L.definability.impliedby
Proof 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
Proof 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))