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

Goal state before:
pp: case none
α : Type u_1
inst✝ : Primcodable α
n : ℕ
⊢ (Nat.casesOn (encode none) 0 fun n ↦ n.succ.succ) = encode (Option.map some none)

pp: case some
α : Type u_1
inst✝ : Primcodable α
n : ℕ
val✝ : α
⊢ (Nat.casesOn (encode (some val✝)) 0 fun n ↦ n.succ.succ) = encode (Option.map some (some val✝))

Tactic:
<;>

Goal state after:
case none
α : Type u_1
inst✝ : Primcodable α
n : ℕ
⊢ (Nat.casesOn (encode none) 0 fun n ↦ n.succ.succ) = encode (Option.map some none)

case some
α : Type u_1
inst✝ : Primcodable α
n : ℕ
val✝ : α
⊢ (Nat.casesOn (encode (some val✝)) 0 fun n ↦ n.succ.succ) = encode (Option.map some (some val✝))
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case none
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
x : σ
n : ℕ
⊢ (Nat.casesOn (encode none) 0 fun x_1 ↦ (encode x).succ) = encode (Option.map (fun x_1 ↦ x) none)

pp: case some
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
x : σ
n : ℕ
val✝ : α
⊢ (Nat.casesOn (encode (some val✝)) 0 fun x_1 ↦ (encode x).succ) = encode (Option.map (fun x_1 ↦ x) (some val✝))

Tactic:
<;>

Goal state after:
case none
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
x : σ
n : ℕ
⊢ (Nat.casesOn (encode none) 0 fun x_1 ↦ (encode x).succ) = encode (Option.map (fun x_1 ↦ x) none)

case some
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
x : σ
n : ℕ
val✝ : α
⊢ (Nat.casesOn (encode (some val✝)) 0 fun x_1 ↦ (encode x).succ) = encode (Option.map (fun x_1 ↦ x) (some val✝))
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
g : α → β
hf : Primrec f
hg : Primrec g
n : ℕ
⊢ (Nat.casesOn (encode none) 0 fun n ↦ encode (Option.map f (decode (encode (Option.map g (decode n))).pred))) =
    encode (Option.map (fun a ↦ f (g a)) none)

pp: case some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
g : α → β
hf : Primrec f
hg : Primrec g
n : ℕ
val✝ : α
⊢ (Nat.casesOn (encode (some val✝)) 0 fun n ↦ encode (Option.map f (decode (encode (Option.map g (decode n))).pred))) =
    encode (Option.map (fun a ↦ f (g a)) (some val✝))

Tactic:
<;>

Goal state after:
case none
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
g : α → β
hf : Primrec f
hg : Primrec g
n : ℕ
⊢ (Nat.casesOn (encode none) 0 fun n ↦ encode (Option.map f (decode (encode (Option.map g (decode n))).pred))) =
    encode (Option.map (fun a ↦ f (g a)) none)

case some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
g : α → β
hf : Primrec f
hg : Primrec g
n : ℕ
val✝ : α
⊢ (Nat.casesOn (encode (some val✝)) 0 fun n ↦ encode (Option.map f (decode (encode (Option.map g (decode n))).pred))) =
    encode (Option.map (fun a ↦ f (g a)) (some val✝))
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case none
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → σ
h : Primrec fun a ↦ encode (f a)
n : ℕ
⊢ encode (Option.map (fun a ↦ encode (f a)) none) = encode (Option.map f none)

pp: case some
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → σ
h : Primrec fun a ↦ encode (f a)
n : ℕ
val✝ : α
⊢ encode (Option.map (fun a ↦ encode (f a)) (some val✝)) = encode (Option.map f (some val✝))

Tactic:
<;>

Goal state after:
case none
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → σ
h : Primrec fun a ↦ encode (f a)
n : ℕ
⊢ encode (Option.map (fun a ↦ encode (f a)) none) = encode (Option.map f none)

case some
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → σ
h : Primrec fun a ↦ encode (f a)
n : ℕ
val✝ : α
⊢ encode (Option.map (fun a ↦ encode (f a)) (some val✝)) = encode (Option.map f (some val✝))
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case some.none
α : Type ?u.4
β : Type ?u.6
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n n_ih ↦ Nat.rec 0 (fun n_1 n_ih ↦ (Nat.pair n n_1).succ) (encode none)) (encode (some val✝)) =
    encode ((some val✝).bind fun a ↦ Option.map (Prod.mk a) none)

pp: case some.some
α : Type ?u.4
β : Type ?u.6
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝¹ : α
val✝ : β
⊢ Nat.rec 0 (fun n n_ih ↦ Nat.rec 0 (fun n_1 n_ih ↦ (Nat.pair n n_1).succ) (encode (some val✝))) (encode (some val✝¹)) =
    encode ((some val✝¹).bind fun a ↦ Option.map (Prod.mk a) (some val✝))

Tactic:
<;>

Goal state after:
case some.none
α : Type ?u.4
β : Type ?u.6
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n n_ih ↦ Nat.rec 0 (fun n_1 n_ih ↦ (Nat.pair n n_1).succ) (encode none)) (encode (some val✝)) =
    encode ((some val✝).bind fun a ↦ Option.map (Prod.mk a) none)

case some.some
α : Type ?u.4
β : Type ?u.6
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝¹ : α
val✝ : β
⊢ Nat.rec 0 (fun n n_ih ↦ Nat.rec 0 (fun n_1 n_ih ↦ (Nat.pair n n_1).succ) (encode (some val✝))) (encode (some val✝¹)) =
    encode ((some val✝¹).bind fun a ↦ Option.map (Prod.mk a) (some val✝))
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case none
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.rec 0 (fun n_1 n_ih ↦ Nat.rec 0 (fun n n_ih ↦ n_1.succ) (encode (decode (Nat.unpair n).2))) (encode none) =
    encode (Option.map Prod.fst (none.bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)))

pp: case some
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n_1 n_ih ↦ Nat.rec 0 (fun n n_ih ↦ n_1.succ) (encode (decode (Nat.unpair n).2))) (encode (some val✝)) =
    encode (Option.map Prod.fst ((some val✝).bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)))

Tactic:
<;>

Goal state after:
case none
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.rec 0 (fun n_1 n_ih ↦ Nat.rec 0 (fun n n_ih ↦ n_1.succ) (encode (decode (Nat.unpair n).2))) (encode none) =
    encode (Option.map Prod.fst (none.bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)))

case some
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n_1 n_ih ↦ Nat.rec 0 (fun n n_ih ↦ n_1.succ) (encode (decode (Nat.unpair n).2))) (encode (some val✝)) =
    encode (Option.map Prod.fst ((some val✝).bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)))
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case some.none
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n n_ih ↦ encode val✝ + 1) (encode none) = encode (Option.map (Function.const β val✝) none)

pp: case some.some
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝¹ : α
val✝ : β
⊢ Nat.rec 0 (fun n n_ih ↦ encode val✝¹ + 1) (encode (some val✝)) =
    encode (Option.map (Function.const β val✝¹) (some val✝))

Tactic:
<;>

Goal state after:
case some.none
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n n_ih ↦ encode val✝ + 1) (encode none) = encode (Option.map (Function.const β val✝) none)

case some.some
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝¹ : α
val✝ : β
⊢ Nat.rec 0 (fun n n_ih ↦ encode val✝¹ + 1) (encode (some val✝)) =
    encode (Option.map (Function.const β val✝¹) (some val✝))
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case none
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.rec 0 (fun n_1 n_ih ↦ Nat.rec 0 (fun n n_ih ↦ n.succ) (encode (decode (Nat.unpair n).2))) (encode none) =
    encode (Option.map Prod.snd (none.bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)))

pp: case some
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n_1 n_ih ↦ Nat.rec 0 (fun n n_ih ↦ n.succ) (encode (decode (Nat.unpair n).2))) (encode (some val✝)) =
    encode (Option.map Prod.snd ((some val✝).bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)))

Tactic:
<;>

Goal state after:
case none
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.rec 0 (fun n_1 n_ih ↦ Nat.rec 0 (fun n n_ih ↦ n.succ) (encode (decode (Nat.unpair n).2))) (encode none) =
    encode (Option.map Prod.snd (none.bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)))

case some
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n_1 n_ih ↦ Nat.rec 0 (fun n n_ih ↦ n.succ) (encode (decode (Nat.unpair n).2))) (encode (some val✝)) =
    encode (Option.map Prod.snd ((some val✝).bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)))
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case some.none
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n n_ih ↦ n + 1) (encode none) = encode none

pp: case some.some
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝¹ : α
val✝ : β
⊢ Nat.rec 0 (fun n n_ih ↦ n + 1) (encode (some val✝)) = encode (some val✝)

Tactic:
<;>

Goal state after:
case some.none
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n n_ih ↦ n + 1) (encode none) = encode none

case some.some
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝¹ : α
val✝ : β
⊢ Nat.rec 0 (fun n n_ih ↦ n + 1) (encode (some val✝)) = encode (some val✝)
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case none
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
f : α → β
g : α → γ
hf : Primrec f
hg : Primrec g
n : ℕ
⊢ (Nat.casesOn (encode none) 0 fun n ↦
      (Nat.pair (encode (Option.map f (decode n))).pred (encode (Option.map g (decode n))).pred).succ) =
    encode (Option.map (fun a ↦ (f a, g a)) none)

pp: case some
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
f : α → β
g : α → γ
hf : Primrec f
hg : Primrec g
n : ℕ
val✝ : α
⊢ (Nat.casesOn (encode (some val✝)) 0 fun n ↦
      (Nat.pair (encode (Option.map f (decode n))).pred (encode (Option.map g (decode n))).pred).succ) =
    encode (Option.map (fun a ↦ (f a, g a)) (some val✝))

Tactic:
<;>

Goal state after:
case none
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
f : α → β
g : α → γ
hf : Primrec f
hg : Primrec g
n : ℕ
⊢ (Nat.casesOn (encode none) 0 fun n ↦
      (Nat.pair (encode (Option.map f (decode n))).pred (encode (Option.map g (decode n))).pred).succ) =
    encode (Option.map (fun a ↦ (f a, g a)) none)

case some
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
f : α → β
g : α → γ
hf : Primrec f
hg : Primrec g
n : ℕ
val✝ : α
⊢ (Nat.casesOn (encode (some val✝)) 0 fun n ↦
      (Nat.pair (encode (Option.map f (decode n))).pred (encode (Option.map g (decode n))).pred).succ) =
    encode (Option.map (fun a ↦ (f a, g a)) (some val✝))
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case zero
α : Type u_1
inst✝ : Primcodable α
a : α
l : List α
⊢ (Nat.casesOn 0 (encode a).succ fun n ↦ encode l[ofNat ℕ n]?) = encode (a :: l)[ofNat ℕ 0]?

pp: case succ
α : Type u_1
inst✝ : Primcodable α
a : α
l : List α
n✝ : ℕ
⊢ (Nat.casesOn (n✝ + 1) (encode a).succ fun n ↦ encode l[ofNat ℕ n]?) = encode (a :: l)[ofNat ℕ (n✝ + 1)]?

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
inst✝ : Primcodable α
a : α
l : List α
⊢ (Nat.casesOn 0 (encode a).succ fun n ↦ encode l[ofNat ℕ n]?) = encode (a :: l)[ofNat ℕ 0]?

case succ
α : Type u_1
inst✝ : Primcodable α
a : α
l : List α
n✝ : ℕ
⊢ (Nat.casesOn (n✝ + 1) (encode a).succ fun n ↦ encode l[ofNat ℕ n]?) = encode (a :: l)[ofNat ℕ (n✝ + 1)]?
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n ↦ encode (decode n)
f : α → List β
g : α → σ
h : α → β × List β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this✝ : Primcodable (List β) := prim H
this : Primrec fun a ↦ Option.map (fun o ↦ Option.casesOn o (g a) (h a)) (decode (encode (f a)))
a : α
⊢ Option.map (fun o ↦ Option.casesOn o (g a) (h a)) (decode (encode [])) =
    some (List.casesOn [] (g a) fun b l ↦ h a (b, l))

pp: case cons
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n ↦ encode (decode n)
f : α → List β
g : α → σ
h : α → β × List β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this✝ : Primcodable (List β) := prim H
this : Primrec fun a ↦ Option.map (fun o ↦ Option.casesOn o (g a) (h a)) (decode (encode (f a)))
a : α
b : β
l : List β
⊢ Option.map (fun o ↦ Option.casesOn o (g a) (h a)) (decode (encode (b :: l))) =
    some (List.casesOn (b :: l) (g a) fun b l ↦ h a (b, l))

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n ↦ encode (decode n)
f : α → List β
g : α → σ
h : α → β × List β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this✝ : Primcodable (List β) := prim H
this : Primrec fun a ↦ Option.map (fun o ↦ Option.casesOn o (g a) (h a)) (decode (encode (f a)))
a : α
⊢ Option.map (fun o ↦ Option.casesOn o (g a) (h a)) (decode (encode [])) =
    some (List.casesOn [] (g a) fun b l ↦ h a (b, l))

case cons
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n ↦ encode (decode n)
f : α → List β
g : α → σ
h : α → β × List β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this✝ : Primcodable (List β) := prim H
this : Primrec fun a ↦ Option.map (fun o ↦ Option.casesOn o (g a) (h a)) (decode (encode (f a)))
a : α
b : β
l : List β
⊢ Option.map (fun o ↦ Option.casesOn o (g a) (h a)) (decode (encode (b :: l))) =
    some (List.casesOn (b :: l) (g a) fun b l ↦ h a (b, l))
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
b : Option β
⊢ Option.map (fun p ↦ f p.1 p.2) (none.bind fun a ↦ Option.map (Prod.mk a) b) = none.bind fun a ↦ Option.map (f a) b

pp: case some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
b : Option β
val✝ : α
⊢ Option.map (fun p ↦ f p.1 p.2) ((some val✝).bind fun a ↦ Option.map (Prod.mk a) b) =
    (some val✝).bind fun a ↦ Option.map (f a) b

Tactic:
<;>

Goal state after:
case none
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
b : Option β
⊢ Option.map (fun p ↦ f p.1 p.2) (none.bind fun a ↦ Option.map (Prod.mk a) b) = none.bind fun a ↦ Option.map (f a) b

case some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
b : Option β
val✝ : α
⊢ Option.map (fun p ↦ f p.1 p.2) ((some val✝).bind fun a ↦ Option.map (Prod.mk a) b) =
    (some val✝).bind fun a ↦ Option.map (f a) b
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case none.none
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
⊢ Option.map (fun p ↦ f p.1 p.2) (none.bind fun a ↦ Option.map (Prod.mk a) none) =
    none.bind fun a ↦ Option.map (f a) none

pp: case none.some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
val✝ : β
⊢ Option.map (fun p ↦ f p.1 p.2) (none.bind fun a ↦ Option.map (Prod.mk a) (some val✝)) =
    none.bind fun a ↦ Option.map (f a) (some val✝)

pp: case some.none
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
val✝ : α
⊢ Option.map (fun p ↦ f p.1 p.2) ((some val✝).bind fun a ↦ Option.map (Prod.mk a) none) =
    (some val✝).bind fun a ↦ Option.map (f a) none

pp: case some.some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
val✝¹ : α
val✝ : β
⊢ Option.map (fun p ↦ f p.1 p.2) ((some val✝¹).bind fun a ↦ Option.map (Prod.mk a) (some val✝)) =
    (some val✝¹).bind fun a ↦ Option.map (f a) (some val✝)

Tactic:
<;>

Goal state after:
case none.none
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
⊢ Option.map (fun p ↦ f p.1 p.2) (none.bind fun a ↦ Option.map (Prod.mk a) none) =
    none.bind fun a ↦ Option.map (f a) none

case none.some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
val✝ : β
⊢ Option.map (fun p ↦ f p.1 p.2) (none.bind fun a ↦ Option.map (Prod.mk a) (some val✝)) =
    none.bind fun a ↦ Option.map (f a) (some val✝)

case some.none
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
val✝ : α
⊢ Option.map (fun p ↦ f p.1 p.2) ((some val✝).bind fun a ↦ Option.map (Prod.mk a) none) =
    (some val✝).bind fun a ↦ Option.map (f a) none

case some.some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
val✝¹ : α
val✝ : β
⊢ Option.map (fun p ↦ f p.1 p.2) ((some val✝¹).bind fun a ↦ Option.map (Prod.mk a) (some val✝)) =
    (some val✝¹).bind fun a ↦ Option.map (f a) (some val✝)
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case succ.nil
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n ↦ encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH ↦ List.casesOn IH.2 IH fun b l ↦ (h a (IH.1, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n ↦ (G a)^[n] (g a, f a)
hF : Primrec fun a ↦ (F a (encode (f a))).1
a : α
n : ℕ
IH : ∀ (l : List β) (x : σ), (G a)^[n] (x, l) = (List.foldl (fun s b ↦ h a (s, b)) x (List.take n l), List.drop n l)
x : σ
⊢ (G a)^[n] (G a (x, [])) = (List.foldl (fun s b ↦ h a (s, b)) x (List.take (n + 1) []), List.drop (n + 1) [])

pp: case succ.cons
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n ↦ encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH ↦ List.casesOn IH.2 IH fun b l ↦ (h a (IH.1, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n ↦ (G a)^[n] (g a, f a)
hF : Primrec fun a ↦ (F a (encode (f a))).1
a : α
n : ℕ
IH : ∀ (l : List β) (x : σ), (G a)^[n] (x, l) = (List.foldl (fun s b ↦ h a (s, b)) x (List.take n l), List.drop n l)
x : σ
b : β
l : List β
⊢ (G a)^[n] (G a (x, b :: l)) =
    (List.foldl (fun s b ↦ h a (s, b)) x (List.take (n + 1) (b :: l)), List.drop (n + 1) (b :: l))

Tactic:
<;>

Goal state after:
case succ.nil
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n ↦ encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH ↦ List.casesOn IH.2 IH fun b l ↦ (h a (IH.1, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n ↦ (G a)^[n] (g a, f a)
hF : Primrec fun a ↦ (F a (encode (f a))).1
a : α
n : ℕ
IH : ∀ (l : List β) (x : σ), (G a)^[n] (x, l) = (List.foldl (fun s b ↦ h a (s, b)) x (List.take n l), List.drop n l)
x : σ
⊢ (G a)^[n] (G a (x, [])) = (List.foldl (fun s b ↦ h a (s, b)) x (List.take (n + 1) []), List.drop (n + 1) [])

case succ.cons
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n ↦ encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH ↦ List.casesOn IH.2 IH fun b l ↦ (h a (IH.1, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n ↦ (G a)^[n] (g a, f a)
hF : Primrec fun a ↦ (F a (encode (f a))).1
a : α
n : ℕ
IH : ∀ (l : List β) (x : σ), (G a)^[n] (x, l) = (List.foldl (fun s b ↦ h a (s, b)) x (List.take n l), List.drop n l)
x : σ
b : β
l : List β
⊢ (G a)^[n] (G a (x, b :: l)) =
    (List.foldl (fun s b ↦ h a (s, b)) x (List.take (n + 1) (b :: l)), List.drop (n + 1) (b :: l))
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case some.zero
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
a : α
⊢ Nat.rec (encode (f a) + 1)
      (fun y IH ↦ encode (Option.map ((fun p ↦ g p.1 p.2) ∘ Prod.mk a ∘ Prod.mk y) (decode (IH - 1)))) 0 =
    encode (Nat.rec (f a) (fun n IH ↦ g a (n, IH)) 0) + 1

pp: case some.succ
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
a : α
n✝ : ℕ
a✝ :
  Nat.rec (encode (f a) + 1)
      (fun y IH ↦ encode (Option.map ((fun p ↦ g p.1 p.2) ∘ Prod.mk a ∘ Prod.mk y) (decode (IH - 1)))) n✝ =
    encode (Nat.rec (f a) (fun n IH ↦ g a (n, IH)) n✝) + 1
⊢ Nat.rec (encode (f a) + 1)
      (fun y IH ↦ encode (Option.map ((fun p ↦ g p.1 p.2) ∘ Prod.mk a ∘ Prod.mk y) (decode (IH - 1)))) (n✝ + 1) =
    encode (Nat.rec (f a) (fun n IH ↦ g a (n, IH)) (n✝ + 1)) + 1

Tactic:
<;>

Goal state after:
case some.zero
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
a : α
⊢ Nat.rec (encode (f a) + 1)
      (fun y IH ↦ encode (Option.map ((fun p ↦ g p.1 p.2) ∘ Prod.mk a ∘ Prod.mk y) (decode (IH - 1)))) 0 =
    encode (Nat.rec (f a) (fun n IH ↦ g a (n, IH)) 0) + 1

case some.succ
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
a : α
n✝ : ℕ
a✝ :
  Nat.rec (encode (f a) + 1)
      (fun y IH ↦ encode (Option.map ((fun p ↦ g p.1 p.2) ∘ Prod.mk a ∘ Prod.mk y) (decode (IH - 1)))) n✝ =
    encode (Nat.rec (f a) (fun n IH ↦ g a (n, IH)) n✝) + 1
⊢ Nat.rec (encode (f a) + 1)
      (fun y IH ↦ encode (Option.map ((fun p ↦ g p.1 p.2) ∘ Prod.mk a ∘ Prod.mk y) (decode (IH - 1)))) (n✝ + 1) =
    encode (Nat.rec (f a) (fun n IH ↦ g a (n, IH)) (n✝ + 1)) + 1
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case nil
β : Type u_2
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n)
this : Primcodable (List β) := prim H
⊢ ∀ (r : List β), List.foldl (fun s b ↦ b :: s) r [] = [].reverseAux r

pp: case cons
β : Type u_2
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n)
this : Primcodable (List β) := prim H
head✝ : β
tail✝ : List β
tail_ih✝ : ∀ (r : List β), List.foldl (fun s b ↦ b :: s) r tail✝ = tail✝.reverseAux r
⊢ ∀ (r : List β), List.foldl (fun s b ↦ b :: s) r (head✝ :: tail✝) = (head✝ :: tail✝).reverseAux r

Tactic:
<;>

Goal state after:
case nil
β : Type u_2
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n)
this : Primcodable (List β) := prim H
⊢ ∀ (r : List β), List.foldl (fun s b ↦ b :: s) r [] = [].reverseAux r

case cons
β : Type u_2
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n)
this : Primcodable (List β) := prim H
head✝ : β
tail✝ : List β
tail_ih✝ : ∀ (r : List β), List.foldl (fun s b ↦ b :: s) r tail✝ = tail✝.reverseAux r
⊢ ∀ (r : List β), List.foldl (fun s b ↦ b :: s) r (head✝ :: tail✝) = (head✝ :: tail✝).reverseAux r