internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Semiterm.val_toS
Proof state before:
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e✝ : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
e : Fin n → M
t : Semiterm L (Fin n) 0
⊢ val s ![] (val s e Empty.elim ∘ ⇑Rew.toS ∘ fvar) t = val s ![] e t
Tactic:
congr
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_toF
Proof state before:
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e✝ : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
e : Fin n → M
t : Semiterm L Empty n
⊢ val s ![] e (Rew.toF t) = valb s e t
Tactic:
simp [val_rew, Matrix.empty_eq]
Proof state after:
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e✝ : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
e : Fin n → M
t : Semiterm L Empty n
⊢ val s (val s ![] e ∘ ⇑Rew.toF ∘ bvar) (val s ![] e ∘ ⇑Rew.toF ∘ fvar) t = valb s e t
Theorem: LO.FirstOrder.Semiterm.val_toF
Proof state before:
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e✝ : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
e : Fin n → M
t : Semiterm L Empty n
⊢ val s (val s ![] e ∘ ⇑Rew.toF ∘ bvar) (val s ![] e ∘ ⇑Rew.toF ∘ fvar) t = valb s e t
Tactic:
congr
Proof state after:
case e_ε
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e✝ : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
e : Fin n → M
t : Semiterm L Empty n
⊢ val s ![] e ∘ ⇑Rew.toF ∘ fvar = Empty.elim
Theorem: LO.FirstOrder.Semiterm.val_toF
Proof state before:
case e_ε
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e✝ : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
e : Fin n → M
t : Semiterm L Empty n
⊢ val s ![] e ∘ ⇑Rew.toF ∘ fvar = Empty.elim
Tactic:
funext i
Proof state after:
case e_ε.h
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e✝ : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
e : Fin n → M
t : Semiterm L Empty n
i : Empty
⊢ (val s ![] e ∘ ⇑Rew.toF ∘ fvar) i = i.elim
Theorem: LO.FirstOrder.Semiterm.val_toF
Proof state before:
case e_ε.h
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e✝ : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
e : Fin n → M
t : Semiterm L Empty n
i : Empty
⊢ (val s ![] e ∘ ⇑Rew.toF ∘ fvar) i = i.elim
Tactic:
simp
Proof state after:
case e_ε.h
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e✝ : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
e : Fin n → M
t : Semiterm L Empty n
i : Empty
⊢ val s ![] e (Rew.toF &i) = i.elim
Theorem: LO.FirstOrder.Semiterm.val_toF
Proof state before:
case e_ε.h
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e✝ : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
e : Fin n → M
t : Semiterm L Empty n
i : Empty
⊢ val s ![] e (Rew.toF &i) = i.elim
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_lMap
Proof state before:
n n₁ n₂ : ℕ
L₁ : Language
L₂ : Language
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e✝¹ : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε✝¹ : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
φ✝ : L₁ →ᵥ L₂
e✝ : Fin n → M
ε✝ : μ → M
φ : L₁ →ᵥ L₂
s₂ : Structure L₂ M
e : Fin n → M
ε : μ → M
t : Semiterm L₁ μ n
⊢ val s₂ e ε (lMap φ t) = val (Structure.lMap φ s₂) e ε t
Tactic:
induction t <;> simp [*, valm, Function.comp, val_func, Semiterm.lMap_func]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_shift
Proof state before:
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε : ℕ → M
t : SyntacticSemiterm L n
⊢ val s e ε (⇑ t) = val s e (ε ∘ Nat.succ) t
Tactic:
simp [val_rew]
Proof state after:
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε : ℕ → M
t : SyntacticSemiterm L n
⊢ val s (val s e ε ∘ ⇑⇑ ∘ bvar) (val s e ε ∘ ⇑⇑ ∘ fvar) t = val s e (ε ∘ Nat.succ) t
Theorem: LO.FirstOrder.Semiterm.val_shift
Proof state before:
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε : ℕ → M
t : SyntacticSemiterm L n
⊢ val s (val s e ε ∘ ⇑⇑ ∘ bvar) (val s e ε ∘ ⇑⇑ ∘ fvar) t = val s e (ε ∘ Nat.succ) t
Tactic:
congr
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_free
Proof state before:
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε : ℕ → M
a : M
t : SyntacticSemiterm L (n + 1)
⊢ val s e (a :>ₙ ε) (Rew.free t) = val s (e <: a) ε t
Tactic:
simp [val_rew]
Proof state after:
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε : ℕ → M
a : M
t : SyntacticSemiterm L (n + 1)
⊢ val s (val s e (a :>ₙ ε) ∘ ⇑Rew.free ∘ bvar) (val s e (a :>ₙ ε) ∘ ⇑Rew.free ∘ fvar) t = val s (e <: a) ε t
Theorem: LO.FirstOrder.Semiterm.val_free
Proof state before:
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε : ℕ → M
a : M
t : SyntacticSemiterm L (n + 1)
⊢ val s (val s e (a :>ₙ ε) ∘ ⇑Rew.free ∘ bvar) (val s e (a :>ₙ ε) ∘ ⇑Rew.free ∘ fvar) t = val s (e <: a) ε t
Tactic:
congr
Proof state after:
case e_e
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε : ℕ → M
a : M
t : SyntacticSemiterm L (n + 1)
⊢ val s e (a :>ₙ ε) ∘ ⇑Rew.free ∘ bvar = e <: a
Theorem: LO.FirstOrder.Semiterm.val_free
Proof state before:
case e_e
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε : ℕ → M
a : M
t : SyntacticSemiterm L (n + 1)
⊢ val s e (a :>ₙ ε) ∘ ⇑Rew.free ∘ bvar = e <: a
Tactic:
exact funext $ Fin.lastCases (by simp) (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_free
Proof state before:
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε : ℕ → M
a : M
t : SyntacticSemiterm L (n + 1)
⊢ (val s e (a :>ₙ ε) ∘ ⇑Rew.free ∘ bvar) (Fin.last n) = (e <: a) (Fin.last n)
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_free
Proof state before:
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε : ℕ → M
a : M
t : SyntacticSemiterm L (n + 1)
⊢ ∀ (i : Fin n), (val s e (a :>ₙ ε) ∘ ⇑Rew.free ∘ bvar) i.castSucc = (e <: a) i.castSucc
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_fix
Proof state before:
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε : ℕ → M
a : M
t : SyntacticSemiterm L n
⊢ val s (e <: a) ε (Rew.fix t) = val s e (a :>ₙ ε) t
Tactic:
simp [val_rew]
Proof state after:
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε : ℕ → M
a : M
t : SyntacticSemiterm L n
⊢ val s (val s (e <: a) ε ∘ ⇑Rew.fix ∘ bvar) (val s (e <: a) ε ∘ ⇑Rew.fix ∘ fvar) t = val s e (a :>ₙ ε) t
Theorem: LO.FirstOrder.Semiterm.val_fix
Proof state before:
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε : ℕ → M
a : M
t : SyntacticSemiterm L n
⊢ val s (val s (e <: a) ε ∘ ⇑Rew.fix ∘ bvar) (val s (e <: a) ε ∘ ⇑Rew.fix ∘ fvar) t = val s e (a :>ₙ ε) t
Tactic:
congr <;> simp [Function.comp]
Proof state after:
case e_ε
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε : ℕ → M
a : M
t : SyntacticSemiterm L n
⊢ (fun x => val s (e <: a) ε (Rew.fix &x)) = a :>ₙ ε
Theorem: LO.FirstOrder.Semiterm.val_fix
Proof state before:
case e_ε
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε : ℕ → M
a : M
t : SyntacticSemiterm L n
⊢ (fun x => val s (e <: a) ε (Rew.fix &x)) = a :>ₙ ε
Tactic:
exact funext (Nat.cases (by simp) (by simp))
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_fix
Proof state before:
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε : ℕ → M
a : M
t : SyntacticSemiterm L n
⊢ val s (e <: a) ε (Rew.fix &0) = (a :>ₙ ε) 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_fix
Proof state before:
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε : ℕ → M
a : M
t : SyntacticSemiterm L n
⊢ ∀ (n_1 : ℕ), val s (e <: a) ε (Rew.fix &(n_1 + 1)) = (a :>ₙ ε) (n_1 + 1)
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_eq_of_funEqOn
Proof state before:
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε' : μ → M
t : Semiterm L μ n
h : Function.funEqOn t.fvar? ε ε'
⊢ val s e ε t = val s e ε' t
Tactic:
induction t <;> simp [val_func]
Proof state after:
case fvar
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε' : μ → M
a✝ : μ
h : Function.funEqOn (&a✝).fvar? ε ε'
⊢ ε a✝ = ε' a✝

case func
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε' : μ → M
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L μ n
a_ih✝ : ∀ (a : Fin arity✝), Function.funEqOn (a✝ a).fvar? ε ε' → val s e ε (a✝ a) = val s e ε' (a✝ a)
h : Function.funEqOn (func a✝¹ a✝).fvar? ε ε'
⊢ (Structure.func a✝¹ fun i => val s e ε (a✝ i)) = Structure.func a✝¹ fun i => val s e ε' (a✝ i)
Theorem: LO.FirstOrder.Semiterm.val_eq_of_funEqOn
Proof state before:
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε' : μ → M
x : μ
h : Function.funEqOn (&x).fvar? ε ε'
⊢ ε x = ε' x
Tactic:
case fvar x => exact h x (by simp [fvar?])
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_eq_of_funEqOn
Proof state before:
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε' : μ → M
k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ n
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? ε ε' → val s e ε (v a) = val s e ε' (v a)
h : Function.funEqOn (func f v).fvar? ε ε'
⊢ (Structure.func f fun i => val s e ε (v i)) = Structure.func f fun i => val s e ε' (v i)
Tactic:
case func k f v ih =>
  congr; funext i; exact ih i (by intro x hx; exact h x (by simp; exact ⟨i, hx⟩))
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_eq_of_funEqOn
Proof state before:
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε' : μ → M
x : μ
h : Function.funEqOn (&x).fvar? ε ε'
⊢ ε x = ε' x
Tactic:
exact h x (by simp [fvar?])
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_eq_of_funEqOn
Proof state before:
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε' : μ → M
x : μ
h : Function.funEqOn (&x).fvar? ε ε'
⊢ (&x).fvar? x
Tactic:
simp [fvar?]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_eq_of_funEqOn
Proof state before:
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε' : μ → M
k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ n
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? ε ε' → val s e ε (v a) = val s e ε' (v a)
h : Function.funEqOn (func f v).fvar? ε ε'
⊢ (Structure.func f fun i => val s e ε (v i)) = Structure.func f fun i => val s e ε' (v i)
Tactic:
congr
Proof state after:
case e_a
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε' : μ → M
k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ n
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? ε ε' → val s e ε (v a) = val s e ε' (v a)
h : Function.funEqOn (func f v).fvar? ε ε'
⊢ (fun i => val s e ε (v i)) = fun i => val s e ε' (v i)
Theorem: LO.FirstOrder.Semiterm.val_eq_of_funEqOn
Proof state before:
case e_a
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε' : μ → M
k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ n
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? ε ε' → val s e ε (v a) = val s e ε' (v a)
h : Function.funEqOn (func f v).fvar? ε ε'
⊢ (fun i => val s e ε (v i)) = fun i => val s e ε' (v i)
Tactic:
funext i
Proof state after:
case e_a.h
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε' : μ → M
k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ n
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? ε ε' → val s e ε (v a) = val s e ε' (v a)
h : Function.funEqOn (func f v).fvar? ε ε'
i : Fin k
⊢ val s e ε (v i) = val s e ε' (v i)
Theorem: LO.FirstOrder.Semiterm.val_eq_of_funEqOn
Proof state before:
case e_a.h
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε' : μ → M
k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ n
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? ε ε' → val s e ε (v a) = val s e ε' (v a)
h : Function.funEqOn (func f v).fvar? ε ε'
i : Fin k
⊢ val s e ε (v i) = val s e ε' (v i)
Tactic:
exact ih i (by intro x hx; exact h x (by simp; exact ⟨i, hx⟩))
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_eq_of_funEqOn
Proof state before:
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε' : μ → M
k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ n
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? ε ε' → val s e ε (v a) = val s e ε' (v a)
h : Function.funEqOn (func f v).fvar? ε ε'
i : Fin k
⊢ Function.funEqOn (v i).fvar? ε ε'
Tactic:
intro x hx
Proof state after:
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε' : μ → M
k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ n
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? ε ε' → val s e ε (v a) = val s e ε' (v a)
h : Function.funEqOn (func f v).fvar? ε ε'
i : Fin k
x : μ
hx : (v i).fvar? x
⊢ ε x = ε' x
Theorem: LO.FirstOrder.Semiterm.val_eq_of_funEqOn
Proof state before:
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε' : μ → M
k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ n
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? ε ε' → val s e ε (v a) = val s e ε' (v a)
h : Function.funEqOn (func f v).fvar? ε ε'
i : Fin k
x : μ
hx : (v i).fvar? x
⊢ ε x = ε' x
Tactic:
exact h x (by simp; exact ⟨i, hx⟩)
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_eq_of_funEqOn
Proof state before:
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε' : μ → M
k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ n
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? ε ε' → val s e ε (v a) = val s e ε' (v a)
h : Function.funEqOn (func f v).fvar? ε ε'
i : Fin k
x : μ
hx : (v i).fvar? x
⊢ (func f v).fvar? x
Tactic:
simp
Proof state after:
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε' : μ → M
k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ n
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? ε ε' → val s e ε (v a) = val s e ε' (v a)
h : Function.funEqOn (func f v).fvar? ε ε'
i : Fin k
x : μ
hx : (v i).fvar? x
⊢ ∃ i, x ∈ (v i).fvarList
Theorem: LO.FirstOrder.Semiterm.val_eq_of_funEqOn
Proof state before:
n n₁ n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
e : Fin n → M
e₁ : Fin n₁ → M
e₂ : Fin n₂ → M
ε : μ → M
ε₁ : μ₁ → M
ε₂ : μ₂ → M
ε' : μ → M
k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ n
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? ε ε' → val s e ε (v a) = val s e ε' (v a)
h : Function.funEqOn (func f v).fvar? ε ε'
i : Fin k
x : μ
hx : (v i).fvar? x
⊢ ∃ i, x ∈ (v i).fvarList
Tactic:
exact ⟨i, hx⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.ofEquiv_val
Proof state before:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
n : ℕ
e : Fin n → N
ε : μ → N
t : Semiterm L μ n
⊢ Semiterm.val (ofEquiv φ) e ε t = φ (Semiterm.val s (⇑φ.symm ∘ e) (⇑φ.symm ∘ ε) t)
Tactic:
induction t <;> simp [*, Semiterm.val_func, ofEquiv_func φ, Function.comp]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.EvalAux_neg
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 μ n
⊢ EvalAux s ε e (~p) = ¬EvalAux s ε e p
Tactic:
induction p using rec' <;> simp [*, EvalAux, ←neg_eq, or_iff_not_imp_left]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_rel₀
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
r : L.Rel 0
⊢ (Eval s e ε) (rel r ![]) ↔ Structure.rel r ![]
Tactic:
simp [eval_rel, Matrix.empty_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_rel₁
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
r : L.Rel 1
t : Semiterm L μ n
⊢ (Eval s e ε) (rel r ![t]) ↔ Structure.rel r ![Semiterm.val s e ε t]
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
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
r : L.Rel 1
t : Semiterm L μ n
⊢ (Structure.rel r fun i => Semiterm.val s e ε t) ↔ Structure.rel r ![Semiterm.val s e ε t]
Theorem: LO.FirstOrder.Semiformula.eval_rel₁
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
r : L.Rel 1
t : Semiterm L μ n
⊢ (Structure.rel r fun i => Semiterm.val s e ε t) ↔ Structure.rel r ![Semiterm.val s e ε t]
Tactic:
apply 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
r : L.Rel 1
t : Semiterm L μ n
⊢ (Structure.rel r fun i => Semiterm.val s e ε t) = Structure.rel r ![Semiterm.val s e ε t]
Theorem: LO.FirstOrder.Semiformula.eval_rel₁
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
r : L.Rel 1
t : Semiterm L μ n
⊢ (Structure.rel r fun i => Semiterm.val s e ε t) = Structure.rel r ![Semiterm.val s e ε t]
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
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
r : L.Rel 1
t : Semiterm L μ n
⊢ (fun i => Semiterm.val s e ε t) = ![Semiterm.val s e ε t]
Theorem: LO.FirstOrder.Semiformula.eval_rel₁
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
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
r : L.Rel 1
t : Semiterm L μ n
⊢ (fun i => Semiterm.val s e ε t) = ![Semiterm.val s e ε t]
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
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
r : L.Rel 1
t : Semiterm L μ n
i : Fin 1
⊢ Semiterm.val s e ε t = ![Semiterm.val s e ε t] i
Theorem: LO.FirstOrder.Semiformula.eval_rel₁
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
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
r : L.Rel 1
t : Semiterm L μ n
i : Fin 1
⊢ Semiterm.val s e ε t = ![Semiterm.val s e ε t] i
Tactic:
cases' i using Fin.cases with i <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_rel₂
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
r : L.Rel 2
t₁ t₂ : Semiterm L μ n
⊢ (Eval s e ε) (rel r ![t₁, t₂]) ↔ Structure.rel r ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂]
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
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
r : L.Rel 2
t₁ t₂ : Semiterm L μ n
⊢ (Structure.rel r fun i => Semiterm.val s e ε (![t₁, t₂] i)) ↔
    Structure.rel r ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂]
Theorem: LO.FirstOrder.Semiformula.eval_rel₂
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
r : L.Rel 2
t₁ t₂ : Semiterm L μ n
⊢ (Structure.rel r fun i => Semiterm.val s e ε (![t₁, t₂] i)) ↔
    Structure.rel r ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂]
Tactic:
apply 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
r : L.Rel 2
t₁ t₂ : Semiterm L μ n
⊢ (Structure.rel r fun i => Semiterm.val s e ε (![t₁, t₂] i)) =
    Structure.rel r ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂]