awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) 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 : ℕ
a' : α
am : Sum.inr a' ∈ F a m
ba : b ∈ f.fix a'
zero : ∀ (a' : α) (am : Sum.inr a' ∈ F a 0) (ba : b ∈ f.fix a'), b ∈ f.fix a
zero₁ : ∀ (a' : α) (ba : b ∈ f.fix a') (am : a' = a), b ∈ f.fix a
succ :
  ∀ (m : ℕ) (IH : ∀ (a' : α) (am : Sum.inr a' ∈ F a m) (ba : b ∈ f.fix a'), b ∈ f.fix a) (a' : α)
    (am : Sum.inr a' ∈ F a (m + 1)) (ba : b ∈ f.fix a'), b ∈ f.fix a
succ₁ :
  ∀ (m : ℕ) (IH : ∀ (a' : α) (am : Sum.inr a' ∈ F a m) (ba : b ∈ f.fix a'), b ∈ f.fix a) (a' : α) (ba : b ∈ f.fix a')
    (am :
      ∃ (b : α),
        Membership.mem (γ := Part (σ ⊕ α))
            (Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
                (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
                  IH.bind fun (s : σ ⊕ α) ↦
                    Sum.rec (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) (fun (val : σ) ↦ Part.some s)
                      (fun (val : α) ↦ f val) s)
                m :
              Part (σ ⊕ α))
            (Sum.inr b) ∧
          Sum.inr a' ∈ f b),
    b ∈ f.fix a
⊢ b ∈ f.fix a

Tactic:
induction m generalizing a' with simp [F] at am
      | zero => rwa [← am]
      | succ m IH =>
        rcases am with ⟨a₂, am₂, fa₂⟩
        exact IH _ am₂ (PFun.mem_fix_iff.2 (Or.inr ⟨_, fa₂, ba⟩))

Premises used: Computable.succ
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) 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 : ℕ) (a' : α), Sum.inr a' ∈ F a m → b ∈ f.fix a' → b ∈ f.fix a

Tactic:
have : ∀ m a', Sum.inr a' ∈ F a m → b ∈ PFun.fix f a' → b ∈ PFun.fix f a := by
      intro m a' am ba
      induction m generalizing a' with simp [F] at am
      | zero => rwa [← am]
      | succ m IH =>
        rcases am with ⟨a₂, am₂, fa₂⟩
        exact IH _ am₂ (PFun.mem_fix_iff.2 (Or.inr ⟨_, fa₂, ba⟩))
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) 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
refine_1 :
  ∀ (h₂ : Sum.inl b ∈ F a 0) (_x : ∃ (b' : σ), Sum.inl b' ∈ F a 0)
    (h₁ : ∀ {m : ℕ}, m < 0 → ∃ (b : α), Sum.inr b ∈ F a m), b ∈ f.fix a
refine_1₁ :
  ∀ (n : ℕ) (h₂ : Sum.inl b ∈ F a (n + 1)) (_x : ∃ (b' : σ), Sum.inl b' ∈ F a (n + 1))
    (h₁ : ∀ {m : ℕ}, m < n + 1 → ∃ (b : α), Sum.inr b ∈ F a m), b ∈ f.fix a
⊢ b ∈ f.fix a

Tactic:
cases n
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) 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
h₂ : Sum.inl b ∈ F a 0
_x : ∃ (b' : σ), Sum.inl b' ∈ F a 0
h₁ : ∀ {m : ℕ}, m < 0 → ∃ (b : α), Sum.inr b ∈ F a m
⊢ b ∈ f.fix a

Tactic:
simp [F] at h₂
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) 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 : ℕ
h₂ : Sum.inl b ∈ F a (n + 1)
_x : ∃ (b' : σ), Sum.inl b' ∈ F a (n + 1)
h₁ : ∀ {m : ℕ}, m < n + 1 → ∃ (b : α), Sum.inr b ∈ F a m
⊢ Membership.mem (γ := Part (σ ⊕ α))
      (Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
          (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
            IH.bind fun (s : σ ⊕ α) ↦
              Sum.rec (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) (fun (val : σ) ↦ Part.some s) (fun (val : α) ↦ f val)
                s)
          n :
        Part (σ ⊕ α))
      (Sum.inl b) ∨
    ∃ (b_1 : α),
      Membership.mem (γ := Part (σ ⊕ α))
          (Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
              (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
                IH.bind fun (s : σ ⊕ α) ↦
                  Sum.rec (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) (fun (val : σ) ↦ Part.some s)
                    (fun (val : α) ↦ f val) s)
              n :
            Part (σ ⊕ α))
          (Sum.inr b_1) ∧
        Sum.inl b ∈ f b_1

Tactic:
simp [F] at h₂
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) 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₂ :
  Membership.mem (γ := Part (σ ⊕ α))
      (Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
          (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
            IH.bind fun (s : σ ⊕ α) ↦
              Sum.rec (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) (fun (val : σ) ↦ Part.some s) (fun (val : α) ↦ f val)
                s)
          n :
        Part (σ ⊕ α))
      (Sum.inl b) ∨
    ∃ (b_1 : α),
      Membership.mem (γ := Part (σ ⊕ α))
          (Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
              (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
                IH.bind fun (s : σ ⊕ α) ↦
                  Sum.rec (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) (fun (val : σ) ↦ Part.some s)
                    (fun (val : α) ↦ f val) s)
              n :
            Part (σ ⊕ α))
          (Sum.inr b_1) ∧
        Sum.inl b ∈ f b_1
refine_1 : ∀ (c : α) (hc : Sum.inr c ∈ F a n), b ∈ f.fix a
⊢ b ∈ f.fix a

Tactic:
obtain ⟨c, hc⟩ := h₁ (Nat.lt_succ_self _)

Premises used: Nat.lt_succ_self
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) 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₂ :
  Membership.mem (γ := Part (σ ⊕ α))
      (Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
          (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
            IH.bind fun (s : σ ⊕ α) ↦
              Sum.rec (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) (fun (val : σ) ↦ Part.some s) (fun (val : α) ↦ f val)
                s)
          n :
        Part (σ ⊕ α))
      (Sum.inl b) ∨
    ∃ (b_1 : α),
      Membership.mem (γ := Part (σ ⊕ α))
          (Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
              (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
                IH.bind fun (s : σ ⊕ α) ↦
                  Sum.rec (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) (fun (val : σ) ↦ Part.some s)
                    (fun (val : α) ↦ f val) s)
              n :
            Part (σ ⊕ α))
          (Sum.inr b_1) ∧
        Sum.inl b ∈ f b_1
c : α
hc : Sum.inr c ∈ F a n
⊢ b ∈ f.fix c → b ∈ f.fix a

Tactic:
specialize this _ _ hc
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) s (fun (x : σ) ↦ Part.some s) f)
      n
n : ℕ
_x : ∃ (b' : σ), Sum.inl b' ∈ F a (n + 1)
h₁ : ∀ {m : ℕ}, m < n + 1 → ∃ (b : α), Sum.inr b ∈ F a m
h₂ :
  Membership.mem (γ := Part (σ ⊕ α))
      (Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
          (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
            IH.bind fun (s : σ ⊕ α) ↦
              Sum.rec (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) (fun (val : σ) ↦ Part.some s) (fun (val : α) ↦ f val)
                s)
          n :
        Part (σ ⊕ α))
      (Sum.inl b) ∨
    ∃ (b_1 : α),
      Membership.mem (γ := Part (σ ⊕ α))
          (Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
              (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
                IH.bind fun (s : σ ⊕ α) ↦
                  Sum.rec (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) (fun (val : σ) ↦ Part.some s)
                    (fun (val : α) ↦ f val) s)
              n :
            Part (σ ⊕ α))
          (Sum.inr b_1) ∧
        Sum.inl b ∈ f b_1
c : α
hc : Sum.inr c ∈ F a n
this : b ∈ f.fix c → b ∈ f.fix a
⊢ b ∈ f.fix a

Tactic:
grind [mem_unique, PFun.mem_fix_iff]

Premises used: PFun.mem_fix_iff, Part.mem_unique
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) 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]
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) 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
rcases :
  ∀ (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
⊢ ∃ (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₂⟩

Premises used: OfNat.ofNat
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) 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

Tactic:
⟨_, ⟨⟨_, hn₁⟩, fun {m} mn => hn₂ m mn (Nat.zero_le _)⟩, hn₁⟩

Premises used: Nat.zero_le, And.intro, Exists.intro
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) 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

Tactic:
exact ⟨_, ⟨⟨_, hn₁⟩, fun {m} mn => hn₂ m mn (Nat.zero_le _)⟩, hn₁⟩
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) s (fun (x : σ) ↦ Part.some s) f)
      n
h : b ∈ f.fix a
refine_2 :
  ∀ (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:
suffices ∀ a', b ∈ PFun.fix 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 by
      rcases this _ h 0 (by simp [F]) with ⟨n, hn₁, hn₂⟩
      exact ⟨_, ⟨⟨_, hn₁⟩, fun {m} mn => hn₂ m mn (Nat.zero_le _)⟩, hn₁⟩
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) s (fun (x : σ) ↦ Part.some s) f)
      n
h : b ∈ f.fix a
a₁ : α
h₁ : b ∈ f.fix a₁
refine_2 :
  ∀ (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
⊢ ∀ (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₁

Premises used: PFun.fixInduction
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) 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
refine_2 : ∀ (h₂ : Sum.inl b ∈ f a₂), ∃ (n : ℕ), Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ (a₂ : α), Sum.inr a₂ ∈ F a m
refine_2₁ :
  ∀ (a₃ : α) (am₃ : Sum.inr a₃ ∈ f a₂),
    b ∈ f.fix a₃ → ∃ (n : ℕ), Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ (a₂ : α), Sum.inr a₂ ∈ F a m
⊢ ∃ (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₃, _⟩)

Premises used: Iff.mp, PFun.mem_fix_iff
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) s (fun (x : σ) ↦ Part.some s) f)
      n
h : b ∈ f.fix a
a₁ : α
h₁ : b ∈ f.fix a₁
a₂ : α
h₂_1 : 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

Tactic:
⟨k.succ, ?_, fun m mk km => ⟨a₂, ?_⟩⟩

Premises used: And.intro, Exists.intro, Nat.succ
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) s (fun (x : σ) ↦ Part.some s) f)
      n
h : b ∈ f.fix a
a₁ : α
h₁ : b ∈ f.fix a₁
a₂ : α
h₂_1 : 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₂
refine_2 : Sum.inl b ∈ F a k.succ
refine_2₁ : ∀ (m : ℕ) (mk : m < k.succ) (km : k ≤ m), Sum.inr a₂ ∈ F a m
⊢ ∃ (n : ℕ), Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ (a₂ : α), Sum.inr a₂ ∈ F a m

Tactic:
refine ⟨k.succ, ?_, fun m mk km => ⟨a₂, ?_⟩⟩
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) s (fun (x : σ) ↦ Part.some s) f)
      n
h : b ∈ f.fix a
a₁ : α
h₁ : b ∈ f.fix a₁
a₂ : α
h₂_1 : 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₂⟩

Premises used: Or.inr
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) s (fun (x : σ) ↦ Part.some s) f)
      n
h : b ∈ f.fix a
a₁ : α
h₁ : b ∈ f.fix a₁
a₂ : α
h₂_1 : 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
refine_2 refine_2₁ refine_2₂ refine_2₃ : Sum.inr a₂ ∈ F a k
⊢ Sum.inr a₂ ∈ F a m

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

Premises used: le_antisymm, Nat.le_of_lt_succ
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) 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₃
⊢ Sum.inr a₃ ∈ F a k.succ

Tactic:
simpa [F] using ⟨_, hk, am₃⟩
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) 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₃
refine_2 :
  ∀ (n : ℕ) (hn₁ : Sum.inl b ∈ F a n) (hn₂ : ∀ m < n, k.succ ≤ m → ∃ (a₂ : α), Sum.inr a₂ ∈ F a m),
    ∃ (n : ℕ), Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ (a₂ : α), Sum.inr a₂ ∈ F a m
⊢ ∃ (n : ℕ), Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ (a₂ : α), Sum.inr a₂ ∈ F a m

Tactic:
rcases IH _ am₃ k.succ (by simpa [F] using ⟨_, hk, am₃⟩) with ⟨n, hn₁, hn₂⟩

Premises used: Nat.succ
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) 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
refine_2 :
  ∀ (F : α → ℕ →. σ ⊕ α) (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₂),
    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),
        ∃ (n : ℕ), Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ (a₂ : α), Sum.inr a₂ ∈ F a m
⊢ ∃ (n : ℕ), Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ (a₂ : α), Sum.inr a₂ ∈ F a m

Tactic:
clear_value F
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α
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
⊢ ∃ (n : ℕ), Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ (a₂ : α), Sum.inr a₂ ∈ F a m

Tactic:
grind