-- Mathlib/Computability/Partrec.lean
theorem fix_aux {α σ} (f : α →. σ ⊕ α) (a : α) (b : σ) :
    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
    (∃ n : ℕ,
        ((∃ b' : σ, Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ b : α, Sum.inr b ∈ F a m) ∧
          Sum.inl b ∈ F a n) ↔
      b ∈ PFun.fix f a

Proof state:
case refine_2.inr.intro.intro.intro.intro.inl
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
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
h : b ∈ f.fix a
a₁ : α
h₁ : b ∈ f.fix a₁
a₂ : α
h₂ : b ∈ f.fix a₂
IH :
  ∀ (a'' : α),
    Sum.inr a'' ∈ f a₂ →
      ∀ (k : ℕ), Sum.inr a'' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
k : ℕ
hk : Sum.inr a₂ ∈ F a k
a₃ : α
am₃ : Sum.inr a₃ ∈ f a₂
right✝ : b ∈ f.fix a₃
n : ℕ
hn₁ : Sum.inl b ∈ F a n
hn₂ : ∀ m < n, k.succ ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
m : ℕ
mn : m < n
km✝ : k ≤ m
km : k < m
⊢ ∃ a₂, Sum.inr a₂ ∈ F a m

Tactic:
exact hn₂ _ mn km

Result:
no goals

Proof state:
case refine_1.intro.intro.intro.succ.inr.intro.intro
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
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
this : ∀ (m : ℕ) (a' : α), Sum.inr a' ∈ F a m → b ∈ f.fix a' → b ∈ f.fix a
n✝ : ℕ
_x : ∃ b', Sum.inl b' ∈ F a (n✝ + 1)
h₁ : ∀ {m : ℕ}, m < n✝ + 1 → ∃ b, Sum.inr b ∈ F a m
a' : α
am' :
  Sum.inr a' ∈
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => IH.bind fun s => Sum.rec (fun val => Part.some s) (fun val => f val) s)
      n✝
fa' : Sum.inl b ∈ f a'
⊢ b ∈ f.fix a

Tactic:
exact this _ _ am' (PFun.mem_fix_iff.2 (Or.inl fa'))

Result:
no goals

Proof state:
case succ.intro.intro
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
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
n : ℕ
h₂ : Sum.inl b ∈ F a n
_x : ∃ b', Sum.inl b' ∈ F a n
h₁ : ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m
m : ℕ
IH : ∀ (a' : α), Sum.inr a' ∈ F a m → b ∈ f.fix a' → b ∈ f.fix a
a' : α
ba : b ∈ f.fix a'
a₂ : α
am₂ :
  Sum.inr a₂ ∈
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => IH.bind fun s => Sum.rec (fun val => Part.some s) (fun val => f val) s)
      m
fa₂ : Sum.inr a' ∈ f a₂
⊢ b ∈ f.fix a

Tactic:
exact IH _ am₂ (PFun.mem_fix_iff.2 (Or.inr ⟨_, fa₂, ba⟩))

Result:
no goals

Proof state:
case refine_1
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
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
h : ∃ n, ((∃ b', Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m) ∧ Sum.inl b ∈ F a n
⊢ b ∈ f.fix a

Tactic:
rcases h with ⟨n, ⟨_x, h₁⟩, h₂⟩

Result:
case refine_1.intro.intro.intro
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
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
n : ℕ
h₂ : Sum.inl b ∈ F a n
_x : ∃ b', Sum.inl b' ∈ F a n
h₁ : ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m
⊢ b ∈ f.fix a

Proof state:
case refine_2
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
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
h : b ∈ f.fix a
⊢ ∀ (a' : α),
    b ∈ f.fix a' → ∀ (k : ℕ), Sum.inr a' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m

Tactic:
intro a₁ h₁

Result:
case refine_2
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
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
h : b ∈ f.fix a
a₁ : α
h₁ : b ∈ f.fix a₁
⊢ ∀ (k : ℕ), Sum.inr a₁ ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m

Proof state:
case succ
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
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
n : ℕ
h₂ : Sum.inl b ∈ F a n
_x : ∃ b', Sum.inl b' ∈ F a n
h₁ : ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m
m : ℕ
IH : ∀ (a' : α), Sum.inr a' ∈ F a m → b ∈ f.fix a' → b ∈ f.fix a
a' : α
ba : b ∈ f.fix a'
am :
  ∃ b,
    Sum.inr b ∈
        Nat.rec (Part.some (Sum.inr a))
          (fun x IH => IH.bind fun s => Sum.rec (fun val => Part.some s) (fun val => f val) s) m ∧
      Sum.inr a' ∈ f b
⊢ b ∈ f.fix a

Tactic:
rcases am with ⟨a₂, am₂, fa₂⟩

Result:
case succ.intro.intro
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
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
n : ℕ
h₂ : Sum.inl b ∈ F a n
_x : ∃ b', Sum.inl b' ∈ F a n
h₁ : ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m
m : ℕ
IH : ∀ (a' : α), Sum.inr a' ∈ F a m → b ∈ f.fix a' → b ∈ f.fix a
a' : α
ba : b ∈ f.fix a'
a₂ : α
am₂ :
  Sum.inr a₂ ∈
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => IH.bind fun s => Sum.rec (fun val => Part.some s) (fun val => f val) s)
      m
fa₂ : Sum.inr a' ∈ f a₂
⊢ b ∈ f.fix a

Proof state:
case refine_1.intro.intro.intro.succ.inl
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
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
this : ∀ (m : ℕ) (a' : α), Sum.inr a' ∈ F a m → b ∈ f.fix a' → b ∈ f.fix a
n✝ : ℕ
_x : ∃ b', Sum.inl b' ∈ F a (n✝ + 1)
h₁ : ∀ {m : ℕ}, m < n✝ + 1 → ∃ b, Sum.inr b ∈ F a m
h₂ :
  Sum.inl b ∈
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => IH.bind fun s => Sum.rec (fun val => Part.some s) (fun val => f val) s)
      n✝
⊢ b ∈ f.fix a

Tactic:
obtain ⟨a', h⟩ := h₁ (Nat.lt_succ_self _)

Result:
case refine_1.intro.intro.intro.succ.inl.intro
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
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
this : ∀ (m : ℕ) (a' : α), Sum.inr a' ∈ F a m → b ∈ f.fix a' → b ∈ f.fix a
n✝ : ℕ
_x : ∃ b', Sum.inl b' ∈ F a (n✝ + 1)
h₁ : ∀ {m : ℕ}, m < n✝ + 1 → ∃ b, Sum.inr b ∈ F a m
h₂ :
  Sum.inl b ∈
    Nat.rec (Part.some (Sum.inr a)) (fun x IH => IH.bind fun s => Sum.rec (fun val => Part.some s) (fun val => f val) s)
      n✝
a' : α
h : Sum.inr a' ∈ F a n✝
⊢ b ∈ f.fix a

Proof state:
case refine_1.intro.intro.intro
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
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
n : ℕ
h₂ : Sum.inl b ∈ F a n
_x : ∃ b', Sum.inl b' ∈ F a n
h₁ : ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m
this : ∀ (m : ℕ) (a' : α), Sum.inr a' ∈ F a m → b ∈ f.fix a' → b ∈ f.fix a
⊢ b ∈ f.fix a

Tactic:
cases n <;> simp [F] at h₂

Result:
case refine_1.intro.intro.intro.succ
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
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
this : ∀ (m : ℕ) (a' : α), Sum.inr a' ∈ F a m → b ∈ f.fix a' → b ∈ f.fix a
n✝ : ℕ
_x : ∃ b', Sum.inl b' ∈ F a (n✝ + 1)
h₁ : ∀ {m : ℕ}, m < n✝ + 1 → ∃ b, Sum.inr b ∈ F a m
h₂ :
  Sum.inl b ∈
      Nat.rec (Part.some (Sum.inr a))
        (fun x IH => IH.bind fun s => Sum.rec (fun val => Part.some s) (fun val => f val) s) n✝ ∨
    ∃ b_1,
      Sum.inr b_1 ∈
          Nat.rec (Part.some (Sum.inr a))
            (fun x IH => IH.bind fun s => Sum.rec (fun val => Part.some s) (fun val => f val) s) n✝ ∧
        Sum.inl b ∈ f b_1
⊢ b ∈ f.fix a