awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 β
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)
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))
⊢ 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)

Tactic:
cases 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 : α → β → σ
⊢ 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:
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 : α → β → σ
val : β
⊢ Eq.{u_3 + 1} (α := Option σ)
    (Option.map (fun (p : α × β) ↦ f p.1 p.2) (Option.bind none fun (a : α) ↦ Option.map (Prod.mk a) (some val)))
    (Option.bind none fun (a : α) ↦ Option.map (f a) (some val))

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 : α → β → σ
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) none))
    ((some val).bind fun (a : α) ↦ Option.map (f a) none)

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 : α → β → σ
val : α
val_1 : β
⊢ Eq.{u_3 + 1} (α := Option σ)
    (Option.map (fun (p : α × β) ↦ f p.1 p.2) ((some val).bind fun (a : α) ↦ Option.map (Prod.mk a) (some val_1)))
    ((some val).bind fun (a : α) ↦ Option.map (f a) (some val_1))

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 : α → β → σ
⊢ ∀ (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
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → β → σ
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)
⊢ 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)))

Tactic:
simp [Primrec₂, Primrec, this]

Premises used: Primrec, 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₂ f ↔
    Primrec₂.{0, 0, u_3} (σ := Option σ) fun (m n : ℕ) ↦
      Option.bind (decode m) fun (a : α) ↦ Option.map (f a) (decode n)

Tactic:
nat_iff.trans <| unpaired'.trans encode_iff

Premises used: Primrec₂.encode_iff, Primrec₂.unpaired', Iff.trans, Primrec₂.nat_iff
-- 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 f
⊢ Primrec₂.{u_1, u_2, u_3} (σ := σ) fun (a : α) (b : β) ↦ f (a, b)

Tactic:
hf

Premises used: Primrec₂
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
p : α × β → Prop
hp : PrimrecPred p
⊢ PrimrecRel fun (a : α) (b : β) ↦ p (a, b)

Tactic:
hp

Premises used: PrimrecRel
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
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))
⊢ 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)

Tactic:
simp only [Nat.unpaired, id_eq, Nat.unpair_pair, decode_prod_val, decode_nat,
        Option.bind_some, Option.map_map, Option.map_some]

Premises used: Option.bind_some, Option.map_map, Option.map_some, Nat.unpaired, Encodable.decode_prod_val, Nat.unpair_pair, Encodable.decode_nat, id_eq
-- Module: Mathlib.Computability.Primrec.Basic
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 : α) ↦
        Option.some (Nat.rec (motive := fun (x : ℕ) ↦ β) (f a) (fun (n : ℕ) (IH : β) ↦ g a (n, IH)) (Nat.unpair n).2))
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 (Option.some a)) =
      encode.{u_2} (α := Option β)
        ((Option.some a).bind fun (a : α) ↦
          Option.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 : α) ↦
        Option.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

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 β
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 α) 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:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
a : α
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
⊢ 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 (Option.some a)) =
    encode.{u_2} (α := Option β)
      ((Option.some a).bind fun (a : α) ↦
        Option.some (Nat.rec (motive := fun (x : ℕ) ↦ β) (f a) (fun (n : ℕ) (IH : β) ↦ g a (n, IH)) (Nat.unpair n).2))

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]

Premises used: Nat.succ_eq_add_one, Option.bind_some, Option.map_map, Nat.pred_eq_sub_one, Encodable.encodek, Option.map_some, Encodable.encode_some
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
a : α
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
some₁ :
  ∀ (n : ℕ),
    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))))
          n =
        encode.{u_2} (α := β) (Nat.rec (motive := fun (x : ℕ) ↦ β) (f a) (fun (n : ℕ) (IH : β) ↦ g a (n, IH)) n : β) +
          1 →
      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))))
          (n + 1) =
        encode.{u_2} (α := β)
            (Nat.rec (motive := fun (x : ℕ) ↦ β) (f a) (fun (n : ℕ) (IH : β) ↦ g a (n, IH)) (n + 1) : β) +
          1
⊢ 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:
induction n.unpair.2

Premises used: Nat.unpair, Prod.snd
-- Module: Mathlib.Computability.Primrec.Basic
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))))
      0 =
    encode.{u_2} (α := β) (Nat.rec (motive := fun (x : ℕ) ↦ β) (f a) (fun (n : ℕ) (IH : β) ↦ g a (n, IH)) 0 : β) + 1

Tactic:
simp [*, encodek]

Premises used: Encodable.encodek
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
a : α
n_1 : ℕ
h :
  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))))
      n_1 =
    encode.{u_2} (α := β) (Nat.rec (motive := fun (x : ℕ) ↦ β) (f a) (fun (n : ℕ) (IH : β) ↦ g a (n, IH)) n_1 : β) + 1
⊢ 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))))
      (n_1 + 1) =
    encode.{u_2} (α := β)
        (Nat.rec (motive := fun (x : ℕ) ↦ β) (f a) (fun (n : ℕ) (IH : β) ↦ g a (n, IH)) (n_1 + 1) : β) +
      1

Tactic:
simp [*, encodek]

Premises used: Encodable.encodek
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → ℕ
g : α → β
h : α → ℕ × β → β
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
⊢ Primrec.{u_1, u_2} (β := β) fun (a : α) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ β) (g a) (fun (n : ℕ) (IH : (fun (x : ℕ) ↦ β) n) ↦ h a (n, IH)) (f a)

Tactic:
(nat_rec hg hh).comp .id hf

Premises used: Primrec.nat_rec, Primrec₂.comp, Primrec.id
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
f : ℕ → α → α
a : α
hf : Primrec₂ f
⊢ Primrec.{0, u_1} (β := α) fun (t : ℕ) ↦ Nat.rec (motive := fun (x : ℕ) ↦ α) a f t

Tactic:
nat_rec' .id (const a) <| comp₂ hf Primrec₂.right

Premises used: Primrec.comp₂, Primrec₂.right, Primrec.const, Primrec.nat_rec', Primrec.id
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → β
g : α → ℕ → β
hf : Primrec f
hg : Primrec₂ g
⊢ Primrec₂.{u_1, 0, u_2} (σ := β) fun (a : α) (n : ℕ) ↦ Nat.casesOn (motive := fun (x : ℕ) ↦ β) n (f a) (g a)

Tactic:
nat_rec hf <| hg.comp₂ Primrec₂.left <| comp₂ fst Primrec₂.right

Premises used: Primrec₂.left, Primrec.comp₂, Primrec.fst, Primrec₂.right, Primrec₂.comp₂, Primrec.nat_rec
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → ℕ
g : α → β
h : α → ℕ → β
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
⊢ Primrec.{u_1, u_2} (β := β) fun (a : α) ↦ Nat.casesOn (motive := fun (x : ℕ) ↦ β) (f a) (g a) (h a)

Tactic:
(nat_casesOn' hg hh).comp .id hf

Premises used: Primrec.nat_casesOn', Primrec₂.comp, Primrec.id
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
f : ℕ → α
a : α
hf : Primrec f
⊢ Primrec.{0, u_1} (β := α) fun (n : ℕ) ↦ Nat.casesOn (motive := fun (x : ℕ) ↦ α) n a f

Tactic:
nat_casesOn .id (const a) (comp₂ hf .right)

Premises used: Primrec.comp₂, Primrec₂.right, Primrec.const, Primrec.id, Primrec.nat_casesOn
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → ℕ
g : α → β
h : α → β → β
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
a : α
zero :
  Nat.rec (motive := fun (x : ℕ) ↦ β) (g a) (fun (n : ℕ) (IH : (fun (x : ℕ) ↦ β) n) ↦ h a (n, IH).2) 0 = (h a)^[0] (g a)
succ :
  ∀ (n : ℕ),
    Nat.rec (motive := fun (x : ℕ) ↦ β) (g a) (fun (n : ℕ) (IH : (fun (x : ℕ) ↦ β) n) ↦ h a (n, IH).2) n =
        (h a)^[n] (g a) →
      Nat.rec (motive := fun (x : ℕ) ↦ β) (g a) (fun (n : ℕ) (IH : (fun (x : ℕ) ↦ β) n) ↦ h a (n, IH).2) (n + 1) =
        (h a)^[n + 1] (g a)
⊢ Nat.rec (motive := fun (x : ℕ) ↦ β) (g a) (fun (n : ℕ) (IH : (fun (x : ℕ) ↦ β) n) ↦ h a (n, IH).2) (f a) =
    (h a)^[f a] (g a)

Tactic:
induction f a
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → ℕ
g : α → β
h : α → β → β
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
a : α
⊢ Nat.rec (motive := fun (x : ℕ) ↦ β) (g a) (fun (n : ℕ) (IH : (fun (x : ℕ) ↦ β) n) ↦ h a (n, IH).2) 0 = (h a)^[0] (g a)

Tactic:
simp [*, -Function.iterate_succ, Function.iterate_succ']

Premises used: Function.iterate_succ, Function.iterate_succ'
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → ℕ
g : α → β
h : α → β → β
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
a : α
n : ℕ
h_1 :
  Nat.rec (motive := fun (x : ℕ) ↦ β) (g a) (fun (n : ℕ) (IH : (fun (x : ℕ) ↦ β) n) ↦ h a (n, IH).2) n = (h a)^[n] (g a)
⊢ Nat.rec (motive := fun (x : ℕ) ↦ β) (g a) (fun (n : ℕ) (IH : (fun (x : ℕ) ↦ β) n) ↦ h a (n, IH).2) (n + 1) =
    (h a)^[n + 1] (g a)

Tactic:
simp [*, -Function.iterate_succ, Function.iterate_succ']

Premises used: Function.iterate_succ, Function.iterate_succ'
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
o : α → Option β
f : α → σ
g : α → β → σ
ho : Primrec o
hf : Primrec f
hg : Primrec₂ g
a : α
none :
  (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_2} (α := Option β) Option.none) (encode (f a)) fun (b : ℕ) ↦
      (encode.{u_3} (α := Option σ)
          (Option.bind (decode (encode (a, b).1)) fun (a : α) ↦ Option.map (g a) (decode b))).pred) =
    encode.{u_3} (α := σ) (Option.casesOn (motive := fun (x : Option β) ↦ σ) Option.none (f a) (g a) : σ)
some :
  ∀ (b : β),
    (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode (Option.some b)) (encode (f a)) fun (b : ℕ) ↦
        (encode.{u_3} (α := Option σ)
            (Option.bind (decode (encode (a, b).1)) fun (a : α) ↦ Option.map (g a) (decode b))).pred) =
      encode.{u_3} (α := σ) (Option.casesOn (motive := fun (x : Option β) ↦ σ) (Option.some b) (f a) (g a) : σ)
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode (o a)) (encode (f a)) fun (b : ℕ) ↦
      (encode.{u_3} (α := Option σ)
          (Option.bind (decode (encode (a, b).1)) fun (a : α) ↦ Option.map (g a) (decode b))).pred) =
    encode.{u_3} (α := σ) (Option.casesOn (motive := fun (x : Option β) ↦ σ) (o a) (f a) (g a) : σ)

Tactic:
rcases o a with - | b
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
o : α → Option β
f : α → σ
g : α → β → σ
ho : Primrec o
hf : Primrec f
hg : Primrec₂ g
a : α
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode.{u_2} (α := Option β) none) (encode (f a)) fun (b : ℕ) ↦
      (encode.{u_3} (α := Option σ)
          (Option.bind (decode (encode (a, b).1)) fun (a : α) ↦ Option.map (g a) (decode b))).pred) =
    encode.{u_3} (α := σ) (Option.casesOn (motive := fun (x : Option β) ↦ σ) none (f a) (g a) : σ)

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 σ
o : α → Option β
f : α → σ
g : α → β → σ
ho : Primrec o
hf : Primrec f
hg : Primrec₂ g
a : α
b : β
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (encode (some b)) (encode (f a)) fun (b : ℕ) ↦
      (encode.{u_3} (α := Option σ)
          (Option.bind (decode (encode (a, b).1)) fun (a : α) ↦ Option.map (g a) (decode b))).pred) =
    encode.{u_3} (α := σ) (Option.casesOn (motive := fun (x : Option β) ↦ σ) (some b) (f a) (g a) : σ)

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 : α → Option β
g : α → β → Option σ
hf : Primrec f
hg : Primrec₂ g
a : α
none :
  Option.casesOn (motive := fun (x : Option β) ↦ Option σ) Option.none Option.none (g a) = Option.bind Option.none (g a)
some :
  ∀ (val : β),
    Option.casesOn (motive := fun (x : Option β) ↦ Option σ) (Option.some val) Option.none (g a) =
      (Option.some val).bind (g a)
⊢ Option.casesOn (motive := fun (x : Option β) ↦ Option σ) (f a) Option.none (g a) = (f a).bind (g a)

Tactic:
cases f 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 : α → Option β
g : α → β → Option σ
hf : Primrec f
hg : Primrec₂ g
a : α
⊢ Option.casesOn (motive := fun (x : Option β) ↦ Option σ) none none (g a) = Option.bind none (g a)

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 : α → Option β
g : α → β → Option σ
hf : Primrec f
hg : Primrec₂ g
a : α
val : β
⊢ Option.casesOn (motive := fun (x : Option β) ↦ Option σ) (some val) none (g a) = (some val).bind (g a)

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
f : α → Option σ
hf : Primrec f
⊢ Primrec.{u_1, u_3} (β := Option σ) fun (o : Option α) ↦ o.bind f

Tactic:
option_bind .id (hf.comp snd).to₂

Premises used: Primrec.snd, Primrec.comp, Primrec.option_bind, Primrec.id, Primrec.to₂