Theorem: equiv_iff (Pdl/Semantics.lean)

State before:
φ ψ : Formula
φ_eq_ψ : φ≡ψ
⊢ ∀ {W : Type} {M : KripkeModel W} {w : W}, (M, w)⊨φ ↔ (M, w)⊨ψ
Tactic:
intro W M w
State after:
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
⊢ (M, w)⊨φ ↔ (M, w)⊨ψ

State before:
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
⊢ (M, w)⊨φ ↔ (M, w)⊨ψ
Tactic:
constructor
State after:
case mp
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
⊢ (M, w)⊨φ → (M, w)⊨ψ

case mpr
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
⊢ (M, w)⊨ψ → (M, w)⊨φ

State before:
case mp
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
⊢ (M, w)⊨φ → (M, w)⊨ψ
Tactic:
intro
State after:
case mp
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨φ
⊢ (M, w)⊨ψ

State before:
case mp
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨φ
⊢ (M, w)⊨ψ
Tactic:
have : evaluate M w φ := by tauto
State after:
case mp
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨φ
this : evaluate M w φ
⊢ (M, w)⊨ψ

State before:
case mp
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨φ
this : evaluate M w φ
⊢ (M, w)⊨ψ
Tactic:
rw [φ_eq_ψ] at this
State after:
case mp
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨φ
this : evaluate M w ψ
⊢ (M, w)⊨ψ

State before:
case mp
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨φ
this : evaluate M w ψ
⊢ (M, w)⊨ψ
Tactic:
tauto
State after:
no goals

State before:
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨φ
⊢ evaluate M w φ
Tactic:
tauto
State after:
no goals

State before:
case mpr
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
⊢ (M, w)⊨ψ → (M, w)⊨φ
Tactic:
intro
State after:
case mpr
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨ψ
⊢ (M, w)⊨φ

State before:
case mpr
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨ψ
⊢ (M, w)⊨φ
Tactic:
have : evaluate M w ψ := by tauto
State after:
case mpr
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨ψ
this : evaluate M w ψ
⊢ (M, w)⊨φ

State before:
case mpr
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨ψ
this : evaluate M w ψ
⊢ (M, w)⊨φ
Tactic:
rw [← φ_eq_ψ] at this
State after:
case mpr
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨ψ
this : evaluate M w φ
⊢ (M, w)⊨φ

State before:
case mpr
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨ψ
this : evaluate M w φ
⊢ (M, w)⊨φ
Tactic:
tauto
State after:
no goals

State before:
φ ψ : Formula
φ_eq_ψ : φ≡ψ
W : Type
M : KripkeModel W
w : W
a✝ : (M, w)⊨ψ
⊢ evaluate M w ψ
Tactic:
tauto
State after:
no goals