Theorem: LO.FirstOrder.Interpretation.eval_translation_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 : ℕ
p : Semisentence L' n
e : Fin n → ι.Sub M
⊢ (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
Tactic:
induction p using Semiformula.rec'
  <;> simp [*, Matrix.constant_eq_singleton, eval_substs, eval_translationRel_iff, eval_rel, eval_nrel]
State after:
case hall
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 n✝ : ℕ
p✝ : Semiformula L' Empty (n✝ + 1)
a✝ : ∀ {e : Fin (n✝ + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p✝) ↔ (Evalbm (ι.Sub M) e) p✝
e : Fin n✝ → ι.Sub M
⊢ (∀ (x : M), (Eval s ![x] Empty.elim) ι.domain → (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p✝)) ↔
    ∀ (a : M) (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p✝

case hex
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 n✝ : ℕ
p✝ : Semiformula L' Empty (n✝ + 1)
a✝ : ∀ {e : Fin (n✝ + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p✝) ↔ (Evalbm (ι.Sub M) e) p✝
e : Fin n✝ → ι.Sub M
⊢ (∃ x, (Eval s ![x] Empty.elim) ι.domain ∧ (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p✝)) ↔
    ∃ a, ∃ (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p✝

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✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
⊢ (∀ (x : M), (Eval s ![x] Empty.elim) ι.domain → (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)) ↔
    ∀ (a : M) (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p
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✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
⊢ (∀ (x : M), (Eval s ![x] Empty.elim) ι.domain → (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)) →
    ∀ (a : M) (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p

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✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
⊢ (∀ (a : M) (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p) →
    ∀ (x : M), (Eval s ![x] Empty.elim) ι.domain → (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)

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✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
⊢ (∀ (x : M), (Eval s ![x] Empty.elim) ι.domain → (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)) →
    ∀ (a : M) (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p
Tactic:
intro h x hx
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✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
h : ∀ (x : M), (Eval s ![x] Empty.elim) ι.domain → (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)
x : M
hx : ι.Dom x
⊢ (Eval subStructure (⟨x, hx⟩ :> e) Empty.elim) p

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✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
h : ∀ (x : M), (Eval s ![x] Empty.elim) ι.domain → (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)
x : M
hx : ι.Dom x
⊢ (Eval subStructure (⟨x, hx⟩ :> e) Empty.elim) p
Tactic:
exact ih.mp (by simpa [Matrix.comp_vecCons'] using h x hx)
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✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
h : ∀ (x : M), (Eval s ![x] Empty.elim) ι.domain → (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)
x : M
hx : ι.Dom x
⊢ (Evalbm M fun i => ↑((⟨x, hx⟩ :> e) i)) (ι.translation p)
Tactic:
simpa [Matrix.comp_vecCons'] using h x hx
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✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
⊢ (∀ (a : M) (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p) →
    ∀ (x : M), (Eval s ![x] Empty.elim) ι.domain → (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)
Tactic:
intro h x hx
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✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
h : ∀ (a : M) (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p
x : M
hx : (Eval s ![x] Empty.elim) ι.domain
⊢ (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)

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✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
h : ∀ (a : M) (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p
x : M
hx : (Eval s ![x] Empty.elim) ι.domain
⊢ (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)
Tactic:
simpa [Matrix.comp_vecCons'] using ih.mpr (h x hx)
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✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
⊢ (∃ x, (Eval s ![x] Empty.elim) ι.domain ∧ (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)) ↔
    ∃ a, ∃ (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p
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✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
⊢ (∃ x, (Eval s ![x] Empty.elim) ι.domain ∧ (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)) →
    ∃ a, ∃ (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p

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✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
⊢ (∃ a, ∃ (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p) →
    ∃ x, (Eval s ![x] Empty.elim) ι.domain ∧ (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)

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✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
⊢ (∃ x, (Eval s ![x] Empty.elim) ι.domain ∧ (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)) →
    ∃ a, ∃ (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p
Tactic:
rintro ⟨x, hx, h⟩
State after:
case mp.intro.intro
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✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
x : M
hx : (Eval s ![x] Empty.elim) ι.domain
h : (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)
⊢ ∃ a, ∃ (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p

State before:
case mp.intro.intro
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✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
x : M
hx : (Eval s ![x] Empty.elim) ι.domain
h : (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)
⊢ ∃ a, ∃ (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p
Tactic:
refine ⟨x, hx, ih.mp (by simpa [Matrix.comp_vecCons'] using 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✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
x : M
hx : (Eval s ![x] Empty.elim) ι.domain
h : (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)
⊢ (Evalbm M fun i => ↑((⟨x, hx⟩ :> e) i)) (ι.translation p)
Tactic:
simpa [Matrix.comp_vecCons'] using h
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✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
⊢ (∃ a, ∃ (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p) →
    ∃ x, (Eval s ![x] Empty.elim) ι.domain ∧ (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)
Tactic:
intro ⟨x, hx, 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✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
x : M
hx : ι.Dom x
h : (Eval subStructure (⟨x, hx⟩ :> e) Empty.elim) p
⊢ ∃ x, (Eval s ![x] Empty.elim) ι.domain ∧ (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)

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✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
x : M
hx : ι.Dom x
h : (Eval subStructure (⟨x, hx⟩ :> e) Empty.elim) p
⊢ ∃ x, (Eval s ![x] Empty.elim) ι.domain ∧ (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)
Tactic:
refine ⟨x, hx, by simpa [Matrix.comp_vecCons'] using ih.mpr 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✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
x : M
hx : ι.Dom x
h : (Eval subStructure (⟨x, hx⟩ :> e) Empty.elim) p
⊢ (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)
Tactic:
simpa [Matrix.comp_vecCons'] using ih.mpr h
State after:
no goals