α : Type u_2
β : Type u_1
γ : Type ?u.356695
σ : Type ?u.356698
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
h : ∀ (a : α), Option.isSome (f a) = true
hf : Primrec f
⊢ Primrec fun a => Option.get (f a) (_ : Option.isSome (f a) = true)
α : Type u_2
β : Type u_1
γ : Type ?u.356695
σ : Type ?u.356698
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
h : ∀ (a : α), Option.isSome (f a) = true
⊢ Primrec f → Primrec fun a => Option.get (f a) (_ : Option.isSome (f a) = true)
intro hf
α : Type u_2
β : Type u_1
γ : Type ?u.356695
σ : Type ?u.356698
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
h : ∀ (a : α), Option.isSome (f a) = true
hf : Primrec f
n : ℕ
⊢ Nat.pred (encode (Option.map f (decode n))) =
    encode (Option.map (fun a => Option.get (f a) (_ : Option.isSome (f a) = true)) (decode n))
α : Type u_2
β : Type u_1
γ : Type ?u.356695
σ : Type ?u.356698
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
h : ∀ (a : α), Option.isSome (f a) = true
hf : Primrec f
⊢ Primrec fun a => Option.get (f a) (_ : Option.isSome (f a) = true)
refine' (Nat.Primrec.pred.comp hf).of_eq fun n => _
α : Type u_2
β : Type u_1
γ : Type ?u.356695
σ : Type ?u.356698
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
h : ∀ (a : α), Option.isSome (f a) = true
hf : Primrec f
n : ℕ
x : Option α
hx : decode n = x
⊢ Nat.pred (encode (Option.map f x)) =
    encode (Option.map (fun a => Option.get (f a) (_ : Option.isSome (f a) = true)) x)
α : Type u_2
β : Type u_1
γ : Type ?u.356695
σ : Type ?u.356698
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
h : ∀ (a : α), Option.isSome (f a) = true
hf : Primrec f
n : ℕ
⊢ Nat.pred (encode (Option.map f (decode n))) =
    encode (Option.map (fun a => Option.get (f a) (_ : Option.isSome (f a) = true)) (decode n))
generalize hx : @decode α _ n = x
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.356695
σ : Type ?u.356698
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → Option β
h : ∀ (a : α), Option.isSome (f a) = true
hf : Primrec f
n : ℕ
x : Option α
hx : decode n = x
⊢ Nat.pred (encode (Option.map f x)) =
    encode (Option.map (fun a => Option.get (f a) (_ : Option.isSome (f a) = true)) x)
cases x <;> simp