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

State before:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐒𝟒 ⊢! p ⟷ pᵇ
Tactic:
induction p using Formula.rec' with
| hand p q ihp ihq => dsimp [BoxdotTranslation]; exact and_replace_iff! ihp ihq;
| hor p q ihp ihq => dsimp [BoxdotTranslation]; exact or_replace_iff! ihp ihq;
| himp p q ihp ihq => dsimp [BoxdotTranslation]; exact imp_replace_iff! ihp ihq;
| hbox p ihp =>
  dsimp [BoxdotTranslation];
  exact iff_trans! (box_iff! ihp) iff_box_boxdot!;
| _ => dsimp [BoxdotTranslation]; exact iff_id!;
State after:
no goals

State before:
case hand
α : Type u_1
inst✝ : DecidableEq α
p✝ p q : Formula α
ihp : 𝐒𝟒 ⊢! p ⟷ pᵇ
ihq : 𝐒𝟒 ⊢! q ⟷ qᵇ
⊢ 𝐒𝟒 ⊢! p ⋏ q ⟷ (p ⋏ q)ᵇ
Tactic:
dsimp [BoxdotTranslation]
State after:
case hand
α : Type u_1
inst✝ : DecidableEq α
p✝ p q : Formula α
ihp : 𝐒𝟒 ⊢! p ⟷ pᵇ
ihq : 𝐒𝟒 ⊢! q ⟷ qᵇ
⊢ 𝐒𝟒 ⊢! p ⋏ q ⟷ pᵇ ⋏ qᵇ

State before:
case hand
α : Type u_1
inst✝ : DecidableEq α
p✝ p q : Formula α
ihp : 𝐒𝟒 ⊢! p ⟷ pᵇ
ihq : 𝐒𝟒 ⊢! q ⟷ qᵇ
⊢ 𝐒𝟒 ⊢! p ⋏ q ⟷ pᵇ ⋏ qᵇ
Tactic:
exact and_replace_iff! ihp ihq
State after:
no goals

State before:
case hor
α : Type u_1
inst✝ : DecidableEq α
p✝ p q : Formula α
ihp : 𝐒𝟒 ⊢! p ⟷ pᵇ
ihq : 𝐒𝟒 ⊢! q ⟷ qᵇ
⊢ 𝐒𝟒 ⊢! p ⋎ q ⟷ (p ⋎ q)ᵇ
Tactic:
dsimp [BoxdotTranslation]
State after:
case hor
α : Type u_1
inst✝ : DecidableEq α
p✝ p q : Formula α
ihp : 𝐒𝟒 ⊢! p ⟷ pᵇ
ihq : 𝐒𝟒 ⊢! q ⟷ qᵇ
⊢ 𝐒𝟒 ⊢! p ⋎ q ⟷ pᵇ ⋎ qᵇ

State before:
case hor
α : Type u_1
inst✝ : DecidableEq α
p✝ p q : Formula α
ihp : 𝐒𝟒 ⊢! p ⟷ pᵇ
ihq : 𝐒𝟒 ⊢! q ⟷ qᵇ
⊢ 𝐒𝟒 ⊢! p ⋎ q ⟷ pᵇ ⋎ qᵇ
Tactic:
exact or_replace_iff! ihp ihq
State after:
no goals

State before:
case himp
α : Type u_1
inst✝ : DecidableEq α
p✝ p q : Formula α
ihp : 𝐒𝟒 ⊢! p ⟷ pᵇ
ihq : 𝐒𝟒 ⊢! q ⟷ qᵇ
⊢ 𝐒𝟒 ⊢! (p ⟶ q) ⟷ (p ⟶ q)ᵇ
Tactic:
dsimp [BoxdotTranslation]
State after:
case himp
α : Type u_1
inst✝ : DecidableEq α
p✝ p q : Formula α
ihp : 𝐒𝟒 ⊢! p ⟷ pᵇ
ihq : 𝐒𝟒 ⊢! q ⟷ qᵇ
⊢ 𝐒𝟒 ⊢! (p ⟶ q) ⟷ (pᵇ ⟶ qᵇ)

State before:
case himp
α : Type u_1
inst✝ : DecidableEq α
p✝ p q : Formula α
ihp : 𝐒𝟒 ⊢! p ⟷ pᵇ
ihq : 𝐒𝟒 ⊢! q ⟷ qᵇ
⊢ 𝐒𝟒 ⊢! (p ⟶ q) ⟷ (pᵇ ⟶ qᵇ)
Tactic:
exact imp_replace_iff! ihp ihq
State after:
no goals

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

State before:
case hbox
α : Type u_1
inst✝ : DecidableEq α
p✝ p : Formula α
ihp : 𝐒𝟒 ⊢! p ⟷ pᵇ
⊢ 𝐒𝟒 ⊢! □p ⟷ ⊡pᵇ
Tactic:
exact iff_trans! (box_iff! ihp) iff_box_boxdot!
State after:
no goals

State before:
case hatom
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
a✝ : α
⊢ 𝐒𝟒 ⊢! atom a✝ ⟷ atom a✝ᵇ
Tactic:
dsimp [BoxdotTranslation]
State after:
case hatom
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
a✝ : α
⊢ 𝐒𝟒 ⊢! atom a✝ ⟷ atom a✝

State before:
case hatom
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
a✝ : α
⊢ 𝐒𝟒 ⊢! atom a✝ ⟷ atom a✝
Tactic:
exact iff_id!
State after:
no goals