internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Interpretation.func_existsUnique
Proof state before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
k : ℕ
f : L'.Func k
v : Fin k → ι.Sub M
this : ∃! y, ι.Dom y ∧ (Evalbm M (y :> fun i => ↑(v i))) (ι.func f)
y : M
hy : ι.Dom y
Hy : (Evalbm M (y :> fun i => ↑(v i))) (ι.func f)
⊢ ∀ (y_1 : ι.Sub M), (Evalbm M (↑y_1 :> fun i => ↑(v i))) (ι.func f) → y_1 = ⟨y, hy⟩
Tactic:
simp
Proof state after:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
k : ℕ
f : L'.Func k
v : Fin k → ι.Sub M
this : ∃! y, ι.Dom y ∧ (Evalbm M (y :> fun i => ↑(v i))) (ι.func f)
y : M
hy : ι.Dom y
Hy : (Evalbm M (y :> fun i => ↑(v i))) (ι.func f)
⊢ ∀ (a : M), ι.Dom a → (Evalbm M (a :> fun i => ↑(v i))) (ι.func f) → a = y
Theorem: LO.FirstOrder.Interpretation.func_existsUnique
Proof state before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
k : ℕ
f : L'.Func k
v : Fin k → ι.Sub M
this : ∃! y, ι.Dom y ∧ (Evalbm M (y :> fun i => ↑(v i))) (ι.func f)
y : M
hy : ι.Dom y
Hy : (Evalbm M (y :> fun i => ↑(v i))) (ι.func f)
⊢ ∀ (a : M), ι.Dom a → (Evalbm M (a :> fun i => ↑(v i))) (ι.func f) → a = y
Tactic:
intro z hz Hz
Proof state after:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
k : ℕ
f : L'.Func k
v : Fin k → ι.Sub M
this : ∃! y, ι.Dom y ∧ (Evalbm M (y :> fun i => ↑(v i))) (ι.func f)
y : M
hy : ι.Dom y
Hy : (Evalbm M (y :> fun i => ↑(v i))) (ι.func f)
z : M
hz : ι.Dom z
Hz : (Evalbm M (z :> fun i => ↑(v i))) (ι.func f)
⊢ z = y
Theorem: LO.FirstOrder.Interpretation.func_existsUnique
Proof state before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
k : ℕ
f : L'.Func k
v : Fin k → ι.Sub M
this : ∃! y, ι.Dom y ∧ (Evalbm M (y :> fun i => ↑(v i))) (ι.func f)
y : M
hy : ι.Dom y
Hy : (Evalbm M (y :> fun i => ↑(v i))) (ι.func f)
z : M
hz : ι.Dom z
Hz : (Evalbm M (z :> fun i => ↑(v i))) (ι.func f)
⊢ z = y
Tactic:
exact this.unique ⟨hz, Hz⟩ ⟨hy, Hy⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Interpretation.eval_varEquals_iff
Proof state before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n : ℕ
t : Semiterm L' Empty n
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals t) ↔ y = Semiterm.valbm (ι.Sub M) x t
Tactic:
induction t generalizing x y
Proof state after:
case bvar
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n : ℕ
a✝ : Fin n
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals #a✝) ↔ y = Semiterm.valbm (ι.Sub M) x #a✝

case fvar
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n : ℕ
a✝ : Empty
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals &a✝) ↔ y = Semiterm.valbm (ι.Sub M) x &a✝

case func
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n arity✝ : ℕ
a✝¹ : L'.Func arity✝
a✝ : Fin arity✝ → Semiterm L' Empty n
a_ih✝ :
  ∀ (a : Fin arity✝) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (a✝ a)) ↔ y = Semiterm.valbm (ι.Sub M) x (a✝ a)
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (Semiterm.func a✝¹ a✝)) ↔
    y = Semiterm.valbm (ι.Sub M) x (Semiterm.func a✝¹ a✝)
Theorem: LO.FirstOrder.Interpretation.eval_varEquals_iff
Proof state before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n : ℕ
a✝ : Fin n
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals #a✝) ↔ y = Semiterm.valbm (ι.Sub M) x #a✝
Tactic:
case bvar => simp [varEquals, Subtype.coe_inj]
Proof state after:
no goals
Theorem: LO.FirstOrder.Interpretation.eval_varEquals_iff
Proof state before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n : ℕ
a✝ : Empty
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals &a✝) ↔ y = Semiterm.valbm (ι.Sub M) x &a✝
Tactic:
case fvar => contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Interpretation.eval_varEquals_iff
Proof state before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n : ℕ
a✝ : Fin n
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals #a✝) ↔ y = Semiterm.valbm (ι.Sub M) x #a✝
Tactic:
simp [varEquals, Subtype.coe_inj]
Proof state after:
no goals
Theorem: LO.FirstOrder.Interpretation.eval_varEquals_iff
Proof state before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n : ℕ
a✝ : Empty
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals &a✝) ↔ y = Semiterm.valbm (ι.Sub M) x &a✝
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Interpretation.eval_varEquals_iff
Proof state before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (Semiterm.func f w)) ↔
    y = Semiterm.valbm (ι.Sub M) x (Semiterm.func f w)
Tactic:
simp [varEquals, eval_embSubsts, Matrix.comp_vecCons', Matrix.constant_eq_singleton, Semiterm.val_func, sub_func_iff]
Proof state after:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (∀ (e : Fin k → M),
      (∀ (i : Fin k), (Evalb s ![e i]) ι.domain ∧ (Evalb s (e i :> fun i => ↑(x i))) (ι.varEquals (w i))) →
        (Evalb s (↑y :> fun i => e i)) (ι.func f)) ↔
    (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f)
Theorem: LO.FirstOrder.Interpretation.eval_varEquals_iff
Proof state before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (∀ (e : Fin k → M),
      (∀ (i : Fin k), (Evalb s ![e i]) ι.domain ∧ (Evalb s (e i :> fun i => ↑(x i))) (ι.varEquals (w i))) →
        (Evalb s (↑y :> fun i => e i)) (ι.func f)) ↔
    (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f)
Tactic:
constructor
Proof state after:
case mp
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (∀ (e : Fin k → M),
      (∀ (i : Fin k), (Evalb s ![e i]) ι.domain ∧ (Evalb s (e i :> fun i => ↑(x i))) (ι.varEquals (w i))) →
        (Evalb s (↑y :> fun i => e i)) (ι.func f)) →
    (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f)

case mpr
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f) →
    ∀ (e : Fin k → M),
      (∀ (i : Fin k), (Evalb s ![e i]) ι.domain ∧ (Evalb s (e i :> fun i => ↑(x i))) (ι.varEquals (w i))) →
        (Evalb s (↑y :> fun i => e i)) (ι.func f)
Theorem: LO.FirstOrder.Interpretation.eval_varEquals_iff
Proof state before:
case mp
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (∀ (e : Fin k → M),
      (∀ (i : Fin k), (Evalb s ![e i]) ι.domain ∧ (Evalb s (e i :> fun i => ↑(x i))) (ι.varEquals (w i))) →
        (Evalb s (↑y :> fun i => e i)) (ι.func f)) →
    (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f)
Tactic:
intro h
Proof state after:
case mp
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
h :
  ∀ (e : Fin k → M),
    (∀ (i : Fin k), (Evalb s ![e i]) ι.domain ∧ (Evalb s (e i :> fun i => ↑(x i))) (ι.varEquals (w i))) →
      (Evalb s (↑y :> fun i => e i)) (ι.func f)
⊢ (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f)
Theorem: LO.FirstOrder.Interpretation.eval_varEquals_iff
Proof state before:
case mp
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
h :
  ∀ (e : Fin k → M),
    (∀ (i : Fin k), (Evalb s ![e i]) ι.domain ∧ (Evalb s (e i :> fun i => ↑(x i))) (ι.varEquals (w i))) →
      (Evalb s (↑y :> fun i => e i)) (ι.func f)
⊢ (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f)
Tactic:
exact h _ (fun i ↦ ⟨ι.pval_sub_domain M _, (@ih i (Semiterm.valbm (Sub ι M) x (w i)) x).mpr rfl⟩)
Proof state after:
no goals
Theorem: LO.FirstOrder.Interpretation.eval_varEquals_iff
Proof state before:
case mpr
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f) →
    ∀ (e : Fin k → M),
      (∀ (i : Fin k), (Evalb s ![e i]) ι.domain ∧ (Evalb s (e i :> fun i => ↑(x i))) (ι.varEquals (w i))) →
        (Evalb s (↑y :> fun i => e i)) (ι.func f)
Tactic:
rintro h v hv
Proof state after:
case mpr
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
h : (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f)
v : Fin k → M
hv : ∀ (i : Fin k), (Evalb s ![v i]) ι.domain ∧ (Evalb s (v i :> fun i => ↑(x i))) (ι.varEquals (w i))
⊢ (Evalb s (↑y :> fun i => v i)) (ι.func f)
Theorem: LO.FirstOrder.Interpretation.eval_varEquals_iff
Proof state before:
case mpr
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
h : (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f)
v : Fin k → M
hv : ∀ (i : Fin k), (Evalb s ![v i]) ι.domain ∧ (Evalb s (v i :> fun i => ↑(x i))) (ι.varEquals (w i))
⊢ (Evalb s (↑y :> fun i => v i)) (ι.func f)
Tactic:
have : v = fun i ↦ (Semiterm.valbm (Sub ι M) x (w i)).val :=
  funext fun i ↦ by simpa using congr_arg Subtype.val ((@ih i ⟨v i, (hv i).1⟩ x).mp (hv i).2)
Proof state after:
case mpr
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
h : (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f)
v : Fin k → M
hv : ∀ (i : Fin k), (Evalb s ![v i]) ι.domain ∧ (Evalb s (v i :> fun i => ↑(x i))) (ι.varEquals (w i))
this : v = fun i => ↑(Semiterm.valbm (ι.Sub M) x (w i))
⊢ (Evalb s (↑y :> fun i => v i)) (ι.func f)
Theorem: LO.FirstOrder.Interpretation.eval_varEquals_iff
Proof state before:
case mpr
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
h : (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f)
v : Fin k → M
hv : ∀ (i : Fin k), (Evalb s ![v i]) ι.domain ∧ (Evalb s (v i :> fun i => ↑(x i))) (ι.varEquals (w i))
this : v = fun i => ↑(Semiterm.valbm (ι.Sub M) x (w i))
⊢ (Evalb s (↑y :> fun i => v i)) (ι.func f)
Tactic:
rcases this
Proof state after:
case mpr.refl
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
h : (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f)
hv :
  ∀ (i : Fin k),
    (Evalb s ![(fun i => ↑(Semiterm.valbm (ι.Sub M) x (w i))) i]) ι.domain ∧
      (Evalb s ((fun i => ↑(Semiterm.valbm (ι.Sub M) x (w i))) i :> fun i => ↑(x i))) (ι.varEquals (w i))
⊢ (Evalb s (↑y :> fun i => (fun i => ↑(Semiterm.valbm (ι.Sub M) x (w i))) i)) (ι.func f)
Theorem: LO.FirstOrder.Interpretation.eval_varEquals_iff
Proof state before:
case mpr.refl
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
h : (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f)
hv :
  ∀ (i : Fin k),
    (Evalb s ![(fun i => ↑(Semiterm.valbm (ι.Sub M) x (w i))) i]) ι.domain ∧
      (Evalb s ((fun i => ↑(Semiterm.valbm (ι.Sub M) x (w i))) i :> fun i => ↑(x i))) (ι.varEquals (w i))
⊢ (Evalb s (↑y :> fun i => (fun i => ↑(Semiterm.valbm (ι.Sub M) x (w i))) i)) (ι.func f)
Tactic:
exact h
Proof state after:
no goals
Theorem: LO.FirstOrder.Interpretation.eval_varEquals_iff
Proof state before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
h : (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f)
v : Fin k → M
hv : ∀ (i : Fin k), (Evalb s ![v i]) ι.domain ∧ (Evalb s (v i :> fun i => ↑(x i))) (ι.varEquals (w i))
i : Fin k
⊢ v i = ↑(Semiterm.valbm (ι.Sub M) x (w i))
Tactic:
simpa using congr_arg Subtype.val ((@ih i ⟨v i, (hv i).1⟩ x).mp (hv i).2)
Proof state after:
no goals
Theorem: LO.FirstOrder.Interpretation.eval_translationRel_iff
Proof state before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
⊢ (Evalbm M fun i => ↑(e i)) (ι.translationRel r v) ↔ Structure.rel r fun i => Semiterm.valbm (ι.Sub M) e (v i)
Tactic:
simp [translationRel, Matrix.comp_vecCons', sub_rel_iff, eval_embSubsts, Matrix.constant_eq_singleton]
Proof state after:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
⊢ (∀ (e_1 : Fin k → M),
      (∀ (i : Fin k), (Evalb s ![e_1 i]) ι.domain ∧ (Evalb s (e_1 i :> fun i => ↑(e i))) (ι.varEquals (v i))) →
        (Eval s e_1 Empty.elim) (ι.rel r)) ↔
    (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
Theorem: LO.FirstOrder.Interpretation.eval_translationRel_iff
Proof state before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
⊢ (∀ (e_1 : Fin k → M),
      (∀ (i : Fin k), (Evalb s ![e_1 i]) ι.domain ∧ (Evalb s (e_1 i :> fun i => ↑(e i))) (ι.varEquals (v i))) →
        (Eval s e_1 Empty.elim) (ι.rel r)) ↔
    (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
Tactic:
constructor
Proof state after:
case mp
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
⊢ (∀ (e_1 : Fin k → M),
      (∀ (i : Fin k), (Evalb s ![e_1 i]) ι.domain ∧ (Evalb s (e_1 i :> fun i => ↑(e i))) (ι.varEquals (v i))) →
        (Eval s e_1 Empty.elim) (ι.rel r)) →
    (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)

case mpr
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
⊢ (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r) →
    ∀ (e_1 : Fin k → M),
      (∀ (i : Fin k), (Evalb s ![e_1 i]) ι.domain ∧ (Evalb s (e_1 i :> fun i => ↑(e i))) (ι.varEquals (v i))) →
        (Eval s e_1 Empty.elim) (ι.rel r)
Theorem: LO.FirstOrder.Interpretation.eval_translationRel_iff
Proof state before:
case mp
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
⊢ (∀ (e_1 : Fin k → M),
      (∀ (i : Fin k), (Evalb s ![e_1 i]) ι.domain ∧ (Evalb s (e_1 i :> fun i => ↑(e i))) (ι.varEquals (v i))) →
        (Eval s e_1 Empty.elim) (ι.rel r)) →
    (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
Tactic:
intro h
Proof state after:
case mp
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
h :
  ∀ (e_1 : Fin k → M),
    (∀ (i : Fin k), (Evalb s ![e_1 i]) ι.domain ∧ (Evalb s (e_1 i :> fun i => ↑(e i))) (ι.varEquals (v i))) →
      (Eval s e_1 Empty.elim) (ι.rel r)
⊢ (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
Theorem: LO.FirstOrder.Interpretation.eval_translationRel_iff
Proof state before:
case mp
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
h :
  ∀ (e_1 : Fin k → M),
    (∀ (i : Fin k), (Evalb s ![e_1 i]) ι.domain ∧ (Evalb s (e_1 i :> fun i => ↑(e i))) (ι.varEquals (v i))) →
      (Eval s e_1 Empty.elim) (ι.rel r)
⊢ (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
Tactic:
exact h (fun i ↦ (Semiterm.valbm (ι.Sub M) e (v i))) (fun i ↦ by simp [eval_varEquals_iff, Matrix.constant_eq_singleton])
Proof state after:
no goals
Theorem: LO.FirstOrder.Interpretation.eval_translationRel_iff
Proof state before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
h :
  ∀ (e_1 : Fin k → M),
    (∀ (i : Fin k), (Evalb s ![e_1 i]) ι.domain ∧ (Evalb s (e_1 i :> fun i => ↑(e i))) (ι.varEquals (v i))) →
      (Eval s e_1 Empty.elim) (ι.rel r)
i : Fin k
⊢ (Evalb s ![(fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) i]) ι.domain ∧
    (Evalb s ((fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) i :> fun i => ↑(e i))) (ι.varEquals (v i))
Tactic:
simp [eval_varEquals_iff, Matrix.constant_eq_singleton]
Proof state after:
no goals