-- Mathlib/Computability/Partrec.lean
theorem fix {f : α →. σ ⊕ α} (hf : Partrec f) : Partrec (PFun.fix f)

Proof state:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α →. σ ⊕ α
hf : Partrec f
F : α → ℕ →. σ ⊕ α :=
  fun a n => Nat.rec (Part.some (Sum.inr a)) (fun x IH => IH.bind fun s => Sum.casesOn s (fun x => Part.some s) f) n
hF : Partrec₂ F
⊢ Partrec f.fix

Tactic:
let p a n := @Part.map _ Bool (fun s => Sum.casesOn s (fun _ => true) fun _ => false) (F a n)

Result:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α →. σ ⊕ α
hf : Partrec f
F : α → ℕ →. σ ⊕ α :=
  fun a n => Nat.rec (Part.some (Sum.inr a)) (fun x IH => IH.bind fun s => Sum.casesOn s (fun x => Part.some s) f) n
hF : Partrec₂ F
p : α → ℕ → Part Bool := fun a n => Part.map (fun s => Sum.casesOn s (fun x => true) fun x => false) (F a n)
⊢ Partrec f.fix

Proof state:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α →. σ ⊕ α
hf : Partrec f
F : α → ℕ →. σ ⊕ α :=
  fun a n => Nat.rec (Part.some (Sum.inr a)) (fun x IH => IH.bind fun s => Sum.casesOn s (fun x => Part.some s) f) n
hF : Partrec₂ F
p : α → ℕ → Part Bool := fun a n => Part.map (fun s => Sum.casesOn s (fun x => true) fun x => false) (F a n)
⊢ Partrec f.fix

Tactic:
have hp : Partrec₂ p :=
  hF.map ((sumCasesOn Computable.id (const true).to₂ (const false).to₂).comp snd).to₂

Result:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α →. σ ⊕ α
hf : Partrec f
F : α → ℕ →. σ ⊕ α :=
  fun a n => Nat.rec (Part.some (Sum.inr a)) (fun x IH => IH.bind fun s => Sum.casesOn s (fun x => Part.some s) f) n
hF : Partrec₂ F
p : α → ℕ → Part Bool := fun a n => Part.map (fun s => Sum.casesOn s (fun x => true) fun x => false) (F a n)
hp : Partrec₂ p
⊢ Partrec f.fix

Proof state:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α →. σ ⊕ α
hf : Partrec f
F : α → ℕ →. σ ⊕ α :=
  fun a n => Nat.rec (Part.some (Sum.inr a)) (fun x IH => IH.bind fun s => Sum.casesOn s (fun x => Part.some s) f) n
⊢ Partrec f.fix

Tactic:
have hF : Partrec₂ F :=
  Partrec.nat_rec snd (sumInr.comp fst).partrec
    (sumCasesOn_right (snd.comp snd) (snd.comp <| snd.comp fst).to₂ (hf.comp snd).to₂).to₂

Result:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α →. σ ⊕ α
hf : Partrec f
F : α → ℕ →. σ ⊕ α :=
  fun a n => Nat.rec (Part.some (Sum.inr a)) (fun x IH => IH.bind fun s => Sum.casesOn s (fun x => Part.some s) f) n
hF : Partrec₂ F
⊢ Partrec f.fix

Proof state:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α →. σ ⊕ α
hf : Partrec f
F : α → ℕ →. σ ⊕ α :=
  fun a n => Nat.rec (Part.some (Sum.inr a)) (fun x IH => IH.bind fun s => Sum.casesOn s (fun x => Part.some s) f) n
hF : Partrec₂ F
p : α → ℕ → Part Bool := fun a n => Part.map (fun s => Sum.casesOn s (fun x => true) fun x => false) (F a n)
hp : Partrec₂ p
⊢ Partrec f.fix

Tactic:
exact (hp.rfind.bind (hF.bind (sumCasesOn_right snd snd.to₂ none.to₂).to₂).to₂).of_eq fun a =>
  ext fun b => by simpa [p] using fix_aux f _ _

Result:
no goals

Proof state:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α →. σ ⊕ α
hf : Partrec f
⊢ Partrec f.fix

Tactic:
let F : α → ℕ →. σ ⊕ α := fun a n =>
  n.rec (some (Sum.inr a)) fun _ IH => IH.bind fun s => Sum.casesOn s (fun _ => Part.some s) f

Result:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α →. σ ⊕ α
hf : Partrec f
F : α → ℕ →. σ ⊕ α :=
  fun a n => Nat.rec (Part.some (Sum.inr a)) (fun x IH => IH.bind fun s => Sum.casesOn s (fun x => Part.some s) f) n
⊢ Partrec f.fix

Proof state:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α →. σ ⊕ α
hf : Partrec f
F : α → ℕ →. σ ⊕ α :=
  fun a n => Nat.rec (Part.some (Sum.inr a)) (fun x IH => IH.bind fun s => Sum.casesOn s (fun x => Part.some s) f) n
hF : Partrec₂ F
p : α → ℕ → Part Bool := fun a n => Part.map (fun s => Sum.casesOn s (fun x => true) fun x => false) (F a n)
hp : Partrec₂ p
a : α
b : σ
⊢ (b ∈
      (Nat.rfind (p a)).bind fun b =>
        (F (a, b).1 (a, b).2).bind fun b_1 =>
          Sum.casesOn ((a, b), b_1).2 (fun b_2 => Part.some (((a, b), b_1), b_2).2) fun b => Part.none) ↔
    b ∈ f.fix a

Tactic:
simpa [p] using fix_aux f _ _

Result:
no goals