internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Semiformula.eval_univItr
Proof state before:
case succ.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
k : ℕ
ih :
  ∀ {e : Fin n → M} {p : Semiformula L μ (n + k)},
    (Eval s e ε) (∀^[k] p) ↔ ∀ (e' : Fin k → M), (Eval s (Matrix.appendr e' e) ε) p
e : Fin n → M
p : Semiformula L μ (n + (k + 1))
⊢ (∀ (e' : Fin (k + 1) → M), (Eval s (Matrix.appendr e' e) ε) p) →
    ∀ (e' : Fin k → M) (x : M), (Eval s (x :> Matrix.appendr e' e) ε) p
Tactic:
intro h e' x
Proof state after:
case succ.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
k : ℕ
ih :
  ∀ {e : Fin n → M} {p : Semiformula L μ (n + k)},
    (Eval s e ε) (∀^[k] p) ↔ ∀ (e' : Fin k → M), (Eval s (Matrix.appendr e' e) ε) p
e : Fin n → M
p : Semiformula L μ (n + (k + 1))
h : ∀ (e' : Fin (k + 1) → M), (Eval s (Matrix.appendr e' e) ε) p
e' : Fin k → M
x : M
⊢ (Eval s (x :> Matrix.appendr e' e) ε) p
Theorem: LO.FirstOrder.Semiformula.eval_univItr
Proof state before:
case succ.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
k : ℕ
ih :
  ∀ {e : Fin n → M} {p : Semiformula L μ (n + k)},
    (Eval s e ε) (∀^[k] p) ↔ ∀ (e' : Fin k → M), (Eval s (Matrix.appendr e' e) ε) p
e : Fin n → M
p : Semiformula L μ (n + (k + 1))
h : ∀ (e' : Fin (k + 1) → M), (Eval s (Matrix.appendr e' e) ε) p
e' : Fin k → M
x : M
⊢ (Eval s (x :> Matrix.appendr e' e) ε) p
Tactic:
simpa using h (x :> e')
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_exItr
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
k : ℕ
e : Fin n → M
p : Semiformula L μ (n + k)
⊢ (Eval s e ε) (∃^[k] p) ↔ ∃ e', (Eval s (Matrix.appendr e' e) ε) p
Tactic:
induction' k with k ih generalizing e <;> simp [*, Matrix.empty_eq, exItr_succ]
Proof state after:
case succ
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
k : ℕ
ih : ∀ {e : Fin n → M} {p : Semiformula L μ (n + k)}, (Eval s e ε) (∃^[k] p) ↔ ∃ e', (Eval s (Matrix.appendr e' e) ε) p
e : Fin n → M
p : Semiformula L μ (n + (k + 1))
⊢ (∃ e' x, (Eval s (x :> Matrix.appendr e' e) ε) p) ↔ ∃ e', (Eval s (Matrix.appendr e' e) ε) p
Theorem: LO.FirstOrder.Semiformula.eval_exItr
Proof state before:
case succ
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
k : ℕ
ih : ∀ {e : Fin n → M} {p : Semiformula L μ (n + k)}, (Eval s e ε) (∃^[k] p) ↔ ∃ e', (Eval s (Matrix.appendr e' e) ε) p
e : Fin n → M
p : Semiformula L μ (n + (k + 1))
⊢ (∃ e' x, (Eval s (x :> Matrix.appendr e' e) ε) p) ↔ ∃ e', (Eval s (Matrix.appendr e' e) ε) p
Tactic:
constructor
Proof state after:
case succ.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
k : ℕ
ih : ∀ {e : Fin n → M} {p : Semiformula L μ (n + k)}, (Eval s e ε) (∃^[k] p) ↔ ∃ e', (Eval s (Matrix.appendr e' e) ε) p
e : Fin n → M
p : Semiformula L μ (n + (k + 1))
⊢ (∃ e' x, (Eval s (x :> Matrix.appendr e' e) ε) p) → ∃ e', (Eval s (Matrix.appendr e' e) ε) p

case succ.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
k : ℕ
ih : ∀ {e : Fin n → M} {p : Semiformula L μ (n + k)}, (Eval s e ε) (∃^[k] p) ↔ ∃ e', (Eval s (Matrix.appendr e' e) ε) p
e : Fin n → M
p : Semiformula L μ (n + (k + 1))
⊢ (∃ e', (Eval s (Matrix.appendr e' e) ε) p) → ∃ e' x, (Eval s (x :> Matrix.appendr e' e) ε) p
Theorem: LO.FirstOrder.Semiformula.eval_exItr
Proof state before:
case succ.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
k : ℕ
ih : ∀ {e : Fin n → M} {p : Semiformula L μ (n + k)}, (Eval s e ε) (∃^[k] p) ↔ ∃ e', (Eval s (Matrix.appendr e' e) ε) p
e : Fin n → M
p : Semiformula L μ (n + (k + 1))
⊢ (∃ e' x, (Eval s (x :> Matrix.appendr e' e) ε) p) → ∃ e', (Eval s (Matrix.appendr e' e) ε) p
Tactic:
rintro ⟨e', x, h⟩
Proof state after:
case succ.mp.intro.intro
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
k : ℕ
ih : ∀ {e : Fin n → M} {p : Semiformula L μ (n + k)}, (Eval s e ε) (∃^[k] p) ↔ ∃ e', (Eval s (Matrix.appendr e' e) ε) p
e : Fin n → M
p : Semiformula L μ (n + (k + 1))
e' : Fin k → M
x : M
h : (Eval s (x :> Matrix.appendr e' e) ε) p
⊢ ∃ e', (Eval s (Matrix.appendr e' e) ε) p
Theorem: LO.FirstOrder.Semiformula.eval_exItr
Proof state before:
case succ.mp.intro.intro
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
k : ℕ
ih : ∀ {e : Fin n → M} {p : Semiformula L μ (n + k)}, (Eval s e ε) (∃^[k] p) ↔ ∃ e', (Eval s (Matrix.appendr e' e) ε) p
e : Fin n → M
p : Semiformula L μ (n + (k + 1))
e' : Fin k → M
x : M
h : (Eval s (x :> Matrix.appendr e' e) ε) p
⊢ ∃ e', (Eval s (Matrix.appendr e' e) ε) p
Tactic:
exact ⟨x :> e', by simpa using h⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_exItr
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
k : ℕ
ih : ∀ {e : Fin n → M} {p : Semiformula L μ (n + k)}, (Eval s e ε) (∃^[k] p) ↔ ∃ e', (Eval s (Matrix.appendr e' e) ε) p
e : Fin n → M
p : Semiformula L μ (n + (k + 1))
e' : Fin k → M
x : M
h : (Eval s (x :> Matrix.appendr e' e) ε) p
⊢ (Eval s (Matrix.appendr (x :> e') e) ε) p
Tactic:
simpa using h
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_exItr
Proof state before:
case succ.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
k : ℕ
ih : ∀ {e : Fin n → M} {p : Semiformula L μ (n + k)}, (Eval s e ε) (∃^[k] p) ↔ ∃ e', (Eval s (Matrix.appendr e' e) ε) p
e : Fin n → M
p : Semiformula L μ (n + (k + 1))
⊢ (∃ e', (Eval s (Matrix.appendr e' e) ε) p) → ∃ e' x, (Eval s (x :> Matrix.appendr e' e) ε) p
Tactic:
rintro ⟨e, h⟩
Proof state after:
case succ.mpr.intro
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
k : ℕ
ih : ∀ {e : Fin n → M} {p : Semiformula L μ (n + k)}, (Eval s e ε) (∃^[k] p) ↔ ∃ e', (Eval s (Matrix.appendr e' e) ε) p
e✝ : Fin n → M
p : Semiformula L μ (n + (k + 1))
e : Fin (k + 1) → M
h : (Eval s (Matrix.appendr e e✝) ε) p
⊢ ∃ e' x, (Eval s (x :> Matrix.appendr e' e✝) ε) p
Theorem: LO.FirstOrder.Semiformula.eval_exItr
Proof state before:
case succ.mpr.intro
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
k : ℕ
ih : ∀ {e : Fin n → M} {p : Semiformula L μ (n + k)}, (Eval s e ε) (∃^[k] p) ↔ ∃ e', (Eval s (Matrix.appendr e' e) ε) p
e✝ : Fin n → M
p : Semiformula L μ (n + (k + 1))
e : Fin (k + 1) → M
h : (Eval s (Matrix.appendr e e✝) ε) p
⊢ ∃ e' x, (Eval s (x :> Matrix.appendr e' e✝) ε) p
Tactic:
exact ⟨Matrix.vecTail e, Matrix.vecHead e,
  by rw [←Matrix.appendr_cons, Matrix.cons_head_tail]; exact h⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_exItr
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
k : ℕ
ih : ∀ {e : Fin n → M} {p : Semiformula L μ (n + k)}, (Eval s e ε) (∃^[k] p) ↔ ∃ e', (Eval s (Matrix.appendr e' e) ε) p
e✝ : Fin n → M
p : Semiformula L μ (n + (k + 1))
e : Fin (k + 1) → M
h : (Eval s (Matrix.appendr e e✝) ε) p
⊢ (Eval s (Matrix.vecHead e :> Matrix.appendr (Matrix.vecTail e) e✝) ε) p
Tactic:
rw [←Matrix.appendr_cons, Matrix.cons_head_tail]
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
k : ℕ
ih : ∀ {e : Fin n → M} {p : Semiformula L μ (n + k)}, (Eval s e ε) (∃^[k] p) ↔ ∃ e', (Eval s (Matrix.appendr e' e) ε) p
e✝ : Fin n → M
p : Semiformula L μ (n + (k + 1))
e : Fin (k + 1) → M
h : (Eval s (Matrix.appendr e e✝) ε) p
⊢ (Eval s (Matrix.appendr e e✝) ε) p
Theorem: LO.FirstOrder.Semiformula.eval_exItr
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
k : ℕ
ih : ∀ {e : Fin n → M} {p : Semiformula L μ (n + k)}, (Eval s e ε) (∃^[k] p) ↔ ∃ e', (Eval s (Matrix.appendr e' e) ε) p
e✝ : Fin n → M
p : Semiformula L μ (n + (k + 1))
e : Fin (k + 1) → M
h : (Eval s (Matrix.appendr e e✝) ε) p
⊢ (Eval s (Matrix.appendr e e✝) ε) p
Tactic:
exact h
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_rew
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
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n₂
p : Semiformula L μ₁ n₁
⊢ (Eval s e₂ ε₂) (ω.hom p) ↔
    (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p
Tactic:
induction p using rec' generalizing n₂ <;> simp [*, Semiterm.val_rew, eval_rel, eval_nrel, Rew.rel, Rew.nrel]
Proof state after:
case hall
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
ε : μ → M
ε₂ : μ₂ → M
n₁ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {e₂ : Fin n₂ → M} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂),
    (Eval s e₂ ε₂) (ω.hom p✝) ↔
      (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
n₂ : ℕ
e₂ : Fin n₂ → M
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ (∀ (x : M),
      (Eval s (Semiterm.val s (x :> e₂) ε₂ ∘ ⇑ω.q ∘ Semiterm.bvar) (Semiterm.val s (x :> e₂) ε₂ ∘ ⇑ω.q ∘ Semiterm.fvar))
        p✝) ↔
    ∀ (x : M), (Eval s (x :> Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝

case hex
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
ε : μ → M
ε₂ : μ₂ → M
n₁ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {e₂ : Fin n₂ → M} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂),
    (Eval s e₂ ε₂) (ω.hom p✝) ↔
      (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
n₂ : ℕ
e₂ : Fin n₂ → M
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ (∃ x,
      (Eval s (Semiterm.val s (x :> e₂) ε₂ ∘ ⇑ω.q ∘ Semiterm.bvar) (Semiterm.val s (x :> e₂) ε₂ ∘ ⇑ω.q ∘ Semiterm.fvar))
        p✝) ↔
    ∃ x, (Eval s (x :> Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
Theorem: LO.FirstOrder.Semiformula.eval_rew
Proof state before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
ε : μ → M
ε₂ : μ₂ → M
n₁ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {e₂ : Fin n₂ → M} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂),
    (Eval s e₂ ε₂) (ω.hom p✝) ↔
      (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
n₂ : ℕ
e₂ : Fin n₂ → M
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ (∀ (x : M),
      (Eval s (Semiterm.val s (x :> e₂) ε₂ ∘ ⇑ω.q ∘ Semiterm.bvar) (Semiterm.val s (x :> e₂) ε₂ ∘ ⇑ω.q ∘ Semiterm.fvar))
        p✝) ↔
    ∀ (x : M), (Eval s (x :> Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
Tactic:
case hall => simp [Function.comp]; exact iff_of_eq $ forall_congr (fun x => by congr; funext i; cases i using Fin.cases <;> simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_rew
Proof state before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
ε : μ → M
ε₂ : μ₂ → M
n₁ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {e₂ : Fin n₂ → M} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂),
    (Eval s e₂ ε₂) (ω.hom p✝) ↔
      (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
n₂ : ℕ
e₂ : Fin n₂ → M
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ (∃ x,
      (Eval s (Semiterm.val s (x :> e₂) ε₂ ∘ ⇑ω.q ∘ Semiterm.bvar) (Semiterm.val s (x :> e₂) ε₂ ∘ ⇑ω.q ∘ Semiterm.fvar))
        p✝) ↔
    ∃ x, (Eval s (x :> Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
Tactic:
case hex => simp [Function.comp]; exact exists_congr (fun x => iff_of_eq $ by congr; funext i; cases i using Fin.cases <;> simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_rew
Proof state before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
ε : μ → M
ε₂ : μ₂ → M
n₁ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {e₂ : Fin n₂ → M} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂),
    (Eval s e₂ ε₂) (ω.hom p✝) ↔
      (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
n₂ : ℕ
e₂ : Fin n₂ → M
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ (∀ (x : M),
      (Eval s (Semiterm.val s (x :> e₂) ε₂ ∘ ⇑ω.q ∘ Semiterm.bvar) (Semiterm.val s (x :> e₂) ε₂ ∘ ⇑ω.q ∘ Semiterm.fvar))
        p✝) ↔
    ∀ (x : M), (Eval s (x :> Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
Tactic:
simp [Function.comp]
Proof state after:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
ε : μ → M
ε₂ : μ₂ → M
n₁ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {e₂ : Fin n₂ → M} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂),
    (Eval s e₂ ε₂) (ω.hom p✝) ↔
      (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
n₂ : ℕ
e₂ : Fin n₂ → M
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ (∀ (x : M), (Eval s (fun x_1 => Semiterm.val s (x :> e₂) ε₂ (ω.q #x_1)) fun x => Semiterm.val s e₂ ε₂ (ω &x)) p✝) ↔
    ∀ (x : M), (Eval s (x :> fun x => Semiterm.val s e₂ ε₂ (ω #x)) fun x => Semiterm.val s e₂ ε₂ (ω &x)) p✝
Theorem: LO.FirstOrder.Semiformula.eval_rew
Proof state before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
ε : μ → M
ε₂ : μ₂ → M
n₁ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {e₂ : Fin n₂ → M} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂),
    (Eval s e₂ ε₂) (ω.hom p✝) ↔
      (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
n₂ : ℕ
e₂ : Fin n₂ → M
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ (∀ (x : M), (Eval s (fun x_1 => Semiterm.val s (x :> e₂) ε₂ (ω.q #x_1)) fun x => Semiterm.val s e₂ ε₂ (ω &x)) p✝) ↔
    ∀ (x : M), (Eval s (x :> fun x => Semiterm.val s e₂ ε₂ (ω #x)) fun x => Semiterm.val s e₂ ε₂ (ω &x)) p✝
Tactic:
exact iff_of_eq $ forall_congr (fun x => by congr; funext i; cases i using Fin.cases <;> simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_rew
Proof state before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
ε : μ → M
ε₂ : μ₂ → M
n₁ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {e₂ : Fin n₂ → M} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂),
    (Eval s e₂ ε₂) (ω.hom p✝) ↔
      (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
n₂ : ℕ
e₂ : Fin n₂ → M
ω : Rew L μ₁ n✝ μ₂ n₂
x : M
⊢ (Eval s (fun x_1 => Semiterm.val s (x :> e₂) ε₂ (ω.q #x_1)) fun x => Semiterm.val s e₂ ε₂ (ω &x)) p✝ =
    (Eval s (x :> fun x => Semiterm.val s e₂ ε₂ (ω #x)) fun x => Semiterm.val s e₂ ε₂ (ω &x)) p✝
Tactic:
congr
Proof state after:
case e_a.e_e
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
ε : μ → M
ε₂ : μ₂ → M
n₁ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {e₂ : Fin n₂ → M} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂),
    (Eval s e₂ ε₂) (ω.hom p✝) ↔
      (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
n₂ : ℕ
e₂ : Fin n₂ → M
ω : Rew L μ₁ n✝ μ₂ n₂
x : M
⊢ (fun x_1 => Semiterm.val s (x :> e₂) ε₂ (ω.q #x_1)) = x :> fun x => Semiterm.val s e₂ ε₂ (ω #x)
Theorem: LO.FirstOrder.Semiformula.eval_rew
Proof state before:
case e_a.e_e
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
ε : μ → M
ε₂ : μ₂ → M
n₁ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {e₂ : Fin n₂ → M} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂),
    (Eval s e₂ ε₂) (ω.hom p✝) ↔
      (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
n₂ : ℕ
e₂ : Fin n₂ → M
ω : Rew L μ₁ n✝ μ₂ n₂
x : M
⊢ (fun x_1 => Semiterm.val s (x :> e₂) ε₂ (ω.q #x_1)) = x :> fun x => Semiterm.val s e₂ ε₂ (ω #x)
Tactic:
funext i
Proof state after:
case e_a.e_e.h
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
ε : μ → M
ε₂ : μ₂ → M
n₁ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {e₂ : Fin n₂ → M} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂),
    (Eval s e₂ ε₂) (ω.hom p✝) ↔
      (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
n₂ : ℕ
e₂ : Fin n₂ → M
ω : Rew L μ₁ n✝ μ₂ n₂
x : M
i : Fin (n✝ + 1)
⊢ Semiterm.val s (x :> e₂) ε₂ (ω.q #i) = (x :> fun x => Semiterm.val s e₂ ε₂ (ω #x)) i
Theorem: LO.FirstOrder.Semiformula.eval_rew
Proof state before:
case e_a.e_e.h
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
ε : μ → M
ε₂ : μ₂ → M
n₁ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {e₂ : Fin n₂ → M} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂),
    (Eval s e₂ ε₂) (ω.hom p✝) ↔
      (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
n₂ : ℕ
e₂ : Fin n₂ → M
ω : Rew L μ₁ n✝ μ₂ n₂
x : M
i : Fin (n✝ + 1)
⊢ Semiterm.val s (x :> e₂) ε₂ (ω.q #i) = (x :> fun x => Semiterm.val s e₂ ε₂ (ω #x)) i
Tactic:
cases i using Fin.cases <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_rew
Proof state before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
ε : μ → M
ε₂ : μ₂ → M
n₁ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {e₂ : Fin n₂ → M} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂),
    (Eval s e₂ ε₂) (ω.hom p✝) ↔
      (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
n₂ : ℕ
e₂ : Fin n₂ → M
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ (∃ x,
      (Eval s (Semiterm.val s (x :> e₂) ε₂ ∘ ⇑ω.q ∘ Semiterm.bvar) (Semiterm.val s (x :> e₂) ε₂ ∘ ⇑ω.q ∘ Semiterm.fvar))
        p✝) ↔
    ∃ x, (Eval s (x :> Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
Tactic:
simp [Function.comp]
Proof state after:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
ε : μ → M
ε₂ : μ₂ → M
n₁ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {e₂ : Fin n₂ → M} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂),
    (Eval s e₂ ε₂) (ω.hom p✝) ↔
      (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
n₂ : ℕ
e₂ : Fin n₂ → M
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ (∃ x, (Eval s (fun x_1 => Semiterm.val s (x :> e₂) ε₂ (ω.q #x_1)) fun x => Semiterm.val s e₂ ε₂ (ω &x)) p✝) ↔
    ∃ x, (Eval s (x :> fun x => Semiterm.val s e₂ ε₂ (ω #x)) fun x => Semiterm.val s e₂ ε₂ (ω &x)) p✝
Theorem: LO.FirstOrder.Semiformula.eval_rew
Proof state before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type w
s : Structure L M
n : ℕ
e : Fin n → M
ε : μ → M
ε₂ : μ₂ → M
n₁ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {n₂ : ℕ} {e₂ : Fin n₂ → M} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂),
    (Eval s e₂ ε₂) (ω.hom p✝) ↔
      (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p✝
n₂ : ℕ
e₂ : Fin n₂ → M
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ (∃ x, (Eval s (fun x_1 => Semiterm.val s (x :> e₂) ε₂ (ω.q #x_1)) fun x => Semiterm.val s e₂ ε₂ (ω &x)) p✝) ↔
    ∃ x, (Eval s (x :> fun x => Semiterm.val s e₂ ε₂ (ω #x)) fun x => Semiterm.val s e₂ ε₂ (ω &x)) p✝
Tactic:
exact exists_congr (fun x => iff_of_eq $ by congr; funext i; cases i using Fin.cases <;> simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_rew_q
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
n₁ : ℕ
x : M
e₂ : Fin n₂ → M
ε₂ : μ₂ → M
ω : Rew L μ₁ n₁ μ₂ n₂
p : Semiformula L μ₁ (n₁ + 1)
⊢ (Eval s (x :> e₂) ε₂) (ω.q.hom p) ↔
    (Eval s (x :> Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) p
Tactic:
simp [eval_rew, Function.comp]
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
n₁ : ℕ
x : M
e₂ : Fin n₂ → M
ε₂ : μ₂ → M
ω : Rew L μ₁ n₁ μ₂ n₂
p : Semiformula L μ₁ (n₁ + 1)
⊢ (Eval s (fun x_1 => Semiterm.val s (x :> e₂) ε₂ (ω.q #x_1)) fun x => Semiterm.val s e₂ ε₂ (ω &x)) p ↔
    (Eval s (x :> fun x => Semiterm.val s e₂ ε₂ (ω #x)) fun x => Semiterm.val s e₂ ε₂ (ω &x)) p
Theorem: LO.FirstOrder.Semiformula.eval_rew_q
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
n₁ : ℕ
x : M
e₂ : Fin n₂ → M
ε₂ : μ₂ → M
ω : Rew L μ₁ n₁ μ₂ n₂
p : Semiformula L μ₁ (n₁ + 1)
⊢ (Eval s (fun x_1 => Semiterm.val s (x :> e₂) ε₂ (ω.q #x_1)) fun x => Semiterm.val s e₂ ε₂ (ω &x)) p ↔
    (Eval s (x :> fun x => Semiterm.val s e₂ ε₂ (ω #x)) fun x => Semiterm.val s e₂ ε₂ (ω &x)) p
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
e₂✝ : Fin n₂ → M
ε : μ → M
ε₂✝ : μ₂ → M
n₁ : ℕ
x : M
e₂ : Fin n₂ → M
ε₂ : μ₂ → M
ω : Rew L μ₁ n₁ μ₂ n₂
p : Semiformula L μ₁ (n₁ + 1)
⊢ (Eval s (fun x_1 => Semiterm.val s (x :> e₂) ε₂ (ω.q #x_1)) fun x => Semiterm.val s e₂ ε₂ (ω &x)) p =
    (Eval s (x :> fun x => Semiterm.val s e₂ ε₂ (ω #x)) fun x => Semiterm.val s e₂ ε₂ (ω &x)) p
Theorem: LO.FirstOrder.Semiformula.eval_rew_q
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
e₂✝ : Fin n₂ → M
ε : μ → M
ε₂✝ : μ₂ → M
n₁ : ℕ
x : M
e₂ : Fin n₂ → M
ε₂ : μ₂ → M
ω : Rew L μ₁ n₁ μ₂ n₂
p : Semiformula L μ₁ (n₁ + 1)
⊢ (Eval s (fun x_1 => Semiterm.val s (x :> e₂) ε₂ (ω.q #x_1)) fun x => Semiterm.val s e₂ ε₂ (ω &x)) p =
    (Eval s (x :> fun x => Semiterm.val s e₂ ε₂ (ω #x)) fun x => Semiterm.val s e₂ ε₂ (ω &x)) p
Tactic:
congr 2
Proof state after:
case a.e_a.e_e
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
n₁ : ℕ
x : M
e₂ : Fin n₂ → M
ε₂ : μ₂ → M
ω : Rew L μ₁ n₁ μ₂ n₂
p : Semiformula L μ₁ (n₁ + 1)
⊢ (fun x_1 => Semiterm.val s (x :> e₂) ε₂ (ω.q #x_1)) = x :> fun x => Semiterm.val s e₂ ε₂ (ω #x)
Theorem: LO.FirstOrder.Semiformula.eval_rew_q
Proof state before:
case a.e_a.e_e
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
n₁ : ℕ
x : M
e₂ : Fin n₂ → M
ε₂ : μ₂ → M
ω : Rew L μ₁ n₁ μ₂ n₂
p : Semiformula L μ₁ (n₁ + 1)
⊢ (fun x_1 => Semiterm.val s (x :> e₂) ε₂ (ω.q #x_1)) = x :> fun x => Semiterm.val s e₂ ε₂ (ω #x)
Tactic:
funext x
Proof state after:
case a.e_a.e_e.h
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
n₁ : ℕ
x✝ : M
e₂ : Fin n₂ → M
ε₂ : μ₂ → M
ω : Rew L μ₁ n₁ μ₂ n₂
p : Semiformula L μ₁ (n₁ + 1)
x : Fin (n₁ + 1)
⊢ Semiterm.val s (x✝ :> e₂) ε₂ (ω.q #x) = (x✝ :> fun x => Semiterm.val s e₂ ε₂ (ω #x)) x