internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Rew.eq_rewriteMap_of_funEqOn_fv
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
e : ξ₁ → ξ₂
inst✝ : DecidableEq ξ₁
t : Semiterm L ξ₁ n₁
f g : ξ₁ → Semiterm L ξ₂ n₂
h : Function.funEqOn (fun x => x ∈ t.fv) f g
⊢ (rewriteMap f) t = (rewriteMap g) t
Tactic:
induction t <;> simp [Rew.func]
Proof state after:
case fvar
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
e : ξ₁ → ξ₂
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
a✝ : ξ₁
h : Function.funEqOn (fun x => x ∈ (&a✝).fv) f g
⊢ f a✝ = g a✝

case func
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
e : ξ₁ → ξ₂
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L ξ₁ n₁
a_ih✝ :
  ∀ (a : Fin arity✝), Function.funEqOn (fun x => x ∈ (a✝ a).fv) f g → (rewriteMap f) (a✝ a) = (rewriteMap g) (a✝ a)
h : Function.funEqOn (fun x => x ∈ (func a✝¹ a✝).fv) f g
⊢ (fun i => (rewriteMap f) (a✝ i)) = fun i => (rewriteMap g) (a✝ i)
Theorem: LO.FirstOrder.Rew.eq_rewriteMap_of_funEqOn_fv
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
e : ξ₁ → ξ₂
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
x : ξ₁
h : Function.funEqOn (fun x_1 => x_1 ∈ (&x).fv) f g
⊢ f x = g x
Tactic:
case fvar x => exact h x (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_rewriteMap_of_funEqOn_fv
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
e : ξ₁ → ξ₂
inst✝ : DecidableEq ξ₁
f✝ g : ξ₁ → Semiterm L ξ₂ n₂
arity✝ : ℕ
f : L.Func arity✝
v : Fin arity✝ → Semiterm L ξ₁ n₁
ih : ∀ (a : Fin arity✝), Function.funEqOn (fun x => x ∈ (v a).fv) f✝ g → (rewriteMap f✝) (v a) = (rewriteMap g) (v a)
h : Function.funEqOn (fun x => x ∈ (func f v).fv) f✝ g
⊢ (fun i => (rewriteMap f✝) (v i)) = fun i => (rewriteMap g) (v i)
Tactic:
case func f v ih =>
  funext i
  exact ih i (fun x hx ↦ h x (by simp [Semiterm.fv_func]; exact ⟨i, hx⟩))
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_rewriteMap_of_funEqOn_fv
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
e : ξ₁ → ξ₂
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
x : ξ₁
h : Function.funEqOn (fun x_1 => x_1 ∈ (&x).fv) f g
⊢ f x = g x
Tactic:
exact h x (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_rewriteMap_of_funEqOn_fv
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
e : ξ₁ → ξ₂
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
x : ξ₁
h : Function.funEqOn (fun x_1 => x_1 ∈ (&x).fv) f g
⊢ (fun x_1 => x_1 ∈ (&x).fv) x
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_rewriteMap_of_funEqOn_fv
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
e : ξ₁ → ξ₂
inst✝ : DecidableEq ξ₁
f✝ g : ξ₁ → Semiterm L ξ₂ n₂
arity✝ : ℕ
f : L.Func arity✝
v : Fin arity✝ → Semiterm L ξ₁ n₁
ih : ∀ (a : Fin arity✝), Function.funEqOn (fun x => x ∈ (v a).fv) f✝ g → (rewriteMap f✝) (v a) = (rewriteMap g) (v a)
h : Function.funEqOn (fun x => x ∈ (func f v).fv) f✝ g
⊢ (fun i => (rewriteMap f✝) (v i)) = fun i => (rewriteMap g) (v i)
Tactic:
funext i
Proof state after:
case h
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
e : ξ₁ → ξ₂
inst✝ : DecidableEq ξ₁
f✝ g : ξ₁ → Semiterm L ξ₂ n₂
arity✝ : ℕ
f : L.Func arity✝
v : Fin arity✝ → Semiterm L ξ₁ n₁
ih : ∀ (a : Fin arity✝), Function.funEqOn (fun x => x ∈ (v a).fv) f✝ g → (rewriteMap f✝) (v a) = (rewriteMap g) (v a)
h : Function.funEqOn (fun x => x ∈ (func f v).fv) f✝ g
i : Fin arity✝
⊢ (rewriteMap f✝) (v i) = (rewriteMap g) (v i)
Theorem: LO.FirstOrder.Rew.eq_rewriteMap_of_funEqOn_fv
Proof state before:
case h
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
e : ξ₁ → ξ₂
inst✝ : DecidableEq ξ₁
f✝ g : ξ₁ → Semiterm L ξ₂ n₂
arity✝ : ℕ
f : L.Func arity✝
v : Fin arity✝ → Semiterm L ξ₁ n₁
ih : ∀ (a : Fin arity✝), Function.funEqOn (fun x => x ∈ (v a).fv) f✝ g → (rewriteMap f✝) (v a) = (rewriteMap g) (v a)
h : Function.funEqOn (fun x => x ∈ (func f v).fv) f✝ g
i : Fin arity✝
⊢ (rewriteMap f✝) (v i) = (rewriteMap g) (v i)
Tactic:
exact ih i (fun x hx ↦ h x (by simp [Semiterm.fv_func]; exact ⟨i, hx⟩))
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_rewriteMap_of_funEqOn_fv
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
e : ξ₁ → ξ₂
inst✝ : DecidableEq ξ₁
f✝ g : ξ₁ → Semiterm L ξ₂ n₂
arity✝ : ℕ
f : L.Func arity✝
v : Fin arity✝ → Semiterm L ξ₁ n₁
ih : ∀ (a : Fin arity✝), Function.funEqOn (fun x => x ∈ (v a).fv) f✝ g → (rewriteMap f✝) (v a) = (rewriteMap g) (v a)
h : Function.funEqOn (fun x => x ∈ (func f v).fv) f✝ g
i : Fin arity✝
x : ξ₁
hx : (fun x => x ∈ (v i).fv) x
⊢ (fun x => x ∈ (func f v).fv) x
Tactic:
simp [Semiterm.fv_func]
Proof state after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
e : ξ₁ → ξ₂
inst✝ : DecidableEq ξ₁
f✝ g : ξ₁ → Semiterm L ξ₂ n₂
arity✝ : ℕ
f : L.Func arity✝
v : Fin arity✝ → Semiterm L ξ₁ n₁
ih : ∀ (a : Fin arity✝), Function.funEqOn (fun x => x ∈ (v a).fv) f✝ g → (rewriteMap f✝) (v a) = (rewriteMap g) (v a)
h : Function.funEqOn (fun x => x ∈ (func f v).fv) f✝ g
i : Fin arity✝
x : ξ₁
hx : (fun x => x ∈ (v i).fv) x
⊢ ∃ a, x ∈ (v a).fv
Theorem: LO.FirstOrder.Rew.eq_rewriteMap_of_funEqOn_fv
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
e : ξ₁ → ξ₂
inst✝ : DecidableEq ξ₁
f✝ g : ξ₁ → Semiterm L ξ₂ n₂
arity✝ : ℕ
f : L.Func arity✝
v : Fin arity✝ → Semiterm L ξ₁ n₁
ih : ∀ (a : Fin arity✝), Function.funEqOn (fun x => x ∈ (v a).fv) f✝ g → (rewriteMap f✝) (v a) = (rewriteMap g) (v a)
h : Function.funEqOn (fun x => x ∈ (func f v).fv) f✝ g
i : Fin arity✝
x : ξ₁
hx : (fun x => x ∈ (v i).fv) x
⊢ ∃ a, x ∈ (v a).fv
Tactic:
exact ⟨i, hx⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.emb_eq_id
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
o : Type v₂
inst✝ : IsEmpty o
⊢ emb = Rew.id
Tactic:
ext x <;> simp
Proof state after:
case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
o : Type v₂
inst✝ : IsEmpty o
x : o
⊢ emb &x = &x
Theorem: LO.FirstOrder.Rew.emb_eq_id
Proof state before:
case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
o : Type v₂
inst✝ : IsEmpty o
x : o
⊢ emb &x = &x
Tactic:
exact isEmptyElim x
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_empty
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ : Rew L ξ₁ n₁ ξ₂ n₂
o : Type v₂
inst✝ : IsEmpty o
h : IsEmpty ξ₁
ω : Rew L ξ₁ 0 ξ₂ n
⊢ ω = empty
Tactic:
ext x
Proof state after:
case hb
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ : Rew L ξ₁ n₁ ξ₂ n₂
o : Type v₂
inst✝ : IsEmpty o
h : IsEmpty ξ₁
ω : Rew L ξ₁ 0 ξ₂ n
x : Fin 0
⊢ ω #x = empty #x

case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ : Rew L ξ₁ n₁ ξ₂ n₂
o : Type v₂
inst✝ : IsEmpty o
h : IsEmpty ξ₁
ω : Rew L ξ₁ 0 ξ₂ n
x : ξ₁
⊢ ω &x = empty &x
Theorem: LO.FirstOrder.Rew.eq_empty
Proof state before:
case hb
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ : Rew L ξ₁ n₁ ξ₂ n₂
o : Type v₂
inst✝ : IsEmpty o
h : IsEmpty ξ₁
ω : Rew L ξ₁ 0 ξ₂ n
x : Fin 0
⊢ ω #x = empty #x

case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ : Rew L ξ₁ n₁ ξ₂ n₂
o : Type v₂
inst✝ : IsEmpty o
h : IsEmpty ξ₁
ω : Rew L ξ₁ 0 ξ₂ n
x : ξ₁
⊢ ω &x = empty &x
Tactic:
{ exact x.elim0 }
Proof state after:
case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ : Rew L ξ₁ n₁ ξ₂ n₂
o : Type v₂
inst✝ : IsEmpty o
h : IsEmpty ξ₁
ω : Rew L ξ₁ 0 ξ₂ n
x : ξ₁
⊢ ω &x = empty &x
Theorem: LO.FirstOrder.Rew.eq_empty
Proof state before:
case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ : Rew L ξ₁ n₁ ξ₂ n₂
o : Type v₂
inst✝ : IsEmpty o
h : IsEmpty ξ₁
ω : Rew L ξ₁ 0 ξ₂ n
x : ξ₁
⊢ ω &x = empty &x
Tactic:
{ exact h.elim' x }
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_empty
Proof state before:
case hb
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ : Rew L ξ₁ n₁ ξ₂ n₂
o : Type v₂
inst✝ : IsEmpty o
h : IsEmpty ξ₁
ω : Rew L ξ₁ 0 ξ₂ n
x : Fin 0
⊢ ω #x = empty #x
Tactic:
exact x.elim0
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_empty
Proof state before:
case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ : Rew L ξ₁ n₁ ξ₂ n₂
o : Type v₂
inst✝ : IsEmpty o
h : IsEmpty ξ₁
ω : Rew L ξ₁ 0 ξ₂ n
x : ξ₁
⊢ ω &x = empty &x
Tactic:
exact h.elim' x
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.bShift_ne_zero
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
t : Semiterm L ξ n
⊢ bShift t ≠ #0
Tactic:
cases t <;> simp[Rew.func, Fin.succ_ne_zero]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.bShift_positive
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
t : Semiterm L ξ n
⊢ (bShift t).Positive
Tactic:
induction t <;> simp [Rew.func, *]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.positive_iff
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
t : Semiterm L ξ (n + 1)
⊢ t.Positive → ∃ t', t = bShift t'
Tactic:
induction t <;> simp
Proof state after:
case bvar
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
a✝ : Fin (n + 1)
⊢ 0 < a✝ → ∃ t', #a✝ = bShift t'

case fvar
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
a✝ : ξ
⊢ ∃ t', &a✝ = bShift t'

case func
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L ξ (n + 1)
a_ih✝ : ∀ (a : Fin arity✝), (a✝ a).Positive → ∃ t', a✝ a = bShift t'
⊢ (∀ (i : Fin arity✝), (a✝ i).Positive) → ∃ t', func a✝¹ a✝ = bShift t'
Theorem: LO.FirstOrder.Rew.positive_iff
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
x : Fin (n + 1)
⊢ 0 < x → ∃ t', #x = bShift t'
Tactic:
case bvar x =>
  intro hx; exact ⟨#(x.pred (Fin.pos_iff_ne_zero.mp hx)), by simp⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.positive_iff
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
x : ξ
⊢ ∃ t', &x = bShift t'
Tactic:
case fvar x => exact ⟨&x, by simp⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.positive_iff
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ (n + 1)
ih : ∀ (a : Fin k), (v a).Positive → ∃ t', v a = bShift t'
⊢ (∀ (i : Fin k), (v i).Positive) → ∃ t', func f v = bShift t'
Tactic:
case func k f v ih =>
  intro h
  have : ∀ i, ∃ t', v i = bShift t' := fun i => ih i (h i)
  choose w hw using this
  exact ⟨func f w, by simp [Rew.func]; funext i; exact hw i⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.positive_iff
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
x : Fin (n + 1)
⊢ 0 < x → ∃ t', #x = bShift t'
Tactic:
intro hx
Proof state after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
x : Fin (n + 1)
hx : 0 < x
⊢ ∃ t', #x = bShift t'
Theorem: LO.FirstOrder.Rew.positive_iff
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
x : Fin (n + 1)
hx : 0 < x
⊢ ∃ t', #x = bShift t'
Tactic:
exact ⟨#(x.pred (Fin.pos_iff_ne_zero.mp hx)), by simp⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.positive_iff
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
x : Fin (n + 1)
hx : 0 < x
⊢ #x = bShift #(x.pred ⋯)
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.positive_iff
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
x : ξ
⊢ ∃ t', &x = bShift t'
Tactic:
exact ⟨&x, by simp⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.positive_iff
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
x : ξ
⊢ &x = bShift &x
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.positive_iff
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ (n + 1)
ih : ∀ (a : Fin k), (v a).Positive → ∃ t', v a = bShift t'
⊢ (∀ (i : Fin k), (v i).Positive) → ∃ t', func f v = bShift t'
Tactic:
intro h
Proof state after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ (n + 1)
ih : ∀ (a : Fin k), (v a).Positive → ∃ t', v a = bShift t'
h : ∀ (i : Fin k), (v i).Positive
⊢ ∃ t', func f v = bShift t'
Theorem: LO.FirstOrder.Rew.positive_iff
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ (n + 1)
ih : ∀ (a : Fin k), (v a).Positive → ∃ t', v a = bShift t'
h : ∀ (i : Fin k), (v i).Positive
⊢ ∃ t', func f v = bShift t'
Tactic:
have : ∀ i, ∃ t', v i = bShift t' := fun i => ih i (h i)
Proof state after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ (n + 1)
ih : ∀ (a : Fin k), (v a).Positive → ∃ t', v a = bShift t'
h : ∀ (i : Fin k), (v i).Positive
this : ∀ (i : Fin k), ∃ t', v i = bShift t'
⊢ ∃ t', func f v = bShift t'
Theorem: LO.FirstOrder.Rew.positive_iff
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ (n + 1)
ih : ∀ (a : Fin k), (v a).Positive → ∃ t', v a = bShift t'
h : ∀ (i : Fin k), (v i).Positive
this : ∀ (i : Fin k), ∃ t', v i = bShift t'
⊢ ∃ t', func f v = bShift t'
Tactic:
choose w hw using this
Proof state after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ (n + 1)
ih : ∀ (a : Fin k), (v a).Positive → ∃ t', v a = bShift t'
h : ∀ (i : Fin k), (v i).Positive
w : Fin k → Semiterm L ξ n
hw : ∀ (i : Fin k), v i = bShift (w i)
⊢ ∃ t', func f v = bShift t'
Theorem: LO.FirstOrder.Rew.positive_iff
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ (n + 1)
ih : ∀ (a : Fin k), (v a).Positive → ∃ t', v a = bShift t'
h : ∀ (i : Fin k), (v i).Positive
w : Fin k → Semiterm L ξ n
hw : ∀ (i : Fin k), v i = bShift (w i)
⊢ ∃ t', func f v = bShift t'
Tactic:
exact ⟨func f w, by simp [Rew.func]; funext i; exact hw i⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.positive_iff
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ (n + 1)
ih : ∀ (a : Fin k), (v a).Positive → ∃ t', v a = bShift t'
h : ∀ (i : Fin k), (v i).Positive
w : Fin k → Semiterm L ξ n
hw : ∀ (i : Fin k), v i = bShift (w i)
⊢ func f v = bShift (func f w)
Tactic:
simp [Rew.func]
Proof state after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ (n + 1)
ih : ∀ (a : Fin k), (v a).Positive → ∃ t', v a = bShift t'
h : ∀ (i : Fin k), (v i).Positive
w : Fin k → Semiterm L ξ n
hw : ∀ (i : Fin k), v i = bShift (w i)
⊢ v = fun i => bShift (w i)
Theorem: LO.FirstOrder.Rew.positive_iff
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ (n + 1)
ih : ∀ (a : Fin k), (v a).Positive → ∃ t', v a = bShift t'
h : ∀ (i : Fin k), (v i).Positive
w : Fin k → Semiterm L ξ n
hw : ∀ (i : Fin k), v i = bShift (w i)
⊢ v = fun i => bShift (w i)
Tactic:
funext i
Proof state after:
case h
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ (n + 1)
ih : ∀ (a : Fin k), (v a).Positive → ∃ t', v a = bShift t'
h : ∀ (i : Fin k), (v i).Positive
w : Fin k → Semiterm L ξ n
hw : ∀ (i : Fin k), v i = bShift (w i)
i : Fin k
⊢ v i = bShift (w i)
Theorem: LO.FirstOrder.Rew.positive_iff
Proof state before:
case h
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ (n + 1)
ih : ∀ (a : Fin k), (v a).Positive → ∃ t', v a = bShift t'
h : ∀ (i : Fin k), (v i).Positive
w : Fin k → Semiterm L ξ n
hw : ∀ (i : Fin k), v i = bShift (w i)
i : Fin k
⊢ v i = bShift (w i)
Tactic:
exact hw i
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.positive_iff
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
t : Semiterm L ξ (n + 1)
⊢ (∃ t', t = bShift t') → t.Positive
Tactic:
rintro ⟨t', rfl⟩
Proof state after:
case intro
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
t' : Semiterm L ξ n
⊢ (bShift t').Positive
Theorem: LO.FirstOrder.Rew.positive_iff
Proof state before:
case intro
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
t' : Semiterm L ξ n
⊢ (bShift t').Positive
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.leftConcat_bShift_comp_bvar
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
⊢ (#0 :> ⇑bShift ∘ bvar) 0 = #0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.leftConcat_bShift_comp_bvar
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
⊢ ∀ (i : Fin n), (#0 :> ⇑bShift ∘ bvar) i.succ = #i.succ
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.bShift_comp_fvar
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
⊢ ∀ (x : ξ), (⇑bShift ∘ fvar) x = &x
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.substs_bvar
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
n' : ℕ
w : Fin n → Semiterm L ξ n'
x : Fin n
⊢ (substs w) #x = w x
Tactic:
simp[substs]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.substs_fvar
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
n' : ℕ
w : Fin n → Semiterm L ξ n'
x : ξ
⊢ (substs w) &x = &x
Tactic:
simp[substs]
Proof state after:
no goals