awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (↑(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)))
have none : Eq (α := Part ℕ)
  (Part.bind (↑(Option.bind Option.none 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 Option.none fun (a : α) ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)) : Part (α × β))
    fun (a : α × β) ↦ Part.some (encode (f a.1 a.2)))
Tactic: cases decode (α := α) n.unpair.1
-- 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 : ℕ
none :
  Eq (α := Part ℕ)
    (Part.bind (↑(Option.bind Option.none 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 Option.none fun (a : α) ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)) : Part (α × β))
      fun (a : α × β) ↦ Part.some (encode (f a.1 a.2)))
⊢ 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)))
have some : ∀ (val : α),
  Eq (α := Part ℕ)
    (Part.bind (↑((Option.some val).bind 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.some val).bind fun (a : α) ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)) : Part (α × β))
      fun (a : α × β) ↦ Part.some (encode (f a.1 a.2)))
Tactic: cases decode (α := α) n.unpair.1
-- 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 : ℕ
val : α
⊢ Eq (α := Part ℕ)
    (Part.bind (↑((Option.some val).bind 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.some val).bind fun (a : α) ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)) : Part (α × β))
      fun (a : α × β) ↦ Part.some (encode (f a.1 a.2)))
have some : Eq (α := Part ℕ)
  ((↑(encode.{u_2} (α := Option β) (decode (Nat.unpair n).2)).ppred : Part ℕ).bind fun (y : ℕ) ↦
    Part.some (encode.{u_4} (α := Option σ) (Option.bind (decode (Nat.unpair n).2) fun (a : β) ↦ f val a)))
  (Part.bind (↑(Option.map (Prod.mk val) (decode (Nat.unpair n).2)) : Part (α × β)) fun (a : α × β) ↦
    Part.some (encode (f a.1 a.2)))
Tactic: simp
-- 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 : ℕ
val : α
⊢ Eq (α := Part ℕ)
    ((↑(encode.{u_2} (α := Option β) (decode (Nat.unpair n).2)).ppred : Part ℕ).bind fun (y : ℕ) ↦
      Part.some (encode.{u_4} (α := Option σ) (Option.bind (decode (Nat.unpair n).2) fun (a : β) ↦ f val a)))
    (Part.bind (↑(Option.map (Prod.mk val) (decode (Nat.unpair n).2)) : Part (α × β)) fun (a : α × β) ↦
      Part.some (encode (f a.1 a.2)))
have some : Eq (α := Part ℕ)
  ((↑(encode.{u_2} (α := Option β) Option.none).ppred : Part ℕ).bind fun (y : ℕ) ↦
    Part.some (encode.{u_4} (α := Option σ) (Option.bind Option.none fun (a : β) ↦ f val a)))
  (Part.bind (↑(Option.map (Prod.mk val) Option.none) : Part (α × β)) fun (a : α × β) ↦ Part.some (encode (f a.1 a.2)))
Tactic: cases decode (α := β) n.unpair.2
-- 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 : ℕ
val : α
some :
  Eq (α := Part ℕ)
    ((↑(encode.{u_2} (α := Option β) Option.none).ppred : Part ℕ).bind fun (y : ℕ) ↦
      Part.some (encode.{u_4} (α := Option σ) (Option.bind Option.none fun (a : β) ↦ f val a)))
    (Part.bind (↑(Option.map (Prod.mk val) Option.none) : Part (α × β)) fun (a : α × β) ↦
      Part.some (encode (f a.1 a.2)))
⊢ Eq (α := Part ℕ)
    ((↑(encode.{u_2} (α := Option β) (decode (Nat.unpair n).2)).ppred : Part ℕ).bind fun (y : ℕ) ↦
      Part.some (encode.{u_4} (α := Option σ) (Option.bind (decode (Nat.unpair n).2) fun (a : β) ↦ f val a)))
    (Part.bind (↑(Option.map (Prod.mk val) (decode (Nat.unpair n).2)) : Part (α × β)) fun (a : α × β) ↦
      Part.some (encode (f a.1 a.2)))
have some₁ : ∀ (val_1 : β),
  Eq (α := Part ℕ)
    ((↑(encode (Option.some val_1)).ppred : Part ℕ).bind fun (y : ℕ) ↦
      Part.some (encode.{u_4} (α := Option σ) ((Option.some val_1).bind fun (a : β) ↦ f val a)))
    ((↑(Option.map (Prod.mk val) (Option.some val_1)) : Part (α × β)).bind fun (a : α × β) ↦
      Part.some (encode (f a.1 a.2)))
Tactic: cases decode (α := β) n.unpair.2
-- Lean 4 proof step from Mathlib.Computability.Partrec (hypothesis)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → β → Option σ
hf : Computable₂ f
⊢ Computable₂.{u_1, 0, u_4} (σ := Option σ) fun (a : α) (n : ℕ) ↦ Option.bind (decode n) (f a)
have this : Partrec.{u_1, u_4} (α := α × ℕ) (σ := Option σ) fun (a : α × ℕ) ↦
  Nat.casesOn (motive := fun (x : ℕ) ↦ Part (Option σ)) (encode.{u_2} (α := Option β) (decode a.2))
    (Part.some Option.none) fun (n : ℕ) ↦ map (f a.1) (↑(decode n) : Part β)
Tactic: have :
      Partrec fun a : α × ℕ =>
        (encode (decode (α := β) a.2)).casesOn (some Option.none)
          fun n => Part.map (f a.1) (decode (α := β) n) :=
      Partrec.nat_casesOn_right
        (h := fun (a : α × ℕ) (n : ℕ) ↦ map (fun b ↦ f a.1 b) (Part.ofOption (decode n)))
        (Primrec.encdec.to_comp.comp snd) (const Option.none)
        ((ofOption (Computable.decode.comp snd)).map (hf.comp (fst.comp <| fst.comp fst) snd).to₂)
-- 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₂ f
this :
  Partrec.{u_1, u_4} (α := α × ℕ) (σ := Option σ) fun (a : α × ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ Part (Option σ)) (encode.{u_2} (α := Option β) (decode a.2))
      (Part.some Option.none) fun (n : ℕ) ↦ map (f a.1) (↑(decode n) : Part β)
⊢ Computable₂.{u_1, 0, u_4} (σ := Option σ) fun (a : α) (n : ℕ) ↦ Option.bind (decode n) (f a)
have refine : ∀ (a : α × ℕ),
  Eq.{u_4 + 1} (α := Part (Option σ))
    (Nat.casesOn (motive := fun (x : ℕ) ↦ Part (Option σ)) (encode.{u_2} (α := Option β) (decode a.2))
        (Part.some Option.none) fun (n : ℕ) ↦ map (f a.1) (↑(decode n) : Part β) :
      Part (Option σ))
    ((↑fun (p : α × ℕ) ↦ (fun (a : α) (n : ℕ) ↦ Option.bind (decode n) (f a)) p.1 p.2 : α × ℕ →. Option σ) a :
      Part (Option σ))
Tactic: refine this.of_eq fun a => ?_
-- 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₂ f
this :
  Partrec.{u_1, u_4} (α := α × ℕ) (σ := Option σ) fun (a : α × ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ Part (Option σ)) (encode.{u_2} (α := Option β) (decode a.2))
      (Part.some Option.none) fun (n : ℕ) ↦ map (f a.1) (↑(decode n) : Part β)
a : α × ℕ
⊢ Eq.{u_4 + 1} (α := Part (Option σ))
    (Nat.casesOn (motive := fun (x : ℕ) ↦ Part (Option σ)) (encode.{u_2} (α := Option β) (decode a.2))
        (Part.some Option.none) fun (n : ℕ) ↦ map (f a.1) (↑(decode n) : Part β) :
      Part (Option σ))
    ((↑fun (p : α × ℕ) ↦ (fun (a : α) (n : ℕ) ↦ Option.bind (decode n) (f a)) p.1 p.2 : α × ℕ →. Option σ) a :
      Part (Option σ))
have simp : Nat.rec (motive := fun (x : ℕ) ↦ Part (Option σ)) (Part.some Option.none)
    (fun (n : ℕ) (n_ih : Part (Option σ)) ↦ map (f a.1) (↑(decode n) : Part β))
    (encode.{u_2} (α := Option β) (decode a.2)) =
  Part.some (Option.bind (decode a.2) (f a.1))
Tactic: simp
-- 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₂ f
this :
  Partrec.{u_1, u_4} (α := α × ℕ) (σ := Option σ) fun (a : α × ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ Part (Option σ)) (encode.{u_2} (α := Option β) (decode a.2))
      (Part.some Option.none) fun (n : ℕ) ↦ map (f a.1) (↑(decode n) : Part β)
a : α × ℕ
⊢ Nat.rec (motive := fun (x : ℕ) ↦ Part (Option σ)) (Part.some Option.none)
      (fun (n : ℕ) (n_ih : Part (Option σ)) ↦ map (f a.1) (↑(decode n) : Part β))
      (encode.{u_2} (α := Option β) (decode a.2)) =
    Part.some (Option.bind (decode a.2) (f a.1))
have none : Nat.rec (motive := fun (x : ℕ) ↦ Part (Option σ)) (Part.some Option.none)
    (fun (n : ℕ) (n_ih : Part (Option σ)) ↦ map (f a.1) (↑(decode n) : Part β))
    (encode.{u_2} (α := Option β) Option.none) =
  Part.some (Option.bind Option.none (f a.1))
Tactic: cases decode (α := β) a.2
-- 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₂ f
this :
  Partrec.{u_1, u_4} (α := α × ℕ) (σ := Option σ) fun (a : α × ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ Part (Option σ)) (encode.{u_2} (α := Option β) (decode a.2))
      (Part.some Option.none) fun (n : ℕ) ↦ map (f a.1) (↑(decode n) : Part β)
a : α × ℕ
none :
  Nat.rec (motive := fun (x : ℕ) ↦ Part (Option σ)) (Part.some Option.none)
      (fun (n : ℕ) (n_ih : Part (Option σ)) ↦ map (f a.1) (↑(decode n) : Part β))
      (encode.{u_2} (α := Option β) Option.none) =
    Part.some (Option.bind Option.none (f a.1))
⊢ Nat.rec (motive := fun (x : ℕ) ↦ Part (Option σ)) (Part.some Option.none)
      (fun (n : ℕ) (n_ih : Part (Option σ)) ↦ map (f a.1) (↑(decode n) : Part β))
      (encode.{u_2} (α := Option β) (decode a.2)) =
    Part.some (Option.bind (decode a.2) (f a.1))
have some : ∀ (val : β),
  Nat.rec (motive := fun (x : ℕ) ↦ Part (Option σ)) (Part.some Option.none)
      (fun (n : ℕ) (n_ih : Part (Option σ)) ↦ map (f a.1) (↑(decode n) : Part β)) (encode (Option.some val)) =
    Part.some ((Option.some val).bind (f a.1))
Tactic: cases decode (α := β) a.2
-- 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 : α → β → σ
⊢ (Computable₂.{u_1, 0, u_4} (σ := Option σ) fun (a : α) (n : ℕ) ↦ Option.map (f a) (decode n)) ↔ Computable₂ f
have h : ∀ (x : α) (x_1 : ℕ), Option.map (f x) (decode x_1) = Option.bind (decode x_1) (Option.some ∘ f x)
Tactic: convert! (bind_decode_iff (f := fun a => Option.some ∘ f a)).trans option_some_iff
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ × σ → σ
hf : Computable f
hg : Computable g
hh : Computable₂ h
a : α
⊢ Eq.{u_4 + 1} (α := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) ((↑g : α →. σ) a)
        (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ (↑(h a) : ℕ × σ →. σ) (y, i)) (f a) :
      Part σ)
    ((↑fun (a : α) ↦
            Nat.rec (motive := fun (x : ℕ) ↦ σ) (g a) (fun (y : ℕ) (IH : (fun (x : ℕ) ↦ σ) y) ↦ h a (y, IH)) (f a) :
          α →. σ)
        a :
      Part σ)
have simp : Eq.{u_4 + 1} (α := Part σ)
  (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
      (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ Part.some (h a (y, i))) (f a) :
    Part σ)
  (Part.some (Nat.rec (motive := fun (x : ℕ) ↦ σ) (g a) (fun (y : ℕ) (IH : σ) ↦ h a (y, IH)) (f a)) : Part σ)
Tactic: simp
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ × σ → σ
hf : Computable f
hg : Computable g
hh : Computable₂ h
a : α
⊢ Eq.{u_4 + 1} (α := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
        (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ Part.some (h a (y, i))) (f a) :
      Part σ)
    (Part.some (Nat.rec (motive := fun (x : ℕ) ↦ σ) (g a) (fun (y : ℕ) (IH : σ) ↦ h a (y, IH)) (f a)) : Part σ)
have zero : Eq.{u_4 + 1} (α := Part σ)
  (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
      (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ Part.some (h a (y, i))) 0 :
    Part σ)
  (Part.some (Nat.rec (motive := fun (x : ℕ) ↦ σ) (g a) (fun (y : ℕ) (IH : σ) ↦ h a (y, IH)) 0) : Part σ)
Tactic: induction f a
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ × σ → σ
hf : Computable f
hg : Computable g
hh : Computable₂ h
a : α
zero :
  Eq.{u_4 + 1} (α := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
        (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ Part.some (h a (y, i))) 0 :
      Part σ)
    (Part.some (Nat.rec (motive := fun (x : ℕ) ↦ σ) (g a) (fun (y : ℕ) (IH : σ) ↦ h a (y, IH)) 0) : Part σ)
⊢ Eq.{u_4 + 1} (α := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
        (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ Part.some (h a (y, i))) (f a) :
      Part σ)
    (Part.some (Nat.rec (motive := fun (x : ℕ) ↦ σ) (g a) (fun (y : ℕ) (IH : σ) ↦ h a (y, IH)) (f a)) : Part σ)
have succ : ∀ (n : ℕ),
  Eq.{u_4 + 1} (α := Part σ)
      (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
          (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ Part.some (h a (y, i))) n :
        Part σ)
      (Part.some (Nat.rec (motive := fun (x : ℕ) ↦ σ) (g a) (fun (y : ℕ) (IH : σ) ↦ h a (y, IH)) n) : Part σ) →
    Eq.{u_4 + 1} (α := Part σ)
      (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
          (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ Part.some (h a (y, i))) (n + 1) :
        Part σ)
      (Part.some (Nat.rec (motive := fun (x : ℕ) ↦ σ) (g a) (fun (y : ℕ) (IH : σ) ↦ h a (y, IH)) (n + 1)) : Part σ)
Tactic: induction f a
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
c : α → Bool
f g : α → σ
hc : Computable c
hf : Computable f
hg : Computable g
a : α
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ σ) (encode (c a)) (g a) fun (b : ℕ) ↦ f (a, b).1) = bif c a then f a else g a
have false : (Nat.casesOn (motive := fun (x : ℕ) ↦ σ) (encode false) (g a) fun (b : ℕ) ↦ f (a, b).1) = bif false then f a else g a
Tactic: cases c a
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
c : α → Bool
f g : α → σ
hc : Computable c
hf : Computable f
hg : Computable g
a : α
false :
  (Nat.casesOn (motive := fun (x : ℕ) ↦ σ) (encode Bool.false) (g a) fun (b : ℕ) ↦ f (a, b).1) =
    bif Bool.false then f a else g a
⊢ (Nat.casesOn (motive := fun (x : ℕ) ↦ σ) (encode (c a)) (g a) fun (b : ℕ) ↦ f (a, b).1) = bif c a then f a else g a
have true : (Nat.casesOn (motive := fun (x : ℕ) ↦ σ) (encode true) (g a) fun (b : ℕ) ↦ f (a, b).1) = bif true then f a else g a
Tactic: cases c a
-- 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 σ
o : α → Option β
f : α → σ
g : α → β → σ
ho : Computable o
hf : Computable f
hg : Computable₂ g
a : α
⊢ Eq.{u_4 + 1} (α := Option σ)
    (Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) (encode (o a)) (Option.some (f a)) fun (n : ℕ) ↦
        Option.map (g a) (decode n) :
      Option σ)
    (Option.some (Option.casesOn (motive := fun (x : Option β) ↦ σ) (o a) (f a) (g a)) : Option σ)
have none : Eq.{u_4 + 1} (α := Option σ)
  (Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) (encode.{u_2} (α := Option β) Option.none) (Option.some (f a))
      fun (n : ℕ) ↦ Option.map (g a) (decode n) :
    Option σ)
  (Option.some (Option.casesOn (motive := fun (x : Option β) ↦ σ) Option.none (f a) (g a)) : Option σ)
Tactic: cases o a
-- 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 σ
o : α → Option β
f : α → σ
g : α → β → σ
ho : Computable o
hf : Computable f
hg : Computable₂ g
a : α
none :
  Eq.{u_4 + 1} (α := Option σ)
    (Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) (encode.{u_2} (α := Option β) Option.none) (Option.some (f a))
        fun (n : ℕ) ↦ Option.map (g a) (decode n) :
      Option σ)
    (Option.some (Option.casesOn (motive := fun (x : Option β) ↦ σ) Option.none (f a) (g a)) : Option σ)
⊢ Eq.{u_4 + 1} (α := Option σ)
    (Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) (encode (o a)) (Option.some (f a)) fun (n : ℕ) ↦
        Option.map (g a) (decode n) :
      Option σ)
    (Option.some (Option.casesOn (motive := fun (x : Option β) ↦ σ) (o a) (f a) (g a)) : Option σ)
have some : ∀ (val : β),
  Eq.{u_4 + 1} (α := Option σ)
    (Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) (encode (Option.some val)) (Option.some (f a)) fun (n : ℕ) ↦
        Option.map (g a) (decode n) :
      Option σ)
    (Option.some (Option.casesOn (motive := fun (x : Option β) ↦ σ) (Option.some val) (f a) (g a)) : Option σ)
Tactic: cases o a
-- 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 β
g : α → β → Option σ
hf : Computable f
hg : Computable₂ g
a : α
⊢ Option.casesOn (motive := fun (x : Option β) ↦ Option σ) (f a) Option.none (g a) = (f a).bind (g a)
have none : Option.casesOn (motive := fun (x : Option β) ↦ Option σ) Option.none Option.none (g a) = Option.bind Option.none (g a)
Tactic: cases f a
-- 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 β
g : α → β → Option σ
hf : Computable f
hg : Computable₂ g
a : α
none :
  Option.casesOn (motive := fun (x : Option β) ↦ Option σ) Option.none Option.none (g a) = Option.bind Option.none (g a)
⊢ Option.casesOn (motive := fun (x : Option β) ↦ Option σ) (f a) Option.none (g a) = (f a).bind (g a)
have some : ∀ (val : β),
  Option.casesOn (motive := fun (x : Option β) ↦ Option σ) (Option.some val) Option.none (g a) =
    (Option.some val).bind (g a)
Tactic: cases f a
-- 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 β
g : α → β → σ
hf : Computable f
hg : Computable₂ g
⊢ Computable.{u_1, u_4} (σ := Option σ) fun (a : α) ↦ Option.map (g a) (f a)
have h : ∀ (x : α), Option.map (g x) (f x) = (f x).bind fun (b : β) ↦ Option.some (g x b)
Tactic: convert! option_bind hf (option_some.comp₂ hg)
-- Lean 4 proof step from Mathlib.Computability.Partrec (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → Option β
g : α → β
hf : Computable f
hg : Computable g
a : α
⊢ (Option.casesOn (motive := fun (x : Option β) ↦ β) (f a) (g a) fun (b : β) ↦ b) = (f a).getD (g a)
have none : (Option.casesOn (motive := fun (x : Option β) ↦ β) Option.none (g a) fun (b : β) ↦ b) = Option.getD Option.none (g a)
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 β
g : α → β
hf : Computable f
hg : Computable g
a : α
none :
  (Option.casesOn (motive := fun (x : Option β) ↦ β) Option.none (g a) fun (b : β) ↦ b) = Option.getD Option.none (g a)
⊢ (Option.casesOn (motive := fun (x : Option β) ↦ β) (f a) (g a) fun (b : β) ↦ b) = (f a).getD (g a)
have some : ∀ (val : β),
  (Option.casesOn (motive := fun (x : Option β) ↦ β) (Option.some val) (g a) fun (b : β) ↦ b) =
    (Option.some val).getD (g a)
Tactic: cases f a
-- Lean 4 proof step from Mathlib.Computability.Partrec (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 : Computable f
hg : Computable₂ g
hh : Computable₂ 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)) =
    Option.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)) =
    Option.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.Partrec (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 : Computable f
hg : Computable₂ g
hh : Computable₂ 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)) =
      Option.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)) =
    Option.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)) =
    Option.some (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ σ) (Sum.inr c) (g a) (h a))
Tactic: rcases f a with b | c