awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.Partrec
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)))
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)))
⊢ 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:
cases decode (α := β) n.unpair.2

Premises used: Nat.unpair, Encodable.decode, Prod.snd
-- Module: Mathlib.Computability.Partrec
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 β) 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:
simp
-- Module: Mathlib.Computability.Partrec
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 : α
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:
simp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → β → Option σ
hf : Computable₂ f
⊢ 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₂)
-- Module: Mathlib.Computability.Partrec
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)

Tactic:
this.of_eq fun a => ?_

Premises used: Computable₂, Partrec.of_eq, Computable
-- Module: Mathlib.Computability.Partrec
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 β)
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 σ))
⊢ Computable₂.{u_1, 0, u_4} (σ := Option σ) fun (a : α) (n : ℕ) ↦ Option.bind (decode n) (f a)

Tactic:
refine this.of_eq fun a => ?_

Premises used: Partrec.of_eq
-- Module: Mathlib.Computability.Partrec
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 : α × ℕ
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))
⊢ 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:
simp
-- Module: Mathlib.Computability.Partrec
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))
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))
⊢ 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:
cases decode (α := β) a.2

Premises used: Encodable.decode, Prod.snd
-- Module: Mathlib.Computability.Partrec
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 β) Option.none) =
    Part.some (Option.bind Option.none (f a.1))

Tactic:
simp [encodek]

Premises used: Encodable.encodek
-- Module: Mathlib.Computability.Partrec
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 : α × ℕ
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:
simp [encodek]

Premises used: Encodable.encodek
-- Module: Mathlib.Computability.Partrec
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.bind (decode n) (Option.some ∘ f a)) ↔
    Computable (σ := σ) fun (p : α × β) ↦ f p.1 p.2

Tactic:
(bind_decode_iff (f := fun a => Option.some ∘ f a)).trans option_some_iff

Premises used: Computable.bind_decode_iff, Computable.option_some_iff, Iff.trans
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → β → σ
h : ∀ (x : α) (x_1 : ℕ), Option.map (f x) (decode x_1) = Option.bind (decode x_1) (Option.some ∘ f x)
⊢ (Computable₂.{u_1, 0, u_4} (σ := Option σ) fun (a : α) (n : ℕ) ↦ Option.map (f a) (decode n)) ↔ Computable₂ f

Tactic:
convert! (bind_decode_iff (f := fun a => Option.some ∘ f a)).trans option_some_iff

Premises used: Computable.bind_decode_iff, Computable.option_some_iff, Iff.trans
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → β → σ
x : α
x_1 : ℕ
⊢ Option.map (f x) (decode x_1) = Option.bind (decode x_1) (Option.some ∘ f x)

Tactic:
apply Option.map_eq_bind

Premises used: Option.map_eq_bind
-- Module: Mathlib.Computability.Partrec
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 : α
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 σ)
⊢ 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 σ)

Tactic:
simp
-- Module: Mathlib.Computability.Partrec
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 σ)
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 σ)
⊢ 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:
induction f a
-- Module: Mathlib.Computability.Partrec
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))) 0 :
      Part σ)
    (Part.some (Nat.rec (motive := fun (x : ℕ) ↦ σ) (g a) (fun (y : ℕ) (IH : σ) ↦ h a (y, IH)) 0) : Part σ)

Tactic:
simp [*]
-- Module: Mathlib.Computability.Partrec
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 : α
n : ℕ
h_1 :
  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:
simp [*]
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ → σ
hf : Computable f
hg : Computable g
hh : Computable₂ h
⊢ Computable.{u_1, u_4} (σ := σ) fun (a : α) ↦ Nat.casesOn (motive := fun (x : ℕ) ↦ σ) (f a) (g a) (h a)

Tactic:
nat_rec hf hg (hh.comp fst <| fst.comp snd).to₂

Premises used: Computable.snd, Computable₂.comp, Computable.comp, Computable.nat_rec, Computable.fst, Computable.to₂
-- Module: Mathlib.Computability.Partrec
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
true :
  (Nat.casesOn (motive := fun (x : ℕ) ↦ σ) (encode Bool.true) (g a) fun (b : ℕ) ↦ f (a, b).1) =
    bif Bool.true 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

Tactic:
cases c a
-- Module: Mathlib.Computability.Partrec
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 false) (g a) fun (b : ℕ) ↦ f (a, b).1) = bif false then f a else g a

Tactic:
rfl
-- Module: Mathlib.Computability.Partrec
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 true) (g a) fun (b : ℕ) ↦ f (a, b).1) = bif true then f a else g a

Tactic:
rfl
-- Module: Mathlib.Computability.Partrec
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 σ)
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 σ)
⊢ 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 σ)

Tactic:
cases o a
-- Module: Mathlib.Computability.Partrec
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.{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:
simp [encodek]

Premises used: Encodable.encodek
-- Module: Mathlib.Computability.Partrec
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 : α
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:
simp [encodek]

Premises used: Encodable.encodek
-- Module: Mathlib.Computability.Partrec
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)
some :
  ∀ (val : β),
    Option.casesOn (motive := fun (x : Option β) ↦ Option σ) (Option.some val) Option.none (g a) =
      (Option.some val).bind (g a)
⊢ Option.casesOn (motive := fun (x : Option β) ↦ Option σ) (f a) Option.none (g a) = (f a).bind (g a)

Tactic:
cases f a
-- Module: Mathlib.Computability.Partrec
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 σ) Option.none Option.none (g a) = Option.bind Option.none (g a)

Tactic:
rfl
-- Module: Mathlib.Computability.Partrec
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 : α
val : β
⊢ Option.casesOn (motive := fun (x : Option β) ↦ Option σ) (Option.some val) Option.none (g a) =
    (Option.some val).bind (g a)

Tactic:
rfl
-- Module: Mathlib.Computability.Partrec
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 : α) ↦ (f a).bind fun (b : β) ↦ Option.some (g a b)

Tactic:
option_bind hf (option_some.comp₂ hg)

Premises used: Computable.option_some, Computable.option_bind, Computable.comp₂
-- Module: Mathlib.Computability.Partrec
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
h : ∀ (x : α), Option.map (g x) (f x) = (f x).bind fun (b : β) ↦ Option.some (g x b)
⊢ Computable.{u_1, u_4} (σ := Option σ) fun (a : α) ↦ Option.map (g a) (f a)

Tactic:
convert! option_bind hf (option_some.comp₂ hg)

Premises used: Computable.option_some, Computable.option_bind, Computable.comp₂
-- Module: Mathlib.Computability.Partrec
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
x : α
⊢ Option.map (g x) (f x) = (f x).bind fun (b : β) ↦ Option.some (g x b)

Tactic:
apply Option.map_eq_bind

Premises used: Option.map_eq_bind
-- Module: Mathlib.Computability.Partrec
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)
some :
  ∀ (val : β),
    (Option.casesOn (motive := fun (x : Option β) ↦ β) (Option.some val) (g a) fun (b : β) ↦ b) =
      (Option.some val).getD (g a)
⊢ (Option.casesOn (motive := fun (x : Option β) ↦ β) (f a) (g a) fun (b : β) ↦ b) = (f a).getD (g a)

Tactic:
cases f a
-- Module: Mathlib.Computability.Partrec
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 β) ↦ β) Option.none (g a) fun (b : β) ↦ b) = Option.getD Option.none (g a)

Tactic:
rfl
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → Option β
g : α → β
hf : Computable f
hg : Computable g
a : α
val : β
⊢ (Option.casesOn (motive := fun (x : Option β) ↦ β) (Option.some val) (g a) fun (b : β) ↦ b) =
    (Option.some val).getD (g a)

Tactic:
rfl
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → β
p : β → Prop
inst_2 : DecidablePred p
h : ∀ (a : α), p (f a)
hp : PrimrecPred p
hf : Computable f
⊢ Computable.{u_1, u_2} (σ := Subtype p) fun (a : α) ↦ Subtype.mk (p := p) (f a) ⋯

Tactic:
hf

Premises used: Part.some, PFun.lift, Computable, Partrec, Part.map, Encodable.encodeSubtype
-- Module: Mathlib.Computability.Partrec
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))
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))
⊢ (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))

Tactic:
rcases f a with b | c