awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
f : α → ℕ
p : α → ℕ → Prop
inst_1 : DecidableRel p
hf : Primrec f
hp : PrimrecRel p
x : α
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
      (fun (n : ℕ) (IH : (fun (x : ℕ) ↦ ℕ) n) ↦ if p x ((n, IH).1 + 1) then (n, IH).1 + 1 else (n, IH).2) 0 =
    Nat.findGreatest (p x) 0

Tactic:
simp [Nat.findGreatest, *]

Premises used: Nat.findGreatest
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
f : α → ℕ
p : α → ℕ → Prop
inst_1 : DecidableRel p
hf : Primrec f
hp : PrimrecRel p
x : α
n : ℕ
h :
  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
      (fun (n : ℕ) (IH : (fun (x : ℕ) ↦ ℕ) n) ↦ if p x ((n, IH).1 + 1) then (n, IH).1 + 1 else (n, IH).2) n =
    Nat.findGreatest (p x) n
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0
      (fun (n : ℕ) (IH : (fun (x : ℕ) ↦ ℕ) n) ↦ if p x ((n, IH).1 + 1) then (n, IH).1 + 1 else (n, IH).2) (n + 1) =
    Nat.findGreatest (p x) (n + 1)

Tactic:
simp [Nat.findGreatest, *]

Premises used: Nat.findGreatest
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
f : α → ℕ
h₁ : PrimrecBounded f
h₂ : PrimrecRel fun (a : α) (b : ℕ) ↦ f a = b
rcases : ∀ (g : α → ℕ) (pg : Primrec g) (hg : ∀ (x : α), f x ≤ g x), Primrec f
⊢ Primrec f

Tactic:
rcases h₁ with ⟨g, pg, hg : ∀ x, f x ≤ g x⟩
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
f : α → ℕ
h₂ : PrimrecRel fun (a : α) (b : ℕ) ↦ f a = b
g : α → ℕ
pg : Primrec g
hg : ∀ (x : α), f x ≤ g x
⊢ Primrec f

Tactic:
(nat_findGreatest pg h₂).of_eq fun n => ?_

Premises used: Primrec.of_eq, Primrec.nat_findGreatest
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
f : α → ℕ
h₂ : PrimrecRel fun (a : α) (b : ℕ) ↦ f a = b
g : α → ℕ
pg : Primrec g
hg : ∀ (x : α), f x ≤ g x
refine : ∀ (n : α), Nat.findGreatest (fun (b : ℕ) ↦ f n = b) (g n) = f n
⊢ Primrec f

Tactic:
refine (nat_findGreatest pg h₂).of_eq fun n => ?_

Premises used: Primrec.of_eq, Primrec.nat_findGreatest
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
f : α → ℕ
h₂ : PrimrecRel fun (a : α) (b : ℕ) ↦ f a = b
g : α → ℕ
pg : Primrec g
hg : ∀ (x : α), f x ≤ g x
n : α
⊢ Nat.findGreatest (fun (b : ℕ) ↦ f n = b) (g n) = f n

Tactic:
(Nat.findGreatest_spec (P := fun b => f n = b) (hg n) rfl).symm

Premises used: Nat.findGreatest_spec, Eq.symm, rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
f : α → ℕ
h₂ : PrimrecRel fun (a : α) (b : ℕ) ↦ f a = b
g : α → ℕ
pg : Primrec g
hg : ∀ (x : α), f x ≤ g x
n : α
⊢ Nat.findGreatest (fun (b : ℕ) ↦ f n = b) (g n) = f n

Tactic:
exact (Nat.findGreatest_spec (P := fun b => f n = b) (hg n) rfl).symm

Premises used: Nat.findGreatest_spec, Eq.symm, rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
⊢ Primrec₂ (σ := ℕ) fun (x1 x2 : ℕ) ↦ x1 / x2

Tactic:
of_graph ⟨_, fst, fun p => Nat.div_le_self _ _⟩ ?_

Premises used: Primrec.fst, Nat.div_le_self, Prod.fst, Primrec.of_graph, And.intro, Exists.intro, Prod.snd, Primrec₂
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
refine : PrimrecRel fun (a : ℕ × ℕ) (b : ℕ) ↦ (fun (x1 x2 : ℕ) ↦ x1 / x2) a.1 a.2 = b
⊢ Primrec₂ (σ := ℕ) fun (x1 x2 : ℕ) ↦ x1 / x2

Tactic:
refine of_graph ⟨_, fst, fun p => Nat.div_le_self _ _⟩ ?_

Premises used: Primrec.fst, Nat.div_le_self, Prod.fst, Primrec.of_graph, And.intro, Exists.intro
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
⊢ PrimrecRel fun (a : ℕ × ℕ) (b : ℕ) ↦ a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2

Tactic:
have : PrimrecRel fun (a : ℕ × ℕ) (b : ℕ) => (a.2 = 0 ∧ b = 0) ∨
      (0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2) :=
    PrimrecPred.or
      (.and (const 0 |> Primrec.eq.comp (fst |> snd.comp)) (const 0 |> Primrec.eq.comp snd))
      (.and (nat_lt.comp (const 0) (fst |> snd.comp)) <|
          .and (nat_le.comp (nat_mul.comp snd (fst |> snd.comp)) (fst |> fst.comp))
          (nat_lt.comp (fst.comp fst) (nat_mul.comp (Primrec.succ.comp snd) (snd.comp fst))))
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
this : PrimrecRel fun (a : ℕ × ℕ) (b : ℕ) ↦ a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2
⊢ PrimrecRel fun (a : ℕ × ℕ) (b : ℕ) ↦ (fun (x1 x2 : ℕ) ↦ x1 / x2) a.1 a.2 = b

Tactic:
this.of_eq ?_

Premises used: PrimrecRel.of_eq
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
this : PrimrecRel fun (a : ℕ × ℕ) (b : ℕ) ↦ a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2
refine :
  ∀ (a : ℕ × ℕ) (b : ℕ),
    a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2 ↔ (fun (x1 x2 : ℕ) ↦ x1 / x2) a.1 a.2 = b
⊢ PrimrecRel fun (a : ℕ × ℕ) (b : ℕ) ↦ (fun (x1 x2 : ℕ) ↦ x1 / x2) a.1 a.2 = b

Tactic:
refine this.of_eq ?_

Premises used: PrimrecRel.of_eq
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
this : PrimrecRel fun (a : ℕ × ℕ) (b : ℕ) ↦ a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2
a k q : ℕ
H : k = 0
⊢ (a, k).2 = 0 ∧ q = 0 ∨ 0 < (a, k).2 ∧ q * (a, k).2 ≤ (a, k).1 ∧ (a, k).1 < (q + 1) * (a, k).2 ↔
    (fun (x1 x2 : ℕ) ↦ x1 / x2) (a, k).1 (a, k).2 = q

Tactic:
simp [H, eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
this : PrimrecRel fun (a : ℕ × ℕ) (b : ℕ) ↦ a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2
a k q : ℕ
H : ¬k = 0
rw : q * k ≤ a ∧ a < (q + 1) * k ↔ q ≤ a / k ∧ a / k ≤ q
rw₁ : q * k ≤ a ∧ a < (q + 1) * k ↔ q ≤ a / k ∧ a / k < q.succ
rw₂ : q * k ≤ a ∧ a < (q + 1) * k ↔ q * k ≤ a ∧ a / k < q.succ
rw₃ rw₄ : q * k ≤ a ∧ a < (q + 1) * k ↔ q * k ≤ a ∧ a < q.succ * k
⊢ q * k ≤ a ∧ a < (q + 1) * k ↔ q = a / k

Tactic:
rw [le_antisymm_iff, ← (@Nat.lt_succ_iff _ q), Nat.le_div_iff_mul_le (Nat.pos_of_ne_zero H),
          Nat.div_lt_iff_lt_mul (Nat.pos_of_ne_zero H)]

Premises used: Nat.div_lt_iff_lt_mul, Nat.pos_of_ne_zero, Nat.lt_succ_iff, le_antisymm_iff, Nat.le_div_iff_mul_le
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
this : PrimrecRel fun (a : ℕ × ℕ) (b : ℕ) ↦ a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2
a k q : ℕ
H : ¬k = 0
⊢ q * k ≤ a ∧ a < (q + 1) * k ↔ q = a / k

Tactic:
have : q * k ≤ a ∧ a < (q + 1) * k ↔ q = a / k := by
      rw [le_antisymm_iff, ← (@Nat.lt_succ_iff _ q), Nat.le_div_iff_mul_le (Nat.pos_of_ne_zero H),
          Nat.div_lt_iff_lt_mul (Nat.pos_of_ne_zero H)]
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
this_1 : PrimrecRel fun (a : ℕ × ℕ) (b : ℕ) ↦ a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2
a k q : ℕ
H : ¬k = 0
this : q * k ≤ a ∧ a < (q + 1) * k ↔ q = a / k
⊢ (a, k).2 = 0 ∧ q = 0 ∨ 0 < (a, k).2 ∧ q * (a, k).2 ≤ (a, k).1 ∧ (a, k).1 < (q + 1) * (a, k).2 ↔
    (fun (x1 x2 : ℕ) ↦ x1 / x2) (a, k).1 (a, k).2 = q

Tactic:
simpa [H, zero_lt_iff, eq_comm (b := q)]

Premises used: eq_comm, zero_lt_iff
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
this : PrimrecRel fun (a : ℕ × ℕ) (b : ℕ) ↦ a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2
a k q : ℕ
if :
  ∀ (H : k = 0),
    (a, k).2 = 0 ∧ q = 0 ∨ 0 < (a, k).2 ∧ q * (a, k).2 ≤ (a, k).1 ∧ (a, k).1 < (q + 1) * (a, k).2 ↔
      (fun (x1 x2 : ℕ) ↦ x1 / x2) (a, k).1 (a, k).2 = q
if₁ :
  ∀ (H : ¬k = 0),
    (a, k).2 = 0 ∧ q = 0 ∨ 0 < (a, k).2 ∧ q * (a, k).2 ≤ (a, k).1 ∧ (a, k).1 < (q + 1) * (a, k).2 ↔
      (fun (x1 x2 : ℕ) ↦ x1 / x2) (a, k).1 (a, k).2 = q
if₂ :
  ∀ (H : k = 0),
    (a, k).2 = 0 ∧ q = 0 ∨ 0 < (a, k).2 ∧ q * (a, k).2 ≤ (a, k).1 ∧ (a, k).1 < (q + 1) * (a, k).2 ↔
      (fun (x1 x2 : ℕ) ↦ x1 / x2) (a, k).1 (a, k).2 = q
if₃ if₄ :
  ∀ (H : ¬k = 0),
    (a, k).2 = 0 ∧ q = 0 ∨ 0 < (a, k).2 ∧ q * (a, k).2 ≤ (a, k).1 ∧ (a, k).1 < (q + 1) * (a, k).2 ↔
      (fun (x1 x2 : ℕ) ↦ x1 / x2) (a, k).1 (a, k).2 = q
⊢ (a, k).2 = 0 ∧ q = 0 ∨ 0 < (a, k).2 ∧ q * (a, k).2 ≤ (a, k).1 ∧ (a, k).1 < (q + 1) * (a, k).2 ↔
    (fun (x1 x2 : ℕ) ↦ x1 / x2) (a, k).1 (a, k).2 = q

Tactic:
if H : k = 0 then simp [H, eq_comm]
  else
    have : q * k ≤ a ∧ a < (q + 1) * k ↔ q = a / k := by
      rw [le_antisymm_iff, ← (@Nat.lt_succ_iff _ q), Nat.le_div_iff_mul_le (Nat.pos_of_ne_zero H),
          Nat.div_lt_iff_lt_mul (Nat.pos_of_ne_zero H)]
    simpa [H, zero_lt_iff, eq_comm (b := q)]

Premises used: eq_comm, zero_lt_iff
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
m n : ℕ
h : (m, n).1 = m % n + (m, n).2 * (fun (x1 x2 : ℕ) ↦ x1 / x2) (m, n).1 (m, n).2
⊢ (m, n).1 - (m, n).2 * (fun (x1 x2 : ℕ) ↦ x1 / x2) (m, n).1 (m, n).2 = m % n

Tactic:
apply Nat.sub_eq_of_eq_add

Premises used: Nat.sub_eq_of_eq_add
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
m n : ℕ
⊢ (m, n).1 = m % n + (m, n).2 * (fun (x1 x2 : ℕ) ↦ x1 / x2) (m, n).1 (m, n).2

Tactic:
simp [add_comm (m % n), Nat.div_add_mod]

Premises used: Nat.div_add_mod, add_comm, HMod.hMod
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
n : ℕ
false : ∀ (H : n.bodd = Bool.false), (id n % 2 == 1) = Bool.false
true : ∀ (H : n.bodd = Bool.true), (id n % 2 == 1) = Bool.true
⊢ (id n % 2 == 1) = n.bodd

Tactic:
cases H : n.bodd

Premises used: Nat.bodd
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
n : ℕ
H : n.bodd = false
⊢ (id n % 2 == 1) = false

Tactic:
simp [Nat.mod_two_of_bodd, H]

Premises used: Nat.mod_two_of_bodd
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
n : ℕ
H : n.bodd = true
⊢ (id n % 2 == 1) = true

Tactic:
simp [Nat.mod_two_of_bodd, H]

Premises used: Nat.mod_two_of_bodd
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
⊢ Primrec Nat.div2

Tactic:
(nat_div.comp .id (const 2)).of_eq fun n => n.div2_val.symm

Premises used: Primrec.of_eq, Primrec.const, Nat.div2_val, Primrec.nat_div, Primrec₂.comp, OfNat.ofNat, Eq.symm, Primrec.id
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
⊢ Primrec (β := ℕ) fun (n : ℕ) ↦ 2 * n

Tactic:
nat_mul.comp (const _) Primrec.id

Premises used: Primrec.nat_mul, Primrec.const, Primrec₂.comp, Primrec.id
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
⊢ Primrec (β := ℕ) fun (n : ℕ) ↦ 2 * n + 1

Tactic:
nat_double |> Primrec.succ.comp

Premises used: Primrec.nat_double, Primrec.succ, Primrec.comp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
simp :
  encode (α := Option ℕ)
      (bif n.bodd then Option.map (fun (b : β) ↦ 2 * encode b + 1) (decode n.div2)
      else Option.map (fun (b : α) ↦ 2 * encode b) (decode n.div2)) =
    encode (α := Option (α ⊕ β))
      (match (motive := Bool → ℕ → Option (α ⊕ β)) n.bodd, n.div2 with
        | false, m => Option.map Sum.inl (decode m)
        | x, m => Option.map Sum.inr (decode m) :
        Option (α ⊕ β))
⊢ encode (α := Option ℕ)
      (bif n.bodd then Option.map (fun (b : β) ↦ 2 * encode (n, b).2 + 1) (decode n.div2)
      else Option.map (fun (b : α) ↦ 2 * encode (n, b).2) (decode n.div2)) =
    encode (α := Option (α ⊕ β)) (decodeSum n)

Tactic:
simp only [decodeSum]

Premises used: Encodable.decodeSum
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
false :
  encode (α := Option ℕ)
      (bif Bool.false then Option.map (fun (b : β) ↦ 2 * encode b + 1) (decode n.div2)
      else Option.map (fun (b : α) ↦ 2 * encode b) (decode n.div2)) =
    encode (α := Option (α ⊕ β))
      (match (motive := Bool → ℕ → Option (α ⊕ β)) Bool.false, n.div2 with
        | Bool.false, m => Option.map Sum.inl (decode m)
        | x, m => Option.map Sum.inr (decode m) :
        Option (α ⊕ β))
true :
  encode (α := Option ℕ)
      (bif Bool.true then Option.map (fun (b : β) ↦ 2 * encode b + 1) (decode n.div2)
      else Option.map (fun (b : α) ↦ 2 * encode b) (decode n.div2)) =
    encode (α := Option (α ⊕ β))
      (match (motive := Bool → ℕ → Option (α ⊕ β)) Bool.true, n.div2 with
        | Bool.false, m => Option.map Sum.inl (decode m)
        | x, m => Option.map Sum.inr (decode m) :
        Option (α ⊕ β))
⊢ encode (α := Option ℕ)
      (bif n.bodd then Option.map (fun (b : β) ↦ 2 * encode b + 1) (decode n.div2)
      else Option.map (fun (b : α) ↦ 2 * encode b) (decode n.div2)) =
    encode (α := Option (α ⊕ β))
      (match (motive := Bool → ℕ → Option (α ⊕ β)) n.bodd, n.div2 with
        | Bool.false, m => Option.map Sum.inl (decode m)
        | x, m => Option.map Sum.inr (decode m) :
        Option (α ⊕ β))

Tactic:
cases Nat.bodd n

Premises used: Nat.bodd
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
false :
  encode (α := Option ℕ) (Option.map (fun (b : α) ↦ 2 * encode b) (decode n.div2)) =
    encode (α := Option (α ⊕ β)) (Option.map Sum.inl (decode n.div2))
⊢ encode (α := Option ℕ)
      (bif Bool.false then Option.map (fun (b : β) ↦ 2 * encode b + 1) (decode n.div2)
      else Option.map (fun (b : α) ↦ 2 * encode b) (decode n.div2)) =
    encode (α := Option (α ⊕ β))
      (match (motive := Bool → ℕ → Option (α ⊕ β)) Bool.false, n.div2 with
        | Bool.false, m => Option.map Sum.inl (decode m)
        | x, m => Option.map Sum.inr (decode m) :
        Option (α ⊕ β))

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
true :
  encode (α := Option ℕ) (Option.map (fun (b : β) ↦ 2 * encode b + 1) (decode n.div2)) =
    encode (α := Option (α ⊕ β)) (Option.map Sum.inr (decode n.div2))
⊢ encode (α := Option ℕ)
      (bif Bool.true then Option.map (fun (b : β) ↦ 2 * encode b + 1) (decode n.div2)
      else Option.map (fun (b : α) ↦ 2 * encode b) (decode n.div2)) =
    encode (α := Option (α ⊕ β))
      (match (motive := Bool → ℕ → Option (α ⊕ β)) Bool.true, n.div2 with
        | false, m => Option.map Sum.inl (decode m)
        | x, m => Option.map Sum.inr (decode m) :
        Option (α ⊕ β))

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
false :
  encode (α := Option ℕ) (Option.map (fun (b : α) ↦ 2 * encode b) none) =
    encode (α := Option (α ⊕ β)) (Option.map Sum.inl none)
false₁ :
  ∀ (val : α),
    encode (α := Option ℕ) (Option.map (fun (b : α) ↦ 2 * encode b) (some val)) =
      encode (α := Option (α ⊕ β)) (Option.map Sum.inl (some val))
⊢ encode (α := Option ℕ) (Option.map (fun (b : α) ↦ 2 * encode b) (decode n.div2)) =
    encode (α := Option (α ⊕ β)) (Option.map Sum.inl (decode n.div2))

Tactic:
cases @decode α _ n.div2

Premises used: Nat.div2, Encodable.decode
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
⊢ encode (α := Option ℕ) (Option.map (fun (b : α) ↦ 2 * encode b) none) =
    encode (α := Option (α ⊕ β)) (Option.map Sum.inl none)

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
val : α
⊢ encode (α := Option ℕ) (Option.map (fun (b : α) ↦ 2 * encode b) (some val)) =
    encode (α := Option (α ⊕ β)) (Option.map Sum.inl (some val))

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
true :
  encode (α := Option ℕ) (Option.map (fun (b : β) ↦ 2 * encode b + 1) none) =
    encode (α := Option (α ⊕ β)) (Option.map Sum.inr none)
true₁ :
  ∀ (val : β),
    encode (α := Option ℕ) (Option.map (fun (b : β) ↦ 2 * encode b + 1) (some val)) =
      encode (α := Option (α ⊕ β)) (Option.map Sum.inr (some val))
⊢ encode (α := Option ℕ) (Option.map (fun (b : β) ↦ 2 * encode b + 1) (decode n.div2)) =
    encode (α := Option (α ⊕ β)) (Option.map Sum.inr (decode n.div2))

Tactic:
cases @decode β _ n.div2

Premises used: Nat.div2, Encodable.decode
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
⊢ encode (α := Option ℕ) (Option.map (fun (b : β) ↦ 2 * encode b + 1) none) =
    encode (α := Option (α ⊕ β)) (Option.map Sum.inr none)

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
val : β
⊢ encode (α := Option ℕ) (Option.map (fun (b : β) ↦ 2 * encode b + 1) (some val)) =
    encode (α := Option (α ⊕ β)) (Option.map Sum.inr (some val))

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
⊢ Primrec (α := α) (β := α ⊕ β) Sum.inl

Tactic:
encode_iff.1 <| nat_double.comp Primrec.encode

Premises used: Primrec.nat_double, Primrec.encode_iff, Primrec.comp, Iff.mp, Primrec.encode
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
⊢ Primrec (α := β) (β := α ⊕ β) Sum.inr

Tactic:
encode_iff.1 <| nat_double_succ.comp Primrec.encode

Premises used: Primrec.encode_iff, Primrec.nat_double_succ, Primrec.comp, Iff.mp, Primrec.encode
-- 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 σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ → σ
hf : Primrec f
hg : Primrec₂ g
hh : Primrec₂ h
a : α
inl :
  ∀ (b : β),
    (bif (encode (α := β ⊕ γ) (Sum.inl b)).bodd then Option.map (h a) (decode (encode (α := β ⊕ γ) (Sum.inl b)).div2)
      else Option.map (g a) (decode (encode (α := β ⊕ γ) (Sum.inl b)).div2)) =
      some (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ σ) (Sum.inl b) (g a) (h a))
inr :
  ∀ (c : γ),
    (bif (encode (α := β ⊕ γ) (Sum.inr c)).bodd then Option.map (h a) (decode (encode (α := β ⊕ γ) (Sum.inr c)).div2)
      else Option.map (g a) (decode (encode (α := β ⊕ γ) (Sum.inr c)).div2)) =
      some (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ σ) (Sum.inr c) (g a) (h a))
⊢ (bif (encode (f a)).bodd then Option.map (h a) (decode (encode (f a)).div2)
    else Option.map (g a) (decode (encode (f a)).div2)) =
    some (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ σ) (f a) (g a) (h a))

Tactic:
rcases f a with b | c
-- 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 σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ → σ
hf : Primrec f
hg : Primrec₂ g
hh : Primrec₂ h
a : α
b : β
⊢ (bif (encode (α := β ⊕ γ) (Sum.inl b)).bodd then Option.map (h a) (decode (encode (α := β ⊕ γ) (Sum.inl b)).div2)
    else Option.map (g a) (decode (encode (α := β ⊕ γ) (Sum.inl b)).div2)) =
    some (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ σ) (Sum.inl b) (g a) (h a))

Tactic:
simp [Nat.div2_val, encodek]

Premises used: Nat.div2_val, Encodable.encodek
-- 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 σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ → σ
hf : Primrec f
hg : Primrec₂ g
hh : Primrec₂ h
a : α
c : γ
⊢ (bif (encode (α := β ⊕ γ) (Sum.inr c)).bodd then Option.map (h a) (decode (encode (α := β ⊕ γ) (Sum.inr c)).div2)
    else Option.map (g a) (decode (encode (α := β ⊕ γ) (Sum.inr c)).div2)) =
    some (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ σ) (Sum.inr c) (g a) (h a))

Tactic:
simp [Nat.div2_val, encodek]

Premises used: Nat.div2_val, Encodable.encodek
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
⊢ PrimrecRel fun (a : α) (b : β) ↦ ¬R a b

Tactic:
PrimrecPred.not hf

Premises used: PrimrecRel, PrimrecPred.not
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
hp : PrimrecPred p
this :
  Primrec.{0, u_1} (β := Option α) fun (n : ℕ) ↦
    Option.bind (decode n) fun (a : α) ↦ Option.guard (fun (b : α) ↦ decide (p b)) a
n : ℕ
none :
  encode.{u_1} (α := Option α) (Option.bind Option.none fun (a : α) ↦ Option.guard (fun (b : α) ↦ decide (p b)) a) =
    encode.{u_1} (α := Option (Subtype p))
      (Option.bind Option.none fun (x : α) ↦
        if h : p x then Option.some (Subtype.mk (p := fun (a : α) ↦ p a) x h) else Option.none)
some :
  ∀ (a : α),
    encode (α := Option α) ((Option.some a).bind fun (a : α) ↦ Option.guard (fun (b : α) ↦ decide (p b)) a) =
      encode (α := Option (Subtype p))
        ((Option.some a).bind fun (x : α) ↦
          if h : p x then Option.some (Subtype.mk (p := fun (a : α) ↦ p a) x h) else Option.none)
⊢ encode.{u_1} (α := Option α) (Option.bind (decode n) fun (a : α) ↦ Option.guard (fun (b : α) ↦ decide (p b)) a) =
    encode.{u_1} (α := Option (Subtype p))
      (Option.bind (decode n) fun (x : α) ↦
        if h : p x then Option.some (Subtype.mk (p := fun (a : α) ↦ p a) x h) else Option.none)

Tactic:
rcases @decode α _ n with - | a

Premises used: Encodable.decode
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
hp : PrimrecPred p
this :
  Primrec.{0, u_1} (β := Option α) fun (n : ℕ) ↦
    Option.bind (decode n) fun (a : α) ↦ Option.guard (fun (b : α) ↦ decide (p b)) a
n : ℕ
⊢ encode.{u_1} (α := Option α) (Option.bind none fun (a : α) ↦ Option.guard (fun (b : α) ↦ decide (p b)) a) =
    encode.{u_1} (α := Option (Subtype p))
      (Option.bind none fun (x : α) ↦ if h : p x then some (Subtype.mk (p := fun (a : α) ↦ p a) x h) else none)

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
hp : PrimrecPred p
this :
  Primrec.{0, u_1} (β := Option α) fun (n : ℕ) ↦
    Option.bind (decode n) fun (a : α) ↦ Option.guard (fun (b : α) ↦ decide (p b)) a
n : ℕ
a : α
some :
  encode (if decide (p a) = true then Option.some a else none) =
    encode.{u_1} (α := Option (Subtype p))
      (if h : p a then Option.some (Subtype.mk (p := fun (a : α) ↦ p a) a h) else none)
⊢ encode (α := Option α) ((Option.some a).bind fun (a : α) ↦ Option.guard (fun (b : α) ↦ decide (p b)) a) =
    encode (α := Option (Subtype p))
      ((Option.some a).bind fun (x : α) ↦
        if h : p x then Option.some (Subtype.mk (p := fun (a : α) ↦ p a) x h) else none)

Tactic:
dsimp [Option.guard]

Premises used: Option.guard
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
hp : PrimrecPred p
this :
  Primrec.{0, u_1} (β := Option α) fun (n : ℕ) ↦
    Option.bind (decode n) fun (a : α) ↦ Option.guard (fun (b : α) ↦ decide (p b)) a
n : ℕ
a : α
pos :
  ∀ (h : p a),
    encode (if decide (p a) = true then some a else none) =
      encode.{u_1} (α := Option (Subtype p)) (if h : p a then some (Subtype.mk (p := fun (a : α) ↦ p a) a h) else none)
neg :
  ∀ (h : ¬p a),
    encode (if decide (p a) = true then some a else none) =
      encode.{u_1} (α := Option (Subtype p)) (if h : p a then some (Subtype.mk (p := fun (a : α) ↦ p a) a h) else none)
⊢ encode (if decide (p a) = true then some a else none) =
    encode.{u_1} (α := Option (Subtype p)) (if h : p a then some (Subtype.mk (p := fun (a : α) ↦ p a) a h) else none)

Tactic:
by_cases h : p a
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
hp : PrimrecPred p
this :
  Primrec.{0, u_1} (β := Option α) fun (n : ℕ) ↦
    Option.bind (decode n) fun (a : α) ↦ Option.guard (fun (b : α) ↦ decide (p b)) a
n : ℕ
a : α
h : p a
pos : encode a = encode (Subtype.mk (p := fun (a : α) ↦ p a) a ⋯)
⊢ encode (if decide (p a) = true then some a else none) =
    encode.{u_1} (α := Option (Subtype p)) (if h : p a then some (Subtype.mk (p := fun (a : α) ↦ p a) a h) else none)

Tactic:
simp [h]
-- Module: Mathlib.Computability.Primrec.Basic
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
hp : PrimrecPred p
this :
  Primrec.{0, u_1} (β := Option α) fun (n : ℕ) ↦
    Option.bind (decode n) fun (a : α) ↦ Option.guard (fun (b : α) ↦ decide (p b)) a
n : ℕ
a : α
h : ¬p a
⊢ encode (if decide (p a) = true then some a else none) =
    encode.{u_1} (α := Option (Subtype p)) (if h : p a then some (Subtype.mk (p := fun (a : α) ↦ p a) a h) else none)

Tactic:
simp [h]