Theorem: disconAnd (Pdl/Discon.lean)

State before:
XS YS : List (List Formula)
⊢ discon (XS⊎YS)≡discon XS⋀discon YS
Tactic:
unfold semEquiv
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)

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

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

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

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

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

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