internlm/Lean-Github huggingface dataset:
Theorem: vocOfBigDis
Proof state before:
case inl
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigDis tail) → ∃ φ ∈ tail, x ∈ voc φ
hyp : x ∈ voc (bigDis (head :: tail))
h✝ : x ∈ vocabOfFormula head
⊢ ∃ φ ∈ head :: tail, x ∈ voc φ
Tactic:
simp
Proof state after:
case inl
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigDis tail) → ∃ φ ∈ tail, x ∈ voc φ
hyp : x ∈ voc (bigDis (head :: tail))
h✝ : x ∈ vocabOfFormula head
⊢ x ∈ vocabOfFormula head ∨ ∃ a ∈ tail, x ∈ vocabOfFormula a
Theorem: vocOfBigDis
Proof state before:
case inl
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigDis tail) → ∃ φ ∈ tail, x ∈ voc φ
hyp : x ∈ voc (bigDis (head :: tail))
h✝ : x ∈ vocabOfFormula head
⊢ x ∈ vocabOfFormula head ∨ ∃ a ∈ tail, x ∈ vocabOfFormula a
Tactic:
tauto
Proof state after:
no goals
Theorem: vocOfBigDis
Proof state before:
case inr
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigDis tail) → ∃ φ ∈ tail, x ∈ voc φ
hyp : x ∈ voc (bigDis (head :: tail))
h✝ : x ∉ vocabOfFormula head
⊢ ∃ φ ∈ head :: tail, x ∈ voc φ
Tactic:
unfold bigDis at hyp
Proof state after:
case inr
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigDis tail) → ∃ φ ∈ tail, x ∈ voc φ
h✝ : x ∉ vocabOfFormula head
hyp :
  x ∈
    voc
      (match head :: tail with
      | [] => ⊥
      | [f] => f
      | f :: rest => f⋁bigDis rest)
⊢ ∃ φ ∈ head :: tail, x ∈ voc φ
Theorem: vocOfBigDis
Proof state before:
case inr
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigDis tail) → ∃ φ ∈ tail, x ∈ voc φ
h✝ : x ∉ vocabOfFormula head
hyp :
  x ∈
    voc
      (match head :: tail with
      | [] => ⊥
      | [f] => f
      | f :: rest => f⋁bigDis rest)
⊢ ∃ φ ∈ head :: tail, x ∈ voc φ
Tactic:
aesop
Proof state after:
no goals
Theorem: vocOfBigCon
Proof state before:
x : Char
l : List Formula
⊢ x ∈ voc (bigCon l) → ∃ φ ∈ l, x ∈ voc φ
Tactic:
intro hyp
Proof state after:
x : Char
l : List Formula
hyp : x ∈ voc (bigCon l)
⊢ ∃ φ ∈ l, x ∈ voc φ
Theorem: vocOfBigCon
Proof state before:
x : Char
l : List Formula
hyp : x ∈ voc (bigCon l)
⊢ ∃ φ ∈ l, x ∈ voc φ
Tactic:
induction l
Proof state after:
case nil
x : Char
hyp : x ∈ voc (bigCon [])
⊢ ∃ φ ∈ [], x ∈ voc φ

case cons
x : Char
head✝ : Formula
tail✝ : List Formula
tail_ih✝ : x ∈ voc (bigCon tail✝) → ∃ φ ∈ tail✝, x ∈ voc φ
hyp : x ∈ voc (bigCon (head✝ :: tail✝))
⊢ ∃ φ ∈ head✝ :: tail✝, x ∈ voc φ
Theorem: vocOfBigCon
Proof state before:
x : Char
hyp : x ∈ voc (bigCon [])
⊢ ∃ φ ∈ [], x ∈ voc φ
Tactic:
case nil  => aesop
Proof state after:
no goals
Theorem: vocOfBigCon
Proof state before:
x : Char
hyp : x ∈ voc (bigCon [])
⊢ ∃ φ ∈ [], x ∈ voc φ
Tactic:
aesop
Proof state after:
no goals
Theorem: vocOfBigCon
Proof state before:
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigCon tail) → ∃ φ ∈ tail, x ∈ voc φ
hyp : x ∈ voc (bigCon (head :: tail))
⊢ ∃ φ ∈ head :: tail, x ∈ voc φ
Tactic:
cases em (x ∈ vocabOfFormula head)
Proof state after:
case inl
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigCon tail) → ∃ φ ∈ tail, x ∈ voc φ
hyp : x ∈ voc (bigCon (head :: tail))
h✝ : x ∈ vocabOfFormula head
⊢ ∃ φ ∈ head :: tail, x ∈ voc φ

case inr
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigCon tail) → ∃ φ ∈ tail, x ∈ voc φ
hyp : x ∈ voc (bigCon (head :: tail))
h✝ : x ∉ vocabOfFormula head
⊢ ∃ φ ∈ head :: tail, x ∈ voc φ
Theorem: vocOfBigCon
Proof state before:
case inl
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigCon tail) → ∃ φ ∈ tail, x ∈ voc φ
hyp : x ∈ voc (bigCon (head :: tail))
h✝ : x ∈ vocabOfFormula head
⊢ ∃ φ ∈ head :: tail, x ∈ voc φ
Tactic:
simp
Proof state after:
case inl
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigCon tail) → ∃ φ ∈ tail, x ∈ voc φ
hyp : x ∈ voc (bigCon (head :: tail))
h✝ : x ∈ vocabOfFormula head
⊢ x ∈ vocabOfFormula head ∨ ∃ a ∈ tail, x ∈ vocabOfFormula a
Theorem: vocOfBigCon
Proof state before:
case inl
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigCon tail) → ∃ φ ∈ tail, x ∈ voc φ
hyp : x ∈ voc (bigCon (head :: tail))
h✝ : x ∈ vocabOfFormula head
⊢ x ∈ vocabOfFormula head ∨ ∃ a ∈ tail, x ∈ vocabOfFormula a
Tactic:
tauto
Proof state after:
no goals
Theorem: vocOfBigCon
Proof state before:
case inr
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigCon tail) → ∃ φ ∈ tail, x ∈ voc φ
hyp : x ∈ voc (bigCon (head :: tail))
h✝ : x ∉ vocabOfFormula head
⊢ ∃ φ ∈ head :: tail, x ∈ voc φ
Tactic:
unfold bigCon at hyp
Proof state after:
case inr
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigCon tail) → ∃ φ ∈ tail, x ∈ voc φ
h✝ : x ∉ vocabOfFormula head
hyp :
  x ∈
    voc
      (match head :: tail with
      | [] => ⊤
      | [f] => f
      | f :: rest => f⋀bigCon rest)
⊢ ∃ φ ∈ head :: tail, x ∈ voc φ
Theorem: vocOfBigCon
Proof state before:
case inr
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigCon tail) → ∃ φ ∈ tail, x ∈ voc φ
h✝ : x ∉ vocabOfFormula head
hyp :
  x ∈
    voc
      (match head :: tail with
      | [] => ⊤
      | [f] => f
      | f :: rest => f⋀bigCon rest)
⊢ ∃ φ ∈ head :: tail, x ∈ voc φ
Tactic:
aesop
Proof state after:
no goals
Theorem: conempty
Proof state before:
⊢ bigCon ∅ = ⊤
Tactic:
rfl
Proof state after:
no goals
Theorem: consingle
Proof state before:
f : Formula
⊢ bigCon [f] = f
Tactic:
rfl
Proof state after:
no goals
Theorem: disempty
Proof state before:
⊢ dis ∅ = ⊥
Tactic:
rfl
Proof state after:
no goals
Theorem: dissingle
Proof state before:
f : Formula
⊢ dis [f] = f
Tactic:
rfl
Proof state after:
no goals
Theorem: disconempty
Proof state before:
⊢ discon {∅} = ⊤
Tactic:
rfl
Proof state after:
no goals
Theorem: disconsingle
Proof state before:
f : Formula
⊢ discon [[f]] = f
Tactic:
rfl
Proof state after:
no goals
Theorem: conEvalHT
Proof state before:
X : List Formula
f : Formula
W : Type
M : KripkeModel W
w : W
⊢ Evaluate (M, w) (bigCon (f :: X)) ↔ Evaluate (M, w) f ∧ Evaluate (M, w) (bigCon X)
Tactic:
cases X
<;> simp
Proof state after:
no goals
Theorem: conEval
Proof 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
Proof 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
Theorem: conEval
Proof state before:
case nil
W : Type
M : KripkeModel W
w : W
⊢ Evaluate (M, w) (bigCon []) ↔ ∀ f ∈ [], Evaluate (M, w) f
Tactic:
simp
Proof state after:
no goals
Theorem: conEval
Proof 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]
Proof 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
Theorem: conEval
Proof 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
Proof 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)
Theorem: conEval
Proof 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 _
Proof 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
Theorem: conEval
Proof 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
Proof state after:
no goals
Theorem: disconEvalHT
Proof state before:
X : List Formula
⊢ ∀ (XS : List (List Formula)), discon (X :: XS)≡bigCon X⋁discon XS
Tactic:
unfold semEquiv
Proof state after:
X : List Formula
⊢ ∀ (XS : List (List Formula)) (W : Type) (M : KripkeModel W) (w : W),
    Evaluate (M, w) (discon (X :: XS)) ↔ Evaluate (M, w) (bigCon X⋁discon XS)
Theorem: disconEvalHT
Proof state before:
X : List Formula
⊢ ∀ (XS : List (List Formula)) (W : Type) (M : KripkeModel W) (w : W),
    Evaluate (M, w) (discon (X :: XS)) ↔ Evaluate (M, w) (bigCon X⋁discon XS)
Tactic:
intro XS W M w
Proof state after:
X : List Formula
XS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ Evaluate (M, w) (discon (X :: XS)) ↔ Evaluate (M, w) (bigCon X⋁discon XS)
Theorem: disconEvalHT
Proof state before:
X : List Formula
XS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ Evaluate (M, w) (discon (X :: XS)) ↔ Evaluate (M, w) (bigCon X⋁discon XS)
Tactic:
cases XS
<;> simp
Proof state after:
no goals
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:
intro N
Proof 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)
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 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, evalDis, 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) (bigCon 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) (bigCon 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) (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
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) (bigCon 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) (bigCon 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) (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
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) (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
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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon X) ∨ ∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f