Theorem: Primrec.of_subtype_iff (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 β
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : β → { a // p a }
this : Primcodable (Subtype p) := Primcodable.subtype hp
hf : Primrec fun x => ↑(f x)
⊢ ∀ (n : β), encode ↑(f n) = encode (f n)
Tactic:
intro b
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 β
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : β → { a // p a }
this : Primcodable (Subtype p) := Primcodable.subtype hp
hf : Primrec fun x => ↑(f x)
b : β
⊢ encode ↑(f b) = encode (f b)

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 β
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : β → { a // p a }
this : Primcodable (Subtype p) := Primcodable.subtype hp
hf : Primrec fun x => ↑(f x)
b : β
⊢ encode ↑(f b) = encode (f b)
Tactic:
simp[Encodable.Subtype.encode_eq]
State after:
no goals