awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : T ⊨ᵇ φ
M : ((L.lhomWithConstants α).onTheory T).ModelType
this_1 : L.Structure (↑M : Type (max (max u v) w)) := (L.lhomWithConstants α).reduct (↑M : Type (max (max u v) w))
this : (↑M : Type (max (max u v) w)) ⊨ T
M' : T.ModelType := ModelType.of T (↑M : Type (max (max u v) w))
⊢ φ.Realize (M := (↑M : Type (max (max u w) v))) fun (a : α) ↦ (↑(L.con a) : (↑M : Type (max (max u w) v)))

Tactic:
h M' (fun a => (L.con a : M)) _

Premises used: setOf, FirstOrder.Language.withConstants, FirstOrder.Language.con, FirstOrder.Language.constantMap, FirstOrder.Language.sum, Set.image, FirstOrder.Language.Formula.Realize, FirstOrder.Language.LHom.onTheory
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : T ⊨ᵇ φ
M : ((L.lhomWithConstants α).onTheory T).ModelType
this_1 : L.Structure (↑M : Type (max (max u v) w)) := (L.lhomWithConstants α).reduct (↑M : Type (max (max u v) w))
this : (↑M : Type (max (max u v) w)) ⊨ T
M' : T.ModelType := ModelType.of T (↑M : Type (max (max u v) w))
⊢ φ.Realize (M := (↑M : Type (max (max u w) v))) fun (a : α) ↦ (↑(L.con a) : (↑M : Type (max (max u w) v)))

Tactic:
exact h M' (fun a => (L.con a : M)) _

Premises used: FirstOrder.Language.con, FirstOrder.Language.constantMap
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h :
  ((L.lhomWithConstants α).onTheory T).ModelsBoundedFormula (α := Empty) (n := 0)
    ((Formula.equivSentence : (a : L.Formula α) → L[[α]].Sentence) φ)
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
this : (constantsOn α).Structure (↑M : Type (max (max u v) w)) := constantsOn.structure v
⊢ (↑M : Type (max (max u v) w)) ⊨ (L.lhomWithConstants α).onTheory T

Tactic:
have : M ⊨ (L.lhomWithConstants α).onTheory T := (LHom.onTheory_model _ _).2 inferInstance
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h :
  ((L.lhomWithConstants α).onTheory T).ModelsBoundedFormula (α := Empty) (n := 0)
    ((Formula.equivSentence : (a : L.Formula α) → L[[α]].Sentence) φ)
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
this_1 : (constantsOn α).Structure (↑M : Type (max (max u v) w)) := constantsOn.structure v
this : (↑M : Type (max (max u v) w)) ⊨ (L.lhomWithConstants α).onTheory T
⊢ φ.Realize v

Tactic:
(Formula.realize_equivSentence _ _).1 (h.realize_sentence M)

Premises used: FirstOrder.Language.Theory.ModelsBoundedFormula.realize_sentence, FirstOrder.Language.Theory.ModelType.Carrier, Iff.mp, FirstOrder.Language.constantMap, FirstOrder.Language.Formula.realize_equivSentence, Sum.elim
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h :
  ((L.lhomWithConstants α).onTheory T).ModelsBoundedFormula (α := Empty) (n := 0)
    ((Formula.equivSentence : (a : L.Formula α) → L[[α]].Sentence) φ)
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
this_1 : (constantsOn α).Structure (↑M : Type (max (max u v) w)) := constantsOn.structure v
this : (↑M : Type (max (max u v) w)) ⊨ (L.lhomWithConstants α).onTheory T
⊢ φ.Realize v

Tactic:
exact (Formula.realize_equivSentence _ _).1 (h.realize_sentence M)

Premises used: FirstOrder.Language.Theory.ModelsBoundedFormula.realize_sentence, FirstOrder.Language.Theory.ModelType.Carrier, Iff.mp, FirstOrder.Language.Formula.realize_equivSentence
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : T ⊨ᵇ φ
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
v : α → M
rw :
  ∀
    (h :
      ((L.lhomWithConstants α).onTheory T).ModelsBoundedFormula (α := Empty) (n := 0)
        ((Formula.equivSentence : (a : L.Formula α) → L[[α]].Sentence) φ))
    (M : Type u_1) [inst : L.Structure M] [M ⊨ T] [Nonempty M] {v : α → M}, φ.Realize v
⊢ φ.Realize v

Tactic:
rw [models_formula_iff_onTheory_models_equivSentence] at h

Premises used: FirstOrder.Language.Theory.models_formula_iff_onTheory_models_equivSentence
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h :
  ((L.lhomWithConstants α).onTheory T).ModelsBoundedFormula (α := Empty) (n := 0)
    ((Formula.equivSentence : (a : L.Formula α) → L[[α]].Sentence) φ)
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
v : α → M
this : Structure.{w, 0, u_1} (constantsOn α) M := constantsOn.structure v
⊢ M ⊨ (L.lhomWithConstants α).onTheory T

Tactic:
have : M ⊨ (L.lhomWithConstants α).onTheory T := (LHom.onTheory_model _ _).2 inferInstance
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h :
  ((L.lhomWithConstants α).onTheory T).ModelsBoundedFormula (α := Empty) (n := 0)
    ((Formula.equivSentence : (a : L.Formula α) → L[[α]].Sentence) φ)
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
v : α → M
this_1 : Structure.{w, 0, u_1} (constantsOn α) M := constantsOn.structure v
this : M ⊨ (L.lhomWithConstants α).onTheory T
⊢ φ.Realize v

Tactic:
(Formula.realize_equivSentence _ _).1 (h.realize_sentence M)

Premises used: FirstOrder.Language.Theory.ModelsBoundedFormula.realize_sentence, Iff.mp, FirstOrder.Language.constantMap, FirstOrder.Language.Formula.realize_equivSentence, Sum.elim
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h :
  ((L.lhomWithConstants α).onTheory T).ModelsBoundedFormula (α := Empty) (n := 0)
    ((Formula.equivSentence : (a : L.Formula α) → L[[α]].Sentence) φ)
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
v : α → M
this_1 : Structure.{w, 0, u_1} (constantsOn α) M := constantsOn.structure v
this : M ⊨ (L.lhomWithConstants α).onTheory T
⊢ φ.Realize v

Tactic:
exact (Formula.realize_equivSentence _ _).1 (h.realize_sentence M)

Premises used: FirstOrder.Language.Theory.ModelsBoundedFormula.realize_sentence, Iff.mp, FirstOrder.Language.Formula.realize_equivSentence
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
⊢ T ⊨ᵇ φ.toFormula ↔ T ⊨ᵇ φ

Tactic:
⟨fun h M v xs => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
refine_1 :
  ∀ (h : T ⊨ᵇ φ.toFormula) (M : T.ModelType) (v : α → (↑M : Type (max (max u v) w)))
    (xs : Fin n → (↑M : Type (max (max u v) w))), φ.Realize v xs
refine_2 : T ⊨ᵇ φ → T ⊨ᵇ φ.toFormula
⊢ T ⊨ᵇ φ.toFormula ↔ T ⊨ᵇ φ

Tactic:
refine ⟨fun h M v xs => ?_, ?_⟩
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
h : T ⊨ᵇ φ.toFormula
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ φ.toFormula.Realize (Sum.elim v xs)

Tactic:
have h' : φ.toFormula.Realize (Sum.elim v xs) := h.realize_formula M
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
h : T ⊨ᵇ φ.toFormula
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
h' : φ.toFormula.Realize (Sum.elim v xs)
⊢ φ.Realize v xs

Tactic:
simp only [BoundedFormula.realize_toFormula, Sum.elim_comp_inl, Sum.elim_comp_inr] at h'

Premises used: Sum.elim_comp_inr, Sum.elim_comp_inl, FirstOrder.Language.BoundedFormula.realize_toFormula
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
h : T ⊨ᵇ φ.toFormula
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
h' : φ.Realize v xs
⊢ φ.Realize v xs

Tactic:
h'
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
h : T ⊨ᵇ φ.toFormula
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
h' : φ.Realize v xs
⊢ φ.Realize v xs

Tactic:
exact h'
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
refine_2 :
  T ⊨ᵇ φ → ∀ (M : T.ModelType) (v : α ⊕ Fin n → (↑M : Type (max (max u v) w))), φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
⊢ T ⊨ᵇ φ → T ⊨ᵇ φ.toFormula

Tactic:
simp only [models_formula_iff, BoundedFormula.realize_toFormula]

Premises used: FirstOrder.Language.Theory.models_formula_iff, FirstOrder.Language.BoundedFormula.realize_toFormula
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
⊢ T ⊨ᵇ φ → ∀ (M : T.ModelType) (v : α ⊕ Fin n → (↑M : Type (max (max u v) w))), φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)

Tactic:
fun h M v => h M _ _

Premises used: Function.comp, Sum.inl, Sum.inr
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
⊢ T ⊨ᵇ φ → ∀ (M : T.ModelType) (v : α ⊕ Fin n → (↑M : Type (max (max u v) w))), φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)

Tactic:
exact fun h M v => h M _ _
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
h : T ⊨ᵇ φ
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
v : α → M
xs : Fin n → M
⊢ φ.toFormula.Realize (Sum.elim v xs)

Tactic:
have h' : φ.toFormula.Realize (Sum.elim v xs) := (models_toFormula_iff.2 h).realize_formula M
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
h : T ⊨ᵇ φ
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
v : α → M
xs : Fin n → M
h' : φ.toFormula.Realize (Sum.elim v xs)
⊢ φ.Realize v xs

Tactic:
simp only [BoundedFormula.realize_toFormula, Sum.elim_comp_inl, Sum.elim_comp_inr] at h'

Premises used: Sum.elim_comp_inr, Sum.elim_comp_inl, FirstOrder.Language.BoundedFormula.realize_toFormula
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
h : T ⊨ᵇ φ
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
v : α → M
xs : Fin n → M
h' : φ.Realize v xs
⊢ φ.Realize v xs

Tactic:
h'
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
h : T ⊨ᵇ φ
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
v : α → M
xs : Fin n → M
h' : φ.Realize v xs
⊢ φ.Realize v xs

Tactic:
exact h'
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
α : Type w
T' : L.Theory
h : ∀ φ ∈ T', T ⊨ᵇ φ
φ : L.Formula α
hφ : T' ⊨ᵇ φ
M : T.ModelType
⊢ (↑M : Type (max (max u v) w)) ⊨ T'

Tactic:
have hM : M ⊨ T' := T'.model_iff.2 (fun ψ hψ => (h ψ hψ).realize_sentence M)
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
α : Type w
T' : L.Theory
h : ∀ φ ∈ T', T ⊨ᵇ φ
φ : L.Formula α
hφ : T' ⊨ᵇ φ
M : T.ModelType
hM : (↑M : Type (max (max u v) w)) ⊨ T'
M' : T'.ModelType := ModelType.mk (T := T') (↑M : Type (max (max u v) w))
⊢ ∀ (v : α → (↑M : Type (max (max u v) w))) (xs : Fin 0 → (↑M : Type (max (max u v) w))), BoundedFormula.Realize φ v xs

Tactic:
hφ M'
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
α : Type w
T' : L.Theory
h : ∀ φ ∈ T', T ⊨ᵇ φ
φ : L.Formula α
hφ : T' ⊨ᵇ φ
M : T.ModelType
hM : (↑M : Type (max (max u v) w)) ⊨ T'
M' : T'.ModelType := ModelType.mk (T := T') (↑M : Type (max (max u v) w))
⊢ ∀ (v : α → (↑M : Type (max (max u v) w))) (xs : Fin 0 → (↑M : Type (max (max u v) w))), BoundedFormula.Realize φ v xs

Tactic:
exact hφ M'
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
simp :
  ¬(T ∪ {Formula.not φ}).IsSatisfiable ↔
    ∃ (T0 : Finset L.Sentence), (↑T0 : Set L.Sentence) ⊆ T ∧ ¬((↑T0 : Set L.Sentence) ∪ {Formula.not φ}).IsSatisfiable
⊢ T ⊨ᵇ φ ↔ ∃ (T0 : Finset L.Sentence), (↑T0 : Set L.Sentence) ⊆ T ∧ (↑T0 : Set L.Sentence) ⊨ᵇ φ

Tactic:
simp only [models_iff_not_satisfiable]

Premises used: FirstOrder.Language.Theory.models_iff_not_satisfiable
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
rw :
  (¬∀ (T0 : Finset L.Sentence), (↑T0 : Set L.Sentence) ⊆ T ∪ {Formula.not φ} → IsSatisfiable (↑T0 : Set L.Sentence)) ↔
    ∃ (T0 : Finset L.Sentence), (↑T0 : Set L.Sentence) ⊆ T ∧ ¬((↑T0 : Set L.Sentence) ∪ {Formula.not φ}).IsSatisfiable
⊢ ¬(T ∪ {Formula.not φ}).IsSatisfiable ↔
    ∃ (T0 : Finset L.Sentence), (↑T0 : Set L.Sentence) ⊆ T ∧ ¬((↑T0 : Set L.Sentence) ∪ {Formula.not φ}).IsSatisfiable

Tactic:
rw [isSatisfiable_iff_isFinitelySatisfiable, IsFinitelySatisfiable]

Premises used: FirstOrder.Language.Theory.isSatisfiable_iff_isFinitelySatisfiable, FirstOrder.Language.Theory.IsFinitelySatisfiable
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
contrapose! :
  (∀ (T0 : Finset L.Sentence), (↑T0 : Set L.Sentence) ⊆ T ∪ {Formula.not φ} → IsSatisfiable (↑T0 : Set L.Sentence)) ↔
    ∀ (T0 : Finset L.Sentence) (_ : (↑T0 : Set L.Sentence) ⊆ T),
      ((↑T0 : Set L.Sentence) ∪ {Formula.not φ}).IsSatisfiable
⊢ (¬∀ (T0 : Finset L.Sentence), (↑T0 : Set L.Sentence) ⊆ T ∪ {Formula.not φ} → IsSatisfiable (↑T0 : Set L.Sentence)) ↔
    ∃ (T0 : Finset L.Sentence), (↑T0 : Set L.Sentence) ⊆ T ∧ ¬((↑T0 : Set L.Sentence) ∪ {Formula.not φ}).IsSatisfiable

Tactic:
contrapose!
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
mp :
  (∀ (T0 : Finset L.Sentence), (↑T0 : Set L.Sentence) ⊆ T ∪ {Formula.not φ} → IsSatisfiable (↑T0 : Set L.Sentence)) →
    ∀ (T0 : Finset L.Sentence) (_ : (↑T0 : Set L.Sentence) ⊆ T),
      ((↑T0 : Set L.Sentence) ∪ {Formula.not φ}).IsSatisfiable
mpr :
  (∀ (T0 : Finset L.Sentence) (_ : (↑T0 : Set L.Sentence) ⊆ T),
      ((↑T0 : Set L.Sentence) ∪ {Formula.not φ}).IsSatisfiable) →
    ∀ (T0 : Finset L.Sentence), (↑T0 : Set L.Sentence) ⊆ T ∪ {Formula.not φ} → IsSatisfiable (↑T0 : Set L.Sentence)
⊢ (∀ (T0 : Finset L.Sentence), (↑T0 : Set L.Sentence) ⊆ T ∪ {Formula.not φ} → IsSatisfiable (↑T0 : Set L.Sentence)) ↔
    ∀ (T0 : Finset L.Sentence) (_ : (↑T0 : Set L.Sentence) ⊆ T),
      ((↑T0 : Set L.Sentence) ∪ {Formula.not φ}).IsSatisfiable

Tactic:
constructor
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
h : ∀ (T0 : Finset L.Sentence), (↑T0 : Set L.Sentence) ⊆ T ∪ {Formula.not φ} → IsSatisfiable (↑T0 : Set L.Sentence)
T0 : Finset L.Sentence
hT0 : (↑T0 : Set L.Sentence) ⊆ T
simp : (↑T0 : Set L.Sentence) ∪ {Formula.not φ} ⊆ T ∪ {Formula.not φ}
⊢ (↑(T0 ∪ {Formula.not φ}) : Set L.Sentence) ⊆ T ∪ {Formula.not φ}

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

Premises used: Finset.coe_singleton, Finset.coe_union
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
h : ∀ (T0 : Finset L.Sentence), (↑T0 : Set L.Sentence) ⊆ T ∪ {Formula.not φ} → IsSatisfiable (↑T0 : Set L.Sentence)
T0 : Finset L.Sentence
hT0 : (↑T0 : Set L.Sentence) ⊆ T
⊢ (↑T0 : Set L.Sentence) ∪ {Formula.not φ} ⊆ T ∪ {Formula.not φ}

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

Premises used: Set.Subset.refl, Set.union_subset_union
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
h : ∀ (T0 : Finset L.Sentence), (↑T0 : Set L.Sentence) ⊆ T ∪ {Formula.not φ} → IsSatisfiable (↑T0 : Set L.Sentence)
T0 : Finset L.Sentence
hT0 : (↑T0 : Set L.Sentence) ⊆ T
⊢ (↑T0 : Set L.Sentence) ∪ {Formula.not φ} ⊆ T ∪ {Formula.not φ}

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

Premises used: Set.Subset.refl, Set.union_subset_union
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
h : ∀ (T0 : Finset L.Sentence), (↑T0 : Set L.Sentence) ⊆ T ∪ {Formula.not φ} → IsSatisfiable (↑T0 : Set L.Sentence)
T0 : Finset L.Sentence
hT0 : (↑T0 : Set L.Sentence) ⊆ T
⊢ ((↑T0 : Set L.Sentence) ∪ {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 _))

Premises used: FirstOrder.Language.Formula.not, Union.union, Singleton.singleton
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
h :
  ∀ (T0 : Finset L.Sentence) (_ : (↑T0 : Set L.Sentence) ⊆ T), ((↑T0 : Set L.Sentence) ∪ {Formula.not φ}).IsSatisfiable
T0 : Finset L.Sentence
hT0 : (↑T0 : Set L.Sentence) ⊆ T ∪ {Formula.not φ}
⊢ (↑(T0.erase (Formula.not φ)) : Set L.Sentence) ⊆ T

Tactic:
simpa using hT0
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
h :
  ∀ (T0 : Finset L.Sentence) (_ : (↑T0 : Set L.Sentence) ⊆ T), ((↑T0 : Set L.Sentence) ∪ {Formula.not φ}).IsSatisfiable
T0 : Finset L.Sentence
hT0 : (↑T0 : Set L.Sentence) ⊆ T ∪ {Formula.not φ}
⊢ (↑T0 : Set L.Sentence) ⊆ (↑(T0.erase (Formula.not φ)) : Set L.Sentence) ∪ {Formula.not φ}

Tactic:
simp
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
h :
  ∀ (T0 : Finset L.Sentence) (_ : (↑T0 : Set L.Sentence) ⊆ T), ((↑T0 : Set L.Sentence) ∪ {Formula.not φ}).IsSatisfiable
T0 : Finset L.Sentence
hT0 : (↑T0 : Set L.Sentence) ⊆ T ∪ {Formula.not φ}
⊢ IsSatisfiable (↑T0 : Set L.Sentence)

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

Premises used: FirstOrder.Language.Formula.not, FirstOrder.Language.Theory.IsSatisfiable.mono, Finset.erase
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
inl : ∀ (hφ : T ⊨ᵇ φ), T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ
inr : ∀ (hφn : T ⊨ᵇ Formula.not φ), T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ

Tactic:
rcases h.2 φ with hφ | hφn

Premises used: And.right
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφ : T ⊨ᵇ φ
inl : ¬T ⊨ᵇ Formula.not φ
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ

Tactic:
simp only [hφ, not_true, iff_false]

Premises used: iff_false, not_true
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφ : T ⊨ᵇ φ
inl : ∃ (x : T.ModelType), ¬(↑x : Type (max u v)) ⊨ Formula.not φ
⊢ ¬T ⊨ᵇ Formula.not φ

Tactic:
rw [models_sentence_iff, not_forall]

Premises used: FirstOrder.Language.Theory.models_sentence_iff, Classical.not_forall
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφ : T ⊨ᵇ φ
⊢ ∃ (x : T.ModelType), ¬(↑x : Type (max u v)) ⊨ Formula.not φ

Tactic:
⟨h.1.some, ?_⟩

Premises used: Nonempty.some, And.left, Exists.intro
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφ : T ⊨ᵇ φ
inl : ¬(↑(Nonempty.some ⋯) : Type (max u v)) ⊨ Formula.not φ
⊢ ∃ (x : T.ModelType), ¬(↑x : Type (max u v)) ⊨ Formula.not φ

Tactic:
refine ⟨h.1.some, ?_⟩
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφ : T ⊨ᵇ φ
inl : (↑(Nonempty.some ⋯) : Type (max u v)) ⊨ φ
⊢ ¬(↑(Nonempty.some ⋯) : Type (max u v)) ⊨ Formula.not φ

Tactic:
simp only [Sentence.realize_not, Classical.not_not]

Premises used: Classical.not_not, FirstOrder.Language.Sentence.realize_not
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφ : T ⊨ᵇ φ
⊢ (↑(Nonempty.some ⋯) : Type (max u v)) ⊨ φ

Tactic:
models_sentence_iff.1 hφ _

Premises used: FirstOrder.Language.Theory.models_sentence_iff, Iff.mp
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφ : T ⊨ᵇ φ
⊢ (↑(Nonempty.some ⋯) : Type (max u v)) ⊨ φ

Tactic:
exact models_sentence_iff.1 hφ _

Premises used: FirstOrder.Language.Theory.models_sentence_iff, Iff.mp
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφn : T ⊨ᵇ Formula.not φ
inr : ¬T ⊨ᵇ φ
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ

Tactic:
simp only [hφn, true_iff]

Premises used: true_iff
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφn : T ⊨ᵇ Formula.not φ
hφ : T ⊨ᵇ φ
⊢ ∀ (M : T.ModelType), (↑M : Type (max u v)) ⊨ Formula.not φ

Tactic:
rw [models_sentence_iff] at *

Premises used: FirstOrder.Language.Theory.models_sentence_iff
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφn : T ⊨ᵇ Formula.not φ
hφ : T ⊨ᵇ φ
hφn₁ : ∀ (M : T.ModelType), (↑M : Type (max u v)) ⊨ Formula.not φ
⊢ ∀ (M : T.ModelType), (↑M : Type (max u v)) ⊨ φ

Tactic:
rw [models_sentence_iff] at *

Premises used: FirstOrder.Language.Theory.models_sentence_iff
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφn : ∀ (M : T.ModelType), (↑M : Type (max u v)) ⊨ Formula.not φ
hφ : ∀ (M : T.ModelType), (↑M : Type (max u v)) ⊨ φ
⊢ False

Tactic:
hφn h.1.some (hφ _)

Premises used: Nonempty.some, FirstOrder.Language.BoundedFormula.Realize, And.left
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφn : ∀ (M : T.ModelType), (↑M : Type (max u v)) ⊨ Formula.not φ
hφ : ∀ (M : T.ModelType), (↑M : Type (max u v)) ⊨ φ
⊢ False

Tactic:
exact hφn h.1.some (hφ _)

Premises used: Nonempty.some, And.left
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
inl : ∀ (hφ : T ⊨ᵇ φ), M ⊨ φ ↔ T ⊨ᵇ φ
inr : ∀ (hφn : T ⊨ᵇ Formula.not φ), M ⊨ φ ↔ T ⊨ᵇ φ
⊢ M ⊨ φ ↔ T ⊨ᵇ φ

Tactic:
rcases h.2 φ with hφ | hφn

Premises used: And.right
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
hφ : T ⊨ᵇ φ
⊢ M ⊨ φ ↔ T ⊨ᵇ φ

Tactic:
iff_of_true (hφ.realize_sentence M) hφ

Premises used: FirstOrder.Language.Theory.ModelsBoundedFormula.realize_sentence, iff_of_true
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
hφ : T ⊨ᵇ φ
⊢ M ⊨ φ ↔ T ⊨ᵇ φ

Tactic:
exact iff_of_true (hφ.realize_sentence M) hφ

Premises used: FirstOrder.Language.Theory.ModelsBoundedFormula.realize_sentence, iff_of_true
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
hφn : T ⊨ᵇ Formula.not φ
⊢ M ⊨ φ ↔ T ⊨ᵇ φ

Tactic:
iff_of_false ((Sentence.realize_not M).1 (hφn.realize_sentence M))
        ((h.models_not_iff φ).1 hφn)

Premises used: FirstOrder.Language.Theory.ModelsBoundedFormula.realize_sentence, FirstOrder.Language.Sentence.realize_not, FirstOrder.Language.Theory.IsComplete.models_not_iff, iff_of_false, Iff.mp
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
hφn : T ⊨ᵇ Formula.not φ
⊢ M ⊨ φ ↔ T ⊨ᵇ φ

Tactic:
exact
      iff_of_false ((Sentence.realize_not M).1 (hφn.realize_sentence M))
        ((h.models_not_iff φ).1 hφn)

Premises used: FirstOrder.Language.Theory.ModelsBoundedFormula.realize_sentence, FirstOrder.Language.Sentence.realize_not, FirstOrder.Language.Theory.IsComplete.models_not_iff, iff_of_false, Iff.mp