Theorem: disconAnd (Bml/bigConDis.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) (by rfl)]
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 (by rfl)]
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 (by rfl)]
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

State before:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ (XS⊎YS).length = ?m.58205
Tactic:
rfl
State after:
no goals

State before:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ XS.length = ?m.69736
Tactic:
rfl
State after:
no goals

State before:
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
⊢ YS.length = ?m.69764
Tactic:
rfl
State after:
no goals