Theorem: Primrec.encode_of_uniform (Logic/Vorspiel/Computability.lean)

State before:
σ✝ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ✝
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
σ : Type u_5
inst✝¹ : Primcodable σ
inst✝ : UniformlyPrimcodable β
b : σ → (a : α) × β a
hb : Primrec b
⊢ Primrec fun x => encode (b x).snd
Tactic:
have : Primrec (fun x => (Nat.unpair (encode (b x))).2) := snd.comp (unpair.comp $ Primrec.encode.comp hb)
State after:
σ✝ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ✝
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
σ : Type u_5
inst✝¹ : Primcodable σ
inst✝ : UniformlyPrimcodable β
b : σ → (a : α) × β a
hb : Primrec b
this : Primrec fun x => (encode (b x)).unpair.2
⊢ Primrec fun x => encode (b x).snd

State before:
σ✝ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ✝
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
σ : Type u_5
inst✝¹ : Primcodable σ
inst✝ : UniformlyPrimcodable β
b : σ → (a : α) × β a
hb : Primrec b
this : Primrec fun x => (encode (b x)).unpair.2
⊢ Primrec fun x => encode (b x).snd
Tactic:
exact this.of_eq <| by
  intro x
  rcases b x with ⟨a, b⟩
  simp[encode_sigma_val]
State after:
no goals

State before:
σ✝ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ✝
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
σ : Type u_5
inst✝¹ : Primcodable σ
inst✝ : UniformlyPrimcodable β
b : σ → (a : α) × β a
hb : Primrec b
this : Primrec fun x => (encode (b x)).unpair.2
⊢ ∀ (n : σ), (encode (b n)).unpair.2 = encode (b n).snd
Tactic:
intro x
State after:
σ✝ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ✝
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
σ : Type u_5
inst✝¹ : Primcodable σ
inst✝ : UniformlyPrimcodable β
b : σ → (a : α) × β a
hb : Primrec b
this : Primrec fun x => (encode (b x)).unpair.2
x : σ
⊢ (encode (b x)).unpair.2 = encode (b x).snd

State before:
σ✝ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ✝
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
σ : Type u_5
inst✝¹ : Primcodable σ
inst✝ : UniformlyPrimcodable β
b : σ → (a : α) × β a
hb : Primrec b
this : Primrec fun x => (encode (b x)).unpair.2
x : σ
⊢ (encode (b x)).unpair.2 = encode (b x).snd
Tactic:
rcases b x with ⟨a, b⟩
State after:
case mk
σ✝ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ✝
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
σ : Type u_5
inst✝¹ : Primcodable σ
inst✝ : UniformlyPrimcodable β
b✝ : σ → (a : α) × β a
hb : Primrec b✝
this : Primrec fun x => (encode (b✝ x)).unpair.2
x : σ
a : α
b : β a
⊢ (encode ⟨a, b⟩).unpair.2 = encode ⟨a, b⟩.snd

State before:
case mk
σ✝ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ✝
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
σ : Type u_5
inst✝¹ : Primcodable σ
inst✝ : UniformlyPrimcodable β
b✝ : σ → (a : α) × β a
hb : Primrec b✝
this : Primrec fun x => (encode (b✝ x)).unpair.2
x : σ
a : α
b : β a
⊢ (encode ⟨a, b⟩).unpair.2 = encode ⟨a, b⟩.snd
Tactic:
simp[encode_sigma_val]
State after:
no goals