case intro.intro
α : Type u_1
β : Type ?u.161236
γ : Type ?u.161239
δ : Type ?u.161242
σ : Type ?u.161245
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → ℕ
h₂ : PrimrecRel fun a b => f a = b
g : α → ℕ
pg : Primrec g
hg : ∀ (x : α), f x ≤ g x
⊢ Primrec f
α : Type u_1
β : Type ?u.161236
γ : Type ?u.161239
δ : Type ?u.161242
σ : Type ?u.161245
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → ℕ
h₁ : PrimrecBounded f
h₂ : PrimrecRel fun a b => f a = b
⊢ Primrec f
rcases h₁ with ⟨g, pg, hg : ∀ x, f x ≤ g x⟩
case intro.intro
α : Type u_1
β : Type ?u.161236
γ : Type ?u.161239
δ : Type ?u.161242
σ : Type ?u.161245
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → ℕ
h₂ : PrimrecRel fun a b => f a = b
g : α → ℕ
pg : Primrec g
hg : ∀ (x : α), f x ≤ g x
n : α
⊢ Nat.findGreatest (fun b => f n = b) (g n) = f n
case intro.intro
α : Type u_1
β : Type ?u.161236
γ : Type ?u.161239
δ : Type ?u.161242
σ : Type ?u.161245
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → ℕ
h₂ : PrimrecRel fun a b => f a = b
g : α → ℕ
pg : Primrec g
hg : ∀ (x : α), f x ≤ g x
⊢ Primrec f
refine (nat_findGreatest pg h₂).of_eq fun n => ?_
no goals
case intro.intro
α : Type u_1
β : Type ?u.161236
γ : Type ?u.161239
δ : Type ?u.161242
σ : Type ?u.161245
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → ℕ
h₂ : PrimrecRel fun a b => f a = b
g : α → ℕ
pg : Primrec g
hg : ∀ (x : α), f x ≤ g x
n : α
⊢ Nat.findGreatest (fun b => f n = b) (g n) = f n
exact (Nat.findGreatest_spec (P := fun b => f n = b) (hg n) rfl).symm