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

State before:
L : Language
T : Theory L
h : System.Consistent T
⊢ Semantics.Satisfiable (Struc L) T
Tactic:
let ⟨M, _, _, h⟩ := satisfiable_iff.mp (satisfiable_of_consistent' h)
State after:
L : Language
T : Theory L
h✝ : System.Consistent T
M : Type u
w✝¹ : Nonempty M
w✝ : Structure L M
h : M ⊧ₘ* T
⊢ Semantics.Satisfiable (Struc L) T

State before:
L : Language
T : Theory L
h✝ : System.Consistent T
M : Type u
w✝¹ : Nonempty M
w✝ : Structure L M
h : M ⊧ₘ* T
⊢ Semantics.Satisfiable (Struc L) T
Tactic:
exact satisfiable_iff.mpr ⟨ULift.{w} M, inferInstance, inferInstance, ((uLift_elementaryEquiv L M).modelsTheory).mpr h⟩
State after:
no goals