awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ
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))
have some : ((Part.map encode (Part.some (f a))).bind fun (n_1 : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (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 encode (h a.1 a.2))
      n_1) =
  Part.map.{u_3, 0} (α := σ) encode
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (g a) (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (y, i))
      (f a))
Tactic: simp only [coe_some, PFun.coe_val, bind_some]
-- 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 : ℕ
a : α
e : decode n = Option.some a
⊢ ((Part.map encode (Part.some (f a))).bind fun (n_1 : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (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 encode (h a.1 a.2))
        n_1) =
    Part.map.{u_3, 0} (α := σ) encode
      (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (g a) (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (y, i))
        (f a))
have some : ((Part.map (α := ℕ) encode (Part.some 0)).bind fun (n_1 : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (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 encode (h a.1 a.2))
      n_1) =
  Part.map.{u_3, 0} (α := σ) encode
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (g a) (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (y, i)) 0)
Tactic: induction f 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 : ℕ
a : α
e : decode n = Option.some a
some :
  ((Part.map (α := ℕ) encode (Part.some 0)).bind fun (n_1 : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (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 encode (h a.1 a.2))
        n_1) =
    Part.map.{u_3, 0} (α := σ) encode
      (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (g a) (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (y, i)) 0)
⊢ ((Part.map encode (Part.some (f a))).bind fun (n_1 : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (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 encode (h a.1 a.2))
        n_1) =
    Part.map.{u_3, 0} (α := σ) encode
      (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (g a) (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (y, i))
        (f a))
have some₁ : ∀ (n_1 : ℕ),
  ((Part.map encode (Part.some n_1)).bind fun (n_2 : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (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 encode (h a.1 a.2))
          n_2) =
      Part.map.{u_3, 0} (α := σ) encode
        (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (g a) (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (y, i))
          n_1) →
    ((Part.map encode (Part.some (n_1 + 1))).bind fun (n_2 : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (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 encode (h a.1 a.2))
          n_2) =
      Part.map.{u_3, 0} (α := σ) encode
        (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (g a) (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (y, i))
          (n_1 + 1))
Tactic: induction 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 : Partrec f
hg : Computable g
n : ℕ
⊢ Eq (α := Part ℕ)
    (do
      let n ← Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.map encode ((↑g : α →. β) a)
      Part.bind (↑(decode n) : Part β) fun (a : β) ↦ Part.map encode (f a))
    (Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.map.{u_3, 0} (α := σ) encode ((fun (a : α) ↦ f (g a)) a))
have simp : Eq (α := Part ℕ)
  (Part.bind (Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.some (encode (g a))) fun (n : ℕ) ↦
    Part.bind (↑(decode n) : Part β) fun (a : β) ↦ Part.map encode (f a))
  (Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.map encode (f (g a)))
Tactic: simp only [PFun.coe_val, map_some, bind_eq_bind]
-- 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 : Computable g
n : ℕ
⊢ Eq (α := Part ℕ)
    (Part.bind (Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.some (encode (g a))) fun (n : ℕ) ↦
      Part.bind (↑(decode n) : Part β) fun (a : β) ↦ Part.map encode (f a))
    (Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.map encode (f (g 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.some (encode (g a))) fun (n : ℕ) ↦
      Part.bind (↑(decode n) : Part β) fun (a : β) ↦ Part.map encode (f a))
    (Part.bind (↑Option.none : Part α) fun (a : α) ↦ Part.map encode (f (g a)))
Tactic: rcases e : decode (α := α) n with - | 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 : Partrec f
hg : Computable g
n : ℕ
none :
  ∀ (e : Eq.{u_1 + 1} (α := Option α) (decode n) Option.none),
    Eq (α := Part ℕ)
      (Part.bind (Part.bind (↑Option.none : Part α) fun (a : α) ↦ Part.some (encode (g a))) fun (n : ℕ) ↦
        Part.bind (↑(decode n) : Part β) fun (a : β) ↦ Part.map encode (f a))
      (Part.bind (↑Option.none : Part α) fun (a : α) ↦ Part.map encode (f (g a)))
⊢ Eq (α := Part ℕ)
    (Part.bind (Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.some (encode (g a))) fun (n : ℕ) ↦
      Part.bind (↑(decode n) : Part β) fun (a : β) ↦ Part.map encode (f a))
    (Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.map encode (f (g a)))
have some : ∀ (a : α) (e : decode n = Option.some a),
  Eq (α := Part ℕ)
    (Part.bind ((↑(Option.some a) : Part α).bind fun (a : α) ↦ Part.some (encode (g a))) fun (n : ℕ) ↦
      Part.bind (↑(decode n) : Part β) fun (a : β) ↦ Part.map encode (f a))
    ((↑(Option.some a) : Part α).bind fun (a : α) ↦ Part.map encode (f (g a)))
Tactic: rcases e : decode (α := α) n with - | a
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
inst : Primcodable α
p : α → ℕ →. Bool
hp : Partrec₂ p
n : ℕ
⊢ (Nat.rfind fun (n_1 : ℕ) ↦
      (fun (m : ℕ) ↦ decide (m = 0)) <$>
        Part.bind (↑(decode (Nat.pair n n_1)) : Part (α × ℕ)) fun (a : α × ℕ) ↦
          Part.map (α := ℕ) encode
            ((fun (a : α × ℕ) ↦ (Part.map (fun (b : Bool) ↦ bif (a, b).2 then 0 else 1) (p a.1 a.2) : Part ℕ)) a)) =
    Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.map (α := ℕ) encode ((fun (a : α) ↦ Nat.rfind (p a)) a)
have none : ∀ (e : Eq.{u_1 + 1} (α := Option α) (decode n) Option.none),
  (Nat.rfind fun (n_1 : ℕ) ↦
      (fun (m : ℕ) ↦ decide (m = 0)) <$>
        Part.bind (↑(decode (Nat.pair n n_1)) : Part (α × ℕ)) fun (a : α × ℕ) ↦
          Part.map (α := ℕ) encode
            ((fun (a : α × ℕ) ↦ (Part.map (fun (b : Bool) ↦ bif (a, b).2 then 0 else 1) (p a.1 a.2) : Part ℕ)) a)) =
    Part.bind (↑Option.none : Part α) fun (a : α) ↦ Part.map (α := ℕ) encode ((fun (a : α) ↦ Nat.rfind (p a)) a)
Tactic: rcases e : decode (α := α) n
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
inst : Primcodable α
p : α → ℕ →. Bool
hp : Partrec₂ p
n : ℕ
none :
  ∀ (e : Eq.{u_1 + 1} (α := Option α) (decode n) Option.none),
    (Nat.rfind fun (n_1 : ℕ) ↦
        (fun (m : ℕ) ↦ decide (m = 0)) <$>
          Part.bind (↑(decode (Nat.pair n n_1)) : Part (α × ℕ)) fun (a : α × ℕ) ↦
            Part.map (α := ℕ) encode
              ((fun (a : α × ℕ) ↦ (Part.map (fun (b : Bool) ↦ bif (a, b).2 then 0 else 1) (p a.1 a.2) : Part ℕ)) a)) =
      Part.bind (↑Option.none : Part α) fun (a : α) ↦ Part.map (α := ℕ) encode ((fun (a : α) ↦ Nat.rfind (p a)) a)
⊢ (Nat.rfind fun (n_1 : ℕ) ↦
      (fun (m : ℕ) ↦ decide (m = 0)) <$>
        Part.bind (↑(decode (Nat.pair n n_1)) : Part (α × ℕ)) fun (a : α × ℕ) ↦
          Part.map (α := ℕ) encode
            ((fun (a : α × ℕ) ↦ (Part.map (fun (b : Bool) ↦ bif (a, b).2 then 0 else 1) (p a.1 a.2) : Part ℕ)) a)) =
    Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.map (α := ℕ) encode ((fun (a : α) ↦ Nat.rfind (p a)) a)
have some : ∀ (val : α) (e : decode n = Option.some val),
  (Nat.rfind fun (n_1 : ℕ) ↦
      (fun (m : ℕ) ↦ decide (m = 0)) <$>
        Part.bind (↑(decode (Nat.pair n n_1)) : Part (α × ℕ)) fun (a : α × ℕ) ↦
          Part.map (α := ℕ) encode
            ((fun (a : α × ℕ) ↦ (Part.map (fun (b : Bool) ↦ bif (a, b).2 then 0 else 1) (p a.1 a.2) : Part ℕ)) a)) =
    (↑(Option.some val) : Part α).bind fun (a : α) ↦ Part.map (α := ℕ) encode ((fun (a : α) ↦ Nat.rfind (p a)) a)
Tactic: rcases e : decode (α := α) n
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
⊢ Eq.{u_2 + 1} (α := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) ((↑g : α →. σ) a)
        (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h (a, y, i).1 (f (a, y, i).1).pred) (f a) :
      Part σ)
    (Nat.casesOn (motive := fun (x : ℕ) ↦ Part σ) (f a) (Part.some (g a)) (h a) : Part σ)
have simp : Eq.{u_2 + 1} (α := Part σ)
  (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
      (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (f a - 1)) (f a) :
    Part σ)
  (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (f a) : Part σ)
Tactic: simp only [PFun.coe_val, Nat.pred_eq_sub_one]
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
⊢ Eq.{u_2 + 1} (α := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
        (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (f a - 1)) (f a) :
      Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (f a) : Part σ)
have zero : Eq.{u_2 + 1} (α := Part σ)
  (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
      (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (HSub.hSub (α := ℕ) 0 1)) 0 :
    Part σ)
  (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) 0 : Part σ)
Tactic: rcases f a with - | n
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
zero :
  Eq.{u_2 + 1} (α := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
        (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (HSub.hSub (α := ℕ) 0 1)) 0 :
      Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) 0 : Part σ)
⊢ Eq.{u_2 + 1} (α := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
        (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (f a - 1)) (f a) :
      Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (f a) : Part σ)
have succ : ∀ (n : ℕ),
  Eq.{u_2 + 1} (α := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
        (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (n + 1 - 1)) (n + 1) :
      Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (n + 1) : Part σ)
Tactic: rcases f a with - | n
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
⊢ Eq.{u_2 + 1} (α := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
        (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (n + 1 - 1)) (n + 1) :
      Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (n + 1) : Part σ)
have succ : ∀ (b : σ)
  (H :
    Membership.mem (γ := Part σ)
      (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
          (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (n + 1 - 1)) (n + 1) :
        Part σ)
      b),
  Membership.mem (γ := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (n + 1) : Part σ)
    b
Tactic: refine ext fun b => ⟨fun H => ?_, fun H => ?_⟩
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
succ :
  ∀ (b : σ)
    (H :
      Membership.mem (γ := Part σ)
        (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
            (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (n + 1 - 1)) (n + 1) :
          Part σ)
        b),
    Membership.mem (γ := Part σ)
      (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (n + 1) :
        Part σ)
      b
⊢ Eq.{u_2 + 1} (α := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
        (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (n + 1 - 1)) (n + 1) :
      Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (n + 1) : Part σ)
have succ₁ : ∀ (b : σ)
  (H :
    Membership.mem (γ := Part σ)
      (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (n + 1) :
        Part σ)
      b),
  Membership.mem (γ := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
        (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (n + 1 - 1)) (n + 1) :
      Part σ)
    b
Tactic: refine ext fun b => ⟨fun H => ?_, fun H => ?_⟩
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H :
  Membership.mem (γ := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
        (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (n + 1 - 1)) (n + 1) :
      Part σ)
    b
⊢ Membership.mem (γ := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (n + 1) : Part σ)
    b
have succ : ∀ (c : σ),
  Membership.mem (γ := Part σ)
      (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
          (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (n + 1 - 1)) n :
        Part σ)
      c →
    ∀ (h₂ : b ∈ h a (n + 1 - 1)),
      Membership.mem (γ := Part σ)
        (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (n + 1) :
          Part σ)
        b
Tactic: rcases mem_bind_iff.1 H with ⟨c, _, h₂⟩
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H :
  Membership.mem (γ := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (n + 1) : Part σ)
    b
m : ℕ
⊢ Dom.{u_2} (α := σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
      (fun (y : ℕ) (IH : (fun (x : ℕ) ↦ Part σ) y) ↦ Part.bind IH fun (x : σ) ↦ h a n) m)
have zero : Dom.{u_2} (α := σ)
  (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
    (fun (y : ℕ) (IH : (fun (x : ℕ) ↦ Part σ) y) ↦ Part.bind IH fun (x : σ) ↦ h a n) 0)
Tactic: induction m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H :
  Membership.mem (γ := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (n + 1) : Part σ)
    b
m : ℕ
zero :
  Dom.{u_2} (α := σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
      (fun (y : ℕ) (IH : (fun (x : ℕ) ↦ Part σ) y) ↦ Part.bind IH fun (x : σ) ↦ h a n) 0)
⊢ Dom.{u_2} (α := σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
      (fun (y : ℕ) (IH : (fun (x : ℕ) ↦ Part σ) y) ↦ Part.bind IH fun (x : σ) ↦ h a n) m)
have succ : ∀ (n_1 : ℕ),
  Dom.{u_2} (α := σ)
      (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
        (fun (y : ℕ) (IH : (fun (x : ℕ) ↦ Part σ) y) ↦ Part.bind IH fun (x : σ) ↦ h a n) n_1) →
    Dom.{u_2} (α := σ)
      (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
        (fun (y : ℕ) (IH : (fun (x : ℕ) ↦ Part σ) y) ↦ Part.bind IH fun (x : σ) ↦ h a n) (n_1 + 1))
Tactic: induction m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Computability.Partrec (hypothesis)
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H :
  Membership.mem (γ := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (n + 1) : Part σ)
    b
⊢ Membership.mem (γ := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
        (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (n + 1 - 1)) (n + 1) :
      Part σ)
    b
have this : ∀ (m : ℕ),
  Dom.{u_2} (α := σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
      (fun (y : ℕ) (IH : (fun (x : ℕ) ↦ Part σ) y) ↦ Part.bind IH fun (x : σ) ↦ h a n) m)
Tactic: have : ∀ m, (Nat.rec (motive := fun _ => Part σ)
            (Part.some (g a)) (fun y IH => IH.bind fun _ => h a n) m).Dom := by
          intro m
          induction m <;> simp [*, H.fst]
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
n : ℕ
f : Fin (n + 1) → α →. σ
hf : ∀ (i : Fin (n + 1)), Partrec (f i)
⊢ Partrec.{u_1, u_2} (α := α) (σ := List.Vector σ (n + 1)) fun (a : α) ↦ Vector.mOfFn fun (i : Fin (n + 1)) ↦ f i a
have simp : Partrec.{u_1, u_2} (α := α) (σ := List.Vector σ (n + 1)) fun (a : α) ↦
  (f 0 a).bind fun (a_1 : σ) ↦
    Part.bind (Vector.mOfFn fun (i : Fin n) ↦ f i.succ a) fun (v : List.Vector σ n) ↦ Part.some (a_1 ::ᵥ v)
Tactic: simp only [Vector.mOfFn, pure_eq_some, bind_eq_bind]
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → β → Option σ
hf : Computable₂.{u_1, 0, u_4} (σ := Option σ) fun (a : α) (n : ℕ) ↦ Option.bind (decode n) (f a)
n : ℕ
⊢ Eq (α := Part ℕ)
    (Part.bind (↑(decode n) : Part (α × ℕ)) fun (a : α × ℕ) ↦
      map.{u_4, 0} (α := Option σ) encode
        ((fun (a : α × ℕ) ↦
            (Part.bind (α := ℕ)
                (do
                  let n ← (↑fun (n : ℕ) ↦ encode.{u_2} (α := Option β) (decode n) : ℕ →. ℕ) a.2
                  (↑n.ppred : Part ℕ))
                (↑fun (b : ℕ) ↦ (fun (a : α) (n : ℕ) ↦ Option.bind (decode n) (f a)) (a, b).1.1 (a, b).1.2 :
                  ℕ →. Option σ) :
              Part (Option σ)))
          a))
    (Part.bind (↑(decode n) : Part (α × β)) fun (a : α × β) ↦
      map.{u_4, 0} (α := Option σ) encode ((↑fun (p : α × β) ↦ f p.1 p.2 : α × β →. Option σ) a))
have simp : Eq (α := Part ℕ)
  (Part.bind (↑(Option.bind (decode (Nat.unpair n).1) fun (a : α) ↦ Option.some (a, (Nat.unpair n).2)) : Part (α × ℕ))
    fun (a : α × ℕ) ↦
    (↑(encode.{u_2} (α := Option β) (decode a.2)).ppred : Part ℕ).bind fun (y : ℕ) ↦
      Part.some (encode.{u_4} (α := Option σ) (Option.bind (decode a.2) fun (a_1 : β) ↦ f a.1 a_1)))
  (Part.bind
    (↑(Option.bind (decode (Nat.unpair n).1) fun (a : α) ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)) :
      Part (α × β))
    fun (a : α × β) ↦ Part.some (encode (f a.1 a.2)))
Tactic: simp only [decode_prod_val, decode_nat, Option.map_some, PFun.coe_val, bind_eq_bind,
          bind_some, Part.map_bind, map_some]