awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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
have refine : ∀ (n : α), Nat.findGreatest (fun (b : ℕ) ↦ f n = b) (g n) = f n
Tactic: refine (nat_findGreatest pg h₂).of_eq fun n => ?_
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
⊢ Primrec₂ (σ := ℕ) fun (x1 x2 : ℕ) ↦ x1 / x2
have refine : PrimrecRel fun (a : ℕ × ℕ) (b : ℕ) ↦ (fun (x1 x2 : ℕ) ↦ x1 / x2) a.1 a.2 = b
Tactic: refine of_graph ⟨_, fst, fun p => Nat.div_le_self _ _⟩ ?_
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (hypothesis)
Goal:
⊢ PrimrecRel fun (a : ℕ × ℕ) (b : ℕ) ↦ (fun (x1 x2 : ℕ) ↦ x1 / x2) a.1 a.2 = b
have this : 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))))
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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
have 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
Tactic: refine this.of_eq ?_
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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
have rw : q * k ≤ a ∧ a < (q + 1) * k ↔ q ≤ a / k ∧ a / k ≤ q
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)]
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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
⊢ q * k ≤ a ∧ a < (q + 1) * k ↔ q = a / k
have rw₁ : q * k ≤ a ∧ a < (q + 1) * k ↔ q ≤ a / k ∧ a / k < q.succ
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)]
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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
⊢ q * k ≤ a ∧ a < (q + 1) * k ↔ q = a / k
have rw₂ : q * k ≤ a ∧ a < (q + 1) * k ↔ q * k ≤ a ∧ a / k < q.succ
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)]
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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
⊢ q * k ≤ a ∧ a < (q + 1) * k ↔ q = a / k
have rw₃ : q * k ≤ a ∧ a < (q + 1) * k ↔ q * k ≤ a ∧ a < q.succ * 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)]
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (hypothesis)
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
have this₁ : 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)]
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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 : ℕ
⊢ (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
have 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
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)]
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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
⊢ (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
have 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
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)]
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
m n : ℕ
⊢ (m, n).1 - (m, n).2 * (fun (x1 x2 : ℕ) ↦ x1 / x2) (m, n).1 (m, n).2 = m % n
have h : (m, n).1 = m % n + (m, n).2 * (fun (x1 x2 : ℕ) ↦ x1 / x2) (m, n).1 (m, n).2
Tactic: apply Nat.sub_eq_of_eq_add
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
n : ℕ
⊢ (id n % 2 == 1) = n.bodd
have false : ∀ (H : n.bodd = false), (id n % 2 == 1) = false
Tactic: cases H : n.bodd
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
n : ℕ
false : ∀ (H : n.bodd = Bool.false), (id n % 2 == 1) = Bool.false
⊢ (id n % 2 == 1) = n.bodd
have true : ∀ (H : n.bodd = true), (id n % 2 == 1) = true
Tactic: cases H : n.bodd
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
⊢ 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)
have 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 (α ⊕ β))
Tactic: simp only [decodeSum]
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
⊢ 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 (α ⊕ β))
have false : encode (α := Option ℕ)
    (bif 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 (α ⊕ β)) false, n.div2 with
      | false, m => Option.map Sum.inl (decode m)
      | x, m => Option.map Sum.inr (decode m) :
      Option (α ⊕ β))
Tactic: cases Nat.bodd n
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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 (α ⊕ β))
⊢ 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 (α ⊕ β))
have true : encode (α := Option ℕ)
    (bif 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 (α ⊕ β)) true, 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
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
⊢ encode (α := Option ℕ)
      (bif 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 (α ⊕ β)) false, n.div2 with
        | false, m => Option.map Sum.inl (decode m)
        | x, m => Option.map Sum.inr (decode m) :
        Option (α ⊕ β))
have false : encode (α := Option ℕ) (Option.map (fun (b : α) ↦ 2 * encode b) (decode n.div2)) =
  encode (α := Option (α ⊕ β)) (Option.map Sum.inl (decode n.div2))
Tactic: simp
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
⊢ encode (α := Option ℕ)
      (bif 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 (α ⊕ β)) true, n.div2 with
        | false, m => Option.map Sum.inl (decode m)
        | x, m => Option.map Sum.inr (decode m) :
        Option (α ⊕ β))
have true : encode (α := Option ℕ) (Option.map (fun (b : β) ↦ 2 * encode b + 1) (decode n.div2)) =
  encode (α := Option (α ⊕ β)) (Option.map Sum.inr (decode n.div2))
Tactic: simp
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
⊢ encode (α := Option ℕ) (Option.map (fun (b : α) ↦ 2 * encode b) (decode n.div2)) =
    encode (α := Option (α ⊕ β)) (Option.map Sum.inl (decode n.div2))
have false : encode (α := Option ℕ) (Option.map (fun (b : α) ↦ 2 * encode b) none) =
  encode (α := Option (α ⊕ β)) (Option.map Sum.inl none)
Tactic: cases @decode α _ n.div2
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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)
⊢ encode (α := Option ℕ) (Option.map (fun (b : α) ↦ 2 * encode b) (decode n.div2)) =
    encode (α := Option (α ⊕ β)) (Option.map Sum.inl (decode n.div2))
have false₁ : ∀ (val : α),
  encode (α := Option ℕ) (Option.map (fun (b : α) ↦ 2 * encode b) (some val)) =
    encode (α := Option (α ⊕ β)) (Option.map Sum.inl (some val))
Tactic: cases @decode α _ n.div2
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
⊢ encode (α := Option ℕ) (Option.map (fun (b : β) ↦ 2 * encode b + 1) (decode n.div2)) =
    encode (α := Option (α ⊕ β)) (Option.map Sum.inr (decode n.div2))
have true : encode (α := Option ℕ) (Option.map (fun (b : β) ↦ 2 * encode b + 1) none) =
  encode (α := Option (α ⊕ β)) (Option.map Sum.inr none)
Tactic: cases @decode β _ n.div2
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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)
⊢ encode (α := Option ℕ) (Option.map (fun (b : β) ↦ 2 * encode b + 1) (decode n.div2)) =
    encode (α := Option (α ⊕ β)) (Option.map Sum.inr (decode n.div2))
have true₁ : ∀ (val : β),
  encode (α := Option ℕ) (Option.map (fun (b : β) ↦ 2 * encode b + 1) (some val)) =
    encode (α := Option (α ⊕ β)) (Option.map Sum.inr (some val))
Tactic: cases @decode β _ n.div2
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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 : α
⊢ (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))
have 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))
Tactic: rcases f a with b | c
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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))
⊢ (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))
have 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))
Tactic: rcases f a with b | c
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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 (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 some (Subtype.mk (p := fun (a : α) ↦ p a) x h) else none)
have none : 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: rcases @decode α _ n with - | a
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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 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 some (Subtype.mk (p := fun (a : α) ↦ p a) x h) else Option.none)
have some : ∀ (a : α),
  encode (α := Option α) ((some a).bind fun (a : α) ↦ Option.guard (fun (b : α) ↦ decide (p b)) a) =
    encode (α := Option (Subtype p))
      ((some a).bind fun (x : α) ↦ if h : p x then some (Subtype.mk (p := fun (a : α) ↦ p a) x h) else Option.none)
Tactic: rcases @decode α _ n with - | a
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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 : α
⊢ encode (α := Option α) ((some a).bind fun (a : α) ↦ Option.guard (fun (b : α) ↦ decide (p b)) a) =
    encode (α := Option (Subtype p))
      ((some a).bind fun (x : α) ↦ if h : p x then some (Subtype.mk (p := fun (a : α) ↦ p a) x h) else none)
have some : 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: dsimp [Option.guard]
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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 : α
⊢ 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)
have 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)
Tactic: by_cases h : p a
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases h : p a
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
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)
have pos : encode a = encode (Subtype.mk (p := fun (a : α) ↦ p a) a sorry)
Tactic: simp [h]
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
hp : PrimrecPred p
this : Primcodable (Subtype p) := Primcodable.subtype (p := p) hp
⊢ Primrec.{u_1, u_1} (α := Subtype p) (Subtype.val (p := p))
have refine : ∀ (n : ℕ),
  encode.{u_1} (α := Option (Subtype p)) (decode n) =
    encode.{u_1} (α := Option α) (Option.map (α := Subtype p) (Subtype.val (p := p)) (decode n))
Tactic: refine (Primcodable.prim (Subtype p)).of_eq fun n => ?_
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
hp : PrimrecPred p
this : Primcodable (Subtype p) := Primcodable.subtype (p := p) hp
n : ℕ
⊢ encode.{u_1} (α := Option (Subtype p)) (decode n) =
    encode.{u_1} (α := Option α) (Option.map (α := Subtype p) (Subtype.val (p := p)) (decode n))
have none : encode.{u_1} (α := Option (Subtype p)) none =
  encode.{u_1} (α := Option α) (Option.map (α := Subtype p) (Subtype.val (p := p)) none)
Tactic: rcases @decode (Subtype p) _ n with (_ | ⟨a, h⟩)
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
hp : PrimrecPred p
this : Primcodable (Subtype p) := Primcodable.subtype (p := p) hp
n : ℕ
none :
  encode.{u_1} (α := Option (Subtype p)) Option.none =
    encode.{u_1} (α := Option α) (Option.map (α := Subtype p) (Subtype.val (p := p)) Option.none)
⊢ encode.{u_1} (α := Option (Subtype p)) (decode n) =
    encode.{u_1} (α := Option α) (Option.map (α := Subtype p) (Subtype.val (p := p)) (decode n))
have some : ∀ (a : α) (h : p a),
  encode (some (Subtype.mk (p := p) a h)) = encode (Option.map (Subtype.val (p := p)) (some (Subtype.mk (p := p) a h)))
Tactic: rcases @decode (Subtype p) _ n with (_ | ⟨a, h⟩)
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
p : β → Prop
inst_2 : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype (p := p) hp
⊢ (Primrec.{u_1, u_2} (β := β) fun (a : α) ↦ (↑(f a) : β)) ↔ Primrec f
have refine : ∀ (h : Primrec.{u_1, u_2} (β := β) fun (a : α) ↦ (↑(f a) : β)), Primrec f
Tactic: refine ⟨fun h => ?_, fun hf => subtype_val.comp hf⟩
-- Lean 4 proof step from Mathlib.Computability.Primrec.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
p : β → Prop
inst_2 : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype (p := p) hp
h : Primrec.{u_1, u_2} (β := β) fun (a : α) ↦ (↑(f a) : β)
⊢ Primrec f
have refine : ∀ (n : ℕ),
  encode.{u_2} (α := Option β) (Option.map (fun (a : α) ↦ (↑(f a) : β)) (decode n)) = encode (Option.map f (decode n))
Tactic: refine Nat.Primrec.of_eq h fun n => ?_