Theorem: LO.FirstOrder.complete (Logic/FirstOrder/Completeness/Completeness.lean)

State before:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
⊢ T ⊢! σ
Tactic:
letI := Classical.typeDecidableEq
State after:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this : (α : Sort ?u.10884) → DecidableEq α := Classical.typeDecidableEq
⊢ T ⊢! σ

State before:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this : (α : Sort ?u.10884) → DecidableEq α := Classical.typeDecidableEq
⊢ T ⊢! σ
Tactic:
have : ∃ u : Finset (Sentence L), ↑u ⊆ insert (~σ) T ∧ ¬Satisfiable (u : Theory L) := by
  simpa using (compact (T := insert (~σ) T)).not.mp (Semantics.consequence_iff_not_satisfiable.mp h)
State after:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝ : (α : Sort ?u.10884) → DecidableEq α := Classical.typeDecidableEq
this : ∃ u, ↑u ⊆ insert (~σ) T ∧ ¬Satisfiable ↑u
⊢ T ⊢! σ

State before:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝ : (α : Sort ?u.10884) → DecidableEq α := Classical.typeDecidableEq
this : ∃ u, ↑u ⊆ insert (~σ) T ∧ ¬Satisfiable ↑u
⊢ T ⊢! σ
Tactic:
choose u hu using this
State after:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this : (α : Sort ?u.10884) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
hu : ↑u ⊆ insert (~σ) T ∧ ¬Satisfiable ↑u
⊢ T ⊢! σ

State before:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this : (α : Sort ?u.10884) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
hu : ↑u ⊆ insert (~σ) T ∧ ¬Satisfiable ↑u
⊢ T ⊢! σ
Tactic:
rcases hu with ⟨ssu, hu⟩
State after:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this : (α : Sort ?u.10884) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
⊢ T ⊢! σ

State before:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this : (α : Sort ?u.10884) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
⊢ T ⊢! σ
Tactic:
haveI : ∀ k, Encodable ((languageFinset u).Func k) := fun _ ↦ Fintype.toEncodable _
State after:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this : (k : ℕ) → Encodable ((languageFinset u).Func k)
⊢ T ⊢! σ

State before:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this : (k : ℕ) → Encodable ((languageFinset u).Func k)
⊢ T ⊢! σ
Tactic:
haveI : ∀ k, Encodable ((languageFinset u).Rel k) := fun _ ↦ Fintype.toEncodable _
State after:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
⊢ T ⊢! σ

State before:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
⊢ T ⊢! σ
Tactic:
let u' : Finset (Sentence (languageFinset u)) := Finset.imageOfFinset u (fun _ hσ ↦ toSubLanguageFinsetSelf hσ)
State after:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
⊢ T ⊢! σ

State before:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
⊢ T ⊢! σ
Tactic:
have image_u' : u'.image (Semiformula.lMap L.ofSubLanguage) = u := by
  ext τ; simp [u', Finset.mem_imageOfFinset_iff]
  exact ⟨by rintro ⟨a, ⟨τ, hτ, rfl⟩, rfl⟩; simp[hτ],
    by intro hτ; exact ⟨toSubLanguageFinsetSelf hτ, ⟨τ, hτ, rfl⟩, Semiformula.lMap_toSubLanguageFinsetSelf hτ⟩⟩
State after:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
⊢ T ⊢! σ

State before:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
⊢ T ⊢! σ
Tactic:
have : ¬Satisfiable (u' : Theory (languageFinset u)) := by
  intro h
  have : Satisfiable (u : Theory L) := by
    rw[←image_u']
    simpa using (satisfiable_lMap L.ofSubLanguage (fun k ↦ Subtype.val_injective) (fun _ ↦ Subtype.val_injective) h)
  contradiction
State after:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝² : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝¹ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this✝ : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
this : ¬Satisfiable ↑u'
⊢ T ⊢! σ

State before:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝² : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝¹ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this✝ : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
this : ¬Satisfiable ↑u'
⊢ T ⊢! σ
Tactic:
have : System.Inconsistent (u' : Theory (languageFinset u)) := Complete.inconsistent_of_unsatisfiable this
State after:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝³ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝² : (k : ℕ) → Encodable ((languageFinset u).Func k)
this✝¹ : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
this✝ : ¬Satisfiable ↑u'
this : System.Inconsistent ↑u'
⊢ T ⊢! σ

State before:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝³ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝² : (k : ℕ) → Encodable ((languageFinset u).Func k)
this✝¹ : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
this✝ : ¬Satisfiable ↑u'
this : System.Inconsistent ↑u'
⊢ T ⊢! σ
Tactic:
have : System.Inconsistent (u : Theory L) := by rw[←image_u']; simpa using System.inconsistent_lMap L.ofSubLanguage this
State after:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝⁴ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝³ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this✝² : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
this✝¹ : ¬Satisfiable ↑u'
this✝ : System.Inconsistent ↑u'
this : System.Inconsistent ↑u
⊢ T ⊢! σ

State before:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝⁴ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝³ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this✝² : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
this✝¹ : ¬Satisfiable ↑u'
this✝ : System.Inconsistent ↑u'
this : System.Inconsistent ↑u
⊢ T ⊢! σ
Tactic:
have : System.Inconsistent (insert (~σ) T) := this.of_supset ssu
State after:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝⁵ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝⁴ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this✝³ : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
this✝² : ¬Satisfiable ↑u'
this✝¹ : System.Inconsistent ↑u'
this✝ : System.Inconsistent ↑u
this : System.Inconsistent (insert (~σ) T)
⊢ T ⊢! σ

State before:
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝⁵ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝⁴ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this✝³ : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
this✝² : ¬Satisfiable ↑u'
this✝¹ : System.Inconsistent ↑u'
this✝ : System.Inconsistent ↑u
this : System.Inconsistent (insert (~σ) T)
⊢ T ⊢! σ
Tactic:
exact Gentzen.provable_iff_inconsistent.mpr this
State after:
no goals

State before:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this : (α : Sort ?u.10884) → DecidableEq α := Classical.typeDecidableEq
⊢ ∃ u, ↑u ⊆ insert (~σ) T ∧ ¬Satisfiable ↑u
Tactic:
simpa using (compact (T := insert (~σ) T)).not.mp (Semantics.consequence_iff_not_satisfiable.mp h)
State after:
no goals

State before:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
⊢ Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
Tactic:
ext τ
State after:
case a
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
τ : Semiformula L Empty 0
⊢ τ ∈ Finset.image (⇑(lMap L.ofSubLanguage)) u' ↔ τ ∈ u

State before:
case a
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
τ : Semiformula L Empty 0
⊢ τ ∈ Finset.image (⇑(lMap L.ofSubLanguage)) u' ↔ τ ∈ u
Tactic:
simp [u', Finset.mem_imageOfFinset_iff]
State after:
case a
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
τ : Semiformula L Empty 0
⊢ (∃ a, (∃ a_1, ∃ (ha : a_1 ∈ u), toSubLanguageFinsetSelf ha = a) ∧ (lMap L.ofSubLanguage) a = τ) ↔ τ ∈ u

State before:
case a
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
τ : Semiformula L Empty 0
⊢ (∃ a, (∃ a_1, ∃ (ha : a_1 ∈ u), toSubLanguageFinsetSelf ha = a) ∧ (lMap L.ofSubLanguage) a = τ) ↔ τ ∈ u
Tactic:
exact ⟨by rintro ⟨a, ⟨τ, hτ, rfl⟩, rfl⟩; simp[hτ],
  by intro hτ; exact ⟨toSubLanguageFinsetSelf hτ, ⟨τ, hτ, rfl⟩, Semiformula.lMap_toSubLanguageFinsetSelf hτ⟩⟩
State after:
no goals

State before:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
τ : Semiformula L Empty 0
⊢ (∃ a, (∃ a_1, ∃ (ha : a_1 ∈ u), toSubLanguageFinsetSelf ha = a) ∧ (lMap L.ofSubLanguage) a = τ) → τ ∈ u
Tactic:
rintro ⟨a, ⟨τ, hτ, rfl⟩, rfl⟩
State after:
case intro.intro.intro.intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
τ : Sentence L
hτ : τ ∈ u
⊢ (lMap L.ofSubLanguage) (toSubLanguageFinsetSelf hτ) ∈ u

State before:
case intro.intro.intro.intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
τ : Sentence L
hτ : τ ∈ u
⊢ (lMap L.ofSubLanguage) (toSubLanguageFinsetSelf hτ) ∈ u
Tactic:
simp[hτ]
State after:
no goals

State before:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
τ : Semiformula L Empty 0
⊢ τ ∈ u → ∃ a, (∃ a_1, ∃ (ha : a_1 ∈ u), toSubLanguageFinsetSelf ha = a) ∧ (lMap L.ofSubLanguage) a = τ
Tactic:
intro hτ
State after:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
τ : Semiformula L Empty 0
hτ : τ ∈ u
⊢ ∃ a, (∃ a_1, ∃ (ha : a_1 ∈ u), toSubLanguageFinsetSelf ha = a) ∧ (lMap L.ofSubLanguage) a = τ

State before:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
τ : Semiformula L Empty 0
hτ : τ ∈ u
⊢ ∃ a, (∃ a_1, ∃ (ha : a_1 ∈ u), toSubLanguageFinsetSelf ha = a) ∧ (lMap L.ofSubLanguage) a = τ
Tactic:
exact ⟨toSubLanguageFinsetSelf hτ, ⟨τ, hτ, rfl⟩, Semiformula.lMap_toSubLanguageFinsetSelf hτ⟩
State after:
no goals

State before:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
⊢ ¬Satisfiable ↑u'
Tactic:
intro h
State after:
L : Language
T : Theory L
σ : Sentence L
h✝ : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
h : Satisfiable ↑u'
⊢ False

State before:
L : Language
T : Theory L
σ : Sentence L
h✝ : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
h : Satisfiable ↑u'
⊢ False
Tactic:
have : Satisfiable (u : Theory L) := by
  rw[←image_u']
  simpa using (satisfiable_lMap L.ofSubLanguage (fun k ↦ Subtype.val_injective) (fun _ ↦ Subtype.val_injective) h)
State after:
L : Language
T : Theory L
σ : Sentence L
h✝ : T ⊨ σ
this✝² : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝¹ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this✝ : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
h : Satisfiable ↑u'
this : Satisfiable ↑u
⊢ False

State before:
L : Language
T : Theory L
σ : Sentence L
h✝ : T ⊨ σ
this✝² : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝¹ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this✝ : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
h : Satisfiable ↑u'
this : Satisfiable ↑u
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
L : Language
T : Theory L
σ : Sentence L
h✝ : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
h : Satisfiable ↑u'
⊢ Satisfiable ↑u
Tactic:
rw[←image_u']
State after:
L : Language
T : Theory L
σ : Sentence L
h✝ : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
h : Satisfiable ↑u'
⊢ Satisfiable ↑(Finset.image (⇑(lMap L.ofSubLanguage)) u')

State before:
L : Language
T : Theory L
σ : Sentence L
h✝ : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
h : Satisfiable ↑u'
⊢ Satisfiable ↑(Finset.image (⇑(lMap L.ofSubLanguage)) u')
Tactic:
simpa using (satisfiable_lMap L.ofSubLanguage (fun k ↦ Subtype.val_injective) (fun _ ↦ Subtype.val_injective) h)
State after:
no goals

State before:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝³ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝² : (k : ℕ) → Encodable ((languageFinset u).Func k)
this✝¹ : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
this✝ : ¬Satisfiable ↑u'
this : System.Inconsistent ↑u'
⊢ System.Inconsistent ↑u
Tactic:
rw[←image_u']
State after:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝³ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝² : (k : ℕ) → Encodable ((languageFinset u).Func k)
this✝¹ : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
this✝ : ¬Satisfiable ↑u'
this : System.Inconsistent ↑u'
⊢ System.Inconsistent ↑(Finset.image (⇑(lMap L.ofSubLanguage)) u')

State before:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝³ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝² : (k : ℕ) → Encodable ((languageFinset u).Func k)
this✝¹ : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
this✝ : ¬Satisfiable ↑u'
this : System.Inconsistent ↑u'
⊢ System.Inconsistent ↑(Finset.image (⇑(lMap L.ofSubLanguage)) u')
Tactic:
simpa using System.inconsistent_lMap L.ofSubLanguage this
State after:
no goals