internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Structure.Eq.eqv_funcExt
Proof state before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
k : ℕ
f : L.Func k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
this : M ⊧ₘ ∀* (“(!(vecEq varSumInL varSumInR) → !!(Semiterm.func f varSumInL) = !!(Semiterm.func f varSumInR))”)
⊢ eqv L (func f v) (func f w)
Tactic:
simp [varSumInL, varSumInR, models_def, vecEq, Semiterm.val_func] at this
Proof state after:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
k : ℕ
f : L.Func k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
this :
  ∀ (e : Fin (k + k) → M),
    (∀ (i : Fin k), op(=).val ![e (Fin.castLE ⋯ i), e (Fin.natAdd k i)]) →
      op(=).val ![func f fun i => e (Fin.castLE ⋯ i), func f fun i => e (Fin.natAdd k i)]
⊢ eqv L (func f v) (func f w)
Theorem: LO.FirstOrder.Structure.Eq.eqv_funcExt
Proof state before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
k : ℕ
f : L.Func k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
this :
  ∀ (e : Fin (k + k) → M),
    (∀ (i : Fin k), op(=).val ![e (Fin.castLE ⋯ i), e (Fin.natAdd k i)]) →
      op(=).val ![func f fun i => e (Fin.castLE ⋯ i), func f fun i => e (Fin.natAdd k i)]
⊢ eqv L (func f v) (func f w)
Tactic:
simpa [Matrix.vecAppend_eq_ite] using this (Matrix.vecAppend rfl v w) (fun i => by simpa [Matrix.vecAppend_eq_ite] using h i)
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.Eq.eqv_funcExt
Proof state before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
k : ℕ
f : L.Func k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
this :
  ∀ (e : Fin (k + k) → M),
    (∀ (i : Fin k), op(=).val ![e (Fin.castLE ⋯ i), e (Fin.natAdd k i)]) →
      op(=).val ![func f fun i => e (Fin.castLE ⋯ i), func f fun i => e (Fin.natAdd k i)]
i : Fin k
⊢ op(=).val ![Matrix.vecAppend ⋯ v w (Fin.castLE ⋯ i), Matrix.vecAppend ⋯ v w (Fin.natAdd k i)]
Tactic:
simpa [Matrix.vecAppend_eq_ite] using h i
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.Eq.eqv_relExt_aux
Proof state before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
k : ℕ
r : L.Rel k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
⊢ rel r v → rel r w
Tactic:
have : M ⊧ₘ ∀* (Semiformula.vecEq varSumInL varSumInR ⟶ Semiformula.rel r varSumInL ⟶ Semiformula.rel r varSumInR) :=
  H.realize (eqAxiom.relExt r (L := L))
Proof state after:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
k : ℕ
r : L.Rel k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
this : M ⊧ₘ ∀* (vecEq varSumInL varSumInR ⟶ Semiformula.rel r varSumInL ⟶ Semiformula.rel r varSumInR)
⊢ rel r v → rel r w
Theorem: LO.FirstOrder.Structure.Eq.eqv_relExt_aux
Proof state before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
k : ℕ
r : L.Rel k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
this : M ⊧ₘ ∀* (vecEq varSumInL varSumInR ⟶ Semiformula.rel r varSumInL ⟶ Semiformula.rel r varSumInR)
⊢ rel r v → rel r w
Tactic:
simp [varSumInL, varSumInR, models_def, vecEq, Semiterm.val_func, eval_rel (r := r)] at this
Proof state after:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
k : ℕ
r : L.Rel k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
this :
  ∀ (e : Fin (k + k) → M),
    (∀ (i : Fin k), op(=).val ![e (Fin.castLE ⋯ i), e (Fin.natAdd k i)]) →
      (rel r fun i => e (Fin.castLE ⋯ i)) → rel r fun i => e (Fin.natAdd k i)
⊢ rel r v → rel r w
Theorem: LO.FirstOrder.Structure.Eq.eqv_relExt_aux
Proof state before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
k : ℕ
r : L.Rel k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
this :
  ∀ (e : Fin (k + k) → M),
    (∀ (i : Fin k), op(=).val ![e (Fin.castLE ⋯ i), e (Fin.natAdd k i)]) →
      (rel r fun i => e (Fin.castLE ⋯ i)) → rel r fun i => e (Fin.natAdd k i)
⊢ rel r v → rel r w
Tactic:
simpa [eval_rel, Matrix.vecAppend_eq_ite] using this (Matrix.vecAppend rfl v w) (fun i => by simpa [Matrix.vecAppend_eq_ite] using h i)
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.Eq.eqv_relExt_aux
Proof state before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
k : ℕ
r : L.Rel k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
this :
  ∀ (e : Fin (k + k) → M),
    (∀ (i : Fin k), op(=).val ![e (Fin.castLE ⋯ i), e (Fin.natAdd k i)]) →
      (rel r fun i => e (Fin.castLE ⋯ i)) → rel r fun i => e (Fin.natAdd k i)
i : Fin k
⊢ op(=).val ![Matrix.vecAppend ⋯ v w (Fin.castLE ⋯ i), Matrix.vecAppend ⋯ v w (Fin.natAdd k i)]
Tactic:
simpa [Matrix.vecAppend_eq_ite] using h i
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.Eq.eqv_relExt
Proof state before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
k : ℕ
r : L.Rel k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
⊢ rel r v = rel r w
Tactic:
simp
Proof state after:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
k : ℕ
r : L.Rel k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
⊢ rel r v ↔ rel r w
Theorem: LO.FirstOrder.Structure.Eq.eqv_relExt
Proof state before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
k : ℕ
r : L.Rel k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
⊢ rel r v ↔ rel r w
Tactic:
constructor
Proof 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 ⊧ₘ* 𝐄𝐐
k : ℕ
r : L.Rel k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
⊢ rel r v → rel r w

case mpr
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
k : ℕ
r : L.Rel k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
⊢ rel r w → rel r v
Theorem: LO.FirstOrder.Structure.Eq.eqv_relExt
Proof 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 ⊧ₘ* 𝐄𝐐
k : ℕ
r : L.Rel k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
⊢ rel r v → rel r w
Tactic:
exact eqv_relExt_aux H r h
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.Eq.eqv_relExt
Proof 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 ⊧ₘ* 𝐄𝐐
k : ℕ
r : L.Rel k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
⊢ rel r w → rel r v
Tactic:
exact eqv_relExt_aux H r (fun i => eqv_symm H (h i))
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.Eq.QuotEq.val_mk
Proof 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
t : Semiterm L μ n
⊢ valm (QuotEq H) (fun i => ⟦e i⟧) (fun i => ⟦ε i⟧) t = ⟦valm M e ε t⟧
Tactic:
induction t <;> simp [*, funk_mk, Semiterm.val_func]
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.Eq.QuotEq.eval_mk
Proof 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]
Proof 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✝
Theorem: LO.FirstOrder.Structure.Eq.QuotEq.eval_mk
Proof 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
Proof 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
Theorem: LO.FirstOrder.Structure.Eq.QuotEq.eval_mk
Proof 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
Proof 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
Theorem: LO.FirstOrder.Structure.Eq.QuotEq.eval_mk
Proof 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⟧)
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.Eq.QuotEq.eval_mk
Proof 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⟧
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.Eq.QuotEq.eval_mk
Proof 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
Proof 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
Theorem: LO.FirstOrder.Structure.Eq.QuotEq.eval_mk
Proof 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
Proof 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
Theorem: LO.FirstOrder.Structure.Eq.QuotEq.eval_mk
Proof 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)
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.Eq.QuotEq.eval_mk
Proof 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
Proof 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
Theorem: LO.FirstOrder.Structure.Eq.QuotEq.eval_mk
Proof 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⟩
Proof 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
Theorem: LO.FirstOrder.Structure.Eq.QuotEq.eval_mk
Proof 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
Proof 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
Theorem: LO.FirstOrder.Structure.Eq.QuotEq.eval_mk
Proof 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)⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.Eq.QuotEq.eval_mk
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.Eq.QuotEq.eval_mk
Proof 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⟩
Proof 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
Theorem: LO.FirstOrder.Structure.Eq.QuotEq.eval_mk
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.Eq.QuotEq.eval_mk
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.Eq.QuotEq.models_iff
Proof state before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
σ : Sentence L
⊢ QuotEq H ⊧ₘ σ ↔ M ⊧ₘ σ
Tactic:
simpa [models_def, Semiformula.Evalf, eq_finZeroElim, Empty.eq_elim] using
  eval_mk (H := H) (e := finZeroElim) (ε := Empty.elim) (p := σ)
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.Eq.QuotEq.rel_eq
Proof state before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b : QuotEq H
⊢ op(=).val ![a, b] ↔ a = b
Tactic:
induction' a using Quotient.ind with a
Proof state after:
case a
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
b : QuotEq H
a : M
⊢ op(=).val ![⟦a⟧, b] ↔ ⟦a⟧ = b
Theorem: LO.FirstOrder.Structure.Eq.QuotEq.rel_eq
Proof state before:
case a
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
b : QuotEq H
a : M
⊢ op(=).val ![⟦a⟧, b] ↔ ⟦a⟧ = b
Tactic:
induction' b using Quotient.ind with b
Proof state after:
case a.a
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b : M
⊢ op(=).val ![⟦a⟧, ⟦b⟧] ↔ ⟦a⟧ = ⟦b⟧
Theorem: LO.FirstOrder.Structure.Eq.QuotEq.rel_eq
Proof state before:
case a.a
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b : M
⊢ op(=).val ![⟦a⟧, ⟦b⟧] ↔ ⟦a⟧ = ⟦b⟧
Tactic:
rw[of_eq_of]
Proof state after:
case a.a
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b : M
⊢ op(=).val ![⟦a⟧, ⟦b⟧] ↔ eqv L a b
Theorem: LO.FirstOrder.Structure.Eq.QuotEq.rel_eq
Proof state before:
case a.a
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b : M
⊢ op(=).val ![⟦a⟧, ⟦b⟧] ↔ eqv L a b
Tactic:
simp [eqv, Semiformula.Operator.val]
Proof state after:
case a.a
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b : M
⊢ (Eval struc ![⟦a⟧, ⟦b⟧] Empty.elim) op(=).sentence ↔ (Eval inst✝ ![a, b] Empty.elim) op(=).sentence
Theorem: LO.FirstOrder.Structure.Eq.QuotEq.rel_eq
Proof state before:
case a.a
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b : M
⊢ (Eval struc ![⟦a⟧, ⟦b⟧] Empty.elim) op(=).sentence ↔ (Eval inst✝ ![a, b] Empty.elim) op(=).sentence
Tactic:
simpa [Evalm, Matrix.fun_eq_vec₂, Empty.eq_elim] using
  eval_mk (H := H) (e := ![a, b]) (ε := Empty.elim) (p := Semiformula.Operator.Eq.eq.sentence)
Proof state after:
no goals
Theorem: LO.FirstOrder.consequence_iff_eq
Proof state before:
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
⊢ T ⊨[Struc L] σ ↔
    ∀ (M : Type v) [inst : Nonempty M] [inst_1 : Structure L M] [inst_2 : Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ
Tactic:
simp [consequence_iff]
Proof state after:
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
⊢ (∀ (M : Type v) (a : M) [inst : Structure L M], M ⊧ₘ* T → M ⊧ₘ σ) ↔
    ∀ (M : Type v) (a : M) [inst : Structure L M] [inst_1 : Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ