Theorem: Primrec.w_elimvL (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 γ
inst✝ : Inhabited (WType β)
fs : α → σ → σ
fγ : σ → α × List γ → γ
hfs : Primrec₂ fs
hfγ : Primrec₂ fγ
⊢ Primrec fun p => elimvL fs (fun x a l => fγ x (a, l)) p.1 p.2
Tactic:
have hfs : Primrec₂ (fun _ p => fs p.1 p.2 : σ × WType β → α × σ → σ) :=
  hfs.comp₂ (fst.comp₂ Primrec₂.right) (snd.comp₂ Primrec₂.right)
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 γ
inst✝ : Inhabited (WType β)
fs : α → σ → σ
fγ : σ → α × List γ → γ
hfs✝ : Primrec₂ fs
hfγ : Primrec₂ fγ
hfs : Primrec₂ fun x p => fs p.1 p.2
⊢ Primrec fun p => elimvL fs (fun x a l => fγ x (a, l)) p.1 p.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 γ
inst✝ : Inhabited (WType β)
fs : α → σ → σ
fγ : σ → α × List γ → γ
hfs✝ : Primrec₂ fs
hfγ : Primrec₂ fγ
hfs : Primrec₂ fun x p => fs p.1 p.2
⊢ Primrec fun p => elimvL fs (fun x a l => fγ x (a, l)) p.1 p.2
Tactic:
have hfγ : Primrec₂ (fun _ p => fγ p.1 p.2 : σ × WType β → σ × α × List γ → γ) :=
  hfγ.comp₂ (fst.comp₂ Primrec₂.right) (snd.comp₂ Primrec₂.right)
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 γ
inst✝ : Inhabited (WType β)
fs : α → σ → σ
fγ : σ → α × List γ → γ
hfs✝ : Primrec₂ fs
hfγ✝ : Primrec₂ fγ
hfs : Primrec₂ fun x p => fs p.1 p.2
hfγ : Primrec₂ fun x p => fγ p.1 p.2
⊢ Primrec fun p => elimvL fs (fun x a l => fγ x (a, l)) p.1 p.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 γ
inst✝ : Inhabited (WType β)
fs : α → σ → σ
fγ : σ → α × List γ → γ
hfs✝ : Primrec₂ fs
hfγ✝ : Primrec₂ fγ
hfs : Primrec₂ fun x p => fs p.1 p.2
hfγ : Primrec₂ fun x p => fγ p.1 p.2
⊢ Primrec fun p => elimvL fs (fun x a l => fγ x (a, l)) p.1 p.2
Tactic:
exact w_elimvL_param hfs hfγ fst snd
State after:
no goals