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)
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this : (α : Sort ?u.10884) → DecidableEq α := Classical.typeDecidableEq
⊢ T ⊢! σ
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝ : (α : Sort ?u.10884) → DecidableEq α := Classical.typeDecidableEq
this : ∃ u, ↑u ⊆ insert (~σ) T ∧ ¬Satisfiable ↑u
⊢ T ⊢! σ