internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.implies
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ x ≺ y ∧
    (∀ (w' : F.World),
        y ≺ w' →
          Satisfies
            { Frame := F,
              Valuation := fun w a =>
                match finv a with
                | 0 => y ≺ w
                | 1 => z ≺ w }
            w' (atom (f 0))) ∧
      ¬Satisfies
          { Frame := F,
            Valuation := fun w a =>
              match finv a with
              | 0 => y ≺ w
              | 1 => z ≺ w }
          y (atom (f 1))
Tactic:
constructor
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.left.left
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ x ≺ y

case intro.intro.intro.intro.intro.intro.intro.intro.left.right
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ (∀ (w' : F.World),
      y ≺ w' →
        Satisfies
          { Frame := F,
            Valuation := fun w a =>
              match finv a with
              | 0 => y ≺ w
              | 1 => z ≺ w }
          w' (atom (f 0))) ∧
    ¬Satisfies
        { Frame := F,
          Valuation := fun w a =>
            match finv a with
            | 0 => y ≺ w
            | 1 => z ≺ w }
        y (atom (f 1))
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.implies
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.left.left
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ x ≺ y

case intro.intro.intro.intro.intro.intro.intro.intro.left.right
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ (∀ (w' : F.World),
      y ≺ w' →
        Satisfies
          { Frame := F,
            Valuation := fun w a =>
              match finv a with
              | 0 => y ≺ w
              | 1 => z ≺ w }
          w' (atom (f 0))) ∧
    ¬Satisfies
        { Frame := F,
          Valuation := fun w a =>
            match finv a with
            | 0 => y ≺ w
            | 1 => z ≺ w }
        y (atom (f 1))
Tactic:
. assumption;
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.left.right
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ (∀ (w' : F.World),
      y ≺ w' →
        Satisfies
          { Frame := F,
            Valuation := fun w a =>
              match finv a with
              | 0 => y ≺ w
              | 1 => z ≺ w }
          w' (atom (f 0))) ∧
    ¬Satisfies
        { Frame := F,
          Valuation := fun w a =>
            match finv a with
            | 0 => y ≺ w
            | 1 => z ≺ w }
        y (atom (f 1))
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.implies
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.left.right
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ (∀ (w' : F.World),
      y ≺ w' →
        Satisfies
          { Frame := F,
            Valuation := fun w a =>
              match finv a with
              | 0 => y ≺ w
              | 1 => z ≺ w }
          w' (atom (f 0))) ∧
    ¬Satisfies
        { Frame := F,
          Valuation := fun w a =>
            match finv a with
            | 0 => y ≺ w
            | 1 => z ≺ w }
        y (atom (f 1))
Tactic:
. simp_all [Satisfies, (fInj 0), (fInj 1)];
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.implies
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.left.left
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ x ≺ y
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.implies
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.left.right
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ (∀ (w' : F.World),
      y ≺ w' →
        Satisfies
          { Frame := F,
            Valuation := fun w a =>
              match finv a with
              | 0 => y ≺ w
              | 1 => z ≺ w }
          w' (atom (f 0))) ∧
    ¬Satisfies
        { Frame := F,
          Valuation := fun w a =>
            match finv a with
            | 0 => y ≺ w
            | 1 => z ≺ w }
        y (atom (f 1))
Tactic:
simp_all [Satisfies, (fInj 0), (fInj 1)]
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.implies
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.right
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ ∃ x_1,
    x ≺ x_1 ∧
      (∀ (w' : F.World),
          x_1 ≺ w' →
            Satisfies
              { Frame := F,
                Valuation := fun w a =>
                  match finv a with
                  | 0 => y ≺ w
                  | 1 => z ≺ w }
              w' (atom (f 1))) ∧
        ¬Satisfies
            { Frame := F,
              Valuation := fun w a =>
                match finv a with
                | 0 => y ≺ w
                | 1 => z ≺ w }
            x_1 (atom (f 0))
Tactic:
existsi z
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.right
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ x ≺ z ∧
    (∀ (w' : F.World),
        z ≺ w' →
          Satisfies
            { Frame := F,
              Valuation := fun w a =>
                match finv a with
                | 0 => y ≺ w
                | 1 => z ≺ w }
            w' (atom (f 1))) ∧
      ¬Satisfies
          { Frame := F,
            Valuation := fun w a =>
              match finv a with
              | 0 => y ≺ w
              | 1 => z ≺ w }
          z (atom (f 0))
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.implies
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.right
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ x ≺ z ∧
    (∀ (w' : F.World),
        z ≺ w' →
          Satisfies
            { Frame := F,
              Valuation := fun w a =>
                match finv a with
                | 0 => y ≺ w
                | 1 => z ≺ w }
            w' (atom (f 1))) ∧
      ¬Satisfies
          { Frame := F,
            Valuation := fun w a =>
              match finv a with
              | 0 => y ≺ w
              | 1 => z ≺ w }
          z (atom (f 0))
Tactic:
constructor
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.right.left
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ x ≺ z

case intro.intro.intro.intro.intro.intro.intro.intro.right.right
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ (∀ (w' : F.World),
      z ≺ w' →
        Satisfies
          { Frame := F,
            Valuation := fun w a =>
              match finv a with
              | 0 => y ≺ w
              | 1 => z ≺ w }
          w' (atom (f 1))) ∧
    ¬Satisfies
        { Frame := F,
          Valuation := fun w a =>
            match finv a with
            | 0 => y ≺ w
            | 1 => z ≺ w }
        z (atom (f 0))
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.implies
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.right.left
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ x ≺ z

case intro.intro.intro.intro.intro.intro.intro.intro.right.right
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ (∀ (w' : F.World),
      z ≺ w' →
        Satisfies
          { Frame := F,
            Valuation := fun w a =>
              match finv a with
              | 0 => y ≺ w
              | 1 => z ≺ w }
          w' (atom (f 1))) ∧
    ¬Satisfies
        { Frame := F,
          Valuation := fun w a =>
            match finv a with
            | 0 => y ≺ w
            | 1 => z ≺ w }
        z (atom (f 0))
Tactic:
. assumption;
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.right.right
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ (∀ (w' : F.World),
      z ≺ w' →
        Satisfies
          { Frame := F,
            Valuation := fun w a =>
              match finv a with
              | 0 => y ≺ w
              | 1 => z ≺ w }
          w' (atom (f 1))) ∧
    ¬Satisfies
        { Frame := F,
          Valuation := fun w a =>
            match finv a with
            | 0 => y ≺ w
            | 1 => z ≺ w }
        z (atom (f 0))
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.implies
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.right.right
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ (∀ (w' : F.World),
      z ≺ w' →
        Satisfies
          { Frame := F,
            Valuation := fun w a =>
              match finv a with
              | 0 => y ≺ w
              | 1 => z ≺ w }
          w' (atom (f 1))) ∧
    ¬Satisfies
        { Frame := F,
          Valuation := fun w a =>
            match finv a with
            | 0 => y ≺ w
            | 1 => z ≺ w }
        z (atom (f 0))
Tactic:
. simp_all [Satisfies, (fInj 0), (fInj 1)];
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.implies
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.right.left
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ x ≺ z
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.implies
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.right.right
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
f : Fin ↑2 → α
finv : α → Fin ↑2
fInj : Function.LeftInverse finv f
⊢ (∀ (w' : F.World),
      z ≺ w' →
        Satisfies
          { Frame := F,
            Valuation := fun w a =>
              match finv a with
              | 0 => y ≺ w
              | 1 => z ≺ w }
          w' (atom (f 1))) ∧
    ¬Satisfies
        { Frame := F,
          Valuation := fun w a =>
            match finv a with
            | 0 => y ≺ w
            | 1 => z ≺ w }
        z (atom (f 0))
Tactic:
simp_all [Satisfies, (fInj 0), (fInj 1)]
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.impliedBy
Proof state before:
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
⊢ Connected F.Rel → F ⊧* .𝟯
Tactic:
intro hCon
Proof state after:
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
⊢ F ⊧* .𝟯
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.impliedBy
Proof state before:
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
⊢ F ⊧* .𝟯
Tactic:
simp [ValidOnFrame, ValidOnModel, Axioms.Dot3]
Proof state after:
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
⊢ ∀ (f x x_1 : Formula α),
    □(□x ⟶ x_1) ⋎ □(□x_1 ⟶ x) = f →
      ∀ (V : Valuation F.World α) (w : { Frame := F, Valuation := V }.World),
        Satisfies { Frame := F, Valuation := V } w f
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.impliedBy
Proof state before:
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
⊢ ∀ (f x x_1 : Formula α),
    □(□x ⟶ x_1) ⋎ □(□x_1 ⟶ x) = f →
      ∀ (V : Valuation F.World α) (w : { Frame := F, Valuation := V }.World),
        Satisfies { Frame := F, Valuation := V } w f
Tactic:
intro _ p q e V x
Proof state after:
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
f✝ p q : Formula α
e : □(□p ⟶ q) ⋎ □(□q ⟶ p) = f✝
V : Valuation F.World α
x : { Frame := F, Valuation := V }.World
⊢ Satisfies { Frame := F, Valuation := V } x f✝
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.impliedBy
Proof state before:
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
f✝ p q : Formula α
e : □(□p ⟶ q) ⋎ □(□q ⟶ p) = f✝
V : Valuation F.World α
x : { Frame := F, Valuation := V }.World
⊢ Satisfies { Frame := F, Valuation := V } x f✝
Tactic:
subst e
Proof state after:
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
p q : Formula α
V : Valuation F.World α
x : { Frame := F, Valuation := V }.World
⊢ Satisfies { Frame := F, Valuation := V } x (□(□p ⟶ q) ⋎ □(□q ⟶ p))
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.impliedBy
Proof state before:
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
p q : Formula α
V : Valuation F.World α
x : { Frame := F, Valuation := V }.World
⊢ Satisfies { Frame := F, Valuation := V } x (□(□p ⟶ q) ⋎ □(□q ⟶ p))
Tactic:
simp only [Satisfies.or_def, or_iff_not_imp_left]
Proof state after:
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
p q : Formula α
V : Valuation F.World α
x : { Frame := F, Valuation := V }.World
⊢ ¬Satisfies { Frame := F, Valuation := V } x (□(□p ⟶ q)) → Satisfies { Frame := F, Valuation := V } x (□(□q ⟶ p))
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.impliedBy
Proof state before:
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
p q : Formula α
V : Valuation F.World α
x : { Frame := F, Valuation := V }.World
⊢ ¬Satisfies { Frame := F, Valuation := V } x (□(□p ⟶ q)) → Satisfies { Frame := F, Valuation := V } x (□(□q ⟶ p))
Tactic:
intro hnxpq
Proof state after:
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
p q : Formula α
V : Valuation F.World α
x : { Frame := F, Valuation := V }.World
hnxpq : ¬Satisfies { Frame := F, Valuation := V } x (□(□p ⟶ q))
⊢ Satisfies { Frame := F, Valuation := V } x (□(□q ⟶ p))
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.impliedBy
Proof state before:
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
p q : Formula α
V : Valuation F.World α
x : { Frame := F, Valuation := V }.World
hnxpq : ¬Satisfies { Frame := F, Valuation := V } x (□(□p ⟶ q))
⊢ Satisfies { Frame := F, Valuation := V } x (□(□q ⟶ p))
Tactic:
obtain ⟨y, rxy, hyp, hnyq⟩ := by simpa using hnxpq;
Proof state after:
case intro.intro.intro
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
p q : Formula α
V : Valuation F.World α
x : { Frame := F, Valuation := V }.World
hnxpq : ¬Satisfies { Frame := F, Valuation := V } x (□(□p ⟶ q))
y : F.World
rxy : x ≺ y
hyp : ∀ (w' : F.World), y ≺ w' → Satisfies { Frame := F, Valuation := V } w' p
hnyq : ¬Satisfies { Frame := F, Valuation := V } y q
⊢ Satisfies { Frame := F, Valuation := V } x (□(□q ⟶ p))
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.impliedBy
Proof state before:
case intro.intro.intro
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
p q : Formula α
V : Valuation F.World α
x : { Frame := F, Valuation := V }.World
hnxpq : ¬Satisfies { Frame := F, Valuation := V } x (□(□p ⟶ q))
y : F.World
rxy : x ≺ y
hyp : ∀ (w' : F.World), y ≺ w' → Satisfies { Frame := F, Valuation := V } w' p
hnyq : ¬Satisfies { Frame := F, Valuation := V } y q
⊢ Satisfies { Frame := F, Valuation := V } x (□(□q ⟶ p))
Tactic:
intro z rxz
Proof state after:
case intro.intro.intro
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
p q : Formula α
V : Valuation F.World α
x : { Frame := F, Valuation := V }.World
hnxpq : ¬Satisfies { Frame := F, Valuation := V } x (□(□p ⟶ q))
y : F.World
rxy : x ≺ y
hyp : ∀ (w' : F.World), y ≺ w' → Satisfies { Frame := F, Valuation := V } w' p
hnyq : ¬Satisfies { Frame := F, Valuation := V } y q
z : { Frame := F, Valuation := V }.Frame.World
rxz : x ≺ z
⊢ Satisfies { Frame := F, Valuation := V } z (□q ⟶ p)
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.impliedBy
Proof state before:
case intro.intro.intro
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
p q : Formula α
V : Valuation F.World α
x : { Frame := F, Valuation := V }.World
hnxpq : ¬Satisfies { Frame := F, Valuation := V } x (□(□p ⟶ q))
y : F.World
rxy : x ≺ y
hyp : ∀ (w' : F.World), y ≺ w' → Satisfies { Frame := F, Valuation := V } w' p
hnyq : ¬Satisfies { Frame := F, Valuation := V } y q
z : { Frame := F, Valuation := V }.Frame.World
rxz : x ≺ z
⊢ Satisfies { Frame := F, Valuation := V } z (□q ⟶ p)
Tactic:
cases hCon ⟨rxy, rxz⟩ with
| inl ryz =>
  have := hyp _ ryz;
  simp_all only [Satisfies.imp_def, implies_true];
| inr rzy =>
  simp [Satisfies.box_def, Satisfies.imp_def]
  intro hq;
  have hyp := hq y rzy;
  contradiction;
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.impliedBy
Proof state before:
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
p q : Formula α
V : Valuation F.World α
x : { Frame := F, Valuation := V }.World
hnxpq : ¬Satisfies { Frame := F, Valuation := V } x (□(□p ⟶ q))
⊢ ?m.143017
Tactic:
simpa using hnxpq
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.impliedBy
Proof state before:
case intro.intro.intro.inl
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
p q : Formula α
V : Valuation F.World α
x : { Frame := F, Valuation := V }.World
hnxpq : ¬Satisfies { Frame := F, Valuation := V } x (□(□p ⟶ q))
y : F.World
rxy : x ≺ y
hyp : ∀ (w' : F.World), y ≺ w' → Satisfies { Frame := F, Valuation := V } w' p
hnyq : ¬Satisfies { Frame := F, Valuation := V } y q
z : { Frame := F, Valuation := V }.Frame.World
rxz : x ≺ z
ryz : F.Rel y z
⊢ Satisfies { Frame := F, Valuation := V } z (□q ⟶ p)
Tactic:
have := hyp _ ryz
Proof state after:
case intro.intro.intro.inl
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
p q : Formula α
V : Valuation F.World α
x : { Frame := F, Valuation := V }.World
hnxpq : ¬Satisfies { Frame := F, Valuation := V } x (□(□p ⟶ q))
y : F.World
rxy : x ≺ y
hyp : ∀ (w' : F.World), y ≺ w' → Satisfies { Frame := F, Valuation := V } w' p
hnyq : ¬Satisfies { Frame := F, Valuation := V } y q
z : { Frame := F, Valuation := V }.Frame.World
rxz : x ≺ z
ryz : F.Rel y z
this : Satisfies { Frame := F, Valuation := V } z p
⊢ Satisfies { Frame := F, Valuation := V } z (□q ⟶ p)
Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.impliedBy
Proof state before:
case intro.intro.intro.inl
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
p q : Formula α
V : Valuation F.World α
x : { Frame := F, Valuation := V }.World
hnxpq : ¬Satisfies { Frame := F, Valuation := V } x (□(□p ⟶ q))
y : F.World
rxy : x ≺ y
hyp : ∀ (w' : F.World), y ≺ w' → Satisfies { Frame := F, Valuation := V } w' p
hnyq : ¬Satisfies { Frame := F, Valuation := V } y q
z : { Frame := F, Valuation := V }.Frame.World
rxz : x ≺ z
ryz : F.Rel y z
this : Satisfies { Frame := F, Valuation := V } z p
⊢ Satisfies { Frame := F, Valuation := V } z (□q ⟶ p)
Tactic:
simp_all only [Satisfies.imp_def, implies_true]
Proof state after:
no goals