Theorem: LO.FirstOrder.Semiformula.eval_Uprod (Logic/FirstOrder/Ultraproduct.lean)

State before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
e : Fin n → Uprod A 𝓤
ε : μ → Uprod A 𝓤
p : Semiformula L μ n
⊢ (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
Tactic:
induction p using rec' <;>
simp[*, Prop.top_eq_true, Prop.bot_eq_false, eval_rel, eval_nrel, Semiterm.val_Uprod]
State after:
case hverum
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
e : Fin n✝ → Uprod A 𝓤
⊢ Set.univ ∈ 𝓤

case hnrel
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L μ n✝
e : Fin n✝ → Uprod A 𝓤
⊢ {i | Structure.rel r✝ fun x => Semiterm.val (s i) (fun x => (e x).val i) (fun x => (ε x).val i) (v✝ x)} ∉ 𝓤 ↔
    {i | ¬Structure.rel r✝ fun i_1 => Semiterm.val (s i) (fun x => (e x).val i) (fun x => (ε x).val i) (v✝ i_1)} ∈ 𝓤

case hand
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ :
  ∀ {e : Fin n✝ → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p✝ ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p✝} ∈ 𝓤
a✝ :
  ∀ {e : Fin n✝ → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) q✝ ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q✝} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
⊢ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p✝} ∈ 𝓤 ∧
      {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q✝} ∈ 𝓤 ↔
    {i |
        (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p✝ ∧
          (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q✝} ∈
      𝓤

case hor
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ :
  ∀ {e : Fin n✝ → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p✝ ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p✝} ∈ 𝓤
a✝ :
  ∀ {e : Fin n✝ → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) q✝ ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q✝} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
⊢ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p✝} ∈ 𝓤 ∨
      {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q✝} ∈ 𝓤 ↔
    {i |
        (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p✝ ∨
          (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q✝} ∈
      𝓤

case hall
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p✝ ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p✝} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
⊢ (∀ (x : Uprod A 𝓤), {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p✝} ∈ 𝓤) ↔
    {i | ∀ (x : A i), (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p✝} ∈ 𝓤

case hex
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p✝ ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p✝} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
⊢ (∃ x, {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p✝} ∈ 𝓤) ↔
    {i | ∃ x, (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p✝} ∈ 𝓤

State before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
e : Fin n✝ → Uprod A 𝓤
⊢ Set.univ ∈ 𝓤
Tactic:
case hverum => exact Filter.univ_mem
State after:
no goals

State before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → Uprod A 𝓤
⊢ {i | Structure.rel r fun x => Semiterm.val (s i) (fun x => (e x).val i) (fun x => (ε x).val i) (v x)} ∉ 𝓤 ↔
    {i | ¬Structure.rel r fun i_1 => Semiterm.val (s i) (fun x => (e x).val i) (fun x => (ε x).val i) (v i_1)} ∈ 𝓤
Tactic:
case hnrel k r v =>
  exact Ultrafilter.compl_mem_iff_not_mem.symm
State after:
no goals

State before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ :
  ∀ {e : Fin n✝ → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p✝ ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p✝} ∈ 𝓤
a✝ :
  ∀ {e : Fin n✝ → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) q✝ ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q✝} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
⊢ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p✝} ∈ 𝓤 ∧
      {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q✝} ∈ 𝓤 ↔
    {i |
        (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p✝ ∧
          (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q✝} ∈
      𝓤
Tactic:
case hand =>
  exact Filter.inter_mem_iff.symm
State after:
no goals

State before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p q : Semiformula L μ n✝
ihp :
  ∀ {e : Fin n✝ → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
ihq :
  ∀ {e : Fin n✝ → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) q ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
⊢ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤 ∨
      {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q} ∈ 𝓤 ↔
    {i |
        (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p ∨
          (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q} ∈
      𝓤
Tactic:
case hor p q ihp ihq =>
  exact Ultrafilter.union_mem_iff.symm
State after:
no goals

State before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
e : Fin n✝ → Uprod A 𝓤
⊢ Set.univ ∈ 𝓤
Tactic:
exact Filter.univ_mem
State after:
no goals

State before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → Uprod A 𝓤
⊢ {i | Structure.rel r fun x => Semiterm.val (s i) (fun x => (e x).val i) (fun x => (ε x).val i) (v x)} ∉ 𝓤 ↔
    {i | ¬Structure.rel r fun i_1 => Semiterm.val (s i) (fun x => (e x).val i) (fun x => (ε x).val i) (v i_1)} ∈ 𝓤
Tactic:
exact Ultrafilter.compl_mem_iff_not_mem.symm
State after:
no goals

State before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ :
  ∀ {e : Fin n✝ → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p✝ ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p✝} ∈ 𝓤
a✝ :
  ∀ {e : Fin n✝ → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) q✝ ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q✝} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
⊢ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p✝} ∈ 𝓤 ∧
      {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q✝} ∈ 𝓤 ↔
    {i |
        (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p✝ ∧
          (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q✝} ∈
      𝓤
Tactic:
exact Filter.inter_mem_iff.symm
State after:
no goals

State before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p q : Semiformula L μ n✝
ihp :
  ∀ {e : Fin n✝ → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
ihq :
  ∀ {e : Fin n✝ → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) q ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
⊢ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤 ∨
      {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q} ∈ 𝓤 ↔
    {i |
        (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p ∨
          (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q} ∈
      𝓤
Tactic:
exact Ultrafilter.union_mem_iff.symm
State after:
no goals

State before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
⊢ (∀ (x : Uprod A 𝓤), {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤) ↔
    {i | ∀ (x : A i), (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
Tactic:
constructor
State after:
case mp
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
⊢ (∀ (x : Uprod A 𝓤), {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤) →
    {i | ∀ (x : A i), (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤

case mpr
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
⊢ {i | ∀ (x : A i), (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤 →
    ∀ (x : Uprod A 𝓤), {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤

State before:
case mp
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
⊢ (∀ (x : Uprod A 𝓤), {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤) →
    {i | ∀ (x : A i), (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
Tactic:
intro h
State after:
case mp
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : ∀ (x : Uprod A 𝓤), {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤
⊢ {i | ∀ (x : A i), (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤

State before:
case mp
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : ∀ (x : Uprod A 𝓤), {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤
⊢ {i | ∀ (x : A i), (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
Tactic:
let z : Uprod A 𝓤 := ⟨fun i =>
  Classical.epsilon (fun z => ¬Eval (s i) (z :> fun x ↦ (e x).val i) (fun x ↦ (ε x).val i) p)⟩
State after:
case mp
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : ∀ (x : Uprod A 𝓤), {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤
z : Uprod A 𝓤 :=
  { val := fun i => Classical.epsilon fun z => ¬(Eval (s i) (z :> fun x => (e x).val i) fun x => (ε x).val i) p }
⊢ {i | ∀ (x : A i), (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤

State before:
case mp
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : ∀ (x : Uprod A 𝓤), {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤
z : Uprod A 𝓤 :=
  { val := fun i => Classical.epsilon fun z => ¬(Eval (s i) (z :> fun x => (e x).val i) fun x => (ε x).val i) p }
⊢ {i | ∀ (x : A i), (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
Tactic:
exact Filter.mem_of_superset (h z) (by
  intro i hι a
  have : Eval (s i) (z.val i :> fun x ↦ (e x).val i) (fun x ↦ (ε x).val i) p :=
    by rw [val_vecCons_val_eq]; exact hι
  by_contra hc
  have : ¬Evalm (A i) (z.val i :> fun x ↦ (e x).val i) (fun x ↦ (ε x).val i) p :=
    Classical.epsilon_spec (p := fun z => ¬(Eval (s i) (z :> fun x ↦ (e x).val i) _ p)) ⟨a, hc⟩
  contradiction)
State after:
no goals

State before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : ∀ (x : Uprod A 𝓤), {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤
z : Uprod A 𝓤 :=
  { val := fun i => Classical.epsilon fun z => ¬(Eval (s i) (z :> fun x => (e x).val i) fun x => (ε x).val i) p }
⊢ {i | (Eval (s i) (fun x => ((z :> e) x).val i) fun x => (ε x).val i) p} ⊆
    {i | ∀ (x : A i), (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p}
Tactic:
intro i hι a
State after:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : ∀ (x : Uprod A 𝓤), {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤
z : Uprod A 𝓤 :=
  { val := fun i => Classical.epsilon fun z => ¬(Eval (s i) (z :> fun x => (e x).val i) fun x => (ε x).val i) p }
i : I
hι : i ∈ {i | (Eval (s i) (fun x => ((z :> e) x).val i) fun x => (ε x).val i) p}
a : A i
⊢ (Eval (s i) (a :> fun x => (e x).val i) fun x => (ε x).val i) p

State before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : ∀ (x : Uprod A 𝓤), {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤
z : Uprod A 𝓤 :=
  { val := fun i => Classical.epsilon fun z => ¬(Eval (s i) (z :> fun x => (e x).val i) fun x => (ε x).val i) p }
i : I
hι : i ∈ {i | (Eval (s i) (fun x => ((z :> e) x).val i) fun x => (ε x).val i) p}
a : A i
⊢ (Eval (s i) (a :> fun x => (e x).val i) fun x => (ε x).val i) p
Tactic:
have : Eval (s i) (z.val i :> fun x ↦ (e x).val i) (fun x ↦ (ε x).val i) p :=
  by rw [val_vecCons_val_eq]; exact hι
State after:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : ∀ (x : Uprod A 𝓤), {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤
z : Uprod A 𝓤 :=
  { val := fun i => Classical.epsilon fun z => ¬(Eval (s i) (z :> fun x => (e x).val i) fun x => (ε x).val i) p }
i : I
hι : i ∈ {i | (Eval (s i) (fun x => ((z :> e) x).val i) fun x => (ε x).val i) p}
a : A i
this : (Eval (s i) (z.val i :> fun x => (e x).val i) fun x => (ε x).val i) p
⊢ (Eval (s i) (a :> fun x => (e x).val i) fun x => (ε x).val i) p

State before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : ∀ (x : Uprod A 𝓤), {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤
z : Uprod A 𝓤 :=
  { val := fun i => Classical.epsilon fun z => ¬(Eval (s i) (z :> fun x => (e x).val i) fun x => (ε x).val i) p }
i : I
hι : i ∈ {i | (Eval (s i) (fun x => ((z :> e) x).val i) fun x => (ε x).val i) p}
a : A i
this : (Eval (s i) (z.val i :> fun x => (e x).val i) fun x => (ε x).val i) p
⊢ (Eval (s i) (a :> fun x => (e x).val i) fun x => (ε x).val i) p
Tactic:
by_contra hc
State after:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : ∀ (x : Uprod A 𝓤), {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤
z : Uprod A 𝓤 :=
  { val := fun i => Classical.epsilon fun z => ¬(Eval (s i) (z :> fun x => (e x).val i) fun x => (ε x).val i) p }
i : I
hι : i ∈ {i | (Eval (s i) (fun x => ((z :> e) x).val i) fun x => (ε x).val i) p}
a : A i
this : (Eval (s i) (z.val i :> fun x => (e x).val i) fun x => (ε x).val i) p
hc : ¬(Eval (s i) (a :> fun x => (e x).val i) fun x => (ε x).val i) p
⊢ False

State before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : ∀ (x : Uprod A 𝓤), {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤
z : Uprod A 𝓤 :=
  { val := fun i => Classical.epsilon fun z => ¬(Eval (s i) (z :> fun x => (e x).val i) fun x => (ε x).val i) p }
i : I
hι : i ∈ {i | (Eval (s i) (fun x => ((z :> e) x).val i) fun x => (ε x).val i) p}
a : A i
this : (Eval (s i) (z.val i :> fun x => (e x).val i) fun x => (ε x).val i) p
hc : ¬(Eval (s i) (a :> fun x => (e x).val i) fun x => (ε x).val i) p
⊢ False
Tactic:
have : ¬Evalm (A i) (z.val i :> fun x ↦ (e x).val i) (fun x ↦ (ε x).val i) p :=
  Classical.epsilon_spec (p := fun z => ¬(Eval (s i) (z :> fun x ↦ (e x).val i) _ p)) ⟨a, hc⟩
State after:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : ∀ (x : Uprod A 𝓤), {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤
z : Uprod A 𝓤 :=
  { val := fun i => Classical.epsilon fun z => ¬(Eval (s i) (z :> fun x => (e x).val i) fun x => (ε x).val i) p }
i : I
hι : i ∈ {i | (Eval (s i) (fun x => ((z :> e) x).val i) fun x => (ε x).val i) p}
a : A i
this✝ : (Eval (s i) (z.val i :> fun x => (e x).val i) fun x => (ε x).val i) p
hc : ¬(Eval (s i) (a :> fun x => (e x).val i) fun x => (ε x).val i) p
this : ¬(Evalm (A i) (z.val i :> fun x => (e x).val i) fun x => (ε x).val i) p
⊢ False

State before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : ∀ (x : Uprod A 𝓤), {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤
z : Uprod A 𝓤 :=
  { val := fun i => Classical.epsilon fun z => ¬(Eval (s i) (z :> fun x => (e x).val i) fun x => (ε x).val i) p }
i : I
hι : i ∈ {i | (Eval (s i) (fun x => ((z :> e) x).val i) fun x => (ε x).val i) p}
a : A i
this✝ : (Eval (s i) (z.val i :> fun x => (e x).val i) fun x => (ε x).val i) p
hc : ¬(Eval (s i) (a :> fun x => (e x).val i) fun x => (ε x).val i) p
this : ¬(Evalm (A i) (z.val i :> fun x => (e x).val i) fun x => (ε x).val i) p
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : ∀ (x : Uprod A 𝓤), {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤
z : Uprod A 𝓤 :=
  { val := fun i => Classical.epsilon fun z => ¬(Eval (s i) (z :> fun x => (e x).val i) fun x => (ε x).val i) p }
i : I
hι : i ∈ {i | (Eval (s i) (fun x => ((z :> e) x).val i) fun x => (ε x).val i) p}
a : A i
⊢ (Eval (s i) (z.val i :> fun x => (e x).val i) fun x => (ε x).val i) p
Tactic:
rw [val_vecCons_val_eq]
State after:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : ∀ (x : Uprod A 𝓤), {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤
z : Uprod A 𝓤 :=
  { val := fun i => Classical.epsilon fun z => ¬(Eval (s i) (z :> fun x => (e x).val i) fun x => (ε x).val i) p }
i : I
hι : i ∈ {i | (Eval (s i) (fun x => ((z :> e) x).val i) fun x => (ε x).val i) p}
a : A i
⊢ (Eval (s i) (fun x => ((z :> fun x => e x) x).val i) fun x => (ε x).val i) p

State before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : ∀ (x : Uprod A 𝓤), {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤
z : Uprod A 𝓤 :=
  { val := fun i => Classical.epsilon fun z => ¬(Eval (s i) (z :> fun x => (e x).val i) fun x => (ε x).val i) p }
i : I
hι : i ∈ {i | (Eval (s i) (fun x => ((z :> e) x).val i) fun x => (ε x).val i) p}
a : A i
⊢ (Eval (s i) (fun x => ((z :> fun x => e x) x).val i) fun x => (ε x).val i) p
Tactic:
exact hι
State after:
no goals

State before:
case mpr
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
⊢ {i | ∀ (x : A i), (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤 →
    ∀ (x : Uprod A 𝓤), {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤
Tactic:
intro h x
State after:
case mpr
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : {i | ∀ (x : A i), (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
x : Uprod A 𝓤
⊢ {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤

State before:
case mpr
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : {i | ∀ (x : A i), (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
x : Uprod A 𝓤
⊢ {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤
Tactic:
exact Filter.mem_of_superset h (by intro i h; simpa [val_vecCons_val_eq] using h (x.val i))
State after:
no goals

State before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : {i | ∀ (x : A i), (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
x : Uprod A 𝓤
⊢ {i | ∀ (x : A i), (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ⊆
    {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p}
Tactic:
intro i h
State after:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h✝ : {i | ∀ (x : A i), (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
x : Uprod A 𝓤
i : I
h : i ∈ {i | ∀ (x : A i), (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p}
⊢ i ∈ {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p}

State before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h✝ : {i | ∀ (x : A i), (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
x : Uprod A 𝓤
i : I
h : i ∈ {i | ∀ (x : A i), (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p}
⊢ i ∈ {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p}
Tactic:
simpa [val_vecCons_val_eq] using h (x.val i)
State after:
no goals

State before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
⊢ (∃ x, {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤) ↔
    {i | ∃ x, (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
Tactic:
constructor
State after:
case mp
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
⊢ (∃ x, {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤) →
    {i | ∃ x, (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤

case mpr
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
⊢ {i | ∃ x, (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤 →
    ∃ x, {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤

State before:
case mp
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
⊢ (∃ x, {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤) →
    {i | ∃ x, (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
Tactic:
rintro ⟨x, hx⟩
State after:
case mp.intro
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
x : Uprod A 𝓤
hx : {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤
⊢ {i | ∃ x, (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤

State before:
case mp.intro
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
x : Uprod A 𝓤
hx : {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤
⊢ {i | ∃ x, (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
Tactic:
exact Filter.mem_of_superset hx (by intro i h; use x.val i; simpa[val_vecCons_val_eq] using h)
State after:
no goals

State before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
x : Uprod A 𝓤
hx : {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤
⊢ {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ⊆
    {i | ∃ x, (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p}
Tactic:
intro i h
State after:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
x : Uprod A 𝓤
hx : {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤
i : I
h : i ∈ {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p}
⊢ i ∈ {i | ∃ x, (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p}

State before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
x : Uprod A 𝓤
hx : {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤
i : I
h : i ∈ {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p}
⊢ i ∈ {i | ∃ x, (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p}
Tactic:
use x.val i
State after:
case h
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
x : Uprod A 𝓤
hx : {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤
i : I
h : i ∈ {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p}
⊢ (Eval (s i) (x.val i :> fun x => (e x).val i) fun x => (ε x).val i) p

State before:
case h
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
x : Uprod A 𝓤
hx : {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤
i : I
h : i ∈ {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p}
⊢ (Eval (s i) (x.val i :> fun x => (e x).val i) fun x => (ε x).val i) p
Tactic:
simpa[val_vecCons_val_eq] using h
State after:
no goals

State before:
case mpr
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
⊢ {i | ∃ x, (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤 →
    ∃ x, {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤
Tactic:
intro h
State after:
case mpr
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : {i | ∃ x, (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
⊢ ∃ x, {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤

State before:
case mpr
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : {i | ∃ x, (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
⊢ ∃ x, {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤
Tactic:
let z : Uprod A 𝓤 := ⟨fun i =>
  Classical.epsilon (fun z => Eval (s i) (z :> fun x ↦ (e x).val i) (fun x ↦ (ε x).val i) p)⟩
State after:
case mpr
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : {i | ∃ x, (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
z : Uprod A 𝓤 :=
  { val := fun i => Classical.epsilon fun z => (Eval (s i) (z :> fun x => (e x).val i) fun x => (ε x).val i) p }
⊢ ∃ x, {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤

State before:
case mpr
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : {i | ∃ x, (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
z : Uprod A 𝓤 :=
  { val := fun i => Classical.epsilon fun z => (Eval (s i) (z :> fun x => (e x).val i) fun x => (ε x).val i) p }
⊢ ∃ x, {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤
Tactic:
use z
State after:
case h
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : {i | ∃ x, (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
z : Uprod A 𝓤 :=
  { val := fun i => Classical.epsilon fun z => (Eval (s i) (z :> fun x => (e x).val i) fun x => (ε x).val i) p }
⊢ {i | (Eval (s i) (fun x => ((z :> e) x).val i) fun x => (ε x).val i) p} ∈ 𝓤

State before:
case h
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : {i | ∃ x, (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
z : Uprod A 𝓤 :=
  { val := fun i => Classical.epsilon fun z => (Eval (s i) (z :> fun x => (e x).val i) fun x => (ε x).val i) p }
⊢ {i | (Eval (s i) (fun x => ((z :> e) x).val i) fun x => (ε x).val i) p} ∈ 𝓤
Tactic:
exact Filter.mem_of_superset h (by
  intro i; rintro ⟨x, hx⟩
  have : Eval (s i) (z.val i :> fun x ↦ (e x).val i) (fun x ↦ (ε x).val i) p :=
    Classical.epsilon_spec (p := fun z => Eval (s i) (z :> fun x ↦ (e x).val i) _ p) ⟨x, hx⟩
  rw[val_vecCons_val_eq] at this; exact this)
State after:
no goals

State before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : {i | ∃ x, (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
z : Uprod A 𝓤 :=
  { val := fun i => Classical.epsilon fun z => (Eval (s i) (z :> fun x => (e x).val i) fun x => (ε x).val i) p }
⊢ {i | ∃ x, (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ⊆
    {i | (Eval (s i) (fun x => ((z :> e) x).val i) fun x => (ε x).val i) p}
Tactic:
intro i
State after:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : {i | ∃ x, (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
z : Uprod A 𝓤 :=
  { val := fun i => Classical.epsilon fun z => (Eval (s i) (z :> fun x => (e x).val i) fun x => (ε x).val i) p }
i : I
⊢ i ∈ {i | ∃ x, (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} →
    i ∈ {i | (Eval (s i) (fun x => ((z :> e) x).val i) fun x => (ε x).val i) p}

State before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : {i | ∃ x, (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
z : Uprod A 𝓤 :=
  { val := fun i => Classical.epsilon fun z => (Eval (s i) (z :> fun x => (e x).val i) fun x => (ε x).val i) p }
i : I
⊢ i ∈ {i | ∃ x, (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} →
    i ∈ {i | (Eval (s i) (fun x => ((z :> e) x).val i) fun x => (ε x).val i) p}
Tactic:
rintro ⟨x, hx⟩
State after:
case intro
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : {i | ∃ x, (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
z : Uprod A 𝓤 :=
  { val := fun i => Classical.epsilon fun z => (Eval (s i) (z :> fun x => (e x).val i) fun x => (ε x).val i) p }
i : I
x : A i
hx : (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p
⊢ i ∈ {i | (Eval (s i) (fun x => ((z :> e) x).val i) fun x => (ε x).val i) p}

State before:
case intro
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : {i | ∃ x, (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
z : Uprod A 𝓤 :=
  { val := fun i => Classical.epsilon fun z => (Eval (s i) (z :> fun x => (e x).val i) fun x => (ε x).val i) p }
i : I
x : A i
hx : (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p
⊢ i ∈ {i | (Eval (s i) (fun x => ((z :> e) x).val i) fun x => (ε x).val i) p}
Tactic:
have : Eval (s i) (z.val i :> fun x ↦ (e x).val i) (fun x ↦ (ε x).val i) p :=
  Classical.epsilon_spec (p := fun z => Eval (s i) (z :> fun x ↦ (e x).val i) _ p) ⟨x, hx⟩
State after:
case intro
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : {i | ∃ x, (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
z : Uprod A 𝓤 :=
  { val := fun i => Classical.epsilon fun z => (Eval (s i) (z :> fun x => (e x).val i) fun x => (ε x).val i) p }
i : I
x : A i
hx : (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p
this : (Eval (s i) (z.val i :> fun x => (e x).val i) fun x => (ε x).val i) p
⊢ i ∈ {i | (Eval (s i) (fun x => ((z :> e) x).val i) fun x => (ε x).val i) p}

State before:
case intro
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : {i | ∃ x, (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
z : Uprod A 𝓤 :=
  { val := fun i => Classical.epsilon fun z => (Eval (s i) (z :> fun x => (e x).val i) fun x => (ε x).val i) p }
i : I
x : A i
hx : (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p
this : (Eval (s i) (z.val i :> fun x => (e x).val i) fun x => (ε x).val i) p
⊢ i ∈ {i | (Eval (s i) (fun x => ((z :> e) x).val i) fun x => (ε x).val i) p}
Tactic:
rw[val_vecCons_val_eq] at this
State after:
case intro
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : {i | ∃ x, (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
z : Uprod A 𝓤 :=
  { val := fun i => Classical.epsilon fun z => (Eval (s i) (z :> fun x => (e x).val i) fun x => (ε x).val i) p }
i : I
x : A i
hx : (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p
this : (Eval (s i) (fun x => ((z :> fun x => e x) x).val i) fun x => (ε x).val i) p
⊢ i ∈ {i | (Eval (s i) (fun x => ((z :> e) x).val i) fun x => (ε x).val i) p}

State before:
case intro
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : {i | ∃ x, (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
z : Uprod A 𝓤 :=
  { val := fun i => Classical.epsilon fun z => (Eval (s i) (z :> fun x => (e x).val i) fun x => (ε x).val i) p }
i : I
x : A i
hx : (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p
this : (Eval (s i) (fun x => ((z :> fun x => e x) x).val i) fun x => (ε x).val i) p
⊢ i ∈ {i | (Eval (s i) (fun x => ((z :> e) x).val i) fun x => (ε x).val i) p}
Tactic:
exact this
State after:
no goals