awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
h : Primcodable α
n : ℕ
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (n + 1) 1 fun (n : ℕ) ↦
      Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_1} (α := Option α) (decode n)) 0 fun (n : ℕ) ↦ n.succ.succ) =
    encode.{u_1} (α := Option (Option α)) (Option.map some (decode n))
have succ : ∀ (H : Eq.{u_1 + 1} (α := Option α) (decode n) none),
  (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (n + 1) 1 fun (n : ℕ) ↦
      Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_1} (α := Option α) (decode n)) 0 fun (n : ℕ) ↦ n.succ.succ) =
    encode.{u_1} (α := Option (Option α)) (Option.map some none)
Tactic: cases H : @decode α _ n
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
h : Primcodable α
n : ℕ
succ :
  ∀ (H : Eq.{u_1 + 1} (α := Option α) (decode n) none),
    (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (n + 1) 1 fun (n : ℕ) ↦
        Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_1} (α := Option α) (decode n)) 0 fun (n : ℕ) ↦ n.succ.succ) =
      encode.{u_1} (α := Option (Option α)) (Option.map some none)
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (n + 1) 1 fun (n : ℕ) ↦
      Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_1} (α := Option α) (decode n)) 0 fun (n : ℕ) ↦ n.succ.succ) =
    encode.{u_1} (α := Option (Option α)) (Option.map some (decode n))
have succ₁ : ∀ (val : α) (H : decode n = some val),
  (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (n + 1) 1 fun (n : ℕ) ↦
      Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_1} (α := Option α) (decode n)) 0 fun (n : ℕ) ↦ n.succ.succ) =
    encode (Option.map some (some val))
Tactic: cases H : @decode α _ n
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
h : Primcodable α
n : ℕ
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) n 1 fun (n : ℕ) ↦
      Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_1} (α := Option α) (decode n)) 0 fun (n : ℕ) ↦ n.succ.succ) =
    encode.{u_1} (α := Option (Option α)) (decode n)
have zero : (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) 0 1 fun (n : ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_1} (α := Option α) (decode n)) 0 fun (n : ℕ) ↦ n.succ.succ) =
  encode.{u_1} (α := Option (Option α)) (decode 0)
Tactic: cases n with
      | zero => rfl
      | succ n =>
        rw [decode_option_succ]
        cases H : @decode α _ n <;> simp [H]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
h : Primcodable α
n : ℕ
zero :
  (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) 0 1 fun (n : ℕ) ↦
      Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_1} (α := Option α) (decode n)) 0 fun (n : ℕ) ↦ n.succ.succ) =
    encode.{u_1} (α := Option (Option α)) (decode 0)
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) n 1 fun (n : ℕ) ↦
      Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_1} (α := Option α) (decode n)) 0 fun (n : ℕ) ↦ n.succ.succ) =
    encode.{u_1} (α := Option (Option α)) (decode n)
have succ : ∀ (n : ℕ),
  (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (n + 1) 1 fun (n : ℕ) ↦
      Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_1} (α := Option α) (decode n)) 0 fun (n : ℕ) ↦ n.succ.succ) =
    encode.{u_1} (α := Option (Option α)) (decode (n + 1))
Tactic: cases n with
      | zero => rfl
      | succ n =>
        rw [decode_option_succ]
        cases H : @decode α _ n <;> simp [H]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
n_1 n : ℕ
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (n + 2) 1 fun (x : ℕ) ↦
      Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) x 2 fun (x : ℕ) ↦ 0) =
    encode (α := Option Bool) (decode (n + 2))
have rw : (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (n + 2) 1 fun (x : ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) x 2 fun (x : ℕ) ↦ 0) =
  encode (α := Option Bool) none
Tactic: rw [decode_ge_two]
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
n_1 n : ℕ
rw :
  (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (n + 2) 1 fun (x : ℕ) ↦
      Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) x 2 fun (x : ℕ) ↦ 0) =
    encode (α := Option Bool) none
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (n + 2) 1 fun (x : ℕ) ↦
      Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) x 2 fun (x : ℕ) ↦ 0) =
    encode (α := Option Bool) (decode (n + 2))
have h : 2 ≤ n + 2
Tactic: rw [decode_ge_two]
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
⊢ encode.{u_1} (α := Option α) (decode n) = encode (Option.map.{u_1, 0} (α := α) encode (decode n))
have none : encode.{u_1} (α := Option α) none = encode (Option.map.{u_1, 0} (α := α) encode none)
Tactic: cases @decode α _ n
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
none : encode.{u_1} (α := Option α) Option.none = encode (Option.map.{u_1, 0} (α := α) encode Option.none)
⊢ encode.{u_1} (α := Option α) (decode n) = encode (Option.map.{u_1, 0} (α := α) encode (decode n))
have some : ∀ (val : α), encode (some val) = encode (Option.map encode (some val))
Tactic: cases @decode α _ n
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_1} (α := Option α) (decode n)) 0 fun (n : ℕ) ↦ n.succ.succ) =
    encode.{u_1} (α := Option (Option α)) (Option.map some (decode n))
have none : (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_1} (α := Option α) none) 0 fun (n : ℕ) ↦ n.succ.succ) =
  encode.{u_1} (α := Option (Option α)) (Option.map some none)
Tactic: cases @decode α _ n
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
none :
  (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_1} (α := Option α) Option.none) 0 fun (n : ℕ) ↦ n.succ.succ) =
    encode.{u_1} (α := Option (Option α)) (Option.map some Option.none)
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_1} (α := Option α) (decode n)) 0 fun (n : ℕ) ↦ n.succ.succ) =
    encode.{u_1} (α := Option (Option α)) (Option.map some (decode n))
have some : ∀ (val : α),
  (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode (some val)) 0 fun (n : ℕ) ↦ n.succ.succ) =
    encode (Option.map some (some val))
Tactic: cases @decode α _ n
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
x : σ
n : ℕ
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_1} (α := Option α) (decode n)) 0 fun (x_1 : ℕ) ↦
      (encode x).succ) =
    encode.{u_3} (α := Option σ) (Option.map (fun (x_1 : α) ↦ x) (decode n))
have none : (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_1} (α := Option α) none) 0 fun (x_1 : ℕ) ↦ (encode x).succ) =
  encode.{u_3} (α := Option σ) (Option.map (fun (x_1 : α) ↦ x) none)
Tactic: cases @decode α _ n
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
x : σ
n : ℕ
none :
  (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_1} (α := Option α) Option.none) 0 fun (x_1 : ℕ) ↦
      (encode x).succ) =
    encode.{u_3} (α := Option σ) (Option.map (fun (x_1 : α) ↦ x) Option.none)
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_1} (α := Option α) (decode n)) 0 fun (x_1 : ℕ) ↦
      (encode x).succ) =
    encode.{u_3} (α := Option σ) (Option.map (fun (x_1 : α) ↦ x) (decode n))
have some : ∀ (val : α),
  (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode (some val)) 0 fun (x_1 : ℕ) ↦ (encode x).succ) =
    encode.{u_3} (α := Option σ) (Option.map (fun (x_1 : α) ↦ x) (some val))
Tactic: cases @decode α _ n
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : β → σ
g : α → β
hf : Primrec f
hg : Primrec g
n : ℕ
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_1} (α := Option α) (decode n)) 0 fun (n : ℕ) ↦
      encode (Option.map f (decode (encode (Option.map g (decode n))).pred))) =
    encode.{u_3} (α := Option σ) (Option.map (fun (a : α) ↦ f (g a)) (decode n))
have none : (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_1} (α := Option α) none) 0 fun (n : ℕ) ↦
    encode (Option.map f (decode (encode (Option.map g (decode n))).pred))) =
  encode.{u_3} (α := Option σ) (Option.map (fun (a : α) ↦ f (g a)) none)
Tactic: cases @decode α _ n
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : β → σ
g : α → β
hf : Primrec f
hg : Primrec g
n : ℕ
none :
  (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_1} (α := Option α) Option.none) 0 fun (n : ℕ) ↦
      encode (Option.map f (decode (encode (Option.map g (decode n))).pred))) =
    encode.{u_3} (α := Option σ) (Option.map (fun (a : α) ↦ f (g a)) Option.none)
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_1} (α := Option α) (decode n)) 0 fun (n : ℕ) ↦
      encode (Option.map f (decode (encode (Option.map g (decode n))).pred))) =
    encode.{u_3} (α := Option σ) (Option.map (fun (a : α) ↦ f (g a)) (decode n))
have some : ∀ (val : α),
  (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode (some val)) 0 fun (n : ℕ) ↦
      encode (Option.map f (decode (encode (Option.map g (decode n))).pred))) =
    encode.{u_3} (α := Option σ) (Option.map (fun (a : α) ↦ f (g a)) (some val))
Tactic: cases @decode α _ n
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
f : α → σ
h : Primrec (β := ℕ) fun (a : α) ↦ encode (f a)
n : ℕ
⊢ encode (α := Option ℕ) (Option.map (fun (a : α) ↦ encode (f a)) (decode n)) = encode (Option.map f (decode n))
have none : encode (α := Option ℕ) (Option.map (fun (a : α) ↦ encode (f a)) none) = encode (Option.map f none)
Tactic: cases @decode α _ n
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
f : α → σ
h : Primrec (β := ℕ) fun (a : α) ↦ encode (f a)
n : ℕ
none : encode (α := Option ℕ) (Option.map (fun (a : α) ↦ encode (f a)) Option.none) = encode (Option.map f Option.none)
⊢ encode (α := Option ℕ) (Option.map (fun (a : α) ↦ encode (f a)) (decode n)) = encode (Option.map f (decode n))
have some : ∀ (val : α),
  encode (α := Option ℕ) (Option.map (fun (a : α) ↦ encode (f a)) (some val)) = encode (Option.map f (some val))
Tactic: cases @decode α _ n
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
⊢ Nat.unpaired
      (fun (z n : ℕ) ↦
        Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) n 0 fun (y : ℕ) ↦
          Nat.unpaired (fun (z n : ℕ) ↦ Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) n 0 fun (y : ℕ) ↦ (Nat.pair z y).succ)
            (Nat.pair (Nat.unpair (Nat.pair z y)).2
              (encode.{u_2} (α := Option β) (decode (Nat.unpair (Nat.pair z y)).1))))
      (Nat.pair (Nat.unpair n).2 (encode.{u_1} (α := Option α) (decode (Nat.unpair n).1))) =
    encode (α := Option (α × β)) (decode n)
have simp : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
    (fun (n_1 n_ih : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n n_ih : ℕ) ↦ (Nat.pair n_1 n).succ)
        (encode.{u_2} (α := Option β) (decode (Nat.unpair n).2)))
    (encode.{u_1} (α := Option α) (decode (Nat.unpair n).1)) =
  encode (α := Option (α × β))
    (Option.bind (decode (Nat.unpair n).1) fun (a : α) ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2))
Tactic: simp only [Nat.unpaired, Nat.unpair_pair, decode_prod_val]
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
      (fun (n_1 n_ih : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n n_ih : ℕ) ↦ (Nat.pair n_1 n).succ)
          (encode.{u_2} (α := Option β) (decode (Nat.unpair n).2)))
      (encode.{u_1} (α := Option α) (decode (Nat.unpair n).1)) =
    encode (α := Option (α × β))
      (Option.bind (decode (Nat.unpair n).1) fun (a : α) ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2))
have none : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
    (fun (n_1 n_ih : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n n_ih : ℕ) ↦ (Nat.pair n_1 n).succ)
        (encode.{u_2} (α := Option β) (decode (Nat.unpair n).2)))
    (encode.{u_1} (α := Option α) none) =
  encode (α := Option (α × β)) (Option.bind none fun (a : α) ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2))
Tactic: cases @decode α _ n.unpair.1
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
none :
  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
      (fun (n_1 n_ih : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n n_ih : ℕ) ↦ (Nat.pair n_1 n).succ)
          (encode.{u_2} (α := Option β) (decode (Nat.unpair n).2)))
      (encode.{u_1} (α := Option α) Option.none) =
    encode (α := Option (α × β))
      (Option.bind Option.none fun (a : α) ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2))
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
      (fun (n_1 n_ih : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n n_ih : ℕ) ↦ (Nat.pair n_1 n).succ)
          (encode.{u_2} (α := Option β) (decode (Nat.unpair n).2)))
      (encode.{u_1} (α := Option α) (decode (Nat.unpair n).1)) =
    encode (α := Option (α × β))
      (Option.bind (decode (Nat.unpair n).1) fun (a : α) ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2))
have some : ∀ (val : α),
  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
      (fun (n_1 n_ih : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n n_ih : ℕ) ↦ (Nat.pair n_1 n).succ)
          (encode.{u_2} (α := Option β) (decode (Nat.unpair n).2)))
      (encode (some val)) =
    encode (α := Option (α × β)) ((some val).bind fun (a : α) ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2))
Tactic: cases @decode α _ n.unpair.1
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
val : α
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
      (fun (n_1 n_ih : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n n_ih : ℕ) ↦ (Nat.pair n_1 n).succ)
          (encode.{u_2} (α := Option β) (decode (Nat.unpair n).2)))
      (encode (some val)) =
    encode (α := Option (α × β)) ((some val).bind fun (a : α) ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2))
have some : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
    (fun (n n_ih : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n_1 n_ih : ℕ) ↦ (Nat.pair n n_1).succ)
        (encode.{u_2} (α := Option β) none))
    (encode (some val)) =
  encode (α := Option (α × β)) ((some val).bind fun (a : α) ↦ Option.map (Prod.mk a) none)
Tactic: cases @decode β _ n.unpair.2
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
val : α
some :
  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
      (fun (n n_ih : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n_1 n_ih : ℕ) ↦ (Nat.pair n n_1).succ)
          (encode.{u_2} (α := Option β) none))
      (encode (Option.some val)) =
    encode (α := Option (α × β)) ((Option.some val).bind fun (a : α) ↦ Option.map (Prod.mk a) none)
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
      (fun (n_1 n_ih : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n n_ih : ℕ) ↦ (Nat.pair n_1 n).succ)
          (encode.{u_2} (α := Option β) (decode (Nat.unpair n).2)))
      (encode (Option.some val)) =
    encode (α := Option (α × β)) ((Option.some val).bind fun (a : α) ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2))
have some₁ : ∀ (val_1 : β),
  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
      (fun (n n_ih : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n_1 n_ih : ℕ) ↦ (Nat.pair n n_1).succ) (encode (Option.some val_1)))
      (encode (Option.some val)) =
    encode (α := Option (α × β)) ((Option.some val).bind fun (a : α) ↦ Option.map (Prod.mk a) (Option.some val_1))
Tactic: cases @decode β _ n.unpair.2
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
⊢ Nat.unpaired
      (fun (z n : ℕ) ↦
        Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) n 0 fun (y : ℕ) ↦
          Nat.unpaired
            (fun (z n : ℕ) ↦
              Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) n 0 fun (y : ℕ) ↦ (Nat.unpair (Nat.pair z y)).1.succ)
            (Nat.pair (Nat.unpair (Nat.pair z y)).2
              (encode.{u_3} (α := Option β) (decode (Nat.unpair (Nat.pair z y)).1))))
      (Nat.pair (Nat.unpair n).2 (encode.{u_2} (α := Option α) (decode (Nat.unpair n).1))) =
    encode.{u_2} (α := Option α) (Option.map (α := α × β) Prod.fst (decode n))
have simp : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
    (fun (n_1 n_ih : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n n_ih : ℕ) ↦ n_1.succ)
        (encode.{u_3} (α := Option β) (decode (Nat.unpair n).2)))
    (encode.{u_2} (α := Option α) (decode (Nat.unpair n).1)) =
  encode.{u_2} (α := Option α)
    (Option.map (α := α × β) Prod.fst
      (Option.bind (decode (Nat.unpair n).1) fun (a : α) ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)))
Tactic: simp only [Nat.unpaired, Nat.unpair_pair, decode_prod_val]
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
      (fun (n_1 n_ih : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n n_ih : ℕ) ↦ n_1.succ)
          (encode.{u_3} (α := Option β) (decode (Nat.unpair n).2)))
      (encode.{u_2} (α := Option α) (decode (Nat.unpair n).1)) =
    encode.{u_2} (α := Option α)
      (Option.map (α := α × β) Prod.fst
        (Option.bind (decode (Nat.unpair n).1) fun (a : α) ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)))
have none : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
    (fun (n_1 n_ih : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n n_ih : ℕ) ↦ n_1.succ)
        (encode.{u_3} (α := Option β) (decode (Nat.unpair n).2)))
    (encode.{u_2} (α := Option α) none) =
  encode.{u_2} (α := Option α)
    (Option.map (α := α × β) Prod.fst (Option.bind none fun (a : α) ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)))
Tactic: cases @decode α _ n.unpair.1
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
none :
  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
      (fun (n_1 n_ih : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n n_ih : ℕ) ↦ n_1.succ)
          (encode.{u_3} (α := Option β) (decode (Nat.unpair n).2)))
      (encode.{u_2} (α := Option α) Option.none) =
    encode.{u_2} (α := Option α)
      (Option.map (α := α × β) Prod.fst
        (Option.bind Option.none fun (a : α) ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)))
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
      (fun (n_1 n_ih : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n n_ih : ℕ) ↦ n_1.succ)
          (encode.{u_3} (α := Option β) (decode (Nat.unpair n).2)))
      (encode.{u_2} (α := Option α) (decode (Nat.unpair n).1)) =
    encode.{u_2} (α := Option α)
      (Option.map (α := α × β) Prod.fst
        (Option.bind (decode (Nat.unpair n).1) fun (a : α) ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)))
have some : ∀ (val : α),
  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
      (fun (n_1 n_ih : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n n_ih : ℕ) ↦ n_1.succ)
          (encode.{u_3} (α := Option β) (decode (Nat.unpair n).2)))
      (encode (some val)) =
    encode.{u_2} (α := Option α)
      (Option.map (α := α × β) Prod.fst
        ((some val).bind fun (a : α) ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)))
Tactic: cases @decode α _ n.unpair.1
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
val : α
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
      (fun (n_1 n_ih : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n n_ih : ℕ) ↦ n_1.succ)
          (encode.{u_3} (α := Option β) (decode (Nat.unpair n).2)))
      (encode (some val)) =
    encode.{u_2} (α := Option α)
      (Option.map (α := α × β) Prod.fst
        ((some val).bind fun (a : α) ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)))
have some : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n n_ih : ℕ) ↦ encode val + 1)
    (encode.{u_3} (α := Option β) (decode (Nat.unpair n).2)) =
  encode (Option.map (Function.const β val) (decode (Nat.unpair n).2))
Tactic: simp
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
val : α
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n n_ih : ℕ) ↦ encode val + 1)
      (encode.{u_3} (α := Option β) (decode (Nat.unpair n).2)) =
    encode (Option.map (Function.const β val) (decode (Nat.unpair n).2))
have some : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n n_ih : ℕ) ↦ encode val + 1) (encode.{u_3} (α := Option β) none) =
  encode (Option.map (Function.const β val) none)
Tactic: cases @decode β _ n.unpair.2
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
val : α
some :
  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n n_ih : ℕ) ↦ encode val + 1) (encode.{u_3} (α := Option β) none) =
    encode (Option.map (Function.const β val) none)
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n n_ih : ℕ) ↦ encode val + 1)
      (encode.{u_3} (α := Option β) (decode (Nat.unpair n).2)) =
    encode (Option.map (Function.const β val) (decode (Nat.unpair n).2))
have some₁ : ∀ (val_1 : β),
  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n n_ih : ℕ) ↦ encode val + 1) (encode (Option.some val_1)) =
    encode (Option.map (Function.const β val) (Option.some val_1))
Tactic: cases @decode β _ n.unpair.2
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
⊢ Nat.unpaired
      (fun (z n : ℕ) ↦
        Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) n 0 fun (y : ℕ) ↦
          Nat.unpaired
            (fun (z n : ℕ) ↦
              Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) n 0 fun (y : ℕ) ↦ (Nat.unpair (Nat.pair z y)).2.succ)
            (Nat.pair (Nat.unpair (Nat.pair z y)).2
              (encode.{u_3} (α := Option β) (decode (Nat.unpair (Nat.pair z y)).1))))
      (Nat.pair (Nat.unpair n).2 (encode.{u_2} (α := Option α) (decode (Nat.unpair n).1))) =
    encode.{u_3} (α := Option β) (Option.map (α := α × β) Prod.snd (decode n))
have simp : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
    (fun (n_1 n_ih : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n n_ih : ℕ) ↦ n.succ)
        (encode.{u_3} (α := Option β) (decode (Nat.unpair n).2)))
    (encode.{u_2} (α := Option α) (decode (Nat.unpair n).1)) =
  encode.{u_3} (α := Option β)
    (Option.map (α := α × β) Prod.snd
      (Option.bind (decode (Nat.unpair n).1) fun (a : α) ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)))
Tactic: simp only [Nat.unpaired, Nat.unpair_pair, decode_prod_val]