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

State before:
L : Language
T : Theory L
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
σ : Sentence L
h : T ⊨ σ
⊢ T ⊢! σ
Tactic:
have : T ⊢'' [Rew.emb.hom σ] :=
  Disjconseq.completeness_of_encodable (T := T) (Γ := {σ}) (fun M i s hM ↦ ⟨σ, List.mem_of_mem_head? rfl, h hM⟩)
State after:
L : Language
T : Theory L
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
σ : Sentence L
h : T ⊨ σ
this : T ⊢'' [Rew.emb.hom σ]
⊢ T ⊢! σ

State before:
L : Language
T : Theory L
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
σ : Sentence L
h : T ⊨ σ
this : T ⊢'' [Rew.emb.hom σ]
⊢ T ⊢! σ
Tactic:
exact ⟨toProof this⟩
State after:
no goals