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

State before:
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
⊢ 𝐕𝐞𝐫 ⊢! p ⟷ pⱽ
Tactic:
induction p using Formula.rec' with
| hbox =>
  apply iff_intro!;
  . exact imply₁'! verum!
  . exact dhyp! (by simp)
| 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 α
a✝ : 𝐕𝐞𝐫 ⊢! p✝ ⟷ p✝ⱽ
⊢ 𝐕𝐞𝐫 ⊢! □p✝ ⟷ (□p✝)ⱽ
Tactic:
apply iff_intro!
State after:
case hbox.h₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
a✝ : 𝐕𝐞𝐫 ⊢! p✝ ⟷ p✝ⱽ
⊢ 𝐕𝐞𝐫 ⊢! □p✝ ⟶ (□p✝)ⱽ

case hbox.h₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
a✝ : 𝐕𝐞𝐫 ⊢! p✝ ⟷ p✝ⱽ
⊢ 𝐕𝐞𝐫 ⊢! (□p✝)ⱽ ⟶ □p✝

State before:
case hbox.h₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
a✝ : 𝐕𝐞𝐫 ⊢! p✝ ⟷ p✝ⱽ
⊢ 𝐕𝐞𝐫 ⊢! □p✝ ⟶ (□p✝)ⱽ

case hbox.h₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
a✝ : 𝐕𝐞𝐫 ⊢! p✝ ⟷ p✝ⱽ
⊢ 𝐕𝐞𝐫 ⊢! (□p✝)ⱽ ⟶ □p✝
Tactic:
. exact imply₁'! verum!
State after:
case hbox.h₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
a✝ : 𝐕𝐞𝐫 ⊢! p✝ ⟷ p✝ⱽ
⊢ 𝐕𝐞𝐫 ⊢! (□p✝)ⱽ ⟶ □p✝

State before:
case hbox.h₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
a✝ : 𝐕𝐞𝐫 ⊢! p✝ ⟷ p✝ⱽ
⊢ 𝐕𝐞𝐫 ⊢! (□p✝)ⱽ ⟶ □p✝
Tactic:
. exact dhyp! (by simp)
State after:
no goals

State before:
case hbox.h₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
a✝ : 𝐕𝐞𝐫 ⊢! p✝ ⟷ p✝ⱽ
⊢ 𝐕𝐞𝐫 ⊢! □p✝ ⟶ (□p✝)ⱽ
Tactic:
exact imply₁'! verum!
State after:
no goals

State before:
case hbox.h₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
a✝ : 𝐕𝐞𝐫 ⊢! p✝ ⟷ p✝ⱽ
⊢ 𝐕𝐞𝐫 ⊢! (□p✝)ⱽ ⟶ □p✝
Tactic:
exact dhyp! (by simp)
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
a✝ : 𝐕𝐞𝐫 ⊢! p✝ ⟷ p✝ⱽ
⊢ 𝐕𝐞𝐫 ⊢! □p✝
Tactic:
simp
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