Theorem: LO.Modal.Standard.AxiomSet.Dot3.definability.impliedBy (Logic/Modal/Standard/Kripke/Dot3.lean)

State before:
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
⊢ Connected F.Rel → F ⊧* .𝟯
Tactic:
intro hCon
State after:
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
⊢ F ⊧* .𝟯

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]
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

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
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✝

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
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))

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]
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))

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
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))

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;
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))

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
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)

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;
State after:
no goals

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
State after:
no goals

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
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)

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]
State after:
no goals

State before:
case intro.intro.intro.inr
α : 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
rzy : F.Rel z y
⊢ Satisfies { Frame := F, Valuation := V } z (□q ⟶ p)
Tactic:
simp [Satisfies.box_def, Satisfies.imp_def]
State after:
case intro.intro.intro.inr
α : 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
rzy : F.Rel z y
⊢ (∀ (w' : F.World), z ≺ w' → Satisfies { Frame := F, Valuation := V } w' q) →
    Satisfies { Frame := F, Valuation := V } z p

State before:
case intro.intro.intro.inr
α : 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
rzy : F.Rel z y
⊢ (∀ (w' : F.World), z ≺ w' → Satisfies { Frame := F, Valuation := V } w' q) →
    Satisfies { Frame := F, Valuation := V } z p
Tactic:
intro hq
State after:
case intro.intro.intro.inr
α : 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
rzy : F.Rel z y
hq : ∀ (w' : F.World), z ≺ w' → Satisfies { Frame := F, Valuation := V } w' q
⊢ Satisfies { Frame := F, Valuation := V } z p

State before:
case intro.intro.intro.inr
α : 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
rzy : F.Rel z y
hq : ∀ (w' : F.World), z ≺ w' → Satisfies { Frame := F, Valuation := V } w' q
⊢ Satisfies { Frame := F, Valuation := V } z p
Tactic:
have hyp := hq y rzy
State after:
case intro.intro.intro.inr
α : 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
rzy : F.Rel z y
hq : ∀ (w' : F.World), z ≺ w' → Satisfies { Frame := F, Valuation := V } w' q
hyp : Satisfies { Frame := F, Valuation := V } y q
⊢ Satisfies { Frame := F, Valuation := V } z p

State before:
case intro.intro.intro.inr
α : 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
rzy : F.Rel z y
hq : ∀ (w' : F.World), z ≺ w' → Satisfies { Frame := F, Valuation := V } w' q
hyp : Satisfies { Frame := F, Valuation := V } y q
⊢ Satisfies { Frame := F, Valuation := V } z p
Tactic:
contradiction
State after:
no goals