[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 _ _)
