intro h x
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} ∈ 𝓤
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} ∈ 𝓤