Theorem: disEval (Pdl/Discon.lean)

State before:
W : Type
M : KripkeModel W
X : List Formula
w : W
⊢ evaluate M w (dis 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 (dis []) ↔ ∃ f ∈ [], evaluate M w f

case cons
W : Type
M : KripkeModel W
w : W
f : Formula
X : List Formula
IH : evaluate M w (dis X) ↔ ∃ f ∈ X, evaluate M w f
⊢ evaluate M w (dis (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 (dis []) ↔ ∃ 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 (dis X) ↔ ∃ f ∈ X, evaluate M w f
⊢ evaluate M w (dis (f :: X)) ↔ ∃ f_1 ∈ f :: X, evaluate M w f_1
Tactic:
rw [disEvalHT]
State after:
case cons
W : Type
M : KripkeModel W
w : W
f : Formula
X : List Formula
IH : evaluate M w (dis X) ↔ ∃ f ∈ X, evaluate M w f
⊢ evaluate M w f ∨ evaluate M w (dis 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 (dis X) ↔ ∃ f ∈ X, evaluate M w f
⊢ evaluate M w f ∨ evaluate M w (dis X) ↔ ∃ f_1 ∈ f :: X, evaluate M w f_1
Tactic:
simp [IH]
State after:
no goals