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

Goal state before:
pp: p : ℕ
⊢ Nat.rec (unpair p).1 (fun y IH ↦ IH - 1) (unpair p).2 = (unpair p).1 - (unpair p).2

Tactic:
;

Goal state after:
p : ℕ
⊢ Nat.rec (unpair p).1 (fun y IH ↦ IH - 1) (unpair p).2 = (unpair p).1 - (unpair p).2
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: p : ℕ
⊢ Nat.rec 0 (fun y IH ↦ (unpair p).1 + IH) (unpair p).2 = (unpair p).1 * (unpair p).2

Tactic:
;

Goal state after:
p : ℕ
⊢ Nat.rec 0 (fun y IH ↦ (unpair p).1 + IH) (unpair p).2 = (unpair p).1 * (unpair p).2
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: m n : ℕ
⊢ ((m.psub n).getD 0).ppred.getD 0 = (m.psub n >>= ppred).getD 0

Tactic:
;

Goal state after:
m n : ℕ
⊢ ((m.psub n).getD 0).ppred.getD 0 = (m.psub n >>= ppred).getD 0
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: m n k : ℕ
⊢ (∃ a, a + n = m ∧ k.succ = a) ↔ k + (n + 1) = m

Tactic:
simp [add_comm, add_left_comm]

Goal state after:
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: p : ℕ
⊢ Nat.rec 1 (fun y IH ↦ IH * (unpair p).1) (unpair p).2 = (unpair p).1 ^ (unpair p).2

Tactic:
;

Goal state after:
p : ℕ
⊢ Nat.rec 1 (fun y IH ↦ IH * (unpair p).1) (unpair p).2 = (unpair p).1 ^ (unpair p).2
Module: Mathlib.Computability.Primrec.Basic

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

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

Tactic:
;

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f g : α → β → σ
hg : Primrec₂ f
H : ∀ (a : α) (b : β), f a b = g a b
a : α
b : β
⊢ f a b = g a b

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f g : α → β → σ
hg : Primrec₂ f
H : ∀ (a : α) (b : β), f a b = g a b
a : α
b : β
⊢ f a b = g a b
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: ⊢ Nat.Primrec fun n ↦ n + 1

Tactic:
;

Goal state after:
⊢ Nat.Primrec fun n ↦ n + 1
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
⊢ (Primrec fun p ↦ f p.1 p.2) ↔ Primrec₂ f

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
⊢ (Primrec fun p ↦ f p.1 p.2) ↔ Primrec₂ f
Module: Mathlib.Computability.Primrec.Basic

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

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

Tactic:
;

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

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

Goal state before:
pp: α : 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 : ℕ
l : List β
⊢ (G a)^[n] (g a, l) = (List.foldl (fun s b ↦ h a (s, b)) (g a) (List.take n l), List.drop n l)

Tactic:
generalize g a = x

Goal state after:
α : 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 : ℕ
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)
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case hz
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n) := ⋯
this✝ : Primrec₂ fun a o ↦ Option.map (List.cons (encode a)) o
this :
  Primrec fun n ↦
    List.foldl (fun o m ↦ (decode m).bind fun a ↦ Option.map (List.cons (encode a)) o) (some [])
      (ofNat (List ℕ) n).reverse
n : ℕ
⊢ encode
      (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
        (ofNat (List ℕ) 0)) =
    encode (decode 0)

pp: case hi
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n) := ⋯
this✝ : Primrec₂ fun a o ↦ Option.map (List.cons (encode a)) o
this :
  Primrec fun n ↦
    List.foldl (fun o m ↦ (decode m).bind fun a ↦ Option.map (List.cons (encode a)) o) (some [])
      (ofNat (List ℕ) n).reverse
n : ℕ
⊢ ∀ (n : ℕ),
    (∀ m ≤ n,
        encode
            (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
              (ofNat (List ℕ) m)) =
          encode (decode m)) →
      encode
          (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
            (ofNat (List ℕ) (n + 1))) =
        encode (decode (n + 1))

Tactic:
;

Goal state after:
case hz
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n) := ⋯
this✝ : Primrec₂ fun a o ↦ Option.map (List.cons (encode a)) o
this :
  Primrec fun n ↦
    List.foldl (fun o m ↦ (decode m).bind fun a ↦ Option.map (List.cons (encode a)) o) (some [])
      (ofNat (List ℕ) n).reverse
n : ℕ
⊢ encode
      (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
        (ofNat (List ℕ) 0)) =
    encode (decode 0)

case hi
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n) := ⋯
this✝ : Primrec₂ fun a o ↦ Option.map (List.cons (encode a)) o
this :
  Primrec fun n ↦
    List.foldl (fun o m ↦ (decode m).bind fun a ↦ Option.map (List.cons (encode a)) o) (some [])
      (ofNat (List ℕ) n).reverse
n : ℕ
⊢ ∀ (n : ℕ),
    (∀ m ≤ n,
        encode
            (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
              (ofNat (List ℕ) m)) =
          encode (decode m)) →
      encode
          (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
            (ofNat (List ℕ) (n + 1))) =
        encode (decode (n + 1))
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case hi
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n) := prim (List ℕ)
this✝ : Primrec₂ fun a o ↦ Option.map (List.cons (encode a)) o
this :
  Primrec fun n ↦
    List.foldl (fun o m ↦ (decode m).bind fun a ↦ Option.map (List.cons (encode a)) o) (some [])
      (ofNat (List ℕ) n).reverse
n✝ n : ℕ
IH :
  ∀ m ≤ n,
    encode
        (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
          (ofNat (List ℕ) m)) =
      encode (decode m)
⊢ encode
      (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
        (ofNat (List ℕ) (n + 1))) =
    encode (decode (n + 1))

Tactic:
;

Goal state after:
case hi
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n) := prim (List ℕ)
this✝ : Primrec₂ fun a o ↦ Option.map (List.cons (encode a)) o
this :
  Primrec fun n ↦
    List.foldl (fun o m ↦ (decode m).bind fun a ↦ Option.map (List.cons (encode a)) o) (some [])
      (ofNat (List ℕ) n).reverse
n✝ n : ℕ
IH :
  ∀ m ≤ n,
    encode
        (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
          (ofNat (List ℕ) m)) =
      encode (decode m)
⊢ encode
      (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
        (ofNat (List ℕ) (n + 1))) =
    encode (decode (n + 1))
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case hi.some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n) := prim (List ℕ)
this✝ : Primrec₂ fun a o ↦ Option.map (List.cons (encode a)) o
this :
  Primrec fun n ↦
    List.foldl (fun o m ↦ (decode m).bind fun a ↦ Option.map (List.cons (encode a)) o) (some [])
      (ofNat (List ℕ) n).reverse
n✝ n : ℕ
IH :
  ∀ m ≤ n,
    encode
        (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
          (ofNat (List ℕ) m)) =
      encode (decode m)
a : α
⊢ encode
      (Option.map (List.cons (encode a))
        (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
          (ofNat (List ℕ) (Nat.unpair n).2))) =
    encode ((some fun x2 ↦ a :: x2) <*> decode (Nat.unpair n).2)

Tactic:
suffices ∀ (o : Option (List ℕ)) (p), encode o = encode p →
            encode (Option.map (List.cons (encode a)) o) = encode (Option.map (List.cons a) p) from
          this _ _ (IH _ (Nat.unpair_right_le n))

Goal state after:
case hi.some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n) := prim (List ℕ)
this✝ : Primrec₂ fun a o ↦ Option.map (List.cons (encode a)) o
this :
  Primrec fun n ↦
    List.foldl (fun o m ↦ (decode m).bind fun a ↦ Option.map (List.cons (encode a)) o) (some [])
      (ofNat (List ℕ) n).reverse
n✝ n : ℕ
IH :
  ∀ m ≤ n,
    encode
        (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
          (ofNat (List ℕ) m)) =
      encode (decode m)
a : α
⊢ ∀ (o : Option (List ℕ)) (p : Option (List α)),
    encode o = encode p → encode (Option.map (List.cons (encode a)) o) = encode (Option.map (List.cons a) p)
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case zero
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
k : ℕ
kn : n ≤ k + 0
y : ℕ
r : lbp p y k
⊢ Acc (lbp p) y

Tactic:
;

Goal state after:
case zero
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
k : ℕ
kn : n ≤ k + 0
y : ℕ
r : lbp p y k
⊢ Acc (lbp p) y
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case succ
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : ∀ (k : ℕ), n ≤ k + m → Acc (lbp p) k
k : ℕ
kn : n ≤ k + (m + 1)
y : ℕ
r : lbp p y k
⊢ Acc (lbp p) y

Tactic:
;

Goal state after:
case succ
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : ∀ (k : ℕ), n ≤ k + m → Acc (lbp p) k
k : ℕ
kn : n ≤ k + (m + 1)
y : ℕ
r : lbp p y k
⊢ Acc (lbp p) y
Module: Mathlib.Computability.Partrec

Goal state before:
pp: p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : ∀ (k : ℕ), n ≤ k + m → Acc (lbp p) k
k : ℕ
kn : n ≤ k + (m + 1)
a : ∀ k_1 ≤ k, false ∈ p k_1
⊢ n ≤ k + m + 1

Tactic:
;

Goal state after:
p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
n : ℕ
pn : true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : ∀ (k : ℕ), n ≤ k + m → Acc (lbp p) k
k : ℕ
kn : n ≤ k + (m + 1)
a : ∀ k_1 ≤ k, false ∈ p k_1
⊢ n ≤ k + m + 1
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : 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
l : List α
n : ℕ
⊢ Sum.rec (fun val ↦ none) (fun val ↦ some val) (F l n) = l[n]?

Tactic:
;

Goal state after:
α : 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
l : List α
n : ℕ
⊢ Sum.rec (fun val ↦ none) (fun val ↦ some val) (F l n) = l[n]?
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 : Primrec fun n ↦ (decode n).bind fun a ↦ Option.guard (fun b ↦ decide (p b)) a
n : ℕ
⊢ encode (none.bind fun a ↦ Option.guard (fun b ↦ decide (p b)) a) =
    encode (none.bind fun x ↦ if h : p x then some ⟨x, h⟩ else none)

pp: case some
α : 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 : α
⊢ encode ((some a).bind fun a ↦ Option.guard (fun b ↦ decide (p b)) a) =
    encode ((some a).bind fun x ↦ if h : p x then some ⟨x, h⟩ else none)

Tactic:
;

Goal state after:
case none
α : 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 : ℕ
⊢ encode (none.bind fun a ↦ Option.guard (fun b ↦ decide (p b)) a) =
    encode (none.bind fun x ↦ if h : p x then some ⟨x, h⟩ else none)

case some
α : 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 : α
⊢ encode ((some a).bind fun a ↦ Option.guard (fun b ↦ decide (p b)) a) =
    encode ((some a).bind fun x ↦ if h : p x then some ⟨x, h⟩ else none)
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 a = encode ⟨a, ⋯⟩

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 a = encode ⟨a, ⋯⟩
Module: Mathlib.Computability.Primrec.List

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

Tactic:
;

Goal state after:
n : ℕ
⊢ Nat.rec [] (fun n IH ↦ IH ++ [n]) n = List.range n
Module: Mathlib.Computability.Primrec.List

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Primcodable α
l : List (List α)
⊢ List.foldr (fun b s ↦ b ++ s) [] l = l.flatten
Module: Mathlib.Computability.Primrec.List

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Primcodable α
l : List α
⊢ List.foldr (fun b s ↦ s + 1) 0 l = l.length
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : 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 (f a) = List.findIdx (p a) (f a)

Tactic:
;

Goal state after:
α : 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 (f a) = List.findIdx (p a) (f a)
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype hp
h : Primrec fun a ↦ ↑(f a)
n : ℕ
⊢ encode (Option.map (fun a ↦ ↑(f a)) none) = encode (Option.map f none)

pp: case some
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype hp
h : Primrec fun a ↦ ↑(f a)
n : ℕ
a : α
⊢ encode (Option.map (fun a ↦ ↑(f a)) (some a)) = encode (Option.map f (some a))

Tactic:
;

Goal state after:
case none
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype hp
h : Primrec fun a ↦ ↑(f a)
n : ℕ
⊢ encode (Option.map (fun a ↦ ↑(f a)) none) = encode (Option.map f none)

case some
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype hp
h : Primrec fun a ↦ ↑(f a)
n : ℕ
a : α
⊢ encode (Option.map (fun a ↦ ↑(f a)) (some a)) = encode (Option.map f (some a))
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype hp
h : Primrec fun a ↦ ↑(f a)
n : ℕ
a : α
⊢ encode ↑(f a) = encode (f a)

Tactic:
;

Goal state after:
case some
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
this : Primcodable (Subtype p) := Primcodable.subtype hp
h : Primrec fun a ↦ ↑(f a)
n : ℕ
a : α
⊢ encode ↑(f a) = encode (f a)
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
f : ℕ → Option α
H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n
a : α
x✝ : ∃ n, a ∈ f n
n : ℕ
h : a ∈ f n
h' : (rfindOpt f).Dom
k : ℕ
hk : (rfindOpt f).get h' ∈ f k
this : a = (rfindOpt f).get h'
⊢ a ∈ rfindOpt f

Tactic:
;

Goal state after:
α : Type u_1
f : ℕ → Option α
H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n
a : α
x✝ : ∃ n, a ∈ f n
n : ℕ
h : a ∈ f n
h' : (rfindOpt f).Dom
k : ℕ
hk : (rfindOpt f).get h' ∈ f k
this : a = (rfindOpt f).get h'
⊢ a ∈ rfindOpt f
Module: Mathlib.Computability.Partrec

Goal state before:
pp: this : Primrec₂ fun n m ↦ if n = m.succ then 0 else 1
n✝ : ℕ
⊢ ∀ {m : ℕ}, m < n✝ → ¬n✝ = m

Tactic:
;

Goal state after:
this : Primrec₂ fun n m ↦ if n = m.succ then 0 else 1
n✝ : ℕ
⊢ ∀ {m : ℕ}, m < n✝ → ¬n✝ = m
Module: Mathlib.Computability.Partrec

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

Tactic:
;

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