internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multidia_def
Proof state before:
case succ.mp.intro.intro.intro.intro
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
x : M.Frame.World
hvx : v ≺^[n] x
hx : Satisfies M x p
⊢ ∃ v, w ≺^[n + 1] v ∧ Satisfies M v p
Tactic:
existsi x
Proof state after:
case succ.mp.intro.intro.intro.intro
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
x : M.Frame.World
hvx : v ≺^[n] x
hx : Satisfies M x p
⊢ w ≺^[n + 1] x ∧ Satisfies M x p
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multidia_def
Proof state before:
case succ.mp.intro.intro.intro.intro
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
x : M.Frame.World
hvx : v ≺^[n] x
hx : Satisfies M x p
⊢ w ≺^[n + 1] x ∧ Satisfies M x p
Tactic:
constructor
Proof state after:
case succ.mp.intro.intro.intro.intro.left
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
x : M.Frame.World
hvx : v ≺^[n] x
hx : Satisfies M x p
⊢ w ≺^[n + 1] x

case succ.mp.intro.intro.intro.intro.right
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
x : M.Frame.World
hvx : v ≺^[n] x
hx : Satisfies M x p
⊢ Satisfies M x p
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multidia_def
Proof state before:
case succ.mp.intro.intro.intro.intro.left
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
x : M.Frame.World
hvx : v ≺^[n] x
hx : Satisfies M x p
⊢ w ≺^[n + 1] x

case succ.mp.intro.intro.intro.intro.right
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
x : M.Frame.World
hvx : v ≺^[n] x
hx : Satisfies M x p
⊢ Satisfies M x p
Tactic:
. existsi v; simp_all;
Proof state after:
case succ.mp.intro.intro.intro.intro.right
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
x : M.Frame.World
hvx : v ≺^[n] x
hx : Satisfies M x p
⊢ Satisfies M x p
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multidia_def
Proof state before:
case succ.mp.intro.intro.intro.intro.right
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
x : M.Frame.World
hvx : v ≺^[n] x
hx : Satisfies M x p
⊢ Satisfies M x p
Tactic:
. simpa;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multidia_def
Proof state before:
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
⊢ ?m.54398
Tactic:
simpa using h
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multidia_def
Proof state before:
case succ.mp.intro.intro.intro.intro.left
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
x : M.Frame.World
hvx : v ≺^[n] x
hx : Satisfies M x p
⊢ w ≺^[n + 1] x
Tactic:
existsi v
Proof state after:
case succ.mp.intro.intro.intro.intro.left
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
x : M.Frame.World
hvx : v ≺^[n] x
hx : Satisfies M x p
⊢ (fun x x_1 => x ≺ x_1) w v ∧ RelItr (fun x x_1 => x ≺ x_1) n v x
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multidia_def
Proof state before:
case succ.mp.intro.intro.intro.intro.left
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
x : M.Frame.World
hvx : v ≺^[n] x
hx : Satisfies M x p
⊢ (fun x x_1 => x ≺ x_1) w v ∧ RelItr (fun x x_1 => x ≺ x_1) n v x
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multidia_def
Proof state before:
case succ.mp.intro.intro.intro.intro.right
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
h : Satisfies M w (◇^[(n + 1)]p)
v : M.Frame.World
hwv : w ≺ v
hv : Satisfies M v ((UnaryModalOperator.mop false)^[n] p)
x : M.Frame.World
hvx : v ≺^[n] x
hx : Satisfies M x p
⊢ Satisfies M x p
Tactic:
simpa
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multidia_def
Proof state before:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
⊢ (∃ v, w ≺^[n + 1] v ∧ Satisfies M v p) → Satisfies M w (◇^[(n + 1)]p)
Tactic:
simp
Proof state after:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
⊢ ∀ (x x_1 : M.Frame.World),
    w ≺ x_1 →
      RelItr (fun x x_2 => x ≺ x_2) n x_1 x →
        Satisfies M x p → ∃ w', w ≺ w' ∧ Satisfies M w' ((UnaryModalOperator.mop false)^[n] p)
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multidia_def
Proof state before:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
⊢ ∀ (x x_1 : M.Frame.World),
    w ≺ x_1 →
      RelItr (fun x x_2 => x ≺ x_2) n x_1 x →
        Satisfies M x p → ∃ w', w ≺ w' ∧ Satisfies M w' ((UnaryModalOperator.mop false)^[n] p)
Tactic:
intro x y hwy hyx hx
Proof state after:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ ∃ w', w ≺ w' ∧ Satisfies M w' ((UnaryModalOperator.mop false)^[n] p)
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multidia_def
Proof state before:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ ∃ w', w ≺ w' ∧ Satisfies M w' ((UnaryModalOperator.mop false)^[n] p)
Tactic:
existsi y
Proof state after:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ w ≺ y ∧ Satisfies M y ((UnaryModalOperator.mop false)^[n] p)
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multidia_def
Proof state before:
case succ.mpr
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ w ≺ y ∧ Satisfies M y ((UnaryModalOperator.mop false)^[n] p)
Tactic:
constructor
Proof state after:
case succ.mpr.left
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ w ≺ y

case succ.mpr.right
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ Satisfies M y ((UnaryModalOperator.mop false)^[n] p)
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multidia_def
Proof state before:
case succ.mpr.left
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ w ≺ y

case succ.mpr.right
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ Satisfies M y ((UnaryModalOperator.mop false)^[n] p)
Tactic:
. simpa;
Proof state after:
case succ.mpr.right
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ Satisfies M y ((UnaryModalOperator.mop false)^[n] p)
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multidia_def
Proof state before:
case succ.mpr.right
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ Satisfies M y ((UnaryModalOperator.mop false)^[n] p)
Tactic:
. apply ih.mpr;
  existsi x;
  simp_all;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multidia_def
Proof state before:
case succ.mpr.left
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ w ≺ y
Tactic:
simpa
Proof state after:
no goals
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multidia_def
Proof state before:
case succ.mpr.right
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ Satisfies M y ((UnaryModalOperator.mop false)^[n] p)
Tactic:
apply ih.mpr
Proof state after:
case succ.mpr.right
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ ∃ v, y ≺^[n] v ∧ Satisfies M v p
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multidia_def
Proof state before:
case succ.mpr.right
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ ∃ v, y ≺^[n] v ∧ Satisfies M v p
Tactic:
existsi x
Proof state after:
case succ.mpr.right
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ y ≺^[n] x ∧ Satisfies M x p
Theorem: LO.Modal.Standard.Formula.Kripke.Satisfies.multidia_def
Proof state before:
case succ.mpr.right
α : Type u_1
M : Model α
p q : Formula α
n : ℕ
ih : ∀ {w : M.World}, Satisfies M w (◇^[n]p) ↔ ∃ v, w ≺^[n] v ∧ Satisfies M v p
w : M.World
x y : M.Frame.World
hwy : w ≺ y
hyx : RelItr (fun x x_1 => x ≺ x_1) n y x
hx : Satisfies M x p
⊢ y ≺^[n] x ∧ Satisfies M x p
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.validOnAxiomSetFrameClass_axiom
Proof state before:
α : Type u_1
Ax : AxiomSet α
p : Formula α
h : p ∈ Ax
⊢ 𝔽(Ax) ⊧ p
Tactic:
intro F hF
Proof state after:
α : Type u_1
Ax : AxiomSet α
p : Formula α
h : p ∈ Ax
F : Frame' α
hF : F ∈ 𝔽(Ax)
⊢ F ⊧ p
Theorem: LO.Modal.Standard.Kripke.validOnAxiomSetFrameClass_axiom
Proof state before:
α : Type u_1
Ax : AxiomSet α
p : Formula α
h : p ∈ Ax
F : Frame' α
hF : F ∈ 𝔽(Ax)
⊢ F ⊧ p
Tactic:
exact hF.realize h
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.iff_definability_memAxiomSetFrameClass
Proof state before:
α : Type u_1
Ax : AxiomSet α
P : FrameProperty
definability : Definability Ax P
⊢ ∀ {F : Frame' α}, F ∈ 𝔽(Ax) ↔ P F
Tactic:
apply definability.defines
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.iff_finiteDefinability_memFiniteFrameClass
Proof state before:
α : Type u_1
Ax : AxiomSet α
P : FiniteFrameProperty
definability : FiniteDefinability Ax P
⊢ ∀ {F : FiniteFrame' α}, 𝔽ꟳ(Ax) F ↔ P F
Tactic:
apply definability.fin_defines
Proof state after:
no goals
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐒𝟒 ⊢! p
⊢ 𝐊𝟒 ⊢! pᵇ
Tactic:
induction h.some using Deduction.inducition_with_nec with
| hMaxm a =>
  rcases a with (hK | hT) | hFour;
  . obtain ⟨_, _, e⟩ := hK; subst_vars; dsimp [Axioms.K, BoxdotTranslation]; apply boxdot_axiomK!;
  . obtain ⟨_, e⟩ := hT; subst_vars; dsimp [Axioms.T, BoxdotTranslation]; apply boxdot_axiomT!;
  . obtain ⟨_, e⟩ := hFour; subst_vars; dsimp [Axioms.Four, BoxdotTranslation]; apply boxdot_axiomFour!;
| hNec hp ihp =>
  dsimp [BoxdotTranslation];
  exact boxdot_nec! $ ihp ⟨hp⟩;
| hMdp hpq hp ihpq ihp =>
  dsimp [BoxdotTranslation] at ihpq ihp;
  exact (ihpq ⟨hpq⟩) ⨀ (ihp ⟨hp⟩);
| _ =>
  dsimp [BoxdotTranslation];
  try first
  | apply verum!;
  | apply conj₁!;
  | apply conj₂!;
  | apply conj₃!;
  | apply disj₁!;
  | apply disj₂!;
  | apply disj₃!;
  | apply imply₁!;
  | apply imply₂!;
  | apply dne!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hMaxm
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
a : p✝ ∈ Ax(𝐒𝟒)
h : 𝐒𝟒 ⊢! p✝
⊢ 𝐊𝟒 ⊢! p✝ᵇ
Tactic:
rcases a with (hK | hT) | hFour
Proof state after:
case hMaxm.inl.inl
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
hK : p✝ ∈ 𝗞
⊢ 𝐊𝟒 ⊢! p✝ᵇ

case hMaxm.inl.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
hT : p✝ ∈ 𝗧
⊢ 𝐊𝟒 ⊢! p✝ᵇ

case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
hFour : p✝ ∈ 𝟰
⊢ 𝐊𝟒 ⊢! p✝ᵇ
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hMaxm.inl.inl
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
hK : p✝ ∈ 𝗞
⊢ 𝐊𝟒 ⊢! p✝ᵇ

case hMaxm.inl.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
hT : p✝ ∈ 𝗧
⊢ 𝐊𝟒 ⊢! p✝ᵇ

case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
hFour : p✝ ∈ 𝟰
⊢ 𝐊𝟒 ⊢! p✝ᵇ
Tactic:
. obtain ⟨_, _, e⟩ := hK; subst_vars; dsimp [Axioms.K, BoxdotTranslation]; apply boxdot_axiomK!;
Proof state after:
case hMaxm.inl.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
hT : p✝ ∈ 𝗧
⊢ 𝐊𝟒 ⊢! p✝ᵇ

case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
hFour : p✝ ∈ 𝟰
⊢ 𝐊𝟒 ⊢! p✝ᵇ
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hMaxm.inl.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
hT : p✝ ∈ 𝗧
⊢ 𝐊𝟒 ⊢! p✝ᵇ

case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
hFour : p✝ ∈ 𝟰
⊢ 𝐊𝟒 ⊢! p✝ᵇ
Tactic:
. obtain ⟨_, e⟩ := hT; subst_vars; dsimp [Axioms.T, BoxdotTranslation]; apply boxdot_axiomT!;
Proof state after:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
hFour : p✝ ∈ 𝟰
⊢ 𝐊𝟒 ⊢! p✝ᵇ
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
hFour : p✝ ∈ 𝟰
⊢ 𝐊𝟒 ⊢! p✝ᵇ
Tactic:
. obtain ⟨_, e⟩ := hFour; subst_vars; dsimp [Axioms.Four, BoxdotTranslation]; apply boxdot_axiomFour!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hMaxm.inl.inl
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
hK : p✝ ∈ 𝗞
⊢ 𝐊𝟒 ⊢! p✝ᵇ
Tactic:
obtain ⟨_, _, e⟩ := hK
Proof state after:
case hMaxm.inl.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
w✝¹ w✝ : Formula α
e : Axioms.K w✝¹ w✝ = p✝
⊢ 𝐊𝟒 ⊢! p✝ᵇ
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hMaxm.inl.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
w✝¹ w✝ : Formula α
e : Axioms.K w✝¹ w✝ = p✝
⊢ 𝐊𝟒 ⊢! p✝ᵇ
Tactic:
subst_vars
Proof state after:
case hMaxm.inl.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
h : 𝐒𝟒 ⊢! Axioms.K w✝¹ w✝
⊢ 𝐊𝟒 ⊢! Axioms.K w✝¹ w✝ᵇ
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hMaxm.inl.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
h : 𝐒𝟒 ⊢! Axioms.K w✝¹ w✝
⊢ 𝐊𝟒 ⊢! Axioms.K w✝¹ w✝ᵇ
Tactic:
dsimp [Axioms.K, BoxdotTranslation]
Proof state after:
case hMaxm.inl.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
h : 𝐒𝟒 ⊢! Axioms.K w✝¹ w✝
⊢ 𝐊𝟒 ⊢! ⊡(w✝¹ᵇ ⟶ w✝ᵇ) ⟶ ⊡w✝¹ᵇ ⟶ ⊡w✝ᵇ
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hMaxm.inl.inl.intro.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝¹ w✝ : Formula α
h : 𝐒𝟒 ⊢! Axioms.K w✝¹ w✝
⊢ 𝐊𝟒 ⊢! ⊡(w✝¹ᵇ ⟶ w✝ᵇ) ⟶ ⊡w✝¹ᵇ ⟶ ⊡w✝ᵇ
Tactic:
apply boxdot_axiomK!
Proof state after:
no goals
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hMaxm.inl.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
hT : p✝ ∈ 𝗧
⊢ 𝐊𝟒 ⊢! p✝ᵇ
Tactic:
obtain ⟨_, e⟩ := hT
Proof state after:
case hMaxm.inl.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
w✝ : Formula α
e : Axioms.T w✝ = p✝
⊢ 𝐊𝟒 ⊢! p✝ᵇ
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hMaxm.inl.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
w✝ : Formula α
e : Axioms.T w✝ = p✝
⊢ 𝐊𝟒 ⊢! p✝ᵇ
Tactic:
subst_vars
Proof state after:
case hMaxm.inl.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐒𝟒 ⊢! Axioms.T w✝
⊢ 𝐊𝟒 ⊢! Axioms.T w✝ᵇ
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hMaxm.inl.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐒𝟒 ⊢! Axioms.T w✝
⊢ 𝐊𝟒 ⊢! Axioms.T w✝ᵇ
Tactic:
dsimp [Axioms.T, BoxdotTranslation]
Proof state after:
case hMaxm.inl.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐒𝟒 ⊢! Axioms.T w✝
⊢ 𝐊𝟒 ⊢! ⊡w✝ᵇ ⟶ w✝ᵇ
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hMaxm.inl.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐒𝟒 ⊢! Axioms.T w✝
⊢ 𝐊𝟒 ⊢! ⊡w✝ᵇ ⟶ w✝ᵇ
Tactic:
apply boxdot_axiomT!
Proof state after:
no goals
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
hFour : p✝ ∈ 𝟰
⊢ 𝐊𝟒 ⊢! p✝ᵇ
Tactic:
obtain ⟨_, e⟩ := hFour
Proof state after:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
w✝ : Formula α
e : Axioms.Four w✝ = p✝
⊢ 𝐊𝟒 ⊢! p✝ᵇ
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
w✝ : Formula α
e : Axioms.Four w✝ = p✝
⊢ 𝐊𝟒 ⊢! p✝ᵇ
Tactic:
subst_vars
Proof state after:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐒𝟒 ⊢! Axioms.Four w✝
⊢ 𝐊𝟒 ⊢! Axioms.Four w✝ᵇ
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐒𝟒 ⊢! Axioms.Four w✝
⊢ 𝐊𝟒 ⊢! Axioms.Four w✝ᵇ
Tactic:
dsimp [Axioms.Four, BoxdotTranslation]
Proof state after:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐒𝟒 ⊢! Axioms.Four w✝
⊢ 𝐊𝟒 ⊢! ⊡w✝ᵇ ⟶ ⊡⊡w✝ᵇ
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐒𝟒 ⊢! Axioms.Four w✝
⊢ 𝐊𝟒 ⊢! ⊡w✝ᵇ ⟶ ⊡⊡w✝ᵇ
Tactic:
apply boxdot_axiomFour!
Proof state after:
no goals
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hNec
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hp : 𝐒𝟒 ⊢ p✝
ihp : 𝐒𝟒 ⊢! p✝ → 𝐊𝟒 ⊢! p✝ᵇ
h : 𝐒𝟒 ⊢! □p✝
⊢ 𝐊𝟒 ⊢! (□p✝)ᵇ
Tactic:
dsimp [BoxdotTranslation]
Proof state after:
case hNec
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hp : 𝐒𝟒 ⊢ p✝
ihp : 𝐒𝟒 ⊢! p✝ → 𝐊𝟒 ⊢! p✝ᵇ
h : 𝐒𝟒 ⊢! □p✝
⊢ 𝐊𝟒 ⊢! ⊡p✝ᵇ
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hNec
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hp : 𝐒𝟒 ⊢ p✝
ihp : 𝐒𝟒 ⊢! p✝ → 𝐊𝟒 ⊢! p✝ᵇ
h : 𝐒𝟒 ⊢! □p✝
⊢ 𝐊𝟒 ⊢! ⊡p✝ᵇ
Tactic:
exact boxdot_nec! $ ihp ⟨hp⟩
Proof state after:
no goals
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hMdp
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
hpq : 𝐒𝟒 ⊢ p✝ ⟶ q✝
hp : 𝐒𝟒 ⊢ p✝
ihpq : 𝐒𝟒 ⊢! p✝ ⟶ q✝ → 𝐊𝟒 ⊢! (p✝ ⟶ q✝)ᵇ
ihp : 𝐒𝟒 ⊢! p✝ → 𝐊𝟒 ⊢! p✝ᵇ
h : 𝐒𝟒 ⊢! q✝
⊢ 𝐊𝟒 ⊢! q✝ᵇ
Tactic:
dsimp [BoxdotTranslation] at ihpq ihp
Proof state after:
case hMdp
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
hpq : 𝐒𝟒 ⊢ p✝ ⟶ q✝
hp : 𝐒𝟒 ⊢ p✝
ihpq : 𝐒𝟒 ⊢! p✝ ⟶ q✝ → 𝐊𝟒 ⊢! p✝ᵇ ⟶ q✝ᵇ
ihp : 𝐒𝟒 ⊢! p✝ → 𝐊𝟒 ⊢! p✝ᵇ
h : 𝐒𝟒 ⊢! q✝
⊢ 𝐊𝟒 ⊢! q✝ᵇ
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hMdp
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
hpq : 𝐒𝟒 ⊢ p✝ ⟶ q✝
hp : 𝐒𝟒 ⊢ p✝
ihpq : 𝐒𝟒 ⊢! p✝ ⟶ q✝ → 𝐊𝟒 ⊢! p✝ᵇ ⟶ q✝ᵇ
ihp : 𝐒𝟒 ⊢! p✝ → 𝐊𝟒 ⊢! p✝ᵇ
h : 𝐒𝟒 ⊢! q✝
⊢ 𝐊𝟒 ⊢! q✝ᵇ
Tactic:
exact (ihpq ⟨hpq⟩) ⨀ (ihp ⟨hp⟩)
Proof state after:
no goals
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐊𝟒 ⊢! (~~p✝ ⟶ p✝)ᵇ
Tactic:
dsimp [BoxdotTranslation]
Proof state after:
case hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐊𝟒 ⊢! ((p✝ᵇ ⟶ ⊥) ⟶ ⊥) ⟶ p✝ᵇ
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐊𝟒 ⊢! ((p✝ᵇ ⟶ ⊥) ⟶ ⊥) ⟶ p✝ᵇ
Tactic:
try first
| apply verum!;
| apply conj₁!;
| apply conj₂!;
| apply conj₃!;
| apply disj₁!;
| apply disj₂!;
| apply disj₃!;
| apply imply₁!;
| apply imply₂!;
| apply dne!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐊𝟒 ⊢! ((p✝ᵇ ⟶ ⊥) ⟶ ⊥) ⟶ p✝ᵇ
Tactic:
first
| apply verum!;
| apply conj₁!;
| apply conj₂!;
| apply conj₃!;
| apply disj₁!;
| apply disj₂!;
| apply disj₃!;
| apply imply₁!;
| apply imply₂!;
| apply dne!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4
Proof state before:
case hVerum
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐒𝟒 ⊢! ⊤
⊢ 𝐊𝟒 ⊢! ⊤
Tactic:
apply verum!
Proof state after:
no goals