internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Rew.q_map
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₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
x : ξ₁
⊢ (map b e).q &x = (map (0 :> Fin.succ ∘ b) e) &x
Tactic:
{ simp }
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_map
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₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
x : Fin (n₁ + 1)
⊢ (map b e).q #x = (map (0 :> Fin.succ ∘ b) e) #x
Tactic:
cases x using Fin.cases <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_map
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₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
x : ξ₁
⊢ (map b e).q &x = (map (0 :> Fin.succ ∘ b) e) &x
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_rewrite
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₂
f : ξ₁ → Semiterm L ξ₂ n
⊢ (rewrite f).q = rewrite (⇑bShift ∘ f)
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₂
f : ξ₁ → Semiterm L ξ₂ n
x : Fin (n + 1)
⊢ (rewrite f).q #x = (rewrite (⇑bShift ∘ f)) #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₂
f : ξ₁ → Semiterm L ξ₂ n
x : ξ₁
⊢ (rewrite f).q &x = (rewrite (⇑bShift ∘ f)) &x
Theorem: LO.FirstOrder.Rew.q_rewrite
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₂
f : ξ₁ → Semiterm L ξ₂ n
x : Fin (n + 1)
⊢ (rewrite f).q #x = (rewrite (⇑bShift ∘ f)) #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₂
f : ξ₁ → Semiterm L ξ₂ n
x : ξ₁
⊢ (rewrite f).q &x = (rewrite (⇑bShift ∘ f)) &x
Tactic:
{ cases x using Fin.cases <;> simp[rewriteMap] }
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₂
f : ξ₁ → Semiterm L ξ₂ n
x : ξ₁
⊢ (rewrite f).q &x = (rewrite (⇑bShift ∘ f)) &x
Theorem: LO.FirstOrder.Rew.q_rewrite
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₂
f : ξ₁ → Semiterm L ξ₂ n
x : ξ₁
⊢ (rewrite f).q &x = (rewrite (⇑bShift ∘ f)) &x
Tactic:
{ simp }
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_rewrite
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₂
f : ξ₁ → Semiterm L ξ₂ n
x : Fin (n + 1)
⊢ (rewrite f).q #x = (rewrite (⇑bShift ∘ f)) #x
Tactic:
cases x using Fin.cases <;> simp[rewriteMap]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_rewrite
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₂
f : ξ₁ → Semiterm L ξ₂ n
x : ξ₁
⊢ (rewrite f).q &x = (rewrite (⇑bShift ∘ f)) &x
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_rewriteMap
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 : ξ₁ → ξ₂
⊢ (rewriteMap e).q = rewriteMap e
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₂
e : ξ₁ → ξ₂
x : Fin (n + 1)
⊢ (rewriteMap e).q #x = (rewriteMap e) #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₂
e : ξ₁ → ξ₂
x : ξ₁
⊢ (rewriteMap e).q &x = (rewriteMap e) &x
Theorem: LO.FirstOrder.Rew.q_rewriteMap
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₂
e : ξ₁ → ξ₂
x : Fin (n + 1)
⊢ (rewriteMap e).q #x = (rewriteMap e) #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₂
e : ξ₁ → ξ₂
x : ξ₁
⊢ (rewriteMap e).q &x = (rewriteMap e) &x
Tactic:
{ cases x using Fin.cases <;> simp[rewriteMap] }
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₂
e : ξ₁ → ξ₂
x : ξ₁
⊢ (rewriteMap e).q &x = (rewriteMap e) &x
Theorem: LO.FirstOrder.Rew.q_rewriteMap
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₂
e : ξ₁ → ξ₂
x : ξ₁
⊢ (rewriteMap e).q &x = (rewriteMap e) &x
Tactic:
{ simp }
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_rewriteMap
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₂
e : ξ₁ → ξ₂
x : Fin (n + 1)
⊢ (rewriteMap e).q #x = (rewriteMap e) #x
Tactic:
cases x using Fin.cases <;> simp[rewriteMap]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_rewriteMap
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₂
e : ξ₁ → ξ₂
x : ξ₁
⊢ (rewriteMap e).q &x = (rewriteMap e) &x
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_emb
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₁
e : IsEmpty o
n : ℕ
⊢ emb.q = emb
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₁
e : IsEmpty o
n : ℕ
x : Fin (n + 1)
⊢ emb.q #x = emb #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₁
e : IsEmpty o
n : ℕ
x : o
⊢ emb.q &x = emb &x
Theorem: LO.FirstOrder.Rew.q_emb
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₁
e : IsEmpty o
n : ℕ
x : Fin (n + 1)
⊢ emb.q #x = emb #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₁
e : IsEmpty o
n : ℕ
x : o
⊢ emb.q &x = emb &x
Tactic:
{ cases x using Fin.cases <;> 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₁
e : IsEmpty o
n : ℕ
x : o
⊢ emb.q &x = emb &x
Theorem: LO.FirstOrder.Rew.q_emb
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₁
e : IsEmpty o
n : ℕ
x : o
⊢ emb.q &x = emb &x
Tactic:
{ exact e.elim x }
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_emb
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₁
e : IsEmpty o
n : ℕ
x : Fin (n + 1)
⊢ emb.q #x = emb #x
Tactic:
cases x using Fin.cases <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_emb
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₁
e : IsEmpty o
n : ℕ
x : o
⊢ emb.q &x = emb &x
Tactic:
exact e.elim x
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.qpow_emb
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₁
e : IsEmpty o
n k : ℕ
⊢ emb.qpow k = emb
Tactic:
induction k <;> simp[*]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_castLE
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 n' : ℕ
h : n ≤ n'
⊢ (castLE h).q = castLE ⋯
Tactic:
ext x <;> simp
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₂
n n' : ℕ
h : n ≤ n'
x : Fin (n + 1)
⊢ (castLE h).q #x = #(Fin.castLE ⋯ x)
Theorem: LO.FirstOrder.Rew.q_castLE
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₂
n n' : ℕ
h : n ≤ n'
x : Fin (n + 1)
⊢ (castLE h).q #x = #(Fin.castLE ⋯ x)
Tactic:
cases x using Fin.cases <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_toS
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₂
⊢ toS.q = bind ![#0] fun x => #x.succ
Tactic:
ext x <;> simp
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₂
x : Fin (0 + 1)
⊢ x = 0
Theorem: LO.FirstOrder.Rew.q_toS
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₂
x : Fin (0 + 1)
⊢ x = 0
Tactic:
cases x using Fin.cases <;> try simp
Proof state after:
case hb.succ
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 0
⊢ i✝.succ = 0
Theorem: LO.FirstOrder.Rew.q_toS
Proof state before:
case hb.zero
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 = 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_toS
Proof state before:
case hb.succ
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 0
⊢ i✝.succ = 0
Tactic:
exact Fin.elim0 (by assumption)
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_toS
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 0
⊢ Fin 0
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.qpow_castLE
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 n n' : ℕ
h : n ≤ n'
⊢ (castLE h).qpow k = castLE ⋯
Tactic:
induction k <;> simp[*]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_substs
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'
⊢ (substs w).q = substs (#0 :> ⇑bShift ∘ w)
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₂
n' : ℕ
w : Fin n → Semiterm L ξ n'
x : Fin (n + 1)
⊢ (substs w).q #x = (substs (#0 :> ⇑bShift ∘ w)) #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₂
n' : ℕ
w : Fin n → Semiterm L ξ n'
x : ξ
⊢ (substs w).q &x = (substs (#0 :> ⇑bShift ∘ w)) &x
Theorem: LO.FirstOrder.Rew.q_substs
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₂
n' : ℕ
w : Fin n → Semiterm L ξ n'
x : Fin (n + 1)
⊢ (substs w).q #x = (substs (#0 :> ⇑bShift ∘ w)) #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₂
n' : ℕ
w : Fin n → Semiterm L ξ n'
x : ξ
⊢ (substs w).q &x = (substs (#0 :> ⇑bShift ∘ w)) &x
Tactic:
{ cases x using Fin.cases <;> 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₂
n' : ℕ
w : Fin n → Semiterm L ξ n'
x : ξ
⊢ (substs w).q &x = (substs (#0 :> ⇑bShift ∘ w)) &x
Theorem: LO.FirstOrder.Rew.q_substs
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₂
n' : ℕ
w : Fin n → Semiterm L ξ n'
x : ξ
⊢ (substs w).q &x = (substs (#0 :> ⇑bShift ∘ w)) &x
Tactic:
{ simp }
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_substs
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₂
n' : ℕ
w : Fin n → Semiterm L ξ n'
x : Fin (n + 1)
⊢ (substs w).q #x = (substs (#0 :> ⇑bShift ∘ w)) #x
Tactic:
cases x using Fin.cases <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_substs
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₂
n' : ℕ
w : Fin n → Semiterm L ξ n'
x : ξ
⊢ (substs w).q &x = (substs (#0 :> ⇑bShift ∘ w)) &x
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_embSubsts
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 : ℕ
w : Fin k → Semiterm L ξ n
⊢ (embSubsts w).q = embSubsts (#0 :> ⇑bShift ∘ w)
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₂
k : ℕ
w : Fin k → Semiterm L ξ n
x : Fin (k + 1)
⊢ (embSubsts w).q #x = (embSubsts (#0 :> ⇑bShift ∘ w)) #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₂
k : ℕ
w : Fin k → Semiterm L ξ n
x : Empty
⊢ (embSubsts w).q &x = (embSubsts (#0 :> ⇑bShift ∘ w)) &x
Theorem: LO.FirstOrder.Rew.q_embSubsts
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₂
k : ℕ
w : Fin k → Semiterm L ξ n
x : Fin (k + 1)
⊢ (embSubsts w).q #x = (embSubsts (#0 :> ⇑bShift ∘ w)) #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₂
k : ℕ
w : Fin k → Semiterm L ξ n
x : Empty
⊢ (embSubsts w).q &x = (embSubsts (#0 :> ⇑bShift ∘ w)) &x
Tactic:
{ cases x using Fin.cases <;> 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₂
k : ℕ
w : Fin k → Semiterm L ξ n
x : Empty
⊢ (embSubsts w).q &x = (embSubsts (#0 :> ⇑bShift ∘ w)) &x
Theorem: LO.FirstOrder.Rew.q_embSubsts
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₂
k : ℕ
w : Fin k → Semiterm L ξ n
x : Empty
⊢ (embSubsts w).q &x = (embSubsts (#0 :> ⇑bShift ∘ w)) &x
Tactic:
{ simp; exact Empty.elim x }
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_embSubsts
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₂
k : ℕ
w : Fin k → Semiterm L ξ n
x : Fin (k + 1)
⊢ (embSubsts w).q #x = (embSubsts (#0 :> ⇑bShift ∘ w)) #x
Tactic:
cases x using Fin.cases <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.q_embSubsts
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₂
k : ℕ
w : Fin k → Semiterm L ξ n
x : Empty
⊢ (embSubsts w).q &x = (embSubsts (#0 :> ⇑bShift ∘ w)) &x
Tactic:
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₂
k : ℕ
w : Fin k → Semiterm L ξ n
x : Empty
⊢ bShift ((embSubsts w) &x) = (embSubsts (#0 :> ⇑bShift ∘ w)) &x
Theorem: LO.FirstOrder.Rew.q_embSubsts
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₂
k : ℕ
w : Fin k → Semiterm L ξ n
x : Empty
⊢ bShift ((embSubsts w) &x) = (embSubsts (#0 :> ⇑bShift ∘ w)) &x
Tactic:
exact Empty.elim x
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.shift_Injective
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₂
⊢ Function.LeftInverse ⇑(map id Nat.pred) ⇑shift
Tactic:
intros p
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₂
p : Semiterm L ℕ n
⊢ (map id Nat.pred) (shift p) = p
Theorem: LO.FirstOrder.Rew.shift_Injective
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₂
p : Semiterm L ℕ n
⊢ (map id Nat.pred) (shift p) = p
Tactic:
simp[←comp_app]
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₂
p : Semiterm L ℕ n
⊢ ((map id Nat.pred).comp shift) p = p
Theorem: LO.FirstOrder.Rew.shift_Injective
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₂
p : Semiterm L ℕ n
⊢ ((map id Nat.pred).comp shift) p = p
Tactic:
apply eq_id_of_eq <;> simp[comp_app]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.free_bvar_castSucc
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
⊢ free #x.castSucc = #x
Tactic:
simp[free]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.free_bvar_last
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₂
⊢ free #(Fin.last n) = &0
Tactic:
simp[free]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.free_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 : ℕ
⊢ free &x = &(x + 1)
Tactic:
simp[free]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.fix_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₂
x : Fin n
⊢ fix #x = #x.castSucc
Tactic:
simp[fix]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.fix_fvar_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₂
⊢ fix &0 = #(Fin.last n)
Tactic:
simp[fix]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.fix_fvar_succ
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 : ℕ
⊢ fix &(x + 1) = &x
Tactic:
simp[fix]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.free_comp_fix
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₂
⊢ Rew.comp free fix = Rew.id
Tactic:
ext x <;> simp[comp_app]
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₂
x : ℕ
⊢ free (fix &x) = &x
Theorem: LO.FirstOrder.Rew.free_comp_fix
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₂
x : ℕ
⊢ free (fix &x) = &x
Tactic:
{ cases x <;> simp }
Proof state after:
no goals