internlm/Lean-Github huggingface dataset:
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]
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]
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:
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 (Classical.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: mapCon_mapForall
Proof state before:
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
⊢ (∃ f ∈ List.map (fun Fδ => Con (g Fδ φ)) X, evaluate M w f) ↔
    ∃ fs ∈ List.map (fun Fδ => g Fδ φ) X, ∀ f ∈ fs, evaluate M w f
Tactic:
simp_all
Proof state after:
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
⊢ (∃ f, (∃ a b, (a, b) ∈ X ∧ Con (g (a, b) φ) = f) ∧ evaluate M w f) ↔
    ∃ fs, (∃ a b, (a, b) ∈ X ∧ g (a, b) φ = fs) ∧ ∀ f ∈ fs, evaluate M w f
Theorem: mapCon_mapForall
Proof state before:
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
⊢ (∃ f, (∃ a b, (a, b) ∈ X ∧ Con (g (a, b) φ) = f) ∧ evaluate M w f) ↔
    ∃ fs, (∃ a b, (a, b) ∈ X ∧ g (a, b) φ = fs) ∧ ∀ f ∈ fs, evaluate M w f
Tactic:
constructor
Proof state after:
case mp
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
⊢ (∃ f, (∃ a b, (a, b) ∈ X ∧ Con (g (a, b) φ) = f) ∧ evaluate M w f) →
    ∃ fs, (∃ a b, (a, b) ∈ X ∧ g (a, b) φ = fs) ∧ ∀ f ∈ fs, evaluate M w f

case mpr
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
⊢ (∃ fs, (∃ a b, (a, b) ∈ X ∧ g (a, b) φ = fs) ∧ ∀ f ∈ fs, evaluate M w f) →
    ∃ f, (∃ a b, (a, b) ∈ X ∧ Con (g (a, b) φ) = f) ∧ evaluate M w f
Theorem: mapCon_mapForall
Proof state before:
case mp
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
⊢ (∃ f, (∃ a b, (a, b) ∈ X ∧ Con (g (a, b) φ) = f) ∧ evaluate M w f) →
    ∃ fs, (∃ a b, (a, b) ∈ X ∧ g (a, b) φ = fs) ∧ ∀ f ∈ fs, evaluate M w f
Tactic:
rintro ⟨f,⟨a, b, ab_in, def_f⟩, w_f⟩
Proof state after:
case mp.intro.intro.intro.intro.intro
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
f : Formula
w_f : evaluate M w f
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
def_f : Con (g (a, b) φ) = f
⊢ ∃ fs, (∃ a b, (a, b) ∈ X ∧ g (a, b) φ = fs) ∧ ∀ f ∈ fs, evaluate M w f
Theorem: mapCon_mapForall
Proof state before:
case mp.intro.intro.intro.intro.intro
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
f : Formula
w_f : evaluate M w f
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
def_f : Con (g (a, b) φ) = f
⊢ ∃ fs, (∃ a b, (a, b) ∈ X ∧ g (a, b) φ = fs) ∧ ∀ f ∈ fs, evaluate M w f
Tactic:
subst def_f
Proof state after:
case mp.intro.intro.intro.intro.intro
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
w_f : evaluate M w (Con (g (a, b) φ))
⊢ ∃ fs, (∃ a b, (a, b) ∈ X ∧ g (a, b) φ = fs) ∧ ∀ f ∈ fs, evaluate M w f
Theorem: mapCon_mapForall
Proof state before:
case mp.intro.intro.intro.intro.intro
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
w_f : evaluate M w (Con (g (a, b) φ))
⊢ ∃ fs, (∃ a b, (a, b) ∈ X ∧ g (a, b) φ = fs) ∧ ∀ f ∈ fs, evaluate M w f
Tactic:
use g (a,b) φ
Proof state after:
case h
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
w_f : evaluate M w (Con (g (a, b) φ))
⊢ (∃ a_1 b_1, (a_1, b_1) ∈ X ∧ g (a_1, b_1) φ = g (a, b) φ) ∧ ∀ f ∈ g (a, b) φ, evaluate M w f
Theorem: mapCon_mapForall
Proof state before:
case h
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
w_f : evaluate M w (Con (g (a, b) φ))
⊢ (∃ a_1 b_1, (a_1, b_1) ∈ X ∧ g (a_1, b_1) φ = g (a, b) φ) ∧ ∀ f ∈ g (a, b) φ, evaluate M w f
Tactic:
constructor
Proof state after:
case h.left
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
w_f : evaluate M w (Con (g (a, b) φ))
⊢ ∃ a_1 b_1, (a_1, b_1) ∈ X ∧ g (a_1, b_1) φ = g (a, b) φ

case h.right
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
w_f : evaluate M w (Con (g (a, b) φ))
⊢ ∀ f ∈ g (a, b) φ, evaluate M w f
Theorem: mapCon_mapForall
Proof state before:
case h.left
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
w_f : evaluate M w (Con (g (a, b) φ))
⊢ ∃ a_1 b_1, (a_1, b_1) ∈ X ∧ g (a_1, b_1) φ = g (a, b) φ
Tactic:
use a, b
Proof state after:
no goals
Theorem: mapCon_mapForall
Proof state before:
case h.right
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
w_f : evaluate M w (Con (g (a, b) φ))
⊢ ∀ f ∈ g (a, b) φ, evaluate M w f
Tactic:
intro f f_in
Proof state after:
case h.right
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
w_f : evaluate M w (Con (g (a, b) φ))
f : Formula
f_in : f ∈ g (a, b) φ
⊢ evaluate M w f
Theorem: mapCon_mapForall
Proof state before:
case h.right
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
w_f : evaluate M w (Con (g (a, b) φ))
f : Formula
f_in : f ∈ g (a, b) φ
⊢ evaluate M w f
Tactic:
rw [conEval] at w_f
Proof state after:
case h.right
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
w_f : ∀ f ∈ g (a, b) φ, evaluate M w f
f : Formula
f_in : f ∈ g (a, b) φ
⊢ evaluate M w f
Theorem: mapCon_mapForall
Proof state before:
case h.right
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
w_f : ∀ f ∈ g (a, b) φ, evaluate M w f
f : Formula
f_in : f ∈ g (a, b) φ
⊢ evaluate M w f
Tactic:
specialize w_f f
Proof state after:
case h.right
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
f : Formula
f_in : f ∈ g (a, b) φ
w_f : f ∈ g (a, b) φ → evaluate M w f
⊢ evaluate M w f
Theorem: mapCon_mapForall
Proof state before:
case h.right
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
f : Formula
f_in : f ∈ g (a, b) φ
w_f : f ∈ g (a, b) φ → evaluate M w f
⊢ evaluate M w f
Tactic:
tauto
Proof state after:
no goals
Theorem: mapCon_mapForall
Proof state before:
case mpr
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
⊢ (∃ fs, (∃ a b, (a, b) ∈ X ∧ g (a, b) φ = fs) ∧ ∀ f ∈ fs, evaluate M w f) →
    ∃ f, (∃ a b, (a, b) ∈ X ∧ Con (g (a, b) φ) = f) ∧ evaluate M w f
Tactic:
rintro ⟨fs,⟨⟨a, b, ab_in, def_fs⟩, w_fs⟩⟩
Proof state after:
case mpr.intro.intro.intro.intro.intro
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
fs : List Formula
w_fs : ∀ f ∈ fs, evaluate M w f
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
def_fs : g (a, b) φ = fs
⊢ ∃ f, (∃ a b, (a, b) ∈ X ∧ Con (g (a, b) φ) = f) ∧ evaluate M w f
Theorem: mapCon_mapForall
Proof state before:
case mpr.intro.intro.intro.intro.intro
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
fs : List Formula
w_fs : ∀ f ∈ fs, evaluate M w f
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
def_fs : g (a, b) φ = fs
⊢ ∃ f, (∃ a b, (a, b) ∈ X ∧ Con (g (a, b) φ) = f) ∧ evaluate M w f
Tactic:
subst def_fs
Proof state after:
case mpr.intro.intro.intro.intro.intro
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
w_fs : ∀ f ∈ g (a, b) φ, evaluate M w f
⊢ ∃ f, (∃ a b, (a, b) ∈ X ∧ Con (g (a, b) φ) = f) ∧ evaluate M w f
Theorem: mapCon_mapForall
Proof state before:
case mpr.intro.intro.intro.intro.intro
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
w_fs : ∀ f ∈ g (a, b) φ, evaluate M w f
⊢ ∃ f, (∃ a b, (a, b) ∈ X ∧ Con (g (a, b) φ) = f) ∧ evaluate M w f
Tactic:
use Con (g (a, b) φ)
Proof state after:
case h
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
w_fs : ∀ f ∈ g (a, b) φ, evaluate M w f
⊢ (∃ a_1 b_1, (a_1, b_1) ∈ X ∧ Con (g (a_1, b_1) φ) = Con (g (a, b) φ)) ∧ evaluate M w (Con (g (a, b) φ))
Theorem: mapCon_mapForall
Proof state before:
case h
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
w_fs : ∀ f ∈ g (a, b) φ, evaluate M w f
⊢ (∃ a_1 b_1, (a_1, b_1) ∈ X ∧ Con (g (a_1, b_1) φ) = Con (g (a, b) φ)) ∧ evaluate M w (Con (g (a, b) φ))
Tactic:
constructor
Proof state after:
case h.left
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
w_fs : ∀ f ∈ g (a, b) φ, evaluate M w f
⊢ ∃ a_1 b_1, (a_1, b_1) ∈ X ∧ Con (g (a_1, b_1) φ) = Con (g (a, b) φ)

case h.right
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
w_fs : ∀ f ∈ g (a, b) φ, evaluate M w f
⊢ evaluate M w (Con (g (a, b) φ))