internlm/Lean-Github huggingface dataset:
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) (bigCon 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) (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
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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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) (bigCon 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: 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) (by rfl)]
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 (by rfl)]
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 (by rfl)]
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: disconAnd
Proof state before:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ (XS⊎YS).length = ?m.58205
Tactic:
rfl
Proof state after:
no goals
Theorem: disconAnd
Proof state before:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ XS.length = ?m.69736
Tactic:
rfl
Proof state after:
no goals
Theorem: disconAnd
Proof state before:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ YS.length = ?m.69764
Tactic:
rfl
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) (by rfl)]
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)
Theorem: disconOr
Proof state before:
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)
Tactic:
rw [disconEval XS (by rfl)]
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) ↔
    (¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f) → Evaluate (M, w) (discon YS)
Theorem: disconOr
Proof state before:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ (∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, Evaluate (M, w) f) ↔
    (¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f) → Evaluate (M, w) (discon YS)
Tactic:
rw [disconEval YS (by rfl)]
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) ↔
    (¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f) → ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
Theorem: disconOr
Proof state before:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ (∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, Evaluate (M, w) f) ↔
    (¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f) → ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
Tactic:
constructor
Proof state after:
case mp
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ (∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, Evaluate (M, w) f) →
    (¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f) → ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f

case mpr
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ ((¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f) → ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f) →
    ∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, Evaluate (M, w) f
Theorem: disconOr
Proof state before:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ (XS ∪ YS).length = ?m.132146
Tactic:
rfl
Proof state after:
no goals
Theorem: disconOr
Proof state before:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ XS.length = ?m.136078
Tactic:
rfl
Proof state after:
no goals
Theorem: disconOr
Proof state before:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ YS.length = ?m.136108
Tactic:
rfl
Proof state after:
no goals
Theorem: disconOr
Proof state before:
case mp
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ (∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, Evaluate (M, w) f) →
    (¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f) → ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
Tactic:
intro lhs
Proof state after:
case mp
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
lhs : ∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, Evaluate (M, w) f
⊢ (¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f) → ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
Theorem: disconOr
Proof state before:
case mp
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
lhs : ∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, Evaluate (M, w) f
⊢ (¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f) → ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
Tactic:
rcases lhs with ⟨Z, Z_in, w_sat_Z⟩
Proof state after:
case mp.intro.intro
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
Z : List Formula
Z_in : Z ∈ XS ∨ Z ∈ YS
w_sat_Z : ∀ f ∈ Z, Evaluate (M, w) f
⊢ (¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f) → ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
Theorem: disconOr
Proof state before:
case mp.intro.intro
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
Z : List Formula
Z_in : Z ∈ XS ∨ Z ∈ YS
w_sat_Z : ∀ f ∈ Z, Evaluate (M, w) f
⊢ (¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f) → ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
Tactic:
intro notL
Proof state after:
case mp.intro.intro
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
Z : List Formula
Z_in : Z ∈ XS ∨ Z ∈ YS
w_sat_Z : ∀ f ∈ Z, Evaluate (M, w) f
notL : ¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f
⊢ ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
Theorem: disconOr
Proof state before:
case mp.intro.intro
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
Z : List Formula
Z_in : Z ∈ XS ∨ Z ∈ YS
w_sat_Z : ∀ f ∈ Z, Evaluate (M, w) f
notL : ¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f
⊢ ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
Tactic:
simp at notL
Proof state after:
case mp.intro.intro
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
Z : List Formula
Z_in : Z ∈ XS ∨ Z ∈ YS
w_sat_Z : ∀ f ∈ Z, Evaluate (M, w) f
notL : ∀ x ∈ XS, ∃ x_1 ∈ x, ¬Evaluate (M, w) x_1
⊢ ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
Theorem: disconOr
Proof state before:
case mp.intro.intro
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
Z : List Formula
Z_in : Z ∈ XS ∨ Z ∈ YS
w_sat_Z : ∀ f ∈ Z, Evaluate (M, w) f
notL : ∀ x ∈ XS, ∃ x_1 ∈ x, ¬Evaluate (M, w) x_1
⊢ ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
Tactic:
cases Z_in
Proof state after:
case mp.intro.intro.inl
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
Z : List Formula
w_sat_Z : ∀ f ∈ Z, Evaluate (M, w) f
notL : ∀ x ∈ XS, ∃ x_1 ∈ x, ¬Evaluate (M, w) x_1
h✝ : Z ∈ XS
⊢ ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f

case mp.intro.intro.inr
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
Z : List Formula
w_sat_Z : ∀ f ∈ Z, Evaluate (M, w) f
notL : ∀ x ∈ XS, ∃ x_1 ∈ x, ¬Evaluate (M, w) x_1
h✝ : Z ∈ YS
⊢ ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
Theorem: disconOr
Proof state before:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
Z : List Formula
w_sat_Z : ∀ f ∈ Z, Evaluate (M, w) f
notL : ∀ x ∈ XS, ∃ x_1 ∈ x, ¬Evaluate (M, w) x_1
Z_in_XS : Z ∈ XS
⊢ ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
Tactic:
case inl Z_in_XS =>
  specialize notL Z Z_in_XS
  rcases notL with ⟨f, f_in_Z, w_not_f⟩
  specialize w_sat_Z f f_in_Z
  absurd w_sat_Z
  exact w_not_f
Proof state after:
no goals
Theorem: disconOr
Proof state before:
case mp.intro.intro.inr
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
Z : List Formula
w_sat_Z : ∀ f ∈ Z, Evaluate (M, w) f
notL : ∀ x ∈ XS, ∃ x_1 ∈ x, ¬Evaluate (M, w) x_1
h✝ : Z ∈ YS
⊢ ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
Tactic:
use Z
Proof state after:
no goals
Theorem: disconOr
Proof state before:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
Z : List Formula
w_sat_Z : ∀ f ∈ Z, Evaluate (M, w) f
notL : ∀ x ∈ XS, ∃ x_1 ∈ x, ¬Evaluate (M, w) x_1
Z_in_XS : Z ∈ XS
⊢ ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
Tactic:
specialize notL Z Z_in_XS
Proof state after:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
Z : List Formula
w_sat_Z : ∀ f ∈ Z, Evaluate (M, w) f
Z_in_XS : Z ∈ XS
notL : ∃ x ∈ Z, ¬Evaluate (M, w) x
⊢ ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
Theorem: disconOr
Proof state before:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
Z : List Formula
w_sat_Z : ∀ f ∈ Z, Evaluate (M, w) f
Z_in_XS : Z ∈ XS
notL : ∃ x ∈ Z, ¬Evaluate (M, w) x
⊢ ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
Tactic:
rcases notL with ⟨f, f_in_Z, w_not_f⟩
Proof state after:
case intro.intro
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
Z : List Formula
w_sat_Z : ∀ f ∈ Z, Evaluate (M, w) f
Z_in_XS : Z ∈ XS
f : Formula
f_in_Z : f ∈ Z
w_not_f : ¬Evaluate (M, w) f
⊢ ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
Theorem: disconOr
Proof state before:
case intro.intro
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
Z : List Formula
w_sat_Z : ∀ f ∈ Z, Evaluate (M, w) f
Z_in_XS : Z ∈ XS
f : Formula
f_in_Z : f ∈ Z
w_not_f : ¬Evaluate (M, w) f
⊢ ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
Tactic:
specialize w_sat_Z f f_in_Z
Proof state after:
case intro.intro
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
Z : List Formula
Z_in_XS : Z ∈ XS
f : Formula
f_in_Z : f ∈ Z
w_not_f : ¬Evaluate (M, w) f
w_sat_Z : Evaluate (M, w) f
⊢ ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
Theorem: disconOr
Proof state before:
case intro.intro
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
Z : List Formula
Z_in_XS : Z ∈ XS
f : Formula
f_in_Z : f ∈ Z
w_not_f : ¬Evaluate (M, w) f
w_sat_Z : Evaluate (M, w) f
⊢ ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
Tactic:
absurd w_sat_Z
Proof state after:
case intro.intro
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
Z : List Formula
Z_in_XS : Z ∈ XS
f : Formula
f_in_Z : f ∈ Z
w_not_f : ¬Evaluate (M, w) f
w_sat_Z : Evaluate (M, w) f
⊢ ¬Evaluate (M, w) f
Theorem: disconOr
Proof state before:
case intro.intro
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
Z : List Formula
Z_in_XS : Z ∈ XS
f : Formula
f_in_Z : f ∈ Z
w_not_f : ¬Evaluate (M, w) f
w_sat_Z : Evaluate (M, w) f
⊢ ¬Evaluate (M, w) f
Tactic:
exact w_not_f
Proof state after:
no goals
Theorem: disconOr
Proof state before:
case mpr
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ ((¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f) → ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f) →
    ∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, Evaluate (M, w) f
Tactic:
intro rhs
Proof state after:
case mpr
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
rhs : (¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f) → ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
⊢ ∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, Evaluate (M, w) f
Theorem: disconOr
Proof state before:
case mpr
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
rhs : (¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f) → ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
⊢ ∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, Evaluate (M, w) f
Tactic:
cases em (∃ Y, Y ∈ XS ∧ ∀ (f : Formula), f ∈ Y → Evaluate (M, w) f)
Proof state after:
case mpr.inl
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
rhs : (¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f) → ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
h✝ : ∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f
⊢ ∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, Evaluate (M, w) f

case mpr.inr
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
rhs : (¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f) → ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
h✝ : ¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f
⊢ ∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, Evaluate (M, w) f
Theorem: disconOr
Proof state before:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
rhs : (¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f) → ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
hyp : ∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f
⊢ ∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, Evaluate (M, w) f
Tactic:
case inl hyp =>
  rcases hyp with ⟨X, X_in, satX⟩
  use X
  exact ⟨Or.inl X_in, satX⟩
Proof state after:
no goals
Theorem: disconOr
Proof state before:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
rhs : (¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f) → ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
nothyp : ¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f
⊢ ∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, Evaluate (M, w) f
Tactic:
case inr nothyp =>
  specialize rhs nothyp
  rcases rhs with ⟨Y, Y_in, satY⟩
  use Y
  exact ⟨Or.inr Y_in, satY⟩
Proof state after:
no goals
Theorem: disconOr
Proof state before:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
rhs : (¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f) → ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
hyp : ∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f
⊢ ∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, Evaluate (M, w) f
Tactic:
rcases hyp with ⟨X, X_in, satX⟩
Proof state after:
case intro.intro
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
rhs : (¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f) → ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
X : List Formula
X_in : X ∈ XS
satX : ∀ f ∈ X, Evaluate (M, w) f
⊢ ∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, Evaluate (M, w) f
Theorem: disconOr
Proof state before:
case intro.intro
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
rhs : (¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f) → ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
X : List Formula
X_in : X ∈ XS
satX : ∀ f ∈ X, Evaluate (M, w) f
⊢ ∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, Evaluate (M, w) f
Tactic:
use X
Proof state after:
case h
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
rhs : (¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f) → ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
X : List Formula
X_in : X ∈ XS
satX : ∀ f ∈ X, Evaluate (M, w) f
⊢ (X ∈ XS ∨ X ∈ YS) ∧ ∀ f ∈ X, Evaluate (M, w) f
Theorem: disconOr
Proof state before:
case h
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
rhs : (¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f) → ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
X : List Formula
X_in : X ∈ XS
satX : ∀ f ∈ X, Evaluate (M, w) f
⊢ (X ∈ XS ∨ X ∈ YS) ∧ ∀ f ∈ X, Evaluate (M, w) f
Tactic:
exact ⟨Or.inl X_in, satX⟩
Proof state after:
no goals
Theorem: disconOr
Proof state before:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
rhs : (¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f) → ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
nothyp : ¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f
⊢ ∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, Evaluate (M, w) f
Tactic:
specialize rhs nothyp
Proof state after:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
nothyp : ¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f
rhs : ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
⊢ ∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, Evaluate (M, w) f
Theorem: disconOr
Proof state before:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
nothyp : ¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f
rhs : ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
⊢ ∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, Evaluate (M, w) f
Tactic:
rcases rhs with ⟨Y, Y_in, satY⟩
Proof state after:
case intro.intro
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
nothyp : ¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f
Y : List Formula
Y_in : Y ∈ YS
satY : ∀ f ∈ Y, Evaluate (M, w) f
⊢ ∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, Evaluate (M, w) f
Theorem: disconOr
Proof state before:
case intro.intro
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
nothyp : ¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f
Y : List Formula
Y_in : Y ∈ YS
satY : ∀ f ∈ Y, Evaluate (M, w) f
⊢ ∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, Evaluate (M, w) f
Tactic:
use Y
Proof state after:
case h
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
nothyp : ¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f
Y : List Formula
Y_in : Y ∈ YS
satY : ∀ f ∈ Y, Evaluate (M, w) f
⊢ (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, Evaluate (M, w) f
Theorem: disconOr
Proof state before:
case h
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
nothyp : ¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f
Y : List Formula
Y_in : Y ∈ YS
satY : ∀ f ∈ Y, Evaluate (M, w) f
⊢ (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, Evaluate (M, w) f
Tactic:
exact ⟨Or.inr Y_in, satY⟩
Proof state after:
no goals
Theorem: union_elem_uplus
Proof state before:
XS YS : Finset (Finset Formula)
X Y : Finset Formula
⊢ X ∈ XS → Y ∈ YS → X ∪ Y ∈ XS⊎YS
Tactic:
intro X_in Y_in
Proof state after:
XS YS : Finset (Finset Formula)
X Y : Finset Formula
X_in : X ∈ XS
Y_in : Y ∈ YS
⊢ X ∪ Y ∈ XS⊎YS
Theorem: union_elem_uplus
Proof state before:
XS YS : Finset (Finset Formula)
X Y : Finset Formula
X_in : X ∈ XS
Y_in : Y ∈ YS
⊢ X ∪ Y ∈ XS⊎YS
Tactic:
simp
Proof state after:
XS YS : Finset (Finset Formula)
X Y : Finset Formula
X_in : X ∈ XS
Y_in : Y ∈ YS
⊢ ∃ a ∈ XS, ∃ a_1 ∈ YS, X ∪ Y = a ∪ a_1
Theorem: union_elem_uplus
Proof state before:
XS YS : Finset (Finset Formula)
X Y : Finset Formula
X_in : X ∈ XS
Y_in : Y ∈ YS
⊢ ∃ a ∈ XS, ∃ a_1 ∈ YS, X ∪ Y = a ∪ a_1
Tactic:
exact ⟨X, X_in, Y, Y_in, rfl⟩
Proof state after:
no goals
Theorem: bigDis_sat
Proof state before:
W : Type
l : List Formula
M : KripkeModel W
w : W
⊢ Evaluate (M, w) (bigDis l) ↔ ∃ φ ∈ l, Evaluate (M, w) φ
Tactic:
constructor
Proof state after:
case mp
W : Type
l : List Formula
M : KripkeModel W
w : W
⊢ Evaluate (M, w) (bigDis l) → ∃ φ ∈ l, Evaluate (M, w) φ

case mpr
W : Type
l : List Formula
M : KripkeModel W
w : W
⊢ (∃ φ ∈ l, Evaluate (M, w) φ) → Evaluate (M, w) (bigDis l)