Theorem: LO.FirstOrder.Interpretation.eval_translationRel_iff (Logic/FirstOrder/Interpretation.lean)

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]
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)

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
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)

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
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)

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])
State after:
no goals

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]
State after:
no goals

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 : ℕ
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)
Tactic:
intro h
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 : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
h : (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)

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 : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
h : (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)
Tactic:
intro l H
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 : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
h : (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
l : Fin k → M
H : ∀ (i : Fin k), (Evalb s ![l i]) ι.domain ∧ (Evalb s (l i :> fun i => ↑(e i))) (ι.varEquals (v i))
⊢ (Eval s l Empty.elim) (ι.rel r)

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 : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
h : (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
l : Fin k → M
H : ∀ (i : Fin k), (Evalb s ![l i]) ι.domain ∧ (Evalb s (l i :> fun i => ↑(e i))) (ι.varEquals (v i))
⊢ (Eval s l Empty.elim) (ι.rel r)
Tactic:
have : l = fun i ↦ (Semiterm.valbm (ι.Sub M) e (v i)).val := funext fun i ↦ by
  let z : ι.Sub M := ⟨l i, (H i).1⟩
  have : Evalbm M (z :> fun i ↦ e i) (ι.varEquals (v i)) := (H i).2
  exact congr_arg Subtype.val (eval_varEquals_iff.mp this)
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 : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
h : (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
l : Fin k → M
H : ∀ (i : Fin k), (Evalb s ![l i]) ι.domain ∧ (Evalb s (l i :> fun i => ↑(e i))) (ι.varEquals (v i))
this : l = fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))
⊢ (Eval s l Empty.elim) (ι.rel r)

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 : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
h : (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
l : Fin k → M
H : ∀ (i : Fin k), (Evalb s ![l i]) ι.domain ∧ (Evalb s (l i :> fun i => ↑(e i))) (ι.varEquals (v i))
this : l = fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))
⊢ (Eval s l Empty.elim) (ι.rel r)
Tactic:
rcases this
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 : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
h : (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
H :
  ∀ (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))
⊢ (Eval s (fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) Empty.elim) (ι.rel r)

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 : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
h : (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
H :
  ∀ (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))
⊢ (Eval s (fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) Empty.elim) (ι.rel r)
Tactic:
exact h
State after:
no goals

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 : (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
l : Fin k → M
H : ∀ (i : Fin k), (Evalb s ![l i]) ι.domain ∧ (Evalb s (l i :> fun i => ↑(e i))) (ι.varEquals (v i))
i : Fin k
⊢ l i = ↑(Semiterm.valbm (ι.Sub M) e (v i))
Tactic:
let z : ι.Sub M := ⟨l i, (H i).1⟩
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
h : (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
l : Fin k → M
H : ∀ (i : Fin k), (Evalb s ![l i]) ι.domain ∧ (Evalb s (l i :> fun i => ↑(e i))) (ι.varEquals (v i))
i : Fin k
z : ι.Sub M := ⟨l i, ⋯⟩
⊢ l i = ↑(Semiterm.valbm (ι.Sub M) e (v i))

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 : (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
l : Fin k → M
H : ∀ (i : Fin k), (Evalb s ![l i]) ι.domain ∧ (Evalb s (l i :> fun i => ↑(e i))) (ι.varEquals (v i))
i : Fin k
z : ι.Sub M := ⟨l i, ⋯⟩
⊢ l i = ↑(Semiterm.valbm (ι.Sub M) e (v i))
Tactic:
have : Evalbm M (z :> fun i ↦ e i) (ι.varEquals (v i)) := (H i).2
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
h : (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
l : Fin k → M
H : ∀ (i : Fin k), (Evalb s ![l i]) ι.domain ∧ (Evalb s (l i :> fun i => ↑(e i))) (ι.varEquals (v i))
i : Fin k
z : ι.Sub M := ⟨l i, ⋯⟩
this : (Evalbm M (↑z :> fun i => ↑(e i))) (ι.varEquals (v i))
⊢ l i = ↑(Semiterm.valbm (ι.Sub M) e (v i))

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 : (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
l : Fin k → M
H : ∀ (i : Fin k), (Evalb s ![l i]) ι.domain ∧ (Evalb s (l i :> fun i => ↑(e i))) (ι.varEquals (v i))
i : Fin k
z : ι.Sub M := ⟨l i, ⋯⟩
this : (Evalbm M (↑z :> fun i => ↑(e i))) (ι.varEquals (v i))
⊢ l i = ↑(Semiterm.valbm (ι.Sub M) e (v i))
Tactic:
exact congr_arg Subtype.val (eval_varEquals_iff.mp this)
State after:
no goals