Theorem: disconEval' (Pdl/Discon.lean)

State before:
W : Type
M : KripkeModel W
w : W
⊢ ∀ {N : ℕ} (XS : List (List Formula)), XS.length = N → (evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f)
Tactic:
intro N
State after:
W : Type
M : KripkeModel W
w : W
N : ℕ
⊢ ∀ (XS : List (List Formula)), XS.length = N → (evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f)

State before:
W : Type
M : KripkeModel W
w : W
N : ℕ
⊢ ∀ (XS : List (List Formula)), XS.length = N → (evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f)
Tactic:
refine Nat.strong_induction_on N ?_
State after:
W : Type
M : KripkeModel W
w : W
N : ℕ
⊢ ∀ (n : ℕ),
    (∀ m < n,
        ∀ (XS : List (List Formula)), XS.length = m → (evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f)) →
      ∀ (XS : List (List Formula)), XS.length = n → (evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f)

State before:
W : Type
M : KripkeModel W
w : W
N : ℕ
⊢ ∀ (n : ℕ),
    (∀ m < n,
        ∀ (XS : List (List Formula)), XS.length = m → (evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f)) →
      ∀ (XS : List (List Formula)), XS.length = n → (evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f)
Tactic:
intro n IH
State after:
W : Type
M : KripkeModel W
w : W
N n : ℕ
IH :
  ∀ m < n, ∀ (XS : List (List Formula)), XS.length = m → (evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f)
⊢ ∀ (XS : List (List Formula)), XS.length = n → (evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f)

State before:
W : Type
M : KripkeModel W
w : W
N n : ℕ
IH :
  ∀ m < n, ∀ (XS : List (List Formula)), XS.length = m → (evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f)
⊢ ∀ (XS : List (List Formula)), XS.length = n → (evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f)
Tactic:
intro XS nDef
State after:
W : Type
M : KripkeModel W
w : W
N n : ℕ
IH :
  ∀ m < n, ∀ (XS : List (List Formula)), XS.length = m → (evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f)
XS : List (List Formula)
nDef : XS.length = n
⊢ evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f

State before:
W : Type
M : KripkeModel W
w : W
N n : ℕ
IH :
  ∀ m < n, ∀ (XS : List (List Formula)), XS.length = m → (evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f)
XS : List (List Formula)
nDef : XS.length = n
⊢ evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Tactic:
subst nDef
State after:
W : Type
M : KripkeModel W
w : W
N : ℕ
XS : List (List Formula)
IH :
  ∀ m < XS.length,
    ∀ (XS : List (List Formula)), XS.length = m → (evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f)
⊢ evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f

State before:
W : Type
M : KripkeModel W
w : W
N : ℕ
XS : List (List Formula)
IH :
  ∀ m < XS.length,
    ∀ (XS : List (List Formula)), XS.length = m → (evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f)
⊢ evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Tactic:
cases' XS with X XS
State after:
case nil
W : Type
M : KripkeModel W
w : W
N : ℕ
IH :
  ∀ m < [].length,
    ∀ (XS : List (List Formula)), XS.length = m → (evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f)
⊢ evaluate M w (discon []) ↔ ∃ Y ∈ [], ∀ f ∈ Y, evaluate M w f

case cons
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH :
  ∀ m < (X :: XS).length,
    ∀ (XS : List (List Formula)), XS.length = m → (evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f)
⊢ evaluate M w (discon (X :: XS)) ↔ ∃ Y ∈ X :: XS, ∀ f ∈ Y, evaluate M w f

State before:
case cons
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH :
  ∀ m < (X :: XS).length,
    ∀ (XS : List (List Formula)), XS.length = m → (evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f)
⊢ evaluate M w (discon (X :: XS)) ↔ ∃ Y ∈ X :: XS, ∀ f ∈ Y, evaluate M w f
Tactic:
specialize IH XS.length (by simp) XS (by rfl)
State after:
case cons
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
⊢ evaluate M w (discon (X :: XS)) ↔ ∃ Y ∈ X :: XS, ∀ f ∈ Y, evaluate M w f

State before:
case cons
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
⊢ evaluate M w (discon (X :: XS)) ↔ ∃ Y ∈ X :: XS, ∀ f ∈ Y, evaluate M w f
Tactic:
rw [disconEvalHT]
State after:
case cons
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
⊢ evaluate M w (Con X⋁discon XS) ↔ ∃ Y ∈ X :: XS, ∀ f ∈ Y, evaluate M w f

State before:
case cons
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
⊢ evaluate M w (Con X⋁discon XS) ↔ ∃ Y ∈ X :: XS, ∀ f ∈ Y, evaluate M w f
Tactic:
rw [evalDis]
State after:
case cons
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
⊢ evaluate M w (Con X) ∨ evaluate M w (discon XS) ↔ ∃ Y ∈ X :: XS, ∀ f ∈ Y, evaluate M w f

State before:
case cons
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
⊢ evaluate M w (Con X) ∨ evaluate M w (discon XS) ↔ ∃ Y ∈ X :: XS, ∀ f ∈ Y, evaluate M w f
Tactic:
rw [IH]
State after:
case cons
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
⊢ (evaluate M w (Con X) ∨ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f) ↔ ∃ Y ∈ X :: XS, ∀ f ∈ Y, evaluate M w f

State before:
case cons
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
⊢ (evaluate M w (Con X) ∨ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f) ↔ ∃ Y ∈ X :: XS, ∀ f ∈ Y, evaluate M w f
Tactic:
constructor
State after:
case cons.mp
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
⊢ (evaluate M w (Con X) ∨ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f) → ∃ Y ∈ X :: XS, ∀ f ∈ Y, evaluate M w f

case cons.mpr
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
⊢ (∃ Y ∈ X :: XS, ∀ f ∈ Y, evaluate M w f) → evaluate M w (Con X) ∨ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f

State before:
case nil
W : Type
M : KripkeModel W
w : W
N : ℕ
IH :
  ∀ m < [].length,
    ∀ (XS : List (List Formula)), XS.length = m → (evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f)
⊢ evaluate M w (discon []) ↔ ∃ Y ∈ [], ∀ f ∈ Y, evaluate M w f
Tactic:
simp
State after:
no goals

State before:
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH :
  ∀ m < (X :: XS).length,
    ∀ (XS : List (List Formula)), XS.length = m → (evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f)
⊢ XS.length < (X :: XS).length
Tactic:
simp
State after:
no goals

State before:
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH :
  ∀ m < (X :: XS).length,
    ∀ (XS : List (List Formula)), XS.length = m → (evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f)
⊢ XS.length = XS.length
Tactic:
rfl
State after:
no goals

State before:
case cons.mp
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
⊢ (evaluate M w (Con X) ∨ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f) → ∃ Y ∈ X :: XS, ∀ f ∈ Y, evaluate M w f
Tactic:
intro lhs
State after:
case cons.mp
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
lhs : evaluate M w (Con X) ∨ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
⊢ ∃ Y ∈ X :: XS, ∀ f ∈ Y, evaluate M w f

State before:
case cons.mp
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
lhs : evaluate M w (Con X) ∨ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
⊢ ∃ Y ∈ X :: XS, ∀ f ∈ Y, evaluate M w f
Tactic:
cases' lhs with lhs lhs
State after:
case cons.mp.inl
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
lhs : evaluate M w (Con X)
⊢ ∃ Y ∈ X :: XS, ∀ f ∈ Y, evaluate M w f

case cons.mp.inr
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
lhs : ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
⊢ ∃ Y ∈ X :: XS, ∀ f ∈ Y, evaluate M w f

State before:
case cons.mp.inl
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
lhs : evaluate M w (Con X)
⊢ ∃ Y ∈ X :: XS, ∀ f ∈ Y, evaluate M w f
Tactic:
use X
State after:
case h
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
lhs : evaluate M w (Con X)
⊢ X ∈ X :: XS ∧ ∀ f ∈ X, evaluate M w f

State before:
case h
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
lhs : evaluate M w (Con X)
⊢ X ∈ X :: XS ∧ ∀ f ∈ X, evaluate M w f
Tactic:
simp
State after:
case h
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
lhs : evaluate M w (Con X)
⊢ ∀ f ∈ X, evaluate M w f

State before:
case h
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
lhs : evaluate M w (Con X)
⊢ ∀ f ∈ X, evaluate M w f
Tactic:
rw [conEval] at lhs
State after:
case h
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
lhs : ∀ f ∈ X, evaluate M w f
⊢ ∀ f ∈ X, evaluate M w f

State before:
case h
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
lhs : ∀ f ∈ X, evaluate M w f
⊢ ∀ f ∈ X, evaluate M w f
Tactic:
tauto
State after:
no goals

State before:
case cons.mp.inr
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
lhs : ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
⊢ ∃ Y ∈ X :: XS, ∀ f ∈ Y, evaluate M w f
Tactic:
cases' lhs with Y claim
State after:
case cons.mp.inr.intro
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Y : List Formula
claim : Y ∈ XS ∧ ∀ f ∈ Y, evaluate M w f
⊢ ∃ Y ∈ X :: XS, ∀ f ∈ Y, evaluate M w f

State before:
case cons.mp.inr.intro
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Y : List Formula
claim : Y ∈ XS ∧ ∀ f ∈ Y, evaluate M w f
⊢ ∃ Y ∈ X :: XS, ∀ f ∈ Y, evaluate M w f
Tactic:
use Y
State after:
case h
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Y : List Formula
claim : Y ∈ XS ∧ ∀ f ∈ Y, evaluate M w f
⊢ Y ∈ X :: XS ∧ ∀ f ∈ Y, evaluate M w f

State before:
case h
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Y : List Formula
claim : Y ∈ XS ∧ ∀ f ∈ Y, evaluate M w f
⊢ Y ∈ X :: XS ∧ ∀ f ∈ Y, evaluate M w f
Tactic:
simp
State after:
case h
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Y : List Formula
claim : Y ∈ XS ∧ ∀ f ∈ Y, evaluate M w f
⊢ (Y = X ∨ Y ∈ XS) ∧ ∀ f ∈ Y, evaluate M w f

State before:
case h
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Y : List Formula
claim : Y ∈ XS ∧ ∀ f ∈ Y, evaluate M w f
⊢ (Y = X ∨ Y ∈ XS) ∧ ∀ f ∈ Y, evaluate M w f
Tactic:
tauto
State after:
no goals

State before:
case cons.mpr
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
⊢ (∃ Y ∈ X :: XS, ∀ f ∈ Y, evaluate M w f) → evaluate M w (Con X) ∨ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Tactic:
intro rhs
State after:
case cons.mpr
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
rhs : ∃ Y ∈ X :: XS, ∀ f ∈ Y, evaluate M w f
⊢ evaluate M w (Con X) ∨ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f

State before:
case cons.mpr
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
rhs : ∃ Y ∈ X :: XS, ∀ f ∈ Y, evaluate M w f
⊢ evaluate M w (Con X) ∨ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Tactic:
cases' rhs with Y rhs
State after:
case cons.mpr.intro
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Y : List Formula
rhs : Y ∈ X :: XS ∧ ∀ f ∈ Y, evaluate M w f
⊢ evaluate M w (Con X) ∨ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f

State before:
case cons.mpr.intro
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Y : List Formula
rhs : Y ∈ X :: XS ∧ ∀ f ∈ Y, evaluate M w f
⊢ evaluate M w (Con X) ∨ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Tactic:
cases' rhs with Y_in Ysat
State after:
case cons.mpr.intro.intro
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Y : List Formula
Y_in : Y ∈ X :: XS
Ysat : ∀ f ∈ Y, evaluate M w f
⊢ evaluate M w (Con X) ∨ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f

State before:
case cons.mpr.intro.intro
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Y : List Formula
Y_in : Y ∈ X :: XS
Ysat : ∀ f ∈ Y, evaluate M w f
⊢ evaluate M w (Con X) ∨ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Tactic:
simp at Y_in
State after:
case cons.mpr.intro.intro
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Y : List Formula
Ysat : ∀ f ∈ Y, evaluate M w f
Y_in : Y = X ∨ Y ∈ XS
⊢ evaluate M w (Con X) ∨ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f

State before:
case cons.mpr.intro.intro
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Y : List Formula
Ysat : ∀ f ∈ Y, evaluate M w f
Y_in : Y = X ∨ Y ∈ XS
⊢ evaluate M w (Con X) ∨ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Tactic:
cases' Y_in with Y_in
State after:
case cons.mpr.intro.intro.inl
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Y : List Formula
Ysat : ∀ f ∈ Y, evaluate M w f
Y_in : Y = X
⊢ evaluate M w (Con X) ∨ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f

case cons.mpr.intro.intro.inr
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Y : List Formula
Ysat : ∀ f ∈ Y, evaluate M w f
h✝ : Y ∈ XS
⊢ evaluate M w (Con X) ∨ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f

State before:
case cons.mpr.intro.intro.inl
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Y : List Formula
Ysat : ∀ f ∈ Y, evaluate M w f
Y_in : Y = X
⊢ evaluate M w (Con X) ∨ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Tactic:
left
State after:
case cons.mpr.intro.intro.inl.h
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Y : List Formula
Ysat : ∀ f ∈ Y, evaluate M w f
Y_in : Y = X
⊢ evaluate M w (Con X)

State before:
case cons.mpr.intro.intro.inl.h
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Y : List Formula
Ysat : ∀ f ∈ Y, evaluate M w f
Y_in : Y = X
⊢ evaluate M w (Con X)
Tactic:
subst Y_in
State after:
case cons.mpr.intro.intro.inl.h
W : Type
M : KripkeModel W
w : W
N : ℕ
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Y : List Formula
Ysat : ∀ f ∈ Y, evaluate M w f
⊢ evaluate M w (Con Y)

State before:
case cons.mpr.intro.intro.inl.h
W : Type
M : KripkeModel W
w : W
N : ℕ
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Y : List Formula
Ysat : ∀ f ∈ Y, evaluate M w f
⊢ evaluate M w (Con Y)
Tactic:
rw [conEval]
State after:
case cons.mpr.intro.intro.inl.h
W : Type
M : KripkeModel W
w : W
N : ℕ
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Y : List Formula
Ysat : ∀ f ∈ Y, evaluate M w f
⊢ ∀ f ∈ Y, evaluate M w f

State before:
case cons.mpr.intro.intro.inl.h
W : Type
M : KripkeModel W
w : W
N : ℕ
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Y : List Formula
Ysat : ∀ f ∈ Y, evaluate M w f
⊢ ∀ f ∈ Y, evaluate M w f
Tactic:
tauto
State after:
no goals

State before:
case cons.mpr.intro.intro.inr
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Y : List Formula
Ysat : ∀ f ∈ Y, evaluate M w f
h✝ : Y ∈ XS
⊢ evaluate M w (Con X) ∨ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Tactic:
right
State after:
case cons.mpr.intro.intro.inr.h
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Y : List Formula
Ysat : ∀ f ∈ Y, evaluate M w f
h✝ : Y ∈ XS
⊢ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f

State before:
case cons.mpr.intro.intro.inr.h
W : Type
M : KripkeModel W
w : W
N : ℕ
X : List Formula
XS : List (List Formula)
IH : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Y : List Formula
Ysat : ∀ f ∈ Y, evaluate M w f
h✝ : Y ∈ XS
⊢ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Tactic:
use Y
State after:
no goals