awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.Primrec.Basic
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 α) 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:
simp
-- Module: Mathlib.Computability.Primrec.Basic
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 β) (decode (Nat.unpair n).2)) =
    encode (Option.map (Function.const β val) (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 (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)))

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
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)
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))
⊢ 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:
cases @decode β _ n.unpair.2

Premises used: Nat.unpair, Encodable.decode, Prod.snd
-- Module: Mathlib.Computability.Primrec.Basic
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 β) none) =
    encode (Option.map (Function.const β val) none)

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
val : α
val_1 : β
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n n_ih : ℕ) ↦ encode val + 1) (encode (some val_1)) =
    encode (Option.map (Function.const β val) (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.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)))
⊢ 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))

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.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)))
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 (Option.some val)) =
      encode.{u_3} (α := Option β)
        (Option.map (α := α × β) Prod.snd
          ((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.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:
cases @decode α _ n.unpair.1

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

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
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
some₁ :
  ∀ (val : β),
    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n n_ih : ℕ) ↦ n + 1) (encode (Option.some val)) =
      encode (Option.some 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)

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

Premises used: Nat.unpair, Encodable.decode, Prod.snd
-- Module: Mathlib.Computability.Primrec.Basic
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 β) none) =
    encode.{u_3} (α := Option β) none

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
val : α
val_1 : β
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (n n_ih : ℕ) ↦ n + 1) (encode (some val_1)) = encode (some val_1)

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

Tactic:
cases @decode α _ n

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

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

Premises used: Encodable.encodek
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
n : ℕ
⊢ ((Nat.unpair n).1, (Nat.unpair n).2) = Nat.unpair n

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

Tactic:
cases n
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
a : α
l : List α
⊢ (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:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
a : α
l : List α
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:
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 : α → β → σ
hf : Primrec (β := σ) fun (p : α × β) ↦ f p.1 p.2
⊢ Primrec₂ f

Tactic:
hf

Premises used: Primrec₂
-- 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 : α → β → σ
hg : Primrec₂ f
H h : ∀ (a : α) (b : β), f a b = g a b
⊢ f = g

Tactic:
funext a b
-- 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 : α → β → σ
hg : Primrec₂ f
H : ∀ (a : α) (b : β), f a b = g a b
a : α
b : β
⊢ f a b = g a b

Tactic:
apply H
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
x : σ
⊢ Primrec₂.{u_1, u_2, u_3} (σ := σ) fun (x_1 : α) (x_2 : β) ↦ x

Tactic:
Primrec.const _

Premises used: Primrec.const, Primrec₂
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
⊢ Primrec₂ (α := α) (β := β) Prod.mk

Tactic:
Primrec.pair .fst .snd

Premises used: Primrec.snd, Primrec.fst, Primrec.pair, Primrec₂
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
⊢ Primrec₂ (σ := α) fun (a : α) (x : β) ↦ a

Tactic:
.fst

Premises used: Primrec.fst, Primrec₂
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
⊢ Primrec₂ (σ := β) fun (x : α) (b : β) ↦ b

Tactic:
.snd

Premises used: Primrec.snd, Primrec₂
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
simp : Nat.Primrec fun (n : ℕ) ↦ n + 1
⊢ Primrec₂ Nat.pair

Tactic:
simp [Primrec₂, Primrec]

Premises used: Primrec, Primrec₂
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
⊢ Nat.Primrec fun (n : ℕ) ↦ n + 1

Tactic:
constructor
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
f : ℕ → ℕ → α
h : Primrec (Nat.unpaired f)
⊢ Primrec₂ f

Tactic:
simpa using h.comp natPair

Premises used: Primrec.comp, Primrec₂.natPair
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
f : ℕ → ℕ → ℕ
⊢ Nat.Primrec (Nat.unpaired f) ↔ Primrec₂ f

Tactic:
Primrec.nat_iff.symm.trans unpaired

Premises used: Primrec₂.unpaired, Primrec.nat_iff, Iff.trans, Iff.symm
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → β → σ
⊢ (Primrec₂ (σ := ℕ) fun (a : α) (b : β) ↦ encode (f a b)) ↔ Primrec₂ f

Tactic:
Primrec.encode_iff

Premises used: Primrec.encode_iff, Primrec₂
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → β → σ
⊢ (Primrec₂.{u_1, u_2, u_3} (σ := Option σ) fun (a : α) (b : β) ↦ some (f a b)) ↔ Primrec₂ f

Tactic:
Primrec.option_some_iff

Premises used: Primrec.option_some_iff, Primrec₂
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_4
β : Type u_5
σ : Type u_6
inst : Denumerable α
inst_1 : Denumerable β
inst_2 : Primcodable σ
f : α → β → σ
⊢ (Primrec.{0, u_6} (β := σ) fun (n : ℕ) ↦ f (ofNat (α × β) n).1 (ofNat (α × β) n).2) ↔
    Primrec.{0, u_6} (β := σ) (Nat.unpaired fun (m n : ℕ) ↦ f (ofNat α m) (ofNat β 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 : α → β → σ
rw : (Primrec (β := σ) fun (p : α × β) ↦ f p.1 p.2) ↔ Primrec₂ f
⊢ Primrec (Function.uncurry f) ↔ Primrec₂ f

Tactic:
rw [show Function.uncurry f = fun p : α × β => f p.1 p.2 from funext fun ⟨a, b⟩ => rfl]

Premises used: Prod.fst, funext, _private.0.Primrec₂.uncurry.match_1, Function.uncurry, Eq, Prod.snd, rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → β → σ
⊢ (Primrec (β := σ) fun (p : α × β) ↦ f p.1 p.2) ↔ Primrec₂ f

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
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
rw₁ rw₂ : Primrec f ↔ Primrec f
⊢ Primrec₂ (Function.curry f) ↔ Primrec f

Tactic:
rw [← uncurry, Function.uncurry_curry]

Premises used: Function.uncurry_curry, Primrec₂.uncurry
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
inst_3 : Primcodable σ
f : γ → σ
g : α → β → γ
hf : Primrec f
hg : Primrec₂ g
⊢ Primrec₂.{u_1, u_2, u_5} (σ := σ) fun (a : α) (b : β) ↦ f (g a b)

Tactic:
hf.comp hg

Premises used: Primrec.comp, Primrec₂
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
inst_3 : Primcodable σ
f : β → γ → σ
g : α → β
h : α → γ
hf : Primrec₂ f
hg : Primrec g
hh : Primrec h
⊢ Primrec.{u_1, u_5} (β := σ) fun (a : α) ↦ f (g a) (h a)

Tactic:
Primrec.comp hf (hg.pair hh)

Premises used: Primrec.pair, Primrec.comp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
inst_3 : Primcodable δ
inst_4 : Primcodable σ
f : γ → δ → σ
g : α → β → γ
h : α → β → δ
hf : Primrec₂ f
hg : Primrec₂ g
hh : Primrec₂ h
⊢ Primrec₂.{u_1, u_2, u_5} (σ := σ) fun (a : α) (b : β) ↦ f (g a b) (h a b)

Tactic:
hf.comp hg hh

Premises used: Primrec₂.comp, Primrec₂
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
hp : PrimrecPred p
⊢ Primrec (β := Bool) fun (a : α) ↦ decide (p a)

Tactic:
hp.choose_spec

Premises used: Exists.choose_spec
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
hp : PrimrecPred p
⊢ Primrec (β := Bool) fun (a : α) ↦ decide (p a)

Tactic:
convert! hp.choose_spec

Premises used: Exists.choose_spec
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
hp : Primrec (β := Bool) fun (a : α) ↦ decide (p a)
⊢ PrimrecPred p

Tactic:
⟨inferInstance, hp⟩

Premises used: inferInstance, Exists.intro, PrimrecPred
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
R : α → β → Prop
inst_2 : DecidableRel R
hR : PrimrecRel R
⊢ Primrec₂ (σ := Bool) fun (a : α) (b : β) ↦ decide (R a b)

Tactic:
PrimrecPred.decide hR

Premises used: PrimrecPred.decide, Primrec₂
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
R : α → β → Prop
inst_2 : DecidableRel R
hp : Primrec₂ (σ := Bool) fun (a : α) (b : β) ↦ decide (R a b)
⊢ PrimrecRel R

Tactic:
Primrec.primrecPred hp

Premises used: PrimrecRel, Primrec.primrecPred
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
R : β → γ → Prop
f : α → β
g : α → γ
hR : PrimrecRel R
hf : Primrec f
hg : Primrec g
⊢ PrimrecPred fun (a : α) ↦ R (f a) (g a)

Tactic:
PrimrecPred.comp hR (hf.pair hg)

Premises used: PrimrecPred.comp, Primrec.pair
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
inst_3 : Primcodable δ
R : γ → δ → Prop
f : α → β → γ
g : α → β → δ
⊢ PrimrecRel R → Primrec₂ f → Primrec₂ g → PrimrecRel fun (a : α) (b : β) ↦ R (f a b) (g a b)

Tactic:
PrimrecRel.comp

Premises used: PrimrecRel, PrimrecRel.comp, Primrec₂
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
p q : α → Prop
hp : PrimrecPred p
H : ∀ (a : α), p a ↔ q a
⊢ PrimrecPred q

Tactic:
funext (fun a => propext (H a)) ▸ hp

Premises used: Eq.rec, funext, propext
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
r s : α → β → Prop
hr : PrimrecRel r
H : ∀ (a : α) (b : β), r a b ↔ s a b
⊢ PrimrecRel s

Tactic:
funext₂ (fun a b => propext (H a b)) ▸ hr

Premises used: Eq.rec, funext₂, propext
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → β → σ
h : Primrec₂ f
⊢ Primrec₂ (swap (φ := fun (a : α) (a_1 : β) ↦ σ) f)

Tactic:
h.comp₂ Primrec₂.right Primrec₂.left

Premises used: Primrec₂.left, Primrec₂.right, Primrec₂.comp₂
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
r : α → β → Prop
h : PrimrecRel r
⊢ PrimrecRel (swap (φ := fun (a : α) (a_1 : β) ↦ Prop) r)

Tactic:
h.comp₂ Primrec₂.right Primrec₂.left

Premises used: Primrec₂.left, Primrec₂.right, PrimrecRel.comp₂
-- Module: Mathlib.Computability.Primrec.Basic
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)
some :
  ∀ (val : α),
    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)
⊢ 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:
cases a
-- Module: Mathlib.Computability.Primrec.Basic
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)
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))
⊢ 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)

Tactic:
cases b