awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.PartrecCode
Goal:
x : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.comp cg)) →
      lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.comp cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.comp cg)
lg : encode cg < encode (cf.comp cg)
succ :
  Eq (α := Option ℕ)
    ((evaln k cg n).bind fun (x : ℕ) ↦
      lup
        (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.comp cg)))))
        (k' + 1, cf) x)
    ((evaln (k' + 1) cg n).bind fun (x : ℕ) ↦ evaln (k' + 1) cf x)
⊢ Eq (α := Option ℕ)
    ((lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair (k' + 1) (encode (cf.comp cg)))))
          (k' + 1, cg) n).bind
      fun (x : ℕ) ↦
      lup
        (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.comp cg)))))
        (k' + 1, cf) x)
    ((evaln (k' + 1) cg n).bind fun (x : ℕ) ↦ evaln (k' + 1) cf x)

Tactic:
rw [hg (Nat.pair_lt_pair_right _ lg)]

Premises used: Nat.pair_lt_pair_right
-- Module: Mathlib.Computability.PartrecCode
Goal:
x : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.comp cg)) →
      lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.comp cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.comp cg)
lg : encode cg < encode (cf.comp cg)
succ :
  Eq (α := Option ℕ)
    (Option.bind Option.none fun (x : ℕ) ↦
      lup
        (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.comp cg)))))
        (k' + 1, cf) x)
    (Option.bind Option.none fun (x : ℕ) ↦ evaln (k' + 1) cf x)
succ₁ :
  ∀ (val : ℕ),
    Eq (α := Option ℕ)
      ((some val).bind fun (x : ℕ) ↦
        lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair (k' + 1) (encode (cf.comp cg)))))
          (k' + 1, cf) x)
      ((some val).bind fun (x : ℕ) ↦ evaln (k' + 1) cf x)
⊢ Eq (α := Option ℕ)
    ((evaln k cg n).bind fun (x : ℕ) ↦
      lup
        (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.comp cg)))))
        (k' + 1, cf) x)
    ((evaln (k' + 1) cg n).bind fun (x : ℕ) ↦ evaln (k' + 1) cf x)

Tactic:
cases evaln k cg n

Premises used: Nat.Partrec.Code.evaln
-- Module: Mathlib.Computability.PartrecCode
Goal:
x : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.comp cg)) →
      lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.comp cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.comp cg)
lg : encode cg < encode (cf.comp cg)
⊢ Eq (α := Option ℕ)
    (Option.bind Option.none fun (x : ℕ) ↦
      lup
        (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.comp cg)))))
        (k' + 1, cf) x)
    (Option.bind Option.none fun (x : ℕ) ↦ evaln (k' + 1) cf x)

Tactic:
rfl
-- Module: Mathlib.Computability.PartrecCode
Goal:
x : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.comp cg)) →
      lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.comp cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.comp cg)
lg : encode cg < encode (cf.comp cg)
val : ℕ
⊢ Eq (α := Option ℕ)
    ((some val).bind fun (x : ℕ) ↦
      lup
        (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.comp cg)))))
        (k' + 1, cf) x)
    ((some val).bind fun (x : ℕ) ↦ evaln (k' + 1) cf x)

Tactic:
simp [k, hg (Nat.pair_lt_pair_right _ lf)]

Premises used: Nat.pair_lt_pair_right
-- Module: Mathlib.Computability.PartrecCode
Goal:
x : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
⊢ encode cf < encode (cf.prec cg)

Tactic:
obtain ⟨lf, lg⟩ := encode_lt_prec cf cg

Premises used: Nat.Partrec.Code.encode_lt_prec
-- Module: Mathlib.Computability.PartrecCode
Goal:
x : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
⊢ encode cg < encode (cf.prec cg)

Tactic:
obtain ⟨lf, lg⟩ := encode_lt_prec cf cg

Premises used: Nat.Partrec.Code.encode_lt_prec
-- Module: Mathlib.Computability.PartrecCode
Goal:
x : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
succ :
  Eq (α := Option ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln k cf (unpair n).1)
        (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
          (lup
                (List.map
                  (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                  (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
                (k', cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind
            fun (i : ℕ) ↦
            lup
              (List.map
                (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
              (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
        (unpair n).2 :
      Option ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k' + 1) cf (unpair n).1)
        (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
          (evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
            evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
        (unpair n).2 :
      Option ℕ)
⊢ Eq (α := Option ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ)
        (lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
          (k' + 1, cf) (unpair n).1)
        (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
          (lup
                (List.map
                  (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                  (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
                (k', cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind
            fun (i : ℕ) ↦
            lup
              (List.map
                (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
              (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
        (unpair n).2 :
      Option ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k' + 1) cf (unpair n).1)
        (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
          (evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
            evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
        (unpair n).2 :
      Option ℕ)

Tactic:
rw [hg (Nat.pair_lt_pair_right _ lf)]

Premises used: Nat.pair_lt_pair_right
-- Module: Mathlib.Computability.PartrecCode
Goal:
x : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
⊢ Eq (α := Option ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln k cf (unpair n).1)
        (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
          (lup
                (List.map
                  (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                  (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
                (k', cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind
            fun (i : ℕ) ↦
            lup
              (List.map
                (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
              (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
        0 :
      Option ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k' + 1) cf (unpair n).1)
        (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
          (evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
            evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
        0 :
      Option ℕ)

Tactic:
rfl
-- Module: Mathlib.Computability.PartrecCode
Goal:
x : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
n_1 : ℕ
succ :
  Eq (α := Option ℕ)
    ((evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
      lup
        (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
        (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
    ((evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
      evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
⊢ Eq (α := Option ℕ)
    ((lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
          (k', cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind
      fun (i : ℕ) ↦
      lup
        (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
        (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
    ((evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
      evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))

Tactic:
rw [hg (Nat.pair_lt_pair_left _ k'.lt_succ_self)]

Premises used: Nat.lt_succ_self, Nat.pair_lt_pair_left
-- Module: Mathlib.Computability.PartrecCode
Goal:
x : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
n_1 : ℕ
succ :
  Eq (α := Option ℕ)
    (Option.bind Option.none fun (i : ℕ) ↦
      lup
        (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
        (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
    (Option.bind Option.none fun (i : ℕ) ↦ evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
succ₁ :
  ∀ (val : ℕ),
    Eq (α := Option ℕ)
      ((some val).bind fun (i : ℕ) ↦
        lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
          (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      ((some val).bind fun (i : ℕ) ↦ evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
⊢ Eq (α := Option ℕ)
    ((evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
      lup
        (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
        (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
    ((evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun (i : ℕ) ↦
      evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))

Tactic:
cases evaln k' _ _

Premises used: Nat.Partrec.Code.evaln
-- Module: Mathlib.Computability.PartrecCode
Goal:
x : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
n_1 : ℕ
⊢ Eq (α := Option ℕ)
    (Option.bind Option.none fun (i : ℕ) ↦
      lup
        (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
        (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
    (Option.bind Option.none fun (i : ℕ) ↦ evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))

Tactic:
rfl
-- Module: Mathlib.Computability.PartrecCode
Goal:
x : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
n_1 val : ℕ
⊢ Eq (α := Option ℕ)
    ((some val).bind fun (i : ℕ) ↦
      lup
        (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
        (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
    ((some val).bind fun (i : ℕ) ↦ evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))

Tactic:
simp [k, hg (Nat.pair_lt_pair_right _ lg)]

Premises used: Nat.pair_lt_pair_right
-- Module: Mathlib.Computability.PartrecCode
Goal:
x : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode cf.rfind') →
      lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode cf.rfind'))))
          (k', c') n =
        evaln k' c' n
⊢ encode cf < encode cf.rfind'

Tactic:
have lf := encode_lt_rfind' cf
-- Module: Mathlib.Computability.PartrecCode
Goal:
x : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode cf.rfind') →
      lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode cf.rfind'))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode cf.rfind'
succ :
  Eq (α := Option ℕ)
    ((evaln k cf n).bind fun (x : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (some (unpair n).2)
        (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
          lup
            (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
              (List.range (Nat.pair (k' + 1) (encode cf.rfind'))))
            (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
        x)
    ((evaln (k' + 1) cf n).bind fun (a : ℕ) ↦
      if a = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
⊢ Eq (α := Option ℕ)
    ((lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair (k' + 1) (encode cf.rfind'))))
          (k' + 1, cf) n).bind
      fun (x : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (some (unpair n).2)
        (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
          lup
            (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
              (List.range (Nat.pair (k' + 1) (encode cf.rfind'))))
            (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
        x)
    ((evaln (k' + 1) cf n).bind fun (a : ℕ) ↦
      if a = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)))

Tactic:
rw [hg (Nat.pair_lt_pair_right _ lf)]

Premises used: Nat.pair_lt_pair_right
-- Module: Mathlib.Computability.PartrecCode
Goal:
x : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode cf.rfind') →
      lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode cf.rfind'))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode cf.rfind'
succ :
  Eq (α := Option ℕ)
    (Option.bind Option.none fun (x : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (some (unpair n).2)
        (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
          lup
            (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
              (List.range (Nat.pair (k' + 1) (encode cf.rfind'))))
            (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
        x)
    (Option.bind Option.none fun (a : ℕ) ↦
      if a = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
succ₁ :
  ∀ (x : ℕ),
    Eq (α := Option ℕ)
      ((some x).bind fun (x : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (some (unpair n).2)
          (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
            lup
              (List.map
                (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                (List.range (Nat.pair (k' + 1) (encode cf.rfind'))))
              (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
          x)
      ((some x).bind fun (a : ℕ) ↦
        if a = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
⊢ Eq (α := Option ℕ)
    ((evaln k cf n).bind fun (x : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (some (unpair n).2)
        (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
          lup
            (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
              (List.range (Nat.pair (k' + 1) (encode cf.rfind'))))
            (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
        x)
    ((evaln (k' + 1) cf n).bind fun (a : ℕ) ↦
      if a = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)))

Tactic:
rcases evaln k cf n with - | x

Premises used: Nat.Partrec.Code.evaln
-- Module: Mathlib.Computability.PartrecCode
Goal:
x : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode cf.rfind') →
      lup
          (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode cf.rfind'))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode cf.rfind'
⊢ Eq (α := Option ℕ)
    (Option.bind Option.none fun (x : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (some (unpair n).2)
        (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
          lup
            (List.map (fun (n : ℕ) ↦ List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
              (List.range (Nat.pair (k' + 1) (encode cf.rfind'))))
            (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
        x)
    (Option.bind Option.none fun (a : ℕ) ↦
      if a = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1)))

Tactic:
rfl