awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsComplete
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
h₁ :
  ∀ (φ : L.BoundedFormula Empty 0),
    Membership.mem (γ := Set (L.BoundedFormula Empty 0)) {φ : L.BoundedFormula Empty 0 | T ⊨ᵇ φ} φ ↔
      φ ∈ L.completeTheory M
⊢ {φ : L.BoundedFormula Empty 0 | T ⊨ᵇ φ} = L.completeTheory M

Tactic:
ext φ
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsComplete
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
φ : L.BoundedFormula Empty 0
h₁ : T ⊨ᵇ φ ↔ M ⊨ φ
⊢ Membership.mem (γ := Set (L.BoundedFormula Empty 0)) {φ : L.BoundedFormula Empty 0 | T ⊨ᵇ φ} φ ↔
    φ ∈ L.completeTheory M

Tactic:
simp only [Set.mem_setOf_eq, L.mem_completeTheory]

Premises used: Set.mem_setOf_eq, FirstOrder.Language.mem_completeTheory
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsComplete
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
φ : L.BoundedFormula Empty 0
⊢ T ⊨ᵇ φ ↔ M ⊨ φ

Tactic:
⟨fun h_models => h_models.realize_sentence M, fun h_realize => ?_⟩

Premises used: FirstOrder.Language.Theory.ModelsBoundedFormula.realize_sentence, Iff.intro
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsComplete
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
φ : L.BoundedFormula Empty 0
h₁ : ∀ (h_realize : M ⊨ φ), T ⊨ᵇ φ
⊢ T ⊨ᵇ φ ↔ M ⊨ φ

Tactic:
refine ⟨fun h_models => h_models.realize_sentence M, fun h_realize => ?_⟩
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsComplete
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
φ : L.BoundedFormula Empty 0
h_realize : M ⊨ φ
hT : T ⊨ᵇ φ
⊢ T ⊨ᵇ φ

Tactic:
hT
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsComplete
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
φ : L.BoundedFormula Empty 0
h_realize : M ⊨ φ
hT : T ⊨ᵇ φ
⊢ T ⊨ᵇ φ

Tactic:
exact hT
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsComplete
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
φ : L.BoundedFormula Empty 0
h_realize : M ⊨ φ
hT : T ⊨ᵇ Formula.not φ
⊢ M ⊨ ∼φ

Tactic:
have : M ⊨ φ.not := hT.realize_sentence M
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsComplete
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
φ : L.BoundedFormula Empty 0
h_realize : M ⊨ φ
hT : T ⊨ᵇ Formula.not φ
this : M ⊨ ∼φ
⊢ ¬M ⊨ φ

Tactic:
rw [Sentence.realize_not] at this

Premises used: FirstOrder.Language.Sentence.realize_not
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsComplete
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
φ : L.BoundedFormula Empty 0
h_realize : M ⊨ φ
hT : T ⊨ᵇ Formula.not φ
this : ¬M ⊨ φ
⊢ T ⊨ᵇ φ

Tactic:
contradiction
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsComplete
M : Type u_1
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Nonempty M
φ : L.BoundedFormula Empty 0
h_realize : M ⊨ φ
⊢ T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ

Tactic:
cases h.2 φ with
  | inl hT => exact hT
  | inr hT =>
      have : M ⊨ φ.not := hT.realize_sentence M
      rw [Sentence.realize_not] at this
      contradiction

Premises used: FirstOrder.Language.Sentence.realize_not, And.right
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
mp : T.IsComplete → T.IsSatisfiable ∧ ∀ (M N : T.ModelType), (↑M : Type (max u v)) ≅[L] (↑N : Type (max u v))
mpr : (T.IsSatisfiable ∧ ∀ (M N : T.ModelType), (↑M : Type (max u v)) ≅[L] (↑N : Type (max u v))) → T.IsComplete
⊢ T.IsComplete ↔ T.IsSatisfiable ∧ ∀ (M N : T.ModelType), (↑M : Type (max u v)) ≅[L] (↑N : Type (max u v))

Tactic:
constructor
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
hcomp : T.IsComplete
⊢ T.IsSatisfiable ∧ ∀ (M N : T.ModelType), (↑M : Type (max u v)) ≅[L] (↑N : Type (max u v))

Tactic:
⟨hcomp.1, ?_⟩

Premises used: And.left, And.intro
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
hcomp : T.IsComplete
mp : ∀ (M N : T.ModelType), (↑M : Type (max u v)) ≅[L] (↑N : Type (max u v))
⊢ T.IsSatisfiable ∧ ∀ (M N : T.ModelType), (↑M : Type (max u v)) ≅[L] (↑N : Type (max u v))

Tactic:
refine ⟨hcomp.1, ?_⟩
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
hcomp : T.IsComplete
M N : T.ModelType
mp : L.completeTheory (↑M : Type (max u v)) = L.completeTheory (↑N : Type (max u v))
mp₁ : {φ : L.BoundedFormula Empty 0 | T ⊨ᵇ φ} = L.completeTheory (↑N : Type (max u v))
mp₂ mp₃ : Eq (α := L.Theory) {φ : L.BoundedFormula Empty 0 | T ⊨ᵇ φ} {φ : L.BoundedFormula Empty 0 | T ⊨ᵇ φ}
⊢ (↑M : Type (max u v)) ≅[L] (↑N : Type (max u v))

Tactic:
rw [ElementarilyEquivalent, ← hcomp.eq_complete_theory, ← hcomp.eq_complete_theory]

Premises used: FirstOrder.Language.ElementarilyEquivalent, FirstOrder.Language.Theory.IsComplete.eq_complete_theory
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
hsat : T.IsSatisfiable
h : ∀ (M N : T.ModelType), (↑M : Type (max u v)) ≅[L] (↑N : Type (max u v))
⊢ T.IsComplete

Tactic:
⟨hsat, ?_⟩

Premises used: FirstOrder.Language.Theory.IsComplete, And.intro
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
hsat : T.IsSatisfiable
h : ∀ (M N : T.ModelType), (↑M : Type (max u v)) ≅[L] (↑N : Type (max u v))
mpr : ∀ (φ : L.Sentence), T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ
⊢ T.IsComplete

Tactic:
refine ⟨hsat, ?_⟩
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
hsat : T.IsSatisfiable
h : ∀ (M N : T.ModelType), (↑M : Type (max u v)) ≅[L] (↑N : Type (max u v))
φ : L.Sentence
mpr : ∀ (M : T.ModelType), T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ
⊢ T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ

Tactic:
obtain ⟨M⟩ := hsat
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : ∀ (M N : T.ModelType), (↑M : Type (max u v)) ≅[L] (↑N : Type (max u v))
φ : L.Sentence
M : T.ModelType
pos : ∀ (hφ : (↑M : Type (max u v)) ⊨ φ), T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ
neg : ∀ (hφ : ¬(↑M : Type (max u v)) ⊨ φ), T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ
⊢ T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ

Tactic:
by_cases hφ : M ⊨ φ
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : ∀ (M N : T.ModelType), (↑M : Type (max u v)) ≅[L] (↑N : Type (max u v))
φ : L.Sentence
M : T.ModelType
hφ : (↑M : Type (max u v)) ⊨ φ
pos : T ⊨ᵇ φ
⊢ T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ

Tactic:
left
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : ∀ (M N : T.ModelType), (↑M : Type (max u v)) ≅[L] (↑N : Type (max u v))
φ : L.Sentence
M : T.ModelType
hφ : (↑M : Type (max u v)) ⊨ φ
⊢ T ⊨ᵇ φ

Tactic:
models_sentence_iff.2 fun N => (elementarilyEquivalent_iff.1 (h M N) φ).1 hφ

Premises used: Iff.mpr, FirstOrder.Language.elementarilyEquivalent_iff, FirstOrder.Language.Theory.models_sentence_iff, Iff.mp
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : ∀ (M N : T.ModelType), (↑M : Type (max u v)) ≅[L] (↑N : Type (max u v))
φ : L.Sentence
M : T.ModelType
hφ : (↑M : Type (max u v)) ⊨ φ
⊢ T ⊨ᵇ φ

Tactic:
exact models_sentence_iff.2 fun N => (elementarilyEquivalent_iff.1 (h M N) φ).1 hφ

Premises used: Iff.mpr, FirstOrder.Language.elementarilyEquivalent_iff, FirstOrder.Language.Theory.models_sentence_iff, Iff.mp
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : ∀ (M N : T.ModelType), (↑M : Type (max u v)) ≅[L] (↑N : Type (max u v))
φ : L.Sentence
M : T.ModelType
hφ : ¬(↑M : Type (max u v)) ⊨ φ
neg : T ⊨ᵇ Formula.not φ
⊢ T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ

Tactic:
right
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : ∀ (M N : T.ModelType), (↑M : Type (max u v)) ≅[L] (↑N : Type (max u v))
φ : L.Sentence
M : T.ModelType
hφ : ¬(↑M : Type (max u v)) ⊨ φ
⊢ T ⊨ᵇ Formula.not φ

Tactic:
models_sentence_iff.2 fun N => (Sentence.realize_not N).2
        (mt (elementarilyEquivalent_iff.1 (h M N) φ).2 hφ)

Premises used: Iff.mpr, FirstOrder.Language.elementarilyEquivalent_iff, FirstOrder.Language.Sentence.realize_not, mt, FirstOrder.Language.Theory.models_sentence_iff, FirstOrder.Language.Theory.ModelType.Carrier, Iff.mp
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : ∀ (M N : T.ModelType), (↑M : Type (max u v)) ≅[L] (↑N : Type (max u v))
φ : L.Sentence
M : T.ModelType
hφ : ¬(↑M : Type (max u v)) ⊨ φ
⊢ T ⊨ᵇ Formula.not φ

Tactic:
exact models_sentence_iff.2 fun N => (Sentence.realize_not N).2
        (mt (elementarilyEquivalent_iff.1 (h M N) φ).2 hφ)

Premises used: Iff.mpr, FirstOrder.Language.elementarilyEquivalent_iff, FirstOrder.Language.Sentence.realize_not, mt, FirstOrder.Language.Theory.models_sentence_iff, FirstOrder.Language.Theory.ModelType.Carrier, Iff.mp
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsComplete
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : M ⊨ T
inst_3 : N ⊨ T
inst_4 : Nonempty M
inst_5 : Nonempty N
rw : L.completeTheory M = L.completeTheory N
rw₁ : {φ : L.BoundedFormula Empty 0 | T ⊨ᵇ φ} = L.completeTheory N
rw₂ rw₃ : Eq (α := L.Theory) {φ : L.BoundedFormula Empty 0 | T ⊨ᵇ φ} {φ : L.BoundedFormula Empty 0 | T ⊨ᵇ φ}
⊢ M ≅[L] N

Tactic:
rw [ElementarilyEquivalent, ← h.eq_complete_theory, ← h.eq_complete_theory]

Premises used: FirstOrder.Language.ElementarilyEquivalent, FirstOrder.Language.Theory.IsComplete.eq_complete_theory
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsMaximal
⊢ T.IsComplete

Tactic:
h.imp_right (forall_imp fun _ => Or.imp models_sentence_of_mem models_sentence_of_mem)

Premises used: forall_imp, FirstOrder.Language.Theory.IsComplete, FirstOrder.Language.Theory.models_sentence_of_mem, And.imp_right, Or.imp
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsMaximal
φ : L.Sentence
⊢ φ ∈ T ∨ Formula.not φ ∈ T

Tactic:
h.2 φ

Premises used: And.right
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsMaximal
φ : L.Sentence
hφ : T ⊨ᵇ φ
⊢ φ ∈ T

Tactic:
(h.mem_or_not_mem φ).resolve_right fun con => ?_

Premises used: FirstOrder.Language.Theory.IsMaximal.mem_or_not_mem, Or.resolve_right
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsMaximal
φ : L.Sentence
hφ : T ⊨ᵇ φ
refine : ∀ (con : Formula.not φ ∈ T), False
⊢ φ ∈ T

Tactic:
refine (h.mem_or_not_mem φ).resolve_right fun con => ?_

Premises used: FirstOrder.Language.Theory.IsMaximal.mem_or_not_mem, Or.resolve_right
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsMaximal
φ : L.Sentence
hφ : T ⊨ᵇ φ
con : Formula.not φ ∈ T
⊢ ¬T.IsSatisfiable

Tactic:
rw [models_iff_not_satisfiable, Set.union_singleton, Set.insert_eq_of_mem con] at hφ

Premises used: Set.insert_eq_of_mem, Set.union_singleton, FirstOrder.Language.Theory.models_iff_not_satisfiable
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsMaximal
φ : L.Sentence
hφ : T ⊨ᵇ φ
con : Formula.not φ ∈ T
hφ₁ : ¬T.IsSatisfiable
⊢ Formula.not φ ∈ T

Tactic:
rw [models_iff_not_satisfiable, Set.union_singleton, Set.insert_eq_of_mem con] at hφ

Premises used: Set.insert_eq_of_mem, Set.union_singleton, FirstOrder.Language.Theory.models_iff_not_satisfiable
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsMaximal
φ : L.Sentence
hφ : ¬T.IsSatisfiable
con : Formula.not φ ∈ T
⊢ False

Tactic:
hφ h.1

Premises used: And.left
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsMaximal
φ : L.Sentence
hφ : ¬T.IsSatisfiable
con : Formula.not φ ∈ T
⊢ False

Tactic:
exact hφ h.1

Premises used: And.left
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsMaximal
φ : L.Sentence
⊢ φ ∈ T ↔ T ⊨ᵇ φ

Tactic:
⟨models_sentence_of_mem, h.mem_of_models⟩

Premises used: FirstOrder.Language.Theory.IsMaximal.mem_of_models, Iff.intro, FirstOrder.Language.Theory.models_sentence_of_mem
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
M : Type w
inst : L.Structure M
inst_1 : Nonempty M
⊢ (L.completeTheory M).IsSatisfiable

Tactic:
Theory.Model.isSatisfiable M

Premises used: FirstOrder.Language.Theory.Model.isSatisfiable
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
M : Type w
inst : L.Structure M
φ : L.Sentence
simp_rw :
  Membership.mem (γ := L.Theory) {φ : L.Sentence | M ⊨ φ} φ ∨
    Membership.mem (γ := L.Theory) {φ : L.Sentence | M ⊨ φ} (Formula.not φ)
simp_rw₁ : M ⊨ φ ∨ M ⊨ Formula.not φ
simp_rw₂ :
  Formula.Realize.{u, v, w, 0} (M := M) φ default ∨ Formula.Realize.{u, v, w, 0} (M := M) (Formula.not φ) default
simp_rw₃ : Formula.Realize.{u, v, w, 0} (M := M) φ default ∨ ¬Formula.Realize.{u, v, w, 0} (M := M) φ default
⊢ φ ∈ L.completeTheory M ∨ Formula.not φ ∈ L.completeTheory M

Tactic:
simp_rw [completeTheory, Set.mem_setOf_eq, Sentence.Realize, Formula.realize_not, or_not]

Premises used: FirstOrder.Language.Sentence.Realize, FirstOrder.Language.completeTheory, Set.mem_setOf_eq, or_not, FirstOrder.Language.Formula.realize_not
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
M : Type w
inst : L.Structure M
inst_1 : Nonempty M
⊢ (L.completeTheory M).IsMaximal

Tactic:
⟨isSatisfiable L M, mem_or_not_mem L M⟩

Premises used: FirstOrder.Language.Theory.IsMaximal, And.intro, FirstOrder.Language.completeTheory.mem_or_not_mem, FirstOrder.Language.completeTheory.isSatisfiable
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
M : Type w
inst : L.Structure M
inst_1 : Nonempty M
⊢ (L.completeTheory M).IsComplete

Tactic:
(completeTheory.isMaximal L M).isComplete

Premises used: FirstOrder.Language.completeTheory.isMaximal, FirstOrder.Language.Theory.IsMaximal.isComplete
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite (↑M : Type (max u v))
φ : L.Sentence
obtain : ∀ (w : Theory.ModelType.{u, v, w} T), #(↑w : Type w) = κ → T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ
⊢ T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ

Tactic:
obtain ⟨_, _⟩ := Theory.exists_model_card_eq ⟨hS.some, hT hS.some⟩ κ h1 h2

Premises used: Nonempty.some, Exists.intro, FirstOrder.Language.Theory.exists_model_card_eq
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite (↑M : Type (max u v))
φ : L.Sentence
w : Theory.ModelType.{u, v, w} T
h_1 : #(↑w : Type w) = κ
rw : (∀ (M : T.ModelType), (↑M : Type (max u v)) ⊨ φ) ∨ ∀ (M : T.ModelType), (↑M : Type (max u v)) ⊨ Formula.not φ
⊢ T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ

Tactic:
rw [Theory.models_sentence_iff, Theory.models_sentence_iff]

Premises used: FirstOrder.Language.Theory.models_sentence_iff
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite (↑M : Type (max u v))
φ : L.Sentence
w : Theory.ModelType.{u, v, w} T
h_1 : #(↑w : Type w) = κ
by_contra! :
  ∀ (MF : T.ModelType) (hMF : ¬(↑MF : Type (max u v)) ⊨ φ) (MT : T.ModelType)
    (hMT : ¬(↑MT : Type (max u v)) ⊨ Formula.not φ), False
⊢ (∀ (M : T.ModelType), (↑M : Type (max u v)) ⊨ φ) ∨ ∀ (M : T.ModelType), (↑M : Type (max u v)) ⊨ Formula.not φ

Tactic:
by_contra! ⟨⟨MF, hMF⟩, MT, hMT⟩
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite (↑M : Type (max u v))
φ : L.Sentence
w : Theory.ModelType.{u, v, w} T
h_1 : #(↑w : Type w) = κ
MF : T.ModelType
hMF : ¬(↑MF : Type (max u v)) ⊨ φ
MT : T.ModelType
hMT : ¬(↑MT : Type (max u v)) ⊨ Formula.not φ
⊢ (↑MT : Type (max u v)) ⊨ φ

Tactic:
rw [Sentence.realize_not, Classical.not_not] at hMT

Premises used: Classical.not_not, FirstOrder.Language.Sentence.realize_not
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite (↑M : Type (max u v))
φ : L.Sentence
w : Theory.ModelType.{u, v, w} T
h_1 : #(↑w : Type w) = κ
MF : T.ModelType
hMF : ¬(↑MF : Type (max u v)) ⊨ φ
MT : T.ModelType
hMT : (↑MT : Type (max u v)) ⊨ φ
⊢ False

Tactic:
hMF ?_
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite (↑M : Type (max u v))
φ : L.Sentence
w : Theory.ModelType.{u, v, w} T
h_1 : #(↑w : Type w) = κ
MF : T.ModelType
hMF : ¬(↑MF : Type (max u v)) ⊨ φ
MT : T.ModelType
hMT : (↑MT : Type (max u v)) ⊨ φ
refine : (↑MF : Type (max u v)) ⊨ φ
⊢ False

Tactic:
refine hMF ?_
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite (↑M : Type (max u v))
φ : L.Sentence
w : Theory.ModelType.{u, v, w} T
h_1 : #(↑w : Type w) = κ
MF : T.ModelType
hMF : ¬(↑MF : Type (max u v)) ⊨ φ
MT : T.ModelType
hMT : (↑MT : Type (max u v)) ⊨ φ
⊢ Infinite (↑MT : Type (max u v))

Tactic:
haveI := hT MT
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite (↑M : Type (max u v))
φ : L.Sentence
w : Theory.ModelType.{u, v, w} T
h_1 : #(↑w : Type w) = κ
MF : T.ModelType
hMF : ¬(↑MF : Type (max u v)) ⊨ φ
MT : T.ModelType
hMT : (↑MT : Type (max u v)) ⊨ φ
this : Infinite (↑MT : Type (max u v))
⊢ Infinite (↑MF : Type (max u v))

Tactic:
haveI := hT MF
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite (↑M : Type (max u v))
φ : L.Sentence
w : Theory.ModelType.{u, v, w} T
h_1 : #(↑w : Type w) = κ
MF : T.ModelType
hMF : ¬(↑MF : Type (max u v)) ⊨ φ
MT : T.ModelType
hMT : (↑MT : Type (max u v)) ⊨ φ
this_1 : Infinite (↑MT : Type (max u v))
this : Infinite (↑MF : Type (max u v))
obtain :
  ∀ (NT : Bundled L.Structure) (MNT : (↑MT : Type (max u v)) ≅[L] (↑NT : Type w)) (hNT : #(↑NT : Type w) = κ),
    (↑MF : Type (max u v)) ⊨ φ
⊢ (↑MF : Type (max u v)) ⊨ φ

Tactic:
obtain ⟨NT, MNT, hNT⟩ := exists_elementarilyEquivalent_card_eq L MT κ h1 h2

Premises used: FirstOrder.Language.exists_elementarilyEquivalent_card_eq, FirstOrder.Language.Theory.ModelType.Carrier
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite (↑M : Type (max u v))
φ : L.Sentence
w : Theory.ModelType.{u, v, w} T
h_1 : #(↑w : Type w) = κ
MF : T.ModelType
hMF : ¬(↑MF : Type (max u v)) ⊨ φ
MT : T.ModelType
hMT : (↑MT : Type (max u v)) ⊨ φ
this_1 : Infinite (↑MT : Type (max u v))
this : Infinite (↑MF : Type (max u v))
NT : Bundled L.Structure
MNT : (↑MT : Type (max u v)) ≅[L] (↑NT : Type w)
hNT : #(↑NT : Type w) = κ
obtain :
  ∀ (NF : Bundled L.Structure) (MNF : (↑MF : Type (max u v)) ≅[L] (↑NF : Type w)) (hNF : #(↑NF : Type w) = κ),
    (↑MF : Type (max u v)) ⊨ φ
⊢ (↑MF : Type (max u v)) ⊨ φ

Tactic:
obtain ⟨NF, MNF, hNF⟩ := exists_elementarilyEquivalent_card_eq L MF κ h1 h2

Premises used: FirstOrder.Language.exists_elementarilyEquivalent_card_eq, FirstOrder.Language.Theory.ModelType.Carrier
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite (↑M : Type (max u v))
φ : L.Sentence
w : Theory.ModelType.{u, v, w} T
h_1 : #(↑w : Type w) = κ
MF : T.ModelType
hMF : ¬(↑MF : Type (max u v)) ⊨ φ
MT : T.ModelType
hMT : (↑MT : Type (max u v)) ⊨ φ
this_1 : Infinite (↑MT : Type (max u v))
this : Infinite (↑MF : Type (max u v))
NT : Bundled L.Structure
MNT : (↑MT : Type (max u v)) ≅[L] (↑NT : Type w)
hNT : #(↑NT : Type w) = κ
NF : Bundled L.Structure
MNF : (↑MF : Type (max u v)) ≅[L] (↑NF : Type w)
hNF : #(↑NF : Type w) = κ
obtain :
  ∀ (TF : (↑(ElementarilyEquivalent.toModel T MNT) : Type w) ≃[L] (↑(ElementarilyEquivalent.toModel T MNF) : Type w)),
    (↑MF : Type (max u v)) ⊨ φ
⊢ (↑MF : Type (max u v)) ⊨ φ

Tactic:
obtain ⟨TF⟩ := h (MNT.toModel T) (MNF.toModel T) hNT hNF

Premises used: FirstOrder.Language.ElementarilyEquivalent.toModel
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite (↑M : Type (max u v))
φ : L.Sentence
w : Theory.ModelType.{u, v, w} T
h_1 : #(↑w : Type w) = κ
MF : T.ModelType
hMF : ¬(↑MF : Type (max u v)) ⊨ φ
MT : T.ModelType
hMT : (↑MT : Type (max u v)) ⊨ φ
this_1 : Infinite (↑MT : Type (max u v))
this : Infinite (↑MF : Type (max u v))
NT : Bundled L.Structure
MNT : (↑MT : Type (max u v)) ≅[L] (↑NT : Type w)
hNT : #(↑NT : Type w) = κ
NF : Bundled L.Structure
MNF : (↑MF : Type (max u v)) ≅[L] (↑NF : Type w)
hNF : #(↑NF : Type w) = κ
TF : (↑(ElementarilyEquivalent.toModel T MNT) : Type w) ≃[L] (↑(ElementarilyEquivalent.toModel T MNF) : Type w)
⊢ (↑MF : Type (max u v)) ⊨ φ

Tactic:
((MNT.realize_sentence φ).trans
        ((StrongHomClass.realize_sentence TF φ).trans (MNF.realize_sentence φ).symm)).1 hMT

Premises used: FirstOrder.Language.StrongHomClass.realize_sentence, Iff.mp, Iff.trans, Iff.symm, FirstOrder.Language.ElementarilyEquivalent.realize_sentence
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite (↑M : Type (max u v))
φ : L.Sentence
w : Theory.ModelType.{u, v, w} T
h_1 : #(↑w : Type w) = κ
MF : T.ModelType
hMF : ¬(↑MF : Type (max u v)) ⊨ φ
MT : T.ModelType
hMT : (↑MT : Type (max u v)) ⊨ φ
this_1 : Infinite (↑MT : Type (max u v))
this : Infinite (↑MF : Type (max u v))
NT : Bundled L.Structure
MNT : (↑MT : Type (max u v)) ≅[L] (↑NT : Type w)
hNT : #(↑NT : Type w) = κ
NF : Bundled L.Structure
MNF : (↑MF : Type (max u v)) ≅[L] (↑NF : Type w)
hNF : #(↑NF : Type w) = κ
TF : (↑(ElementarilyEquivalent.toModel T MNT) : Type w) ≃[L] (↑(ElementarilyEquivalent.toModel T MNF) : Type w)
⊢ (↑MF : Type (max u v)) ⊨ φ

Tactic:
exact
      ((MNT.realize_sentence φ).trans
        ((StrongHomClass.realize_sentence TF φ).trans (MNF.realize_sentence φ).symm)).1 hMT

Premises used: FirstOrder.Language.StrongHomClass.realize_sentence, Iff.mp, Iff.trans, Iff.symm, FirstOrder.Language.ElementarilyEquivalent.realize_sentence
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
κ : Cardinal.{w}
T : Language.empty.Theory
M N : T.ModelType
hM : #(↑M : Type w) = κ
hN : #(↑N : Type w) = κ
rw : lift.{w, w} #(↑M : Type w) = lift.{w, w} #(↑N : Type w)
rw₁ : lift.{w, w} κ = lift.{w, w} #(↑N : Type w)
rw₂ rw₃ : lift.{w, w} κ = lift.{w, w} κ
⊢ Nonempty.{w + 1} ((↑M : Type w) ≃[Language.empty] (↑N : Type w))

Tactic:
rw [empty.nonempty_equiv_iff, hM, hN]

Premises used: FirstOrder.Language.empty.nonempty_equiv_iff
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
⊢ lift.{0, 0} Language.empty.card ≤ lift.{0, 0} ℵ₀

Tactic:
simp