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

State before:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐒𝟒 ⊢! p ↔ 𝐊𝟒 ⊢! pᵇ
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐒𝟒 ⊢! p → 𝐊𝟒 ⊢! pᵇ

case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐊𝟒 ⊢! pᵇ → 𝐒𝟒 ⊢! p

State before:
case mp
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐒𝟒 ⊢! p → 𝐊𝟒 ⊢! pᵇ

case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐊𝟒 ⊢! pᵇ → 𝐒𝟒 ⊢! p
Tactic:
. apply boxdotTranslatedK4_of_S4;
State after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐊𝟒 ⊢! pᵇ → 𝐒𝟒 ⊢! p

State before:
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐊𝟒 ⊢! pᵇ → 𝐒𝟒 ⊢! p
Tactic:
. apply S4_of_boxdotTranslatedK4;
State after:
no goals

State before:
case mp
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐒𝟒 ⊢! p → 𝐊𝟒 ⊢! pᵇ
Tactic:
apply boxdotTranslatedK4_of_S4
State after:
no goals

State before:
case mpr
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐊𝟒 ⊢! pᵇ → 𝐒𝟒 ⊢! p
Tactic:
apply S4_of_boxdotTranslatedK4
State after:
no goals