awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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) φ)
have 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) φ)
Tactic: refine ⟨fun h => models_sentence_iff.2 (fun M => ?_),
    fun h => models_formula_iff.2 (fun M v => ?_)⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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) φ)
⊢ T ⊨ᵇ φ ↔
    ((L.lhomWithConstants α).onTheory T).ModelsBoundedFormula (α := Empty) (n := 0)
      ((Formula.equivSentence : (a : L.Formula α) → L[[α]].Sentence) φ)
have 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
Tactic: refine ⟨fun h => models_sentence_iff.2 (fun M => ?_),
    fun h => models_formula_iff.2 (fun M v => ?_)⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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))
⊢ Sentence.Realize (L := L[[α]]) (↑M : Type (max (max u w) v))
    ((Formula.equivSentence : (a : L.Formula α) → L[[α]].Sentence) φ)
have refine_1 : φ.Realize (M := (↑M : Type (max (max u w) v))) fun (a : α) ↦ (↑(L.con a) : (↑M : Type (max (max u w) v)))
Tactic: rw [Formula.realize_equivSentence]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (hypothesis)
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))
⊢ φ.Realize (M := (↑M : Type (max (max u w) v))) fun (a : α) ↦ (↑(L.con a) : (↑M : Type (max (max u w) v)))
have this₁ : (↑M : Type (max (max u v) w)) ⊨ T
Tactic: have : M ⊨ T := (LHom.onTheory_model _ _).1 M.is_model
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (hypothesis)
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
⊢ φ.Realize v
have this₁ : (↑M : Type (max (max u v) w)) ⊨ (L.lhomWithConstants α).onTheory T
Tactic: have : M ⊨ (L.lhomWithConstants α).onTheory T := (LHom.onTheory_model _ _).2 inferInstance
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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
⊢ φ.Realize v
have 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
Tactic: rw [models_formula_iff_onTheory_models_equivSentence] at h
Cleared hypotheses: h, M, inst, inst_1, inst_2, v
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (hypothesis)
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
⊢ φ.Realize v
have this₁ : M ⊨ (L.lhomWithConstants α).onTheory T
Tactic: have : M ⊨ (L.lhomWithConstants α).onTheory T := (LHom.onTheory_model _ _).2 inferInstance
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
⊢ T ⊨ᵇ φ.toFormula ↔ T ⊨ᵇ φ
have 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
Tactic: refine ⟨fun h M v xs => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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
⊢ T ⊨ᵇ φ.toFormula ↔ T ⊨ᵇ φ
have refine_2 : T ⊨ᵇ φ → T ⊨ᵇ φ.toFormula
Tactic: refine ⟨fun h M v xs => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (hypothesis)
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))
⊢ φ.Realize v xs
have h' : φ.toFormula.Realize (Sum.elim v xs)
Tactic: have h' : φ.toFormula.Realize (Sum.elim v xs) := h.realize_formula M
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
⊢ T ⊨ᵇ φ → T ⊨ᵇ φ.toFormula
have refine_2 : T ⊨ᵇ φ → ∀ (M : T.ModelType) (v : α ⊕ Fin n → (↑M : Type (max (max u v) w))), φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
Tactic: simp only [models_formula_iff, BoundedFormula.realize_toFormula]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (hypothesis)
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
⊢ φ.Realize v xs
have h' : φ.toFormula.Realize (Sum.elim v xs)
Tactic: have h' : φ.toFormula.Realize (Sum.elim v xs) := (models_toFormula_iff.2 h).realize_formula M
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (hypothesis)
Goal:
L : Language
T : L.Theory
α : Type w
T' : L.Theory
h : ∀ φ ∈ T', T ⊨ᵇ φ
φ : L.Formula α
hφ : T' ⊨ᵇ φ
M : T.ModelType
⊢ ∀ (v : α → (↑M : Type (max (max u v) w))) (xs : Fin 0 → (↑M : Type (max (max u v) w))), BoundedFormula.Realize φ v xs
have hM : (↑M : Type (max (max u v) w)) ⊨ T'
Tactic: have hM : M ⊨ T' := T'.model_iff.2 (fun ψ hψ => (h ψ hψ).realize_sentence M)
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
φ : L.Sentence
⊢ T ⊨ᵇ φ ↔ ∃ (T0 : Finset L.Sentence), (↑T0 : Set L.Sentence) ⊆ T ∧ (↑T0 : Set L.Sentence) ⊨ᵇ φ
have simp : ¬(T ∪ {Formula.not φ}).IsSatisfiable ↔
  ∃ (T0 : Finset L.Sentence), (↑T0 : Set L.Sentence) ⊆ T ∧ ¬((↑T0 : Set L.Sentence) ∪ {Formula.not φ}).IsSatisfiable
Tactic: simp only [models_iff_not_satisfiable]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
φ : L.Sentence
⊢ ¬(T ∪ {Formula.not φ}).IsSatisfiable ↔
    ∃ (T0 : Finset L.Sentence), (↑T0 : Set L.Sentence) ⊆ T ∧ ¬((↑T0 : Set L.Sentence) ∪ {Formula.not φ}).IsSatisfiable
have 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
Tactic: rw [isSatisfiable_iff_isFinitelySatisfiable, IsFinitelySatisfiable]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
φ : 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
have 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
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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
⊢ (∀ (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
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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 ∪ {Formula.not φ}) : Set L.Sentence) ⊆ T ∪ {Formula.not φ}
have simp : (↑T0 : Set L.Sentence) ∪ {Formula.not φ} ⊆ T ∪ {Formula.not φ}
Tactic: simp only [Finset.coe_union, Finset.coe_singleton]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ
have inl : ∀ (hφ : T ⊨ᵇ φ), T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ
Tactic: rcases h.2 φ with hφ | hφn
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
inl : ∀ (hφ : T ⊨ᵇ φ), T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ
have inr : ∀ (hφn : T ⊨ᵇ Formula.not φ), T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ
Tactic: rcases h.2 φ with hφ | hφn
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφ : T ⊨ᵇ φ
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ
have inl : ¬T ⊨ᵇ Formula.not φ
Tactic: simp only [hφ, not_true, iff_false]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφ : T ⊨ᵇ φ
⊢ ¬T ⊨ᵇ Formula.not φ
have inl : ∃ (x : T.ModelType), ¬(↑x : Type (max u v)) ⊨ Formula.not φ
Tactic: rw [models_sentence_iff, not_forall]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφ : T ⊨ᵇ φ
⊢ ∃ (x : T.ModelType), ¬(↑x : Type (max u v)) ⊨ Formula.not φ
have inl : ¬(↑(Nonempty.some sorry) : Type (max u v)) ⊨ Formula.not φ
Tactic: refine ⟨h.1.some, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφ : T ⊨ᵇ φ
⊢ ¬(↑(Nonempty.some ⋯) : Type (max u v)) ⊨ Formula.not φ
have inl : (↑(Nonempty.some sorry) : Type (max u v)) ⊨ φ
Tactic: simp only [Sentence.realize_not, Classical.not_not]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφn : T ⊨ᵇ Formula.not φ
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ
have inr : ¬T ⊨ᵇ φ
Tactic: simp only [hφn, true_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (hypothesis)
Goal:
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφn : T ⊨ᵇ Formula.not φ
hφ : T ⊨ᵇ φ
⊢ False
have hφn₁ : ∀ (M : T.ModelType), (↑M : Type (max u v)) ⊨ Formula.not φ
Tactic: rw [models_sentence_iff] at *
Cleared hypotheses: hφn, hφ
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (hypothesis)
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 φ
⊢ False
have hφ₁ : ∀ (M : T.ModelType), (↑M : Type (max u v)) ⊨ φ
Tactic: rw [models_sentence_iff] at *
Cleared hypotheses: hφn, hφ
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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
⊢ M ⊨ φ ↔ T ⊨ᵇ φ
have inl : ∀ (hφ : T ⊨ᵇ φ), M ⊨ φ ↔ T ⊨ᵇ φ
Tactic: rcases h.2 φ with hφ | hφn
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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 ⊨ᵇ φ
⊢ M ⊨ φ ↔ T ⊨ᵇ φ
have inr : ∀ (hφn : T ⊨ᵇ Formula.not φ), M ⊨ φ ↔ T ⊨ᵇ φ
Tactic: rcases h.2 φ with hφ | hφn
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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 ⊨ᵇ φ} = L.completeTheory M
have h₁ : ∀ (φ : L.BoundedFormula Empty 0),
  Membership.mem (γ := Set (L.BoundedFormula Empty 0)) {φ : L.BoundedFormula Empty 0 | T ⊨ᵇ φ} φ ↔
    φ ∈ L.completeTheory M
Tactic: ext φ
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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
⊢ Membership.mem (γ := Set (L.BoundedFormula Empty 0)) {φ : L.BoundedFormula Empty 0 | T ⊨ᵇ φ} φ ↔
    φ ∈ L.completeTheory M
have h₁ : T ⊨ᵇ φ ↔ M ⊨ φ
Tactic: simp only [Set.mem_setOf_eq, L.mem_completeTheory]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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 ⊨ φ
have h₁ : ∀ (h_realize : M ⊨ φ), T ⊨ᵇ φ
Tactic: refine ⟨fun h_models => h_models.realize_sentence M, fun h_realize => ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (hypothesis)
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 φ
⊢ T ⊨ᵇ φ
have this : M ⊨ ∼φ
Tactic: have : M ⊨ φ.not := hT.realize_sentence M
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (hypothesis)
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 ⊨ᵇ φ
have this₁ : ¬M ⊨ φ
Tactic: rw [Sentence.realize_not] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (hypothesis)
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 ⊨ᵇ φ
have x : 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
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
⊢ T.IsComplete ↔ T.IsSatisfiable ∧ ∀ (M N : T.ModelType), (↑M : Type (max u v)) ≅[L] (↑N : Type (max u v))
have mp : T.IsComplete → T.IsSatisfiable ∧ ∀ (M N : T.ModelType), (↑M : Type (max u v)) ≅[L] (↑N : Type (max u v))
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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))
⊢ T.IsComplete ↔ T.IsSatisfiable ∧ ∀ (M N : T.ModelType), (↑M : Type (max u v)) ≅[L] (↑N : Type (max u v))
have mpr : (T.IsSatisfiable ∧ ∀ (M N : T.ModelType), (↑M : Type (max u v)) ≅[L] (↑N : Type (max u v))) → T.IsComplete
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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))
have mp : ∀ (M N : T.ModelType), (↑M : Type (max u v)) ≅[L] (↑N : Type (max u v))
Tactic: refine ⟨hcomp.1, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
hcomp : T.IsComplete
M N : T.ModelType
⊢ (↑M : Type (max u v)) ≅[L] (↑N : Type (max u v))
have mp : L.completeTheory (↑M : Type (max u v)) = L.completeTheory (↑N : Type (max u v))
Tactic: rw [ElementarilyEquivalent, ← hcomp.eq_complete_theory, ← hcomp.eq_complete_theory]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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))
⊢ (↑M : Type (max u v)) ≅[L] (↑N : Type (max u v))
have mp₁ : {φ : L.BoundedFormula Empty 0 | T ⊨ᵇ φ} = L.completeTheory (↑N : Type (max u v))
Tactic: rw [ElementarilyEquivalent, ← hcomp.eq_complete_theory, ← hcomp.eq_complete_theory]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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))
⊢ (↑M : Type (max u v)) ≅[L] (↑N : Type (max u v))
have mp₂ : Eq (α := L.Theory) {φ : L.BoundedFormula Empty 0 | T ⊨ᵇ φ} {φ : L.BoundedFormula Empty 0 | T ⊨ᵇ φ}
Tactic: rw [ElementarilyEquivalent, ← hcomp.eq_complete_theory, ← hcomp.eq_complete_theory]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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
have mpr : ∀ (φ : L.Sentence), T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ
Tactic: refine ⟨hsat, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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
⊢ T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ
have mpr : ∀ (M : T.ModelType), T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ
Tactic: obtain ⟨M⟩ := hsat
Cleared hypotheses: hsat
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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
⊢ T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ
have pos : ∀ (hφ : (↑M : Type (max u v)) ⊨ φ), T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ
Tactic: by_cases hφ : M ⊨ φ
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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 φ
⊢ T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ
have neg : ∀ (hφ : ¬(↑M : Type (max u v)) ⊨ φ), T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ
Tactic: by_cases hφ : M ⊨ φ
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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 ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ
have pos : T ⊨ᵇ φ
Tactic: left
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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 ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ
have neg : T ⊨ᵇ Formula.not φ
Tactic: right
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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
⊢ M ≅[L] N
have rw : L.completeTheory M = L.completeTheory N
Tactic: rw [ElementarilyEquivalent, ← h.eq_complete_theory, ← h.eq_complete_theory]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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
⊢ M ≅[L] N
have rw₁ : {φ : L.BoundedFormula Empty 0 | T ⊨ᵇ φ} = L.completeTheory N
Tactic: rw [ElementarilyEquivalent, ← h.eq_complete_theory, ← h.eq_complete_theory]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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
⊢ M ≅[L] N
have rw₂ : Eq (α := L.Theory) {φ : L.BoundedFormula Empty 0 | T ⊨ᵇ φ} {φ : L.BoundedFormula Empty 0 | T ⊨ᵇ φ}
Tactic: rw [ElementarilyEquivalent, ← h.eq_complete_theory, ← h.eq_complete_theory]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
h : T.IsMaximal
φ : L.Sentence
hφ : T ⊨ᵇ φ
⊢ φ ∈ T
have refine : ∀ (con : Formula.not φ ∈ T), False
Tactic: refine (h.mem_or_not_mem φ).resolve_right fun con => ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (hypothesis)
Goal:
L : Language
T : L.Theory
h : T.IsMaximal
φ : L.Sentence
hφ : T ⊨ᵇ φ
con : Formula.not φ ∈ T
⊢ False
have hφ₁ : ¬T.IsSatisfiable
Tactic: rw [models_iff_not_satisfiable, Set.union_singleton, Set.insert_eq_of_mem con] at hφ
Cleared hypotheses: hφ, con
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
φ : L.Sentence
⊢ φ ∈ L.completeTheory M ∨ Formula.not φ ∈ L.completeTheory M
have simp_rw : Membership.mem (γ := L.Theory) {φ : L.Sentence | M ⊨ φ} φ ∨
  Membership.mem (γ := L.Theory) {φ : L.Sentence | M ⊨ φ} (Formula.not φ)
Tactic: simp_rw [completeTheory, Set.mem_setOf_eq, Sentence.Realize, Formula.realize_not, or_not]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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 φ)
⊢ φ ∈ L.completeTheory M ∨ Formula.not φ ∈ L.completeTheory M
have simp_rw₁ : M ⊨ φ ∨ M ⊨ Formula.not φ
Tactic: simp_rw [completeTheory, Set.mem_setOf_eq, Sentence.Realize, Formula.realize_not, or_not]