awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
h : Primcodable α
n : ℕ
succ :
  (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))
⊢ (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:
rw [decode_option_succ]

Premises used: Encodable.decode_option_succ
-- Module: Mathlib.Computability.Primrec.Basic
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)
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))
⊢ (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))

Tactic:
cases H : @decode α _ n

Premises used: Encodable.decode
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
h : Primcodable α
n : ℕ
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:
simp [H]
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
h : Primcodable α
n : ℕ
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:
simp [H]
-- Module: Mathlib.Computability.Primrec.Basic
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)
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))
⊢ (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)

Tactic:
cases n with
      | zero => rfl
      | succ n =>
        rw [decode_option_succ]
        cases H : @decode α _ n <;> simp [H]

Premises used: Encodable.decode_option_succ, Nat.Primrec.zero, Encodable.decode
-- Module: Mathlib.Computability.Primrec.Basic
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
h : 2 ≤ n + 2
⊢ (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))

Tactic:
rw [decode_ge_two]

Premises used: Encodable.decode_ge_two
-- Module: Mathlib.Computability.Primrec.Basic
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) none

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
n_1 n : ℕ
⊢ 2 ≤ n + 2

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
none : encode.{u_1} (α := Option α) Option.none = encode (Option.map.{u_1, 0} (α := α) encode Option.none)
some : ∀ (val : α), encode (Option.some val) = encode (Option.map encode (Option.some val))
⊢ encode.{u_1} (α := Option α) (decode n) = encode (Option.map.{u_1, 0} (α := α) encode (decode n))

Tactic:
cases @decode α _ n

Premises used: Encodable.decode
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
⊢ encode.{u_1} (α := Option α) none = encode (Option.map.{u_1, 0} (α := α) encode none)

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
val : α
⊢ encode (some val) = encode (Option.map encode (some val))

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
⊢ Primrec.{0, u_1} (β := Option α) decode

Tactic:
Nat.Primrec.succ.comp (Primcodable.prim α)

Premises used: Nat.Primrec.succ, Nat.Primrec.comp, Primrec, Primcodable.prim
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_4
β : Type u_5
inst : Denumerable α
inst_1 : Primcodable β
f : α → β
h : Primrec f
n : ℕ
⊢ (encode (Option.map f (decode n))).pred = encode (f (ofNat α n))

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_4
β : Type u_5
inst : Denumerable α
inst_1 : Primcodable β
f : α → β
h : Nat.Primrec fun (n : ℕ) ↦ encode (f (ofNat α n))
n : ℕ
⊢ (encode (f (ofNat α n))).succ = encode (Option.map f (decode n))

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
f : ℕ → ℕ
⊢ Primrec f ↔ Nat.Primrec f

Tactic:
dom_denumerable

Premises used: Primrec.dom_denumerable, Denumerable.ofNat
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
⊢ Primrec (β := ℕ) fun (n : ℕ) ↦ encode.{u_1} (α := Option α) (decode n)

Tactic:
nat_iff.2 (Primcodable.prim _)

Premises used: Iff.mpr, Primrec.nat_iff, Primcodable.prim
-- Module: Mathlib.Computability.Primrec.Basic
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 Option.some Option.none)
some :
  ∀ (val : α),
    (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode (Option.some val)) 0 fun (n : ℕ) ↦ n.succ.succ) =
      encode (Option.map Option.some (Option.some val))
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_1} (α := Option α) (decode n)) 0 fun (n : ℕ) ↦ n.succ.succ) =
    encode.{u_1} (α := Option (Option α)) (Option.map Option.some (decode n))

Tactic:
cases @decode α _ n

Premises used: Encodable.decode
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
⊢ (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:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
val : α
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode (some val)) 0 fun (n : ℕ) ↦ n.succ.succ) =
    encode (Option.map some (some val))

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
f g : α → σ
hf : Primrec f
H : ∀ (n : α), f n = g n
⊢ Primrec g

Tactic:
(funext H : f = g) ▸ hf

Premises used: Eq.rec, funext
-- Module: Mathlib.Computability.Primrec.Basic
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)
some :
  ∀ (val : α),
    (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode (Option.some val)) 0 fun (x_1 : ℕ) ↦ (encode x).succ) =
      encode.{u_3} (α := Option σ) (Option.map (fun (x_1 : α) ↦ x) (Option.some val))
⊢ (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))

Tactic:
cases @decode α _ n

Premises used: Encodable.decode
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
x : σ
n : ℕ
⊢ (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:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
x : σ
n : ℕ
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:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
⊢ ∀ (n : ℕ), encode.{u_1} (α := Option α) (decode n) = encode.{u_1} (α := Option α) (Option.map id (decode n))

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
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)
some :
  ∀ (val : α),
    (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode (Option.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)) (Option.some val))
⊢ (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))

Tactic:
cases @decode α _ n

Premises used: Encodable.decode
-- Module: Mathlib.Computability.Primrec.Basic
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 α) 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:
simp [encodek]

Premises used: Encodable.encodek
-- Module: Mathlib.Computability.Primrec.Basic
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 : ℕ
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:
simp [encodek]

Premises used: Encodable.encodek
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
⊢ Primrec Nat.succ

Tactic:
nat_iff.2 Nat.Primrec.succ

Premises used: Iff.mpr, Nat.Primrec.succ, Primrec.nat_iff
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
⊢ Primrec Nat.pred

Tactic:
nat_iff.2 Nat.Primrec.pred

Premises used: Iff.mpr, Nat.Primrec.pred, Primrec.nat_iff
-- Module: Mathlib.Computability.Primrec.Basic
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)
some :
  ∀ (val : α),
    encode (α := Option ℕ) (Option.map (fun (a : α) ↦ encode (f a)) (Option.some val)) =
      encode (Option.map f (Option.some val))
⊢ encode (α := Option ℕ) (Option.map (fun (a : α) ↦ encode (f a)) (decode n)) = encode (Option.map f (decode n))

Tactic:
cases @decode α _ n

Premises used: Encodable.decode
-- Module: Mathlib.Computability.Primrec.Basic
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)) none) = encode (Option.map f none)

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
f : α → σ
h : Primrec (β := ℕ) fun (a : α) ↦ encode (f a)
n : ℕ
val : α
⊢ encode (α := Option ℕ) (Option.map (fun (a : α) ↦ encode (f a)) (some val)) = encode (Option.map f (some val))

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_4
β : Type u_5
inst : Denumerable α
inst_1 : Primcodable β
f : α → β
⊢ Primrec f ↔ Primrec.{0, u_5} (β := β) fun (n : ℕ) ↦ f (ofNat α n)

Tactic:
dom_denumerable.trans <| nat_iff.symm.trans encode_iff

Premises used: Primrec.encode_iff, Primrec.nat_iff, Primrec.dom_denumerable, Iff.trans, Iff.symm
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_4
inst : Denumerable α
⊢ Primrec (ofNat α)

Tactic:
ofNat_iff.1 Primrec.id

Premises used: Iff.mp, Primrec.ofNat_iff, Primrec.id, Denumerable.ofNat
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
f : α → σ
⊢ (Primrec.{u_1, u_3} (β := Option σ) fun (a : α) ↦ some (f a)) ↔ Primrec f

Tactic:
⟨fun h => encode_iff.1 <| pred.comp <| encode_iff.2 h, option_some.comp⟩

Premises used: Iff.mpr, Primrec.encode_iff, Primrec.option_some, Primrec.comp, Iff.intro, Iff.mp, Primrec.pred
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
β : Type u_4
e : β ≃ α
⊢ Primrec.{u_4, u_1} (α := β) (β := α) (⇑e : (a : β) → α)

Tactic:
letI : Primcodable β := Primcodable.ofEquiv α e
  encode_iff.1 Primrec.encode

Premises used: Primrec.encode_iff, Iff.mp, Primrec.encode
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
β : Type u_4
e : β ≃ α
this : Primcodable β := Primcodable.ofEquiv α e
⊢ Primrec (β := ℕ) fun (a : α) ↦ encode.{u_1} (α := α) ((e : (a : β) → α) ((e.symm : (a : α) → β) a : β) : α)

Tactic:
simp [Primrec.encode]

Premises used: Primrec.encode
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
β : Type u_4
e : β ≃ α
f : σ → β
this : Primcodable β := Primcodable.ofEquiv α e
h : Primrec.{u_3, u_1} (β := α) fun (a : σ) ↦ (e : (a : β) → α) (f a)
a : σ
⊢ (e.symm : (a : α) → β) ((e : (a : β) → α) (f a) : α) = f a

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
β : Type u_4
e : β ≃ α
f : σ → α
this : Primcodable β := Primcodable.ofEquiv α e
h : Primrec.{u_3, u_4} (β := β) fun (a : σ) ↦ (e.symm : (a : α) → β) (f a)
a : σ
⊢ (e : (a : β) → α) ((e.symm : (a : α) → β) (f a) : β) = f a

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
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))
⊢ 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)

Tactic:
simp only [Nat.unpaired, Nat.unpair_pair, decode_prod_val]

Premises used: Nat.unpaired, Encodable.decode_prod_val, Nat.unpair_pair
-- Module: Mathlib.Computability.Primrec.Basic
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))
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 (Option.some val)) =
      encode (α := Option (α × β))
        ((Option.some val).bind 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))

Tactic:
cases @decode α _ n.unpair.1

Premises used: Nat.unpair, Prod.fst, Encodable.decode
-- Module: Mathlib.Computability.Primrec.Basic
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 α) none) =
    encode (α := Option (α × β)) (Option.bind none fun (a : α) ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2))

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
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)
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))
⊢ 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))

Tactic:
cases @decode β _ n.unpair.2

Premises used: Nat.unpair, Encodable.decode, Prod.snd
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
val : α
⊢ 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:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
val : α
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 (some val_1)))
      (encode (some val)) =
    encode (α := Option (α × β)) ((some val).bind fun (a : α) ↦ Option.map (Prod.mk a) (some val_1))

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
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)))
⊢ 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))

Tactic:
simp only [Nat.unpaired, Nat.unpair_pair, decode_prod_val]

Premises used: Nat.unpaired, Encodable.decode_prod_val, Nat.unpair_pair
-- Module: Mathlib.Computability.Primrec.Basic
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)))
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 (Option.some val)) =
      encode.{u_2} (α := Option α)
        (Option.map (α := α × β) Prod.fst
          ((Option.some val).bind 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)))

Tactic:
cases @decode α _ n.unpair.1

Premises used: Nat.unpair, Prod.fst, Encodable.decode