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

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

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 [Connected] at hCon
State after:
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : ∃ x x_1, F.Rel x x_1 ∧ ∃ x_2, F.Rel x x_2 ∧ ¬F.Rel x_1 x_2 ∧ ¬F.Rel x_2 x_1
⊢ ¬F ⊧* .𝟯

State before:
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : ∃ x x_1, F.Rel x x_1 ∧ ∃ x_2, F.Rel x x_2 ∧ ¬F.Rel x_1 x_2 ∧ ¬F.Rel x_2 x_1
⊢ ¬F ⊧* .𝟯
Tactic:
obtain ⟨x, y, rxy, z, ryz, nryz, nrzy⟩ := hCon
State after:
case intro.intro.intro.intro.intro.intro
α : 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 ⊧* .𝟯

State before:
case intro.intro.intro.intro.intro.intro
α : 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 ⊧* .𝟯
Tactic:
simp [ValidOnFrame]
State after:
case intro.intro.intro.intro.intro.intro
α : 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
⊢ ∃ a b x, ¬ValidOnModel { Frame := F, Valuation := x } (Axioms.Dot3 a b)

State before:
case intro.intro.intro.intro.intro.intro
α : 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
⊢ ∃ a b x, ¬ValidOnModel { Frame := F, Valuation := x } (Axioms.Dot3 a b)
Tactic:
obtain ⟨f, finv, fInj⟩ := atleast.mapping
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
α : 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
⊢ ∃ a b x, ¬ValidOnModel { Frame := F, Valuation := x } (Axioms.Dot3 a b)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
α : 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
⊢ ∃ a b x, ¬ValidOnModel { Frame := F, Valuation := x } (Axioms.Dot3 a b)
Tactic:
existsi f 0, f 1, (λ w a =>
  match (finv a) with
  | 0 => y ≺ w
  | 1 => z ≺ w
)
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
α : 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
⊢ ¬ValidOnModel
      { Frame := F,
        Valuation := fun w a =>
          match finv a with
          | 0 => y ≺ w
          | 1 => z ≺ w }
      (Axioms.Dot3 (atom (f 0)) (atom (f 1)))

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
α : 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
⊢ ¬ValidOnModel
      { Frame := F,
        Valuation := fun w a =>
          match finv a with
          | 0 => y ≺ w
          | 1 => z ≺ w }
      (Axioms.Dot3 (atom (f 0)) (atom (f 1)))
Tactic:
simp [ValidOnModel, not_forall, Axioms.Dot3]
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
α : 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,
    (∃ 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 0))) ∧
            ¬Satisfies
                { Frame := F,
                  Valuation := fun w a =>
                    match finv a with
                    | 0 => y ≺ w
                    | 1 => z ≺ w }
                x_1 (atom (f 1))) ∧
      ∃ 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))

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
α : 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,
    (∃ 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 0))) ∧
            ¬Satisfies
                { Frame := F,
                  Valuation := fun w a =>
                    match finv a with
                    | 0 => y ≺ w
                    | 1 => z ≺ w }
                x_1 (atom (f 1))) ∧
      ∃ 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 x
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
α : 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 0))) ∧
          ¬Satisfies
              { Frame := F,
                Valuation := fun w a =>
                  match finv a with
                  | 0 => y ≺ w
                  | 1 => z ≺ w }
              x_1 (atom (f 1))) ∧
    ∃ 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))

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
α : 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 0))) ∧
          ¬Satisfies
              { Frame := F,
                Valuation := fun w a =>
                  match finv a with
                  | 0 => y ≺ w
                  | 1 => z ≺ w }
              x_1 (atom (f 1))) ∧
    ∃ 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:
constructor
State after:
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_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 0))) ∧
        ¬Satisfies
            { Frame := F,
              Valuation := fun w a =>
                match finv a with
                | 0 => y ≺ w
                | 1 => z ≺ w }
            x_1 (atom (f 1))

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

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_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 0))) ∧
        ¬Satisfies
            { Frame := F,
              Valuation := fun w a =>
                match finv a with
                | 0 => y ≺ w
                | 1 => z ≺ w }
            x_1 (atom (f 1))

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 y;
  constructor;
  . assumption;
  . simp_all [Satisfies, (fInj 0), (fInj 1)];
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_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))

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;
  constructor;
  . assumption;
  . simp_all [Satisfies, (fInj 0), (fInj 1)];
State after:
no goals

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_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 0))) ∧
        ¬Satisfies
            { Frame := F,
              Valuation := fun w a =>
                match finv a with
                | 0 => y ≺ w
                | 1 => z ≺ w }
            x_1 (atom (f 1))
Tactic:
existsi y
State after:
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))

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

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

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

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

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

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

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

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

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

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

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