awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
f : ℕ → ℕ
hf : Nat.Primrec f
zero : Nat.Partrec (↑fun (x : ℕ) ↦ 0 : ℕ →. ℕ)
succ : Nat.Partrec (↑Nat.succ : ℕ →. ℕ)
⊢ Nat.Partrec (↑f : ℕ →. ℕ)
have left : Nat.Partrec (↑fun (n : ℕ) ↦ (unpair n).1 : ℕ →. ℕ)
Tactic: induction hf with
  | zero => exact zero
  | succ => exact succ
  | left => exact left
  | right => exact right
  | pair _ _ pf pg =>
    refine (pf.pair pg).of_eq_tot fun n => ?_
    simp [Seq.seq]
  | comp _ _ pf pg =>
    refine (pf.comp pg).of_eq_tot fun n => (by simp)
  | prec _ _ pf pg =>
    refine (pf.prec pg).of_eq_tot fun n => ?_
    simp only [unpaired, PFun.coe_val, bind_eq_bind]
    induction n.unpair.2 with
    | zero => simp
    | succ m IH =>
      simp only [mem_bind_iff, mem_some_iff]
      exact ⟨_, IH, rfl⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
f : ℕ → ℕ
hf : Nat.Primrec f
zero : Nat.Partrec (↑fun (x : ℕ) ↦ 0 : ℕ →. ℕ)
succ : Nat.Partrec (↑Nat.succ : ℕ →. ℕ)
left : Nat.Partrec (↑fun (n : ℕ) ↦ (unpair n).1 : ℕ →. ℕ)
⊢ Nat.Partrec (↑f : ℕ →. ℕ)
have right : Nat.Partrec (↑fun (n : ℕ) ↦ (unpair n).2 : ℕ →. ℕ)
Tactic: induction hf with
  | zero => exact zero
  | succ => exact succ
  | left => exact left
  | right => exact right
  | pair _ _ pf pg =>
    refine (pf.pair pg).of_eq_tot fun n => ?_
    simp [Seq.seq]
  | comp _ _ pf pg =>
    refine (pf.comp pg).of_eq_tot fun n => (by simp)
  | prec _ _ pf pg =>
    refine (pf.prec pg).of_eq_tot fun n => ?_
    simp only [unpaired, PFun.coe_val, bind_eq_bind]
    induction n.unpair.2 with
    | zero => simp
    | succ m IH =>
      simp only [mem_bind_iff, mem_some_iff]
      exact ⟨_, IH, rfl⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
f : ℕ → ℕ
hf : Nat.Primrec f
zero : Nat.Partrec (↑fun (x : ℕ) ↦ 0 : ℕ →. ℕ)
succ : Nat.Partrec (↑Nat.succ : ℕ →. ℕ)
left : Nat.Partrec (↑fun (n : ℕ) ↦ (unpair n).1 : ℕ →. ℕ)
right : Nat.Partrec (↑fun (n : ℕ) ↦ (unpair n).2 : ℕ →. ℕ)
⊢ Nat.Partrec (↑f : ℕ →. ℕ)
have pair : ∀ {f g : ℕ → ℕ},
  Nat.Primrec f →
    Nat.Primrec g →
      ∀ (pf : Nat.Partrec (↑f : ℕ →. ℕ)) (pg : Nat.Partrec (↑g : ℕ →. ℕ)),
        Nat.Partrec (↑fun (n : ℕ) ↦ Nat.pair (f n) (g n) : ℕ →. ℕ)
Tactic: induction hf with
  | zero => exact zero
  | succ => exact succ
  | left => exact left
  | right => exact right
  | pair _ _ pf pg =>
    refine (pf.pair pg).of_eq_tot fun n => ?_
    simp [Seq.seq]
  | comp _ _ pf pg =>
    refine (pf.comp pg).of_eq_tot fun n => (by simp)
  | prec _ _ pf pg =>
    refine (pf.prec pg).of_eq_tot fun n => ?_
    simp only [unpaired, PFun.coe_val, bind_eq_bind]
    induction n.unpair.2 with
    | zero => simp
    | succ m IH =>
      simp only [mem_bind_iff, mem_some_iff]
      exact ⟨_, IH, rfl⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
f : ℕ → ℕ
hf : Nat.Primrec f
zero : Nat.Partrec (↑fun (x : ℕ) ↦ 0 : ℕ →. ℕ)
succ : Nat.Partrec (↑Nat.succ : ℕ →. ℕ)
left : Nat.Partrec (↑fun (n : ℕ) ↦ (unpair n).1 : ℕ →. ℕ)
right : Nat.Partrec (↑fun (n : ℕ) ↦ (unpair n).2 : ℕ →. ℕ)
pair :
  ∀ {f g : ℕ → ℕ},
    Nat.Primrec f →
      Nat.Primrec g →
        ∀ (pf : Nat.Partrec (↑f : ℕ →. ℕ)) (pg : Nat.Partrec (↑g : ℕ →. ℕ)),
          Nat.Partrec (↑fun (n : ℕ) ↦ Nat.pair (f n) (g n) : ℕ →. ℕ)
⊢ Nat.Partrec (↑f : ℕ →. ℕ)
have comp : ∀ {f g : ℕ → ℕ},
  Nat.Primrec f →
    Nat.Primrec g →
      ∀ (pf : Nat.Partrec (↑f : ℕ →. ℕ)) (pg : Nat.Partrec (↑g : ℕ →. ℕ)), Nat.Partrec (↑fun (n : ℕ) ↦ f (g n) : ℕ →. ℕ)
Tactic: induction hf with
  | zero => exact zero
  | succ => exact succ
  | left => exact left
  | right => exact right
  | pair _ _ pf pg =>
    refine (pf.pair pg).of_eq_tot fun n => ?_
    simp [Seq.seq]
  | comp _ _ pf pg =>
    refine (pf.comp pg).of_eq_tot fun n => (by simp)
  | prec _ _ pf pg =>
    refine (pf.prec pg).of_eq_tot fun n => ?_
    simp only [unpaired, PFun.coe_val, bind_eq_bind]
    induction n.unpair.2 with
    | zero => simp
    | succ m IH =>
      simp only [mem_bind_iff, mem_some_iff]
      exact ⟨_, IH, rfl⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
f : ℕ → ℕ
hf : Nat.Primrec f
zero : Nat.Partrec (↑fun (x : ℕ) ↦ 0 : ℕ →. ℕ)
succ : Nat.Partrec (↑Nat.succ : ℕ →. ℕ)
left : Nat.Partrec (↑fun (n : ℕ) ↦ (unpair n).1 : ℕ →. ℕ)
right : Nat.Partrec (↑fun (n : ℕ) ↦ (unpair n).2 : ℕ →. ℕ)
pair :
  ∀ {f g : ℕ → ℕ},
    Nat.Primrec f →
      Nat.Primrec g →
        ∀ (pf : Nat.Partrec (↑f : ℕ →. ℕ)) (pg : Nat.Partrec (↑g : ℕ →. ℕ)),
          Nat.Partrec (↑fun (n : ℕ) ↦ Nat.pair (f n) (g n) : ℕ →. ℕ)
comp :
  ∀ {f g : ℕ → ℕ},
    Nat.Primrec f →
      Nat.Primrec g →
        ∀ (pf : Nat.Partrec (↑f : ℕ →. ℕ)) (pg : Nat.Partrec (↑g : ℕ →. ℕ)),
          Nat.Partrec (↑fun (n : ℕ) ↦ f (g n) : ℕ →. ℕ)
⊢ Nat.Partrec (↑f : ℕ →. ℕ)
have prec : ∀ {f g : ℕ → ℕ},
  Nat.Primrec f →
    Nat.Primrec g →
      ∀ (pf : Nat.Partrec (↑f : ℕ →. ℕ)) (pg : Nat.Partrec (↑g : ℕ →. ℕ)),
        Nat.Partrec
          (↑(unpaired fun (z n : ℕ) ↦
                Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f z) (fun (y IH : ℕ) ↦ g (Nat.pair z (Nat.pair y IH))) n) :
            ℕ →. ℕ)
Tactic: induction hf with
  | zero => exact zero
  | succ => exact succ
  | left => exact left
  | right => exact right
  | pair _ _ pf pg =>
    refine (pf.pair pg).of_eq_tot fun n => ?_
    simp [Seq.seq]
  | comp _ _ pf pg =>
    refine (pf.comp pg).of_eq_tot fun n => (by simp)
  | prec _ _ pf pg =>
    refine (pf.prec pg).of_eq_tot fun n => ?_
    simp only [unpaired, PFun.coe_val, bind_eq_bind]
    induction n.unpair.2 with
    | zero => simp
    | succ m IH =>
      simp only [mem_bind_iff, mem_some_iff]
      exact ⟨_, IH, rfl⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
this : Primrec₂ (σ := ℕ) fun (n m : ℕ) ↦ if n = m.succ then 0 else 1
n : ℕ
⊢ (Nat.rfind fun (n_1 : ℕ) ↦
      (fun (m : ℕ) ↦ decide (m = 0)) <$>
        (↑(unpaired fun (n m : ℕ) ↦ if n = m.succ then 0 else 1) : ℕ →. ℕ) (Nat.pair n n_1)) =
    (↑n.ppred : Part ℕ)
have zero : (Nat.rfind fun (n : ℕ) ↦
    (fun (m : ℕ) ↦ decide (m = 0)) <$>
      (↑(unpaired fun (n m : ℕ) ↦ if n = m.succ then 0 else 1) : ℕ →. ℕ) (Nat.pair 0 n)) =
  (↑(Nat.ppred 0) : Part ℕ)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
this : Primrec₂ (σ := ℕ) fun (n m : ℕ) ↦ if n = m.succ then 0 else 1
n : ℕ
zero :
  (Nat.rfind fun (n : ℕ) ↦
      (fun (m : ℕ) ↦ decide (m = 0)) <$>
        (↑(unpaired fun (n m : ℕ) ↦ if n = m.succ then 0 else 1) : ℕ →. ℕ) (Nat.pair 0 n)) =
    (↑(Nat.ppred 0) : Part ℕ)
⊢ (Nat.rfind fun (n_1 : ℕ) ↦
      (fun (m : ℕ) ↦ decide (m = 0)) <$>
        (↑(unpaired fun (n m : ℕ) ↦ if n = m.succ then 0 else 1) : ℕ →. ℕ) (Nat.pair n n_1)) =
    (↑n.ppred : Part ℕ)
have succ : ∀ (n : ℕ),
  (Nat.rfind fun (n_1 : ℕ) ↦
      (fun (m : ℕ) ↦ decide (m = 0)) <$>
        (↑(unpaired fun (n m : ℕ) ↦ if n = m.succ then 0 else 1) : ℕ →. ℕ) (Nat.pair (n + 1) n_1)) =
    (↑(n + 1).ppred : Part ℕ)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
this : Primrec₂ (σ := ℕ) fun (n m : ℕ) ↦ if n = m.succ then 0 else 1
n : ℕ
⊢ n ∈
    Nat.rfind fun (n_1 : ℕ) ↦
      (fun (m : ℕ) ↦ decide (m = 0)) <$>
        (↑(unpaired fun (n m : ℕ) ↦ if n = m.succ then 0 else 1) : ℕ →. ℕ) (Nat.pair (n + 1) n_1)
have simp : ∀ {m : ℕ}, m < n → ¬n = m
Tactic: simp
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → σ
hf : Primrec f
n : ℕ
⊢ Eq (α := Part ℕ)
    (do
      let n ← (↑fun (n : ℕ) ↦ encode (Option.map f (decode n)) : ℕ →. ℕ) n
      (↑n.ppred : Part ℕ))
    (Part.bind (↑(decode n) : Part α) fun (a : α) ↦ map encode ((↑f : α →. σ) a))
have simp : (↑(encode (Option.map f (decode n))).ppred : Part ℕ) =
  Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.some (encode (f a))
Tactic: simp
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → σ
hf : Primrec f
n : ℕ
⊢ (↑(encode (Option.map f (decode n))).ppred : Part ℕ) =
    Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.some (encode (f a))
have none : (↑(encode (Option.map f Option.none)).ppred : Part ℕ) =
  Part.bind (↑Option.none : Part α) fun (a : α) ↦ Part.some (encode (f a))
Tactic: cases decode (α := α) n
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → σ
hf : Primrec f
n : ℕ
none :
  (↑(encode (Option.map f Option.none)).ppred : Part ℕ) =
    Part.bind (↑Option.none : Part α) fun (a : α) ↦ Part.some (encode (f a))
⊢ (↑(encode (Option.map f (decode n))).ppred : Part ℕ) =
    Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.some (encode (f a))
have some : ∀ (val : α),
  (↑(encode (Option.map f (Option.some val))).ppred : Part ℕ) =
    (↑(Option.some val) : Part α).bind fun (a : α) ↦ Part.some (encode (f a))
Tactic: cases decode (α := α) n
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
⊢ Eq (α := Part ℕ)
    (do
      let n ← Part.bind (↑(decode n) : Part α) fun (a : α) ↦ map encode ((↑f : α →. Option β) a)
      (↑n.ppred : Part ℕ))
    (Part.bind (↑(decode n) : Part α) fun (a : α) ↦ map.{u_2, 0} (α := β) encode ((fun (a : α) ↦ (↑(f a) : Part β)) a))
have none : Eq (α := Part ℕ)
  (do
    let n ← Part.bind (↑Option.none : Part α) fun (a : α) ↦ map encode ((↑f : α →. Option β) a)
    (↑n.ppred : Part ℕ))
  (Part.bind (↑Option.none : Part α) fun (a : α) ↦ map.{u_2, 0} (α := β) encode ((fun (a : α) ↦ (↑(f a) : Part β)) a))
Tactic: rcases decode (α := α) n with - | a
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
none :
  Eq (α := Part ℕ)
    (do
      let n ← Part.bind (↑Option.none : Part α) fun (a : α) ↦ map encode ((↑f : α →. Option β) a)
      (↑n.ppred : Part ℕ))
    (Part.bind (↑Option.none : Part α) fun (a : α) ↦ map.{u_2, 0} (α := β) encode ((fun (a : α) ↦ (↑(f a) : Part β)) a))
⊢ Eq (α := Part ℕ)
    (do
      let n ← Part.bind (↑(decode n) : Part α) fun (a : α) ↦ map encode ((↑f : α →. Option β) a)
      (↑n.ppred : Part ℕ))
    (Part.bind (↑(decode n) : Part α) fun (a : α) ↦ map.{u_2, 0} (α := β) encode ((fun (a : α) ↦ (↑(f a) : Part β)) a))
have some : ∀ (a : α),
  Eq (α := Part ℕ)
    (do
      let n ← (↑(Option.some a) : Part α).bind fun (a : α) ↦ map encode ((↑f : α →. Option β) a)
      (↑n.ppred : Part ℕ))
    ((↑(Option.some a) : Part α).bind fun (a : α) ↦ map.{u_2, 0} (α := β) encode ((fun (a : α) ↦ (↑(f a) : Part β)) a))
Tactic: rcases decode (α := α) n with - | a
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
a : α
⊢ Eq (α := Part ℕ)
    (do
      let n ← (↑(Option.some a) : Part α).bind fun (a : α) ↦ map encode ((↑f : α →. Option β) a)
      (↑n.ppred : Part ℕ))
    ((↑(Option.some a) : Part α).bind fun (a : α) ↦ map.{u_2, 0} (α := β) encode ((fun (a : α) ↦ (↑(f a) : Part β)) a))
have some : (↑(encode (f a)).ppred : Part ℕ) = map encode (↑(f a) : Part β)
Tactic: simp
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
a : α
⊢ (↑(encode (f a)).ppred : Part ℕ) = map encode (↑(f a) : Part β)
have some : (↑(encode.{u_2} (α := Option β) Option.none).ppred : Part ℕ) = map.{u_2, 0} (α := β) encode (↑Option.none : Part β)
Tactic: cases f a
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
a : α
some :
  (↑(encode.{u_2} (α := Option β) Option.none).ppred : Part ℕ) = map.{u_2, 0} (α := β) encode (↑Option.none : Part β)
⊢ (↑(encode (f a)).ppred : Part ℕ) = map encode (↑(f a) : Part β)
have some₁ : ∀ (val : β), (↑(encode (Option.some val)).ppred : Part ℕ) = map encode (↑(Option.some val) : Part β)
Tactic: cases f a
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
f : α → β
g : α → γ
hf : Computable f
hg : Computable g
n : ℕ
⊢ ((Nat.pair <$> Part.bind (↑(decode n) : Part α) fun (a : α) ↦ map encode ((↑f : α →. β) a)) <*>
      Part.bind (↑(decode n) : Part α) fun (a : α) ↦ map encode ((↑g : α →. γ) a)) =
    Part.bind (↑(decode n) : Part α) fun (a : α) ↦ map (α := β × γ) encode ((↑fun (a : α) ↦ (f a, g a) : α →. β × γ) a)
have none : ((Nat.pair <$> Part.bind (↑Option.none : Part α) fun (a : α) ↦ map encode ((↑f : α →. β) a)) <*>
    Part.bind (↑Option.none : Part α) fun (a : α) ↦ map encode ((↑g : α →. γ) a)) =
  Part.bind (↑Option.none : Part α) fun (a : α) ↦ map (α := β × γ) encode ((↑fun (a : α) ↦ (f a, g a) : α →. β × γ) a)
Tactic: cases decode (α := α) n
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
f : α → β
g : α → γ
hf : Computable f
hg : Computable g
n : ℕ
none :
  ((Nat.pair <$> Part.bind (↑Option.none : Part α) fun (a : α) ↦ map encode ((↑f : α →. β) a)) <*>
      Part.bind (↑Option.none : Part α) fun (a : α) ↦ map encode ((↑g : α →. γ) a)) =
    Part.bind (↑Option.none : Part α) fun (a : α) ↦ map (α := β × γ) encode ((↑fun (a : α) ↦ (f a, g a) : α →. β × γ) a)
⊢ ((Nat.pair <$> Part.bind (↑(decode n) : Part α) fun (a : α) ↦ map encode ((↑f : α →. β) a)) <*>
      Part.bind (↑(decode n) : Part α) fun (a : α) ↦ map encode ((↑g : α →. γ) a)) =
    Part.bind (↑(decode n) : Part α) fun (a : α) ↦ map (α := β × γ) encode ((↑fun (a : α) ↦ (f a, g a) : α →. β × γ) a)
have some : ∀ (val : α),
  ((Nat.pair <$> (↑(Option.some val) : Part α).bind fun (a : α) ↦ map encode ((↑f : α →. β) a)) <*>
      (↑(Option.some val) : Part α).bind fun (a : α) ↦ map encode ((↑g : α →. γ) a)) =
    (↑(Option.some val) : Part α).bind fun (a : α) ↦
      map (α := β × γ) encode ((↑fun (a : α) ↦ (f a, g a) : α →. β × γ) a)
Tactic: cases decode (α := α) n
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
n : ℕ
⊢ Eq (α := Part ℕ) Part.none
    (Part.bind (↑(decode n) : Part α) fun (a : α) ↦
      map.{u_3, 0} (α := σ) encode ((fun (x : α) ↦ (Part.none : Part σ)) a))
have none₁ : Eq (α := Part ℕ) Part.none
  (Part.bind (↑Option.none : Part α) fun (a : α) ↦
    map.{u_3, 0} (α := σ) encode ((fun (x : α) ↦ (Part.none : Part σ)) a))
Tactic: cases decode (α := α) n
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
n : ℕ
none₁ :
  Eq (α := Part ℕ) Part.none
    (Part.bind (↑Option.none : Part α) fun (a : α) ↦
      map.{u_3, 0} (α := σ) encode ((fun (x : α) ↦ (Part.none : Part σ)) a))
⊢ Eq (α := Part ℕ) Part.none
    (Part.bind (↑(decode n) : Part α) fun (a : α) ↦
      map.{u_3, 0} (α := σ) encode ((fun (x : α) ↦ (Part.none : Part σ)) a))
have some : ∀ (val : α),
  Eq (α := Part ℕ) Part.none
    ((↑(Option.some val) : Part α).bind fun (a : α) ↦
      map.{u_3, 0} (α := σ) encode ((fun (x : α) ↦ (Part.none : Part σ)) a))
Tactic: cases decode (α := α) n
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α →. β
g : α → β →. σ
hf : Partrec f
hg : Partrec₂ g
n : ℕ
⊢ Eq (α := Part ℕ)
    (do
      let n ← Nat.pair <$> Part.some n <*> Part.bind (↑(decode n) : Part α) fun (a : α) ↦ map encode (f a)
      Part.bind (↑(decode n) : Part (α × β)) fun (a : α × β) ↦
          map.{u_3, 0} (α := σ) encode ((fun (p : α × β) ↦ g p.1 p.2) a))
    (Part.bind (↑(decode n) : Part α) fun (a : α) ↦ map.{u_3, 0} (α := σ) encode ((fun (a : α) ↦ (f a).bind (g a)) a))
have none : ∀ (e : Eq.{u_1 + 1} (α := Option α) (decode n) Option.none),
  Eq (α := Part ℕ)
    (do
      let n ← Nat.pair <$> Part.some n <*> Part.bind (↑Option.none : Part α) fun (a : α) ↦ map encode (f a)
      Part.bind (↑(decode n) : Part (α × β)) fun (a : α × β) ↦
          map.{u_3, 0} (α := σ) encode ((fun (p : α × β) ↦ g p.1 p.2) a))
    (Part.bind (↑Option.none : Part α) fun (a : α) ↦ map.{u_3, 0} (α := σ) encode ((fun (a : α) ↦ (f a).bind (g a)) a))
Tactic: rcases e : decode (α := α) n
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α →. β
g : α → β →. σ
hf : Partrec f
hg : Partrec₂ g
n : ℕ
none :
  ∀ (e : Eq.{u_1 + 1} (α := Option α) (decode n) Option.none),
    Eq (α := Part ℕ)
      (do
        let n ← Nat.pair <$> Part.some n <*> Part.bind (↑Option.none : Part α) fun (a : α) ↦ map encode (f a)
        Part.bind (↑(decode n) : Part (α × β)) fun (a : α × β) ↦
            map.{u_3, 0} (α := σ) encode ((fun (p : α × β) ↦ g p.1 p.2) a))
      (Part.bind (↑Option.none : Part α) fun (a : α) ↦
        map.{u_3, 0} (α := σ) encode ((fun (a : α) ↦ (f a).bind (g a)) a))
⊢ Eq (α := Part ℕ)
    (do
      let n ← Nat.pair <$> Part.some n <*> Part.bind (↑(decode n) : Part α) fun (a : α) ↦ map encode (f a)
      Part.bind (↑(decode n) : Part (α × β)) fun (a : α × β) ↦
          map.{u_3, 0} (α := σ) encode ((fun (p : α × β) ↦ g p.1 p.2) a))
    (Part.bind (↑(decode n) : Part α) fun (a : α) ↦ map.{u_3, 0} (α := σ) encode ((fun (a : α) ↦ (f a).bind (g a)) a))
have some : ∀ (val : α) (e : decode n = Option.some val),
  Eq (α := Part ℕ)
    (do
      let n ← Nat.pair <$> Part.some n <*> (↑(Option.some val) : Part α).bind fun (a : α) ↦ map encode (f a)
      Part.bind (↑(decode n) : Part (α × β)) fun (a : α × β) ↦
          map.{u_3, 0} (α := σ) encode ((fun (p : α × β) ↦ g p.1 p.2) a))
    ((↑(Option.some val) : Part α).bind fun (a : α) ↦ map.{u_3, 0} (α := σ) encode ((fun (a : α) ↦ (f a).bind (g a)) a))
Tactic: rcases e : decode (α := α) n
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
⊢ Eq (α := Part ℕ)
    (Part.bind (Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.map encode ((↑f : α →. ℕ) a)) fun (n_1 : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.map encode (g a))
        (fun (y : ℕ) (IH : Part ℕ) ↦ do
          let i ← IH
          Part.bind (↑(decode (Nat.pair n (Nat.pair y i))) : Part (α × ℕ × σ)) fun (a : Prod.{u_1, u_3} α (ℕ × σ)) ↦
              Part.map.{u_3, 0} (α := σ) encode ((fun (p : Prod.{u_1, u_3} α (ℕ × σ)) ↦ h p.1 p.2) a))
        n_1)
    (Part.bind (↑(decode n) : Part α) fun (a : α) ↦
      Part.map.{u_3, 0} (α := σ) encode
        ((fun (a : α) ↦
            (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (g a)
                (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (y, i)) (f a) :
              Part σ))
          a))
have none : ∀ (e : Eq.{u_1 + 1} (α := Option α) (decode n) Option.none),
  Eq (α := Part ℕ)
    (Part.bind (Part.bind (↑Option.none : Part α) fun (a : α) ↦ Part.map encode ((↑f : α →. ℕ) a)) fun (n_1 : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (Part.bind (↑Option.none : Part α) fun (a : α) ↦ Part.map encode (g a))
        (fun (y : ℕ) (IH : Part ℕ) ↦ do
          let i ← IH
          Part.bind (↑(decode (Nat.pair n (Nat.pair y i))) : Part (α × ℕ × σ)) fun (a : Prod.{u_1, u_3} α (ℕ × σ)) ↦
              Part.map.{u_3, 0} (α := σ) encode ((fun (p : Prod.{u_1, u_3} α (ℕ × σ)) ↦ h p.1 p.2) a))
        n_1)
    (Part.bind (↑Option.none : Part α) fun (a : α) ↦
      Part.map.{u_3, 0} (α := σ) encode
        ((fun (a : α) ↦
            (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (g a)
                (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (y, i)) (f a) :
              Part σ))
          a))
Tactic: rcases e : decode (α := α) n with - | a
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
none :
  ∀ (e : Eq.{u_1 + 1} (α := Option α) (decode n) Option.none),
    Eq (α := Part ℕ)
      (Part.bind (Part.bind (↑Option.none : Part α) fun (a : α) ↦ Part.map encode ((↑f : α →. ℕ) a)) fun (n_1 : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (Part.bind (↑Option.none : Part α) fun (a : α) ↦ Part.map encode (g a))
          (fun (y : ℕ) (IH : Part ℕ) ↦ do
            let i ← IH
            Part.bind (↑(decode (Nat.pair n (Nat.pair y i))) : Part (α × ℕ × σ)) fun (a : Prod.{u_1, u_3} α (ℕ × σ)) ↦
                Part.map.{u_3, 0} (α := σ) encode ((fun (p : Prod.{u_1, u_3} α (ℕ × σ)) ↦ h p.1 p.2) a))
          n_1)
      (Part.bind (↑Option.none : Part α) fun (a : α) ↦
        Part.map.{u_3, 0} (α := σ) encode
          ((fun (a : α) ↦
              (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (g a)
                  (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (y, i)) (f a) :
                Part σ))
            a))
⊢ Eq (α := Part ℕ)
    (Part.bind (Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.map encode ((↑f : α →. ℕ) a)) fun (n_1 : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.map encode (g a))
        (fun (y : ℕ) (IH : Part ℕ) ↦ do
          let i ← IH
          Part.bind (↑(decode (Nat.pair n (Nat.pair y i))) : Part (α × ℕ × σ)) fun (a : Prod.{u_1, u_3} α (ℕ × σ)) ↦
              Part.map.{u_3, 0} (α := σ) encode ((fun (p : Prod.{u_1, u_3} α (ℕ × σ)) ↦ h p.1 p.2) a))
        n_1)
    (Part.bind (↑(decode n) : Part α) fun (a : α) ↦
      Part.map.{u_3, 0} (α := σ) encode
        ((fun (a : α) ↦
            (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (g a)
                (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (y, i)) (f a) :
              Part σ))
          a))
have some : ∀ (a : α) (e : decode n = Option.some a),
  Eq (α := Part ℕ)
    (Part.bind ((↑(Option.some a) : Part α).bind fun (a : α) ↦ Part.map encode ((↑f : α →. ℕ) a)) fun (n_1 : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) ((↑(Option.some a) : Part α).bind fun (a : α) ↦ Part.map encode (g a))
        (fun (y : ℕ) (IH : Part ℕ) ↦ do
          let i ← IH
          Part.bind (↑(decode (Nat.pair n (Nat.pair y i))) : Part (α × ℕ × σ)) fun (a : Prod.{u_1, u_3} α (ℕ × σ)) ↦
              Part.map.{u_3, 0} (α := σ) encode ((fun (p : Prod.{u_1, u_3} α (ℕ × σ)) ↦ h p.1 p.2) a))
        n_1)
    ((↑(Option.some a) : Part α).bind fun (a : α) ↦
      Part.map.{u_3, 0} (α := σ) encode
        ((fun (a : α) ↦
            (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (g a)
                (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (y, i)) (f a) :
              Part σ))
          a))
Tactic: rcases e : decode (α := α) n with - | a