internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
ih : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∃' p).fvarList) ε ε'
x✝ : M
x : μ
hx : (fun x => x ∈ p.fvarList) x
⊢ (fun x => x ∈ (∃' p).fvarList) x
Tactic:
simp [fvar?]
Proof state after:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
ih : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∃' p).fvarList) ε ε'
x✝ : M
x : μ
hx : (fun x => x ∈ p.fvarList) x
⊢ x ∈ p.fvarList
Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
ε' : μ → M
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
ih : ∀ {e : Fin (n✝ + 1) → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (∃' p).fvarList) ε ε'
x✝ : M
x : μ
hx : (fun x => x ∈ p.fvarList) x
⊢ x ∈ p.fvarList
Tactic:
exact hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.val_fvUnivClosure_inhabited
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
h : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
⊢ (Evalf s Empty.elim) (∀ᶠ* p) ↔ ∀ (ε : μ → M), (Evalf s ε) p
Tactic:
simp [Formula.fvUnivClosure, eval_rewriteMap]
Proof state after:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
h : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
⊢ (∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p) ↔ ∀ (ε : μ → M), (Evalf s ε) p
Theorem: LO.FirstOrder.Semiformula.val_fvUnivClosure_inhabited
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
h : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
⊢ (∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p) ↔ ∀ (ε : μ → M), (Evalf s ε) p
Tactic:
haveI : Inhabited μ := ⟨Classical.ofNonempty⟩
Proof state after:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
h : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this : Inhabited μ
⊢ (∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p) ↔ ∀ (ε : μ → M), (Evalf s ε) p
Theorem: LO.FirstOrder.Semiformula.val_fvUnivClosure_inhabited
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
h : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this : Inhabited μ
⊢ (∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p) ↔ ∀ (ε : μ → M), (Evalf s ε) p
Tactic:
constructor
Proof state after:
case mp
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
h : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this : Inhabited μ
⊢ (∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p) → ∀ (ε : μ → M), (Evalf s ε) p

case mpr
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
h : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this : Inhabited μ
⊢ (∀ (ε : μ → M), (Evalf s ε) p) → ∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p
Theorem: LO.FirstOrder.Semiformula.val_fvUnivClosure_inhabited
Proof state before:
case mp
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
h : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this : Inhabited μ
⊢ (∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p) → ∀ (ε : μ → M), (Evalf s ε) p
Tactic:
intro h ε
Proof state after:
case mp
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₂ : μ₂ → M
h✝ : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this : Inhabited μ
h : ∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p
ε : μ → M
⊢ (Evalf s ε) p
Theorem: LO.FirstOrder.Semiformula.val_fvUnivClosure_inhabited
Proof state before:
case mp
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₂ : μ₂ → M
h✝ : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this : Inhabited μ
h : ∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p
ε : μ → M
⊢ (Evalf s ε) p
Tactic:
have := h (fun i ↦ ε $ Semiformula.fvListingInv _ i)
Proof state after:
case mp
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₂ : μ₂ → M
h✝ : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this✝ : Inhabited μ
h : ∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p
ε : μ → M
this : (Eval s ![] fun x => ε (fvListingInv p (fvListing p x))) p
⊢ (Evalf s ε) p
Theorem: LO.FirstOrder.Semiformula.val_fvUnivClosure_inhabited
Proof state before:
case mp
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₂ : μ₂ → M
h✝ : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this✝ : Inhabited μ
h : ∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p
ε : μ → M
this : (Eval s ![] fun x => ε (fvListingInv p (fvListing p x))) p
⊢ (Evalf s ε) p
Tactic:
exact (eval_iff_of_funEqOn p (by intro x hx; simp [fvListingInv_fvListing hx])).mp this
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.val_fvUnivClosure_inhabited
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₂ : μ₂ → M
h✝ : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this✝ : Inhabited μ
h : ∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p
ε : μ → M
this : (Eval s ![] fun x => ε (fvListingInv p (fvListing p x))) p
⊢ Function.funEqOn (fvar? p) (fun x => ε (fvListingInv p (fvListing p x))) ε
Tactic:
intro x hx
Proof state after:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₂ : μ₂ → M
h✝ : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this✝ : Inhabited μ
h : ∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p
ε : μ → M
this : (Eval s ![] fun x => ε (fvListingInv p (fvListing p x))) p
x : μ
hx : fvar? p x
⊢ (fun x => ε (fvListingInv p (fvListing p x))) x = ε x
Theorem: LO.FirstOrder.Semiformula.val_fvUnivClosure_inhabited
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε✝ : μ → M
ε₂ : μ₂ → M
h✝ : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this✝ : Inhabited μ
h : ∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p
ε : μ → M
this : (Eval s ![] fun x => ε (fvListingInv p (fvListing p x))) p
x : μ
hx : fvar? p x
⊢ (fun x => ε (fvListingInv p (fvListing p x))) x = ε x
Tactic:
simp [fvListingInv_fvListing hx]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.val_fvUnivClosure_inhabited
Proof state before:
case mpr
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
h : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this : Inhabited μ
⊢ (∀ (ε : μ → M), (Evalf s ε) p) → ∀ (e : Fin ((fvarList p).length + 1) → M), (Eval s ![] fun x => e (fvListing p x)) p
Tactic:
intro h e
Proof state after:
case mpr
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e✝ : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
h✝ : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this : Inhabited μ
h : ∀ (ε : μ → M), (Evalf s ε) p
e : Fin ((fvarList p).length + 1) → M
⊢ (Eval s ![] fun x => e (fvListing p x)) p
Theorem: LO.FirstOrder.Semiformula.val_fvUnivClosure_inhabited
Proof state before:
case mpr
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e✝ : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
h✝ : Nonempty μ
inst✝ : DecidableEq μ
p : Formula L μ
this : Inhabited μ
h : ∀ (ε : μ → M), (Evalf s ε) p
e : Fin ((fvarList p).length + 1) → M
⊢ (Eval s ![] fun x => e (fvListing p x)) p
Tactic:
exact h (fun x ↦ e $ Semiformula.fvListing p x)
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.val_fvUnivClosure
Proof state before:
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
inst✝¹ : Nonempty M
inst✝ : DecidableEq μ
p : Formula L μ
⊢ (Evalf s Empty.elim) (∀ᶠ* p) ↔ ∀ (ε : μ → M), (Evalf s ε) p
Tactic:
by_cases hμ : Nonempty μ
Proof state after:
case pos
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
inst✝¹ : Nonempty M
inst✝ : DecidableEq μ
p : Formula L μ
hμ : Nonempty μ
⊢ (Evalf s Empty.elim) (∀ᶠ* p) ↔ ∀ (ε : μ → M), (Evalf s ε) p

case neg
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
inst✝¹ : Nonempty M
inst✝ : DecidableEq μ
p : Formula L μ
hμ : ¬Nonempty μ
⊢ (Evalf s Empty.elim) (∀ᶠ* p) ↔ ∀ (ε : μ → M), (Evalf s ε) p
Theorem: LO.FirstOrder.Semiformula.val_fvUnivClosure
Proof state before:
case pos
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
inst✝¹ : Nonempty M
inst✝ : DecidableEq μ
p : Formula L μ
hμ : Nonempty μ
⊢ (Evalf s Empty.elim) (∀ᶠ* p) ↔ ∀ (ε : μ → M), (Evalf s ε) p
Tactic:
exact val_fvUnivClosure_inhabited
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.val_fvUnivClosure
Proof state before:
case neg
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
inst✝¹ : Nonempty M
inst✝ : DecidableEq μ
p : Formula L μ
hμ : ¬Nonempty μ
⊢ (Evalf s Empty.elim) (∀ᶠ* p) ↔ ∀ (ε : μ → M), (Evalf s ε) p
Tactic:
haveI hμ : IsEmpty μ := not_nonempty_iff.mp hμ
Proof state after:
case neg
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
inst✝¹ : Nonempty M
inst✝ : DecidableEq μ
p : Formula L μ
hμ✝ : ¬Nonempty μ
hμ : IsEmpty μ
⊢ (Evalf s Empty.elim) (∀ᶠ* p) ↔ ∀ (ε : μ → M), (Evalf s ε) p
Theorem: LO.FirstOrder.Semiformula.val_fvUnivClosure
Proof state before:
case neg
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
inst✝¹ : Nonempty M
inst✝ : DecidableEq μ
p : Formula L μ
hμ✝ : ¬Nonempty μ
hμ : IsEmpty μ
⊢ (Evalf s Empty.elim) (∀ᶠ* p) ↔ ∀ (ε : μ → M), (Evalf s ε) p
Tactic:
simp [Formula.fvUnivClosure_sentence p, IsEmpty.eq_elim]
Proof state after:
case neg
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
inst✝¹ : Nonempty M
inst✝ : DecidableEq μ
p : Formula L μ
hμ✝ : ¬Nonempty μ
hμ : IsEmpty μ
⊢ (Eval s Fin.isEmpty'.elim' hμ.elim') p ↔ (Evalf s hμ.elim') p
Theorem: LO.FirstOrder.Semiformula.val_fvUnivClosure
Proof state before:
case neg
n₂ : ℕ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
e₂ : Fin n₂ → M
ε : μ → M
ε₂ : μ₂ → M
inst✝¹ : Nonempty M
inst✝ : DecidableEq μ
p : Formula L μ
hμ✝ : ¬Nonempty μ
hμ : IsEmpty μ
⊢ (Eval s Fin.isEmpty'.elim' hμ.elim') p ↔ (Evalf s hμ.elim') p
Tactic:
simp [Matrix.empty_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.eval_ofEquiv_iff
Proof state before:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
⊢ (Eval (ofEquiv φ) e ε) ⊤ ↔ (Eval s (⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) ⊤
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.eval_ofEquiv_iff
Proof state before:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
⊢ (Eval (ofEquiv φ) e ε) ⊥ ↔ (Eval s (⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) ⊥
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.eval_ofEquiv_iff
Proof state before:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L μ x✝
⊢ (Eval (ofEquiv φ) e ε) (Semiformula.rel r v) ↔ (Eval s (⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) (Semiformula.rel r v)
Tactic:
simp [Function.comp, eval_rel, ofEquiv_rel φ, Structure.ofEquiv_val φ]
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.eval_ofEquiv_iff
Proof state before:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L μ x✝
⊢ (Eval (ofEquiv φ) e ε) (nrel r v) ↔ (Eval s (⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) (nrel r v)
Tactic:
simp [Function.comp, eval_nrel, ofEquiv_rel φ, Structure.ofEquiv_val φ]
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.eval_ofEquiv_iff
Proof state before:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p q : Semiformula L μ x✝
⊢ (Eval (ofEquiv φ) e ε) (p ⋏ q) ↔ (Eval s (⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) (p ⋏ q)
Tactic:
simp [eval_ofEquiv_iff (p := p), eval_ofEquiv_iff (p := q)]
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.eval_ofEquiv_iff
Proof state before:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p q : Semiformula L μ x✝
⊢ (Eval (ofEquiv φ) e ε) (p ⋎ q) ↔ (Eval s (⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) (p ⋎ q)
Tactic:
simp [eval_ofEquiv_iff (p := p), eval_ofEquiv_iff (p := q)]
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.eval_ofEquiv_iff
Proof state before:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
⊢ (Eval (ofEquiv φ) e ε) (∀' p) ↔ (Eval s (⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) (∀' p)
Tactic:
simp
Proof state after:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
⊢ (∀ (x : N), (Eval (ofEquiv φ) (x :> e) ε) p) ↔ ∀ (x : M), (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
Theorem: LO.FirstOrder.Structure.eval_ofEquiv_iff
Proof state before:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
⊢ (∀ (x : N), (Eval (ofEquiv φ) (x :> e) ε) p) ↔ ∀ (x : M), (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
Tactic:
exact
⟨fun h x => by simpa[Matrix.comp_vecCons''] using eval_ofEquiv_iff.mp (h (φ x)),
fun h x => eval_ofEquiv_iff.mpr (by simpa[Matrix.comp_vecCons''] using h (φ.symm x))⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.eval_ofEquiv_iff
Proof state before:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
h : ∀ (x : N), (Eval (ofEquiv φ) (x :> e) ε) p
x : M
⊢ (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
Tactic:
simpa[Matrix.comp_vecCons''] using eval_ofEquiv_iff.mp (h (φ x))
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.eval_ofEquiv_iff
Proof state before:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
h : ∀ (x : M), (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
x : N
⊢ (Eval s (⇑φ.symm ∘ (x :> e)) (⇑φ.symm ∘ ε)) p
Tactic:
simpa[Matrix.comp_vecCons''] using h (φ.symm x)
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.eval_ofEquiv_iff
Proof state before:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
⊢ (Eval (ofEquiv φ) e ε) (∃' p) ↔ (Eval s (⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) (∃' p)
Tactic:
simp
Proof state after:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
⊢ (∃ x, (Eval (ofEquiv φ) (x :> e) ε) p) ↔ ∃ x, (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
Theorem: LO.FirstOrder.Structure.eval_ofEquiv_iff
Proof state before:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
⊢ (∃ x, (Eval (ofEquiv φ) (x :> e) ε) p) ↔ ∃ x, (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
Tactic:
exact
⟨by rintro ⟨x, h⟩; exists φ.symm x; simpa[Matrix.comp_vecCons''] using eval_ofEquiv_iff.mp h,
by rintro ⟨x, h⟩; exists φ x; apply eval_ofEquiv_iff.mpr; simpa[Matrix.comp_vecCons''] using h⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.eval_ofEquiv_iff
Proof state before:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
⊢ (∃ x, (Eval (ofEquiv φ) (x :> e) ε) p) → ∃ x, (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
Tactic:
rintro ⟨x, h⟩
Proof state after:
case intro
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
x : N
h : (Eval (ofEquiv φ) (x :> e) ε) p
⊢ ∃ x, (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
Theorem: LO.FirstOrder.Structure.eval_ofEquiv_iff
Proof state before:
case intro
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
x : N
h : (Eval (ofEquiv φ) (x :> e) ε) p
⊢ ∃ x, (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
Tactic:
exists φ.symm x
Proof state after:
case intro
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
x : N
h : (Eval (ofEquiv φ) (x :> e) ε) p
⊢ (Eval s (φ.symm x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
Theorem: LO.FirstOrder.Structure.eval_ofEquiv_iff
Proof state before:
case intro
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
x : N
h : (Eval (ofEquiv φ) (x :> e) ε) p
⊢ (Eval s (φ.symm x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
Tactic:
simpa[Matrix.comp_vecCons''] using eval_ofEquiv_iff.mp h
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.eval_ofEquiv_iff
Proof state before:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
⊢ (∃ x, (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p) → ∃ x, (Eval (ofEquiv φ) (x :> e) ε) p
Tactic:
rintro ⟨x, h⟩
Proof state after:
case intro
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
x : M
h : (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
⊢ ∃ x, (Eval (ofEquiv φ) (x :> e) ε) p
Theorem: LO.FirstOrder.Structure.eval_ofEquiv_iff
Proof state before:
case intro
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
x : M
h : (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
⊢ ∃ x, (Eval (ofEquiv φ) (x :> e) ε) p
Tactic:
exists φ x
Proof state after:
case intro
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
x : M
h : (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
⊢ (Eval (ofEquiv φ) (φ x :> e) ε) p
Theorem: LO.FirstOrder.Structure.eval_ofEquiv_iff
Proof state before:
case intro
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
x : M
h : (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
⊢ (Eval (ofEquiv φ) (φ x :> e) ε) p
Tactic:
apply eval_ofEquiv_iff.mpr
Proof state after:
case intro
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
x : M
h : (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
⊢ (Eval s (⇑φ.symm ∘ (φ x :> e)) (⇑φ.symm ∘ ε)) p
Theorem: LO.FirstOrder.Structure.eval_ofEquiv_iff
Proof state before:
case intro
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
x : M
h : (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
⊢ (Eval s (⇑φ.symm ∘ (φ x :> e)) (⇑φ.symm ∘ ε)) p
Tactic:
simpa[Matrix.comp_vecCons''] using h
Proof state after:
no goals
Theorem: LO.FirstOrder.models_iff
Proof state before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
T U : Theory L
σ : Sentence L
⊢ M ⊧ₘ σ ↔ (Semiformula.Evalf s Empty.elim) σ
Tactic:
simp [models_def]
Proof state after:
no goals
Theorem: LO.FirstOrder.satisfiable_iff
Proof state before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
T U : Theory L
⊢ Semantics.Satisfiable (Struc L) T → ∃ M, ∃ (x : Nonempty M), ∃ x_1, M ⊧ₘ* T
Tactic:
rintro ⟨s, hs⟩
Proof state after:
case intro
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type u_1
inst✝ : Nonempty M
s✝ : Structure L M
T U : Theory L
s : Struc L
hs : s ⊧* T
⊢ ∃ M, ∃ (x : Nonempty M), ∃ x_1, M ⊧ₘ* T
Theorem: LO.FirstOrder.satisfiable_iff
Proof state before:
case intro
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type u_1
inst✝ : Nonempty M
s✝ : Structure L M
T U : Theory L
s : Struc L
hs : s ⊧* T
⊢ ∃ M, ∃ (x : Nonempty M), ∃ x_1, M ⊧ₘ* T
Tactic:
exact ⟨s.Dom, s.nonempty, s.struc, hs⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.satisfiable_iff
Proof state before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
T U : Theory L
⊢ (∃ M, ∃ (x : Nonempty M), ∃ x_1, M ⊧ₘ* T) → Semantics.Satisfiable (Struc L) T
Tactic:
rintro ⟨M, i, s, hT⟩
Proof state after:
case intro.intro.intro
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M✝ : Type u_1
inst✝ : Nonempty M✝
s✝ : Structure L M✝
T U : Theory L
M : Type v
i : Nonempty M
s : Structure L M
hT : M ⊧ₘ* T
⊢ Semantics.Satisfiable (Struc L) T