awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.PartrecBasis
Goal:
c : Code
hf : Nat.Partrec c.eval
⊢ Partrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ c.eval v.head

Tactic:
simpa [eval_eq_rfindOpt] using
      rfindOpt <|
        of_prim <|
          Primrec.encode_iff.2 <|
            primrec_evaln.comp <|
              (Primrec.vector_head.pair (_root_.Primrec.const c)).pair <|
                Primrec.vector_head.comp Primrec.vector_tail

Premises used: Iff.mpr, Primrec.pair, Nat.Partrec.Code.primrec_evaln, Nat.Partrec'.of_prim, Primrec.const, Primrec.encode_iff, Primrec.comp, Nat.Partrec.Code.eval_eq_rfindOpt, Nat.Partrec'.rfindOpt, Primrec.vector_head
-- Module: Mathlib.Computability.PartrecBasis
Goal:
this : ∀ (f : ℕ →. ℕ), Nat.Partrec f → Partrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ f v.head
n : ℕ
f : List.Vector ℕ n →. ℕ
hf : Partrec f
g : (n₁ : ℕ) → Part ℕ :=
  fun (n₁ : ℕ) ↦ Part.bind (↑(decode n₁) : Part (List.Vector ℕ n)) fun (a : List.Vector ℕ n) ↦ Part.map encode (f a)
i : List.Vector ℕ n
dsimp :
  (Part.bind (↑(decode (encode i)) : Part (List.Vector ℕ n)) fun (a : List.Vector ℕ n) ↦ Part.map encode (f a)) = f i
⊢ g (encode i) = f i

Tactic:
dsimp only [g]
-- Module: Mathlib.Computability.PartrecBasis
Goal:
this : ∀ (f : ℕ →. ℕ), Nat.Partrec f → Partrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ f v.head
n : ℕ
f : List.Vector ℕ n →. ℕ
hf : Partrec f
g : (n₁ : ℕ) → Part ℕ :=
  fun (n₁ : ℕ) ↦ Part.bind (↑(decode n₁) : Part (List.Vector ℕ n)) fun (a : List.Vector ℕ n) ↦ Part.map encode (f a)
i : List.Vector ℕ n
⊢ (Part.bind (↑(decode (encode i)) : Part (List.Vector ℕ n)) fun (a : List.Vector ℕ n) ↦ Part.map encode (f a)) = f i

Tactic:
simp [encodek, Part.map_id']

Premises used: Part.map_id', Encodable.encodek
-- Module: Mathlib.Computability.PartrecBasis
Goal:
this : ∀ (f : ℕ →. ℕ), Nat.Partrec f → Partrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ f v.head
n : ℕ
f : List.Vector ℕ n →. ℕ
hf : Partrec f
g : (n₁ : ℕ) → Part ℕ :=
  fun (n₁ : ℕ) ↦ Part.bind (↑(decode n₁) : Part (List.Vector ℕ n)) fun (a : List.Vector ℕ n) ↦ Part.map encode (f a)
⊢ Partrec' f

Tactic:
exact
        (comp₁ g (this g hf) (prim Nat.Primrec'.encode)).of_eq fun i => by
          dsimp only [g]; simp [encodek, Part.map_id']

Premises used: Nat.Primrec'.encode, Nat.Partrec'.comp₁, Nat.Partrec'.prim, Nat.Partrec'.of_eq
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
⊢ Partrec' f ↔ Partrec f

Tactic:
⟨to_part, of_part⟩

Premises used: Nat.Partrec'.to_part, Nat.Partrec'.of_part, Iff.intro
-- Module: Mathlib.Computability.PartrecBasis
Goal:
f : ℕ →. ℕ
h : Partrec (α := List.Vector ℕ 1) (σ := ℕ) fun (v : List.Vector ℕ 1) ↦ f v.head
v : ℕ
⊢ f (List.Vector.head (n := 0) (ofFn fun (i : Fin 1) ↦ id v)) = f v

Tactic:
simp only [id, head_ofFn]

Premises used: id, List.Vector.head_ofFn
-- Module: Mathlib.Computability.PartrecBasis
Goal:
f : ℕ → ℕ →. ℕ
h : Partrec (α := List.Vector ℕ 2) (σ := ℕ) fun (v : List.Vector ℕ 2) ↦ f v.head v.tail.head
v : ℕ × ℕ
⊢ f (v.1 ::ᵥ v.2 ::ᵥ nil).head (v.1 ::ᵥ v.2 ::ᵥ nil).tail.head = f v.1 v.2

Tactic:
simp only [head_cons, tail_cons]

Premises used: List.Vector.tail_cons, List.Vector.head_cons
-- Module: Mathlib.Computability.PartrecBasis
Goal:
m n : ℕ
f : List.Vector ℕ m → List.Vector ℕ n
h : Vec f
⊢ Computable f

Tactic:
simpa only [ofFn_get] using vector_ofFn fun i => to_part (h i)

Premises used: Nat.Partrec'.to_part, List.Vector.ofFn_get, Computable.vector_ofFn
-- Module: Mathlib.Computability.PartrecCode
Goal:
f : ℕ →. ℕ
hf : Nat.Partrec f
⊢ Partrec₂ (β := ℕ) (σ := ℕ) fun (a m : ℕ) ↦
    Part.map (fun (x : ℕ) ↦ x + m) (Nat.rfind fun (n : ℕ) ↦ (fun (m : ℕ) ↦ decide (m = 0)) <$> f (Nat.pair a (n + m)))

Tactic:
Partrec.map
        ((@Partrec₂.unpaired' fun a b : ℕ =>
              Nat.rfind fun n => (fun m => m = 0) <$> f (Nat.pair a (n + b))).1
          ?_)
        (Primrec.nat_add.comp Primrec.snd <| Primrec.snd.comp Primrec.fst).to_comp.to₂

Premises used: Primrec.nat_add, Primrec.snd, Primrec.to_comp, Primrec.fst, Partrec₂.unpaired', Primrec.comp, Iff.mp, Partrec.map, Primrec₂.comp, Partrec₂, Computable.to₂
-- Module: Mathlib.Computability.PartrecCode
Goal:
f : ℕ →. ℕ
hf : Nat.Partrec f
fun :
  Nat.Partrec
    (unpaired fun (a b : ℕ) ↦ Nat.rfind fun (n : ℕ) ↦ (fun (m : ℕ) ↦ decide (m = 0)) <$> f (Nat.pair a (n + b)))
⊢ Partrec₂ (β := ℕ) (σ := ℕ) fun (a m : ℕ) ↦
    Part.map (fun (x : ℕ) ↦ x + m) (Nat.rfind fun (n : ℕ) ↦ (fun (m : ℕ) ↦ decide (m = 0)) <$> f (Nat.pair a (n + m)))

Tactic:
refine
      Partrec.map
        ((@Partrec₂.unpaired' fun a b : ℕ =>
              Nat.rfind fun n => (fun m => m = 0) <$> f (Nat.pair a (n + b))).1
          ?_)
        (Primrec.nat_add.comp Primrec.snd <| Primrec.snd.comp Primrec.fst).to_comp.to₂

Premises used: Primrec.nat_add, Primrec.snd, Primrec.to_comp, Primrec.fst, Partrec₂.unpaired', Primrec.comp, Iff.mp, Partrec.map, Primrec₂.comp, Computable.to₂
-- Module: Mathlib.Computability.PartrecCode
Goal:
f : ℕ →. ℕ
hf : Nat.Partrec f
⊢ Nat.Partrec fun (a : ℕ) ↦
    Nat.rfind fun (n : ℕ) ↦
      (fun (m : ℕ) ↦ decide (m = 0)) <$>
        unpaired (fun (a b : ℕ) ↦ f (Nat.pair (unpair a).1 (b + (unpair a).2))) (Nat.pair a n)

Tactic:
have : Nat.Partrec (fun a => Nat.rfind (fun n => (fun m => decide (m = 0)) <$>
      Nat.unpaired (fun a b => f (Nat.pair (Nat.unpair a).1 (b + (Nat.unpair a).2)))
        (Nat.pair a n))) :=
      rfind
        (Partrec₂.unpaired'.2
          ((Partrec.nat_iff.2 hf).comp
              (Primrec₂.pair.comp (Primrec.fst.comp <| Primrec.unpair.comp Primrec.fst)
                  (Primrec.nat_add.comp Primrec.snd
                    (Primrec.snd.comp <| Primrec.unpair.comp Primrec.fst))).to_comp))
-- Module: Mathlib.Computability.PartrecCode
Goal:
f : ℕ →. ℕ
hf : Nat.Partrec f
this :
  Nat.Partrec fun (a : ℕ) ↦
    Nat.rfind fun (n : ℕ) ↦
      (fun (m : ℕ) ↦ decide (m = 0)) <$>
        unpaired (fun (a b : ℕ) ↦ f (Nat.pair (unpair a).1 (b + (unpair a).2))) (Nat.pair a n)
⊢ Nat.Partrec
    (unpaired fun (a b : ℕ) ↦ Nat.rfind fun (n : ℕ) ↦ (fun (m : ℕ) ↦ decide (m = 0)) <$> f (Nat.pair a (n + b)))

Tactic:
simpa
-- Module: Mathlib.Computability.PartrecCode
Goal:
h : Code.const 0 = Code.const 0
⊢ Eq (α := ℕ) 0 0

Tactic:
simp
-- Module: Mathlib.Computability.PartrecCode
Goal:
n₁ n₂ : ℕ
h : succ.comp (Code.const n₁) = succ.comp (Code.const n₂)
⊢ succ = succ

Tactic:
injection h with h₁ h₂
-- Module: Mathlib.Computability.PartrecCode
Goal:
n₁ n₂ : ℕ
h : succ.comp (Code.const n₁) = succ.comp (Code.const n₂)
h₁ : succ = succ
⊢ Code.const n₁ = Code.const n₂

Tactic:
injection h with h₁ h₂
-- Module: Mathlib.Computability.PartrecCode
Goal:
n₁ n₂ : ℕ
h₁ : succ = succ
h₂ : Code.const n₁ = Code.const n₂
⊢ n₁ + 1 = n₂ + 1

Tactic:
simp only [const_inj h₂]
-- Module: Mathlib.Computability.PartrecCode
Goal:
n : ℕ
m : ℕ := n.div2.div2
simp : n / 2 / 2 < n + 4
⊢ m < n + 4

Tactic:
simp only [m, div2_val]

Premises used: Nat.div2_val
-- Module: Mathlib.Computability.PartrecCode
Goal:
n : ℕ
m : ℕ := n.div2.div2
⊢ n / 2 / 2 < n + 4

Tactic:
lt_of_le_of_lt (le_trans (Nat.div_le_self _ _) (Nat.div_le_self _ _))
          (Nat.succ_le_succ (Nat.le_add_right _ _))

Premises used: lt_of_le_of_lt, Nat.le_add_right, Nat.div_le_self, Nat.succ_le_succ, le_trans
-- Module: Mathlib.Computability.PartrecCode
Goal:
n : ℕ
m : ℕ := n.div2.div2
⊢ n / 2 / 2 < n + 4

Tactic:
exact
        lt_of_le_of_lt (le_trans (Nat.div_le_self _ _) (Nat.div_le_self _ _))
          (Nat.succ_le_succ (Nat.le_add_right _ _))

Premises used: lt_of_le_of_lt, Nat.le_add_right, Nat.div_le_self, Nat.succ_le_succ, le_trans
-- Module: Mathlib.Computability.PartrecCode
Goal:
⊢ (ofNatCode 0).encodeCode = 0

Tactic:
simp [ofNatCode, encodeCode]

Premises used: Nat.Partrec.Code.encodeCode, Nat.Partrec.Code.ofNatCode
-- Module: Mathlib.Computability.PartrecCode
Goal:
⊢ (ofNatCode 1).encodeCode = 1

Tactic:
simp [ofNatCode, encodeCode]

Premises used: Nat.Partrec.Code.encodeCode, Nat.Partrec.Code.ofNatCode
-- Module: Mathlib.Computability.PartrecCode
Goal:
⊢ (ofNatCode 2).encodeCode = 2

Tactic:
simp [ofNatCode, encodeCode]

Premises used: Nat.Partrec.Code.encodeCode, Nat.Partrec.Code.ofNatCode
-- Module: Mathlib.Computability.PartrecCode
Goal:
⊢ (ofNatCode 3).encodeCode = 3

Tactic:
simp [ofNatCode, encodeCode]

Premises used: Nat.Partrec.Code.encodeCode, Nat.Partrec.Code.ofNatCode
-- Module: Mathlib.Computability.PartrecCode
Goal:
n : ℕ
m : ℕ := n.div2.div2
⊢ m < n + 4

Tactic:
have hm : m < n + 4 := by
      simp only [m, div2_val]
      exact
        lt_of_le_of_lt (le_trans (Nat.div_le_self _ _) (Nat.div_le_self _ _))
          (Nat.succ_le_succ (Nat.le_add_right _ _))
-- Module: Mathlib.Computability.PartrecCode
Goal:
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
⊢ (unpair m).1 < n + 4

Tactic:
have _m1 : m.unpair.1 < n + 4 := lt_of_le_of_lt m.unpair_left_le hm
-- Module: Mathlib.Computability.PartrecCode
Goal:
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
_m1 : (unpair m).1 < n + 4
⊢ (unpair m).2 < n + 4

Tactic:
have _m2 : m.unpair.2 < n + 4 := lt_of_le_of_lt m.unpair_right_le hm
-- Module: Mathlib.Computability.PartrecCode
Goal:
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
_m1 : (unpair m).1 < n + 4
_m2 : (unpair m).2 < n + 4
⊢ (ofNatCode m).encodeCode = m

Tactic:
have IH := encode_ofNatCode m
-- Module: Mathlib.Computability.PartrecCode
Goal:
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
_m1 : (unpair m).1 < n + 4
_m2 : (unpair m).2 < n + 4
IH : (ofNatCode m).encodeCode = m
⊢ (ofNatCode (unpair m).1).encodeCode = (unpair m).1

Tactic:
have IH1 := encode_ofNatCode m.unpair.1
-- Module: Mathlib.Computability.PartrecCode
Goal:
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
_m1 : (unpair m).1 < n + 4
_m2 : (unpair m).2 < n + 4
IH : (ofNatCode m).encodeCode = m
IH1 : (ofNatCode (unpair m).1).encodeCode = (unpair m).1
⊢ (ofNatCode (unpair m).2).encodeCode = (unpair m).2

Tactic:
have IH2 := encode_ofNatCode m.unpair.2
-- Module: Mathlib.Computability.PartrecCode
Goal:
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
_m1 : (unpair m).1 < n + 4
_m2 : (unpair m).2 < n + 4
IH : (ofNatCode m).encodeCode = m
IH1 : (ofNatCode (unpair m).1).encodeCode = (unpair m).1
IH2 : (ofNatCode (unpair m).2).encodeCode = (unpair m).2
rw : bit n.bodd (bit n.div2.bodd n.div2.div2) + 4
| n + 4

Tactic:
rw [← Nat.bit_bodd_div2 n, ← Nat.bit_bodd_div2 n.div2]

Premises used: Nat.bit_bodd_div2, Nat.div2
-- Module: Mathlib.Computability.PartrecCode
Goal:
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
_m1 : (unpair m).1 < n + 4
_m2 : (unpair m).2 < n + 4
IH : (ofNatCode m).encodeCode = m
IH1 : (ofNatCode (unpair m).1).encodeCode = (unpair m).1
IH2 : (ofNatCode (unpair m).2).encodeCode = (unpair m).2
conv_rhs : (ofNatCode (n + 4)).encodeCode = bit n.bodd (bit n.div2.bodd n.div2.div2) + 4
⊢ (ofNatCode (n + 4)).encodeCode = n + 4

Tactic:
conv_rhs => rw [← Nat.bit_bodd_div2 n, ← Nat.bit_bodd_div2 n.div2]

Premises used: Nat.bit_bodd_div2, Nat.div2
-- Module: Mathlib.Computability.PartrecCode
Goal:
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
_m1 : (unpair m).1 < n + 4
_m2 : (unpair m).2 < n + 4
IH : (ofNatCode m).encodeCode = m
IH1 : (ofNatCode (unpair m).1).encodeCode = (unpair m).1
IH2 : (ofNatCode (unpair m).2).encodeCode = (unpair m).2
simp :
  encodeCode
      (match (motive := Bool → Bool → Code) n.bodd, n.div2.bodd with
      | false, false => (ofNatCode (unpair n.div2.div2).1).pair (ofNatCode (unpair n.div2.div2).2)
      | false, true => (ofNatCode (unpair n.div2.div2).1).comp (ofNatCode (unpair n.div2.div2).2)
      | true, false => (ofNatCode (unpair n.div2.div2).1).prec (ofNatCode (unpair n.div2.div2).2)
      | true, true => (ofNatCode n.div2.div2).rfind') =
    bit n.bodd (bit n.div2.bodd n.div2.div2) + 4
⊢ (ofNatCode (n + 4)).encodeCode = bit n.bodd (bit n.div2.bodd n.div2.div2) + 4

Tactic:
simp only [ofNatCode.eq_5]

Premises used: Nat.Partrec.Code.ofNatCode.eq_5
-- Module: Mathlib.Computability.PartrecCode
Goal:
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
_m1 : (unpair m).1 < n + 4
_m2 : (unpair m).2 < n + 4
IH : (ofNatCode m).encodeCode = m
IH1 : (ofNatCode (unpair m).1).encodeCode = (unpair m).1
IH2 : (ofNatCode (unpair m).2).encodeCode = (unpair m).2
false :
  encodeCode
      (match (motive := Bool → Bool → Code) Bool.false, n.div2.bodd with
      | Bool.false, Bool.false => (ofNatCode (unpair n.div2.div2).1).pair (ofNatCode (unpair n.div2.div2).2)
      | Bool.false, Bool.true => (ofNatCode (unpair n.div2.div2).1).comp (ofNatCode (unpair n.div2.div2).2)
      | Bool.true, Bool.false => (ofNatCode (unpair n.div2.div2).1).prec (ofNatCode (unpair n.div2.div2).2)
      | Bool.true, Bool.true => (ofNatCode n.div2.div2).rfind') =
    bit Bool.false (bit n.div2.bodd n.div2.div2) + 4
true :
  encodeCode
      (match (motive := Bool → Bool → Code) Bool.true, n.div2.bodd with
      | Bool.false, Bool.false => (ofNatCode (unpair n.div2.div2).1).pair (ofNatCode (unpair n.div2.div2).2)
      | Bool.false, Bool.true => (ofNatCode (unpair n.div2.div2).1).comp (ofNatCode (unpair n.div2.div2).2)
      | Bool.true, Bool.false => (ofNatCode (unpair n.div2.div2).1).prec (ofNatCode (unpair n.div2.div2).2)
      | Bool.true, Bool.true => (ofNatCode n.div2.div2).rfind') =
    bit Bool.true (bit n.div2.bodd n.div2.div2) + 4
⊢ encodeCode
      (match (motive := Bool → Bool → Code) n.bodd, n.div2.bodd with
      | Bool.false, Bool.false => (ofNatCode (unpair n.div2.div2).1).pair (ofNatCode (unpair n.div2.div2).2)
      | Bool.false, Bool.true => (ofNatCode (unpair n.div2.div2).1).comp (ofNatCode (unpair n.div2.div2).2)
      | Bool.true, Bool.false => (ofNatCode (unpair n.div2.div2).1).prec (ofNatCode (unpair n.div2.div2).2)
      | Bool.true, Bool.true => (ofNatCode n.div2.div2).rfind') =
    bit n.bodd (bit n.div2.bodd n.div2.div2) + 4

Tactic:
cases n.bodd

Premises used: Nat.bodd
-- Module: Mathlib.Computability.PartrecCode
Goal:
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
_m1 : (unpair m).1 < n + 4
_m2 : (unpair m).2 < n + 4
IH : (ofNatCode m).encodeCode = m
IH1 : (ofNatCode (unpair m).1).encodeCode = (unpair m).1
IH2 : (ofNatCode (unpair m).2).encodeCode = (unpair m).2
false :
  encodeCode
      (match (motive := Bool → Bool → Code) Bool.false, Bool.false with
      | Bool.false, Bool.false => (ofNatCode (unpair n.div2.div2).1).pair (ofNatCode (unpair n.div2.div2).2)
      | Bool.false, true => (ofNatCode (unpair n.div2.div2).1).comp (ofNatCode (unpair n.div2.div2).2)
      | true, Bool.false => (ofNatCode (unpair n.div2.div2).1).prec (ofNatCode (unpair n.div2.div2).2)
      | true, true => (ofNatCode n.div2.div2).rfind') =
    bit Bool.false (bit Bool.false n.div2.div2) + 4
false₁ :
  encodeCode
      (match (motive := Bool → Bool → Code) Bool.false, true with
      | Bool.false, Bool.false => (ofNatCode (unpair n.div2.div2).1).pair (ofNatCode (unpair n.div2.div2).2)
      | Bool.false, true => (ofNatCode (unpair n.div2.div2).1).comp (ofNatCode (unpair n.div2.div2).2)
      | true, Bool.false => (ofNatCode (unpair n.div2.div2).1).prec (ofNatCode (unpair n.div2.div2).2)
      | true, true => (ofNatCode n.div2.div2).rfind') =
    bit Bool.false (bit true n.div2.div2) + 4
⊢ encodeCode
      (match (motive := Bool → Bool → Code) Bool.false, n.div2.bodd with
      | Bool.false, Bool.false => (ofNatCode (unpair n.div2.div2).1).pair (ofNatCode (unpair n.div2.div2).2)
      | Bool.false, true => (ofNatCode (unpair n.div2.div2).1).comp (ofNatCode (unpair n.div2.div2).2)
      | true, Bool.false => (ofNatCode (unpair n.div2.div2).1).prec (ofNatCode (unpair n.div2.div2).2)
      | true, true => (ofNatCode n.div2.div2).rfind') =
    bit Bool.false (bit n.div2.bodd n.div2.div2) + 4

Tactic:
cases n.div2.bodd

Premises used: Nat.div2, Nat.bodd
-- Module: Mathlib.Computability.PartrecCode
Goal:
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
_m1 : (unpair m).1 < n + 4
_m2 : (unpair m).2 < n + 4
IH : (ofNatCode m).encodeCode = m
IH1 : (ofNatCode (unpair m).1).encodeCode = (unpair m).1
IH2 : (ofNatCode (unpair m).2).encodeCode = (unpair m).2
true :
  encodeCode
      (match (motive := Bool → Bool → Code) Bool.true, false with
      | false, false => (ofNatCode (unpair n.div2.div2).1).pair (ofNatCode (unpair n.div2.div2).2)
      | false, Bool.true => (ofNatCode (unpair n.div2.div2).1).comp (ofNatCode (unpair n.div2.div2).2)
      | Bool.true, false => (ofNatCode (unpair n.div2.div2).1).prec (ofNatCode (unpair n.div2.div2).2)
      | Bool.true, Bool.true => (ofNatCode n.div2.div2).rfind') =
    bit Bool.true (bit false n.div2.div2) + 4
true₁ :
  encodeCode
      (match (motive := Bool → Bool → Code) Bool.true, Bool.true with
      | false, false => (ofNatCode (unpair n.div2.div2).1).pair (ofNatCode (unpair n.div2.div2).2)
      | false, Bool.true => (ofNatCode (unpair n.div2.div2).1).comp (ofNatCode (unpair n.div2.div2).2)
      | Bool.true, false => (ofNatCode (unpair n.div2.div2).1).prec (ofNatCode (unpair n.div2.div2).2)
      | Bool.true, Bool.true => (ofNatCode n.div2.div2).rfind') =
    bit Bool.true (bit Bool.true n.div2.div2) + 4
⊢ encodeCode
      (match (motive := Bool → Bool → Code) Bool.true, n.div2.bodd with
      | false, false => (ofNatCode (unpair n.div2.div2).1).pair (ofNatCode (unpair n.div2.div2).2)
      | false, Bool.true => (ofNatCode (unpair n.div2.div2).1).comp (ofNatCode (unpair n.div2.div2).2)
      | Bool.true, false => (ofNatCode (unpair n.div2.div2).1).prec (ofNatCode (unpair n.div2.div2).2)
      | Bool.true, Bool.true => (ofNatCode n.div2.div2).rfind') =
    bit Bool.true (bit n.div2.bodd n.div2.div2) + 4

Tactic:
cases n.div2.bodd

Premises used: Nat.div2, Nat.bodd
-- Module: Mathlib.Computability.PartrecCode
Goal:
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
_m1 : (unpair m).1 < n + 4
_m2 : (unpair m).2 < n + 4
IH : (ofNatCode m).encodeCode = m
IH1 : (ofNatCode (unpair m).1).encodeCode = (unpair m).1
IH2 : (ofNatCode (unpair m).2).encodeCode = (unpair m).2
⊢ encodeCode
      (match (motive := Bool → Bool → Code) false, false with
      | false, false => (ofNatCode (unpair n.div2.div2).1).pair (ofNatCode (unpair n.div2.div2).2)
      | false, true => (ofNatCode (unpair n.div2.div2).1).comp (ofNatCode (unpair n.div2.div2).2)
      | true, false => (ofNatCode (unpair n.div2.div2).1).prec (ofNatCode (unpair n.div2.div2).2)
      | true, true => (ofNatCode n.div2.div2).rfind') =
    bit false (bit false n.div2.div2) + 4

Tactic:
simp [m, encodeCode, IH, IH1, IH2, Nat.bit_val]

Premises used: Nat.Partrec.Code.encodeCode, Nat.bit_val
-- Module: Mathlib.Computability.PartrecCode
Goal:
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
_m1 : (unpair m).1 < n + 4
_m2 : (unpair m).2 < n + 4
IH : (ofNatCode m).encodeCode = m
IH1 : (ofNatCode (unpair m).1).encodeCode = (unpair m).1
IH2 : (ofNatCode (unpair m).2).encodeCode = (unpair m).2
⊢ encodeCode
      (match (motive := Bool → Bool → Code) false, true with
      | false, false => (ofNatCode (unpair n.div2.div2).1).pair (ofNatCode (unpair n.div2.div2).2)
      | false, true => (ofNatCode (unpair n.div2.div2).1).comp (ofNatCode (unpair n.div2.div2).2)
      | true, false => (ofNatCode (unpair n.div2.div2).1).prec (ofNatCode (unpair n.div2.div2).2)
      | true, true => (ofNatCode n.div2.div2).rfind') =
    bit false (bit true n.div2.div2) + 4

Tactic:
simp [m, encodeCode, IH, IH1, IH2, Nat.bit_val]

Premises used: Nat.Partrec.Code.encodeCode, Nat.bit_val
-- Module: Mathlib.Computability.PartrecCode
Goal:
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
_m1 : (unpair m).1 < n + 4
_m2 : (unpair m).2 < n + 4
IH : (ofNatCode m).encodeCode = m
IH1 : (ofNatCode (unpair m).1).encodeCode = (unpair m).1
IH2 : (ofNatCode (unpair m).2).encodeCode = (unpair m).2
⊢ encodeCode
      (match (motive := Bool → Bool → Code) true, false with
      | false, false => (ofNatCode (unpair n.div2.div2).1).pair (ofNatCode (unpair n.div2.div2).2)
      | false, true => (ofNatCode (unpair n.div2.div2).1).comp (ofNatCode (unpair n.div2.div2).2)
      | true, false => (ofNatCode (unpair n.div2.div2).1).prec (ofNatCode (unpair n.div2.div2).2)
      | true, true => (ofNatCode n.div2.div2).rfind') =
    bit true (bit false n.div2.div2) + 4

Tactic:
simp [m, encodeCode, IH, IH1, IH2, Nat.bit_val]

Premises used: Nat.Partrec.Code.encodeCode, Nat.bit_val
-- Module: Mathlib.Computability.PartrecCode
Goal:
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
_m1 : (unpair m).1 < n + 4
_m2 : (unpair m).2 < n + 4
IH : (ofNatCode m).encodeCode = m
IH1 : (ofNatCode (unpair m).1).encodeCode = (unpair m).1
IH2 : (ofNatCode (unpair m).2).encodeCode = (unpair m).2
⊢ encodeCode
      (match (motive := Bool → Bool → Code) true, true with
      | false, false => (ofNatCode (unpair n.div2.div2).1).pair (ofNatCode (unpair n.div2.div2).2)
      | false, true => (ofNatCode (unpair n.div2.div2).1).comp (ofNatCode (unpair n.div2.div2).2)
      | true, false => (ofNatCode (unpair n.div2.div2).1).prec (ofNatCode (unpair n.div2.div2).2)
      | true, true => (ofNatCode n.div2.div2).rfind') =
    bit true (bit true n.div2.div2) + 4

Tactic:
simp [m, encodeCode, IH, IH1, IH2, Nat.bit_val]

Premises used: Nat.Partrec.Code.encodeCode, Nat.bit_val
-- Module: Mathlib.Computability.PartrecCode
Goal:
c : Code
zero : ofNatCode Code.zero.encodeCode = Code.zero
succ : ofNatCode Code.succ.encodeCode = Code.succ
left : ofNatCode Code.left.encodeCode = Code.left
right : ofNatCode Code.right.encodeCode = Code.right
pair :
  ∀ (a a_1 : Code),
    ofNatCode a.encodeCode = a → ofNatCode a_1.encodeCode = a_1 → ofNatCode (a.pair a_1).encodeCode = a.pair a_1
comp :
  ∀ (a a_1 : Code),
    ofNatCode a.encodeCode = a → ofNatCode a_1.encodeCode = a_1 → ofNatCode (a.comp a_1).encodeCode = a.comp a_1
prec :
  ∀ (a a_1 : Code),
    ofNatCode a.encodeCode = a → ofNatCode a_1.encodeCode = a_1 → ofNatCode (a.prec a_1).encodeCode = a.prec a_1
rfind' : ∀ (a : Code), ofNatCode a.encodeCode = a → ofNatCode a.rfind'.encodeCode = a.rfind'
⊢ ofNatCode c.encodeCode = c

Tactic:
induction c
-- Module: Mathlib.Computability.PartrecCode
Goal:
⊢ ofNatCode zero.encodeCode = zero

Tactic:
simp [encodeCode, ofNatCode, Nat.div2_val, *]

Premises used: Nat.Partrec.Code.encodeCode, Nat.div2_val, Nat.Partrec.Code.ofNatCode
-- Module: Mathlib.Computability.PartrecCode
Goal:
⊢ ofNatCode succ.encodeCode = succ

Tactic:
simp [encodeCode, ofNatCode, Nat.div2_val, *]

Premises used: Nat.Partrec.Code.encodeCode, Nat.div2_val, Nat.Partrec.Code.ofNatCode
-- Module: Mathlib.Computability.PartrecCode
Goal:
⊢ ofNatCode left.encodeCode = left

Tactic:
simp [encodeCode, ofNatCode, Nat.div2_val, *]

Premises used: Nat.Partrec.Code.encodeCode, Nat.div2_val, Nat.Partrec.Code.ofNatCode
-- Module: Mathlib.Computability.PartrecCode
Goal:
⊢ ofNatCode right.encodeCode = right

Tactic:
simp [encodeCode, ofNatCode, Nat.div2_val, *]

Premises used: Nat.Partrec.Code.encodeCode, Nat.div2_val, Nat.Partrec.Code.ofNatCode
-- Module: Mathlib.Computability.PartrecCode
Goal:
a a_1 : Code
a_ih : ofNatCode a.encodeCode = a
a_ih_1 : ofNatCode a_1.encodeCode = a_1
⊢ ofNatCode (a.pair a_1).encodeCode = a.pair a_1

Tactic:
simp [encodeCode, ofNatCode, Nat.div2_val, *]

Premises used: Nat.Partrec.Code.encodeCode, Nat.div2_val, Nat.Partrec.Code.ofNatCode
-- Module: Mathlib.Computability.PartrecCode
Goal:
a a_1 : Code
a_ih : ofNatCode a.encodeCode = a
a_ih_1 : ofNatCode a_1.encodeCode = a_1
⊢ ofNatCode (a.comp a_1).encodeCode = a.comp a_1

Tactic:
simp [encodeCode, ofNatCode, Nat.div2_val, *]

Premises used: Nat.Partrec.Code.encodeCode, Nat.div2_val, Nat.Partrec.Code.ofNatCode
-- Module: Mathlib.Computability.PartrecCode
Goal:
a a_1 : Code
a_ih : ofNatCode a.encodeCode = a
a_ih_1 : ofNatCode a_1.encodeCode = a_1
⊢ ofNatCode (a.prec a_1).encodeCode = a.prec a_1

Tactic:
simp [encodeCode, ofNatCode, Nat.div2_val, *]

Premises used: Nat.Partrec.Code.encodeCode, Nat.div2_val, Nat.Partrec.Code.ofNatCode
-- Module: Mathlib.Computability.PartrecCode
Goal:
a : Code
a_ih : ofNatCode a.encodeCode = a
⊢ ofNatCode a.rfind'.encodeCode = a.rfind'

Tactic:
simp [encodeCode, ofNatCode, Nat.div2_val, *]

Premises used: Nat.Partrec.Code.encodeCode, Nat.div2_val, Nat.Partrec.Code.ofNatCode
-- Module: Mathlib.Computability.PartrecCode
Goal:
⊢ encode = encodeCode

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Computability.PartrecCode
Goal:
⊢ ofNat Code = ofNatCode

Tactic:
rfl

Premises used: WellFounded.Nat.fix, WellFounded.Nat.fix.go, rfl