internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof 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
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, (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
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, (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 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)⟩
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, (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} ∈ 𝓤
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, (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
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 𝓤
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} ∈ 𝓤
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof 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)
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, (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
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, (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}
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, (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⟩
Proof 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}
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof 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⟩
Proof 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}
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof 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
Proof 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}
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.val_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
e : Fin n → Uprod A 𝓤
ε : μ → Uprod A 𝓤
p : Formula L μ
⊢ (Evalfm (Uprod A 𝓤) ε) p ↔ {i | (Evalf (s i) fun x => (ε x).val i) p} ∈ 𝓤
Tactic:
simp[Evalf, eval_Uprod, Matrix.empty_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.models_Uprod
Proof state before:
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
inst✝¹ : Nonempty I
inst✝ : ∀ (i : I), Nonempty (A i)
σ : Sentence L
⊢ Uprod A 𝓤 ⊧ₘ σ ↔ {i | A i ⊧ₘ σ} ∈ 𝓤
Tactic:
simp[models_def, Semiformula.val_Uprod, Empty.eq_elim]
Proof state after:
no goals
Theorem: LO.FirstOrder.ultrafilter_exists
Proof state before:
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
⊢ ∀ (T_1 : Finset (Set (FinSubtheory T))), ↑T_1 ⊆ Semiformula.domain A '' T → (⋂₀ ↑T_1).Nonempty
Tactic:
haveI : DecidableEq (Set (FinSubtheory T)) := fun _ _ => Classical.propDecidable _
Proof state after:
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : DecidableEq (Set (FinSubtheory T))
⊢ ∀ (T_1 : Finset (Set (FinSubtheory T))), ↑T_1 ⊆ Semiformula.domain A '' T → (⋂₀ ↑T_1).Nonempty
Theorem: LO.FirstOrder.ultrafilter_exists
Proof state before:
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : DecidableEq (Set (FinSubtheory T))
⊢ ∀ (T_1 : Finset (Set (FinSubtheory T))), ↑T_1 ⊆ Semiformula.domain A '' T → (⋂₀ ↑T_1).Nonempty
Tactic:
simp[Finset.subset_image_iff, Semiformula.domain]
Proof state after:
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : DecidableEq (Set (FinSubtheory T))
⊢ ∀ (a : Finset (Sentence L)), ↑a ⊆ T → ∃ a_2, ∃ (h : ↑a_2 ⊆ T), ∀ a_3 ∈ a, A ⟨a_2, ⋯⟩ ⊧ₘ a_3
Theorem: LO.FirstOrder.ultrafilter_exists
Proof state before:
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : DecidableEq (Set (FinSubtheory T))
⊢ ∀ (a : Finset (Sentence L)), ↑a ⊆ T → ∃ a_2, ∃ (h : ↑a_2 ⊆ T), ∀ a_3 ∈ a, A ⟨a_2, ⋯⟩ ⊧ₘ a_3
Tactic:
intro t ht
Proof state after:
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : DecidableEq (Set (FinSubtheory T))
t : Finset (Sentence L)
ht : ↑t ⊆ T
⊢ ∃ a, ∃ (h : ↑a ⊆ T), ∀ a_1 ∈ t, A ⟨a, ⋯⟩ ⊧ₘ a_1
Theorem: LO.FirstOrder.ultrafilter_exists
Proof state before:
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : DecidableEq (Set (FinSubtheory T))
t : Finset (Sentence L)
ht : ↑t ⊆ T
⊢ ∃ a, ∃ (h : ↑a ⊆ T), ∀ a_1 ∈ t, A ⟨a, ⋯⟩ ⊧ₘ a_1
Tactic:
use t
Proof state after:
case h
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : DecidableEq (Set (FinSubtheory T))
t : Finset (Sentence L)
ht : ↑t ⊆ T
⊢ ∃ (h : ↑t ⊆ T), ∀ a ∈ t, A ⟨t, ⋯⟩ ⊧ₘ a
Theorem: LO.FirstOrder.ultrafilter_exists
Proof state before:
case h
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : DecidableEq (Set (FinSubtheory T))
t : Finset (Sentence L)
ht : ↑t ⊆ T
⊢ ∃ (h : ↑t ⊆ T), ∀ a ∈ t, A ⟨t, ⋯⟩ ⊧ₘ a
Tactic:
use ht
Proof state after:
case h
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : DecidableEq (Set (FinSubtheory T))
t : Finset (Sentence L)
ht : ↑t ⊆ T
⊢ ∀ a ∈ t, A ⟨t, ⋯⟩ ⊧ₘ a
Theorem: LO.FirstOrder.ultrafilter_exists
Proof state before:
case h
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : DecidableEq (Set (FinSubtheory T))
t : Finset (Sentence L)
ht : ↑t ⊆ T
⊢ ∀ a ∈ t, A ⟨t, ⋯⟩ ⊧ₘ a
Tactic:
intro σ hσ
Proof state after:
case h
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : DecidableEq (Set (FinSubtheory T))
t : Finset (Sentence L)
ht : ↑t ⊆ T
σ : Sentence L
hσ : σ ∈ t
⊢ A ⟨t, ⋯⟩ ⊧ₘ σ
Theorem: LO.FirstOrder.ultrafilter_exists
Proof state before:
case h
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : DecidableEq (Set (FinSubtheory T))
t : Finset (Sentence L)
ht : ↑t ⊆ T
σ : Sentence L
hσ : σ ∈ t
⊢ A ⟨t, ⋯⟩ ⊧ₘ σ
Tactic:
exact (H ⟨t, ht⟩).RealizeSet hσ
Proof state after:
no goals
Theorem: LO.FirstOrder.compactness_aux
Proof state before:
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
⊢ Satisfiable T ↔ ∀ (i : FinSubtheory T), Satisfiable ↑↑i
Tactic:
constructor
Proof state after:
case mp
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
⊢ Satisfiable T → ∀ (i : FinSubtheory T), Satisfiable ↑↑i

case mpr
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
⊢ (∀ (i : FinSubtheory T), Satisfiable ↑↑i) → Satisfiable T
Theorem: LO.FirstOrder.compactness_aux
Proof state before:
case mp
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
⊢ Satisfiable T → ∀ (i : FinSubtheory T), Satisfiable ↑↑i
Tactic:
rintro h ⟨t, ht⟩
Proof state after:
case mp.mk
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
h : Satisfiable T
t : Finset (Sentence L)
ht : ↑t ⊆ T
⊢ Satisfiable ↑↑⟨t, ht⟩
Theorem: LO.FirstOrder.compactness_aux
Proof state before:
case mp.mk
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
h : Satisfiable T
t : Finset (Sentence L)
ht : ↑t ⊆ T
⊢ Satisfiable ↑↑⟨t, ht⟩
Tactic:
exact Semantics.Satisfiable.of_subset h ht
Proof state after:
no goals
Theorem: LO.FirstOrder.compactness_aux
Proof state before:
case mpr
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
⊢ (∀ (i : FinSubtheory T), Satisfiable ↑↑i) → Satisfiable T
Tactic:
intro h
Proof state after:
case mpr
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
⊢ Satisfiable T
Theorem: LO.FirstOrder.compactness_aux
Proof state before:
case mpr
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
⊢ Satisfiable T
Tactic:
have : ∀ i : FinSubtheory T, ∃ (M : Type u) (_ : Nonempty M) (_ : Structure L M), M ⊧ₘ* (i.val : Theory L) :=
  by intro i; exact satisfiable_iff.mp (h i)
Proof state after:
case mpr
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
this : ∀ (i : FinSubtheory T), ∃ M, ∃ (x : Nonempty M), ∃ x_1, M ⊧ₘ* ↑↑i
⊢ Satisfiable T
Theorem: LO.FirstOrder.compactness_aux
Proof state before:
case mpr
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
this : ∀ (i : FinSubtheory T), ∃ M, ∃ (x : Nonempty M), ∃ x_1, M ⊧ₘ* ↑↑i
⊢ Satisfiable T
Tactic:
choose A si s hA using this
Proof state after:
case mpr
L : Language
T : Theory L
A✝ : FinSubtheory T → Type u
s✝ : (i : FinSubtheory T) → Structure L (A✝ i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
A : FinSubtheory T → Type u
si : ∀ (i : FinSubtheory T), Nonempty (A i)
s : (i : FinSubtheory T) → Structure L (A i)
hA : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
⊢ Satisfiable T
Theorem: LO.FirstOrder.compactness_aux
Proof state before:
case mpr
L : Language
T : Theory L
A✝ : FinSubtheory T → Type u
s✝ : (i : FinSubtheory T) → Structure L (A✝ i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
A : FinSubtheory T → Type u
si : ∀ (i : FinSubtheory T), Nonempty (A i)
s : (i : FinSubtheory T) → Structure L (A i)
hA : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
⊢ Satisfiable T
Tactic:
have : ∃ 𝓤 : Ultrafilter (FinSubtheory T), Set.image (Semiformula.domain A) T ⊆ 𝓤.sets := ultrafilter_exists A hA
Proof state after:
case mpr
L : Language
T : Theory L
A✝ : FinSubtheory T → Type u
s✝ : (i : FinSubtheory T) → Structure L (A✝ i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
A : FinSubtheory T → Type u
si : ∀ (i : FinSubtheory T), Nonempty (A i)
s : (i : FinSubtheory T) → Structure L (A i)
hA : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : ∃ 𝓤, Semiformula.domain A '' T ⊆ (↑𝓤).sets
⊢ Satisfiable T
Theorem: LO.FirstOrder.compactness_aux
Proof state before:
case mpr
L : Language
T : Theory L
A✝ : FinSubtheory T → Type u
s✝ : (i : FinSubtheory T) → Structure L (A✝ i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
A : FinSubtheory T → Type u
si : ∀ (i : FinSubtheory T), Nonempty (A i)
s : (i : FinSubtheory T) → Structure L (A i)
hA : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : ∃ 𝓤, Semiformula.domain A '' T ⊆ (↑𝓤).sets
⊢ Satisfiable T
Tactic:
rcases this with ⟨𝓤, h𝓤⟩
Proof state after:
case mpr.intro
L : Language
T : Theory L
A✝ : FinSubtheory T → Type u
s✝ : (i : FinSubtheory T) → Structure L (A✝ i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
A : FinSubtheory T → Type u
si : ∀ (i : FinSubtheory T), Nonempty (A i)
s : (i : FinSubtheory T) → Structure L (A i)
hA : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
𝓤 : Ultrafilter (FinSubtheory T)
h𝓤 : Semiformula.domain A '' T ⊆ (↑𝓤).sets
⊢ Satisfiable T