[GOAL]
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → Structure L (M a)
src✝ : Setoid ((a : α) → M a) := productSetoid (↑u) M
n : ℕ
f : Functions L n
x y : Fin n → (a : α) → M a
xy : x ≈ y
⊢ funMap f x ≈ funMap f y
[PROOFSTEP]
refine' mem_of_superset (iInter_mem.2 xy) fun a ha => _
[GOAL]
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → Structure L (M a)
src✝ : Setoid ((a : α) → M a) := productSetoid (↑u) M
n : ℕ
f : Functions L n
x y : Fin n → (a : α) → M a
xy : x ≈ y
a : α
ha : a ∈ ⋂ (i : Fin n), {x_1 | (fun a => x i a = y i a) x_1}
⊢ a ∈ {x_1 | (fun a => funMap f x a = funMap f y a) x_1}
[PROOFSTEP]
simp only [Set.mem_iInter, Set.mem_setOf_eq] at ha
[GOAL]
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → Structure L (M a)
src✝ : Setoid ((a : α) → M a) := productSetoid (↑u) M
n : ℕ
f : Functions L n
x y : Fin n → (a : α) → M a
xy : x ≈ y
a : α
ha : ∀ (i : Fin n), x i a = y i a
⊢ a ∈ {x_1 | (fun a => funMap f x a = funMap f y a) x_1}
[PROOFSTEP]
simp only [Set.mem_setOf_eq, ha]
[GOAL]
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → Structure L (M a)
src✝ : Setoid ((a : α) → M a) := productSetoid (↑u) M
n : ℕ
r : Relations L n
x y : Fin n → (a : α) → M a
xy : x ≈ y
⊢ RelMap r x = RelMap r y
[PROOFSTEP]
rw [← iff_eq_eq]
[GOAL]
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → Structure L (M a)
src✝ : Setoid ((a : α) → M a) := productSetoid (↑u) M
n : ℕ
r : Relations L n
x y : Fin n → (a : α) → M a
xy : x ≈ y
⊢ RelMap r x ↔ RelMap r y
[PROOFSTEP]
refine' ⟨fun hx => _, fun hy => _⟩
[GOAL]
case refine'_1
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → Structure L (M a)
src✝ : Setoid ((a : α) → M a) := productSetoid (↑u) M
n : ℕ
r : Relations L n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hx : RelMap r x
⊢ RelMap r y
[PROOFSTEP]
refine' mem_of_superset (inter_mem hx (iInter_mem.2 xy)) _
[GOAL]
case refine'_1
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → Structure L (M a)
src✝ : Setoid ((a : α) → M a) := productSetoid (↑u) M
n : ℕ
r : Relations L n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hx : RelMap r x
⊢ {x_1 | (fun a => RelMap r fun i => x i a) x_1} ∩ ⋂ (i : Fin n), {x_1 | (fun a => x i a = y i a) x_1} ⊆
    {x | (fun a => RelMap r fun i => y i a) x}
[PROOFSTEP]
rintro a ⟨ha1, ha2⟩
[GOAL]
case refine'_1.intro
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → Structure L (M a)
src✝ : Setoid ((a : α) → M a) := productSetoid (↑u) M
n : ℕ
r : Relations L n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hx : RelMap r x
a : α
ha1 : a ∈ {x_1 | (fun a => RelMap r fun i => x i a) x_1}
ha2 : a ∈ ⋂ (i : Fin n), {x_1 | (fun a => x i a = y i a) x_1}
⊢ a ∈ {x | (fun a => RelMap r fun i => y i a) x}
[PROOFSTEP]
simp only [Set.mem_iInter, Set.mem_setOf_eq] at *
[GOAL]
case refine'_1.intro
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → Structure L (M a)
src✝ : Setoid ((a : α) → M a) := productSetoid (↑u) M
n : ℕ
r : Relations L n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hx : ∀ᶠ (a : α) in ↑u, RelMap r fun i => x i a
a : α
ha1 : RelMap r fun i => x i a
ha2 : ∀ (i : Fin n), x i a = y i a
⊢ RelMap r fun i => y i a
[PROOFSTEP]
rw [← funext ha2]
[GOAL]
case refine'_1.intro
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → Structure L (M a)
src✝ : Setoid ((a : α) → M a) := productSetoid (↑u) M
n : ℕ
r : Relations L n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hx : ∀ᶠ (a : α) in ↑u, RelMap r fun i => x i a
a : α
ha1 : RelMap r fun i => x i a
ha2 : ∀ (i : Fin n), x i a = y i a
⊢ RelMap r fun x_1 => x x_1 a
[PROOFSTEP]
exact ha1
[GOAL]
case refine'_2
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → Structure L (M a)
src✝ : Setoid ((a : α) → M a) := productSetoid (↑u) M
n : ℕ
r : Relations L n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hy : RelMap r y
⊢ RelMap r x
[PROOFSTEP]
refine' mem_of_superset (inter_mem hy (iInter_mem.2 xy)) _
[GOAL]
case refine'_2
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → Structure L (M a)
src✝ : Setoid ((a : α) → M a) := productSetoid (↑u) M
n : ℕ
r : Relations L n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hy : RelMap r y
⊢ {x | (fun a => RelMap r fun i => y i a) x} ∩ ⋂ (i : Fin n), {x_1 | (fun a => x i a = y i a) x_1} ⊆
    {x_1 | (fun a => RelMap r fun i => x i a) x_1}
[PROOFSTEP]
rintro a ⟨ha1, ha2⟩
[GOAL]
case refine'_2.intro
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → Structure L (M a)
src✝ : Setoid ((a : α) → M a) := productSetoid (↑u) M
n : ℕ
r : Relations L n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hy : RelMap r y
a : α
ha1 : a ∈ {x | (fun a => RelMap r fun i => y i a) x}
ha2 : a ∈ ⋂ (i : Fin n), {x_1 | (fun a => x i a = y i a) x_1}
⊢ a ∈ {x_1 | (fun a => RelMap r fun i => x i a) x_1}
[PROOFSTEP]
simp only [Set.mem_iInter, Set.mem_setOf_eq] at *
[GOAL]
case refine'_2.intro
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → Structure L (M a)
src✝ : Setoid ((a : α) → M a) := productSetoid (↑u) M
n : ℕ
r : Relations L n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hy : ∀ᶠ (a : α) in ↑u, RelMap r fun i => y i a
a : α
ha1 : RelMap r fun i => y i a
ha2 : ∀ (i : Fin n), x i a = y i a
⊢ RelMap r fun i => x i a
[PROOFSTEP]
rw [funext ha2]
[GOAL]
case refine'_2.intro
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → Structure L (M a)
src✝ : Setoid ((a : α) → M a) := productSetoid (↑u) M
n : ℕ
r : Relations L n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hy : ∀ᶠ (a : α) in ↑u, RelMap r fun i => y i a
a : α
ha1 : RelMap r fun i => y i a
ha2 : ∀ (i : Fin n), x i a = y i a
⊢ RelMap r fun x => y x a
[PROOFSTEP]
exact ha1
[GOAL]
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → Structure L (M a)
n : ℕ
f : Functions L n
x : Fin n → (a : α) → M a
⊢ (funMap f fun i => Quotient.mk' (x i)) = Quotient.mk' fun a => funMap f fun i => x i a
[PROOFSTEP]
apply funMap_quotient_mk'
[GOAL]
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → Structure L (M a)
β : Type u_3
x : β → (a : α) → M a
t : Term L β
⊢ Term.realize (fun i => Quotient.mk' (x i)) t = Quotient.mk' fun a => Term.realize (fun i => x i a) t
[PROOFSTEP]
convert
  @Term.realize_quotient_mk' L _ ((u : Filter α).productSetoid M) (Ultraproduct.setoidPrestructure M u) _ t x using 2
[GOAL]
case h.e'_3.h.e'_3
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → Structure L (M a)
β : Type u_3
x : β → (a : α) → M a
t : Term L β
⊢ (fun a => Term.realize (fun i => x i a) t) = Term.realize x t
[PROOFSTEP]
ext a
[GOAL]
case h.e'_3.h.e'_3.h
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → Structure L (M a)
β : Type u_3
x : β → (a : α) → M a
t : Term L β
a : α
⊢ Term.realize (fun i => x i a) t = Term.realize x t a
[PROOFSTEP]
induction t
[GOAL]
case h.e'_3.h.e'_3.h.var
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → Structure L (M a)
β : Type u_3
x : β → (a : α) → M a
a : α
_a✝ : β
⊢ Term.realize (fun i => x i a) (var _a✝) = Term.realize x (var _a✝) a
case h.e'_3.h.e'_3.h.func
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → Structure L (M a)
β : Type u_3
x : β → (a : α) → M a
a : α
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L β
_ts_ih✝ : ∀ (a_1 : Fin l✝), Term.realize (fun i => x i a) (_ts✝ a_1) = Term.realize x (_ts✝ a_1) a
⊢ Term.realize (fun i => x i a) (func _f✝ _ts✝) = Term.realize x (func _f✝ _ts✝) a
[PROOFSTEP]
case var => rfl
[GOAL]
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → Structure L (M a)
β : Type u_3
x : β → (a : α) → M a
a : α
_a✝ : β
⊢ Term.realize (fun i => x i a) (var _a✝) = Term.realize x (var _a✝) a
[PROOFSTEP]
case var => rfl
[GOAL]
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → Structure L (M a)
β : Type u_3
x : β → (a : α) → M a
a : α
_a✝ : β
⊢ Term.realize (fun i => x i a) (var _a✝) = Term.realize x (var _a✝) a
[PROOFSTEP]
rfl
[GOAL]
case h.e'_3.h.e'_3.h.func
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → Structure L (M a)
β : Type u_3
x : β → (a : α) → M a
a : α
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L β
_ts_ih✝ : ∀ (a_1 : Fin l✝), Term.realize (fun i => x i a) (_ts✝ a_1) = Term.realize x (_ts✝ a_1) a
⊢ Term.realize (fun i => x i a) (func _f✝ _ts✝) = Term.realize x (func _f✝ _ts✝) a
[PROOFSTEP]
case func _ _ _ t_ih =>
  simp only [Term.realize, t_ih]
  rfl
[GOAL]
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → Structure L (M a)
β : Type u_3
x : β → (a : α) → M a
a : α
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L β
t_ih : ∀ (a_1 : Fin l✝), Term.realize (fun i => x i a) (_ts✝ a_1) = Term.realize x (_ts✝ a_1) a
⊢ Term.realize (fun i => x i a) (func _f✝ _ts✝) = Term.realize x (func _f✝ _ts✝) a
[PROOFSTEP]
case func _ _ _ t_ih =>
  simp only [Term.realize, t_ih]
  rfl
[GOAL]
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → Structure L (M a)
β : Type u_3
x : β → (a : α) → M a
a : α
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L β
t_ih : ∀ (a_1 : Fin l✝), Term.realize (fun i => x i a) (_ts✝ a_1) = Term.realize x (_ts✝ a_1) a
⊢ Term.realize (fun i => x i a) (func _f✝ _ts✝) = Term.realize x (func _f✝ _ts✝) a
[PROOFSTEP]
simp only [Term.realize, t_ih]
[GOAL]
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → Structure L (M a)
β : Type u_3
x : β → (a : α) → M a
a : α
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L β
t_ih : ∀ (a_1 : Fin l✝), Term.realize (fun i => x i a) (_ts✝ a_1) = Term.realize x (_ts✝ a_1) a
⊢ (funMap _f✝ fun i => Term.realize x (_ts✝ i) a) = funMap _f✝ (fun i => Term.realize x (_ts✝ i)) a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
φ : BoundedFormula L β n
x : β → (a : α) → M a
v : Fin n → (a : α) → M a
⊢ (BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
    ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize φ (fun i => x i a) fun i => v i a
[PROOFSTEP]
letI := (u : Filter α).productSetoid M
[GOAL]
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
φ : BoundedFormula L β n
x : β → (a : α) → M a
v : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
⊢ (BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
    ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize φ (fun i => x i a) fun i => v i a
[PROOFSTEP]
induction' φ with _ _ _ _ _ _ _ _ m _ _ ih ih' k φ ih
[GOAL]
case falsum
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
n✝ : ℕ
v : Fin n✝ → (a : α) → M a
⊢ (BoundedFormula.Realize BoundedFormula.falsum (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
    ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize BoundedFormula.falsum (fun i => x i a) fun i => v i a
[PROOFSTEP]
simp only [BoundedFormula.Realize, eventually_const]
[GOAL]
case equal
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
n✝ : ℕ
t₁✝ t₂✝ : Term L (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
⊢ (BoundedFormula.Realize (BoundedFormula.equal t₁✝ t₂✝) (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
    ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize (BoundedFormula.equal t₁✝ t₂✝) (fun i => x i a) fun i => v i a
[PROOFSTEP]
have h2 : ∀ a : α, (Sum.elim (fun i : β => x i a) fun i => v i a) = fun i => Sum.elim x v i a := fun a =>
  funext fun i => Sum.casesOn i (fun i => rfl) fun i => rfl
[GOAL]
case equal
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
n✝ : ℕ
t₁✝ t₂✝ : Term L (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i => x i a) fun i => v i a) = fun i => Sum.elim x v i a
⊢ (BoundedFormula.Realize (BoundedFormula.equal t₁✝ t₂✝) (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
    ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize (BoundedFormula.equal t₁✝ t₂✝) (fun i => x i a) fun i => v i a
[PROOFSTEP]
simp only [BoundedFormula.Realize, h2, term_realize_cast]
[GOAL]
case equal
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
n✝ : ℕ
t₁✝ t₂✝ : Term L (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i => x i a) fun i => v i a) = fun i => Sum.elim x v i a
⊢ Term.realize (Sum.elim (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) t₁✝ =
      Term.realize (Sum.elim (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) t₂✝ ↔
    ∀ᶠ (a : α) in ↑u, Term.realize (fun i => Sum.elim x v i a) t₁✝ = Term.realize (fun i => Sum.elim x v i a) t₂✝
[PROOFSTEP]
erw [(Sum.comp_elim ((↑) : (∀ a, M a) → (u : Filter α).Product M) x v).symm, term_realize_cast, term_realize_cast]
[GOAL]
case equal
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
n✝ : ℕ
t₁✝ t₂✝ : Term L (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i => x i a) fun i => v i a) = fun i => Sum.elim x v i a
⊢ ((Quotient.mk' fun a => Term.realize (fun i => Sum.elim x v i a) t₁✝) =
      Quotient.mk' fun a => Term.realize (fun i => Sum.elim x v i a) t₂✝) ↔
    ∀ᶠ (a : α) in ↑u, Term.realize (fun i => Sum.elim x v i a) t₁✝ = Term.realize (fun i => Sum.elim x v i a) t₂✝
[PROOFSTEP]
exact Quotient.eq''
[GOAL]
case rel
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
⊢ (BoundedFormula.Realize (BoundedFormula.rel R✝ ts✝) (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
    ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize (BoundedFormula.rel R✝ ts✝) (fun i => x i a) fun i => v i a
[PROOFSTEP]
have h2 : ∀ a : α, (Sum.elim (fun i : β => x i a) fun i => v i a) = fun i => Sum.elim x v i a := fun a =>
  funext fun i => Sum.casesOn i (fun i => rfl) fun i => rfl
[GOAL]
case rel
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i => x i a) fun i => v i a) = fun i => Sum.elim x v i a
⊢ (BoundedFormula.Realize (BoundedFormula.rel R✝ ts✝) (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
    ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize (BoundedFormula.rel R✝ ts✝) (fun i => x i a) fun i => v i a
[PROOFSTEP]
simp only [BoundedFormula.Realize, h2]
[GOAL]
case rel
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i => x i a) fun i => v i a) = fun i => Sum.elim x v i a
⊢ (RelMap R✝ fun i => Term.realize (Sum.elim (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) (ts✝ i)) ↔
    ∀ᶠ (a : α) in ↑u, RelMap R✝ fun i => Term.realize (fun i => Sum.elim x v i a) (ts✝ i)
[PROOFSTEP]
erw [(Sum.comp_elim ((↑) : (∀ a, M a) → (u : Filter α).Product M) x v).symm]
[GOAL]
case rel
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i => x i a) fun i => v i a) = fun i => Sum.elim x v i a
⊢ (RelMap R✝ fun i => Term.realize (Quotient.mk' ∘ Sum.elim x v) (ts✝ i)) ↔
    ∀ᶠ (a : α) in ↑u, RelMap R✝ fun i => Term.realize (fun i => Sum.elim x v i a) (ts✝ i)
[PROOFSTEP]
conv_lhs => enter [2, i]; erw [term_realize_cast]
[GOAL]
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i => x i a) fun i => v i a) = fun i => Sum.elim x v i a
| RelMap R✝ fun i => Term.realize (Quotient.mk' ∘ Sum.elim x v) (ts✝ i)
[PROOFSTEP]
enter [2, i]; erw [term_realize_cast]
[GOAL]
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i => x i a) fun i => v i a) = fun i => Sum.elim x v i a
| RelMap R✝ fun i => Term.realize (Quotient.mk' ∘ Sum.elim x v) (ts✝ i)
[PROOFSTEP]
enter [2, i]; erw [term_realize_cast]
[GOAL]
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i => x i a) fun i => v i a) = fun i => Sum.elim x v i a
| RelMap R✝ fun i => Term.realize (Quotient.mk' ∘ Sum.elim x v) (ts✝ i)
[PROOFSTEP]
enter [2, i]
[GOAL]
case h
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i => x i a) fun i => v i a) = fun i => Sum.elim x v i a
i : Fin l✝
| Term.realize (Quotient.mk' ∘ Sum.elim x v) (ts✝ i)
[PROOFSTEP]
erw [term_realize_cast]
[GOAL]
case rel
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
n✝ l✝ : ℕ
R✝ : Relations L l✝
ts✝ : Fin l✝ → Term L (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i => x i a) fun i => v i a) = fun i => Sum.elim x v i a
⊢ (RelMap R✝ fun i => Quotient.mk' fun a => Term.realize (fun i => Sum.elim x v i a) (ts✝ i)) ↔
    ∀ᶠ (a : α) in ↑u, RelMap R✝ fun i => Term.realize (fun i => Sum.elim x v i a) (ts✝ i)
[PROOFSTEP]
apply relMap_quotient_mk'
[GOAL]
case imp
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
m : ℕ
f₁✝ f₂✝ : BoundedFormula L β m
ih :
  ∀ (v : Fin m → (a : α) → M a),
    (BoundedFormula.Realize f₁✝ (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize f₁✝ (fun i => x i a) fun i => v i a
ih' :
  ∀ (v : Fin m → (a : α) → M a),
    (BoundedFormula.Realize f₂✝ (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize f₂✝ (fun i => x i a) fun i => v i a
v : Fin m → (a : α) → M a
⊢ (BoundedFormula.Realize (f₁✝ ⟹ f₂✝) (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
    ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize (f₁✝ ⟹ f₂✝) (fun i => x i a) fun i => v i a
[PROOFSTEP]
simp only [BoundedFormula.Realize, ih v, ih' v]
[GOAL]
case imp
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
m : ℕ
f₁✝ f₂✝ : BoundedFormula L β m
ih :
  ∀ (v : Fin m → (a : α) → M a),
    (BoundedFormula.Realize f₁✝ (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize f₁✝ (fun i => x i a) fun i => v i a
ih' :
  ∀ (v : Fin m → (a : α) → M a),
    (BoundedFormula.Realize f₂✝ (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize f₂✝ (fun i => x i a) fun i => v i a
v : Fin m → (a : α) → M a
⊢ ((∀ᶠ (a : α) in ↑u, BoundedFormula.Realize f₁✝ (fun i => x i a) fun i => v i a) →
      ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize f₂✝ (fun i => x i a) fun i => v i a) ↔
    ∀ᶠ (a : α) in ↑u,
      (BoundedFormula.Realize f₁✝ (fun i => x i a) fun i => v i a) →
        BoundedFormula.Realize f₂✝ (fun i => x i a) fun i => v i a
[PROOFSTEP]
rw [Ultrafilter.eventually_imp]
[GOAL]
case all
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
k : ℕ
φ : BoundedFormula L β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize φ (fun i => x i a) fun i => v i a
v : Fin k → (a : α) → M a
⊢ (BoundedFormula.Realize (∀'φ) (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
    ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize (∀'φ) (fun i => x i a) fun i => v i a
[PROOFSTEP]
simp only [BoundedFormula.Realize]
[GOAL]
case all
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
k : ℕ
φ : BoundedFormula L β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize φ (fun i => x i a) fun i => v i a
v : Fin k → (a : α) → M a
⊢ (∀ (x_1 : Quotient (productSetoid ↑u fun a => M a)),
      BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) (Fin.snoc (fun i => Quotient.mk' (v i)) x_1)) ↔
    ∀ᶠ (a : α) in ↑u, ∀ (x_1 : M a), BoundedFormula.Realize φ (fun i => x i a) (Fin.snoc (fun i => v i a) x_1)
[PROOFSTEP]
apply
  Iff.trans (b :=
    ∀ m : ∀ a : α, M a,
      φ.Realize (fun i : β => (x i : (u : Filter α).Product M))
        (Fin.snoc (((↑) : (∀ a, M a) → (u : Filter α).Product M) ∘ v) (m : (u : Filter α).Product M)))
[GOAL]
case all.h₁
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
k : ℕ
φ : BoundedFormula L β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize φ (fun i => x i a) fun i => v i a
v : Fin k → (a : α) → M a
⊢ (∀ (x_1 : Quotient (productSetoid ↑u fun a => M a)),
      BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) (Fin.snoc (fun i => Quotient.mk' (v i)) x_1)) ↔
    ∀ (m : (a : α) → M a),
      BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) (Fin.snoc (Quotient.mk' ∘ v) (Quotient.mk' m))
[PROOFSTEP]
exact forall_quotient_iff
[GOAL]
case all.h₂
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
k : ℕ
φ : BoundedFormula L β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize φ (fun i => x i a) fun i => v i a
v : Fin k → (a : α) → M a
⊢ (∀ (m : (a : α) → M a),
      BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) (Fin.snoc (Quotient.mk' ∘ v) (Quotient.mk' m))) ↔
    ∀ᶠ (a : α) in ↑u, ∀ (x_1 : M a), BoundedFormula.Realize φ (fun i => x i a) (Fin.snoc (fun i => v i a) x_1)
[PROOFSTEP]
have h' :
  ∀ (m : ∀ a, M a) (a : α),
    (fun i : Fin (k + 1) => (Fin.snoc v m : _ → ∀ a, M a) i a) = Fin.snoc (fun i : Fin k => v i a) (m a) :=
  by
  refine' fun m a => funext (Fin.reverseInduction _ fun i _ => _)
  · simp only [Fin.snoc_last]
  · simp only [Fin.snoc_castSucc]
[GOAL]
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
k : ℕ
φ : BoundedFormula L β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize φ (fun i => x i a) fun i => v i a
v : Fin k → (a : α) → M a
⊢ ∀ (m : (a : α) → M a) (a : α), (fun i => Fin.snoc v m i a) = Fin.snoc (fun i => v i a) (m a)
[PROOFSTEP]
refine' fun m a => funext (Fin.reverseInduction _ fun i _ => _)
[GOAL]
case refine'_1
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
k : ℕ
φ : BoundedFormula L β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize φ (fun i => x i a) fun i => v i a
v : Fin k → (a : α) → M a
m : (a : α) → M a
a : α
⊢ Fin.snoc v m (Fin.last k) a = Fin.snoc (fun i => v i a) (m a) (Fin.last k)
[PROOFSTEP]
simp only [Fin.snoc_last]
[GOAL]
case refine'_2
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
k : ℕ
φ : BoundedFormula L β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize φ (fun i => x i a) fun i => v i a
v : Fin k → (a : α) → M a
m : (a : α) → M a
a : α
i : Fin k
x✝ : Fin.snoc v m (Fin.succ i) a = Fin.snoc (fun i => v i a) (m a) (Fin.succ i)
⊢ Fin.snoc v m (Fin.castSucc i) a = Fin.snoc (fun i => v i a) (m a) (Fin.castSucc i)
[PROOFSTEP]
simp only [Fin.snoc_castSucc]
[GOAL]
case all.h₂
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
k : ℕ
φ : BoundedFormula L β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize φ (fun i => x i a) fun i => v i a
v : Fin k → (a : α) → M a
h' : ∀ (m : (a : α) → M a) (a : α), (fun i => Fin.snoc v m i a) = Fin.snoc (fun i => v i a) (m a)
⊢ (∀ (m : (a : α) → M a),
      BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) (Fin.snoc (Quotient.mk' ∘ v) (Quotient.mk' m))) ↔
    ∀ᶠ (a : α) in ↑u, ∀ (x_1 : M a), BoundedFormula.Realize φ (fun i => x i a) (Fin.snoc (fun i => v i a) x_1)
[PROOFSTEP]
simp only [← Fin.comp_snoc]
[GOAL]
case all.h₂
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
k : ℕ
φ : BoundedFormula L β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize φ (fun i => x i a) fun i => v i a
v : Fin k → (a : α) → M a
h' : ∀ (m : (a : α) → M a) (a : α), (fun i => Fin.snoc v m i a) = Fin.snoc (fun i => v i a) (m a)
⊢ (∀ (m : (a : α) → M a), BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) (Quotient.mk' ∘ Fin.snoc v m)) ↔
    ∀ᶠ (a : α) in ↑u, ∀ (x_1 : M a), BoundedFormula.Realize φ (fun i => x i a) (Fin.snoc (fun i => v i a) x_1)
[PROOFSTEP]
simp only [Function.comp, ih, h']
[GOAL]
case all.h₂
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
k : ℕ
φ : BoundedFormula L β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize φ (fun i => x i a) fun i => v i a
v : Fin k → (a : α) → M a
h' : ∀ (m : (a : α) → M a) (a : α), (fun i => Fin.snoc v m i a) = Fin.snoc (fun i => v i a) (m a)
⊢ (∀ (m : (a : α) → M a),
      ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize φ (fun i => x i a) (Fin.snoc (fun i => v i a) (m a))) ↔
    ∀ᶠ (a : α) in ↑u, ∀ (x_1 : M a), BoundedFormula.Realize φ (fun i => x i a) (Fin.snoc (fun i => v i a) x_1)
[PROOFSTEP]
refine' ⟨fun h => _, fun h m => _⟩
[GOAL]
case all.h₂.refine'_1
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
k : ℕ
φ : BoundedFormula L β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize φ (fun i => x i a) fun i => v i a
v : Fin k → (a : α) → M a
h' : ∀ (m : (a : α) → M a) (a : α), (fun i => Fin.snoc v m i a) = Fin.snoc (fun i => v i a) (m a)
h : ∀ (m : (a : α) → M a), ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize φ (fun i => x i a) (Fin.snoc (fun i => v i a) (m a))
⊢ ∀ᶠ (a : α) in ↑u, ∀ (x_1 : M a), BoundedFormula.Realize φ (fun i => x i a) (Fin.snoc (fun i => v i a) x_1)
[PROOFSTEP]
contrapose! h
[GOAL]
case all.h₂.refine'_1
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
k : ℕ
φ : BoundedFormula L β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize φ (fun i => x i a) fun i => v i a
v : Fin k → (a : α) → M a
h' : ∀ (m : (a : α) → M a) (a : α), (fun i => Fin.snoc v m i a) = Fin.snoc (fun i => v i a) (m a)
h : ¬∀ᶠ (a : α) in ↑u, ∀ (x_1 : M a), BoundedFormula.Realize φ (fun i => x i a) (Fin.snoc (fun i => v i a) x_1)
⊢ ∃ m, ¬∀ᶠ (a : α) in ↑u, BoundedFormula.Realize φ (fun i => x i a) (Fin.snoc (fun i => v i a) (m a))
[PROOFSTEP]
simp_rw [← Ultrafilter.eventually_not, not_forall] at h
[GOAL]
case all.h₂.refine'_1
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
k : ℕ
φ : BoundedFormula L β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize φ (fun i => x i a) fun i => v i a
v : Fin k → (a : α) → M a
h' : ∀ (m : (a : α) → M a) (a : α), (fun i => Fin.snoc v m i a) = Fin.snoc (fun i => v i a) (m a)
h : ∀ᶠ (x_1 : α) in ↑u, ∃ x_2, ¬BoundedFormula.Realize φ (fun i => x i x_1) (Fin.snoc (fun i => v i x_1) x_2)
⊢ ∃ m, ¬∀ᶠ (a : α) in ↑u, BoundedFormula.Realize φ (fun i => x i a) (Fin.snoc (fun i => v i a) (m a))
[PROOFSTEP]
refine' ⟨fun a : α => Classical.epsilon fun m : M a => ¬φ.Realize (fun i => x i a) (Fin.snoc (fun i => v i a) m), _⟩
[GOAL]
case all.h₂.refine'_1
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
k : ℕ
φ : BoundedFormula L β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize φ (fun i => x i a) fun i => v i a
v : Fin k → (a : α) → M a
h' : ∀ (m : (a : α) → M a) (a : α), (fun i => Fin.snoc v m i a) = Fin.snoc (fun i => v i a) (m a)
h : ∀ᶠ (x_1 : α) in ↑u, ∃ x_2, ¬BoundedFormula.Realize φ (fun i => x i x_1) (Fin.snoc (fun i => v i x_1) x_2)
⊢ ¬∀ᶠ (a : α) in ↑u,
      BoundedFormula.Realize φ (fun i => x i a)
        (Fin.snoc (fun i => v i a)
          ((fun a =>
              Classical.epsilon fun m => ¬BoundedFormula.Realize φ (fun i => x i a) (Fin.snoc (fun i => v i a) m))
            a))
[PROOFSTEP]
rw [← Ultrafilter.eventually_not]
[GOAL]
case all.h₂.refine'_1
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
k : ℕ
φ : BoundedFormula L β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize φ (fun i => x i a) fun i => v i a
v : Fin k → (a : α) → M a
h' : ∀ (m : (a : α) → M a) (a : α), (fun i => Fin.snoc v m i a) = Fin.snoc (fun i => v i a) (m a)
h : ∀ᶠ (x_1 : α) in ↑u, ∃ x_2, ¬BoundedFormula.Realize φ (fun i => x i x_1) (Fin.snoc (fun i => v i x_1) x_2)
⊢ ∀ᶠ (x_1 : α) in ↑u,
    ¬BoundedFormula.Realize φ (fun i => x i x_1)
        (Fin.snoc (fun i => v i x_1)
          ((fun a =>
              Classical.epsilon fun m => ¬BoundedFormula.Realize φ (fun i => x i a) (Fin.snoc (fun i => v i a) m))
            x_1))
[PROOFSTEP]
exact Filter.mem_of_superset h fun a ha => Classical.epsilon_spec ha
[GOAL]
case all.h₂.refine'_2
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
k : ℕ
φ : BoundedFormula L β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize φ (fun i => x i a) fun i => v i a
v : Fin k → (a : α) → M a
h' : ∀ (m : (a : α) → M a) (a : α), (fun i => Fin.snoc v m i a) = Fin.snoc (fun i => v i a) (m a)
h : ∀ᶠ (a : α) in ↑u, ∀ (x_1 : M a), BoundedFormula.Realize φ (fun i => x i a) (Fin.snoc (fun i => v i a) x_1)
m : (a : α) → M a
⊢ ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize φ (fun i => x i a) (Fin.snoc (fun i => v i a) (m a))
[PROOFSTEP]
rw [Filter.eventually_iff] at *
[GOAL]
case all.h₂.refine'_2
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
v✝ : Fin n → (a : α) → M a
this : Setoid ((a : α) → M a) := productSetoid (↑u) M
k : ℕ
φ : BoundedFormula L β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, BoundedFormula.Realize φ (fun i => x i a) fun i => v i a
v : Fin k → (a : α) → M a
h' : ∀ (m : (a : α) → M a) (a : α), (fun i => Fin.snoc v m i a) = Fin.snoc (fun i => v i a) (m a)
h : {x_1 | ∀ (x_2 : M x_1), BoundedFormula.Realize φ (fun i => x i x_1) (Fin.snoc (fun i => v i x_1) x_2)} ∈ ↑u
m : (a : α) → M a
⊢ {x_1 | BoundedFormula.Realize φ (fun i => x i x_1) (Fin.snoc (fun i => v i x_1) (m x_1))} ∈ ↑u
[PROOFSTEP]
exact Filter.mem_of_superset h fun a ha => ha (m a)
[GOAL]
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
φ : Formula L β
x : β → (a : α) → M a
⊢ (Formula.Realize φ fun i => Quotient.mk' (x i)) ↔ ∀ᶠ (a : α) in ↑u, Formula.Realize φ fun i => x i a
[PROOFSTEP]
simp_rw [Formula.Realize, ← boundedFormula_realize_cast φ x, iff_eq_eq]
[GOAL]
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
φ : Formula L β
x : β → (a : α) → M a
⊢ BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) default =
    BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' fun a => default i
[PROOFSTEP]
exact congr rfl (Subsingleton.elim _ _)
[GOAL]
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
φ : Sentence L
⊢ Product (↑u) M ⊨ φ ↔ ∀ᶠ (a : α) in ↑u, M a ⊨ φ
[PROOFSTEP]
simp_rw [Sentence.Realize]
[GOAL]
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
φ : Sentence L
⊢ Formula.Realize φ default ↔ ∀ᶠ (a : α) in ↑u, Formula.Realize φ default
[PROOFSTEP]
erw [← realize_formula_cast φ, iff_eq_eq]
[GOAL]
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
φ : Sentence L
⊢ Formula.Realize φ default = Formula.Realize φ fun i => Quotient.mk' fun a => default i
[PROOFSTEP]
exact congr rfl (Subsingleton.elim _ _)


[GOAL]
L : Language
T : Theory L
α : Type w
p q : CompleteType T α
h : (fun p => ↑p) p = (fun p => ↑p) q
⊢ p = q
[PROOFSTEP]
cases p
[GOAL]
case mk
L : Language
T : Theory L
α : Type w
q : CompleteType T α
toTheory✝ : Theory (L[[α]])
subset'✝ : LHom.onTheory (lhomWithConstants L α) T ⊆ toTheory✝
isMaximal'✝ : IsMaximal toTheory✝
h : (fun p => ↑p) { toTheory := toTheory✝, subset' := subset'✝, isMaximal' := isMaximal'✝ } = (fun p => ↑p) q
⊢ { toTheory := toTheory✝, subset' := subset'✝, isMaximal' := isMaximal'✝ } = q
[PROOFSTEP]
cases q
[GOAL]
case mk.mk
L : Language
T : Theory L
α : Type w
toTheory✝¹ : Theory (L[[α]])
subset'✝¹ : LHom.onTheory (lhomWithConstants L α) T ⊆ toTheory✝¹
isMaximal'✝¹ : IsMaximal toTheory✝¹
toTheory✝ : Theory (L[[α]])
subset'✝ : LHom.onTheory (lhomWithConstants L α) T ⊆ toTheory✝
isMaximal'✝ : IsMaximal toTheory✝
h :
  (fun p => ↑p) { toTheory := toTheory✝¹, subset' := subset'✝¹, isMaximal' := isMaximal'✝¹ } =
    (fun p => ↑p) { toTheory := toTheory✝, subset' := subset'✝, isMaximal' := isMaximal'✝ }
⊢ { toTheory := toTheory✝¹, subset' := subset'✝¹, isMaximal' := isMaximal'✝¹ } =
    { toTheory := toTheory✝, subset' := subset'✝, isMaximal' := isMaximal'✝ }
[PROOFSTEP]
congr
[GOAL]
L : Language
T : Theory L
α : Type w
p : CompleteType T α
φ : Sentence (L[[α]])
hf : Formula.not φ ∈ p
ht : φ ∈ p
⊢ False
[PROOFSTEP]
have h : ¬IsSatisfiable ({ φ, φ.not } : L[[α]].Theory) :=
  by
  rintro ⟨@⟨_, _, h, _⟩⟩
  simp only [model_iff, mem_insert_iff, mem_singleton_iff, forall_eq_or_imp, forall_eq] at h
  exact h.2 h.1
[GOAL]
L : Language
T : Theory L
α : Type w
p : CompleteType T α
φ : Sentence (L[[α]])
hf : Formula.not φ ∈ p
ht : φ ∈ p
⊢ ¬IsSatisfiable {φ, Formula.not φ}
[PROOFSTEP]
rintro ⟨@⟨_, _, h, _⟩⟩
[GOAL]
case intro.mk
L : Language
T : Theory L
α : Type w
p : CompleteType T α
φ : Sentence (L[[α]])
hf : Formula.not φ ∈ p
ht : φ ∈ p
Carrier✝ : Type (max (max u w) v)
struc✝ : Structure (L[[α]]) Carrier✝
h : Carrier✝ ⊨ {φ, Formula.not φ}
nonempty'✝ : Nonempty Carrier✝
⊢ False
[PROOFSTEP]
simp only [model_iff, mem_insert_iff, mem_singleton_iff, forall_eq_or_imp, forall_eq] at h
[GOAL]
case intro.mk
L : Language
T : Theory L
α : Type w
p : CompleteType T α
φ : Sentence (L[[α]])
hf : Formula.not φ ∈ p
ht : φ ∈ p
Carrier✝ : Type (max (max u w) v)
struc✝ : Structure (L[[α]]) Carrier✝
nonempty'✝ : Nonempty Carrier✝
h : Carrier✝ ⊨ φ ∧ Carrier✝ ⊨ Formula.not φ
⊢ False
[PROOFSTEP]
exact h.2 h.1
[GOAL]
L : Language
T : Theory L
α : Type w
p : CompleteType T α
φ : Sentence (L[[α]])
hf : Formula.not φ ∈ p
ht : φ ∈ p
h : ¬IsSatisfiable {φ, Formula.not φ}
⊢ False
[PROOFSTEP]
refine' h (p.isMaximal.1.mono _)
[GOAL]
L : Language
T : Theory L
α : Type w
p : CompleteType T α
φ : Sentence (L[[α]])
hf : Formula.not φ ∈ p
ht : φ ∈ p
h : ¬IsSatisfiable {φ, Formula.not φ}
⊢ {φ, Formula.not φ} ⊆ ↑p
[PROOFSTEP]
rw [insert_subset_iff, singleton_subset_iff]
[GOAL]
L : Language
T : Theory L
α : Type w
p : CompleteType T α
φ : Sentence (L[[α]])
hf : Formula.not φ ∈ p
ht : φ ∈ p
h : ¬IsSatisfiable {φ, Formula.not φ}
⊢ φ ∈ ↑p ∧ Formula.not φ ∈ ↑p
[PROOFSTEP]
exact ⟨ht, hf⟩
[GOAL]
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
⊢ {p | S ⊆ ↑p} = ∅ ↔ ¬IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ S)
[PROOFSTEP]
rw [iff_not_comm, ← not_nonempty_iff_eq_empty, Classical.not_not, Set.Nonempty]
[GOAL]
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
⊢ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ S) ↔ ∃ x, x ∈ {p | S ⊆ ↑p}
[PROOFSTEP]
refine'
  ⟨fun h =>
    ⟨⟨L[[α]].completeTheory h.some, (subset_union_left _ S).trans completeTheory.subset,
        completeTheory.isMaximal (L[[α]]) h.some⟩,
      (subset_union_right ((L.lhomWithConstants α).onTheory T) _).trans completeTheory.subset⟩,
    _⟩
[GOAL]
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
⊢ (∃ x, x ∈ {p | S ⊆ ↑p}) → IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ S)
[PROOFSTEP]
rintro ⟨p, hp⟩
[GOAL]
case intro
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
p : CompleteType T α
hp : p ∈ {p | S ⊆ ↑p}
⊢ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ S)
[PROOFSTEP]
exact p.isMaximal.1.mono (union_subset p.subset hp)
[GOAL]
L : Language
T : Theory L
α : Type w
φ : Sentence (L[[α]])
⊢ {p | φ ∈ p} = Set.univ ↔ LHom.onTheory (lhomWithConstants L α) T ⊨ᵇ φ
[PROOFSTEP]
rw [models_iff_not_satisfiable, ← compl_empty_iff, compl_setOf_mem, ← setOf_subset_eq_empty_iff]
[GOAL]
L : Language
T : Theory L
α : Type w
φ : Sentence (L[[α]])
⊢ {p | Formula.not φ ∈ p} = ∅ ↔ {p | {Formula.not φ} ⊆ ↑p} = ∅
[PROOFSTEP]
simp
[GOAL]
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
⊢ {p | S ⊆ ↑p} = Set.univ ↔ ∀ (φ : Sentence (L[[α]])), φ ∈ S → LHom.onTheory (lhomWithConstants L α) T ⊨ᵇ φ
[PROOFSTEP]
have h : {p : T.CompleteType α | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S) :=
  by
  ext
  simp [subset_def]
[GOAL]
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
⊢ {p | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
[PROOFSTEP]
ext
[GOAL]
case h
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
x✝ : CompleteType T α
⊢ x✝ ∈ {p | S ⊆ ↑p} ↔ x✝ ∈ ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
[PROOFSTEP]
simp [subset_def]
[GOAL]
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
h : {p | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
⊢ {p | S ⊆ ↑p} = Set.univ ↔ ∀ (φ : Sentence (L[[α]])), φ ∈ S → LHom.onTheory (lhomWithConstants L α) T ⊨ᵇ φ
[PROOFSTEP]
simp_rw [h, sInter_eq_univ, ← setOf_mem_eq_univ_iff]
[GOAL]
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
h : {p | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
⊢ (∀ (s : Set (CompleteType T α)), s ∈ (fun φ => {p | φ ∈ p}) '' S → s = Set.univ) ↔
    ∀ (φ : Sentence (L[[α]])), φ ∈ S → {p | φ ∈ p} = Set.univ
[PROOFSTEP]
refine' ⟨fun h φ φS => h _ ⟨_, φS, rfl⟩, _⟩
[GOAL]
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
h : {p | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
⊢ (∀ (φ : Sentence (L[[α]])), φ ∈ S → {p | φ ∈ p} = Set.univ) →
    ∀ (s : Set (CompleteType T α)), s ∈ (fun φ => {p | φ ∈ p}) '' S → s = Set.univ
[PROOFSTEP]
rintro h _ ⟨φ, h1, rfl⟩
[GOAL]
case intro.intro
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
h✝ : {p | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
h : ∀ (φ : Sentence (L[[α]])), φ ∈ S → {p | φ ∈ p} = Set.univ
φ : Sentence (L[[α]])
h1 : φ ∈ S
⊢ (fun φ => {p | φ ∈ p}) φ = Set.univ
[PROOFSTEP]
exact h _ h1
[GOAL]
L : Language
T : Theory L
α : Type w
⊢ Nonempty (CompleteType T α) ↔ IsSatisfiable T
[PROOFSTEP]
rw [← isSatisfiable_onTheory_iff (lhomWithConstants_injective L α)]
[GOAL]
L : Language
T : Theory L
α : Type w
⊢ Nonempty (CompleteType T α) ↔ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T)
[PROOFSTEP]
rw [nonempty_iff_univ_nonempty, nonempty_iff_ne_empty, Ne.def, not_iff_comm, ←
  union_empty ((L.lhomWithConstants α).onTheory T), ← setOf_subset_eq_empty_iff]
[GOAL]
L : Language
T : Theory L
α : Type w
⊢ {p | ∅ ⊆ ↑p} = ∅ ↔ Set.univ = ∅
[PROOFSTEP]
simp
[GOAL]
L : Language
T : Theory L
α : Type w
ι : Type u_1
S : ι → Theory (L[[α]])
⊢ ⋂ (i : ι), {p | S i ⊆ ↑p} = {p | ⋃ (i : ι), S i ⊆ ↑p}
[PROOFSTEP]
ext
[GOAL]
case h
L : Language
T : Theory L
α : Type w
ι : Type u_1
S : ι → Theory (L[[α]])
x✝ : CompleteType T α
⊢ x✝ ∈ ⋂ (i : ι), {p | S i ⊆ ↑p} ↔ x✝ ∈ {p | ⋃ (i : ι), S i ⊆ ↑p}
[PROOFSTEP]
simp only [mem_iInter, mem_setOf_eq, iUnion_subset_iff]
[GOAL]
L : Language
T : Theory L
α : Type w
p : CompleteType T α
t : Finset (Sentence (L[[α]]))
⊢ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (Finset.toList t) ∈ p ↔ ↑t ⊆ ↑p
[PROOFSTEP]
simp_rw [subset_def, ← SetLike.mem_coe, p.isMaximal.mem_iff_models, models_sentence_iff, Sentence.Realize,
  Formula.Realize, BoundedFormula.realize_foldr_inf, Finset.mem_toList]
[GOAL]
L : Language
T : Theory L
α : Type w
p : CompleteType T α
t : Finset (Sentence (L[[α]]))
⊢ (∀ (M : ModelType ↑p) (φ : BoundedFormula (L[[α]]) Empty 0), φ ∈ t → BoundedFormula.Realize φ default default) ↔
    ∀ (x : Sentence (L[[α]])), x ∈ ↑t → ∀ (M : ModelType ↑p), BoundedFormula.Realize x default default
[PROOFSTEP]
exact ⟨fun h φ hφ M => h _ _ hφ, fun h M φ hφ => h _ hφ _⟩
[GOAL]
L : Language
T : Theory L
α : Type w
M : Type w'
inst✝² : Structure L M
inst✝¹ : Nonempty M
inst✝ : M ⊨ T
v : α → M
φ : Formula L α
⊢ ↑Formula.equivSentence φ ∈ typeOf T v ↔ Formula.Realize φ v
[PROOFSTEP]
simp
[GOAL]
L : Language
T : Theory L
α : Type w
M : Type w'
inst✝² : Structure L M
inst✝¹ : Nonempty M
inst✝ : M ⊨ T
p : CompleteType T α
⊢ ∃ M, p ∈ realizedTypes T (↑M) α
[PROOFSTEP]
obtain ⟨M⟩ := p.isMaximal.1
[GOAL]
case intro
L : Language
T : Theory L
α : Type w
M✝ : Type w'
inst✝² : Structure L M✝
inst✝¹ : Nonempty M✝
inst✝ : M✝ ⊨ T
p : CompleteType T α
M : ModelType ↑p
⊢ ∃ M, p ∈ realizedTypes T (↑M) α
[PROOFSTEP]
refine' ⟨(M.subtheoryModel p.subset).reduct (L.lhomWithConstants α), fun a => (L.con a : M), _⟩
[GOAL]
case intro
L : Language
T : Theory L
α : Type w
M✝ : Type w'
inst✝² : Structure L M✝
inst✝¹ : Nonempty M✝
inst✝ : M✝ ⊨ T
p : CompleteType T α
M : ModelType ↑p
⊢ (typeOf T fun a => ↑(Language.con L a)) = p
[PROOFSTEP]
refine' SetLike.ext fun φ => _
[GOAL]
case intro
L : Language
T : Theory L
α : Type w
M✝ : Type w'
inst✝² : Structure L M✝
inst✝¹ : Nonempty M✝
inst✝ : M✝ ⊨ T
p : CompleteType T α
M : ModelType ↑p
φ : Sentence (L[[α]])
⊢ (φ ∈ typeOf T fun a => ↑(Language.con L a)) ↔ φ ∈ p
[PROOFSTEP]
simp only [CompleteType.mem_typeOf]
[GOAL]
case intro
L : Language
T : Theory L
α : Type w
M✝ : Type w'
inst✝² : Structure L M✝
inst✝¹ : Nonempty M✝
inst✝ : M✝ ⊨ T
p : CompleteType T α
M : ModelType ↑p
φ : Sentence (L[[α]])
⊢ (Formula.Realize (↑Formula.equivSentence.symm φ) fun a => ↑(Language.con L a)) ↔ φ ∈ p
[PROOFSTEP]
refine'
  (@Formula.realize_equivSentence_symm_con _ ((M.subtheoryModel p.subset).reduct (L.lhomWithConstants α)) _ _ M.struc _
        φ).trans
    (_root_.trans (_root_.trans _ (p.isMaximal.isComplete.realize_sentence_iff φ M))
      (p.isMaximal.mem_iff_models φ).symm)
[GOAL]
case intro
L : Language
T : Theory L
α : Type w
M✝ : Type w'
inst✝² : Structure L M✝
inst✝¹ : Nonempty M✝
inst✝ : M✝ ⊨ T
p : CompleteType T α
M : ModelType ↑p
φ : Sentence (L[[α]])
⊢ ↑(ModelType.reduct (lhomWithConstants L α)
          (ModelType.subtheoryModel M (_ : LHom.onTheory (lhomWithConstants L α) T ⊆ ↑p))) ⊨
      φ ↔
    ↑M ⊨ φ
[PROOFSTEP]
rfl