internlm/Lean-Github huggingface dataset:
Theorem: disconEval'
Proof 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 ?_
Proof 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)
Theorem: disconEval'
Proof 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
Proof 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)
Theorem: disconEval'
Proof 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
Proof 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
Theorem: disconEval'
Proof 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
Proof 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
Theorem: disconEval'
Proof 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
Proof 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
Theorem: disconEval'
Proof 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)
Proof 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
Theorem: disconEval'
Proof 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]
Proof 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
Theorem: disconEval'
Proof 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]
Proof 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
Theorem: disconEval'
Proof 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]
Proof 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
Theorem: disconEval'
Proof 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
Proof 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
Theorem: disconEval'
Proof 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
Proof state after:
no goals
Theorem: disconEval'
Proof 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
Proof state after:
no goals
Theorem: disconEval'
Proof 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
Proof state after:
no goals
Theorem: disconEval'
Proof 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
Proof 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
Theorem: disconEval'
Proof 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
Proof 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
Theorem: disconEval'
Proof 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
Proof 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
Theorem: disconEval'
Proof 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
Proof 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
Theorem: disconEval'
Proof 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
Proof 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
Theorem: disconEval'
Proof 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
Proof state after:
no goals
Theorem: disconEval'
Proof 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
Proof 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
Theorem: disconEval'
Proof 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
Proof 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
Theorem: disconEval'
Proof 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
Proof 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
Theorem: disconEval'
Proof 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
Proof state after:
no goals
Theorem: disconEval'
Proof 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
Proof 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
Theorem: disconEval'
Proof 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
Proof 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
Theorem: disconEval'
Proof 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
Proof 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
Theorem: disconEval'
Proof 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
Proof 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
Theorem: disconEval'
Proof 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
Proof 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
Theorem: disconEval'
Proof 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
Proof 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)
Theorem: disconEval'
Proof 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
Proof 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)
Theorem: disconEval'
Proof 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]
Proof 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
Theorem: disconEval'
Proof 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
Proof state after:
no goals
Theorem: disconEval'
Proof 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
Proof 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
Theorem: disconEval'
Proof 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
Proof state after:
no goals
Theorem: disconEval
Proof state before:
W : Type
M : KripkeModel W
w : W
⊢ ∀ (XS : List (List Formula)), evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Tactic:
intro XS
Proof state after:
W : Type
M : KripkeModel W
w : W
XS : List (List Formula)
⊢ evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Theorem: disconEval
Proof state before:
W : Type
M : KripkeModel W
w : W
XS : List (List Formula)
⊢ evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Tactic:
apply disconEval' XS rfl
Proof state after:
no goals
Theorem: disconAnd
Proof state before:
XS YS : List (List Formula)
⊢ discon (XS⊎YS)≡discon XS⋀discon YS
Tactic:
unfold semEquiv
Proof state after:
XS YS : List (List Formula)
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w (discon (XS⊎YS)) ↔ evaluate M w (discon XS⋀discon YS)
Theorem: disconAnd
Proof state before:
XS YS : List (List Formula)
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w (discon (XS⊎YS)) ↔ evaluate M w (discon XS⋀discon YS)
Tactic:
intro W M w
Proof state after:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (discon (XS⊎YS)) ↔ evaluate M w (discon XS⋀discon YS)
Theorem: disconAnd
Proof state before:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (discon (XS⊎YS)) ↔ evaluate M w (discon XS⋀discon YS)
Tactic:
rw [disconEval (XS ⊎ YS)]
Proof state after:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ (∃ Y ∈ XS⊎YS, ∀ f ∈ Y, evaluate M w f) ↔ evaluate M w (discon XS⋀discon YS)
Theorem: disconAnd
Proof state before:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ (∃ Y ∈ XS⊎YS, ∀ f ∈ Y, evaluate M w f) ↔ evaluate M w (discon XS⋀discon YS)
Tactic:
simp
Proof state after:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ (∃ a ∈ XS, ∃ b ∈ YS, ∀ (f : Formula), f ∈ a ∨ f ∈ b → evaluate M w f) ↔
    evaluate M w (discon XS) ∧ evaluate M w (discon YS)
Theorem: disconAnd
Proof state before:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ (∃ a ∈ XS, ∃ b ∈ YS, ∀ (f : Formula), f ∈ a ∨ f ∈ b → evaluate M w f) ↔
    evaluate M w (discon XS) ∧ evaluate M w (discon YS)
Tactic:
rw [disconEval XS]
Proof state after:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ (∃ a ∈ XS, ∃ b ∈ YS, ∀ (f : Formula), f ∈ a ∨ f ∈ b → evaluate M w f) ↔
    (∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f) ∧ evaluate M w (discon YS)
Theorem: disconAnd
Proof state before:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ (∃ a ∈ XS, ∃ b ∈ YS, ∀ (f : Formula), f ∈ a ∨ f ∈ b → evaluate M w f) ↔
    (∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f) ∧ evaluate M w (discon YS)
Tactic:
rw [disconEval YS]
Proof state after:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ (∃ a ∈ XS, ∃ b ∈ YS, ∀ (f : Formula), f ∈ a ∨ f ∈ b → evaluate M w f) ↔
    (∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f) ∧ ∃ Y ∈ YS, ∀ f ∈ Y, evaluate M w f
Theorem: disconAnd
Proof state before:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ (∃ a ∈ XS, ∃ b ∈ YS, ∀ (f : Formula), f ∈ a ∨ f ∈ b → evaluate M w f) ↔
    (∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f) ∧ ∃ Y ∈ YS, ∀ f ∈ Y, evaluate M w f
Tactic:
aesop
Proof state after:
no goals
Theorem: disconOr
Proof state before:
XS YS : List (List Formula)
⊢ discon (XS ∪ YS)≡discon XS⋁discon YS
Tactic:
unfold semEquiv
Proof state after:
XS YS : List (List Formula)
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w (discon (XS ∪ YS)) ↔ evaluate M w (discon XS⋁discon YS)
Theorem: disconOr
Proof state before:
XS YS : List (List Formula)
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w (discon (XS ∪ YS)) ↔ evaluate M w (discon XS⋁discon YS)
Tactic:
intro W M w
Proof state after:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (discon (XS ∪ YS)) ↔ evaluate M w (discon XS⋁discon YS)
Theorem: disconOr
Proof state before:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (discon (XS ∪ YS)) ↔ evaluate M w (discon XS⋁discon YS)
Tactic:
rw [disconEval (XS ∪ YS)]
Proof state after:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ (∃ Y ∈ XS ∪ YS, ∀ f ∈ Y, evaluate M w f) ↔ evaluate M w (discon XS⋁discon YS)
Theorem: disconOr
Proof state before:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ (∃ Y ∈ XS ∪ YS, ∀ f ∈ Y, evaluate M w f) ↔ evaluate M w (discon XS⋁discon YS)
Tactic:
simp
Proof state after:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ (∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, evaluate M w f) ↔ ¬evaluate M w (discon XS) → evaluate M w (discon YS)