awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.Partrec (hypothesis)
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
⊢ b ∈ f.fix a
have 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
Tactic: simp [F] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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
⊢ b ∈ f.fix a
have refine_1 : ∀ (c : α) (hc : Sum.inr c ∈ F a n), b ∈ f.fix a
Tactic: obtain ⟨c, hc⟩ := h₁ (Nat.lt_succ_self _)
-- Lean 4 proof step from Mathlib.Computability.Partrec (hypothesis)
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 a
have this₁ : b ∈ f.fix c → b ∈ f.fix a
Tactic: specialize this _ _ hc
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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 : ℕ), ((∃ (b' : σ), Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ (b : α), Sum.inr b ∈ F a m) ∧ Sum.inl b ∈ F a n
have 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
Tactic: rcases this _ h 0 (by simp [F]) with ⟨n, hn₁, hn₂⟩
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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
⊢ ∃ (n : ℕ), ((∃ (b' : σ), Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ (b : α), Sum.inr b ∈ F a m) ∧ Sum.inl b ∈ F a n
have 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
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₁⟩
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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₁
⊢ ∀ (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
have 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
Tactic: apply @PFun.fixInduction _ _ _ _ _ _ h₁
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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
⊢ ∃ (n : ℕ), Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ (a₂ : α), Sum.inr a₂ ∈ F a m
have 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
Tactic: rcases PFun.mem_fix_iff.1 h₂ with (h₂ | ⟨a₃, am₃, _⟩)
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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
⊢ ∃ (n : ℕ), Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ (a₂ : α), Sum.inr a₂ ∈ F a m
have 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
Tactic: rcases PFun.mem_fix_iff.1 h₂ with (h₂ | ⟨a₃, am₃, _⟩)
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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
have refine_2 : Sum.inl b ∈ F a k.succ
Tactic: refine ⟨k.succ, ?_, fun m mk km => ⟨a₂, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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
⊢ ∃ (n : ℕ), Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ (a₂ : α), Sum.inr a₂ ∈ F a m
have refine_2₁ : ∀ (m : ℕ) (mk : m < k.succ) (km : k ≤ m), Sum.inr a₂ ∈ F a m
Tactic: refine ⟨k.succ, ?_, fun m mk km => ⟨a₂, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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 : ℕ), Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ (a₂ : α), Sum.inr a₂ ∈ F a m
have 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
Tactic: rcases IH _ am₃ k.succ (by simpa [F] using ⟨_, hk, am₃⟩) with ⟨n, hn₁, hn₂⟩
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
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
⊢ ∃ (n : ℕ), Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ (a₂ : α), Sum.inr a₂ ∈ F a m
have 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
Tactic: clear_value F
Cleared hypotheses: F, h, a₁, h₁, a₂, h₂, IH, k, hk, a₃, am₃, right, n, hn₁, hn₂
-- Lean 4 proof step from Mathlib.Computability.Partrec (hypothesis)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f : α →. σ ⊕ α
hf : Partrec f
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
⊢ Partrec f.fix
have hF : Partrec₂ F
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₂
-- Lean 4 proof step from Mathlib.Computability.Partrec (hypothesis)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f : α →. σ ⊕ α
hf : Partrec f
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
hF : Partrec₂ F
p : (a : α) → (n : ℕ) → Part Bool :=
  fun (a : α) (n : ℕ) ↦
    Part.map
      (fun (s : σ ⊕ α) ↦ Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Bool) s (fun (x : σ) ↦ true) fun (x : α) ↦ false)
      (F a n)
⊢ Partrec f.fix
have hp : Partrec₂ p
Tactic: have hp : Partrec₂ p :=
    hF.map ((sumCasesOn Computable.id (const true).to₂ (const false).to₂).comp snd).to₂
-- Lean 4 proof step from Mathlib.Computability.PartrecBasis (hypothesis)
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
n_1 : ℕ
f_1 : List.Vector ℕ (n_1 + 1) → ℕ
h : Partrec' (↑f_1 : List.Vector ℕ (n_1 + 1) →. ℕ)
hf : Partrec (↑f_1 : List.Vector ℕ (n_1 + 1) →. ℕ)
⊢ Partrec (α := List.Vector ℕ n_1) (σ := ℕ) fun (v : List.Vector ℕ n_1) ↦
    Nat.rfind fun (n : ℕ) ↦ Part.some (decide (f_1 (n ::ᵥ v) = 0))
have this : Partrec (α := List.Vector ℕ n_1 × ℕ) (σ := ℕ) fun (a : List.Vector ℕ n_1 × ℕ) ↦
  (↑f_1 : List.Vector ℕ (n_1 + 1) →. ℕ) (a.2 ::ᵥ a.1)
Tactic: have := hf.comp (vector_cons.comp snd fst)
-- Lean 4 proof step from Mathlib.Computability.PartrecBasis (hypothesis)
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
n_1 : ℕ
f_1 : List.Vector ℕ (n_1 + 1) → ℕ
h : Partrec' (↑f_1 : List.Vector ℕ (n_1 + 1) →. ℕ)
hf : Partrec (↑f_1 : List.Vector ℕ (n_1 + 1) →. ℕ)
this :
  Partrec (α := List.Vector ℕ n_1 × ℕ) (σ := ℕ) fun (a : List.Vector ℕ n_1 × ℕ) ↦
    (↑f_1 : List.Vector ℕ (n_1 + 1) →. ℕ) (a.2 ::ᵥ a.1)
⊢ Partrec (α := List.Vector ℕ n_1) (σ := ℕ) fun (v : List.Vector ℕ n_1) ↦
    Nat.rfind fun (n : ℕ) ↦ Part.some (decide (f_1 (n ::ᵥ v) = 0))
have this₁ : Partrec₂ (β := ℕ) (σ := Bool) fun (a : List.Vector ℕ n_1) ↦
  (↑fun (b : ℕ) ↦ decide (id (f_1 ((a, b).2 ::ᵥ (a, b).1)) = 0) : ℕ →. Bool)
Tactic: have :=
      ((Primrec.eq.decide.comp _root_.Primrec.id (_root_.Primrec.const 0)).to_comp.comp
        this).to₂.partrec₂
-- Lean 4 proof step from Mathlib.Computability.PartrecBasis (goal)
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
pf : Partrec' f
⊢ Partrec f
have prim : ∀ {n : ℕ} {f : List.Vector ℕ n → ℕ} (hf : Primrec' f), Partrec (↑f : List.Vector ℕ n →. ℕ)
Tactic: induction pf with
  | prim hf => exact hf.to_prim.to_comp
  | comp _ _ _ hf hg => exact (Partrec.vector_mOfFn hg).bind (hf.comp snd)
  | rfind _ hf =>
    have := hf.comp (vector_cons.comp snd fst)
    have :=
      ((Primrec.eq.decide.comp _root_.Primrec.id (_root_.Primrec.const 0)).to_comp.comp
        this).to₂.partrec₂
    exact _root_.Partrec.rfind this
Cleared hypotheses: pf
-- Lean 4 proof step from Mathlib.Computability.PartrecBasis (goal)
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
pf : Partrec' f
prim : ∀ {n : ℕ} {f : List.Vector ℕ n → ℕ} (hf : Primrec' f), Partrec (↑f : List.Vector ℕ n →. ℕ)
⊢ Partrec f
have comp : ∀ {m n : ℕ} {f : List.Vector ℕ n →. ℕ} (g : Fin n → List.Vector ℕ m →. ℕ),
  Partrec' f →
    (∀ (i : Fin n), Partrec' (g i)) →
      ∀ (hf : Partrec f) (hg : ∀ (i : Fin n), Partrec (g i)),
        Partrec (α := List.Vector ℕ m) (σ := ℕ) fun (v : List.Vector ℕ m) ↦ (mOfFn fun (i : Fin n) ↦ g i v) >>= f
Tactic: induction pf with
  | prim hf => exact hf.to_prim.to_comp
  | comp _ _ _ hf hg => exact (Partrec.vector_mOfFn hg).bind (hf.comp snd)
  | rfind _ hf =>
    have := hf.comp (vector_cons.comp snd fst)
    have :=
      ((Primrec.eq.decide.comp _root_.Primrec.id (_root_.Primrec.const 0)).to_comp.comp
        this).to₂.partrec₂
    exact _root_.Partrec.rfind this
Cleared hypotheses: pf
-- Lean 4 proof step from Mathlib.Computability.PartrecBasis (goal)
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
pf : Partrec' f
prim : ∀ {n : ℕ} {f : List.Vector ℕ n → ℕ} (hf : Primrec' f), Partrec (↑f : List.Vector ℕ n →. ℕ)
comp :
  ∀ {m n : ℕ} {f : List.Vector ℕ n →. ℕ} (g : Fin n → List.Vector ℕ m →. ℕ),
    Partrec' f →
      (∀ (i : Fin n), Partrec' (g i)) →
        ∀ (hf : Partrec f) (hg : ∀ (i : Fin n), Partrec (g i)),
          Partrec (α := List.Vector ℕ m) (σ := ℕ) fun (v : List.Vector ℕ m) ↦ (mOfFn fun (i : Fin n) ↦ g i v) >>= f
⊢ Partrec f
have rfind : ∀ {n : ℕ} {f : List.Vector ℕ (n + 1) → ℕ},
  Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ) →
    ∀ (hf : Partrec (↑f : List.Vector ℕ (n + 1) →. ℕ)),
      Partrec (α := List.Vector ℕ n) (σ := ℕ) fun (v : List.Vector ℕ n) ↦
        Nat.rfind fun (n_1 : ℕ) ↦ Part.some (decide (f (n_1 ::ᵥ v) = 0))
Tactic: induction pf with
  | prim hf => exact hf.to_prim.to_comp
  | comp _ _ _ hf hg => exact (Partrec.vector_mOfFn hg).bind (hf.comp snd)
  | rfind _ hf =>
    have := hf.comp (vector_cons.comp snd fst)
    have :=
      ((Primrec.eq.decide.comp _root_.Primrec.id (_root_.Primrec.const 0)).to_comp.comp
        this).to₂.partrec₂
    exact _root_.Partrec.rfind this
Cleared hypotheses: pf
-- Lean 4 proof step from Mathlib.Computability.PartrecBasis (goal)
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
hf : Partrec' f
v : List.Vector ℕ (n + 1)
⊢ (mOfFn fun (i : Fin n) ↦ (↑fun (v : List.Vector ℕ (n + 1)) ↦ v.get i.succ : List.Vector ℕ (n + 1) →. ℕ) v) >>= f =
    f v.tail
have rw : (mOfFn fun (i : Fin n) ↦ (↑fun (v : List.Vector ℕ (n + 1)) ↦ v.get i.succ : List.Vector ℕ (n + 1) →. ℕ) v) >>= f =
  f (ofFn fun (x : Fin n) ↦ v.get x.succ)
Tactic: rw [← ofFn_get v.tail, funext (get_tail_succ v)]
-- Lean 4 proof step from Mathlib.Computability.PartrecBasis (goal)
Goal:
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
v : List.Vector ℕ n
b : ℕ
⊢ Membership.mem (γ := Part ℕ)
      ((Nat.rfind fun (n_1 : ℕ) ↦ Part.some (decide (1 - f (n_1 ::ᵥ v) = 0))).bind fun (a : ℕ) ↦
        (↑pred : ℕ →. ℕ) (f (a ::ᵥ v)))
      b ↔
    Membership.mem (γ := Part ℕ) (Nat.rfindOpt fun (a : ℕ) ↦ ofNat (Option ℕ) (f (a ::ᵥ v))) b
have simp : (∃ a ∈ Nat.rfind fun (n_1 : ℕ) ↦ Part.some (decide (1 ≤ f (n_1 ::ᵥ v))), b = (f (a ::ᵥ v)).pred) ↔
  ∃ a ∈ Nat.rfind fun (n_1 : ℕ) ↦ (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool),
    ofNat (Option ℕ) (f (a ::ᵥ v)) = some b
Tactic: simp only [Nat.rfindOpt, Nat.sub_eq_zero_iff_le, PFun.coe_val, Part.mem_bind_iff,
        Part.mem_some_iff, Option.mem_def, Part.mem_coe]
-- Lean 4 proof step from Mathlib.Computability.PartrecBasis (goal)
Goal:
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
v : List.Vector ℕ n
b : ℕ
⊢ (∃ a ∈ Nat.rfind fun (n_1 : ℕ) ↦ Part.some (decide (1 ≤ f (n_1 ::ᵥ v))), b = (f (a ::ᵥ v)).pred) ↔
    ∃ a ∈ Nat.rfind fun (n_1 : ℕ) ↦ (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool),
      ofNat (Option ℕ) (f (a ::ᵥ v)) = some b
have refine_1 : ∀ (a : ℕ),
  (a ∈ Nat.rfind fun (n_1 : ℕ) ↦ Part.some (decide (1 ≤ f (n_1 ::ᵥ v)))) =
    (a ∈ Nat.rfind fun (n_1 : ℕ) ↦ (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool))
Tactic: refine
        exists_congr fun a => (and_congr (iff_of_eq ?_) Iff.rfl).trans (and_congr_right fun h => ?_)
-- Lean 4 proof step from Mathlib.Computability.PartrecBasis (goal)
Goal:
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
v : List.Vector ℕ n
b : ℕ
refine_1 :
  ∀ (a : ℕ),
    (a ∈ Nat.rfind fun (n_1 : ℕ) ↦ Part.some (decide (1 ≤ f (n_1 ::ᵥ v)))) =
      (a ∈ Nat.rfind fun (n_1 : ℕ) ↦ (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool))
⊢ (∃ a ∈ Nat.rfind fun (n_1 : ℕ) ↦ Part.some (decide (1 ≤ f (n_1 ::ᵥ v))), b = (f (a ::ᵥ v)).pred) ↔
    ∃ a ∈ Nat.rfind fun (n_1 : ℕ) ↦ (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool),
      ofNat (Option ℕ) (f (a ::ᵥ v)) = some b
have refine_2 : ∀ (a : ℕ)
  (h : a ∈ Nat.rfind fun (n_1 : ℕ) ↦ (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool)),
  b = (f (a ::ᵥ v)).pred ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b
Tactic: refine
        exists_congr fun a => (and_congr (iff_of_eq ?_) Iff.rfl).trans (and_congr_right fun h => ?_)
-- Lean 4 proof step from Mathlib.Computability.PartrecBasis (goal)
Goal:
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
v : List.Vector ℕ n
b a : ℕ
⊢ (a ∈ Nat.rfind fun (n_1 : ℕ) ↦ Part.some (decide (1 ≤ f (n_1 ::ᵥ v)))) =
    (a ∈ Nat.rfind fun (n_1 : ℕ) ↦ (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool))
have refine_1 : Eq (α := ℕ →. Bool) (fun (n_1 : ℕ) ↦ Part.some (decide (1 ≤ f (n_1 ::ᵥ v)))) fun (n_1 : ℕ) ↦
  (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool)
Tactic: congr
-- Lean 4 proof step from Mathlib.Computability.PartrecBasis (goal)
Goal:
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
v : List.Vector ℕ n
b a : ℕ
⊢ Eq (α := ℕ →. Bool) (fun (n_1 : ℕ) ↦ Part.some (decide (1 ≤ f (n_1 ::ᵥ v)))) fun (n_1 : ℕ) ↦
    (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool)
have refine_1 : ∀ (n_1 : ℕ),
  Part.some (decide (1 ≤ f (n_1 ::ᵥ v))) =
    (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool)
Tactic: funext n