Theorem: LO.FirstOrder.UTerm.func_primrec (Logic/FirstOrder/Computability/Term.lean)

State before:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
⊢ Primrec₂ fun a b => (equivW L μ) (func a b)
Tactic:
have h₁ := w_mkFin (β := Edge L μ)
  (fun f => (Sum.inr $ Sum.inr ⟨k, f⟩) : L.Func k → Node L μ)
  (fun _ => Fintype.card_fin k)
  (sum_inr.comp $ sum_inr.comp $ sigma_pair k)
State after:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
h₁ : Primrec₂ fun x w => WType.mk ((fun f => Sum.inr (Sum.inr ⟨k, f⟩)) x) ((fintypeArrowEquivFinArrow' ⋯).symm w)
⊢ Primrec₂ fun a b => (equivW L μ) (func a b)

State before:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
h₁ : Primrec₂ fun x w => WType.mk ((fun f => Sum.inr (Sum.inr ⟨k, f⟩)) x) ((fintypeArrowEquivFinArrow' ⋯).symm w)
⊢ Primrec₂ fun a b => (equivW L μ) (func a b)
Tactic:
have h₂ : Primrec (fun v => (fun i => equivW L μ (v i)) : (Fin k → UTerm L μ) → (Fin k → WType (Edge L μ))) :=
  finArrow_map Primrec.of_equiv k
State after:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
h₁ : Primrec₂ fun x w => WType.mk ((fun f => Sum.inr (Sum.inr ⟨k, f⟩)) x) ((fintypeArrowEquivFinArrow' ⋯).symm w)
h₂ : Primrec fun v i => (equivW L μ) (v i)
⊢ Primrec₂ fun a b => (equivW L μ) (func a b)

State before:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
h₁ : Primrec₂ fun x w => WType.mk ((fun f => Sum.inr (Sum.inr ⟨k, f⟩)) x) ((fintypeArrowEquivFinArrow' ⋯).symm w)
h₂ : Primrec fun v i => (equivW L μ) (v i)
⊢ Primrec₂ fun a b => (equivW L μ) (func a b)
Tactic:
exact (Primrec₂.comp₂ h₁ Primrec₂.left (h₂.comp₂ Primrec₂.right)).of_eq
  (fun a v => by simp[equivW, toW, Edge])
State after:
no goals

State before:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
h₁ : Primrec₂ fun x w => WType.mk ((fun f => Sum.inr (Sum.inr ⟨k, f⟩)) x) ((fintypeArrowEquivFinArrow' ⋯).symm w)
h₂ : Primrec fun v i => (equivW L μ) (v i)
a : L.Func k
v : Fin k → UTerm L μ
⊢ WType.mk ((fun f => Sum.inr (Sum.inr ⟨k, f⟩)) a) ((fintypeArrowEquivFinArrow' ⋯).symm fun i => (equivW L μ) (v i)) =
    (equivW L μ) (func a v)
Tactic:
simp[equivW, toW, Edge]
State after:
no goals