L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
h : ¬IsSatisfiable (T ∪ {Formula.not φ})
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
⊢ M ⊨ φ
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
h : T ⊨ᵇ φ
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
⊢ M ⊨ φ
rw [models_iff_not_satisfiable] at h
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
⊢ IsSatisfiable (T ∪ {Formula.not φ})
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
h : ¬IsSatisfiable (T ∪ {Formula.not φ})
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
⊢ M ⊨ φ
contrapose! h
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
this : M ⊨ T ∪ {Formula.not φ}
⊢ IsSatisfiable (T ∪ {Formula.not φ})
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
⊢ IsSatisfiable (T ∪ {Formula.not φ})
have : M ⊨ T ∪ {Formula.not φ} := by
  simp only [Set.union_singleton, model_iff, Set.mem_insert_iff, forall_eq_or_imp,
    Sentence.realize_not]
  rw [← model_iff]
  exact ⟨h, inferInstance⟩
no goals
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
this : M ⊨ T ∪ {Formula.not φ}
⊢ IsSatisfiable (T ∪ {Formula.not φ})
exact Model.isSatisfiable M
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
⊢ ¬M ⊨ φ ∧ ∀ (a : Sentence L), a ∈ T → M ⊨ a
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
⊢ M ⊨ T ∪ {Formula.not φ}
simp only [Set.union_singleton, model_iff, Set.mem_insert_iff, forall_eq_or_imp,
  Sentence.realize_not]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
⊢ ¬M ⊨ φ ∧ M ⊨ T
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
⊢ ¬M ⊨ φ ∧ ∀ (a : Sentence L), a ∈ T → M ⊨ a
rw [← model_iff]
no goals
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
⊢ ¬M ⊨ φ ∧ M ⊨ T
exact ⟨h, inferInstance⟩