Theorem: LO.FirstOrder.Interpretation.func_existsUnique (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
k : ℕ
f : L'.Func k
v : Fin k → ι.Sub M
⊢ ∃! y, (Evalbm M (↑y :> fun i => ↑(v i))) (ι.func f)
Tactic:
have : ∃! y, ι.Dom y ∧ Evalbm M (y :> fun i ↦ v i) (ι.func f) := ι.func_existsUnique_on_dom M f (fun i ↦ v i) (fun i ↦ by simp [(v i).prop])
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, (Evalbm M (↑y :> fun i => ↑(v i))) (ι.func f)

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, (Evalbm M (↑y :> fun i => ↑(v i))) (ι.func f)
Tactic:
rcases this.exists with ⟨y, hy, Hy⟩
State after:
case 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
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, (Evalbm M (↑y :> fun i => ↑(v i))) (ι.func f)

State before:
case 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
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, (Evalbm M (↑y :> fun i => ↑(v i))) (ι.func f)
Tactic:
exact ExistsUnique.intro ⟨y, hy⟩ (by simpa using Hy) (by simp; intro z hz Hz; exact this.unique ⟨hz, Hz⟩ ⟨hy, Hy⟩)
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
k : ℕ
f : L'.Func k
v : Fin k → ι.Sub M
i : Fin k
⊢ ι.Dom ((fun i => ↑(v i)) i)
Tactic:
simp [(v i).prop]
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
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)
⊢ (Evalbm M (↑⟨y, hy⟩ :> fun i => ↑(v i))) (ι.func f)
Tactic:
simpa using Hy
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
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
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

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

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