Theorem: LO.FirstOrder.Structure.Eq.QuotEq.eval_mk (Logic/FirstOrder/Basic/Eq.lean)

State before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n : ℕ
e : Fin n → M
ε : μ → M
p : Semiformula L μ n
⊢ (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p ↔ (Evalm M e ε) p
Tactic:
induction p using Semiformula.rec' <;> simp [*, Semiformula.eval_rel, Semiformula.eval_nrel, val_mk, rel_mk]
State after:
case hall
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n : ℕ
ε : μ → M
n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : ∀ {e : Fin (n✝ + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p✝ ↔ (Evalm M e ε) p✝
e : Fin n✝ → M
⊢ (∀ (x : QuotEq H), (Eval struc (x :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p✝) ↔ ∀ (x : M), (Eval inst✝ (x :> e) ε) p✝

case hex
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n : ℕ
ε : μ → M
n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : ∀ {e : Fin (n✝ + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p✝ ↔ (Evalm M e ε) p✝
e : Fin n✝ → M
⊢ (∃ x, (Eval struc (x :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p✝) ↔ ∃ x, (Eval inst✝ (x :> e) ε) p✝

State before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n✝ : ℕ
ε : μ → M
n : ℕ
p : Semiformula L μ (n + 1)
ih : ∀ {e : Fin (n + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p ↔ (Evalm M e ε) p
e : Fin n → M
⊢ (∀ (x : QuotEq H), (Eval struc (x :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p) ↔ ∀ (x : M), (Eval inst✝ (x :> e) ε) p
Tactic:
constructor
State after:
case mp
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n✝ : ℕ
ε : μ → M
n : ℕ
p : Semiformula L μ (n + 1)
ih : ∀ {e : Fin (n + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p ↔ (Evalm M e ε) p
e : Fin n → M
⊢ (∀ (x : QuotEq H), (Eval struc (x :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p) → ∀ (x : M), (Eval inst✝ (x :> e) ε) p

case mpr
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n✝ : ℕ
ε : μ → M
n : ℕ
p : Semiformula L μ (n + 1)
ih : ∀ {e : Fin (n + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p ↔ (Evalm M e ε) p
e : Fin n → M
⊢ (∀ (x : M), (Eval inst✝ (x :> e) ε) p) → ∀ (x : QuotEq H), (Eval struc (x :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p

State before:
case mp
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n✝ : ℕ
ε : μ → M
n : ℕ
p : Semiformula L μ (n + 1)
ih : ∀ {e : Fin (n + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p ↔ (Evalm M e ε) p
e : Fin n → M
⊢ (∀ (x : QuotEq H), (Eval struc (x :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p) → ∀ (x : M), (Eval inst✝ (x :> e) ε) p
Tactic:
intro h a
State after:
case mp
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n✝ : ℕ
ε : μ → M
n : ℕ
p : Semiformula L μ (n + 1)
ih : ∀ {e : Fin (n + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p ↔ (Evalm M e ε) p
e : Fin n → M
h : ∀ (x : QuotEq H), (Eval struc (x :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p
a : M
⊢ (Eval inst✝ (a :> e) ε) p

State before:
case mp
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n✝ : ℕ
ε : μ → M
n : ℕ
p : Semiformula L μ (n + 1)
ih : ∀ {e : Fin (n + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p ↔ (Evalm M e ε) p
e : Fin n → M
h : ∀ (x : QuotEq H), (Eval struc (x :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p
a : M
⊢ (Eval inst✝ (a :> e) ε) p
Tactic:
exact (ih (e := a :> e)).mp (by simpa [Matrix.comp_vecCons] using h ⟦a⟧)
State after:
no goals

State before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n✝ : ℕ
ε : μ → M
n : ℕ
p : Semiformula L μ (n + 1)
ih : ∀ {e : Fin (n + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p ↔ (Evalm M e ε) p
e : Fin n → M
h : ∀ (x : QuotEq H), (Eval struc (x :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p
a : M
⊢ (Evalm (QuotEq H) (fun i => ⟦(a :> e) i⟧) fun i => ⟦ε i⟧) p
Tactic:
simpa [Matrix.comp_vecCons] using h ⟦a⟧
State after:
no goals

State before:
case mpr
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n✝ : ℕ
ε : μ → M
n : ℕ
p : Semiformula L μ (n + 1)
ih : ∀ {e : Fin (n + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p ↔ (Evalm M e ε) p
e : Fin n → M
⊢ (∀ (x : M), (Eval inst✝ (x :> e) ε) p) → ∀ (x : QuotEq H), (Eval struc (x :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p
Tactic:
intro h a
State after:
case mpr
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n✝ : ℕ
ε : μ → M
n : ℕ
p : Semiformula L μ (n + 1)
ih : ∀ {e : Fin (n + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p ↔ (Evalm M e ε) p
e : Fin n → M
h : ∀ (x : M), (Eval inst✝ (x :> e) ε) p
a : QuotEq H
⊢ (Eval struc (a :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p

State before:
case mpr
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n✝ : ℕ
ε : μ → M
n : ℕ
p : Semiformula L μ (n + 1)
ih : ∀ {e : Fin (n + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p ↔ (Evalm M e ε) p
e : Fin n → M
h : ∀ (x : M), (Eval inst✝ (x :> e) ε) p
a : QuotEq H
⊢ (Eval struc (a :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p
Tactic:
induction' a using Quotient.ind with a
State after:
case mpr.a
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n✝ : ℕ
ε : μ → M
n : ℕ
p : Semiformula L μ (n + 1)
ih : ∀ {e : Fin (n + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p ↔ (Evalm M e ε) p
e : Fin n → M
h : ∀ (x : M), (Eval inst✝ (x :> e) ε) p
a : M
⊢ (Eval struc (⟦a⟧ :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p

State before:
case mpr.a
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n✝ : ℕ
ε : μ → M
n : ℕ
p : Semiformula L μ (n + 1)
ih : ∀ {e : Fin (n + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p ↔ (Evalm M e ε) p
e : Fin n → M
h : ∀ (x : M), (Eval inst✝ (x :> e) ε) p
a : M
⊢ (Eval struc (⟦a⟧ :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p
Tactic:
simpa [Matrix.comp_vecCons] using ih.mpr (h a)
State after:
no goals

State before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n✝ : ℕ
ε : μ → M
n : ℕ
p : Semiformula L μ (n + 1)
ih : ∀ {e : Fin (n + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p ↔ (Evalm M e ε) p
e : Fin n → M
⊢ (∃ x, (Eval struc (x :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p) ↔ ∃ x, (Eval inst✝ (x :> e) ε) p
Tactic:
constructor
State after:
case mp
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n✝ : ℕ
ε : μ → M
n : ℕ
p : Semiformula L μ (n + 1)
ih : ∀ {e : Fin (n + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p ↔ (Evalm M e ε) p
e : Fin n → M
⊢ (∃ x, (Eval struc (x :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p) → ∃ x, (Eval inst✝ (x :> e) ε) p

case mpr
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n✝ : ℕ
ε : μ → M
n : ℕ
p : Semiformula L μ (n + 1)
ih : ∀ {e : Fin (n + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p ↔ (Evalm M e ε) p
e : Fin n → M
⊢ (∃ x, (Eval inst✝ (x :> e) ε) p) → ∃ x, (Eval struc (x :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p

State before:
case mp
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n✝ : ℕ
ε : μ → M
n : ℕ
p : Semiformula L μ (n + 1)
ih : ∀ {e : Fin (n + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p ↔ (Evalm M e ε) p
e : Fin n → M
⊢ (∃ x, (Eval struc (x :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p) → ∃ x, (Eval inst✝ (x :> e) ε) p
Tactic:
intro ⟨a, h⟩
State after:
case mp
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n✝ : ℕ
ε : μ → M
n : ℕ
p : Semiformula L μ (n + 1)
ih : ∀ {e : Fin (n + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p ↔ (Evalm M e ε) p
e : Fin n → M
a : QuotEq H
h : (Eval struc (a :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p
⊢ ∃ x, (Eval inst✝ (x :> e) ε) p

State before:
case mp
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n✝ : ℕ
ε : μ → M
n : ℕ
p : Semiformula L μ (n + 1)
ih : ∀ {e : Fin (n + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p ↔ (Evalm M e ε) p
e : Fin n → M
a : QuotEq H
h : (Eval struc (a :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p
⊢ ∃ x, (Eval inst✝ (x :> e) ε) p
Tactic:
induction' a using Quotient.ind with a
State after:
case mp.a
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n✝ : ℕ
ε : μ → M
n : ℕ
p : Semiformula L μ (n + 1)
ih : ∀ {e : Fin (n + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p ↔ (Evalm M e ε) p
e : Fin n → M
a : M
h : (Eval struc (⟦a⟧ :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p
⊢ ∃ x, (Eval inst✝ (x :> e) ε) p

State before:
case mp.a
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n✝ : ℕ
ε : μ → M
n : ℕ
p : Semiformula L μ (n + 1)
ih : ∀ {e : Fin (n + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p ↔ (Evalm M e ε) p
e : Fin n → M
a : M
h : (Eval struc (⟦a⟧ :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p
⊢ ∃ x, (Eval inst✝ (x :> e) ε) p
Tactic:
exact ⟨a, (ih (e := a :> e)).mp (by simpa [Matrix.comp_vecCons] using h)⟩
State after:
no goals

State before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n✝ : ℕ
ε : μ → M
n : ℕ
p : Semiformula L μ (n + 1)
ih : ∀ {e : Fin (n + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p ↔ (Evalm M e ε) p
e : Fin n → M
a : M
h : (Eval struc (⟦a⟧ :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p
⊢ (Evalm (QuotEq H) (fun i => ⟦(a :> e) i⟧) fun i => ⟦ε i⟧) p
Tactic:
simpa [Matrix.comp_vecCons] using h
State after:
no goals

State before:
case mpr
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n✝ : ℕ
ε : μ → M
n : ℕ
p : Semiformula L μ (n + 1)
ih : ∀ {e : Fin (n + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p ↔ (Evalm M e ε) p
e : Fin n → M
⊢ (∃ x, (Eval inst✝ (x :> e) ε) p) → ∃ x, (Eval struc (x :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p
Tactic:
intro ⟨a, h⟩
State after:
case mpr
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n✝ : ℕ
ε : μ → M
n : ℕ
p : Semiformula L μ (n + 1)
ih : ∀ {e : Fin (n + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p ↔ (Evalm M e ε) p
e : Fin n → M
a : M
h : (Eval inst✝ (a :> e) ε) p
⊢ ∃ x, (Eval struc (x :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p

State before:
case mpr
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n✝ : ℕ
ε : μ → M
n : ℕ
p : Semiformula L μ (n + 1)
ih : ∀ {e : Fin (n + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p ↔ (Evalm M e ε) p
e : Fin n → M
a : M
h : (Eval inst✝ (a :> e) ε) p
⊢ ∃ x, (Eval struc (x :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p
Tactic:
exact ⟨⟦a⟧, by simpa [Matrix.comp_vecCons] using ih.mpr h⟩
State after:
no goals

State before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n✝ : ℕ
ε : μ → M
n : ℕ
p : Semiformula L μ (n + 1)
ih : ∀ {e : Fin (n + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p ↔ (Evalm M e ε) p
e : Fin n → M
a : M
h : (Eval inst✝ (a :> e) ε) p
⊢ (Eval struc (⟦a⟧ :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p
Tactic:
simpa [Matrix.comp_vecCons] using ih.mpr h
State after:
no goals