Theorem: mapCon_mapForall (Pdl/Discon.lean)

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
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

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
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

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⟩
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

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
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

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) φ
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

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
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

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
State after:
no goals

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
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

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
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

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
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

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
State after:
no goals

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⟩⟩
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

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
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

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) φ)
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) φ))

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
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) φ))

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_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) φ)
Tactic:
use a, b
State after:
no goals

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_fs : ∀ f ∈ g (a, b) φ, evaluate M w f
⊢ evaluate M w (Con (g (a, b) φ))
Tactic:
rw [conEval]
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_fs : ∀ f ∈ g (a, b) φ, evaluate M w f
⊢ ∀ f ∈ g (a, b) φ, evaluate M w f

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_fs : ∀ f ∈ g (a, b) φ, evaluate M w f
⊢ ∀ f ∈ g (a, b) φ, evaluate M w f
Tactic:
intro f
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_fs : ∀ f ∈ g (a, b) φ, evaluate M w f
f : Formula
⊢ f ∈ g (a, b) φ → evaluate M w f

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_fs : ∀ f ∈ g (a, b) φ, evaluate M w f
f : Formula
⊢ f ∈ g (a, b) φ → evaluate M w f
Tactic:
tauto
State after:
no goals