Theorem: LO.FirstOrder.Semiformula.substs_primrec (Logic/FirstOrder/Computability/Formula.lean)

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁸ : Primcodable α
inst✝⁷ : Primcodable μ
inst✝⁶ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Rel
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n n' : ℕ
this : Primrec₂ fun v p => (Rew.bind v fun x => &x).hom p
⊢ Primrec₂ fun v p => (Rew.substs v).hom p
Tactic:
exact this.of_eq <| by { intro v p; rw[Rew.eq_bind (Rew.substs v)]; simp[Function.comp] }
State after:
no goals

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁸ : Primcodable α
inst✝⁷ : Primcodable μ
inst✝⁶ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Rel
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n n' : ℕ
this : Primrec₂ fun v p => (Rew.bind v fun x => &x).hom p
⊢ ∀ (a : Fin n → Semiterm L μ n') (b : Semiformula L μ n), (Rew.bind a fun x => &x).hom b = (Rew.substs a).hom b
Tactic:
intro v p
State after:
L : Language
μ : Type v
α : Type u_1
inst✝⁸ : Primcodable α
inst✝⁷ : Primcodable μ
inst✝⁶ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Rel
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n n' : ℕ
this : Primrec₂ fun v p => (Rew.bind v fun x => &x).hom p
v : Fin n → Semiterm L μ n'
p : Semiformula L μ n
⊢ (Rew.bind v fun x => &x).hom p = (Rew.substs v).hom p

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁸ : Primcodable α
inst✝⁷ : Primcodable μ
inst✝⁶ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Rel
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n n' : ℕ
this : Primrec₂ fun v p => (Rew.bind v fun x => &x).hom p
v : Fin n → Semiterm L μ n'
p : Semiformula L μ n
⊢ (Rew.bind v fun x => &x).hom p = (Rew.substs v).hom p
Tactic:
rw[Rew.eq_bind (Rew.substs v)]
State after:
L : Language
μ : Type v
α : Type u_1
inst✝⁸ : Primcodable α
inst✝⁷ : Primcodable μ
inst✝⁶ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Rel
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n n' : ℕ
this : Primrec₂ fun v p => (Rew.bind v fun x => &x).hom p
v : Fin n → Semiterm L μ n'
p : Semiformula L μ n
⊢ (Rew.bind v fun x => &x).hom p = (Rew.bind (⇑(Rew.substs v) ∘ Semiterm.bvar) (⇑(Rew.substs v) ∘ Semiterm.fvar)).hom p

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁸ : Primcodable α
inst✝⁷ : Primcodable μ
inst✝⁶ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : (k : ℕ) → Primcodable (L.Rel k)
inst✝³ : UniformlyPrimcodable L.Rel
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n n' : ℕ
this : Primrec₂ fun v p => (Rew.bind v fun x => &x).hom p
v : Fin n → Semiterm L μ n'
p : Semiformula L μ n
⊢ (Rew.bind v fun x => &x).hom p = (Rew.bind (⇑(Rew.substs v) ∘ Semiterm.bvar) (⇑(Rew.substs v) ∘ Semiterm.fvar)).hom p
Tactic:
simp[Function.comp]
State after:
no goals