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✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (nrel r v).fvarList) ε ε'
⊢ (¬Structure.rel r fun i => Semiterm.val s e ε (v i)) ↔ ¬Structure.rel r fun i => Semiterm.val s e ε' (v i)
Tactic:
apply iff_of_eq
Proof state after:
case a
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✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (nrel r v).fvarList) ε ε'
⊢ (¬Structure.rel r fun i => Semiterm.val s e ε (v i)) = ¬Structure.rel r fun i => Semiterm.val s e ε' (v i)
Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
case a
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✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (nrel r v).fvarList) ε ε'
⊢ (¬Structure.rel r fun i => Semiterm.val s e ε (v i)) = ¬Structure.rel r fun i => Semiterm.val s e ε' (v i)
Tactic:
congr
Proof state after:
case a.e_a.e_a
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✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (nrel r v).fvarList) ε ε'
⊢ (fun i => Semiterm.val s e ε (v i)) = fun i => Semiterm.val s e ε' (v i)
Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
case a.e_a.e_a
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✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (nrel r v).fvarList) ε ε'
⊢ (fun i => Semiterm.val s e ε (v i)) = fun i => Semiterm.val s e ε' (v i)
Tactic:
funext i
Proof state after:
case a.e_a.e_a.h
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✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (nrel r v).fvarList) ε ε'
i : Fin k
⊢ Semiterm.val s e ε (v i) = Semiterm.val s e ε' (v i)
Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
case a.e_a.e_a.h
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✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (nrel r v).fvarList) ε ε'
i : Fin k
⊢ Semiterm.val s e ε (v i) = Semiterm.val s e ε' (v i)
Tactic:
exact Semiterm.val_eq_of_funEqOn (v i) (fun x hx ↦ h x (by simp [fvarList]; exact ⟨i, hx⟩))
Proof state after:
no goals
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✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (nrel r v).fvarList) ε ε'
i : Fin k
x : μ
hx : (v i).fvar? x
⊢ (fun x => x ∈ (nrel r v).fvarList) x
Tactic:
simp [fvarList]
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✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (nrel r v).fvarList) ε ε'
i : Fin k
x : μ
hx : (v i).fvar? x
⊢ ∃ a, x ∈ (v a).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✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (nrel r v).fvarList) ε ε'
i : Fin k
x : μ
hx : (v i).fvar? x
⊢ ∃ a, x ∈ (v a).fvarList
Tactic:
exact ⟨i, hx⟩
Proof state after:
no goals
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 q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fvarList) ε ε'
⊢ (Eval s e ε) (p ⋏ q) ↔ (Eval s e ε') (p ⋏ q)
Tactic:
simp
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 q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fvarList) ε ε'
⊢ (Eval s e ε) p ∧ (Eval s e ε) q ↔ (Eval s e ε') p ∧ (Eval s e ε') q
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 q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fvarList) ε ε'
⊢ (Eval s e ε) p ∧ (Eval s e ε) q ↔ (Eval s e ε') p ∧ (Eval s e ε') q
Tactic:
apply and_congr
Proof state after:
case h₁
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 q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fvarList) ε ε'
⊢ (Eval s e ε) p ↔ (Eval s e ε') p

case h₂
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 q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fvarList) ε ε'
⊢ (Eval s e ε) q ↔ (Eval s e ε') q
Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
case h₁
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 q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fvarList) ε ε'
⊢ (Eval s e ε) p ↔ (Eval s e ε') p
Tactic:
exact ihp (fun x (hx : x ∈ p.fvarList) ↦ h x $ by simp [hx, fvarList])
Proof state after:
no goals
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 q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fvarList) ε ε'
x : μ
hx : x ∈ p.fvarList
⊢ (fun x => x ∈ (p ⋏ q).fvarList) x
Tactic:
simp [hx, fvarList]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
case h₂
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 q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fvarList) ε ε'
⊢ (Eval s e ε) q ↔ (Eval s e ε') q
Tactic:
exact ihq (fun x (hx : x ∈ q.fvarList) ↦ h x $ by simp [hx, fvarList])
Proof state after:
no goals
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 q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fvarList) ε ε'
x : μ
hx : x ∈ q.fvarList
⊢ (fun x => x ∈ (p ⋏ q).fvarList) x
Tactic:
simp [hx, fvarList]
Proof state after:
no goals
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 q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fvarList) ε ε'
⊢ (Eval s e ε) (p ⋎ q) ↔ (Eval s e ε') (p ⋎ q)
Tactic:
simp
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 q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fvarList) ε ε'
⊢ (Eval s e ε) p ∨ (Eval s e ε) q ↔ (Eval s e ε') p ∨ (Eval s e ε') q
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 q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fvarList) ε ε'
⊢ (Eval s e ε) p ∨ (Eval s e ε) q ↔ (Eval s e ε') p ∨ (Eval s e ε') q
Tactic:
apply or_congr
Proof state after:
case h₁
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 q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fvarList) ε ε'
⊢ (Eval s e ε) p ↔ (Eval s e ε') p

case h₂
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 q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fvarList) ε ε'
⊢ (Eval s e ε) q ↔ (Eval s e ε') q
Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
case h₁
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 q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fvarList) ε ε'
⊢ (Eval s e ε) p ↔ (Eval s e ε') p
Tactic:
exact ihp (fun x (hx : x ∈ p.fvarList) ↦ h x $ by simp [hx, fvarList])
Proof state after:
no goals
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 q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fvarList) ε ε'
x : μ
hx : x ∈ p.fvarList
⊢ (fun x => x ∈ (p ⋎ q).fvarList) x
Tactic:
simp [hx, fvarList]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
case h₂
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 q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fvarList) ε ε'
⊢ (Eval s e ε) q ↔ (Eval s e ε') q
Tactic:
exact ihq (fun x (hx : x ∈ q.fvarList) ↦ h x $ by simp [hx, fvarList])
Proof state after:
no goals
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 q : Semiformula L μ n✝
ihp : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ p.fvarList) ε ε' → ((Eval s e ε) p ↔ (Eval s e ε') p)
ihq : ∀ {e : Fin n✝ → M}, Function.funEqOn (fun x => x ∈ q.fvarList) ε ε' → ((Eval s e ε) q ↔ (Eval s e ε') q)
e : Fin n✝ → M
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fvarList) ε ε'
x : μ
hx : x ∈ q.fvarList
⊢ (fun x => x ∈ (p ⋎ q).fvarList) x
Tactic:
simp [hx, fvarList]
Proof state after:
no goals
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) ε ε'
⊢ (Eval s e ε) (∀' p) ↔ (Eval s e ε') (∀' p)
Tactic:
simp
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), (Eval s (x :> e) ε) p) ↔ ∀ (x : M), (Eval s (x :> e) ε') p
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), (Eval s (x :> e) ε) p) ↔ ∀ (x : M), (Eval s (x :> e) ε') p
Tactic:
apply forall_congr'
Proof state after:
case h
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) ε ε'
⊢ ∀ (a : M), (Eval s (a :> e) ε) p ↔ (Eval s (a :> e) ε') p
Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
case h
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) ε ε'
⊢ ∀ (a : M), (Eval s (a :> e) ε) p ↔ (Eval s (a :> e) ε') p
Tactic:
intro x
Proof state after:
case h
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
⊢ (Eval s (x :> e) ε) p ↔ (Eval s (x :> e) ε') p
Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
case h
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
⊢ (Eval s (x :> e) ε) p ↔ (Eval s (x :> e) ε') p
Tactic:
exact ih (fun x hx ↦ h _ $ by simp [fvar?]; exact hx)
Proof state after:
no goals
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.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) ε ε'
⊢ (Eval s e ε) (∃' p) ↔ (Eval s e ε') (∃' p)
Tactic:
simp
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, (Eval s (x :> e) ε) p) ↔ ∃ x, (Eval s (x :> e) ε') p
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, (Eval s (x :> e) ε) p) ↔ ∃ x, (Eval s (x :> e) ε') p
Tactic:
apply exists_congr
Proof state after:
case h
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) ε ε'
⊢ ∀ (a : M), (Eval s (a :> e) ε) p ↔ (Eval s (a :> e) ε') p
Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
case h
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) ε ε'
⊢ ∀ (a : M), (Eval s (a :> e) ε) p ↔ (Eval s (a :> e) ε') p
Tactic:
intro x
Proof state after:
case h
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
⊢ (Eval s (x :> e) ε) p ↔ (Eval s (x :> e) ε') p
Theorem: LO.FirstOrder.Semiformula.eval_iff_of_funEqOn
Proof state before:
case h
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
⊢ (Eval s (x :> e) ε) p ↔ (Eval s (x :> e) ε') p
Tactic:
exact ih (fun x hx ↦ h _ $ by simp [fvar?]; exact hx)
Proof state after:
no goals