Theorem: WType.SubWType.primrec_elimDecode_param (Logic/Vorspiel/W.lean)

State before:
α : Type u_1
β : α → Type u_2
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
σ : Type u_3
γ : Type u_4
inst✝¹ : Primcodable σ
inst✝ : Primcodable γ
f : σ → α × List γ → γ
hf : Primrec₂ f
⊢ Primrec₂ fun x p => elimDecode β (fun a ih => f x (a, ih)) p.1 p.2
Tactic:
have : Primrec₂ (fun p ih => some $ elimDecodeG β (fun x a ih => f x (a, ih)) p.1 p.2 ih : σ × (ℕ × ℕ) → List (Option γ) → Option (Option γ)) :=
  option_some.comp (elimDecodeG_primrec β hf)
State after:
α : Type u_1
β : α → Type u_2
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
σ : Type u_3
γ : Type u_4
inst✝¹ : Primcodable σ
inst✝ : Primcodable γ
f : σ → α × List γ → γ
hf : Primrec₂ f
this : Primrec₂ fun p ih => some (WType.SubWType.elimDecodeG β (fun x a ih => f x (a, ih)) p.1 p.2 ih)
⊢ Primrec₂ fun x p => elimDecode β (fun a ih => f x (a, ih)) p.1 p.2

State before:
α : Type u_1
β : α → Type u_2
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
σ : Type u_3
γ : Type u_4
inst✝¹ : Primcodable σ
inst✝ : Primcodable γ
f : σ → α × List γ → γ
hf : Primrec₂ f
this : Primrec₂ fun p ih => some (WType.SubWType.elimDecodeG β (fun x a ih => f x (a, ih)) p.1 p.2 ih)
⊢ Primrec₂ fun x p => elimDecode β (fun a ih => f x (a, ih)) p.1 p.2
Tactic:
exact nat_strong_rec'2 _ this (by simp[elimDecodeG_eq_elimDecode β])
State after:
no goals

State before:
α : Type u_1
β : α → Type u_2
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
σ : Type u_3
γ : Type u_4
inst✝¹ : Primcodable σ
inst✝ : Primcodable γ
f : σ → α × List γ → γ
hf : Primrec₂ f
this : Primrec₂ fun p ih => some (WType.SubWType.elimDecodeG β (fun x a ih => f x (a, ih)) p.1 p.2 ih)
⊢ ∀ (a : σ) (n m : ℕ),
    some
        (WType.SubWType.elimDecodeG β (fun x a ih => f x (a, ih)) (a, n, m).1 (a, n, m).2
          (List.map (fun i => elimDecode β (fun a_1 ih => f a (a_1, ih)) i.unpair.1 i.unpair.2)
            (List.range (n.pair m)))) =
      some (elimDecode β (fun a_1 ih => f a (a_1, ih)) (n, m).1 (n, m).2)
Tactic:
simp[elimDecodeG_eq_elimDecode β]
State after:
no goals