-- Mathlib/Computability/Primrec.lean
theorem subtype_val_iff {p : β → Prop} [DecidablePred p] {hp : PrimrecPred p} {f : α → Subtype p} :
    haveI := Primcodable.subtype hp
    (Primrec fun a => (f a).1) ↔ Primrec f

Proof state:
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype hp
h : Primrec fun a => ↑(f a)
⊢ Primrec f

Tactic:
refine Nat.Primrec.of_eq h fun n => ?_

Result:
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype hp
h : Primrec fun a => ↑(f a)
n : ℕ
⊢ encode (Option.map (fun a => ↑(f a)) (decode n)) = encode (Option.map f (decode n))

Proof state:
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype hp
⊢ (Primrec fun a => ↑(f a)) ↔ Primrec f

Tactic:
refine ⟨fun h => ?_, fun hf => subtype_val.comp hf⟩

Result:
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype hp
h : Primrec fun a => ↑(f a)
⊢ Primrec f

Proof state:
case some
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype hp
h : Primrec fun a => ↑(f a)
n : ℕ
a : α
⊢ encode ↑(f a) = encode (f a)

Tactic:
rfl

Result:
no goals

Proof state:
case none
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype hp
h : Primrec fun a => ↑(f a)
n : ℕ
⊢ encode (Option.map (fun a => ↑(f a)) none) = encode (Option.map f none)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
⊢ (Primrec fun a => ↑(f a)) ↔ Primrec f

Tactic:
letI := Primcodable.subtype hp

Result:
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype hp
⊢ (Primrec fun a => ↑(f a)) ↔ Primrec f

Proof state:
case some
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype hp
h : Primrec fun a => ↑(f a)
n : ℕ
a : α
⊢ encode (Option.map (fun a => ↑(f a)) (some a)) = encode (Option.map f (some a))

Tactic:
simp

Result:
case some
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype hp
h : Primrec fun a => ↑(f a)
n : ℕ
a : α
⊢ encode ↑(f a) = encode (f a)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype hp
h : Primrec fun a => ↑(f a)
n : ℕ
⊢ encode (Option.map (fun a => ↑(f a)) (decode n)) = encode (Option.map f (decode n))

Tactic:
rcases @decode α _ n with - | a

Result:
case none
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype hp
h : Primrec fun a => ↑(f a)
n : ℕ
⊢ encode (Option.map (fun a => ↑(f a)) none) = encode (Option.map f none)

case some
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype hp
h : Primrec fun a => ↑(f a)
n : ℕ
a : α
⊢ encode (Option.map (fun a => ↑(f a)) (some a)) = encode (Option.map f (some a))