Theorem: LO.Modal.Standard.boxdotTranslatedK4_of_S4 (Logic/Modal/Standard/Boxdot.lean)

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

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

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!;
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✝ᵇ

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!;
State after:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
hFour : p✝ ∈ 𝟰
⊢ 𝐊𝟒 ⊢! p✝ᵇ

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

State before:
case hMaxm.inl.inl
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
hK : p✝ ∈ 𝗞
⊢ 𝐊𝟒 ⊢! p✝ᵇ
Tactic:
obtain ⟨_, _, e⟩ := hK
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✝ᵇ

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

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

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

State before:
case hMaxm.inl.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
hT : p✝ ∈ 𝗧
⊢ 𝐊𝟒 ⊢! p✝ᵇ
Tactic:
obtain ⟨_, e⟩ := hT
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✝ᵇ

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
State after:
case hMaxm.inl.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐒𝟒 ⊢! Axioms.T w✝
⊢ 𝐊𝟒 ⊢! Axioms.T w✝ᵇ

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]
State after:
case hMaxm.inl.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐒𝟒 ⊢! Axioms.T w✝
⊢ 𝐊𝟒 ⊢! ⊡w✝ᵇ ⟶ w✝ᵇ

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

State before:
case hMaxm.inr
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
hFour : p✝ ∈ 𝟰
⊢ 𝐊𝟒 ⊢! p✝ᵇ
Tactic:
obtain ⟨_, e⟩ := hFour
State after:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! p✝
w✝ : Formula α
e : Axioms.Four w✝ = p✝
⊢ 𝐊𝟒 ⊢! p✝ᵇ

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
State after:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐒𝟒 ⊢! Axioms.Four w✝
⊢ 𝐊𝟒 ⊢! Axioms.Four w✝ᵇ

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]
State after:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐒𝟒 ⊢! Axioms.Four w✝
⊢ 𝐊𝟒 ⊢! ⊡w✝ᵇ ⟶ ⊡⊡w✝ᵇ

State before:
case hMaxm.inr.intro
α : Type u_1
inst✝ : DecidableEq α
p w✝ : Formula α
h : 𝐒𝟒 ⊢! Axioms.Four w✝
⊢ 𝐊𝟒 ⊢! ⊡w✝ᵇ ⟶ ⊡⊡w✝ᵇ
Tactic:
apply boxdot_axiomFour!
State after:
no goals

State before:
case hNec
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hp : 𝐒𝟒 ⊢ p✝
ihp : 𝐒𝟒 ⊢! p✝ → 𝐊𝟒 ⊢! p✝ᵇ
h : 𝐒𝟒 ⊢! □p✝
⊢ 𝐊𝟒 ⊢! (□p✝)ᵇ
Tactic:
dsimp [BoxdotTranslation]
State after:
case hNec
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
hp : 𝐒𝟒 ⊢ p✝
ihp : 𝐒𝟒 ⊢! p✝ → 𝐊𝟒 ⊢! p✝ᵇ
h : 𝐒𝟒 ⊢! □p✝
⊢ 𝐊𝟒 ⊢! ⊡p✝ᵇ

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

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

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

State before:
case hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐊𝟒 ⊢! (~~p✝ ⟶ p✝)ᵇ
Tactic:
dsimp [BoxdotTranslation]
State after:
case hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐊𝟒 ⊢! ((p✝ᵇ ⟶ ⊥) ⟶ ⊥) ⟶ p✝ᵇ

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

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

State before:
case hVerum
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐒𝟒 ⊢! ⊤
⊢ 𝐊𝟒 ⊢! ⊤
Tactic:
apply verum!
State after:
no goals

State before:
case hConj₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐒𝟒 ⊢! p✝ ⋏ q✝ ⟶ p✝
⊢ 𝐊𝟒 ⊢! p✝ᵇ ⋏ q✝ᵇ ⟶ p✝ᵇ
Tactic:
apply conj₁!
State after:
no goals

State before:
case hConj₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐒𝟒 ⊢! p✝ ⋏ q✝ ⟶ q✝
⊢ 𝐊𝟒 ⊢! p✝ᵇ ⋏ q✝ᵇ ⟶ q✝ᵇ
Tactic:
apply conj₂!
State after:
no goals

State before:
case hConj₃
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐒𝟒 ⊢! p✝ ⟶ q✝ ⟶ p✝ ⋏ q✝
⊢ 𝐊𝟒 ⊢! p✝ᵇ ⟶ q✝ᵇ ⟶ p✝ᵇ ⋏ q✝ᵇ
Tactic:
apply conj₃!
State after:
no goals

State before:
case hDisj₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐒𝟒 ⊢! p✝ ⟶ p✝ ⋎ q✝
⊢ 𝐊𝟒 ⊢! p✝ᵇ ⟶ p✝ᵇ ⋎ q✝ᵇ
Tactic:
apply disj₁!
State after:
no goals

State before:
case hDisj₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐒𝟒 ⊢! q✝ ⟶ p✝ ⋎ q✝
⊢ 𝐊𝟒 ⊢! q✝ᵇ ⟶ p✝ᵇ ⋎ q✝ᵇ
Tactic:
apply disj₂!
State after:
no goals

State before:
case hDisj₃
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ r✝ : Formula α
h : 𝐒𝟒 ⊢! (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
⊢ 𝐊𝟒 ⊢! (p✝ᵇ ⟶ r✝ᵇ) ⟶ (q✝ᵇ ⟶ r✝ᵇ) ⟶ p✝ᵇ ⋎ q✝ᵇ ⟶ r✝ᵇ
Tactic:
apply disj₃!
State after:
no goals

State before:
case hImply₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
h : 𝐒𝟒 ⊢! p✝ ⟶ q✝ ⟶ p✝
⊢ 𝐊𝟒 ⊢! p✝ᵇ ⟶ q✝ᵇ ⟶ p✝ᵇ
Tactic:
apply imply₁!
State after:
no goals

State before:
case hImply₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ r✝ : Formula α
h : 𝐒𝟒 ⊢! (p✝ ⟶ q✝ ⟶ r✝) ⟶ (p✝ ⟶ q✝) ⟶ p✝ ⟶ r✝
⊢ 𝐊𝟒 ⊢! (p✝ᵇ ⟶ q✝ᵇ ⟶ r✝ᵇ) ⟶ (p✝ᵇ ⟶ q✝ᵇ) ⟶ p✝ᵇ ⟶ r✝ᵇ
Tactic:
apply imply₂!
State after:
no goals

State before:
case hDne
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
h : 𝐒𝟒 ⊢! ~~p✝ ⟶ p✝
⊢ 𝐊𝟒 ⊢! ((p✝ᵇ ⟶ ⊥) ⟶ ⊥) ⟶ p✝ᵇ
Tactic:
apply dne!
State after:
no goals