awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.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)))
have none : 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 α) none) =
  encode.{u_3} (α := Option β)
    (Option.map (α := α × β) Prod.snd (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.succ)
          (encode.{u_3} (α := Option β) (decode (Nat.unpair n).2)))
      (encode.{u_2} (α := Option α) Option.none) =
    encode.{u_3} (α := Option β)
      (Option.map (α := α × β) Prod.snd
        (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.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)))
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.succ)
          (encode.{u_3} (α := Option β) (decode (Nat.unpair n).2)))
      (encode (some val)) =
    encode.{u_3} (α := Option β)
      (Option.map (α := α × β) Prod.snd
        ((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.succ)
          (encode.{u_3} (α := Option β) (decode (Nat.unpair n).2)))
      (encode (some val)) =
    encode.{u_3} (α := Option β)
      (Option.map (α := α × β) Prod.snd
        ((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 : ℕ) ↦ n + 1)
    (encode.{u_3} (α := Option β) (decode (Nat.unpair n).2)) =
  encode.{u_3} (α := Option β) (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 : ℕ) ↦ n + 1)
      (encode.{u_3} (α := Option β) (decode (Nat.unpair n).2)) =
    encode.{u_3} (α := Option β) (decode (Nat.unpair n).2)
have some : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n n_ih : ℕ) ↦ n + 1) (encode.{u_3} (α := Option β) none) =
  encode.{u_3} (α := Option β) 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 : ℕ) ↦ n + 1) (encode.{u_3} (α := Option β) none) =
    encode.{u_3} (α := Option β) none
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n n_ih : ℕ) ↦ n + 1)
      (encode.{u_3} (α := Option β) (decode (Nat.unpair n).2)) =
    encode.{u_3} (α := Option β) (decode (Nat.unpair n).2)
have some₁ : ∀ (val : β),
  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n n_ih : ℕ) ↦ n + 1) (encode (Option.some val)) = encode (Option.some val)
Tactic: cases @decode β _ n.unpair.2
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
f : α → β
g : α → γ
hf : Primrec f
hg : Primrec g
n : ℕ
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_2} (α := Option α) (decode n)) 0 fun (n : ℕ) ↦
      (Nat.pair (encode (Option.map f (decode n))).pred (encode (Option.map g (decode n))).pred).succ) =
    encode (α := Option (β × γ)) (Option.map (fun (a : α) ↦ (f a, g a)) (decode n))
have none : (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_2} (α := Option α) none) 0 fun (n : ℕ) ↦
    (Nat.pair (encode (Option.map f (decode n))).pred (encode (Option.map g (decode n))).pred).succ) =
  encode (α := Option (β × γ)) (Option.map (fun (a : α) ↦ (f a, g a)) none)
Tactic: cases @decode α _ n
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
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_2} (α := Option α) Option.none) 0 fun (n : ℕ) ↦
      (Nat.pair (encode (Option.map f (decode n))).pred (encode (Option.map g (decode n))).pred).succ) =
    encode (α := Option (β × γ)) (Option.map (fun (a : α) ↦ (f a, g a)) Option.none)
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_2} (α := Option α) (decode n)) 0 fun (n : ℕ) ↦
      (Nat.pair (encode (Option.map f (decode n))).pred (encode (Option.map g (decode n))).pred).succ) =
    encode (α := Option (β × γ)) (Option.map (fun (a : α) ↦ (f a, g a)) (decode n))
have some : ∀ (val : α),
  (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode (some val)) 0 fun (n : ℕ) ↦
      (Nat.pair (encode (Option.map f (decode n))).pred (encode (Option.map g (decode n))).pred).succ) =
    encode (α := Option (β × γ)) (Option.map (fun (a : α) ↦ (f a, g a)) (some val))
Tactic: cases @decode α _ n
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
inst : Primcodable α
a : α
l : List α
n : ℕ
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) n (encode a).succ fun (n : ℕ) ↦
      encode (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (ofNat ℕ n))) =
    encode (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) (ofNat ℕ n))
have zero : (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) 0 (encode a).succ fun (n : ℕ) ↦
    encode (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (ofNat ℕ n))) =
  encode (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) (ofNat ℕ 0))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
inst : Primcodable α
a : α
l : List α
n : ℕ
zero :
  (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) 0 (encode a).succ fun (n : ℕ) ↦
      encode (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (ofNat ℕ n))) =
    encode (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) (ofNat ℕ 0))
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) n (encode a).succ fun (n : ℕ) ↦
      encode (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (ofNat ℕ n))) =
    encode (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) (ofNat ℕ n))
have succ : ∀ (n : ℕ),
  (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (n + 1) (encode a).succ fun (n : ℕ) ↦
      encode (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (ofNat ℕ n))) =
    encode (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) (ofNat ℕ (n + 1)))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
⊢ Primrec₂ Nat.pair
have simp : Nat.Primrec fun (n : ℕ) ↦ n + 1
Tactic: simp [Primrec₂, Primrec]
-- 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 : α → β → σ
⊢ Primrec (Function.uncurry f) ↔ Primrec₂ f
have rw : (Primrec (β := σ) fun (p : α × β) ↦ f p.1 p.2) ↔ Primrec₂ f
Tactic: rw [show Function.uncurry f = fun p : α × β => f p.1 p.2 from funext fun ⟨a, b⟩ => rfl]
-- 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 : α × β → σ
⊢ Primrec₂ (Function.curry f) ↔ Primrec f
have rw : Primrec (Function.uncurry (Function.curry f)) ↔ Primrec f
Tactic: rw [← uncurry, Function.uncurry_curry]
-- 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 : α × β → σ
rw : Primrec (Function.uncurry (Function.curry f)) ↔ Primrec f
⊢ Primrec₂ (Function.curry f) ↔ Primrec f
have rw₁ : Primrec f ↔ Primrec f
Tactic: rw [← uncurry, Function.uncurry_curry]
-- 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 : α → β → σ
a : Option α
b : Option β
⊢ Eq.{u_3 + 1} (α := Option σ)
    (Option.map (fun (p : α × β) ↦ f p.1 p.2) (a.bind fun (a : α) ↦ Option.map (Prod.mk a) b))
    (a.bind fun (a : α) ↦ Option.map (f a) b)
have none : Eq.{u_3 + 1} (α := Option σ)
  (Option.map (fun (p : α × β) ↦ f p.1 p.2) (Option.bind none fun (a : α) ↦ Option.map (Prod.mk a) b))
  (Option.bind none fun (a : α) ↦ Option.map (f a) b)
Tactic: cases a
Cleared hypotheses: a
-- 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 : α → β → σ
a : Option α
b : Option β
none :
  Eq.{u_3 + 1} (α := Option σ)
    (Option.map (fun (p : α × β) ↦ f p.1 p.2) (Option.bind Option.none fun (a : α) ↦ Option.map (Prod.mk a) b))
    (Option.bind Option.none fun (a : α) ↦ Option.map (f a) b)
⊢ Eq.{u_3 + 1} (α := Option σ)
    (Option.map (fun (p : α × β) ↦ f p.1 p.2) (a.bind fun (a : α) ↦ Option.map (Prod.mk a) b))
    (a.bind fun (a : α) ↦ Option.map (f a) b)
have some : ∀ (val : α),
  Eq.{u_3 + 1} (α := Option σ)
    (Option.map (fun (p : α × β) ↦ f p.1 p.2) ((some val).bind fun (a : α) ↦ Option.map (Prod.mk a) b))
    ((some val).bind fun (a : α) ↦ Option.map (f a) b)
Tactic: cases a
Cleared hypotheses: a
-- 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 : α → β → σ
b : Option β
⊢ Eq.{u_3 + 1} (α := Option σ)
    (Option.map (fun (p : α × β) ↦ f p.1 p.2) (Option.bind none fun (a : α) ↦ Option.map (Prod.mk a) b))
    (Option.bind none fun (a : α) ↦ Option.map (f a) b)
have none : Eq.{u_3 + 1} (α := Option σ)
  (Option.map (fun (p : α × β) ↦ f p.1 p.2) (Option.bind none fun (a : α) ↦ Option.map (Prod.mk a) none))
  (Option.bind none fun (a : α) ↦ Option.map (f a) none)
Tactic: cases b
Cleared hypotheses: b
-- 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 : α → β → σ
b : Option β
none :
  Eq.{u_3 + 1} (α := Option σ)
    (Option.map (fun (p : α × β) ↦ f p.1 p.2)
      (Option.bind Option.none fun (a : α) ↦ Option.map (Prod.mk a) Option.none))
    (Option.bind Option.none fun (a : α) ↦ Option.map (f a) Option.none)
⊢ Eq.{u_3 + 1} (α := Option σ)
    (Option.map (fun (p : α × β) ↦ f p.1 p.2) (Option.bind Option.none fun (a : α) ↦ Option.map (Prod.mk a) b))
    (Option.bind Option.none fun (a : α) ↦ Option.map (f a) b)
have none₁ : ∀ (val : β),
  Eq.{u_3 + 1} (α := Option σ)
    (Option.map (fun (p : α × β) ↦ f p.1 p.2) (Option.bind Option.none fun (a : α) ↦ Option.map (Prod.mk a) (some val)))
    (Option.bind Option.none fun (a : α) ↦ Option.map (f a) (some val))
Tactic: cases b
Cleared hypotheses: b
-- 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 : α → β → σ
b : Option β
val : α
⊢ Eq.{u_3 + 1} (α := Option σ)
    (Option.map (fun (p : α × β) ↦ f p.1 p.2) ((some val).bind fun (a : α) ↦ Option.map (Prod.mk a) b))
    ((some val).bind fun (a : α) ↦ Option.map (f a) b)
have some : Eq.{u_3 + 1} (α := Option σ)
  (Option.map (fun (p : α × β) ↦ f p.1 p.2) ((some val).bind fun (a : α) ↦ Option.map (Prod.mk a) none))
  ((some val).bind fun (a : α) ↦ Option.map (f a) none)
Tactic: cases b
Cleared hypotheses: b
-- 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 : α → β → σ
b : Option β
val : α
some :
  Eq.{u_3 + 1} (α := Option σ)
    (Option.map (fun (p : α × β) ↦ f p.1 p.2) ((Option.some val).bind fun (a : α) ↦ Option.map (Prod.mk a) none))
    ((Option.some val).bind fun (a : α) ↦ Option.map (f a) none)
⊢ Eq.{u_3 + 1} (α := Option σ)
    (Option.map (fun (p : α × β) ↦ f p.1 p.2) ((Option.some val).bind fun (a : α) ↦ Option.map (Prod.mk a) b))
    ((Option.some val).bind fun (a : α) ↦ Option.map (f a) b)
have some₁ : ∀ (val_1 : β),
  Eq.{u_3 + 1} (α := Option σ)
    (Option.map (fun (p : α × β) ↦ f p.1 p.2)
      ((Option.some val).bind fun (a : α) ↦ Option.map (Prod.mk a) (Option.some val_1)))
    ((Option.some val).bind fun (a : α) ↦ Option.map (f a) (Option.some val_1))
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → β → σ
⊢ Primrec₂ f ↔
    Nat.Primrec
      (Nat.unpaired fun (m n : ℕ) ↦
        encode.{u_3} (α := Option σ) (Option.bind (decode m) fun (a : α) ↦ Option.map (f a) (decode n)))
have this : ∀ (a : Option α) (b : Option β),
  Eq.{u_3 + 1} (α := Option σ)
    (Option.map (fun (p : α × β) ↦ f p.1 p.2) (a.bind fun (a : α) ↦ Option.map (Prod.mk a) b))
    (a.bind fun (a : α) ↦ Option.map (f a) b)
Tactic: have :
    ∀ (a : Option α) (b : Option β),
      Option.map (fun p : α × β => f p.1 p.2)
          (Option.bind a fun a : α => Option.map (Prod.mk a) b) =
        Option.bind a fun a => Option.map (f a) b := fun a b => by
          cases a <;> cases b <;> rfl
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
⊢ Eq (α := ℕ)
    (Nat.unpaired
      (fun (z n : ℕ) ↦
        Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) n 0 fun (y : ℕ) ↦
          Nat.unpaired
            (fun (z n : ℕ) ↦
              Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (encode (Option.map f (decode z)))
                (fun (y IH : ℕ) ↦
                  encode.{u_2} (α := Option β)
                    (Option.map (fun (p : Prod.{u_1, u_2} α (ℕ × β)) ↦ g p.1 p.2)
                      (decode
                        (Nat.pair (Nat.unpair (Nat.pair z (Nat.pair y IH))).1
                          (Nat.pair (Nat.unpair (Nat.unpair (Nat.pair z (Nat.pair y IH))).2).1
                            (Nat.unpair (Nat.unpair (Nat.pair z (Nat.pair y IH))).2).2.pred)))))
                n)
            (Nat.pair (Nat.unpair (Nat.pair z y)).2 (Nat.unpair (Nat.unpair (Nat.pair z y)).1).2))
      (Nat.pair (id n) (encode.{u_1} (α := Option α) (decode (Nat.unpair n).1))))
    (Nat.unpaired
      (fun (m n : ℕ) ↦
        encode.{u_2} (α := Option β)
          (Option.bind (decode m) fun (a : α) ↦
            Option.map
              (fun (n : ℕ) ↦
                Nat.rec (motive := fun (x : ℕ) ↦ β) (f a) (fun (n : ℕ) (IH : (fun (x : ℕ) ↦ β) n) ↦ g a (n, IH)) n)
              (decode n)))
      n)
have simp : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
    (fun (n_1 n_ih : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (encode (Option.map f (decode n_1)))
        (fun (y IH : ℕ) ↦
          encode.{u_2} (α := Option β)
            (Option.map (fun (p : Prod.{u_1, u_2} α (ℕ × β)) ↦ g p.1 p.2)
              (Option.bind (decode n_1) fun (a : α) ↦ Option.map (Prod.mk a ∘ Prod.mk y) (decode IH.pred))))
        (Nat.unpair n).2)
    (encode.{u_1} (α := Option α) (decode (Nat.unpair n).1)) =
  encode.{u_2} (α := Option β)
    (Option.bind (decode (Nat.unpair n).1) fun (a : α) ↦
      some (Nat.rec (motive := fun (x : ℕ) ↦ β) (f a) (fun (n : ℕ) (IH : β) ↦ g a (n, IH)) (Nat.unpair n).2))
Tactic: simp only [Nat.unpaired, id_eq, Nat.unpair_pair, decode_prod_val, decode_nat,
        Option.bind_some, Option.map_map, Option.map_some]
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
      (fun (n_1 n_ih : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (encode (Option.map f (decode n_1)))
          (fun (y IH : ℕ) ↦
            encode.{u_2} (α := Option β)
              (Option.map (fun (p : Prod.{u_1, u_2} α (ℕ × β)) ↦ g p.1 p.2)
                (Option.bind (decode n_1) fun (a : α) ↦ Option.map (Prod.mk a ∘ Prod.mk y) (decode IH.pred))))
          (Nat.unpair n).2)
      (encode.{u_1} (α := Option α) (decode (Nat.unpair n).1)) =
    encode.{u_2} (α := Option β)
      (Option.bind (decode (Nat.unpair n).1) fun (a : α) ↦
        some (Nat.rec (motive := fun (x : ℕ) ↦ β) (f a) (fun (n : ℕ) (IH : β) ↦ g a (n, IH)) (Nat.unpair n).2))
have none : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
    (fun (n_1 n_ih : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (encode (Option.map f (decode n_1)))
        (fun (y IH : ℕ) ↦
          encode.{u_2} (α := Option β)
            (Option.map (fun (p : Prod.{u_1, u_2} α (ℕ × β)) ↦ g p.1 p.2)
              (Option.bind (decode n_1) fun (a : α) ↦ Option.map (Prod.mk a ∘ Prod.mk y) (decode IH.pred))))
        (Nat.unpair n).2)
    (encode.{u_1} (α := Option α) none) =
  encode.{u_2} (α := Option β)
    (Option.bind none fun (a : α) ↦
      some (Nat.rec (motive := fun (x : ℕ) ↦ β) (f a) (fun (n : ℕ) (IH : β) ↦ g a (n, IH)) (Nat.unpair n).2))
Tactic: rcases @decode α _ n.unpair.1 with - | a
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
none :
  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
      (fun (n_1 n_ih : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (encode (Option.map f (decode n_1)))
          (fun (y IH : ℕ) ↦
            encode.{u_2} (α := Option β)
              (Option.map (fun (p : Prod.{u_1, u_2} α (ℕ × β)) ↦ g p.1 p.2)
                (Option.bind (decode n_1) fun (a : α) ↦ Option.map (Prod.mk a ∘ Prod.mk y) (decode IH.pred))))
          (Nat.unpair n).2)
      (encode.{u_1} (α := Option α) Option.none) =
    encode.{u_2} (α := Option β)
      (Option.bind Option.none fun (a : α) ↦
        some (Nat.rec (motive := fun (x : ℕ) ↦ β) (f a) (fun (n : ℕ) (IH : β) ↦ g a (n, IH)) (Nat.unpair n).2))
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
      (fun (n_1 n_ih : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (encode (Option.map f (decode n_1)))
          (fun (y IH : ℕ) ↦
            encode.{u_2} (α := Option β)
              (Option.map (fun (p : Prod.{u_1, u_2} α (ℕ × β)) ↦ g p.1 p.2)
                (Option.bind (decode n_1) fun (a : α) ↦ Option.map (Prod.mk a ∘ Prod.mk y) (decode IH.pred))))
          (Nat.unpair n).2)
      (encode.{u_1} (α := Option α) (decode (Nat.unpair n).1)) =
    encode.{u_2} (α := Option β)
      (Option.bind (decode (Nat.unpair n).1) fun (a : α) ↦
        some (Nat.rec (motive := fun (x : ℕ) ↦ β) (f a) (fun (n : ℕ) (IH : β) ↦ g a (n, IH)) (Nat.unpair n).2))
have some : ∀ (a : α),
  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
      (fun (n_1 n_ih : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (encode (Option.map f (decode n_1)))
          (fun (y IH : ℕ) ↦
            encode.{u_2} (α := Option β)
              (Option.map (fun (p : Prod.{u_1, u_2} α (ℕ × β)) ↦ g p.1 p.2)
                (Option.bind (decode n_1) fun (a : α) ↦ Option.map (Prod.mk a ∘ Prod.mk y) (decode IH.pred))))
          (Nat.unpair n).2)
      (encode (some a)) =
    encode.{u_2} (α := Option β)
      ((some a).bind fun (a : α) ↦
        some (Nat.rec (motive := fun (x : ℕ) ↦ β) (f a) (fun (n : ℕ) (IH : β) ↦ g a (n, IH)) (Nat.unpair n).2))
Tactic: rcases @decode α _ n.unpair.1 with - | a
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
a : α
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
      (fun (n_1 n_ih : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (encode (Option.map f (decode n_1)))
          (fun (y IH : ℕ) ↦
            encode.{u_2} (α := Option β)
              (Option.map (fun (p : Prod.{u_1, u_2} α (ℕ × β)) ↦ g p.1 p.2)
                (Option.bind (decode n_1) fun (a : α) ↦ Option.map (Prod.mk a ∘ Prod.mk y) (decode IH.pred))))
          (Nat.unpair n).2)
      (encode (some a)) =
    encode.{u_2} (α := Option β)
      ((some a).bind fun (a : α) ↦
        some (Nat.rec (motive := fun (x : ℕ) ↦ β) (f a) (fun (n : ℕ) (IH : β) ↦ g a (n, IH)) (Nat.unpair n).2))
have some : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (encode (f a) + 1)
    (fun (y IH : ℕ) ↦
      encode.{u_2} (α := Option β)
        (Option.map (α := β) ((fun (p : Prod.{u_1, u_2} α (ℕ × β)) ↦ g p.1 p.2) ∘ Prod.mk a ∘ Prod.mk y)
          (decode (IH - 1))))
    (Nat.unpair n).2 =
  encode.{u_2} (α := β)
      (Nat.rec (motive := fun (x : ℕ) ↦ β) (f a) (fun (n : ℕ) (IH : β) ↦ g a (n, IH)) (Nat.unpair n).2 : β) +
    1
Tactic: simp only [Nat.pred_eq_sub_one, encode_some, Nat.succ_eq_add_one, encodek, Option.map_some,
        Option.bind_some, Option.map_map]
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
a : α
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (encode (f a) + 1)
      (fun (y IH : ℕ) ↦
        encode.{u_2} (α := Option β)
          (Option.map (α := β) ((fun (p : Prod.{u_1, u_2} α (ℕ × β)) ↦ g p.1 p.2) ∘ Prod.mk a ∘ Prod.mk y)
            (decode (IH - 1))))
      (Nat.unpair n).2 =
    encode.{u_2} (α := β)
        (Nat.rec (motive := fun (x : ℕ) ↦ β) (f a) (fun (n : ℕ) (IH : β) ↦ g a (n, IH)) (Nat.unpair n).2 : β) +
      1
have some : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (encode (f a) + 1)
    (fun (y IH : ℕ) ↦
      encode.{u_2} (α := Option β)
        (Option.map (α := β) ((fun (p : Prod.{u_1, u_2} α (ℕ × β)) ↦ g p.1 p.2) ∘ Prod.mk a ∘ Prod.mk y)
          (decode (IH - 1))))
    0 =
  encode.{u_2} (α := β) (Nat.rec (motive := fun (x : ℕ) ↦ β) (f a) (fun (n : ℕ) (IH : β) ↦ g a (n, IH)) 0 : β) + 1
Tactic: induction n.unpair.2