awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
M : Type w'
inst : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #(↑N0 : Type (max (max (max u w') v) w))
N : Bundled L[[M]].Structure
hN : #(↑N : Type w) = κ
NN0 : (↑N : Type w) ↪ₑ[L[[M]]] (↑N0 : Type (max (max (max u v) w) w'))
this : Structure.{u, v, w} L (↑N : Type w) := (L.lhomWithConstants M).reduct (↑N : Type w)
h : (↑N : Type w) ⊨ L.elementaryDiagram M
⊢ ∃ (N : Bundled L.Structure), Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w)) ∧ #(↑N : Type w) = κ

Tactic:
⟨Bundled.of N, ⟨?_⟩, hN⟩

Premises used: Nonempty.intro, CategoryTheory.Bundled.of, CategoryTheory.Bundled.α, And.intro, Exists.intro
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
M : Type w'
inst : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #(↑N0 : Type (max (max (max u w') v) w))
N : Bundled L[[M]].Structure
hN : #(↑N : Type w) = κ
NN0 : (↑N : Type w) ↪ₑ[L[[M]]] (↑N0 : Type (max (max (max u v) w) w'))
this : Structure.{u, v, w} L (↑N : Type w) := (L.lhomWithConstants M).reduct (↑N : Type w)
h : (↑N : Type w) ⊨ L.elementaryDiagram M
refine : ElementaryEmbedding.{w', w, u, v} L M (↑(Bundled.of (↑N : Type w)) : Type w)
⊢ ∃ (N : Bundled L.Structure), Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w)) ∧ #(↑N : Type w) = κ

Tactic:
refine ⟨Bundled.of N, ⟨?_⟩, hN⟩
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
M : Type w'
inst : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #(↑N0 : Type (max (max (max u w') v) w))
N : Bundled L[[M]].Structure
hN : #(↑N : Type w) = κ
NN0 : (↑N : Type w) ↪ₑ[L[[M]]] (↑N0 : Type (max (max (max u v) w) w'))
this : Structure.{u, v, w} L (↑N : Type w) := (L.lhomWithConstants M).reduct (↑N : Type w)
h : (↑N : Type w) ⊨ L.elementaryDiagram M
⊢ ElementaryEmbedding.{w', w, u, v} L M (↑(Bundled.of (↑N : Type w)) : Type w)

Tactic:
apply ElementaryEmbedding.ofModelsElementaryDiagram L M N

Premises used: CategoryTheory.Bundled.α, FirstOrder.Language.ElementaryEmbedding.ofModelsElementaryDiagram
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
M : Type w'
inst : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h : lift.{w', w} κ ≤ lift.{w, w'} #M
inl :
  ∀ (N : Bundled L.Structure) (hN1 : Nonempty (ElementaryEmbedding.{w, w', u, v} L (↑N : Type w) M))
    (hN2 : #(↑N : Type w) = κ),
    ∃ (N : Bundled L.Structure),
      (Nonempty (ElementaryEmbedding.{w, w', u, v} L (↑N : Type w) M) ∨
          Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w))) ∧
        #(↑N : Type w) = κ
⊢ ∃ (N : Bundled L.Structure),
    (Nonempty (ElementaryEmbedding.{w, w', u, v} L (↑N : Type w) M) ∨
        Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w))) ∧
      #(↑N : Type w) = κ

Tactic:
obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_le L M κ h1 h2 h

Premises used: FirstOrder.Language.exists_elementaryEmbedding_card_eq_of_le
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
M : Type w'
inst : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h : lift.{w', w} κ ≤ lift.{w, w'} #M
N : Bundled L.Structure
hN1 : Nonempty (ElementaryEmbedding.{w, w', u, v} L (↑N : Type w) M)
hN2 : #(↑N : Type w) = κ
⊢ ∃ (N : Bundled L.Structure),
    (Nonempty (ElementaryEmbedding.{w, w', u, v} L (↑N : Type w) M) ∨
        Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w))) ∧
      #(↑N : Type w) = κ

Tactic:
⟨N, Or.inl hN1, hN2⟩

Premises used: And.intro, Exists.intro, Or.inl
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
M : Type w'
inst : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h : lift.{w', w} κ ≤ lift.{w, w'} #M
N : Bundled L.Structure
hN1 : Nonempty (ElementaryEmbedding.{w, w', u, v} L (↑N : Type w) M)
hN2 : #(↑N : Type w) = κ
⊢ ∃ (N : Bundled L.Structure),
    (Nonempty (ElementaryEmbedding.{w, w', u, v} L (↑N : Type w) M) ∨
        Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w))) ∧
      #(↑N : Type w) = κ

Tactic:
exact ⟨N, Or.inl hN1, hN2⟩
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
M : Type w'
inst : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h : lift.{w, w'} #M < lift.{w', w} κ
inr :
  ∀ (N : Bundled L.Structure) (hN1 : Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w)))
    (hN2 : #(↑N : Type w) = κ),
    ∃ (N : Bundled L.Structure),
      (Nonempty (ElementaryEmbedding.{w, w', u, v} L (↑N : Type w) M) ∨
          Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w))) ∧
        #(↑N : Type w) = κ
⊢ ∃ (N : Bundled L.Structure),
    (Nonempty (ElementaryEmbedding.{w, w', u, v} L (↑N : Type w) M) ∨
        Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w))) ∧
      #(↑N : Type w) = κ

Tactic:
obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_ge L M κ h2 (le_of_lt h)

Premises used: le_of_lt, FirstOrder.Language.exists_elementaryEmbedding_card_eq_of_ge
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
M : Type w'
inst : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h : lift.{w, w'} #M < lift.{w', w} κ
N : Bundled L.Structure
hN1 : Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w))
hN2 : #(↑N : Type w) = κ
⊢ ∃ (N : Bundled L.Structure),
    (Nonempty (ElementaryEmbedding.{w, w', u, v} L (↑N : Type w) M) ∨
        Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w))) ∧
      #(↑N : Type w) = κ

Tactic:
⟨N, Or.inr hN1, hN2⟩

Premises used: And.intro, Exists.intro, Or.inr
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
M : Type w'
inst : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h : lift.{w, w'} #M < lift.{w', w} κ
N : Bundled L.Structure
hN1 : Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w))
hN2 : #(↑N : Type w) = κ
⊢ ∃ (N : Bundled L.Structure),
    (Nonempty (ElementaryEmbedding.{w, w', u, v} L (↑N : Type w) M) ∨
        Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w))) ∧
      #(↑N : Type w) = κ

Tactic:
exact ⟨N, Or.inr hN1, hN2⟩
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
M : Type w'
inst : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
⊢ lift.{w', w} κ ≤ lift.{w, w'} #M ∨ lift.{w, w'} #M < lift.{w', w} κ

Tactic:
cases le_or_gt (lift.{w'} κ) (Cardinal.lift.{w} #M) with
  | inl h =>
    obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_le L M κ h1 h2 h
    exact ⟨N, Or.inl hN1, hN2⟩
  | inr h =>
    obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_ge L M κ h2 (le_of_lt h)
    exact ⟨N, Or.inr hN1, hN2⟩
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
M : Type w'
inst : L.Structure M
inst_1 : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
inl :
  ∀ (N : Bundled L.Structure) (hNκ : #(↑N : Type w) = κ)
    (NM : Nonempty (ElementaryEmbedding.{w, w', u, v} L (↑N : Type w) M)),
    ∃ (N : Bundled L.Structure), ElementarilyEquivalent.{u, v, w', w} L M (↑N : Type w) ∧ #(↑N : Type w) = κ
inr :
  ∀ (N : Bundled L.Structure) (hNκ : #(↑N : Type w) = κ)
    (MN : Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w))),
    ∃ (N : Bundled L.Structure), ElementarilyEquivalent.{u, v, w', w} L M (↑N : Type w) ∧ #(↑N : Type w) = κ
⊢ ∃ (N : Bundled L.Structure), ElementarilyEquivalent.{u, v, w', w} L M (↑N : Type w) ∧ #(↑N : Type w) = κ

Tactic:
obtain ⟨N, NM | MN, hNκ⟩ := exists_elementaryEmbedding_card_eq L M κ h1 h2

Premises used: FirstOrder.Language.exists_elementaryEmbedding_card_eq
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
M : Type w'
inst : L.Structure M
inst_1 : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
N : Bundled L.Structure
hNκ : #(↑N : Type w) = κ
NM : Nonempty (ElementaryEmbedding.{w, w', u, v} L (↑N : Type w) M)
⊢ ∃ (N : Bundled L.Structure), ElementarilyEquivalent.{u, v, w', w} L M (↑N : Type w) ∧ #(↑N : Type w) = κ

Tactic:
⟨N, NM.some.elementarilyEquivalent.symm, hNκ⟩

Premises used: FirstOrder.Language.ElementarilyEquivalent.symm, FirstOrder.Language.ElementaryEmbedding.elementarilyEquivalent, Nonempty.some, And.intro, Exists.intro
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
M : Type w'
inst : L.Structure M
inst_1 : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
N : Bundled L.Structure
hNκ : #(↑N : Type w) = κ
NM : Nonempty (ElementaryEmbedding.{w, w', u, v} L (↑N : Type w) M)
⊢ ∃ (N : Bundled L.Structure), ElementarilyEquivalent.{u, v, w', w} L M (↑N : Type w) ∧ #(↑N : Type w) = κ

Tactic:
exact ⟨N, NM.some.elementarilyEquivalent.symm, hNκ⟩
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
M : Type w'
inst : L.Structure M
inst_1 : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
N : Bundled L.Structure
hNκ : #(↑N : Type w) = κ
MN : Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w))
⊢ ∃ (N : Bundled L.Structure), ElementarilyEquivalent.{u, v, w', w} L M (↑N : Type w) ∧ #(↑N : Type w) = κ

Tactic:
⟨N, MN.some.elementarilyEquivalent, hNκ⟩

Premises used: FirstOrder.Language.ElementaryEmbedding.elementarilyEquivalent, Nonempty.some, And.intro, Exists.intro
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
M : Type w'
inst : L.Structure M
inst_1 : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
N : Bundled L.Structure
hNκ : #(↑N : Type w) = κ
MN : Nonempty (ElementaryEmbedding.{w', w, u, v} L M (↑N : Type w))
⊢ ∃ (N : Bundled L.Structure), ElementarilyEquivalent.{u, v, w', w} L M (↑N : Type w) ∧ #(↑N : Type w) = κ

Tactic:
exact ⟨N, MN.some.elementarilyEquivalent, hNκ⟩
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
M : T.ModelType
MI : Infinite (↑M : Type (max u v))
intro :
  ∀ (N : Bundled L.Structure) (hN : (↑M : Type (max u v)) ≅[L] (↑N : Type w)) (h1 : ℵ₀ ≤ #(↑N : Type w))
    (h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} #(↑N : Type w)),
    ∃ (N_1 : ModelType.{u, v, w} T), #(↑N_1 : Type w) = #(↑N : Type w)
⊢ ∃ (N : ModelType.{u, v, w} T), #(↑N : Type w) = κ

Tactic:
obtain ⟨N, hN, rfl⟩ := exists_elementarilyEquivalent_card_eq L M κ h1 h2

Premises used: FirstOrder.Language.exists_elementarilyEquivalent_card_eq, FirstOrder.Language.Theory.ModelType.Carrier, rfl
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
M : T.ModelType
MI : Infinite (↑M : Type (max u v))
N : Bundled L.Structure
hN : (↑M : Type (max u v)) ≅[L] (↑N : Type w)
h1 : ℵ₀ ≤ #(↑N : Type w)
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} #(↑N : Type w)
⊢ Nonempty.{w + 1} (↑N : Type w)

Tactic:
haveI : Nonempty N := hN.nonempty
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
M : T.ModelType
MI : Infinite (↑M : Type (max u v))
N : Bundled L.Structure
hN : (↑M : Type (max u v)) ≅[L] (↑N : Type w)
h1 : ℵ₀ ≤ #(↑N : Type w)
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} #(↑N : Type w)
this : Nonempty.{w + 1} (↑N : Type w)
⊢ ∃ (N_1 : ModelType.{u, v, w} T), #(↑N_1 : Type w) = #(↑N : Type w)

Tactic:
⟨hN.theory_model.bundled, rfl⟩

Premises used: FirstOrder.Language.ElementarilyEquivalent.theory_model, Exists.intro, FirstOrder.Language.Theory.Model.bundled, rfl
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
M : T.ModelType
MI : Infinite (↑M : Type (max u v))
N : Bundled L.Structure
hN : (↑M : Type (max u v)) ≅[L] (↑N : Type w)
h1 : ℵ₀ ≤ #(↑N : Type w)
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} #(↑N : Type w)
this : Nonempty.{w + 1} (↑N : Type w)
⊢ ∃ (N_1 : ModelType.{u, v, w} T), #(↑N_1 : Type w) = #(↑N : Type w)

Tactic:
exact ⟨hN.theory_model.bundled, rfl⟩
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : ∃ (M : T.ModelType), Infinite (↑M : Type (max u v))
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
intro : ∀ (M : T.ModelType) (MI : Infinite (↑M : Type (max u v))), ∃ (N : ModelType.{u, v, w} T), #(↑N : Type w) = κ
⊢ ∃ (N : ModelType.{u, v, w} T), #(↑N : Type w) = κ

Tactic:
cases h with
  | intro M MI =>
    obtain ⟨N, hN, rfl⟩ := exists_elementarilyEquivalent_card_eq L M κ h1 h2
    haveI : Nonempty N := hN.nonempty
    exact ⟨hN.theory_model.bundled, rfl⟩

Premises used: rfl
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
⊢ T ⊨ᵇ φ ↔ ∀ (M : T.ModelType) (v : α → (↑M : Type (max (max u v) w))), φ.Realize v

Tactic:
forall_congr' fun _ => forall_congr' fun _ => Unique.forall_iff

Premises used: FirstOrder.Language.Theory.ModelsBoundedFormula, Unique.forall_iff, forall_congr'
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
⊢ T ⊨ᵇ φ ↔ ∀ (M : T.ModelType), (↑M : Type (max u v)) ⊨ φ

Tactic:
models_formula_iff.trans (forall_congr' fun _ => Unique.forall_iff)

Premises used: FirstOrder.Language.Theory.models_formula_iff, Unique.forall_iff, forall_congr', Iff.trans
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
h : φ ∈ T
⊢ T ⊨ᵇ φ

Tactic:
models_sentence_iff.2 fun _ => realize_sentence_of_mem T h

Premises used: Iff.mpr, FirstOrder.Language.Theory.models_sentence_iff, FirstOrder.Language.Theory.realize_sentence_of_mem
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
rw : (∀ (M : T.ModelType), (↑M : Type (max u v)) ⊨ φ) ↔ ¬Nonempty (T ∪ {Formula.not φ}).ModelType
⊢ T ⊨ᵇ φ ↔ ¬(T ∪ {Formula.not φ}).IsSatisfiable

Tactic:
rw [models_sentence_iff, IsSatisfiable]

Premises used: FirstOrder.Language.Theory.IsSatisfiable, FirstOrder.Language.Theory.models_sentence_iff
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
⊢ (∀ (M : T.ModelType), (↑M : Type (max u v)) ⊨ φ) ↔ ¬Nonempty (T ∪ {Formula.not φ}).ModelType

Tactic:
⟨fun h1 h2 =>
      (Sentence.realize_not _).1
        (realize_sentence_of_mem (T ∪ {Formula.not φ})
          (Set.subset_union_right (Set.mem_singleton _)))
        (h1 (h2.some.subtheoryModel Set.subset_union_left)),
      fun h M => ?_⟩

Premises used: Set.mem_singleton, Set.subset_union_right, FirstOrder.Language.Sentence.realize_not, Nonempty.some, Set.subset_union_left, FirstOrder.Language.Formula.not, Iff.intro, FirstOrder.Language.Theory.ModelType.Carrier, Iff.mp, Union.union, Singleton.singleton, FirstOrder.Language.Theory.realize_sentence_of_mem, FirstOrder.Language.Theory.ModelType.subtheoryModel
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
h1 : ∀ (h : ¬Nonempty (T ∪ {Formula.not φ}).ModelType) (M : T.ModelType), (↑M : Type (max u v)) ⊨ φ
⊢ (∀ (M : T.ModelType), (↑M : Type (max u v)) ⊨ φ) ↔ ¬Nonempty (T ∪ {Formula.not φ}).ModelType

Tactic:
refine
    ⟨fun h1 h2 =>
      (Sentence.realize_not _).1
        (realize_sentence_of_mem (T ∪ {Formula.not φ})
          (Set.subset_union_right (Set.mem_singleton _)))
        (h1 (h2.some.subtheoryModel Set.subset_union_left)),
      fun h M => ?_⟩
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
h : ¬Nonempty (T ∪ {Formula.not φ}).ModelType
M : T.ModelType
contrapose : ∀ (h : ¬(↑M : Type (max u v)) ⊨ φ), Nonempty (T ∪ {Formula.not φ}).ModelType
⊢ (↑M : Type (max u v)) ⊨ φ

Tactic:
contrapose h
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
M : T.ModelType
h : ¬(↑M : Type (max u v)) ⊨ φ
⊢ (↑M : Type (max u v)) ⊨ Formula.not φ

Tactic:
rw [← Sentence.realize_not] at h

Premises used: FirstOrder.Language.Sentence.realize_not
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
M : T.ModelType
h : (↑M : Type (max u v)) ⊨ Formula.not φ
⊢ Nonempty (T ∪ {Formula.not φ}).ModelType

Tactic:
⟨{  Carrier := M
        is_model := ⟨fun ψ hψ => hψ.elim (realize_sentence_of_mem _) fun h' => ?_⟩ }⟩

Premises used: Nonempty.intro, FirstOrder.Language.Theory.ModelType.mk, FirstOrder.Language.Theory.ModelType.Carrier
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
M : T.ModelType
h : (↑M : Type (max u v)) ⊨ Formula.not φ
Carrier :
  ∀ (ψ : L.Sentence) (hψ : ψ ∈ T ∪ {Formula.not φ}) (h' : Membership.mem (γ := Set L.Sentence) {Formula.not φ} ψ),
    (↑M : Type (max u v)) ⊨ ψ
⊢ Nonempty (T ∪ {Formula.not φ}).ModelType

Tactic:
refine
    ⟨{  Carrier := M
        is_model := ⟨fun ψ hψ => hψ.elim (realize_sentence_of_mem _) fun h' => ?_⟩ }⟩
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
M : T.ModelType
h : (↑M : Type (max u v)) ⊨ Formula.not φ
ψ : L.Sentence
hψ : ψ ∈ T ∪ {Formula.not φ}
h' : Membership.mem (γ := Set L.Sentence) {Formula.not φ} ψ
rw : (↑M : Type (max u v)) ⊨ Formula.not φ
⊢ (↑M : Type (max u v)) ⊨ ψ

Tactic:
rw [Set.mem_singleton_iff.1 h']

Premises used: Set.mem_singleton_iff, Iff.mp
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
M : T.ModelType
h : (↑M : Type (max u v)) ⊨ Formula.not φ
ψ : L.Sentence
hψ : ψ ∈ T ∪ {Formula.not φ}
h' : Membership.mem (γ := Set L.Sentence) {Formula.not φ} ψ
⊢ (↑M : Type (max u v)) ⊨ Formula.not φ

Tactic:
h
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
M : T.ModelType
h : (↑M : Type (max u v)) ⊨ Formula.not φ
ψ : L.Sentence
hψ : ψ ∈ T ∪ {Formula.not φ}
h' : Membership.mem (γ := Set L.Sentence) {Formula.not φ} ψ
⊢ (↑M : Type (max u v)) ⊨ Formula.not φ

Tactic:
exact h
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
h : T ⊨ᵇ φ
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
rw : ∀ (h : ¬(T ∪ {Formula.not φ}).IsSatisfiable) (M : Type u_1) [inst : L.Structure M] [M ⊨ T] [Nonempty M], M ⊨ φ
⊢ M ⊨ φ

Tactic:
rw [models_iff_not_satisfiable] at h

Premises used: FirstOrder.Language.Theory.models_iff_not_satisfiable
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
h : ¬(T ∪ {Formula.not φ}).IsSatisfiable
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
contrapose : ∀ (h : ¬M ⊨ φ), (T ∪ {Formula.not φ}).IsSatisfiable
⊢ M ⊨ φ

Tactic:
contrapose h
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
h : ¬M ⊨ φ
simp : ¬M ⊨ φ ∧ ∀ a ∈ T, M ⊨ a
⊢ M ⊨ T ∪ {Formula.not φ}

Tactic:
simp only [Set.union_singleton, model_iff, Set.mem_insert_iff, forall_eq_or_imp,
      Sentence.realize_not]

Premises used: FirstOrder.Language.Theory.model_iff, FirstOrder.Language.Sentence.realize_not, forall_eq_or_imp, Set.mem_insert_iff, Set.union_singleton
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
h : ¬M ⊨ φ
rw : ¬M ⊨ φ ∧ M ⊨ T
⊢ ¬M ⊨ φ ∧ ∀ a ∈ T, M ⊨ a

Tactic:
rw [← model_iff]

Premises used: FirstOrder.Language.Theory.model_iff
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
h : ¬M ⊨ φ
⊢ ¬M ⊨ φ ∧ M ⊨ T

Tactic:
⟨h, inferInstance⟩

Premises used: inferInstance, And.intro
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
h : ¬M ⊨ φ
⊢ ¬M ⊨ φ ∧ M ⊨ T

Tactic:
exact ⟨h, inferInstance⟩
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
h : ¬M ⊨ φ
⊢ M ⊨ T ∪ {Formula.not φ}

Tactic:
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⟩
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
h : ¬M ⊨ φ
this : M ⊨ T ∪ {Formula.not φ}
⊢ (T ∪ {Formula.not φ}).IsSatisfiable

Tactic:
Model.isSatisfiable M

Premises used: FirstOrder.Language.Theory.Model.isSatisfiable
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
φ : L.Sentence
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
h : ¬M ⊨ φ
this : M ⊨ T ∪ {Formula.not φ}
⊢ (T ∪ {Formula.not φ}).IsSatisfiable

Tactic:
exact Model.isSatisfiable M

Premises used: FirstOrder.Language.Theory.Model.isSatisfiable
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
⊢ T ⊨ᵇ φ ↔
    ((L.lhomWithConstants α).onTheory T).ModelsBoundedFormula (α := Empty) (n := 0)
      ((Formula.equivSentence : (a : L.Formula α) → L[[α]].Sentence) φ)

Tactic:
⟨fun h => models_sentence_iff.2 (fun M => ?_),
    fun h => models_formula_iff.2 (fun M v => ?_)⟩

Premises used: Iff.mpr, FirstOrder.Language.Theory.models_formula_iff, FirstOrder.Language.Theory.models_sentence_iff, Iff.intro
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
refine_1 :
  ∀ (h : T ⊨ᵇ φ) (M : ((L.lhomWithConstants α).onTheory T).ModelType),
    Sentence.Realize (L := L[[α]]) (↑M : Type (max (max u w) v))
      ((Formula.equivSentence : (a : L.Formula α) → L[[α]].Sentence) φ)
refine_2 :
  ∀
    (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))), φ.Realize v
⊢ T ⊨ᵇ φ ↔
    ((L.lhomWithConstants α).onTheory T).ModelsBoundedFormula (α := Empty) (n := 0)
      ((Formula.equivSentence : (a : L.Formula α) → L[[α]].Sentence) φ)

Tactic:
refine ⟨fun h => models_sentence_iff.2 (fun M => ?_),
    fun h => models_formula_iff.2 (fun M v => ?_)⟩
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : T ⊨ᵇ φ
M : ((L.lhomWithConstants α).onTheory T).ModelType
this : L.Structure (↑M : Type (max (max u v) w)) := (L.lhomWithConstants α).reduct (↑M : Type (max (max u v) w))
refine_1 : φ.Realize (M := (↑M : Type (max (max u w) v))) fun (a : α) ↦ (↑(L.con a) : (↑M : Type (max (max u w) v)))
⊢ Sentence.Realize (L := L[[α]]) (↑M : Type (max (max u w) v))
    ((Formula.equivSentence : (a : L.Formula α) → L[[α]].Sentence) φ)

Tactic:
rw [Formula.realize_equivSentence]

Premises used: FirstOrder.Language.Formula.realize_equivSentence
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : T ⊨ᵇ φ
M : ((L.lhomWithConstants α).onTheory T).ModelType
this : L.Structure (↑M : Type (max (max u v) w)) := (L.lhomWithConstants α).reduct (↑M : Type (max (max u v) w))
⊢ (↑M : Type (max (max u v) w)) ⊨ T

Tactic:
have : M ⊨ T := (LHom.onTheory_model _ _).1 M.is_model