Theorem: LO.Modal.Standard.deducible_iff_trivTranslation (Logic/Modal/Standard/Maximal.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐓𝐫𝐢𝐯 ⊢! p ⟷ pᵀ
Tactic:
induction p using Formula.rec' with
| hbox p ih =>
  simp [TrivTranslation];
  apply iff_intro!;
  . exact imp_trans! axiomT! (conj₁'! ih)
  . exact imp_trans! (conj₂'! ih) axiomTc!
| himp _ _ ih₁ ih₂ => exact imp_replace_iff! ih₁ ih₂;
| hand _ _ ih₁ ih₂ => exact and_replace_iff! ih₁ ih₂;
| hor _ _ ih₁ ih₂ => exact or_replace_iff! ih₁ ih₂;
| _ => apply iff_id!
State after:
no goals

State before:
case hbox
α : Type u_1
inst✝ : DecidableEq α
p✝ p : Formula α
ih : 𝐓𝐫𝐢𝐯 ⊢! p ⟷ pᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! □p ⟷ (□p)ᵀ
Tactic:
simp [TrivTranslation]
State after:
case hbox
α : Type u_1
inst✝ : DecidableEq α
p✝ p : Formula α
ih : 𝐓𝐫𝐢𝐯 ⊢! p ⟷ pᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! □p ⟷ pᵀ

State before:
case hbox
α : Type u_1
inst✝ : DecidableEq α
p✝ p : Formula α
ih : 𝐓𝐫𝐢𝐯 ⊢! p ⟷ pᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! □p ⟷ pᵀ
Tactic:
apply iff_intro!
State after:
case hbox.h₁
α : Type u_1
inst✝ : DecidableEq α
p✝ p : Formula α
ih : 𝐓𝐫𝐢𝐯 ⊢! p ⟷ pᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! □p ⟶ pᵀ

case hbox.h₂
α : Type u_1
inst✝ : DecidableEq α
p✝ p : Formula α
ih : 𝐓𝐫𝐢𝐯 ⊢! p ⟷ pᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! pᵀ ⟶ □p

State before:
case hbox.h₁
α : Type u_1
inst✝ : DecidableEq α
p✝ p : Formula α
ih : 𝐓𝐫𝐢𝐯 ⊢! p ⟷ pᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! □p ⟶ pᵀ

case hbox.h₂
α : Type u_1
inst✝ : DecidableEq α
p✝ p : Formula α
ih : 𝐓𝐫𝐢𝐯 ⊢! p ⟷ pᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! pᵀ ⟶ □p
Tactic:
. exact imp_trans! axiomT! (conj₁'! ih)
State after:
case hbox.h₂
α : Type u_1
inst✝ : DecidableEq α
p✝ p : Formula α
ih : 𝐓𝐫𝐢𝐯 ⊢! p ⟷ pᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! pᵀ ⟶ □p

State before:
case hbox.h₂
α : Type u_1
inst✝ : DecidableEq α
p✝ p : Formula α
ih : 𝐓𝐫𝐢𝐯 ⊢! p ⟷ pᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! pᵀ ⟶ □p
Tactic:
. exact imp_trans! (conj₂'! ih) axiomTc!
State after:
no goals

State before:
case hbox.h₁
α : Type u_1
inst✝ : DecidableEq α
p✝ p : Formula α
ih : 𝐓𝐫𝐢𝐯 ⊢! p ⟷ pᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! □p ⟶ pᵀ
Tactic:
exact imp_trans! axiomT! (conj₁'! ih)
State after:
no goals

State before:
case hbox.h₂
α : Type u_1
inst✝ : DecidableEq α
p✝ p : Formula α
ih : 𝐓𝐫𝐢𝐯 ⊢! p ⟷ pᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! pᵀ ⟶ □p
Tactic:
exact imp_trans! (conj₂'! ih) axiomTc!
State after:
no goals

State before:
case himp
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
ih₁ : 𝐓𝐫𝐢𝐯 ⊢! p✝ ⟷ p✝ᵀ
ih₂ : 𝐓𝐫𝐢𝐯 ⊢! q✝ ⟷ q✝ᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! (p✝ ⟶ q✝) ⟷ (p✝ ⟶ q✝)ᵀ
Tactic:
exact imp_replace_iff! ih₁ ih₂
State after:
no goals

State before:
case hand
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
ih₁ : 𝐓𝐫𝐢𝐯 ⊢! p✝ ⟷ p✝ᵀ
ih₂ : 𝐓𝐫𝐢𝐯 ⊢! q✝ ⟷ q✝ᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! p✝ ⋏ q✝ ⟷ (p✝ ⋏ q✝)ᵀ
Tactic:
exact and_replace_iff! ih₁ ih₂
State after:
no goals

State before:
case hor
α : Type u_1
inst✝ : DecidableEq α
p p✝ q✝ : Formula α
ih₁ : 𝐓𝐫𝐢𝐯 ⊢! p✝ ⟷ p✝ᵀ
ih₂ : 𝐓𝐫𝐢𝐯 ⊢! q✝ ⟷ q✝ᵀ
⊢ 𝐓𝐫𝐢𝐯 ⊢! p✝ ⋎ q✝ ⟷ (p✝ ⋎ q✝)ᵀ
Tactic:
exact or_replace_iff! ih₁ ih₂
State after:
no goals

State before:
case hatom
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
a✝ : α
⊢ 𝐓𝐫𝐢𝐯 ⊢! atom a✝ ⟷ atom a✝ᵀ
Tactic:
apply iff_id!
State after:
no goals