Theorem: bigConNeg_union_sat_down (Bml/bigConDis.lean)

State before:
X : Finset Formula
l : List Formula
⊢ Satisfiable (X ∪ {bigCon (List.map (fun x => ~x) l)}) → ∀ φ ∈ l, Satisfiable (X ∪ {~φ})
Tactic:
intro hyp
State after:
X : Finset Formula
l : List Formula
hyp : Satisfiable (X ∪ {bigCon (List.map (fun x => ~x) l)})
⊢ ∀ φ ∈ l, Satisfiable (X ∪ {~φ})

State before:
X : Finset Formula
l : List Formula
hyp : Satisfiable (X ∪ {bigCon (List.map (fun x => ~x) l)})
⊢ ∀ φ ∈ l, Satisfiable (X ∪ {~φ})
Tactic:
rcases hyp with ⟨W, M, w, sat⟩
State after:
case intro.intro.intro
X : Finset Formula
l : List Formula
W : Type
M : KripkeModel W
w : W
sat : ∀ φ ∈ X ∪ {bigCon (List.map (fun x => ~x) l)}, Evaluate (M, w) φ
⊢ ∀ φ ∈ l, Satisfiable (X ∪ {~φ})

State before:
case intro.intro.intro
X : Finset Formula
l : List Formula
W : Type
M : KripkeModel W
w : W
sat : ∀ φ ∈ X ∪ {bigCon (List.map (fun x => ~x) l)}, Evaluate (M, w) φ
⊢ ∀ φ ∈ l, Satisfiable (X ∪ {~φ})
Tactic:
simp at *
State after:
case intro.intro.intro
X : Finset Formula
l : List Formula
W : Type
M : KripkeModel W
w : W
sat : (∀ a ∈ l, ¬Evaluate (M, w) a) ∧ ∀ a ∈ X, Evaluate (M, w) a
⊢ ∀ φ ∈ l, ∃ W M w, ¬Evaluate (M, w) φ ∧ ∀ a ∈ X, Evaluate (M, w) a

State before:
case intro.intro.intro
X : Finset Formula
l : List Formula
W : Type
M : KripkeModel W
w : W
sat : (∀ a ∈ l, ¬Evaluate (M, w) a) ∧ ∀ a ∈ X, Evaluate (M, w) a
⊢ ∀ φ ∈ l, ∃ W M w, ¬Evaluate (M, w) φ ∧ ∀ a ∈ X, Evaluate (M, w) a
Tactic:
cases' sat with lNotSat XSat
State after:
case intro.intro.intro.intro
X : Finset Formula
l : List Formula
W : Type
M : KripkeModel W
w : W
lNotSat : ∀ a ∈ l, ¬Evaluate (M, w) a
XSat : ∀ a ∈ X, Evaluate (M, w) a
⊢ ∀ φ ∈ l, ∃ W M w, ¬Evaluate (M, w) φ ∧ ∀ a ∈ X, Evaluate (M, w) a

State before:
case intro.intro.intro.intro
X : Finset Formula
l : List Formula
W : Type
M : KripkeModel W
w : W
lNotSat : ∀ a ∈ l, ¬Evaluate (M, w) a
XSat : ∀ a ∈ X, Evaluate (M, w) a
⊢ ∀ φ ∈ l, ∃ W M w, ¬Evaluate (M, w) φ ∧ ∀ a ∈ X, Evaluate (M, w) a
Tactic:
intro φ inl
State after:
case intro.intro.intro.intro
X : Finset Formula
l : List Formula
W : Type
M : KripkeModel W
w : W
lNotSat : ∀ a ∈ l, ¬Evaluate (M, w) a
XSat : ∀ a ∈ X, Evaluate (M, w) a
φ : Formula
inl : φ ∈ l
⊢ ∃ W M w, ¬Evaluate (M, w) φ ∧ ∀ a ∈ X, Evaluate (M, w) a

State before:
case intro.intro.intro.intro
X : Finset Formula
l : List Formula
W : Type
M : KripkeModel W
w : W
lNotSat : ∀ a ∈ l, ¬Evaluate (M, w) a
XSat : ∀ a ∈ X, Evaluate (M, w) a
φ : Formula
inl : φ ∈ l
⊢ ∃ W M w, ¬Evaluate (M, w) φ ∧ ∀ a ∈ X, Evaluate (M, w) a
Tactic:
use W, M, w
State after:
case h
X : Finset Formula
l : List Formula
W : Type
M : KripkeModel W
w : W
lNotSat : ∀ a ∈ l, ¬Evaluate (M, w) a
XSat : ∀ a ∈ X, Evaluate (M, w) a
φ : Formula
inl : φ ∈ l
⊢ ¬Evaluate (M, w) φ ∧ ∀ a ∈ X, Evaluate (M, w) a

State before:
case h
X : Finset Formula
l : List Formula
W : Type
M : KripkeModel W
w : W
lNotSat : ∀ a ∈ l, ¬Evaluate (M, w) a
XSat : ∀ a ∈ X, Evaluate (M, w) a
φ : Formula
inl : φ ∈ l
⊢ ¬Evaluate (M, w) φ ∧ ∀ a ∈ X, Evaluate (M, w) a
Tactic:
apply And.intro (lNotSat φ inl) (XSat)
State after:
no goals