-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f : List.Vector ℕ (n_2 + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n_2 + 1) →. ℕ)
cf : Code
v : List.Vector ℕ n_2
hf : ∀ (a : ℕ), cf.eval (a :: (↑v : List ℕ)) = Part.some [f (a ::ᵥ v)]
v' v₀ : List ℕ
n : ℕ
h2 :
  Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        (cf.eval v).bind fun (y : List ℕ) ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (n :: (↑v : List ℕ)))
    v'
IH :
  ∀ (a'' : List ℕ),
    Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
        ((cf.eval (n :: (↑v : List ℕ))).bind fun (y : List ℕ) ↦
          Part.some
            (if y.headI = 0 then Sum.inl ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail)
            else Sum.inr ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail)))
        (Sum.inr a'') →
      ∀ (n : ℕ),
        a'' = n :: (↑v : List ℕ) →
          (∀ m < n, ¬f (m ::ᵥ v) = 0) →
            ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
hm : ∀ m < n, ¬f (m ::ᵥ v) = 0
this :
  Sum.inl v' ∈
      Part.some
        (if [f (n ::ᵥ v)].headI = 0 then Sum.inl ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail)
        else Sum.inr ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail)) ∨
    ∃ (a' : List ℕ),
      Sum.inr a' ∈
          Part.some
            (if [f (n ::ᵥ v)].headI = 0 then Sum.inl ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail)
            else Sum.inr ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail)) ∧
        Membership.mem (γ := Part (List ℕ))
          (PFun.fix
            (fun (v : List ℕ) ↦
              (cf.eval v).bind fun (y : List ℕ) ↦
                Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
            a')
          v'
pos :
  ∀ (h : [f (n ::ᵥ v)].headI = 0)
    (this :
      Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
          (Part.some (Sum.inl ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail))) (Sum.inl v') ∨
        ∃ (a' : List ℕ),
          Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
              (Part.some (Sum.inl ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail))) (Sum.inr a') ∧
            Membership.mem (γ := Part (List ℕ))
              (PFun.fix
                (fun (v : List ℕ) ↦
                  (cf.eval v).bind fun (y : List ℕ) ↦
                    Part.some
                      (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
                a')
              v'),
    ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
⊢ ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
have neg : ∀ (h : ¬[f (n ::ᵥ v)].headI = 0)
  (this :
    Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
        (Part.some (Sum.inr ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail))) (Sum.inl v') ∨
      ∃ (a' : List ℕ),
        Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
            (Part.some (Sum.inr ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail))) (Sum.inr a') ∧
          Membership.mem (γ := Part (List ℕ))
            (PFun.fix
              (fun (v : List ℕ) ↦
                (cf.eval v).bind fun (y : List ℕ) ↦
                  Part.some
                    (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
              a')
            v'),
  ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
Tactic: split_ifs at this with h
Cleared hypotheses: this