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

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → ℕ
g : α → β
h : α → β → β
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
a : α
⊢ Nat.rec (g a) (fun n IH ↦ h a (n, IH).2) 0 = (h a)^[0] (g a)

pp: case succ
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → ℕ
g : α → β
h : α → β → β
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
a : α
n✝ : ℕ
a✝ : Nat.rec (g a) (fun n IH ↦ h a (n, IH).2) n✝ = (h a)^[n✝] (g a)
⊢ Nat.rec (g a) (fun n IH ↦ h a (n, IH).2) (n✝ + 1) = (h a)^[n✝ + 1] (g a)

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → ℕ
g : α → β
h : α → β → β
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
a : α
⊢ Nat.rec (g a) (fun n IH ↦ h a (n, IH).2) 0 = (h a)^[0] (g a)

case succ
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → ℕ
g : α → β
h : α → β → β
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
a : α
n✝ : ℕ
a✝ : Nat.rec (g a) (fun n IH ↦ h a (n, IH).2) n✝ = (h a)^[n✝] (g a)
⊢ Nat.rec (g a) (fun n IH ↦ h a (n, IH).2) (n✝ + 1) = (h a)^[n✝ + 1] (g a)
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 σ
o : α → Option β
f : α → σ
g : α → β → σ
ho : Primrec o
hf : Primrec f
hg : Primrec₂ g
a : α
⊢ (Nat.casesOn (encode none) (encode (f a)) fun b ↦
      (encode ((decode (encode (a, b).1)).bind fun a ↦ Option.map (g a) (decode b))).pred) =
    encode (Option.casesOn none (f a) (g a))

pp: case some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β → σ
ho : Primrec o
hf : Primrec f
hg : Primrec₂ g
a : α
b : β
⊢ (Nat.casesOn (encode (some b)) (encode (f a)) fun b ↦
      (encode ((decode (encode (a, b).1)).bind fun a ↦ Option.map (g a) (decode b))).pred) =
    encode (Option.casesOn (some b) (f a) (g a))

Tactic:
<;>

Goal state after:
case none
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β → σ
ho : Primrec o
hf : Primrec f
hg : Primrec₂ g
a : α
⊢ (Nat.casesOn (encode none) (encode (f a)) fun b ↦
      (encode ((decode (encode (a, b).1)).bind fun a ↦ Option.map (g a) (decode b))).pred) =
    encode (Option.casesOn none (f a) (g a))

case some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β → σ
ho : Primrec o
hf : Primrec f
hg : Primrec₂ g
a : α
b : β
⊢ (Nat.casesOn (encode (some b)) (encode (f a)) fun b ↦
      (encode ((decode (encode (a, b).1)).bind fun a ↦ Option.map (g a) (decode b))).pred) =
    encode (Option.casesOn (some b) (f a) (g a))
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 : α → Option β
g : α → β → Option σ
hf : Primrec f
hg : Primrec₂ g
a : α
⊢ Option.casesOn none none (g a) = none.bind (g a)

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

Tactic:
<;>

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

case some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → Option β
g : α → β → Option σ
hf : Primrec f
hg : Primrec₂ g
a : α
val✝ : β
⊢ Option.casesOn (some val✝) none (g a) = (some val✝).bind (g a)
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 : α → Option β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
x : α
⊢ (none.bind fun b ↦ some (g x b)) = Option.map (g x) none

pp: case some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → Option β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
x : α
val✝ : β
⊢ ((some val✝).bind fun b ↦ some (g x b)) = Option.map (g x) (some val✝)

Tactic:
<;>

Goal state after:
case none
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → Option β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
x : α
⊢ (none.bind fun b ↦ some (g x b)) = Option.map (g x) none

case some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → Option β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
x : α
val✝ : β
⊢ ((some val✝).bind fun b ↦ some (g x b)) = Option.map (g x) (some val✝)
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case none
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × α
a : α
⊢ (Option.casesOn ((fun a x ↦ a) (none, a).1 (none, a).2) ((fun x b ↦ b) (none, a).1 (none, a).2) fun b ↦ b) =
    (none, a).1.getD (none, a).2

pp: case some
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × α
a val✝ : α
⊢ (Option.casesOn ((fun a x ↦ a) (some val✝, a).1 (some val✝, a).2) ((fun x b ↦ b) (some val✝, a).1 (some val✝, a).2)
      fun b ↦ b) =
    (some val✝, a).1.getD (some val✝, a).2

Tactic:
<;>

Goal state after:
case none
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × α
a : α
⊢ (Option.casesOn ((fun a x ↦ a) (none, a).1 (none, a).2) ((fun x b ↦ b) (none, a).1 (none, a).2) fun b ↦ b) =
    (none, a).1.getD (none, a).2

case some
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × α
a val✝ : α
⊢ (Option.casesOn ((fun a x ↦ a) (some val✝, a).1 (some val✝, a).2) ((fun x b ↦ b) (some val✝, a).1 (some val✝, a).2)
      fun b ↦ b) =
    (some val✝, a).1.getD (some val✝, a).2
Module: Mathlib.Computability.Primrec.Basic

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

pp: case some
α : Type u_1
inst✝ : Primcodable α
val✝ : α
⊢ (Option.casesOn (id (some val✝)) false fun b ↦ true) = (some val✝).isSome

Tactic:
<;>

Goal state after:
case none
α : Type u_1
inst✝ : Primcodable α
⊢ (Option.casesOn (id none) false fun b ↦ true) = none.isSome

case some
α : Type u_1
inst✝ : Primcodable α
val✝ : α
⊢ (Option.casesOn (id (some val✝)) false fun b ↦ true) = (some val✝).isSome
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case false
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
c : α → Bool
f g : α → σ
hc : Primrec c
hf : Primrec f
hg : Primrec 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_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
c : α → Bool
f g : α → σ
hc : Primrec c
hf : Primrec f
hg : Primrec 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_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
c : α → Bool
f g : α → σ
hc : Primrec c
hf : Primrec f
hg : Primrec 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_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
c : α → Bool
f g : α → σ
hc : Primrec c
hf : Primrec f
hg : Primrec 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.Primrec.Basic

Goal state before:
pp: case false
α : Type u_1
inst✝ : Primcodable α
f : Bool → α
⊢ (bif id false then f true else f false) = f false

pp: case true
α : Type u_1
inst✝ : Primcodable α
f : Bool → α
⊢ (bif id true then f true else f false) = f true

Tactic:
<;>

Goal state after:
case false
α : Type u_1
inst✝ : Primcodable α
f : Bool → α
⊢ (bif id false then f true else f false) = f false

case true
α : Type u_1
inst✝ : Primcodable α
f : Bool → α
⊢ (bif id true then f true else f false) = f true
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case false
α : Type u_1
inst✝ : Primcodable α
f : Bool → Bool → α
x✝ : Bool × Bool
b : Bool
⊢ (bif (false, b).1 then f true (false, b).2 else f false (false, b).2) = f (false, b).1 (false, b).2

pp: case true
α : Type u_1
inst✝ : Primcodable α
f : Bool → Bool → α
x✝ : Bool × Bool
b : Bool
⊢ (bif (true, b).1 then f true (true, b).2 else f false (true, b).2) = f (true, b).1 (true, b).2

Tactic:
<;>

Goal state after:
case false
α : Type u_1
inst✝ : Primcodable α
f : Bool → Bool → α
x✝ : Bool × Bool
b : Bool
⊢ (bif (false, b).1 then f true (false, b).2 else f false (false, b).2) = f (false, b).1 (false, b).2

case true
α : Type u_1
inst✝ : Primcodable α
f : Bool → Bool → α
x✝ : Bool × Bool
b : Bool
⊢ (bif (true, b).1 then f true (true, b).2 else f false (true, b).2) = f (true, b).1 (true, b).2
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case hi.some.none
α : 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 : α
p : Option (List α)
IH : encode none = encode p
⊢ encode (Option.map (List.cons (encode a)) none) = encode (Option.map (List.cons a) p)

pp: case hi.some.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 : α
p : Option (List α)
val✝ : List ℕ
IH : encode (some val✝) = encode p
⊢ encode (Option.map (List.cons (encode a)) (some val✝)) = encode (Option.map (List.cons a) p)

Tactic:
<;>

Goal state after:
case hi.some.none
α : 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 : α
p : Option (List α)
IH : encode none = encode p
⊢ encode (Option.map (List.cons (encode a)) none) = encode (Option.map (List.cons a) p)

case hi.some.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 : α
p : Option (List α)
val✝ : List ℕ
IH : encode (some val✝) = encode p
⊢ encode (Option.map (List.cons (encode a)) (some val✝)) = encode (Option.map (List.cons a) p)
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case none
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × Option α
o₂ : Option α
⊢ (Option.casesOn (none, o₂).1 (none, o₂).2 fun b ↦ ((none, o₂), b).1.1) =
    (fun x1 x2 ↦ x1 <|> x2) (none, o₂).1 (none, o₂).2

pp: case some
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × Option α
o₂ : Option α
val✝ : α
⊢ (Option.casesOn (some val✝, o₂).1 (some val✝, o₂).2 fun b ↦ ((some val✝, o₂), b).1.1) =
    (fun x1 x2 ↦ x1 <|> x2) (some val✝, o₂).1 (some val✝, o₂).2

Tactic:
<;>

Goal state after:
case none
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × Option α
o₂ : Option α
⊢ (Option.casesOn (none, o₂).1 (none, o₂).2 fun b ↦ ((none, o₂), b).1.1) =
    (fun x1 x2 ↦ x1 <|> x2) (none, o₂).1 (none, o₂).2

case some
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × Option α
o₂ : Option α
val✝ : α
⊢ (Option.casesOn (some val✝, o₂).1 (some val✝, o₂).2 fun b ↦ ((some val✝, o₂), b).1.1) =
    (fun x1 x2 ↦ x1 <|> x2) (some val✝, o₂).1 (some val✝, o₂).2
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case none.none
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × Option α
⊢ (Option.casesOn (none, none).1 (none, none).2 fun b ↦ ((none, none), b).1.1) =
    (fun x1 x2 ↦ x1 <|> x2) (none, none).1 (none, none).2

pp: case none.some
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × Option α
val✝ : α
⊢ (Option.casesOn (none, some val✝).1 (none, some val✝).2 fun b ↦ ((none, some val✝), b).1.1) =
    (fun x1 x2 ↦ x1 <|> x2) (none, some val✝).1 (none, some val✝).2

pp: case some.none
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × Option α
val✝ : α
⊢ (Option.casesOn (some val✝, none).1 (some val✝, none).2 fun b ↦ ((some val✝, none), b).1.1) =
    (fun x1 x2 ↦ x1 <|> x2) (some val✝, none).1 (some val✝, none).2

pp: case some.some
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × Option α
val✝¹ val✝ : α
⊢ (Option.casesOn (some val✝¹, some val✝).1 (some val✝¹, some val✝).2 fun b ↦ ((some val✝¹, some val✝), b).1.1) =
    (fun x1 x2 ↦ x1 <|> x2) (some val✝¹, some val✝).1 (some val✝¹, some val✝).2

Tactic:
<;>

Goal state after:
case none.none
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × Option α
⊢ (Option.casesOn (none, none).1 (none, none).2 fun b ↦ ((none, none), b).1.1) =
    (fun x1 x2 ↦ x1 <|> x2) (none, none).1 (none, none).2

case none.some
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × Option α
val✝ : α
⊢ (Option.casesOn (none, some val✝).1 (none, some val✝).2 fun b ↦ ((none, some val✝), b).1.1) =
    (fun x1 x2 ↦ x1 <|> x2) (none, some val✝).1 (none, some val✝).2

case some.none
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × Option α
val✝ : α
⊢ (Option.casesOn (some val✝, none).1 (some val✝, none).2 fun b ↦ ((some val✝, none), b).1.1) =
    (fun x1 x2 ↦ x1 <|> x2) (some val✝, none).1 (some val✝, none).2

case some.some
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × Option α
val✝¹ val✝ : α
⊢ (Option.casesOn (some val✝¹, some val✝).1 (some val✝¹, some val✝).2 fun b ↦ ((some val✝¹, some val✝), b).1.1) =
    (fun x1 x2 ↦ x1 <|> x2) (some val✝¹, some val✝).1 (some val✝¹, some val✝).2
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case zero
α : Type u_1
inst✝¹ : Primcodable α
f : α → ℕ
p : α → ℕ → Prop
inst✝ : DecidableRel p
hf : Primrec f
hp : PrimrecRel p
x : α
⊢ Nat.rec 0 (fun n IH ↦ if p x ((n, IH).1 + 1) then (n, IH).1 + 1 else (n, IH).2) 0 = Nat.findGreatest (p x) 0

pp: case succ
α : Type u_1
inst✝¹ : Primcodable α
f : α → ℕ
p : α → ℕ → Prop
inst✝ : DecidableRel p
hf : Primrec f
hp : PrimrecRel p
x : α
n✝ : ℕ
a✝ : Nat.rec 0 (fun n IH ↦ if p x ((n, IH).1 + 1) then (n, IH).1 + 1 else (n, IH).2) n✝ = Nat.findGreatest (p x) n✝
⊢ Nat.rec 0 (fun n IH ↦ if p x ((n, IH).1 + 1) then (n, IH).1 + 1 else (n, IH).2) (n✝ + 1) =
    Nat.findGreatest (p x) (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
inst✝¹ : Primcodable α
f : α → ℕ
p : α → ℕ → Prop
inst✝ : DecidableRel p
hf : Primrec f
hp : PrimrecRel p
x : α
⊢ Nat.rec 0 (fun n IH ↦ if p x ((n, IH).1 + 1) then (n, IH).1 + 1 else (n, IH).2) 0 = Nat.findGreatest (p x) 0

case succ
α : Type u_1
inst✝¹ : Primcodable α
f : α → ℕ
p : α → ℕ → Prop
inst✝ : DecidableRel p
hf : Primrec f
hp : PrimrecRel p
x : α
n✝ : ℕ
a✝ : Nat.rec 0 (fun n IH ↦ if p x ((n, IH).1 + 1) then (n, IH).1 + 1 else (n, IH).2) n✝ = Nat.findGreatest (p x) n✝
⊢ Nat.rec 0 (fun n IH ↦ if p x ((n, IH).1 + 1) then (n, IH).1 + 1 else (n, IH).2) (n✝ + 1) =
    Nat.findGreatest (p x) (n✝ + 1)
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case nil
α : Type u_1
inst✝ : Primcodable α
⊢ (List.casesOn (id []) none fun b l ↦ some ([], b, l).2.1) = [].head?

pp: case cons
α : Type u_1
inst✝ : Primcodable α
head✝ : α
tail✝ : List α
⊢ (List.casesOn (id (head✝ :: tail✝)) none fun b l ↦ some (head✝ :: tail✝, b, l).2.1) = (head✝ :: tail✝).head?

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
inst✝ : Primcodable α
⊢ (List.casesOn (id []) none fun b l ↦ some ([], b, l).2.1) = [].head?

case cons
α : Type u_1
inst✝ : Primcodable α
head✝ : α
tail✝ : List α
⊢ (List.casesOn (id (head✝ :: tail✝)) none fun b l ↦ some (head✝ :: tail✝, b, l).2.1) = (head✝ :: tail✝).head?
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case nil
α : Type u_1
inst✝ : Primcodable α
⊢ (List.casesOn (id []) [] fun b l ↦ ([], b, l).2.2) = [].tail

pp: case cons
α : Type u_1
inst✝ : Primcodable α
head✝ : α
tail✝ : List α
⊢ (List.casesOn (id (head✝ :: tail✝)) [] fun b l ↦ (head✝ :: tail✝, b, l).2.2) = (head✝ :: tail✝).tail

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
inst✝ : Primcodable α
⊢ (List.casesOn (id []) [] fun b l ↦ ([], b, l).2.2) = [].tail

case cons
α : Type u_1
inst✝ : Primcodable α
head✝ : α
tail✝ : List α
⊢ (List.casesOn (id (head✝ :: tail✝)) [] fun b l ↦ (head✝ :: tail✝, b, l).2.2) = (head✝ :: tail✝).tail
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 : α → σ
h : α → β × List β × σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : α → List β × σ := fun a ↦ List.foldr (fun b s ↦ (b :: s.1, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
⊢ List.foldr (fun b s ↦ (b :: s.1, h a (b, s))) ([], g a) [] = ([], List.rec (g a) (fun b l IH ↦ h a (b, l, IH)) [])

pp: case cons
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → List β
g : α → σ
h : α → β × List β × σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : α → List β × σ := fun a ↦ List.foldr (fun b s ↦ (b :: s.1, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
head✝ : β
tail✝ : List β
tail_ih✝ :
  List.foldr (fun b s ↦ (b :: s.1, h a (b, s))) ([], g a) tail✝ =
    (tail✝, List.rec (g a) (fun b l IH ↦ h a (b, l, IH)) tail✝)
⊢ List.foldr (fun b s ↦ (b :: s.1, h a (b, s))) ([], g a) (head✝ :: tail✝) =
    (head✝ :: tail✝, List.rec (g a) (fun b l IH ↦ h a (b, l, IH)) (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 : α → σ
h : α → β × List β × σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : α → List β × σ := fun a ↦ List.foldr (fun b s ↦ (b :: s.1, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
⊢ List.foldr (fun b s ↦ (b :: s.1, h a (b, s))) ([], g a) [] = ([], List.rec (g a) (fun b l IH ↦ h a (b, l, IH)) [])

case cons
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → List β
g : α → σ
h : α → β × List β × σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : α → List β × σ := fun a ↦ List.foldr (fun b s ↦ (b :: s.1, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
head✝ : β
tail✝ : List β
tail_ih✝ :
  List.foldr (fun b s ↦ (b :: s.1, h a (b, s))) ([], g a) tail✝ =
    (tail✝, List.rec (g a) (fun b l IH ↦ h a (b, l, IH)) tail✝)
⊢ List.foldr (fun b s ↦ (b :: s.1, h a (b, s))) ([], g a) (head✝ :: tail✝) =
    (head✝ :: tail✝, List.rec (g a) (fun b l IH ↦ h a (b, l, IH)) (head✝ :: tail✝))
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case false
n : ℕ
H : n.bodd = false
⊢ (id n % 2 == 1) = false

pp: case true
n : ℕ
H : n.bodd = true
⊢ (id n % 2 == 1) = true

Tactic:
<;>

Goal state after:
case false
n : ℕ
H : n.bodd = false
⊢ (id n % 2 == 1) = false

case true
n : ℕ
H : n.bodd = true
⊢ (id n % 2 == 1) = true
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case false
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ encode
      (bif false then Option.map (fun b ↦ 2 * encode b + 1) (decode n.div2)
      else Option.map (fun b ↦ 2 * encode b) (decode n.div2)) =
    encode
      (match false, n.div2 with
      | false, m => Option.map Sum.inl (decode m)
      | x, m => Option.map Sum.inr (decode m))

pp: case true
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ encode
      (bif true then Option.map (fun b ↦ 2 * encode b + 1) (decode n.div2)
      else Option.map (fun b ↦ 2 * encode b) (decode n.div2)) =
    encode
      (match true, n.div2 with
      | false, m => Option.map Sum.inl (decode m)
      | x, m => Option.map Sum.inr (decode m))

Tactic:
<;>

Goal state after:
case false
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ encode
      (bif false then Option.map (fun b ↦ 2 * encode b + 1) (decode n.div2)
      else Option.map (fun b ↦ 2 * encode b) (decode n.div2)) =
    encode
      (match false, n.div2 with
      | false, m => Option.map Sum.inl (decode m)
      | x, m => Option.map Sum.inr (decode m))

case true
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ encode
      (bif true then Option.map (fun b ↦ 2 * encode b + 1) (decode n.div2)
      else Option.map (fun b ↦ 2 * encode b) (decode n.div2)) =
    encode
      (match true, n.div2 with
      | false, m => Option.map Sum.inl (decode m)
      | x, m => Option.map Sum.inr (decode m))
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case false.none
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ encode (Option.map (fun b ↦ 2 * encode b) none) = encode (Option.map Sum.inl none)

pp: case false.some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ encode (Option.map (fun b ↦ 2 * encode b) (some val✝)) = encode (Option.map Sum.inl (some val✝))

Tactic:
<;>

Goal state after:
case false.none
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ encode (Option.map (fun b ↦ 2 * encode b) none) = encode (Option.map Sum.inl none)

case false.some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ encode (Option.map (fun b ↦ 2 * encode b) (some val✝)) = encode (Option.map Sum.inl (some val✝))
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case true.none
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ encode (Option.map (fun b ↦ 2 * encode b + 1) none) = encode (Option.map Sum.inr none)

pp: case true.some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : β
⊢ encode (Option.map (fun b ↦ 2 * encode b + 1) (some val✝)) = encode (Option.map Sum.inr (some val✝))

Tactic:
<;>

Goal state after:
case true.none
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ encode (Option.map (fun b ↦ 2 * encode b + 1) none) = encode (Option.map Sum.inr none)

case true.some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : β
⊢ encode (Option.map (fun b ↦ 2 * encode b + 1) (some val✝)) = encode (Option.map Sum.inr (some val✝))