Theorem: Primrec.w_mk₀ (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 : σ → α
h : ∀ (x : σ), IsEmpty (β (f x))
hf : Primrec f
v : {x : σ} → β (f x) → WType β
⊢ Primrec fun x => WType.mk (f x) v
Tactic:
have : Primrec (fun x => Nat.pair 1 (Nat.pair (encode $ f x) 0) : σ → ℕ) :=
  Primrec₂.natPair.comp (const 1) (Primrec₂.natPair.comp (Primrec.encode.comp hf) (const 0))
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 : σ → α
h : ∀ (x : σ), IsEmpty (β (f x))
hf : Primrec f
v : {x : σ} → β (f x) → WType β
this : Primrec fun x => Nat.pair 1 ((encode (f x)).pair 0)
⊢ Primrec fun x => WType.mk (f x) v

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 : σ → α
h : ∀ (x : σ), IsEmpty (β (f x))
hf : Primrec f
v : {x : σ} → β (f x) → WType β
this : Primrec fun x => Nat.pair 1 ((encode (f x)).pair 0)
⊢ Primrec fun x => WType.mk (f x) v
Tactic:
exact Primrec.encode_iff.mp (this.of_eq $ fun x => by simp[encode_mk_eq, encode_fintypeArrow_isEmpty])
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 : σ → α
h : ∀ (x : σ), IsEmpty (β (f x))
hf : Primrec f
v : {x : σ} → β (f x) → WType β
this : Primrec fun x => Nat.pair 1 ((encode (f x)).pair 0)
x : σ
⊢ Nat.pair 1 ((encode (f x)).pair 0) = encode (WType.mk (f x) v)
Tactic:
simp[encode_mk_eq, encode_fintypeArrow_isEmpty]
State after:
no goals