-- 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
α : 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' : α),
    b ∈ f.fix a' →
      (∀ (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 : ℕ), 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₂ IH k hk

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₁
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
⊢ ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m

Proof state:
case refine_2.inl.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 : 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
h₂ : Sum.inl b ∈ f a₂
⊢ Sum.inl b ∈ F a k.succ

Tactic:
simpa [F] using Or.inr ⟨_, hk, h₂⟩

Result:
no goals

Proof state:
α : 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
this :
  ∀ (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
⊢ Sum.inr a ∈ F a 0

Tactic:
simp [F]

Result:
no goals

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₁ : α
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
⊢ ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m

Tactic:
rcases PFun.mem_fix_iff.1 h₂ with (h₂ | ⟨a₃, am₃, _⟩)

Result:
case refine_2.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
h₂ : Sum.inl b ∈ f a₂
⊢ ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m

case refine_2.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
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, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m

Proof state:
case refine_2.inl.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₁
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
h₂ : Sum.inl b ∈ f a₂
m : ℕ
mk : m < k.succ
km : k ≤ m
⊢ Sum.inr a₂ ∈ F a m

Tactic:
rwa [le_antisymm (Nat.le_of_lt_succ mk) km]

Result:
no goals

Proof state:
α : 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, ((∃ 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:
refine ⟨fun h => ?_, fun h => ?_⟩

Result:
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

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
⊢ ∃ n, ((∃ b', Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m) ∧ Sum.inl b ∈ F a n

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₁ : α
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

Tactic:
apply @PFun.fixInduction _ _ _ _ _ _ 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₁
⊢ ∀ (a' : α),
    b ∈ f.fix a' →
      (∀ (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 : ℕ), 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:
α : 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
this :
  ∀ (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
⊢ ∃ n, ((∃ b', Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m) ∧ Sum.inl b ∈ F a n

Tactic:
rcases this _ h 0 (by simp [F]) with ⟨n, hn₁, hn₂⟩

Result:
case 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
h : b ∈ f.fix a
this :
  ∀ (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
n : ℕ
hn₁ : Sum.inl b ∈ F a n
hn₂ : ∀ m < n, 0 ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
⊢ ∃ n, ((∃ b', Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m) ∧ Sum.inl b ∈ F a n