internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof 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)⟩
Proof 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} ∈ 𝓤
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof 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)
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof 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
Proof 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
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof 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ι
Proof 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
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof 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
Proof 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
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof 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⟩
Proof 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
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof 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]
Proof 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
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof 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ι
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof 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
Proof 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} ∈ 𝓤
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof 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))
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof 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
Proof 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}
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof 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)
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof 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
Proof 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} ∈ 𝓤
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof 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⟩
Proof 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} ∈ 𝓤
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof 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)
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof 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
Proof 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}
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof 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
Proof 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