Theorem: conEval (Pdl/Discon.lean)

State before:
W : Type
M : KripkeModel W
X : List Formula
w : W
⊢ evaluate M w (Con X) ↔ ∀ f ∈ X, evaluate M w f
Tactic:
induction' X with f X IH
State after:
case nil
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (Con []) ↔ ∀ f ∈ [], evaluate M w f

case cons
W : Type
M : KripkeModel W
w : W
f : Formula
X : List Formula
IH : evaluate M w (Con X) ↔ ∀ f ∈ X, evaluate M w f
⊢ evaluate M w (Con (f :: X)) ↔ ∀ f_1 ∈ f :: X, evaluate M w f_1

State before:
case nil
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (Con []) ↔ ∀ f ∈ [], evaluate M w f
Tactic:
simp
State after:
no goals

State before:
case cons
W : Type
M : KripkeModel W
w : W
f : Formula
X : List Formula
IH : evaluate M w (Con X) ↔ ∀ f ∈ X, evaluate M w f
⊢ evaluate M w (Con (f :: X)) ↔ ∀ f_1 ∈ f :: X, evaluate M w f_1
Tactic:
rw [conEvalHT]
State after:
case cons
W : Type
M : KripkeModel W
w : W
f : Formula
X : List Formula
IH : evaluate M w (Con X) ↔ ∀ f ∈ X, evaluate M w f
⊢ evaluate M w f ∧ evaluate M w (Con X) ↔ ∀ f_1 ∈ f :: X, evaluate M w f_1

State before:
case cons
W : Type
M : KripkeModel W
w : W
f : Formula
X : List Formula
IH : evaluate M w (Con X) ↔ ∀ f ∈ X, evaluate M w f
⊢ evaluate M w f ∧ evaluate M w (Con X) ↔ ∀ f_1 ∈ f :: X, evaluate M w f_1
Tactic:
simp
State after:
case cons
W : Type
M : KripkeModel W
w : W
f : Formula
X : List Formula
IH : evaluate M w (Con X) ↔ ∀ f ∈ X, evaluate M w f
⊢ evaluate M w f → (evaluate M w (Con X) ↔ ∀ a ∈ X, evaluate M w a)

State before:
case cons
W : Type
M : KripkeModel W
w : W
f : Formula
X : List Formula
IH : evaluate M w (Con X) ↔ ∀ f ∈ X, evaluate M w f
⊢ evaluate M w f → (evaluate M w (Con X) ↔ ∀ a ∈ X, evaluate M w a)
Tactic:
intro _
State after:
case cons
W : Type
M : KripkeModel W
w : W
f : Formula
X : List Formula
IH : evaluate M w (Con X) ↔ ∀ f ∈ X, evaluate M w f
a✝ : evaluate M w f
⊢ evaluate M w (Con X) ↔ ∀ a ∈ X, evaluate M w a

State before:
case cons
W : Type
M : KripkeModel W
w : W
f : Formula
X : List Formula
IH : evaluate M w (Con X) ↔ ∀ f ∈ X, evaluate M w f
a✝ : evaluate M w f
⊢ evaluate M w (Con X) ↔ ∀ a ∈ X, evaluate M w a
Tactic:
assumption
State after:
no goals