mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case some.zero
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : 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 0)).bind fun n_1 ↦
      Nat.rec (Part.map encode (g a))
        (fun y IH ↦ do
          let i ← IH
          (↑(decode (Nat.pair n (Nat.pair y i)))).bind fun a ↦ Part.map encode (h a.1 a.2))
        n_1) =
    Part.map encode (Nat.rec (g a) (fun y IH ↦ IH.bind fun i ↦ h a (y, i)) 0)

pp: case some.succ
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
n✝ : ℕ
a✝ :
  ((Part.map encode (Part.some n✝)).bind fun n_1 ↦
      Nat.rec (Part.map encode (g a))
        (fun y IH ↦ do
          let i ← IH
          (↑(decode (Nat.pair n (Nat.pair y i)))).bind fun a ↦ Part.map encode (h a.1 a.2))
        n_1) =
    Part.map encode (Nat.rec (g a) (fun y IH ↦ IH.bind fun i ↦ h a (y, i)) n✝)
⊢ ((Part.map encode (Part.some (n✝ + 1))).bind fun n_1 ↦
      Nat.rec (Part.map encode (g a))
        (fun y IH ↦ do
          let i ← IH
          (↑(decode (Nat.pair n (Nat.pair y i)))).bind fun a ↦ Part.map encode (h a.1 a.2))
        n_1) =
    Part.map encode (Nat.rec (g a) (fun y IH ↦ IH.bind fun i ↦ h a (y, i)) (n✝ + 1))

Tactic:
<;>

Goal state after:
case some.zero
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : 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 0)).bind fun n_1 ↦
      Nat.rec (Part.map encode (g a))
        (fun y IH ↦ do
          let i ← IH
          (↑(decode (Nat.pair n (Nat.pair y i)))).bind fun a ↦ Part.map encode (h a.1 a.2))
        n_1) =
    Part.map encode (Nat.rec (g a) (fun y IH ↦ IH.bind fun i ↦ h a (y, i)) 0)

case some.succ
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
n✝ : ℕ
a✝ :
  ((Part.map encode (Part.some n✝)).bind fun n_1 ↦
      Nat.rec (Part.map encode (g a))
        (fun y IH ↦ do
          let i ← IH
          (↑(decode (Nat.pair n (Nat.pair y i)))).bind fun a ↦ Part.map encode (h a.1 a.2))
        n_1) =
    Part.map encode (Nat.rec (g a) (fun y IH ↦ IH.bind fun i ↦ h a (y, i)) n✝)
⊢ ((Part.map encode (Part.some (n✝ + 1))).bind fun n_1 ↦
      Nat.rec (Part.map encode (g a))
        (fun y IH ↦ do
          let i ← IH
          (↑(decode (Nat.pair n (Nat.pair y i)))).bind fun a ↦ Part.map encode (h a.1 a.2))
        n_1) =
    Part.map encode (Nat.rec (g a) (fun y IH ↦ IH.bind fun i ↦ h a (y, i)) (n✝ + 1))
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β →. σ
g : α → β
hf : Partrec f
hg : Computable g
n : ℕ
e : decode n = Option.none
⊢ (((↑Option.none).bind fun a ↦ Part.some (encode (g a))).bind fun n ↦
      (↑(decode n)).bind fun a ↦ Part.map encode (f a)) =
    (↑Option.none).bind fun a ↦ Part.map encode (f (g a))

pp: case some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β →. σ
g : α → β
hf : Partrec f
hg : Computable g
n : ℕ
a : α
e : decode n = Option.some a
⊢ (((↑(Option.some a)).bind fun a ↦ Part.some (encode (g a))).bind fun n ↦
      (↑(decode n)).bind fun a ↦ Part.map encode (f a)) =
    (↑(Option.some a)).bind fun a ↦ Part.map encode (f (g a))

Tactic:
<;>

Goal state after:
case none
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β →. σ
g : α → β
hf : Partrec f
hg : Computable g
n : ℕ
e : decode n = Option.none
⊢ (((↑Option.none).bind fun a ↦ Part.some (encode (g a))).bind fun n ↦
      (↑(decode n)).bind fun a ↦ Part.map encode (f a)) =
    (↑Option.none).bind fun a ↦ Part.map encode (f (g a))

case some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β →. σ
g : α → β
hf : Partrec f
hg : Computable g
n : ℕ
a : α
e : decode n = Option.some a
⊢ (((↑(Option.some a)).bind fun a ↦ Part.some (encode (g a))).bind fun n ↦
      (↑(decode n)).bind fun a ↦ Part.map encode (f a)) =
    (↑(Option.some a)).bind fun a ↦ Part.map encode (f (g a))
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case none
α : Type u_1
inst✝ : Primcodable α
p : α → ℕ →. Bool
hp : Partrec₂ p
n : ℕ
e : decode n = Option.none
⊢ (Nat.rfind fun n_1 ↦
      (fun m ↦ decide (m = 0)) <$>
        (↑(decode (Nat.pair n n_1))).bind fun a ↦
          Part.map encode ((fun a ↦ Part.map (fun b ↦ bif (a, b).2 then 0 else 1) (p a.1 a.2)) a)) =
    (↑Option.none).bind fun a ↦ Part.map encode ((fun a ↦ Nat.rfind (p a)) a)

pp: case some
α : Type u_1
inst✝ : Primcodable α
p : α → ℕ →. Bool
hp : Partrec₂ p
n : ℕ
val✝ : α
e : decode n = Option.some val✝
⊢ (Nat.rfind fun n_1 ↦
      (fun m ↦ decide (m = 0)) <$>
        (↑(decode (Nat.pair n n_1))).bind fun a ↦
          Part.map encode ((fun a ↦ Part.map (fun b ↦ bif (a, b).2 then 0 else 1) (p a.1 a.2)) a)) =
    (↑(Option.some val✝)).bind fun a ↦ Part.map encode ((fun a ↦ Nat.rfind (p a)) a)

Tactic:
<;>

Goal state after:
case none
α : Type u_1
inst✝ : Primcodable α
p : α → ℕ →. Bool
hp : Partrec₂ p
n : ℕ
e : decode n = Option.none
⊢ (Nat.rfind fun n_1 ↦
      (fun m ↦ decide (m = 0)) <$>
        (↑(decode (Nat.pair n n_1))).bind fun a ↦
          Part.map encode ((fun a ↦ Part.map (fun b ↦ bif (a, b).2 then 0 else 1) (p a.1 a.2)) a)) =
    (↑Option.none).bind fun a ↦ Part.map encode ((fun a ↦ Nat.rfind (p a)) a)

case some
α : Type u_1
inst✝ : Primcodable α
p : α → ℕ →. Bool
hp : Partrec₂ p
n : ℕ
val✝ : α
e : decode n = Option.some val✝
⊢ (Nat.rfind fun n_1 ↦
      (fun m ↦ decide (m = 0)) <$>
        (↑(decode (Nat.pair n n_1))).bind fun a ↦
          Part.map encode ((fun a ↦ Part.map (fun b ↦ bif (a, b).2 then 0 else 1) (p a.1 a.2)) a)) =
    (↑(Option.some val✝)).bind fun a ↦ Part.map encode ((fun a ↦ Nat.rfind (p a)) a)
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case zero
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ Nat.rec (Part.some (g a)) (fun n n_ih ↦ h a n) (n + 1)
⊢ (Nat.rec (Part.some (g a)) (fun y IH ↦ IH.bind fun x ↦ h a n) 0).Dom

pp: case succ
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ Nat.rec (Part.some (g a)) (fun n n_ih ↦ h a n) (n + 1)
n✝ : ℕ
a✝ : (Nat.rec (Part.some (g a)) (fun y IH ↦ IH.bind fun x ↦ h a n) n✝).Dom
⊢ (Nat.rec (Part.some (g a)) (fun y IH ↦ IH.bind fun x ↦ h a n) (n✝ + 1)).Dom

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ Nat.rec (Part.some (g a)) (fun n n_ih ↦ h a n) (n + 1)
⊢ (Nat.rec (Part.some (g a)) (fun y IH ↦ IH.bind fun x ↦ h a n) 0).Dom

case succ
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ Nat.rec (Part.some (g a)) (fun n n_ih ↦ h a n) (n + 1)
n✝ : ℕ
a✝ : (Nat.rec (Part.some (g a)) (fun y IH ↦ IH.bind fun x ↦ h a n) n✝).Dom
⊢ (Nat.rec (Part.some (g a)) (fun y IH ↦ IH.bind fun x ↦ h a n) (n✝ + 1)).Dom
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ fun a n ↦ (decode n).bind (f a)
n : ℕ
⊢ ((↑(Option.none.bind fun a ↦ Option.some (a, (Nat.unpair n).2))).bind fun a ↦
      (↑(encode (decode a.2)).ppred).bind fun y ↦ Part.some (encode ((decode a.2).bind fun a_1 ↦ f a.1 a_1))) =
    (↑(Option.none.bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2))).bind fun a ↦
      Part.some (encode (f a.1 a.2))

pp: case some
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ fun a n ↦ (decode n).bind (f a)
n : ℕ
val✝ : α
⊢ ((↑((Option.some val✝).bind fun a ↦ Option.some (a, (Nat.unpair n).2))).bind fun a ↦
      (↑(encode (decode a.2)).ppred).bind fun y ↦ Part.some (encode ((decode a.2).bind fun a_1 ↦ f a.1 a_1))) =
    (↑((Option.some val✝).bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2))).bind fun a ↦
      Part.some (encode (f a.1 a.2))

Tactic:
<;>

Goal state after:
case none
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ fun a n ↦ (decode n).bind (f a)
n : ℕ
⊢ ((↑(Option.none.bind fun a ↦ Option.some (a, (Nat.unpair n).2))).bind fun a ↦
      (↑(encode (decode a.2)).ppred).bind fun y ↦ Part.some (encode ((decode a.2).bind fun a_1 ↦ f a.1 a_1))) =
    (↑(Option.none.bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2))).bind fun a ↦
      Part.some (encode (f a.1 a.2))

case some
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ fun a n ↦ (decode n).bind (f a)
n : ℕ
val✝ : α
⊢ ((↑((Option.some val✝).bind fun a ↦ Option.some (a, (Nat.unpair n).2))).bind fun a ↦
      (↑(encode (decode a.2)).ppred).bind fun y ↦ Part.some (encode ((decode a.2).bind fun a_1 ↦ f a.1 a_1))) =
    (↑((Option.some val✝).bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2))).bind fun a ↦
      Part.some (encode (f a.1 a.2))
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case some.none
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ fun a n ↦ (decode n).bind (f a)
n : ℕ
val✝ : α
⊢ ((↑(encode Option.none).ppred).bind fun y ↦ Part.some (encode (Option.none.bind fun a ↦ f val✝ a))) =
    (↑(Option.map (Prod.mk val✝) Option.none)).bind fun a ↦ Part.some (encode (f a.1 a.2))

pp: case some.some
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ fun a n ↦ (decode n).bind (f a)
n : ℕ
val✝¹ : α
val✝ : β
⊢ ((↑(encode (Option.some val✝)).ppred).bind fun y ↦ Part.some (encode ((Option.some val✝).bind fun a ↦ f val✝¹ a))) =
    (↑(Option.map (Prod.mk val✝¹) (Option.some val✝))).bind fun a ↦ Part.some (encode (f a.1 a.2))

Tactic:
<;>

Goal state after:
case some.none
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ fun a n ↦ (decode n).bind (f a)
n : ℕ
val✝ : α
⊢ ((↑(encode Option.none).ppred).bind fun y ↦ Part.some (encode (Option.none.bind fun a ↦ f val✝ a))) =
    (↑(Option.map (Prod.mk val✝) Option.none)).bind fun a ↦ Part.some (encode (f a.1 a.2))

case some.some
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ fun a n ↦ (decode n).bind (f a)
n : ℕ
val✝¹ : α
val✝ : β
⊢ ((↑(encode (Option.some val✝)).ppred).bind fun y ↦ Part.some (encode ((Option.some val✝).bind fun a ↦ f val✝¹ a))) =
    (↑(Option.map (Prod.mk val✝¹) (Option.some val✝))).bind fun a ↦ Part.some (encode (f a.1 a.2))
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ f
this : Partrec fun a ↦ Nat.casesOn (encode (decode a.2)) (Part.some Option.none) fun n ↦ map (f a.1) ↑(decode n)
a : α × ℕ
⊢ Nat.rec (Part.some Option.none) (fun n n_ih ↦ map (f a.1) ↑(decode n)) (encode Option.none) =
    Part.some (Option.none.bind (f a.1))

pp: case some
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ f
this : Partrec fun a ↦ Nat.casesOn (encode (decode a.2)) (Part.some Option.none) fun n ↦ map (f a.1) ↑(decode n)
a : α × ℕ
val✝ : β
⊢ Nat.rec (Part.some Option.none) (fun n n_ih ↦ map (f a.1) ↑(decode n)) (encode (Option.some val✝)) =
    Part.some ((Option.some val✝).bind (f a.1))

Tactic:
<;>

Goal state after:
case none
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ f
this : Partrec fun a ↦ Nat.casesOn (encode (decode a.2)) (Part.some Option.none) fun n ↦ map (f a.1) ↑(decode n)
a : α × ℕ
⊢ Nat.rec (Part.some Option.none) (fun n n_ih ↦ map (f a.1) ↑(decode n)) (encode Option.none) =
    Part.some (Option.none.bind (f a.1))

case some
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
hf : Computable₂ f
this : Partrec fun a ↦ Nat.casesOn (encode (decode a.2)) (Part.some Option.none) fun n ↦ map (f a.1) ↑(decode n)
a : α × ℕ
val✝ : β
⊢ Nat.rec (Part.some Option.none) (fun n n_ih ↦ map (f a.1) ↑(decode n)) (encode (Option.some val✝)) =
    Part.some ((Option.some val✝).bind (f a.1))
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case zero
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ × σ → σ
hf : Computable f
hg : Computable g
hh : Computable₂ h
a : α
⊢ Nat.rec (Part.some (g a)) (fun y IH ↦ IH.bind fun i ↦ Part.some (h a (y, i))) 0 =
    Part.some (Nat.rec (g a) (fun y IH ↦ h a (y, IH)) 0)

pp: case succ
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ × σ → σ
hf : Computable f
hg : Computable g
hh : Computable₂ h
a : α
n✝ : ℕ
a✝ :
  Nat.rec (Part.some (g a)) (fun y IH ↦ IH.bind fun i ↦ Part.some (h a (y, i))) n✝ =
    Part.some (Nat.rec (g a) (fun y IH ↦ h a (y, IH)) n✝)
⊢ Nat.rec (Part.some (g a)) (fun y IH ↦ IH.bind fun i ↦ Part.some (h a (y, i))) (n✝ + 1) =
    Part.some (Nat.rec (g a) (fun y IH ↦ h a (y, IH)) (n✝ + 1))

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ × σ → σ
hf : Computable f
hg : Computable g
hh : Computable₂ h
a : α
⊢ Nat.rec (Part.some (g a)) (fun y IH ↦ IH.bind fun i ↦ Part.some (h a (y, i))) 0 =
    Part.some (Nat.rec (g a) (fun y IH ↦ h a (y, IH)) 0)

case succ
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ × σ → σ
hf : Computable f
hg : Computable g
hh : Computable₂ h
a : α
n✝ : ℕ
a✝ :
  Nat.rec (Part.some (g a)) (fun y IH ↦ IH.bind fun i ↦ Part.some (h a (y, i))) n✝ =
    Part.some (Nat.rec (g a) (fun y IH ↦ h a (y, IH)) n✝)
⊢ Nat.rec (Part.some (g a)) (fun y IH ↦ IH.bind fun i ↦ Part.some (h a (y, i))) (n✝ + 1) =
    Part.some (Nat.rec (g a) (fun y IH ↦ h a (y, IH)) (n✝ + 1))
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case false
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
c : α → Bool
f g : α → σ
hc : Computable c
hf : Computable f
hg : Computable g
a : α
⊢ (Nat.casesOn (encode false) (g a) fun b ↦ f (a, b).1) = bif false then f a else g a

pp: case true
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
c : α → Bool
f g : α → σ
hc : Computable c
hf : Computable f
hg : Computable g
a : α
⊢ (Nat.casesOn (encode true) (g a) fun b ↦ f (a, b).1) = bif true then f a else g a

Tactic:
<;>

Goal state after:
case false
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
c : α → Bool
f g : α → σ
hc : Computable c
hf : Computable f
hg : Computable g
a : α
⊢ (Nat.casesOn (encode false) (g a) fun b ↦ f (a, b).1) = bif false then f a else g a

case true
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
c : α → Bool
f g : α → σ
hc : Computable c
hf : Computable f
hg : Computable g
a : α
⊢ (Nat.casesOn (encode true) (g a) fun b ↦ f (a, b).1) = bif true then f a else g a
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β → σ
ho : Computable o
hf : Computable f
hg : Computable₂ g
a : α
⊢ (Nat.casesOn (encode Option.none) (Option.some (f a)) fun n ↦ Option.map (g a) (decode n)) =
    Option.some (Option.casesOn Option.none (f a) (g a))

pp: case some
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β → σ
ho : Computable o
hf : Computable f
hg : Computable₂ g
a : α
val✝ : β
⊢ (Nat.casesOn (encode (Option.some val✝)) (Option.some (f a)) fun n ↦ Option.map (g a) (decode n)) =
    Option.some (Option.casesOn (Option.some val✝) (f a) (g a))

Tactic:
<;>

Goal state after:
case none
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β → σ
ho : Computable o
hf : Computable f
hg : Computable₂ g
a : α
⊢ (Nat.casesOn (encode Option.none) (Option.some (f a)) fun n ↦ Option.map (g a) (decode n)) =
    Option.some (Option.casesOn Option.none (f a) (g a))

case some
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β → σ
ho : Computable o
hf : Computable f
hg : Computable₂ g
a : α
val✝ : β
⊢ (Nat.casesOn (encode (Option.some val✝)) (Option.some (f a)) fun n ↦ Option.map (g a) (decode n)) =
    Option.some (Option.casesOn (Option.some val✝) (f a) (g a))
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → Option β
g : α → β → Option σ
hf : Computable f
hg : Computable₂ g
a : α
⊢ Option.casesOn Option.none Option.none (g a) = Option.none.bind (g a)

pp: case some
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → Option β
g : α → β → Option σ
hf : Computable f
hg : Computable₂ g
a : α
val✝ : β
⊢ Option.casesOn (Option.some val✝) Option.none (g a) = (Option.some val✝).bind (g a)

Tactic:
<;>

Goal state after:
case none
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → Option β
g : α → β → Option σ
hf : Computable f
hg : Computable₂ g
a : α
⊢ Option.casesOn Option.none Option.none (g a) = Option.none.bind (g a)

case some
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → Option β
g : α → β → Option σ
hf : Computable f
hg : Computable₂ g
a : α
val✝ : β
⊢ Option.casesOn (Option.some val✝) Option.none (g a) = (Option.some val✝).bind (g a)
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
g : α → β
hf : Computable f
hg : Computable g
a : α
⊢ (Option.casesOn Option.none (g a) fun b ↦ b) = Option.none.getD (g a)

pp: case some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
g : α → β
hf : Computable f
hg : Computable g
a : α
val✝ : β
⊢ (Option.casesOn (Option.some val✝) (g a) fun b ↦ b) = (Option.some val✝).getD (g a)

Tactic:
<;>

Goal state after:
case none
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
g : α → β
hf : Computable f
hg : Computable g
a : α
⊢ (Option.casesOn Option.none (g a) fun b ↦ b) = Option.none.getD (g a)

case some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
g : α → β
hf : Computable f
hg : Computable g
a : α
val✝ : β
⊢ (Option.casesOn (Option.some val✝) (g a) fun b ↦ b) = (Option.some val✝).getD (g a)
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ → σ
hf : Computable f
hg : Computable₂ g
hh : Computable₂ h
a : α
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 (Sum.inl b) (g a) (h a))

pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ → σ
hf : Computable f
hg : Computable₂ g
hh : Computable₂ h
a : α
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 (Sum.inr c) (g a) (h a))

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ → σ
hf : Computable f
hg : Computable₂ g
hh : Computable₂ h
a : α
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 (Sum.inl b) (g a) (h a))

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ → σ
hf : Computable f
hg : Computable₂ g
hh : Computable₂ h
a : α
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 (Sum.inr c) (g a) (h a))
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β →. σ
ho : Computable o
hf : Computable f
hg : Partrec₂ g
this : Partrec fun a ↦ Nat.casesOn (encode (o a)) (Part.some (f a)) fun n ↦ (↑(decode n)).bind (g a)
a : α
⊢ (Nat.casesOn (encode Option.none) (Part.some (f a)) fun n ↦ (↑(decode n)).bind (g a)) =
    Option.casesOn Option.none (Part.some (f a)) (g a)

pp: case some
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β →. σ
ho : Computable o
hf : Computable f
hg : Partrec₂ g
this : Partrec fun a ↦ Nat.casesOn (encode (o a)) (Part.some (f a)) fun n ↦ (↑(decode n)).bind (g a)
a : α
b : β
⊢ (Nat.casesOn (encode (Option.some b)) (Part.some (f a)) fun n ↦ (↑(decode n)).bind (g a)) =
    Option.casesOn (Option.some b) (Part.some (f a)) (g a)

Tactic:
<;>

Goal state after:
case none
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β →. σ
ho : Computable o
hf : Computable f
hg : Partrec₂ g
this : Partrec fun a ↦ Nat.casesOn (encode (o a)) (Part.some (f a)) fun n ↦ (↑(decode n)).bind (g a)
a : α
⊢ (Nat.casesOn (encode Option.none) (Part.some (f a)) fun n ↦ (↑(decode n)).bind (g a)) =
    Option.casesOn Option.none (Part.some (f a)) (g a)

case some
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β →. σ
ho : Computable o
hf : Computable f
hg : Partrec₂ g
this : Partrec fun a ↦ Nat.casesOn (encode (o a)) (Part.some (f a)) fun n ↦ (↑(decode n)).bind (g a)
a : α
b : β
⊢ (Nat.casesOn (encode (Option.some b)) (Part.some (f a)) fun n ↦ (↑(decode n)).bind (g a)) =
    Option.casesOn (Option.some b) (Part.some (f a)) (g a)