internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.complete
Proof state before:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
τ : Semiformula L Empty 0
hτ : τ ∈ u
⊢ ∃ a, (∃ a_1, ∃ (ha : a_1 ∈ u), toSubLanguageFinsetSelf ha = a) ∧ (lMap L.ofSubLanguage) a = τ
Tactic:
exact ⟨toSubLanguageFinsetSelf hτ, ⟨τ, hτ, rfl⟩, Semiformula.lMap_toSubLanguageFinsetSelf hτ⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.complete
Proof state before:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
⊢ ¬Satisfiable ↑u'
Tactic:
intro h
Proof state after:
L : Language
T : Theory L
σ : Sentence L
h✝ : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
h : Satisfiable ↑u'
⊢ False
Theorem: LO.FirstOrder.complete
Proof state before:
L : Language
T : Theory L
σ : Sentence L
h✝ : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
h : Satisfiable ↑u'
⊢ False
Tactic:
have : Satisfiable (u : Theory L) := by
  rw[←image_u']
  simpa using (satisfiable_lMap L.ofSubLanguage (fun k ↦ Subtype.val_injective) (fun _ ↦ Subtype.val_injective) h)
Proof state after:
L : Language
T : Theory L
σ : Sentence L
h✝ : T ⊨ σ
this✝² : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝¹ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this✝ : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
h : Satisfiable ↑u'
this : Satisfiable ↑u
⊢ False
Theorem: LO.FirstOrder.complete
Proof state before:
L : Language
T : Theory L
σ : Sentence L
h✝ : T ⊨ σ
this✝² : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝¹ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this✝ : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
h : Satisfiable ↑u'
this : Satisfiable ↑u
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.complete
Proof state before:
L : Language
T : Theory L
σ : Sentence L
h✝ : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
h : Satisfiable ↑u'
⊢ Satisfiable ↑u
Tactic:
rw[←image_u']
Proof state after:
L : Language
T : Theory L
σ : Sentence L
h✝ : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
h : Satisfiable ↑u'
⊢ Satisfiable ↑(Finset.image (⇑(lMap L.ofSubLanguage)) u')
Theorem: LO.FirstOrder.complete
Proof state before:
L : Language
T : Theory L
σ : Sentence L
h✝ : T ⊨ σ
this✝¹ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
h : Satisfiable ↑u'
⊢ Satisfiable ↑(Finset.image (⇑(lMap L.ofSubLanguage)) u')
Tactic:
simpa using (satisfiable_lMap L.ofSubLanguage (fun k ↦ Subtype.val_injective) (fun _ ↦ Subtype.val_injective) h)
Proof state after:
no goals
Theorem: LO.FirstOrder.complete
Proof state before:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝³ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝² : (k : ℕ) → Encodable ((languageFinset u).Func k)
this✝¹ : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
this✝ : ¬Satisfiable ↑u'
this : System.Inconsistent ↑u'
⊢ System.Inconsistent ↑u
Tactic:
rw[←image_u']
Proof state after:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝³ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝² : (k : ℕ) → Encodable ((languageFinset u).Func k)
this✝¹ : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
this✝ : ¬Satisfiable ↑u'
this : System.Inconsistent ↑u'
⊢ System.Inconsistent ↑(Finset.image (⇑(lMap L.ofSubLanguage)) u')
Theorem: LO.FirstOrder.complete
Proof state before:
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝³ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝² : (k : ℕ) → Encodable ((languageFinset u).Func k)
this✝¹ : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
this✝ : ¬Satisfiable ↑u'
this : System.Inconsistent ↑u'
⊢ System.Inconsistent ↑(Finset.image (⇑(lMap L.ofSubLanguage)) u')
Tactic:
simpa using System.inconsistent_lMap L.ofSubLanguage this
Proof state after:
no goals
Theorem: LO.FirstOrder.satisfiable_of_consistent
Proof state before:
L : Language
T : Theory L
h : System.Consistent T
⊢ Semantics.Satisfiable (Struc L) T
Tactic:
let ⟨M, _, _, h⟩ := satisfiable_iff.mp (satisfiable_of_consistent' h)
Proof state after:
L : Language
T : Theory L
h✝ : System.Consistent T
M : Type u
w✝¹ : Nonempty M
w✝ : Structure L M
h : M ⊧ₘ* T
⊢ Semantics.Satisfiable (Struc L) T
Theorem: LO.FirstOrder.satisfiable_of_consistent
Proof state before:
L : Language
T : Theory L
h✝ : System.Consistent T
M : Type u
w✝¹ : Nonempty M
w✝ : Structure L M
h : M ⊧ₘ* T
⊢ Semantics.Satisfiable (Struc L) T
Tactic:
exact satisfiable_iff.mpr ⟨ULift.{w} M, inferInstance, inferInstance, ((uLift_elementaryEquiv L M).modelsTheory).mpr h⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.satidfiable_iff_satisfiable
Proof state before:
L : Language
T : Theory L
⊢ Semantics.Satisfiable (Struc L) T ↔ Satisfiable T
Tactic:
simp [satisfiable_iff_consistent'.{u, w}, satisfiable_iff_consistent]
Proof state after:
no goals
Theorem: LO.FirstOrder.consequence_iff_consequence
Proof state before:
L : Language
T : Theory L
σ : Sentence L
⊢ T ⊨[Struc L] σ ↔ T ⊨ σ
Tactic:
simp [Semantics.consequence_iff_not_satisfiable, satidfiable_iff_satisfiable.{u, w}]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_func₀
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
f : L.Func 0
v : Fin 0 → Semiterm L μ n
⊢ val s e ε (func f v) = Structure.func f ![]
Tactic:
simp [val_func, Matrix.empty_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_func₁
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
f : L.Func 1
t : Semiterm L μ n
⊢ val s e ε (func f ![t]) = Structure.func f ![val s e ε t]
Tactic:
simp [val_func]
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
f : L.Func 1
t : Semiterm L μ n
⊢ (Structure.func f fun i => val s e ε t) = Structure.func f ![val s e ε t]
Theorem: LO.FirstOrder.Semiterm.val_func₁
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
f : L.Func 1
t : Semiterm L μ n
⊢ (Structure.func f fun i => val s e ε t) = Structure.func f ![val s e ε t]
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
f : L.Func 1
t : Semiterm L μ n
⊢ (fun i => val s e ε t) = ![val s e ε t]
Theorem: LO.FirstOrder.Semiterm.val_func₁
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
f : L.Func 1
t : Semiterm L μ n
⊢ (fun i => val s e ε t) = ![val s e ε t]
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
f : L.Func 1
t : Semiterm L μ n
i : Fin 1
⊢ val s e ε t = ![val s e ε t] i
Theorem: LO.FirstOrder.Semiterm.val_func₁
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
f : L.Func 1
t : Semiterm L μ n
i : Fin 1
⊢ val s e ε t = ![val s e ε t] i
Tactic:
cases' i using Fin.cases with i <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_func₂
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
f : L.Func 2
t u : Semiterm L μ n
⊢ val s e ε (func f ![t, u]) = Structure.func f ![val s e ε t, val s e ε u]
Tactic:
simp [val_func]
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
f : L.Func 2
t u : Semiterm L μ n
⊢ (Structure.func f fun i => val s e ε (![t, u] i)) = Structure.func f ![val s e ε t, val s e ε u]
Theorem: LO.FirstOrder.Semiterm.val_func₂
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
f : L.Func 2
t u : Semiterm L μ n
⊢ (Structure.func f fun i => val s e ε (![t, u] i)) = Structure.func f ![val s e ε t, val s e ε u]
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
f : L.Func 2
t u : Semiterm L μ n
⊢ (fun i => val s e ε (![t, u] i)) = ![val s e ε t, val s e ε u]
Theorem: LO.FirstOrder.Semiterm.val_func₂
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
f : L.Func 2
t u : Semiterm L μ n
⊢ (fun i => val s e ε (![t, u] i)) = ![val s e ε t, val s e ε u]
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
f : L.Func 2
t u : Semiterm L μ n
i : Fin 2
⊢ val s e ε (![t, u] i) = ![val s e ε t, val s e ε u] i
Theorem: LO.FirstOrder.Semiterm.val_func₂
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
f : L.Func 2
t u : Semiterm L μ n
i : Fin 2
⊢ val s e ε (![t, u] i) = ![val s e ε t, val s e ε u] i
Tactic:
cases' i using Fin.cases with i <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_rew
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
ω : Rew L μ₁ n₁ μ₂ n₂
t : Semiterm L μ₁ n₁
⊢ val s e₂ ε₂ (ω t) = val s (val s e₂ ε₂ ∘ ⇑ω ∘ bvar) (val s e₂ ε₂ ∘ ⇑ω ∘ fvar) t
Tactic:
induction t <;> simp [*, Rew.func, val_func]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_rewrite
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
f : μ₁ → Semiterm L μ₂ n
t : Semiterm L μ₁ n
⊢ val s e ε₂ ((Rew.rewrite f) t) = val s e (fun x => val s e ε₂ (f x)) 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
f : μ₁ → Semiterm L μ₂ n
t : Semiterm L μ₁ n
⊢ val s (val s e ε₂ ∘ ⇑(Rew.rewrite f) ∘ bvar) (val s e ε₂ ∘ ⇑(Rew.rewrite f) ∘ fvar) t =
    val s e (fun x => val s e ε₂ (f x)) t
Theorem: LO.FirstOrder.Semiterm.val_rewrite
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
f : μ₁ → Semiterm L μ₂ n
t : Semiterm L μ₁ n
⊢ val s (val s e ε₂ ∘ ⇑(Rew.rewrite f) ∘ bvar) (val s e ε₂ ∘ ⇑(Rew.rewrite f) ∘ fvar) t =
    val s e (fun x => val s e ε₂ (f x)) t
Tactic:
congr
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_rewriteMap
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
f : μ₁ → μ₂
t : Semiterm L μ₁ n
⊢ val s e ε₂ ((Rew.rewriteMap f) t) = val s e (fun x => ε₂ (f x)) 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
f : μ₁ → μ₂
t : Semiterm L μ₁ n
⊢ val s (val s e ε₂ ∘ ⇑(Rew.rewriteMap f) ∘ bvar) (val s e ε₂ ∘ ⇑(Rew.rewriteMap f) ∘ fvar) t =
    val s e (fun x => ε₂ (f x)) t
Theorem: LO.FirstOrder.Semiterm.val_rewriteMap
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
f : μ₁ → μ₂
t : Semiterm L μ₁ n
⊢ val s (val s e ε₂ ∘ ⇑(Rew.rewriteMap f) ∘ bvar) (val s e ε₂ ∘ ⇑(Rew.rewriteMap f) ∘ fvar) t =
    val s e (fun x => ε₂ (f x)) t
Tactic:
congr
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_substs
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
w : Fin n₁ → Semiterm L μ n₂
t : Semiterm L μ n₁
⊢ val s e₂ ε ((Rew.substs w) t) = val s (fun x => val s e₂ ε (w x)) ε 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
w : Fin n₁ → Semiterm L μ n₂
t : Semiterm L μ n₁
⊢ val s (val s e₂ ε ∘ ⇑(Rew.substs w) ∘ bvar) (val s e₂ ε ∘ ⇑(Rew.substs w) ∘ fvar) t =
    val s (fun x => val s e₂ ε (w x)) ε t
Theorem: LO.FirstOrder.Semiterm.val_substs
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
w : Fin n₁ → Semiterm L μ n₂
t : Semiterm L μ n₁
⊢ val s (val s e₂ ε ∘ ⇑(Rew.substs w) ∘ bvar) (val s e₂ ε ∘ ⇑(Rew.substs w) ∘ fvar) t =
    val s (fun x => val s e₂ ε (w x)) ε t
Tactic:
congr
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_bShift
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
a : M
t : Semiterm L μ n
⊢ val s (a :> e) ε (Rew.bShift t) = val s e ε t
Tactic:
simp [val_rew, Function.comp]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_bShift'
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 + 1) → M
t : Semiterm L μ n
⊢ val s e ε (Rew.bShift t) = val s (fun x => e x.succ) ε t
Tactic:
simp [val_rew, Function.comp]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_emb
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
o : Type v'
i : IsEmpty o
t : Semiterm L o n
⊢ val s e ε (Rew.emb t) = val s e (fun a => i.elim 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
o : Type v'
i : IsEmpty o
t : Semiterm L o n
⊢ val s (val s e ε ∘ ⇑Rew.emb ∘ bvar) (val s e ε ∘ ⇑Rew.emb ∘ fvar) t = val s e (fun a => i.elim a) t
Theorem: LO.FirstOrder.Semiterm.val_emb
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
o : Type v'
i : IsEmpty o
t : Semiterm L o n
⊢ val s (val s e ε ∘ ⇑Rew.emb ∘ bvar) (val s e ε ∘ ⇑Rew.emb ∘ fvar) t = val s e (fun a => i.elim a) 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
o : Type v'
i : IsEmpty o
t : Semiterm L o n
⊢ val s e ε ∘ ⇑Rew.emb ∘ fvar = fun a => i.elim a
Theorem: LO.FirstOrder.Semiterm.val_emb
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
o : Type v'
i : IsEmpty o
t : Semiterm L o n
⊢ val s e ε ∘ ⇑Rew.emb ∘ fvar = fun a => i.elim a
Tactic:
{ funext x; exact i.elim' x }
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_emb
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
o : Type v'
i : IsEmpty o
t : Semiterm L o n
⊢ val s e ε ∘ ⇑Rew.emb ∘ fvar = fun a => i.elim a
Tactic:
funext x
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
o : Type v'
i : IsEmpty o
t : Semiterm L o n
x : o
⊢ (val s e ε ∘ ⇑Rew.emb ∘ fvar) x = i.elim x
Theorem: LO.FirstOrder.Semiterm.val_emb
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
o : Type v'
i : IsEmpty o
t : Semiterm L o n
x : o
⊢ (val s e ε ∘ ⇑Rew.emb ∘ fvar) x = i.elim x
Tactic:
exact i.elim' x
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_castLE
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
h : n₁ ≤ n₂
t : Semiterm L μ n₁
⊢ val s e₂ ε ((Rew.castLE h) t) = val s (fun x => e₂ (Fin.castLE h x)) ε 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
h : n₁ ≤ n₂
t : Semiterm L μ n₁
⊢ val s (val s e₂ ε ∘ ⇑(Rew.castLE h) ∘ bvar) (val s e₂ ε ∘ ⇑(Rew.castLE h) ∘ fvar) t =
    val s (fun x => e₂ (Fin.castLE h x)) ε t
Theorem: LO.FirstOrder.Semiterm.val_castLE
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
h : n₁ ≤ n₂
t : Semiterm L μ n₁
⊢ val s (val s e₂ ε ∘ ⇑(Rew.castLE h) ∘ bvar) (val s e₂ ε ∘ ⇑(Rew.castLE h) ∘ fvar) t =
    val s (fun x => e₂ (Fin.castLE h x)) ε t
Tactic:
congr
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_embSubsts
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
k : ℕ
w : Fin k → Semiterm L μ n
t : Semiterm L Empty k
⊢ val s e ε ((Rew.embSubsts w) t) = valb s (fun x => val s e ε (w x)) t
Tactic:
simp [val_rew, Empty.eq_elim]
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
k : ℕ
w : Fin k → Semiterm L μ n
t : Semiterm L Empty k
⊢ val s (val s e ε ∘ ⇑(Rew.embSubsts w) ∘ bvar) Empty.elim t = valb s (fun x => val s e ε (w x)) t
Theorem: LO.FirstOrder.Semiterm.val_embSubsts
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
k : ℕ
w : Fin k → Semiterm L μ n
t : Semiterm L Empty k
⊢ val s (val s e ε ∘ ⇑(Rew.embSubsts w) ∘ bvar) Empty.elim t = valb s (fun x => val s e ε (w x)) t
Tactic:
congr
Proof state after:
no goals
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
⊢ valb s e (Rew.toS t) = val 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 (Fin n) 0
⊢ val s ![] (val s e Empty.elim ∘ ⇑Rew.toS ∘ fvar) t = val s ![] e t