-- Mathlib/Computability/PartrecCode.lean
theorem encode_ofNatCode : ∀ n, encodeCode (ofNatCode n) = n
  | 0 => by simp [ofNatCode, encodeCode]
  | 1 => by simp [ofNatCode, encodeCode]
  | 2 => by simp [ofNatCode, encodeCode]
  | 3 => by simp [ofNatCode, encodeCode]
  | n + 4 => by
    let m := n.div2.div2
    have hm : m < n + 4

Proof state:
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
⊢ (match 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').encodeCode =
    bit n.bodd (bit n.div2.bodd n.div2.div2) + 4

Tactic:
cases n.bodd <;> cases n.div2.bodd <;>
  simp [m, encodeCode, ofNatCode, IH, IH1, IH2, Nat.bit_val]

Result:
no goals

Proof state:
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

Tactic:
have IH2 := encode_ofNatCode m.unpair.2

Result:
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

Proof state:
⊢ (ofNatCode 0).encodeCode = 0

Tactic:
simp [ofNatCode, encodeCode]

Result:
no goals

Proof state:
n : ℕ
⊢ (ofNatCode (n + 4)).encodeCode = n + 4

Tactic:
let m := n.div2.div2

Result:
n : ℕ
m : ℕ := n.div2.div2
⊢ (ofNatCode (n + 4)).encodeCode = n + 4

Proof state:
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

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

Result:
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

Proof state:
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 _ _))

Result:
no goals

Proof state:
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

Tactic:
have IH1 := encode_ofNatCode m.unpair.1

Result:
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

Proof state:
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

Tactic:
have IH := encode_ofNatCode m

Result:
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

Proof state:
⊢ (ofNatCode 1).encodeCode = 1

Tactic:
simp [ofNatCode, encodeCode]

Result:
no goals

Proof state:
⊢ (ofNatCode 2).encodeCode = 2

Tactic:
simp [ofNatCode, encodeCode]

Result:
no goals

Proof state:
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
⊢ (ofNatCode (n + 4)).encodeCode = n + 4

Tactic:
have _m1 : m.unpair.1 < n + 4 := lt_of_le_of_lt m.unpair_left_le hm

Result:
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
_m1 : (unpair m).1 < n + 4
⊢ (ofNatCode (n + 4)).encodeCode = n + 4

Proof state:
⊢ (ofNatCode 3).encodeCode = 3

Tactic:
simp [ofNatCode, encodeCode]

Result:
no goals

Proof state:
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

Tactic:
simp only [ofNatCode.eq_5]

Result:
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
⊢ (match 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').encodeCode =
    bit n.bodd (bit n.div2.bodd n.div2.div2) + 4

Proof state:
n : ℕ
m : ℕ := n.div2.div2
⊢ (ofNatCode (n + 4)).encodeCode = 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 _ _))

Result:
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
⊢ (ofNatCode (n + 4)).encodeCode = n + 4

Proof state:
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
_m1 : (unpair m).1 < n + 4
⊢ (ofNatCode (n + 4)).encodeCode = n + 4

Tactic:
have _m2 : m.unpair.2 < n + 4 := lt_of_le_of_lt m.unpair_right_le hm

Result:
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

Proof state:
n : ℕ
m : ℕ := n.div2.div2
⊢ m < n + 4

Tactic:
simp only [m, div2_val]

Result:
n : ℕ
m : ℕ := n.div2.div2
⊢ n / 2 / 2 < n + 4