internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Semiformula.eval_rew_q
Proof state before:
case a.e_a.e_e.h
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂✝ : Fin n₂ → M
ε : μ → M
ε₂✝ : μ₂ → M
n₁ : ℕ
x✝ : M
e₂ : Fin n₂ → M
ε₂ : μ₂ → M
ω : Rew L μ₁ n₁ μ₂ n₂
p : Semiformula L μ₁ (n₁ + 1)
x : Fin (n₁ + 1)
⊢ Semiterm.val s (x✝ :> e₂) ε₂ (ω.q #x) = (x✝ :> fun x => Semiterm.val s e₂ ε₂ (ω #x)) x
Tactic:
cases x using Fin.cases <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_map
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e✝ : Fin n → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₂ : μ₂ → M
n₁ : ℕ
b : Fin n₁ → Fin n₂
f : μ₁ → μ₂
e : Fin n₂ → M
ε : μ₂ → M
p : Semiformula L μ₁ n₁
⊢ (Eval s e ε) ((Rew.map b f).hom p) ↔ (Eval s (e ∘ b) (ε ∘ f)) p
Tactic:
simp [eval_rew, Function.comp]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_rewrite
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
f : μ₁ → Semiterm L μ₂ n
p : Semiformula L μ₁ n
⊢ (Eval s e ε₂) ((Rew.rewrite f).hom p) ↔ (Eval s e fun x => Semiterm.val s e ε₂ (f x)) p
Tactic:
simp [eval_rew, Function.comp]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_rewriteMap
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
f : μ₁ → μ₂
p : Semiformula L μ₁ n
⊢ (Eval s e ε₂) ((Rew.rewriteMap f).hom p) ↔ (Eval s e fun x => ε₂ (f x)) p
Tactic:
simp [eval_rew, Function.comp]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_castLE
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
n₁ : ℕ
h : n₁ ≤ n₂
p : Semiformula L μ n₁
⊢ (Eval s e₂ ε) ((Rew.castLE h).hom p) ↔ (Eval s (fun x => e₂ (Fin.castLE h x)) ε) p
Tactic:
simp [eval_rew, Function.comp]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_bShift
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
x : M
p : Semiformula L μ n
⊢ (Eval s (x :> e) ε) (Rew.bShift.hom p) ↔ (Eval s e ε) p
Tactic:
simp [eval_rew, Function.comp]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_bShift'
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
e' : Fin (n + 1) → M
p : Semiformula L μ n
⊢ (Eval s e' ε) (Rew.bShift.hom p) ↔ (Eval s (fun x => e' x.succ) ε) p
Tactic:
simp [eval_rew, Function.comp]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_substs
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
k : ℕ
w : Fin k → Semiterm L μ n
p : Semiformula L μ k
⊢ (Eval s e ε) ((Rew.substs w).hom p) ↔ (Eval s (fun i => Semiterm.val s e ε (w i)) ε) p
Tactic:
simp [eval_rew, Function.comp]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_emb
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
p : Semiformula L Empty n
⊢ (Eval s e ε) (Rew.emb.hom p) ↔ (Eval s e Empty.elim) p
Tactic:
simp [eval_rew, Function.comp]
Proof state after:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
p : Semiformula L Empty n
⊢ (Eval s (fun x => e x) fun x => instIsEmptyEmpty.elim x) p ↔ (Eval s e Empty.elim) p
Theorem: LO.FirstOrder.Semiformula.eval_emb
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
p : Semiformula L Empty n
⊢ (Eval s (fun x => e x) fun x => instIsEmptyEmpty.elim x) p ↔ (Eval s e Empty.elim) p
Tactic:
apply iff_of_eq
Proof state after:
case a
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
p : Semiformula L Empty n
⊢ (Eval s (fun x => e x) fun x => instIsEmptyEmpty.elim x) p = (Eval s e Empty.elim) p
Theorem: LO.FirstOrder.Semiformula.eval_emb
Proof state before:
case a
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
p : Semiformula L Empty n
⊢ (Eval s (fun x => e x) fun x => instIsEmptyEmpty.elim x) p = (Eval s e Empty.elim) p
Tactic:
congr
Proof state after:
case a.e_a.e_ε
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
p : Semiformula L Empty n
⊢ (fun x => instIsEmptyEmpty.elim x) = Empty.elim
Theorem: LO.FirstOrder.Semiformula.eval_emb
Proof state before:
case a.e_a.e_ε
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
p : Semiformula L Empty n
⊢ (fun x => instIsEmptyEmpty.elim x) = Empty.elim
Tactic:
funext x
Proof state after:
case a.e_a.e_ε.h
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
p : Semiformula L Empty n
x : Empty
⊢ instIsEmptyEmpty.elim x = x.elim
Theorem: LO.FirstOrder.Semiformula.eval_emb
Proof state before:
case a.e_a.e_ε.h
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
p : Semiformula L Empty n
x : Empty
⊢ instIsEmptyEmpty.elim x = x.elim
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_empty
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
o : Type u_1
h : IsEmpty o
p : Formula L o
⊢ (Eval s e ε) (Rew.empty.hom p) ↔ (Eval s ![] fun a => h.elim a) p
Tactic:
simp [eval_rew, Function.comp, Matrix.empty_eq]
Proof state after:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
o : Type u_1
h : IsEmpty o
p : Formula L o
⊢ (Eval s ![] fun x => Semiterm.val s e ε (Rew.empty &x)) p ↔ (Eval s ![] fun a => h.elim a) p
Theorem: LO.FirstOrder.Semiformula.eval_empty
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
o : Type u_1
h : IsEmpty o
p : Formula L o
⊢ (Eval s ![] fun x => Semiterm.val s e ε (Rew.empty &x)) p ↔ (Eval s ![] fun a => h.elim a) p
Tactic:
apply iff_of_eq
Proof state after:
case a
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
o : Type u_1
h : IsEmpty o
p : Formula L o
⊢ (Eval s ![] fun x => Semiterm.val s e ε (Rew.empty &x)) p = (Eval s ![] fun a => h.elim a) p
Theorem: LO.FirstOrder.Semiformula.eval_empty
Proof state before:
case a
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
o : Type u_1
h : IsEmpty o
p : Formula L o
⊢ (Eval s ![] fun x => Semiterm.val s e ε (Rew.empty &x)) p = (Eval s ![] fun a => h.elim a) p
Tactic:
congr
Proof state after:
case a.e_a.e_ε
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
o : Type u_1
h : IsEmpty o
p : Formula L o
⊢ (fun x => Semiterm.val s e ε (Rew.empty &x)) = fun a => h.elim a
Theorem: LO.FirstOrder.Semiformula.eval_empty
Proof state before:
case a.e_a.e_ε
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
o : Type u_1
h : IsEmpty o
p : Formula L o
⊢ (fun x => Semiterm.val s e ε (Rew.empty &x)) = fun a => h.elim a
Tactic:
funext x
Proof state after:
case a.e_a.e_ε.h
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
o : Type u_1
h : IsEmpty o
p : Formula L o
x : o
⊢ Semiterm.val s e ε (Rew.empty &x) = h.elim x
Theorem: LO.FirstOrder.Semiformula.eval_empty
Proof state before:
case a.e_a.e_ε.h
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
o : Type u_1
h : IsEmpty o
p : Formula L o
x : o
⊢ Semiterm.val s e ε (Rew.empty &x) = h.elim x
Tactic:
exact h.elim' x
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_toS
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e✝ : Fin n → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₂ : μ₂ → M
e : Fin n → M
ε : Empty → M
p : Formula L (Fin n)
⊢ (Eval s e ε) (Rew.toS.hom p) ↔ (Eval s ![] e) p
Tactic:
simp [Rew.toS, eval_rew, Function.comp, Matrix.empty_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_embSubsts
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
k : ℕ
w : Fin k → Semiterm L μ n
σ : Semisentence L k
⊢ (Eval s e ε) ((Rew.embSubsts w).hom σ) ↔ (Evalb s fun x => Semiterm.val s e ε (w x)) σ
Tactic:
simp [eval_rew, Function.comp, Empty.eq_elim]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_free
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₂ : μ₂ → M
ε : ℕ → M
a : M
p : SyntacticSemiformula L (n + 1)
⊢ (Eval s e (a :>ₙ ε)) ((Rew.hom Rew.free) p) ↔ (Eval s (e <: a) ε) p
Tactic:
simp [eval_rew, Function.comp]
Proof state after:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₂ : μ₂ → M
ε : ℕ → M
a : M
p : SyntacticSemiformula L (n + 1)
⊢ (Eval s (fun x => Semiterm.val s e (a :>ₙ ε) (Rew.free #x)) fun x => ε x) p ↔ (Eval s (e <: a) ε) p
Theorem: LO.FirstOrder.Semiformula.eval_free
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₂ : μ₂ → M
ε : ℕ → M
a : M
p : SyntacticSemiformula L (n + 1)
⊢ (Eval s (fun x => Semiterm.val s e (a :>ₙ ε) (Rew.free #x)) fun x => ε x) p ↔ (Eval s (e <: a) ε) p
Tactic:
apply iff_of_eq
Proof state after:
case a
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₂ : μ₂ → M
ε : ℕ → M
a : M
p : SyntacticSemiformula L (n + 1)
⊢ (Eval s (fun x => Semiterm.val s e (a :>ₙ ε) (Rew.free #x)) fun x => ε x) p = (Eval s (e <: a) ε) p
Theorem: LO.FirstOrder.Semiformula.eval_free
Proof state before:
case a
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₂ : μ₂ → M
ε : ℕ → M
a : M
p : SyntacticSemiformula L (n + 1)
⊢ (Eval s (fun x => Semiterm.val s e (a :>ₙ ε) (Rew.free #x)) fun x => ε x) p = (Eval s (e <: a) ε) p
Tactic:
congr
Proof state after:
case a.e_a.e_e
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₂ : μ₂ → M
ε : ℕ → M
a : M
p : SyntacticSemiformula L (n + 1)
⊢ (fun x => Semiterm.val s e (a :>ₙ ε) (Rew.free #x)) = e <: a
Theorem: LO.FirstOrder.Semiformula.eval_free
Proof state before:
case a.e_a.e_e
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₂ : μ₂ → M
ε : ℕ → M
a : M
p : SyntacticSemiformula L (n + 1)
⊢ (fun x => Semiterm.val s e (a :>ₙ ε) (Rew.free #x)) = e <: a
Tactic:
funext x
Proof state after:
case a.e_a.e_e.h
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₂ : μ₂ → M
ε : ℕ → M
a : M
p : SyntacticSemiformula L (n + 1)
x : Fin (n + 1)
⊢ Semiterm.val s e (a :>ₙ ε) (Rew.free #x) = (e <: a) x
Theorem: LO.FirstOrder.Semiformula.eval_free
Proof state before:
case a.e_a.e_e.h
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₂ : μ₂ → M
ε : ℕ → M
a : M
p : SyntacticSemiformula L (n + 1)
x : Fin (n + 1)
⊢ Semiterm.val s e (a :>ₙ ε) (Rew.free #x) = (e <: a) x
Tactic:
cases x using Fin.lastCases <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_shift
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₂ : μ₂ → M
ε : ℕ → M
a : M
p : SyntacticSemiformula L n
⊢ (Eval s e (a :>ₙ ε)) ((Rew.hom ⇑) p) ↔ (Eval s e ε) p
Tactic:
simp [eval_rew, Function.comp]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
p : Semiformula L μ n
h : Function.funEqOn p.fvar? ε ε'
⊢ (Eval s e ε) p ↔ (Eval s e ε') p
Tactic:
unfold fvar? at h
Proof state after:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
p : Semiformula L μ n
h : Function.funEqOn (fun x => x ∈ p.fvarList) ε ε'
⊢ (Eval s e ε) p ↔ (Eval s e ε') p
Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ ⊤.fvarList) ε ε'
⊢ (Eval s e ε) ⊤ ↔ (Eval s e ε') ⊤
Tactic:
case hverum => simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ ⊥.fvarList) ε ε'
⊢ (Eval s e ε) ⊥ ↔ (Eval s e ε') ⊥
Tactic:
case hfalsum => simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (rel r v).fvarList) ε ε'
⊢ (Eval s e ε) (rel r v) ↔ (Eval s e ε') (rel r v)
Tactic:
case hrel k r v =>
  simp [eval_rel]; apply iff_of_eq; congr
  funext i
  exact Semiterm.val_eq_of_funEqOn (v i) (fun x hx ↦ h x (by simp [fvarList]; exact ⟨i, hx⟩))
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (nrel r v).fvarList) ε ε'
⊢ (Eval s e ε) (nrel r v) ↔ (Eval s e ε') (nrel r v)
Tactic:
case hnrel k r v =>
  simp [eval_nrel]; apply iff_of_eq; congr
  funext i
  exact Semiterm.val_eq_of_funEqOn (v i) (fun x hx ↦ h x (by simp [fvarList]; exact ⟨i, hx⟩))
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
ih : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∀' p).fvarList) ε ε'
⊢ (Eval s e ε) (∀' p) ↔ (Eval s e ε') (∀' p)
Tactic:
case hall p ih =>
  simp; apply forall_congr'; intro x
  exact ih (fun x hx ↦ h _ $ by simp [fvar?]; exact hx)
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
ih : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∃' p).fvarList) ε ε'
⊢ (Eval s e ε) (∃' p) ↔ (Eval s e ε') (∃' p)
Tactic:
case hex p ih =>
  simp; apply exists_congr; intro x
  exact ih (fun x hx ↦ h _ $ by simp [fvar?]; exact hx)
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ ⊤.fvarList) ε ε'
⊢ (Eval s e ε) ⊤ ↔ (Eval s e ε') ⊤
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ ⊥.fvarList) ε ε'
⊢ (Eval s e ε) ⊥ ↔ (Eval s e ε') ⊥
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (rel r v).fvarList) ε ε'
⊢ (Eval s e ε) (rel r v) ↔ (Eval s e ε') (rel r v)
Tactic:
simp [eval_rel]
Proof state after:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (rel r v).fvarList) ε ε'
⊢ (Structure.rel r fun i => Semiterm.val s e ε (v i)) ↔ Structure.rel r fun i => Semiterm.val s e ε' (v i)
Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (rel r v).fvarList) ε ε'
⊢ (Structure.rel r fun i => Semiterm.val s e ε (v i)) ↔ Structure.rel r fun i => Semiterm.val s e ε' (v i)
Tactic:
apply iff_of_eq
Proof state after:
case a
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (rel r v).fvarList) ε ε'
⊢ (Structure.rel r fun i => Semiterm.val s e ε (v i)) = Structure.rel r fun i => Semiterm.val s e ε' (v i)
Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
case a
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (rel r v).fvarList) ε ε'
⊢ (Structure.rel r fun i => Semiterm.val s e ε (v i)) = Structure.rel r fun i => Semiterm.val s e ε' (v i)
Tactic:
congr
Proof state after:
case a.e_a
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (rel r v).fvarList) ε ε'
⊢ (fun i => Semiterm.val s e ε (v i)) = fun i => Semiterm.val s e ε' (v i)
Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
case a.e_a
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (rel r v).fvarList) ε ε'
⊢ (fun i => Semiterm.val s e ε (v i)) = fun i => Semiterm.val s e ε' (v i)
Tactic:
funext i
Proof state after:
case a.e_a.h
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (rel r v).fvarList) ε ε'
i : Fin k
⊢ Semiterm.val s e ε (v i) = Semiterm.val s e ε' (v i)
Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
case a.e_a.h
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (rel r v).fvarList) ε ε'
i : Fin k
⊢ Semiterm.val s e ε (v i) = Semiterm.val s e ε' (v i)
Tactic:
exact Semiterm.val_eq_of_funEqOn (v i) (fun x hx ↦ h x (by simp [fvarList]; exact ⟨i, hx⟩))
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (rel r v).fvarList) ε ε'
i : Fin k
x : μ
hx : (v i).fvar? x
⊢ (fun x => x ∈ (rel r v).fvarList) x
Tactic:
simp [fvarList]
Proof state after:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (rel r v).fvarList) ε ε'
i : Fin k
x : μ
hx : (v i).fvar? x
⊢ ∃ a, x ∈ (v a).fvarList
Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (rel r v).fvarList) ε ε'
i : Fin k
x : μ
hx : (v i).fvar? x
⊢ ∃ a, x ∈ (v a).fvarList
Tactic:
exact ⟨i, hx⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (nrel r v).fvarList) ε ε'
⊢ (Eval s e ε) (nrel r v) ↔ (Eval s e ε') (nrel r v)
Tactic:
simp [eval_nrel]
Proof state after:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (nrel r v).fvarList) ε ε'
⊢ (¬Structure.rel r fun i => Semiterm.val s e ε (v i)) ↔ ¬Structure.rel r fun i => Semiterm.val s e ε' (v i)