-- Mathlib/ModelTheory/Satisfiability.lean
theorem isSatisfiable_iff_isFinitelySatisfiable {T : L.Theory} :
    T.IsSatisfiable ↔ T.IsFinitelySatisfiable :=
  ⟨Theory.IsSatisfiable.isFinitelySatisfiable, fun h => by
    classical
      set M : Finset T → Type max u v := fun T0 : Finset T =>
        (h (T0.map (Function.Embedding.subtype fun x => x ∈ T)) T0.map_subtype_subset).some.Carrier
      let M' := Filter.Product (Ultrafilter.of (Filter.atTop : Filter (Finset T))) M
      have h' : M' ⊨ T

Proof state:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
M : Finset ↑T → Type (max u v) := fun T0 => ↑(Nonempty.some ⋯)
M' : Type (max u v) := (↑(Ultrafilter.of Filter.atTop)).Product M
⊢ M' ⊨ T

Tactic:
refine ⟨fun φ hφ => ?_⟩

Result:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
M : Finset ↑T → Type (max u v) := fun T0 => ↑(Nonempty.some ⋯)
M' : Type (max u v) := (↑(Ultrafilter.of Filter.atTop)).Product M
φ : L.Sentence
hφ : φ ∈ T
⊢ M' ⊨ φ

Proof state:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
M : Finset ↑T → Type (max u v) := fun T0 => ↑(Nonempty.some ⋯)
M' : Type (max u v) := (↑(Ultrafilter.of Filter.atTop)).Product M
φ : L.Sentence
hφ : φ ∈ T
⊢ M' ⊨ φ

Tactic:
rw [Ultraproduct.sentence_realize]

Result:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
M : Finset ↑T → Type (max u v) := fun T0 => ↑(Nonempty.some ⋯)
M' : Type (max u v) := (↑(Ultrafilter.of Filter.atTop)).Product M
φ : L.Sentence
hφ : φ ∈ T
⊢ ∀ᶠ (a : Finset ↑T) in ↑(Ultrafilter.of Filter.atTop), M a ⊨ φ

Proof state:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
M : Finset ↑T → Type (max u v) := fun T0 => ↑(Nonempty.some ⋯)
M' : Type (max u v) := (↑(Ultrafilter.of Filter.atTop)).Product M
φ : L.Sentence
hφ : φ ∈ T
s : Finset ↑T
h' : s ≥ {⟨φ, hφ⟩}
⊢ ∃ (x : φ ∈ T), ⟨φ, ⋯⟩ ∈ s

Tactic:
exact ⟨hφ, h' (Finset.mem_singleton_self _)⟩

Result:
no goals

Proof state:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
M : Finset ↑T → Type (max u v) := fun T0 => ↑(Nonempty.some ⋯)
⊢ T.IsSatisfiable

Tactic:
let M' := Filter.Product (Ultrafilter.of (Filter.atTop : Filter (Finset T))) M

Result:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
M : Finset ↑T → Type (max u v) := fun T0 => ↑(Nonempty.some ⋯)
M' : Type (max u v) := (↑(Ultrafilter.of Filter.atTop)).Product M
⊢ T.IsSatisfiable

Proof state:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
M : Finset ↑T → Type (max u v) := fun T0 => ↑(Nonempty.some ⋯)
M' : Type (max u v) := (↑(Ultrafilter.of Filter.atTop)).Product M
φ : L.Sentence
hφ : φ ∈ T
⊢ ∀ᶠ (a : Finset ↑T) in ↑(Ultrafilter.of Filter.atTop), M a ⊨ φ

Tactic:
refine
  Filter.Eventually.filter_mono (Ultrafilter.of_le _)
    (Filter.eventually_atTop.2
      ⟨{⟨φ, hφ⟩}, fun s h' =>
        Theory.realize_sentence_of_mem (s.map (Function.Embedding.subtype fun x => x ∈ T))
          ?_⟩)

Result:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
M : Finset ↑T → Type (max u v) := fun T0 => ↑(Nonempty.some ⋯)
M' : Type (max u v) := (↑(Ultrafilter.of Filter.atTop)).Product M
φ : L.Sentence
hφ : φ ∈ T
s : Finset ↑T
h' : s ≥ {⟨φ, hφ⟩}
⊢ φ ∈ ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ T) s)

Proof state:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
⊢ T.IsSatisfiable

Tactic:
set M : Finset T → Type max u v := fun T0 : Finset T =>
  (h (T0.map (Function.Embedding.subtype fun x => x ∈ T)) T0.map_subtype_subset).some.Carrier

Result:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
M : Finset ↑T → Type (max u v) := fun T0 => ↑(Nonempty.some ⋯)
⊢ T.IsSatisfiable

Proof state:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
M : Finset ↑T → Type (max u v) := fun T0 => ↑(Nonempty.some ⋯)
M' : Type (max u v) := (↑(Ultrafilter.of Filter.atTop)).Product M
⊢ T.IsSatisfiable

Tactic:
have h' : M' ⊨ T := by
  refine ⟨fun φ hφ => ?_⟩
  rw [Ultraproduct.sentence_realize]
  refine
    Filter.Eventually.filter_mono (Ultrafilter.of_le _)
      (Filter.eventually_atTop.2
        ⟨{⟨φ, hφ⟩}, fun s h' =>
          Theory.realize_sentence_of_mem (s.map (Function.Embedding.subtype fun x => x ∈ T))
            ?_⟩)
  simp only [Finset.coe_map, Function.Embedding.coe_subtype, Set.mem_image, Finset.mem_coe,
    Subtype.exists, Subtype.coe_mk, exists_and_right, exists_eq_right]
  exact ⟨hφ, h' (Finset.mem_singleton_self _)⟩

Result:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
M : Finset ↑T → Type (max u v) := fun T0 => ↑(Nonempty.some ⋯)
M' : Type (max u v) := (↑(Ultrafilter.of Filter.atTop)).Product M
h' : M' ⊨ T
⊢ T.IsSatisfiable

Proof state:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
⊢ T.IsSatisfiable

Tactic:
classical
  set M : Finset T → Type max u v := fun T0 : Finset T =>
    (h (T0.map (Function.Embedding.subtype fun x => x ∈ T)) T0.map_subtype_subset).some.Carrier
  let M' := Filter.Product (Ultrafilter.of (Filter.atTop : Filter (Finset T))) M
  have h' : M' ⊨ T := by
    refine ⟨fun φ hφ => ?_⟩
    rw [Ultraproduct.sentence_realize]
    refine
      Filter.Eventually.filter_mono (Ultrafilter.of_le _)
        (Filter.eventually_atTop.2
          ⟨{⟨φ, hφ⟩}, fun s h' =>
            Theory.realize_sentence_of_mem (s.map (Function.Embedding.subtype fun x => x ∈ T))
              ?_⟩)
    simp only [Finset.coe_map, Function.Embedding.coe_subtype, Set.mem_image, Finset.mem_coe,
      Subtype.exists, Subtype.coe_mk, exists_and_right, exists_eq_right]
    exact ⟨hφ, h' (Finset.mem_singleton_self _)⟩
  exact ⟨ModelType.of T M'⟩

Result:
no goals

Proof state:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
M : Finset ↑T → Type (max u v) := fun T0 => ↑(Nonempty.some ⋯)
M' : Type (max u v) := (↑(Ultrafilter.of Filter.atTop)).Product M
h' : M' ⊨ T
⊢ T.IsSatisfiable

Tactic:
exact ⟨ModelType.of T M'⟩

Result:
no goals

Proof state:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
M : Finset ↑T → Type (max u v) := fun T0 => ↑(Nonempty.some ⋯)
M' : Type (max u v) := (↑(Ultrafilter.of Filter.atTop)).Product M
φ : L.Sentence
hφ : φ ∈ T
s : Finset ↑T
h' : s ≥ {⟨φ, hφ⟩}
⊢ φ ∈ ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ T) s)

Tactic:
simp only [Finset.coe_map, Function.Embedding.coe_subtype, Set.mem_image, Finset.mem_coe,
  Subtype.exists, Subtype.coe_mk, exists_and_right, exists_eq_right]

Result:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
M : Finset ↑T → Type (max u v) := fun T0 => ↑(Nonempty.some ⋯)
M' : Type (max u v) := (↑(Ultrafilter.of Filter.atTop)).Product M
φ : L.Sentence
hφ : φ ∈ T
s : Finset ↑T
h' : s ≥ {⟨φ, hφ⟩}
⊢ ∃ (x : φ ∈ T), ⟨φ, ⋯⟩ ∈ s