Theorem: Primrec.sigma_prod_right (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_7
β : α → Type u_5
γ : α → Type u_6
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : (a : α) → Primcodable (γ a)
inst✝¹ : UniformlyPrimcodable β
inst✝ : UniformlyPrimcodable γ
this : Primrec fun p => (encode p).unpair.1.pair (encode p).unpair.2.unpair.2
x✝ : (a : α) × β a × γ a
k : α
b : β k
v : γ k
⊢ (encode ⟨k, (b, v)⟩).unpair.1.pair (encode ⟨k, (b, v)⟩).unpair.2.unpair.2 =
    encode ⟨⟨k, (b, v)⟩.fst, ⟨k, (b, v)⟩.snd.2⟩
Tactic:
simp[encode_finArrow]
State after:
no goals