Theorem: repl_in_F_equiv (Pdl/Substitution.lean)

State before:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
⊢ φ1≡φ2 → repl_in_F x ψ φ1≡repl_in_F x ψ φ2
Tactic:
intro hyp
State after:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
⊢ repl_in_F x ψ φ1≡repl_in_F x ψ φ2

State before:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
⊢ repl_in_F x ψ φ1≡repl_in_F x ψ φ2
Tactic:
intro W M w
State after:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (repl_in_F x ψ φ1) ↔ evaluate M w (repl_in_F x ψ φ2)

State before:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (repl_in_F x ψ φ1) ↔ evaluate M w (repl_in_F x ψ φ2)
Tactic:
have claim1 := repl_in_model_sat_iff x ψ φ1 M w
State after:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
claim1 : (M, w)⊨repl_in_F x ψ φ1 ↔ (repl_in_model x ψ M, w)⊨φ1
⊢ evaluate M w (repl_in_F x ψ φ1) ↔ evaluate M w (repl_in_F x ψ φ2)

State before:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
claim1 : (M, w)⊨repl_in_F x ψ φ1 ↔ (repl_in_model x ψ M, w)⊨φ1
⊢ evaluate M w (repl_in_F x ψ φ1) ↔ evaluate M w (repl_in_F x ψ φ2)
Tactic:
have claim2 := repl_in_model_sat_iff x ψ φ2 M w
State after:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
claim1 : (M, w)⊨repl_in_F x ψ φ1 ↔ (repl_in_model x ψ M, w)⊨φ1
claim2 : (M, w)⊨repl_in_F x ψ φ2 ↔ (repl_in_model x ψ M, w)⊨φ2
⊢ evaluate M w (repl_in_F x ψ φ1) ↔ evaluate M w (repl_in_F x ψ φ2)

State before:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
claim1 : (M, w)⊨repl_in_F x ψ φ1 ↔ (repl_in_model x ψ M, w)⊨φ1
claim2 : (M, w)⊨repl_in_F x ψ φ2 ↔ (repl_in_model x ψ M, w)⊨φ2
⊢ evaluate M w (repl_in_F x ψ φ1) ↔ evaluate M w (repl_in_F x ψ φ2)
Tactic:
simp only [evaluatePoint, modelCanSemImplyForm] at *
State after:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
claim1 : evaluate M w (repl_in_F x ψ φ1) ↔ evaluate (repl_in_model x ψ M) w φ1
claim2 : evaluate M w (repl_in_F x ψ φ2) ↔ evaluate (repl_in_model x ψ M) w φ2
⊢ evaluate M w (repl_in_F x ψ φ1) ↔ evaluate M w (repl_in_F x ψ φ2)

State before:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
claim1 : evaluate M w (repl_in_F x ψ φ1) ↔ evaluate (repl_in_model x ψ M) w φ1
claim2 : evaluate M w (repl_in_F x ψ φ2) ↔ evaluate (repl_in_model x ψ M) w φ2
⊢ evaluate M w (repl_in_F x ψ φ1) ↔ evaluate M w (repl_in_F x ψ φ2)
Tactic:
rw [claim1]
State after:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
claim1 : evaluate M w (repl_in_F x ψ φ1) ↔ evaluate (repl_in_model x ψ M) w φ1
claim2 : evaluate M w (repl_in_F x ψ φ2) ↔ evaluate (repl_in_model x ψ M) w φ2
⊢ evaluate (repl_in_model x ψ M) w φ1 ↔ evaluate M w (repl_in_F x ψ φ2)

State before:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
claim1 : evaluate M w (repl_in_F x ψ φ1) ↔ evaluate (repl_in_model x ψ M) w φ1
claim2 : evaluate M w (repl_in_F x ψ φ2) ↔ evaluate (repl_in_model x ψ M) w φ2
⊢ evaluate (repl_in_model x ψ M) w φ1 ↔ evaluate M w (repl_in_F x ψ φ2)
Tactic:
rw [claim2]
State after:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
claim1 : evaluate M w (repl_in_F x ψ φ1) ↔ evaluate (repl_in_model x ψ M) w φ1
claim2 : evaluate M w (repl_in_F x ψ φ2) ↔ evaluate (repl_in_model x ψ M) w φ2
⊢ evaluate (repl_in_model x ψ M) w φ1 ↔ evaluate (repl_in_model x ψ M) w φ2

State before:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
claim1 : evaluate M w (repl_in_F x ψ φ1) ↔ evaluate (repl_in_model x ψ M) w φ1
claim2 : evaluate M w (repl_in_F x ψ φ2) ↔ evaluate (repl_in_model x ψ M) w φ2
⊢ evaluate (repl_in_model x ψ M) w φ1 ↔ evaluate (repl_in_model x ψ M) w φ2
Tactic:
have := @equiv_iff φ1 φ2 hyp W (repl_in_model x ψ M) w
State after:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
claim1 : evaluate M w (repl_in_F x ψ φ1) ↔ evaluate (repl_in_model x ψ M) w φ1
claim2 : evaluate M w (repl_in_F x ψ φ2) ↔ evaluate (repl_in_model x ψ M) w φ2
this : (repl_in_model x ψ M, w)⊨φ1 ↔ (repl_in_model x ψ M, w)⊨φ2
⊢ evaluate (repl_in_model x ψ M) w φ1 ↔ evaluate (repl_in_model x ψ M) w φ2

State before:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
claim1 : evaluate M w (repl_in_F x ψ φ1) ↔ evaluate (repl_in_model x ψ M) w φ1
claim2 : evaluate M w (repl_in_F x ψ φ2) ↔ evaluate (repl_in_model x ψ M) w φ2
this : (repl_in_model x ψ M, w)⊨φ1 ↔ (repl_in_model x ψ M, w)⊨φ2
⊢ evaluate (repl_in_model x ψ M) w φ1 ↔ evaluate (repl_in_model x ψ M) w φ2
Tactic:
simp only [evaluatePoint, modelCanSemImplyForm] at *
State after:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
claim1 : evaluate M w (repl_in_F x ψ φ1) ↔ evaluate (repl_in_model x ψ M) w φ1
claim2 : evaluate M w (repl_in_F x ψ φ2) ↔ evaluate (repl_in_model x ψ M) w φ2
this : evaluate (repl_in_model x ψ M) w φ1 ↔ evaluate (repl_in_model x ψ M) w φ2
⊢ evaluate (repl_in_model x ψ M) w φ1 ↔ evaluate (repl_in_model x ψ M) w φ2

State before:
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
claim1 : evaluate M w (repl_in_F x ψ φ1) ↔ evaluate (repl_in_model x ψ M) w φ1
claim2 : evaluate M w (repl_in_F x ψ φ2) ↔ evaluate (repl_in_model x ψ M) w φ2
this : evaluate (repl_in_model x ψ M) w φ1 ↔ evaluate (repl_in_model x ψ M) w φ2
⊢ evaluate (repl_in_model x ψ M) w φ1 ↔ evaluate (repl_in_model x ψ M) w φ2
Tactic:
exact this
State after:
no goals