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

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 : Primrec f
hg : Primrec₂ g
hh : Primrec₂ 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)) =
    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 : Primrec f
hg : Primrec₂ g
hh : Primrec₂ 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)) =
    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 : Primrec f
hg : Primrec₂ g
hh : Primrec₂ 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)) =
    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 : Primrec f
hg : Primrec₂ g
hh : Primrec₂ 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)) =
    some (Sum.casesOn (Sum.inr c) (g a) (h a))
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case cons.zero.nil
α : Type u_1
inst✝ : Primcodable α
F : List α → ℕ → ℕ ⊕ α :=
  fun l n ↦ List.foldl (fun s a ↦ Sum.casesOn s (fun x ↦ Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p ↦ Sum.casesOn (F p.1 p.2) (fun x ↦ none) some
a : α
⊢ [a][0]? =
    Sum.rec (fun val ↦ none) (fun val ↦ some val)
      (List.foldl
        (fun s a ↦ Sum.rec (fun val ↦ Nat.rec (Sum.inr a) (fun n n_ih ↦ Sum.inl n) val) (fun val ↦ Sum.inr val) s)
        (Sum.inr a) [])

pp: case cons.zero.cons
α : Type u_1
inst✝ : Primcodable α
F : List α → ℕ → ℕ ⊕ α :=
  fun l n ↦ List.foldl (fun s a ↦ Sum.casesOn s (fun x ↦ Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p ↦ Sum.casesOn (F p.1 p.2) (fun x ↦ none) some
a head✝ : α
tail✝ : List α
tail_ih✝ :
  (a :: tail✝)[0]? =
    Sum.rec (fun val ↦ none) (fun val ↦ some val)
      (List.foldl
        (fun s a ↦ Sum.rec (fun val ↦ Nat.rec (Sum.inr a) (fun n n_ih ↦ Sum.inl n) val) (fun val ↦ Sum.inr val) s)
        (Sum.inr a) tail✝)
⊢ (a :: head✝ :: tail✝)[0]? =
    Sum.rec (fun val ↦ none) (fun val ↦ some val)
      (List.foldl
        (fun s a ↦ Sum.rec (fun val ↦ Nat.rec (Sum.inr a) (fun n n_ih ↦ Sum.inl n) val) (fun val ↦ Sum.inr val) s)
        (Sum.inr a) (head✝ :: tail✝))

Tactic:
<;>

Goal state after:
case cons.zero.nil
α : Type u_1
inst✝ : Primcodable α
F : List α → ℕ → ℕ ⊕ α :=
  fun l n ↦ List.foldl (fun s a ↦ Sum.casesOn s (fun x ↦ Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p ↦ Sum.casesOn (F p.1 p.2) (fun x ↦ none) some
a : α
⊢ [a][0]? =
    Sum.rec (fun val ↦ none) (fun val ↦ some val)
      (List.foldl
        (fun s a ↦ Sum.rec (fun val ↦ Nat.rec (Sum.inr a) (fun n n_ih ↦ Sum.inl n) val) (fun val ↦ Sum.inr val) s)
        (Sum.inr a) [])

case cons.zero.cons
α : Type u_1
inst✝ : Primcodable α
F : List α → ℕ → ℕ ⊕ α :=
  fun l n ↦ List.foldl (fun s a ↦ Sum.casesOn s (fun x ↦ Nat.casesOn x (Sum.inr a) Sum.inl) Sum.inr) (Sum.inl n) l
hF : Primrec₂ F
this : Primrec fun p ↦ Sum.casesOn (F p.1 p.2) (fun x ↦ none) some
a head✝ : α
tail✝ : List α
tail_ih✝ :
  (a :: tail✝)[0]? =
    Sum.rec (fun val ↦ none) (fun val ↦ some val)
      (List.foldl
        (fun s a ↦ Sum.rec (fun val ↦ Nat.rec (Sum.inr a) (fun n n_ih ↦ Sum.inl n) val) (fun val ↦ Sum.inr val) s)
        (Sum.inr a) tail✝)
⊢ (a :: head✝ :: tail✝)[0]? =
    Sum.rec (fun val ↦ none) (fun val ↦ some val)
      (List.foldl
        (fun s a ↦ Sum.rec (fun val ↦ Nat.rec (Sum.inr a) (fun n n_ih ↦ Sum.inl n) val) (fun val ↦ Sum.inr val) s)
        (Sum.inr a) (head✝ :: tail✝))
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primrec fun n ↦ (decode n).bind fun a ↦ Option.guard (fun b ↦ decide (p b)) a
n : ℕ
a : α
h : p a
⊢ encode (if decide (p a) = true then some a else none) = encode (if h : p a then some ⟨a, h⟩ else none)

pp: case neg
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primrec fun n ↦ (decode n).bind fun a ↦ Option.guard (fun b ↦ decide (p b)) a
n : ℕ
a : α
h : ¬p a
⊢ encode (if decide (p a) = true then some a else none) = encode (if h : p a then some ⟨a, h⟩ else none)

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primrec fun n ↦ (decode n).bind fun a ↦ Option.guard (fun b ↦ decide (p b)) a
n : ℕ
a : α
h : p a
⊢ encode (if decide (p a) = true then some a else none) = encode (if h : p a then some ⟨a, h⟩ else none)

case neg
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primrec fun n ↦ (decode n).bind fun a ↦ Option.guard (fun b ↦ decide (p b)) a
n : ℕ
a : α
h : ¬p a
⊢ encode (if decide (p a) = true then some a else none) = encode (if h : p a then some ⟨a, h⟩ else none)
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case nil
α : Type u_1
inst✝ : Primcodable α
l₂ : List α
⊢ List.foldr (fun b s ↦ (([], l₂), b, s).2.1 :: (([], l₂), b, s).2.2) ([], l₂).2 ([], l₂).1 = [] ++ l₂

pp: case cons
α : Type u_1
inst✝ : Primcodable α
l₂ : List α
head✝ : α
tail✝ : List α
tail_ih✝ :
  List.foldr (fun b s ↦ ((tail✝, l₂), b, s).2.1 :: ((tail✝, l₂), b, s).2.2) (tail✝, l₂).2 (tail✝, l₂).1 = tail✝ ++ l₂
⊢ List.foldr (fun b s ↦ ((head✝ :: tail✝, l₂), b, s).2.1 :: ((head✝ :: tail✝, l₂), b, s).2.2) (head✝ :: tail✝, l₂).2
      (head✝ :: tail✝, l₂).1 =
    head✝ :: tail✝ ++ l₂

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
inst✝ : Primcodable α
l₂ : List α
⊢ List.foldr (fun b s ↦ (([], l₂), b, s).2.1 :: (([], l₂), b, s).2.2) ([], l₂).2 ([], l₂).1 = [] ++ l₂

case cons
α : Type u_1
inst✝ : Primcodable α
l₂ : List α
head✝ : α
tail✝ : List α
tail_ih✝ :
  List.foldr (fun b s ↦ ((tail✝, l₂), b, s).2.1 :: ((tail✝, l₂), b, s).2.2) (tail✝, l₂).2 (tail✝, l₂).1 = tail✝ ++ l₂
⊢ List.foldr (fun b s ↦ ((head✝ :: tail✝, l₂), b, s).2.1 :: ((head✝ :: tail✝, l₂), b, s).2.2) (head✝ :: tail✝, l₂).2
      (head✝ :: tail✝, l₂).1 =
    head✝ :: tail✝ ++ l₂
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → List β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
a : α
⊢ List.foldr (fun b s ↦ g (a, b, s).1 (a, b, s).2.1 :: (a, b, s).2.2) [] [] = List.map (g a) []

pp: case cons
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → List β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
a : α
head✝ : β
tail✝ : List β
tail_ih✝ : List.foldr (fun b s ↦ g (a, b, s).1 (a, b, s).2.1 :: (a, b, s).2.2) [] tail✝ = List.map (g a) tail✝
⊢ List.foldr (fun b s ↦ g (a, b, s).1 (a, b, s).2.1 :: (a, b, s).2.2) [] (head✝ :: tail✝) =
    List.map (g a) (head✝ :: tail✝)

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → List β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
a : α
⊢ List.foldr (fun b s ↦ g (a, b, s).1 (a, b, s).2.1 :: (a, b, s).2.2) [] [] = List.map (g a) []

case cons
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → List β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
a : α
head✝ : β
tail✝ : List β
tail_ih✝ : List.foldr (fun b s ↦ g (a, b, s).1 (a, b, s).2.1 :: (a, b, s).2.2) [] tail✝ = List.map (g a) tail✝
⊢ List.foldr (fun b s ↦ g (a, b, s).1 (a, b, s).2.1 :: (a, b, s).2.2) [] (head✝ :: tail✝) =
    List.map (g a) (head✝ :: tail✝)
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case zero
⊢ Nat.rec [] (fun n IH ↦ IH ++ [n]) 0 = List.range 0

pp: case succ
n✝ : ℕ
a✝ : Nat.rec [] (fun n IH ↦ IH ++ [n]) n✝ = List.range n✝
⊢ Nat.rec [] (fun n IH ↦ IH ++ [n]) (n✝ + 1) = List.range (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
⊢ Nat.rec [] (fun n IH ↦ IH ++ [n]) 0 = List.range 0

case succ
n✝ : ℕ
a✝ : Nat.rec [] (fun n IH ↦ IH ++ [n]) n✝ = List.range n✝
⊢ Nat.rec [] (fun n IH ↦ IH ++ [n]) (n✝ + 1) = List.range (n✝ + 1)
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case nil
α : Type u_1
inst✝ : Primcodable α
⊢ List.foldr (fun b s ↦ b ++ s) [] [] = [].flatten

pp: case cons
α : Type u_1
inst✝ : Primcodable α
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : List.foldr (fun b s ↦ b ++ s) [] tail✝ = tail✝.flatten
⊢ List.foldr (fun b s ↦ b ++ s) [] (head✝ :: tail✝) = (head✝ :: tail✝).flatten

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
inst✝ : Primcodable α
⊢ List.foldr (fun b s ↦ b ++ s) [] [] = [].flatten

case cons
α : Type u_1
inst✝ : Primcodable α
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : List.foldr (fun b s ↦ b ++ s) [] tail✝ = tail✝.flatten
⊢ List.foldr (fun b s ↦ b ++ s) [] (head✝ :: tail✝) = (head✝ :: tail✝).flatten
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case none
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primcodable (Subtype p) := Primcodable.subtype hp
n : ℕ
⊢ encode none = encode (Option.map Subtype.val none)

pp: case some
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primcodable (Subtype p) := Primcodable.subtype hp
n : ℕ
a : α
h : p a
⊢ encode (some ⟨a, h⟩) = encode (Option.map Subtype.val (some ⟨a, h⟩))

Tactic:
<;>

Goal state after:
case none
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primcodable (Subtype p) := Primcodable.subtype hp
n : ℕ
⊢ encode none = encode (Option.map Subtype.val none)

case some
α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primcodable (Subtype p) := Primcodable.subtype hp
n : ℕ
a : α
h : p a
⊢ encode (some ⟨a, h⟩) = encode (Option.map Subtype.val (some ⟨a, h⟩))
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case none
α : Type u_1
inst✝ : Primcodable α
⊢ (Option.casesOn (id none) [] fun b ↦ [id b]) = none.toList

pp: case some
α : Type u_1
inst✝ : Primcodable α
val✝ : α
⊢ (Option.casesOn (id (some val✝)) [] fun b ↦ [id b]) = (some val✝).toList

Tactic:
<;>

Goal state after:
case none
α : Type u_1
inst✝ : Primcodable α
⊢ (Option.casesOn (id none) [] fun b ↦ [id b]) = none.toList

case some
α : Type u_1
inst✝ : Primcodable α
val✝ : α
⊢ (Option.casesOn (id (some val✝)) [] fun b ↦ [id b]) = (some val✝).toList
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case nil
α : Type u_1
inst✝ : Primcodable α
⊢ List.foldr (fun b s ↦ s + 1) 0 [] = [].length

pp: case cons
α : Type u_1
inst✝ : Primcodable α
head✝ : α
tail✝ : List α
tail_ih✝ : List.foldr (fun b s ↦ s + 1) 0 tail✝ = tail✝.length
⊢ List.foldr (fun b s ↦ s + 1) 0 (head✝ :: tail✝) = (head✝ :: tail✝).length

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
inst✝ : Primcodable α
⊢ List.foldr (fun b s ↦ s + 1) 0 [] = [].length

case cons
α : Type u_1
inst✝ : Primcodable α
head✝ : α
tail✝ : List α
tail_ih✝ : List.foldr (fun b s ↦ s + 1) 0 tail✝ = tail✝.length
⊢ List.foldr (fun b s ↦ s + 1) 0 (head✝ :: tail✝) = (head✝ :: tail✝).length
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → List β
p : α → β → Bool
hf : Primrec f
hp : Primrec₂ p
a : α
⊢ List.foldr (fun b s ↦ bif p a b then 0 else s + 1) 0 [] = List.findIdx (p a) []

pp: case cons
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → List β
p : α → β → Bool
hf : Primrec f
hp : Primrec₂ p
a : α
head✝ : β
tail✝ : List β
tail_ih✝ : List.foldr (fun b s ↦ bif p a b then 0 else s + 1) 0 tail✝ = List.findIdx (p a) tail✝
⊢ List.foldr (fun b s ↦ bif p a b then 0 else s + 1) 0 (head✝ :: tail✝) = List.findIdx (p a) (head✝ :: tail✝)

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → List β
p : α → β → Bool
hf : Primrec f
hp : Primrec₂ p
a : α
⊢ List.foldr (fun b s ↦ bif p a b then 0 else s + 1) 0 [] = List.findIdx (p a) []

case cons
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → List β
p : α → β → Bool
hf : Primrec f
hp : Primrec₂ p
a : α
head✝ : β
tail✝ : List β
tail_ih✝ : List.foldr (fun b s ↦ bif p a b then 0 else s + 1) 0 tail✝ = List.findIdx (p a) tail✝
⊢ List.foldr (fun b s ↦ bif p a b then 0 else s + 1) 0 (head✝ :: tail✝) = List.findIdx (p a) (head✝ :: tail✝)
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
h : ∀ (a : α), (f a).isSome = true
hf : Primrec f
n : ℕ
hx : decode n = none
⊢ (encode (Option.map f none)).pred = encode (Option.map (fun a ↦ (f a).get ⋯) none)

pp: case some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
h : ∀ (a : α), (f a).isSome = true
hf : Primrec f
n : ℕ
val✝ : α
hx : decode n = some val✝
⊢ (encode (Option.map f (some val✝))).pred = encode (Option.map (fun a ↦ (f a).get ⋯) (some val✝))

Tactic:
<;>

Goal state after:
case none
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
h : ∀ (a : α), (f a).isSome = true
hf : Primrec f
n : ℕ
hx : decode n = none
⊢ (encode (Option.map f none)).pred = encode (Option.map (fun a ↦ (f a).get ⋯) none)

case some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
h : ∀ (a : α), (f a).isSome = true
hf : Primrec f
n : ℕ
val✝ : α
hx : decode n = some val✝
⊢ (encode (Option.map f (some val✝))).pred = encode (Option.map (fun a ↦ (f a).get ⋯) (some val✝))
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case cons.false
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : DecidableEq α
a : α
p : α × β
ps : List (α × β)
ih :
  (List.recOn (a, ps).2 none fun b l IH ↦
      bif ((a, ps), b, l, IH).1.1 == ((a, ps), b, l, IH).2.1.1 then some ((a, ps), b, l, IH).2.1.2
      else ((a, ps), b, l, IH).2.2.2) =
    List.lookup a ps
ha : (a == p.1) = false
⊢ (bif false then some p.2 else List.lookup a ps) =
    match false with
    | true => some p.2
    | false => List.lookup a ps

pp: case cons.true
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : DecidableEq α
a : α
p : α × β
ps : List (α × β)
ih :
  (List.recOn (a, ps).2 none fun b l IH ↦
      bif ((a, ps), b, l, IH).1.1 == ((a, ps), b, l, IH).2.1.1 then some ((a, ps), b, l, IH).2.1.2
      else ((a, ps), b, l, IH).2.2.2) =
    List.lookup a ps
ha : (a == p.1) = true
⊢ (bif true then some p.2 else List.lookup a ps) =
    match true with
    | true => some p.2
    | false => List.lookup a ps

Tactic:
<;>

Goal state after:
case cons.false
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : DecidableEq α
a : α
p : α × β
ps : List (α × β)
ih :
  (List.recOn (a, ps).2 none fun b l IH ↦
      bif ((a, ps), b, l, IH).1.1 == ((a, ps), b, l, IH).2.1.1 then some ((a, ps), b, l, IH).2.1.2
      else ((a, ps), b, l, IH).2.2.2) =
    List.lookup a ps
ha : (a == p.1) = false
⊢ (bif false then some p.2 else List.lookup a ps) =
    match false with
    | true => some p.2
    | false => List.lookup a ps

case cons.true
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : DecidableEq α
a : α
p : α × β
ps : List (α × β)
ih :
  (List.recOn (a, ps).2 none fun b l IH ↦
      bif ((a, ps), b, l, IH).1.1 == ((a, ps), b, l, IH).2.1.1 then some ((a, ps), b, l, IH).2.1.2
      else ((a, ps), b, l, IH).2.2.2) =
    List.lookup a ps
ha : (a == p.1) = true
⊢ (bif true then some p.2 else List.lookup a ps) =
    match true with
    | true => some p.2
    | false => List.lookup a ps
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case none
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → σ
hf : Primrec f
n : ℕ
⊢ ↑(encode (Option.map f Option.none)).ppred = (↑Option.none).bind fun a ↦ Part.some (encode (f a))

pp: case some
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → σ
hf : Primrec f
n : ℕ
val✝ : α
⊢ ↑(encode (Option.map f (Option.some val✝))).ppred = (↑(Option.some val✝)).bind fun a ↦ Part.some (encode (f a))

Tactic:
<;>

Goal state after:
case none
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → σ
hf : Primrec f
n : ℕ
⊢ ↑(encode (Option.map f Option.none)).ppred = (↑Option.none).bind fun a ↦ Part.some (encode (f a))

case some
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → σ
hf : Primrec f
n : ℕ
val✝ : α
⊢ ↑(encode (Option.map f (Option.some val✝))).ppred = (↑(Option.some val✝)).bind fun a ↦ Part.some (encode (f a))
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
⊢ (do
      let n ← (↑Option.none).bind fun a ↦ map encode (↑f a)
      ↑n.ppred) =
    (↑Option.none).bind fun a ↦ map encode ((fun a ↦ ↑(f a)) a)

pp: case some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
a : α
⊢ (do
      let n ← (↑(Option.some a)).bind fun a ↦ map encode (↑f a)
      ↑n.ppred) =
    (↑(Option.some a)).bind fun a ↦ map encode ((fun a ↦ ↑(f a)) a)

Tactic:
<;>

Goal state after:
case none
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
⊢ (do
      let n ← (↑Option.none).bind fun a ↦ map encode (↑f a)
      ↑n.ppred) =
    (↑Option.none).bind fun a ↦ map encode ((fun a ↦ ↑(f a)) a)

case some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
a : α
⊢ (do
      let n ← (↑(Option.some a)).bind fun a ↦ map encode (↑f a)
      ↑n.ppred) =
    (↑(Option.some a)).bind fun a ↦ map encode ((fun a ↦ ↑(f a)) a)
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case some.none
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
a : α
⊢ ↑(encode Option.none).ppred = map encode ↑Option.none

pp: case some.some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
a : α
val✝ : β
⊢ ↑(encode (Option.some val✝)).ppred = map encode ↑(Option.some val✝)

Tactic:
<;>

Goal state after:
case some.none
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
a : α
⊢ ↑(encode Option.none).ppred = map encode ↑Option.none

case some.some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
a : α
val✝ : β
⊢ ↑(encode (Option.some val✝)).ppred = map encode ↑(Option.some val✝)
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 : Computable f
hg : Computable g
n : ℕ
⊢ ((Nat.pair <$> (↑Option.none).bind fun a ↦ map encode (↑f a)) <*> (↑Option.none).bind fun a ↦ map encode (↑g a)) =
    (↑Option.none).bind fun a ↦ map encode ((↑fun a ↦ (f a, g a)) a)

pp: case some
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
f : α → β
g : α → γ
hf : Computable f
hg : Computable g
n : ℕ
val✝ : α
⊢ ((Nat.pair <$> (↑(Option.some val✝)).bind fun a ↦ map encode (↑f a)) <*>
      (↑(Option.some val✝)).bind fun a ↦ map encode (↑g a)) =
    (↑(Option.some val✝)).bind fun a ↦ map encode ((↑fun a ↦ (f a, g a)) 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 : Computable f
hg : Computable g
n : ℕ
⊢ ((Nat.pair <$> (↑Option.none).bind fun a ↦ map encode (↑f a)) <*> (↑Option.none).bind fun a ↦ map encode (↑g a)) =
    (↑Option.none).bind fun a ↦ map encode ((↑fun a ↦ (f a, g a)) a)

case some
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
f : α → β
g : α → γ
hf : Computable f
hg : Computable g
n : ℕ
val✝ : α
⊢ ((Nat.pair <$> (↑(Option.some val✝)).bind fun a ↦ map encode (↑f a)) <*>
      (↑(Option.some val✝)).bind fun a ↦ map encode (↑g a)) =
    (↑(Option.some val✝)).bind fun a ↦ map encode ((↑fun a ↦ (f a, g a)) a)
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case none
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
⊢ Part.none = (↑Option.none).bind fun a ↦ map encode ((fun x ↦ Part.none) a)

pp: case some
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
val✝ : α
⊢ Part.none = (↑(Option.some val✝)).bind fun a ↦ map encode ((fun x ↦ Part.none) a)

Tactic:
<;>

Goal state after:
case none
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
⊢ Part.none = (↑Option.none).bind fun a ↦ map encode ((fun x ↦ Part.none) a)

case some
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
val✝ : α
⊢ Part.none = (↑(Option.some val✝)).bind fun a ↦ map encode ((fun x ↦ Part.none) a)
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 : Partrec₂ g
n : ℕ
e : decode n = Option.none
⊢ (do
      let n ← Nat.pair <$> Part.some n <*> (↑Option.none).bind fun a ↦ map encode (f a)
      (↑(decode n)).bind fun a ↦ map encode ((fun p ↦ g p.1 p.2) a)) =
    (↑Option.none).bind fun a ↦ map encode ((fun a ↦ (f a).bind (g a)) 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 : Partrec₂ g
n : ℕ
val✝ : α
e : decode n = Option.some val✝
⊢ (do
      let n ← Nat.pair <$> Part.some n <*> (↑(Option.some val✝)).bind fun a ↦ map encode (f a)
      (↑(decode n)).bind fun a ↦ map encode ((fun p ↦ g p.1 p.2) a)) =
    (↑(Option.some val✝)).bind fun a ↦ map encode ((fun a ↦ (f a).bind (g a)) 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 : Partrec₂ g
n : ℕ
e : decode n = Option.none
⊢ (do
      let n ← Nat.pair <$> Part.some n <*> (↑Option.none).bind fun a ↦ map encode (f a)
      (↑(decode n)).bind fun a ↦ map encode ((fun p ↦ g p.1 p.2) a)) =
    (↑Option.none).bind fun a ↦ map encode ((fun a ↦ (f a).bind (g a)) a)

case some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α →. β
g : α → β →. σ
hf : Partrec f
hg : Partrec₂ g
n : ℕ
val✝ : α
e : decode n = Option.some val✝
⊢ (do
      let n ← Nat.pair <$> Part.some n <*> (↑(Option.some val✝)).bind fun a ↦ map encode (f a)
      (↑(decode n)).bind fun a ↦ map encode ((fun p ↦ g p.1 p.2) a)) =
    (↑(Option.some val✝)).bind fun a ↦ map encode ((fun a ↦ (f a).bind (g a)) a)