awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.PartrecBasis (goal)
Goal:
n_1 : ℕ
f : List.Vector ℕ (n_1 + 1) → ℕ
hf : Partrec' (↑f : List.Vector ℕ (n_1 + 1) →. ℕ)
v : List.Vector ℕ n_1
b a n : ℕ
⊢ Part.some (decide (1 ≤ f (n ::ᵥ v))) = (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n ::ᵥ v))))) : Part Bool)
have refine_1 : Part.some (decide (LE.le (α := ℕ) 1 0)) = (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) 0))) : Part Bool)
Tactic: cases f (n ::ᵥ v)
-- Lean 4 proof step from Mathlib.Computability.PartrecBasis (goal)
Goal:
n_1 : ℕ
f : List.Vector ℕ (n_1 + 1) → ℕ
hf : Partrec' (↑f : List.Vector ℕ (n_1 + 1) →. ℕ)
v : List.Vector ℕ n_1
b a n : ℕ
refine_1 : Part.some (decide (LE.le (α := ℕ) 1 0)) = (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) 0))) : Part Bool)
⊢ Part.some (decide (1 ≤ f (n ::ᵥ v))) = (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n ::ᵥ v))))) : Part Bool)
have refine_1₁ : ∀ (n : ℕ), Part.some (decide (1 ≤ n + 1)) = (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (n + 1)))) : Part Bool)
Tactic: cases f (n ::ᵥ v)
-- Lean 4 proof step from Mathlib.Computability.PartrecBasis (goal)
Goal:
n_1 : ℕ
f : List.Vector ℕ (n_1 + 1) → ℕ
hf : Partrec' (↑f : List.Vector ℕ (n_1 + 1) →. ℕ)
v : List.Vector ℕ n_1
b a n : ℕ
⊢ Part.some (decide (LE.le (α := ℕ) 1 0)) = (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) 0))) : Part Bool)
have refine_1 : Eq (α := Option ℕ) (ofNat (Option ℕ) 0) Option.none
Tactic: simp
-- Lean 4 proof step from Mathlib.Computability.PartrecBasis (goal)
Goal:
n_1 : ℕ
f : List.Vector ℕ (n_1 + 1) → ℕ
hf : Partrec' (↑f : List.Vector ℕ (n_1 + 1) →. ℕ)
v : List.Vector ℕ n_1
b a n n_2 : ℕ
⊢ Part.some (decide (1 ≤ n_2 + 1)) = (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (n_2 + 1)))) : Part Bool)
have refine_1 : Option.isSome (α := ℕ) (ofNat (Option ℕ) (n_2 + 1)) = true
Tactic: simp
-- Lean 4 proof step from Mathlib.Computability.PartrecBasis (hypothesis)
Goal:
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
v : List.Vector ℕ n
b 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
have this : true ∈ (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (a ::ᵥ v))))) : Part Bool)
Tactic: have := Nat.rfind_spec h
-- Lean 4 proof step from Mathlib.Computability.PartrecBasis (hypothesis)
Goal:
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun (n_1 : ℕ) ↦ (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool)
this : true ∈ (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (a ::ᵥ v))))) : Part Bool)
⊢ b = (f (a ::ᵥ v)).pred ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b
have this₁ : true = Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (a ::ᵥ v)))
Tactic: simp only [Part.coe_some, Part.mem_some_iff] at this
Cleared hypotheses: this
-- 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 : ℕ
h : a ∈ Nat.rfind fun (n_1 : ℕ) ↦ (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool)
this : true = Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (a ::ᵥ v)))
⊢ b = (f (a ::ᵥ v)).pred ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b
have refine_2 : ∀ (this : true = Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (a ::ᵥ v)))),
  b = (f (a ::ᵥ v)).pred ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b
Tactic: revert this
Cleared hypotheses: this
-- 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 : ℕ
h : a ∈ Nat.rfind fun (n_1 : ℕ) ↦ (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool)
⊢ ∀ (this : true = Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (a ::ᵥ v)))),
    b = (f (a ::ᵥ v)).pred ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b
have refine_2 : ∀ (this : true = Option.isSome (α := ℕ) (ofNat (Option ℕ) 0)), b = pred 0 ↔ ofNat (Option ℕ) 0 = some b
Tactic: rcases f (a ::ᵥ v) with - | c
-- 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 : ℕ
h : a ∈ Nat.rfind fun (n_1 : ℕ) ↦ (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool)
refine_2 : ∀ (this : true = Option.isSome (α := ℕ) (ofNat (Option ℕ) 0)), b = pred 0 ↔ ofNat (Option ℕ) 0 = some b
⊢ ∀ (this : true = Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (a ::ᵥ v)))),
    b = (f (a ::ᵥ v)).pred ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b
have refine_2₁ : ∀ (c : ℕ) (this : true = Option.isSome (α := ℕ) (ofNat (Option ℕ) (c + 1))),
  b = (c + 1).pred ↔ ofNat (Option ℕ) (c + 1) = some b
Tactic: rcases f (a ::ᵥ v) with - | c
-- 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 : ℕ
h : a ∈ Nat.rfind fun (n_1 : ℕ) ↦ (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool)
c : ℕ
this : true = Option.isSome (α := ℕ) (ofNat (Option ℕ) (c + 1))
⊢ b = (c + 1).pred ↔ ofNat (Option ℕ) (c + 1) = some b
have refine_2 : some (c + 1).pred = some b ↔ ofNat (Option ℕ) (c + 1) = some b
Tactic: rw [← Option.some_inj, eq_comm]
-- Lean 4 proof step from Mathlib.Computability.PartrecBasis (goal)
Goal:
f : ℕ →. ℕ
hf : Nat.Partrec f
⊢ Partrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ f v.head
have obtain : ∀ (c : Code) (hf : Nat.Partrec c.eval), Partrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ c.eval v.head
Tactic: obtain ⟨c, rfl⟩ := exists_code.1 hf
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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)))
have fun : Nat.Partrec (unpaired fun (a b : ℕ) ↦ Nat.rfind fun (n : ℕ) ↦ (fun (m : ℕ) ↦ decide (m = 0)) <$> f (Nat.pair a (n + b)))
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₂
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
f : ℕ →. ℕ
hf : Nat.Partrec f
⊢ Nat.Partrec
    (unpaired fun (a b : ℕ) ↦ Nat.rfind fun (n : ℕ) ↦ (fun (m : ℕ) ↦ decide (m = 0)) <$> f (Nat.pair a (n + b)))
have 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)
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))
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
n₁ n₂ : ℕ
h : succ.comp (Code.const n₁) = succ.comp (Code.const n₂)
⊢ n₁ + 1 = n₂ + 1
have h₁ : succ = succ
Tactic: injection h with h₁ h₂
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
n₁ n₂ : ℕ
h : succ.comp (Code.const n₁) = succ.comp (Code.const n₂)
h₁ : succ = succ
⊢ n₁ + 1 = n₂ + 1
have h₂ : Code.const n₁ = Code.const n₂
Tactic: injection h with h₁ h₂
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
n : ℕ
m : ℕ := n.div2.div2
⊢ m < n + 4
have simp : n / 2 / 2 < n + 4
Tactic: simp only [m, div2_val]
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
n : ℕ
m : ℕ := n.div2.div2
⊢ (ofNatCode (n + 4)).encodeCode = n + 4
have hm : 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 _ _))
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
⊢ (ofNatCode (n + 4)).encodeCode = n + 4
have _m1 : (unpair m).1 < n + 4
Tactic: have _m1 : m.unpair.1 < n + 4 := lt_of_le_of_lt m.unpair_left_le hm
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
_m1 : (unpair m).1 < n + 4
⊢ (ofNatCode (n + 4)).encodeCode = n + 4
have _m2 : (unpair m).2 < n + 4
Tactic: have _m2 : m.unpair.2 < n + 4 := lt_of_le_of_lt m.unpair_right_le hm
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
_m1 : (unpair m).1 < n + 4
_m2 : (unpair m).2 < n + 4
⊢ (ofNatCode (n + 4)).encodeCode = n + 4
have IH : (ofNatCode m).encodeCode = m
Tactic: have IH := encode_ofNatCode m
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
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 (n + 4)).encodeCode = n + 4
have IH1 : (ofNatCode (unpair m).1).encodeCode = (unpair m).1
Tactic: have IH1 := encode_ofNatCode m.unpair.1
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
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 (n + 4)).encodeCode = n + 4
have IH2 : (ofNatCode (unpair m).2).encodeCode = (unpair m).2
Tactic: have IH2 := encode_ofNatCode m.unpair.2
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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
| n + 4
have rw : bit n.bodd (bit n.div2.bodd n.div2.div2) + 4
Tactic: rw [← Nat.bit_bodd_div2 n, ← Nat.bit_bodd_div2 n.div2]
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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
⊢ (ofNatCode (n + 4)).encodeCode = n + 4
have conv_rhs : (ofNatCode (n + 4)).encodeCode = bit n.bodd (bit n.div2.bodd n.div2.div2) + 4
Tactic: conv_rhs => rw [← Nat.bit_bodd_div2 n, ← Nat.bit_bodd_div2 n.div2]
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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
⊢ (ofNatCode (n + 4)).encodeCode = bit n.bodd (bit n.div2.bodd n.div2.div2) + 4
have 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
Tactic: simp only [ofNatCode.eq_5]
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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) 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
have false : encodeCode
    (match (motive := Bool → Bool → Code) false, 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 false (bit n.div2.bodd n.div2.div2) + 4
Tactic: cases n.bodd
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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, 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
⊢ 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, 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 n.bodd (bit n.div2.bodd n.div2.div2) + 4
have true : encodeCode
    (match (motive := Bool → Bool → Code) true, 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 true (bit n.div2.bodd n.div2.div2) + 4
Tactic: cases n.bodd
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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, 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 false (bit n.div2.bodd n.div2.div2) + 4
have false : 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: cases n.div2.bodd
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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
⊢ 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
have 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
Tactic: cases n.div2.bodd
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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, 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 true (bit n.div2.bodd n.div2.div2) + 4
have true : 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: cases n.div2.bodd
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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
⊢ 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
have 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
Tactic: cases n.div2.bodd
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
c : Code
⊢ ofNatCode c.encodeCode = c
have zero : ofNatCode zero.encodeCode = zero
Tactic: induction c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
c : Code
zero : ofNatCode Code.zero.encodeCode = Code.zero
⊢ ofNatCode c.encodeCode = c
have succ : ofNatCode succ.encodeCode = succ
Tactic: induction c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
c : Code
zero : ofNatCode Code.zero.encodeCode = Code.zero
succ : ofNatCode Code.succ.encodeCode = Code.succ
⊢ ofNatCode c.encodeCode = c
have left : ofNatCode left.encodeCode = left
Tactic: induction c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
c : Code
zero : ofNatCode Code.zero.encodeCode = Code.zero
succ : ofNatCode Code.succ.encodeCode = Code.succ
left : ofNatCode Code.left.encodeCode = Code.left
⊢ ofNatCode c.encodeCode = c
have right : ofNatCode right.encodeCode = right
Tactic: induction c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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
⊢ ofNatCode c.encodeCode = c
have 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
Tactic: induction c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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
⊢ ofNatCode c.encodeCode = c
have 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
Tactic: induction c
Cleared hypotheses: c