Theorem: conEval (Bml/bigConDis.lean)

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

case cons
W : Type
M : KripkeModel W
w : W
f : Formula
X : List Formula
IH : Evaluate (M, w) (bigCon X) ↔ ∀ f ∈ X, Evaluate (M, w) f
⊢ Evaluate (M, w) (bigCon (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) (bigCon []) ↔ ∀ 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) (bigCon X) ↔ ∀ f ∈ X, Evaluate (M, w) f
⊢ Evaluate (M, w) (bigCon (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) (bigCon X) ↔ ∀ f ∈ X, Evaluate (M, w) f
⊢ Evaluate (M, w) f ∧ Evaluate (M, w) (bigCon 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) (bigCon X) ↔ ∀ f ∈ X, Evaluate (M, w) f
⊢ Evaluate (M, w) f ∧ Evaluate (M, w) (bigCon 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) (bigCon X) ↔ ∀ f ∈ X, Evaluate (M, w) f
⊢ Evaluate (M, w) f → (Evaluate (M, w) (bigCon 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) (bigCon X) ↔ ∀ f ∈ X, Evaluate (M, w) f
⊢ Evaluate (M, w) f → (Evaluate (M, w) (bigCon 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) (bigCon X) ↔ ∀ f ∈ X, Evaluate (M, w) f
a✝ : Evaluate (M, w) f
⊢ Evaluate (M, w) (bigCon 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) (bigCon X) ↔ ∀ f ∈ X, Evaluate (M, w) f
a✝ : Evaluate (M, w) f
⊢ Evaluate (M, w) (bigCon X) ↔ ∀ a ∈ X, Evaluate (M, w) a
Tactic:
assumption
State after:
no goals