Theorem: Primrec.w_elimL_param (Logic/Vorspiel/W.lean)

State before:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : σ → α × List γ → γ
w : σ → WType β
hf : Primrec₂ f
hw : Primrec w
⊢ Primrec fun x => elimL (fun p l => f x (p, l)) (w x)
Tactic:
have : Primrec₂ (fun x w => elimL (fun p l => f x (p, l)) w : σ → WType β → γ) :=
Primrec₂.decode_iff₂.mp
  (by simp[decode_elimL_eq]
      exact (SubWType.primrec_elimDecode_param β hf).comp₂ Primrec₂.left
        (Primrec.pair (fst.comp $ Primrec.unpair.comp snd) (snd.comp $ Primrec.unpair.comp snd)).to₂)
State after:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : σ → α × List γ → γ
w : σ → WType β
hf : Primrec₂ f
hw : Primrec w
this : Primrec₂ fun x w => elimL (fun p l => f x (p, l)) w
⊢ Primrec fun x => elimL (fun p l => f x (p, l)) (w x)

State before:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : σ → α × List γ → γ
w : σ → WType β
hf : Primrec₂ f
hw : Primrec w
this : Primrec₂ fun x w => elimL (fun p l => f x (p, l)) w
⊢ Primrec fun x => elimL (fun p l => f x (p, l)) (w x)
Tactic:
exact this.comp Primrec.id hw
State after:
no goals

State before:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : σ → α × List γ → γ
w : σ → WType β
hf : Primrec₂ f
hw : Primrec w
⊢ Primrec₂ fun a n => Option.map (fun w => elimL (fun p l => f a (p, l)) w) (decode n)
Tactic:
simp[decode_elimL_eq]
State after:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : σ → α × List γ → γ
w : σ → WType β
hf : Primrec₂ f
hw : Primrec w
⊢ Primrec₂ fun a n => SubWType.elimDecode β (fun p l => f a (p, l)) n.unpair.1 n.unpair.2

State before:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : σ → α × List γ → γ
w : σ → WType β
hf : Primrec₂ f
hw : Primrec w
⊢ Primrec₂ fun a n => SubWType.elimDecode β (fun p l => f a (p, l)) n.unpair.1 n.unpair.2
Tactic:
exact (SubWType.primrec_elimDecode_param β hf).comp₂ Primrec₂.left
  (Primrec.pair (fst.comp $ Primrec.unpair.comp snd) (snd.comp $ Primrec.unpair.comp snd)).to₂
State after:
no goals