-- Mathlib/ModelTheory/Satisfiability.lean
theorem models_iff_finset_models {φ : L.Sentence} :
    T ⊨ᵇ φ ↔ ∃ T0 : Finset L.Sentence, (T0 : L.Theory) ⊆ T ∧ (T0 : L.Theory) ⊨ᵇ φ

Proof state:
case mpr
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
h : ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T → (↑T0 ∪ {Formula.not φ}).IsSatisfiable
T0 : Finset L.Sentence
hT0 : ↑T0 ⊆ T ∪ {Formula.not φ}
⊢ IsSatisfiable ↑T0

Tactic:
exact IsSatisfiable.mono (h (T0.erase (Formula.not φ))
  (by simpa using hT0)) (by simp)

Result:
no goals

Proof state:
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
⊢ (∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0) ↔
    ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T → (↑T0 ∪ {Formula.not φ}).IsSatisfiable

Tactic:
constructor

Result:
case mp
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
⊢ (∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0) →
    ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T → (↑T0 ∪ {Formula.not φ}).IsSatisfiable

case mpr
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
⊢ (∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T → (↑T0 ∪ {Formula.not φ}).IsSatisfiable) →
    ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0

Proof state:
case mp
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
h : ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0
T0 : Finset L.Sentence
hT0 : ↑T0 ⊆ T
⊢ (↑T0 ∪ {Formula.not φ}).IsSatisfiable

Tactic:
simpa using h (T0 ∪ {Formula.not φ})
  (by
    simp only [Finset.coe_union, Finset.coe_singleton]
    exact Set.union_subset_union hT0 (Set.Subset.refl _))

Result:
no goals

Proof state:
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
h : ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T → (↑T0 ∪ {Formula.not φ}).IsSatisfiable
T0 : Finset L.Sentence
hT0 : ↑T0 ⊆ T ∪ {Formula.not φ}
⊢ ↑(T0.erase (Formula.not φ)) ⊆ T

Tactic:
simpa using hT0

Result:
no goals

Proof state:
case mp
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
⊢ (∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0) →
    ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T → (↑T0 ∪ {Formula.not φ}).IsSatisfiable

Tactic:
intro h T0 hT0

Result:
case mp
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
h : ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0
T0 : Finset L.Sentence
hT0 : ↑T0 ⊆ T
⊢ (↑T0 ∪ {Formula.not φ}).IsSatisfiable

Proof state:
L : Language
T : L.Theory
φ : L.Sentence
⊢ T ⊨ᵇ φ ↔ ∃ T0, ↑T0 ⊆ T ∧ ↑T0 ⊨ᵇ φ

Tactic:
simp only [models_iff_not_satisfiable]

Result:
L : Language
T : L.Theory
φ : L.Sentence
⊢ ¬(T ∪ {Formula.not φ}).IsSatisfiable ↔ ∃ T0, ↑T0 ⊆ T ∧ ¬(↑T0 ∪ {Formula.not φ}).IsSatisfiable

Proof state:
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
h : ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0
T0 : Finset L.Sentence
hT0 : ↑T0 ⊆ T
⊢ ↑(T0 ∪ {Formula.not φ}) ⊆ T ∪ {Formula.not φ}

Tactic:
simp only [Finset.coe_union, Finset.coe_singleton]

Result:
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
h : ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0
T0 : Finset L.Sentence
hT0 : ↑T0 ⊆ T
⊢ ↑T0 ∪ {Formula.not φ} ⊆ T ∪ {Formula.not φ}

Proof state:
case mpr
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
⊢ (∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T → (↑T0 ∪ {Formula.not φ}).IsSatisfiable) →
    ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0

Tactic:
intro h T0 hT0

Result:
case mpr
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
h : ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T → (↑T0 ∪ {Formula.not φ}).IsSatisfiable
T0 : Finset L.Sentence
hT0 : ↑T0 ⊆ T ∪ {Formula.not φ}
⊢ IsSatisfiable ↑T0

Proof state:
L : Language
T : L.Theory
φ : L.Sentence
⊢ ¬(T ∪ {Formula.not φ}).IsSatisfiable ↔ ∃ T0, ↑T0 ⊆ T ∧ ¬(↑T0 ∪ {Formula.not φ}).IsSatisfiable

Tactic:
rw [← not_iff_not, not_not, isSatisfiable_iff_isFinitelySatisfiable, IsFinitelySatisfiable]

Result:
L : Language
T : L.Theory
φ : L.Sentence
⊢ (∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0) ↔
    ¬∃ T0, ↑T0 ⊆ T ∧ ¬(↑T0 ∪ {Formula.not φ}).IsSatisfiable

Proof state:
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
h : ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T → (↑T0 ∪ {Formula.not φ}).IsSatisfiable
T0 : Finset L.Sentence
hT0 : ↑T0 ⊆ T ∪ {Formula.not φ}
⊢ ↑T0 ⊆ ↑(T0.erase (Formula.not φ)) ∪ {Formula.not φ}

Tactic:
simp

Result:
no goals

Proof state:
L : Language
T : L.Theory
φ : L.Sentence
⊢ (∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0) ↔
    ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T → (↑T0 ∪ {Formula.not φ}).IsSatisfiable

Tactic:
letI := Classical.decEq (Sentence L)

Result:
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
⊢ (∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0) ↔
    ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T → (↑T0 ∪ {Formula.not φ}).IsSatisfiable

Proof state:
L : Language
T : L.Theory
φ : L.Sentence
⊢ (∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0) ↔
    ¬∃ T0, ↑T0 ⊆ T ∧ ¬(↑T0 ∪ {Formula.not φ}).IsSatisfiable

Tactic:
push_neg

Result:
L : Language
T : L.Theory
φ : L.Sentence
⊢ (∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0) ↔
    ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T → (↑T0 ∪ {Formula.not φ}).IsSatisfiable

Proof state:
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
h : ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0
T0 : Finset L.Sentence
hT0 : ↑T0 ⊆ T
⊢ ↑T0 ∪ {Formula.not φ} ⊆ T ∪ {Formula.not φ}

Tactic:
exact Set.union_subset_union hT0 (Set.Subset.refl _)

Result:
no goals