Theorem: disconEval (Bml/bigConDis.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 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, evalDis, 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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