Theorem: equivSat (Pdl/Semantics.lean)

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

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

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

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

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