α : Type u_2
β : Type ?u.130006
γ : Type ?u.130009
σ : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
⊢ Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun i => h a (Nat.pred (f a))) (f a) =
    Nat.rec (Part.some (g a)) (fun n n_ih => h a n) (f a)
α : Type u_2
β : Type ?u.130006
γ : Type ?u.130009
σ : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
⊢ Nat.rec (↑g a) (fun y IH => Part.bind IH fun i => h (a, y, i).fst (Nat.pred (f (a, y, i).fst))) (f a) =
    Nat.casesOn (f a) (Part.some (g a)) (h a)
simp
case succ
α : Type u_2
β : Type ?u.130006
γ : Type ?u.130009
σ : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
⊢ (Part.bind (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun i => h a n) n) fun i => h a n) = h a n
α : Type u_2
β : Type ?u.130006
γ : Type ?u.130009
σ : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
⊢ Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun i => h a (Nat.pred (f a))) (f a) =
    Nat.rec (Part.some (g a)) (fun n n_ih => h a n) (f a)
cases' f a with n <;> simp
case succ.refine'_1
α : Type u_2
β : Type ?u.130006
γ : Type ?u.130009
σ : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ Part.bind (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun i => h a n) n) fun i => h a n
⊢ b ∈ h a n

case succ.refine'_2
α : Type u_2
β : Type ?u.130006
γ : Type ?u.130009
σ : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ h a n
⊢ b ∈ Part.bind (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun i => h a n) n) fun i => h a n
case succ
α : Type u_2
β : Type ?u.130006
γ : Type ?u.130009
σ : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
⊢ (Part.bind (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun i => h a n) n) fun i => h a n) = h a n
refine' ext fun b => ⟨fun H => _, fun H => _⟩
case succ.refine'_1.intro.intro
α : Type u_2
β : Type ?u.130006
γ : Type ?u.130009
σ : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ Part.bind (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun i => h a n) n) fun i => h a n
c : σ
left✝ : c ∈ Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun i => h a n) n
h₂ : b ∈ h a n
⊢ b ∈ h a n
case succ.refine'_1
α : Type u_2
β : Type ?u.130006
γ : Type ?u.130009
σ : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ Part.bind (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun i => h a n) n) fun i => h a n
⊢ b ∈ h a n
rcases mem_bind_iff.1 H with ⟨c, _, h₂⟩
no goals
case succ.refine'_1.intro.intro
α : Type u_2
β : Type ?u.130006
γ : Type ?u.130009
σ : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ Part.bind (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun i => h a n) n) fun i => h a n
c : σ
left✝ : c ∈ Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun i => h a n) n
h₂ : b ∈ h a n
⊢ b ∈ h a n
exact h₂
case succ.refine'_2
α : Type u_2
β : Type ?u.130006
γ : Type ?u.130009
σ : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ h a n
this : ∀ (m : ℕ), (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun x => h a n) m).Dom
⊢ b ∈ Part.bind (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun i => h a n) n) fun i => h a n
case succ.refine'_2
α : Type u_2
β : Type ?u.130006
γ : Type ?u.130009
σ : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ h a n
⊢ b ∈ Part.bind (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun i => h a n) n) fun i => h a n
have : ∀ m, (Nat.rec (motive := fun _ => Part σ)
    (Part.some (g a)) (fun y IH => IH.bind fun _ => h a n) m).Dom := by
  intro m
  induction m <;> simp [*, H.fst]
no goals
case succ.refine'_2
α : Type u_2
β : Type ?u.130006
γ : Type ?u.130009
σ : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ h a n
this : ∀ (m : ℕ), (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun x => h a n) m).Dom
⊢ b ∈ Part.bind (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun i => h a n) n) fun i => h a n
exact ⟨⟨this n, H.fst⟩, H.snd⟩
α : Type u_2
β : Type ?u.130006
γ : Type ?u.130009
σ : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ h a n
m : ℕ
⊢ (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun x => h a n) m).Dom
α : Type u_2
β : Type ?u.130006
γ : Type ?u.130009
σ : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ h a n
⊢ ∀ (m : ℕ), (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun x => h a n) m).Dom
intro m
no goals
α : Type u_2
β : Type ?u.130006
γ : Type ?u.130009
σ : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ h a n
m : ℕ
⊢ (Nat.rec (Part.some (g a)) (fun y IH => Part.bind IH fun x => h a n) m).Dom
induction m <;> simp [*, H.fst]