Theorem: LO.FirstOrder.Semiformula.emb_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 σ
⊢ Primrec ⇑Rew.emb.hom
Tactic:
rw[Rew.eq_bind Rew.emb]
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 σ
⊢ Primrec ⇑(Rew.bind (⇑Rew.emb ∘ Semiterm.bvar) (⇑Rew.emb ∘ Semiterm.fvar)).hom

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 σ
⊢ Primrec ⇑(Rew.bind (⇑Rew.emb ∘ Semiterm.bvar) (⇑Rew.emb ∘ Semiterm.fvar)).hom
Tactic:
simp[Function.comp]
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 σ
⊢ Primrec ⇑(Rew.bind (fun x => #x) fun x => Rew.emb &x).hom

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 σ
⊢ Primrec ⇑(Rew.bind (fun x => #x) fun x => Rew.emb &x).hom
Tactic:
exact bind_primrec (const _)
  (Primrec₂.option_some_iff.mp $ (Primrec₂.const none).of_eq <| by rintro _ ⟨⟩) Primrec.id
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 σ
⊢ Semiformula L Empty 0 → ∀ (b : Empty), none = some (Rew.emb &b)
Tactic:
rintro _ ⟨⟩
State after:
no goals