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

State before:
L : Language
μ : Type v
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
σ : Type u_1
γ : Type u_2
inst✝¹ : Primcodable σ
inst✝ : Primcodable γ
b : σ → ℕ → γ
e : σ → μ → γ
u : σ → ((k : ℕ) × L.Func k) × List γ → γ
t : σ → UTerm L μ
hb : Primrec₂ b
he : Primrec₂ e
hu : Primrec₂ u
ht : Primrec t
⊢ Primrec fun x => elim (b x) (e x) (fun {k} f v => u x (⟨k, f⟩, List.ofFn v)) (t x)
Tactic:
have hF : Primrec₂ (F b e u) :=
  sum_casesOn (fst.comp snd) (hb.comp₂ (fst.comp₂ Primrec₂.left) Primrec₂.right)
    (sum_casesOn snd (he.comp₂ (fst.comp₂ $ fst.comp₂ $ Primrec₂.left) Primrec₂.right)
      (hu.comp₂ (fst.comp₂ $ fst.comp₂ $ Primrec₂.left) (Primrec₂.pair.comp₂ snd (snd.comp₂ $ snd.comp₂ $ fst.comp₂ $ Primrec₂.left))))
State after:
L : Language
μ : Type v
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
σ : Type u_1
γ : Type u_2
inst✝¹ : Primcodable σ
inst✝ : Primcodable γ
b : σ → ℕ → γ
e : σ → μ → γ
u : σ → ((k : ℕ) × L.Func k) × List γ → γ
t : σ → UTerm L μ
hb : Primrec₂ b
he : Primrec₂ e
hu : Primrec₂ u
ht : Primrec t
hF : Primrec₂ (LO.FirstOrder.UTerm.F b e u)
⊢ Primrec fun x => elim (b x) (e x) (fun {k} f v => u x (⟨k, f⟩, List.ofFn v)) (t x)

State before:
L : Language
μ : Type v
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
σ : Type u_1
γ : Type u_2
inst✝¹ : Primcodable σ
inst✝ : Primcodable γ
b : σ → ℕ → γ
e : σ → μ → γ
u : σ → ((k : ℕ) × L.Func k) × List γ → γ
t : σ → UTerm L μ
hb : Primrec₂ b
he : Primrec₂ e
hu : Primrec₂ u
ht : Primrec t
hF : Primrec₂ (LO.FirstOrder.UTerm.F b e u)
⊢ Primrec fun x => elim (b x) (e x) (fun {k} f v => u x (⟨k, f⟩, List.ofFn v)) (t x)
Tactic:
exact (w_elimL_param hF (Primrec.of_equiv.comp ht)).of_eq (fun x => by simp[elim_eq])
State after:
no goals

State before:
L : Language
μ : Type v
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
σ : Type u_1
γ : Type u_2
inst✝¹ : Primcodable σ
inst✝ : Primcodable γ
b : σ → ℕ → γ
e : σ → μ → γ
u : σ → ((k : ℕ) × L.Func k) × List γ → γ
t : σ → UTerm L μ
hb : Primrec₂ b
he : Primrec₂ e
hu : Primrec₂ u
ht : Primrec t
hF : Primrec₂ (LO.FirstOrder.UTerm.F b e u)
x : σ
⊢ WType.elimL (fun p l => LO.FirstOrder.UTerm.F b e u x (p, l)) ((equivW L μ) (t x)) =
    elim (b x) (e x) (fun {k} f v => u x (⟨k, f⟩, List.ofFn v)) (t x)
Tactic:
simp[elim_eq]
State after:
no goals