Theorem: bigDis_union_sat_down (Bml/bigConDis.lean)

State before:
X : Finset Formula
l : List Formula
⊢ Satisfiable (X ∪ {bigDis l}) → ∃ φ ∈ l, Satisfiable (X ∪ {φ})
Tactic:
simp at *
State after:
X : Finset Formula
l : List Formula
⊢ ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x),
    ∀ x_3 ∈ l,
      Evaluate (x_1, x_2) x_3 →
        (∀ a ∈ X, Evaluate (x_1, x_2) a) → ∃ φ ∈ l, ∃ W M w, Evaluate (M, w) φ ∧ ∀ a ∈ X, Evaluate (M, w) a

State before:
X : Finset Formula
l : List Formula
⊢ ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x),
    ∀ x_3 ∈ l,
      Evaluate (x_1, x_2) x_3 →
        (∀ a ∈ X, Evaluate (x_1, x_2) a) → ∃ φ ∈ l, ∃ W M w, Evaluate (M, w) φ ∧ ∀ a ∈ X, Evaluate (M, w) a
Tactic:
tauto
State after:
no goals