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

Goal state before:
pp: p : ℕ × ℕ
⊢ ¬p.2 ≤ p.1 ↔ (fun x1 x2 ↦ x1 < x2) p.1 p.2

Tactic:
simp

Goal state after:
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))

Tactic:
simp

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

Goal state before:
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:
simp

Goal state after:
case true
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ encode (Option.map (fun b ↦ 2 * encode b + 1) (decode n.div2)) = encode (Option.map Sum.inr (decode n.div2))
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)
a : ∀ k_1 ≤ k, false ∈ p k_1
⊢ Acc (lbp p) (k + 1)

Tactic:
| succ m IH =>

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

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

Tactic:
simp

Goal state after:
n : ℕ
⊢ Nat.rec [] (fun n IH ↦ IH ++ [n]) n = List.range n
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

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
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 (Option.map (fun a ↦ ↑(f a)) (some a)) = encode (Option.map f (some a))

Tactic:
simp

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.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)

Tactic:
simp

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

Goal state before:
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:
simp

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

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)
this : Primrec₂ fun a n ↦ List.map (f a) (List.range n)
a : α
n : ℕ
⊢ (List.map (f (a, n).1) (List.range (a, n).2.succ))[(a, n).2]? = some (f a n)

Tactic:
simp

Goal state after:
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

Tactic:
simp

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

Goal state before:
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:
simp

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Nat.Partrec ↑f✝
pg : Nat.Partrec ↑g✝
n : ℕ
⊢ f✝ (g✝ n) ∈ ↑g✝ n >>= ↑f✝

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case prec.zero
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Nat.Partrec ↑f✝
pg : Nat.Partrec ↑g✝
n : ℕ
⊢ Nat.rec (f✝ (unpair n).1) (fun y IH ↦ g✝ (Nat.pair (unpair n).1 (Nat.pair y IH))) 0 ∈
    Nat.rec (Part.some (f✝ (unpair n).1))
      (fun y IH ↦ IH.bind fun i ↦ Part.some (g✝ (Nat.pair (unpair n).1 (Nat.pair y i)))) 0

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case prec.succ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Nat.Partrec ↑f✝
pg : Nat.Partrec ↑g✝
n m : ℕ
IH :
  Nat.rec (f✝ (unpair n).1) (fun y IH ↦ g✝ (Nat.pair (unpair n).1 (Nat.pair y IH))) m ∈
    Nat.rec (Part.some (f✝ (unpair n).1))
      (fun y IH ↦ IH.bind fun i ↦ Part.some (g✝ (Nat.pair (unpair n).1 (Nat.pair y i)))) m
⊢ Nat.rec (f✝ (unpair n).1) (fun y IH ↦ g✝ (Nat.pair (unpair n).1 (Nat.pair y IH))) (m + 1) ∈
    Nat.rec (Part.some (f✝ (unpair n).1))
      (fun y IH ↦ IH.bind fun i ↦ Part.some (g✝ (Nat.pair (unpair n).1 (Nat.pair y i)))) (m + 1)

Tactic:
| succ m IH =>

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: this : Primrec₂ fun n m ↦ if n = m.succ then 0 else 1
⊢ ∀ (a : ℕ),
    a ∉ Nat.rfind fun n ↦ (fun m ↦ decide (m = 0)) <$> ↑(unpaired fun n m ↦ if n = m.succ then 0 else 1) (Nat.pair 0 n)

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: this : Primrec₂ fun n m ↦ if n = m.succ then 0 else 1
n✝ : ℕ
⊢ n✝ ∈
    Nat.rfind fun n ↦
      (fun m ↦ decide (m = 0)) <$> ↑(unpaired fun n m ↦ if n = m.succ then 0 else 1) (Nat.pair (n✝ + 1) n)

Tactic:
simp

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 : ℕ
⊢ (do
      let n ← (↑fun n ↦ encode (Option.map f (decode n))) n
      ↑n.ppred) =
    (↑(decode n)).bind fun a ↦ map encode (↑f a)

Tactic:
simp

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))
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))

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
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:
simp

Goal state after:
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)

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
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:
simp

Goal state after:
case some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
a : α
⊢ ↑(encode (f a)).ppred = map encode ↑(f 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

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
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:
simp

Goal state after:
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)

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
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:
simp

Goal state after:
Module: Mathlib.Computability.Partrec

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

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.Partrec

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

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.Partrec

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

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.Partrec

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

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
a b c : V
M2 : (G ⊔ edge a c).Subgraph
hab : G.Adj a b
hnGac : ¬G.Adj a c
hnac : a ≠ c
hnbc : b ≠ c
hM2 : M2.IsPerfectMatching
hM2ac : M2.Adj a c
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
x' : V
M1 : (G ⊔ edge x' b).Subgraph
hxa : G.Adj x' a
hnGxb : ¬G.Adj x' b
hnxb : x' ≠ b
hnxc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x' b
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x' b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x' b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x' b
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x' b
hxc : x' ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
p : cycles.Walk a x'
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x' b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ {x'_1 : V}, x'_1 ∈ {x', b} → ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x'_1 → M2.Adj c' x'_1
⊢ x' ∈ {x', b}

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.Partrec

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

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.Partrec

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

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.Partrec

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Computable₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = Option.some (f a n)
this : Computable₂ fun a n ↦ List.map (f a) (List.range n)
a : α × ℕ
⊢ (fun a b ↦ (List.map (f (a, b).1) (List.range (a, b).2.succ))[(a, b).2]?) a.1 a.2 = Option.some (f a.1 a.2)

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : Fin n → α → σ
hf : ∀ (i : Fin n), Computable (f i)
a : α
⊢ (Vector.mOfFn fun i ↦ ↑(f i) a) = (↑fun a ↦ List.Vector.ofFn fun i ↦ f i a) a

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ →. σ
hf : Computable f
hg : Computable₂ g
hh : Partrec₂ h
this :
  Partrec fun a ↦
    Option.casesOn (Sum.casesOn (f a) (fun x ↦ Option.none) Option.some)
      (Part.some (Sum.casesOn (f a) (fun b ↦ Option.some (g a b)) fun x ↦ Option.none)) fun c ↦
      Part.map Option.some (h a c)
a : α
val✝ : β
⊢ (Option.casesOn (Sum.casesOn (Sum.inl val✝) (fun x ↦ Option.none) Option.some)
      (Part.some (Sum.casesOn (Sum.inl val✝) (fun b ↦ Option.some (g a b)) fun x ↦ Option.none)) fun c ↦
      Part.map Option.some (h a c)) =
    Part.map Option.some (Sum.casesOn (Sum.inl val✝) (fun b ↦ Part.some (g a b)) (h a))

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ →. σ
hf : Computable f
hg : Computable₂ g
hh : Partrec₂ h
this :
  Partrec fun a ↦
    Option.casesOn (Sum.casesOn (f a) (fun x ↦ Option.none) Option.some)
      (Part.some (Sum.casesOn (f a) (fun b ↦ Option.some (g a b)) fun x ↦ Option.none)) fun c ↦
      Part.map Option.some (h a c)
a : α
val✝ : γ
⊢ (Option.casesOn (Sum.casesOn (Sum.inr val✝) (fun x ↦ Option.none) Option.some)
      (Part.some (Sum.casesOn (Sum.inr val✝) (fun b ↦ Option.some (g a b)) fun x ↦ Option.none)) fun c ↦
      Part.map Option.some (h a c)) =
    Part.map Option.some (Sum.casesOn (Sum.inr val✝) (fun b ↦ Part.some (g a b)) (h a))

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β →. σ
h : α → γ → σ
hf : Computable f
hg : Partrec₂ g
hh : Computable₂ h
a : α
val✝ : β
⊢ Sum.casesOn (Sum.casesOn (Sum.inl val✝) (fun b ↦ Sum.inr (a, b).2) fun b ↦ Sum.inl (a, b).2)
      (fun b ↦ Part.some (h a b)) (g a) =
    Sum.casesOn (Sum.inl val✝) (g a) fun c ↦ Part.some (h a c)

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β →. σ
h : α → γ → σ
hf : Computable f
hg : Partrec₂ g
hh : Computable₂ h
a : α
val✝ : γ
⊢ Sum.casesOn (Sum.casesOn (Sum.inr val✝) (fun b ↦ Sum.inr (a, b).2) fun b ↦ Sum.inl (a, b).2)
      (fun b ↦ Part.some (h a b)) (g a) =
    Sum.casesOn (Sum.inr val✝) (g a) fun c ↦ Part.some (h a c)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : Primcodable α
w✝ : DecidablePred p
hf : Primrec fun a ↦ decide (p a)
⊢ ∀ (a : List α), ¬(filter (fun x ↦ decide (p x)) a).length = 0 ↔ ∃ a_1 ∈ a, p a_1

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : Primcodable α
w✝ : DecidablePred p
hf : Primrec fun a ↦ decide (p a)
⊢ ∀ (a : List α), (filter (fun x ↦ decide (p x)) a).length = a.length ↔ ∀ a_1 ∈ a, p a_1

Tactic:
simp

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

Goal state before:
pp: p : ℕ → Prop
hf : PrimrecPred p
⊢ ∀ (a : ℕ), (∃ a_1 ∈ range a, p a_1) ↔ ∃ x < a, p x

Tactic:
simp

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

Goal state before:
pp: p : ℕ → Prop
hf : PrimrecPred p
⊢ ∀ (a : ℕ), (∀ a_1 ∈ range a, p a_1) ↔ ∀ x < a, p x

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
inst✝¹ : Primcodable α
inst✝ : Primcodable β
hf : PrimrecRel R
L : List α
b : β
⊢ (filter (fun x ↦ decide (R x b)) L).length ≠ 0 ↔ ∃ a ∈ L, R a b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
inst✝¹ : Primcodable α
inst✝ : Primcodable β
hf : PrimrecRel R
L : List α
b : β
⊢ (filter (fun x ↦ decide (R x b)) L).length = L.length ↔ ∀ a ∈ L, R a b

Tactic:
simp

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: case succ
α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
n : ℕ
h₂ : Sum.inl b ∈ F a n
_x : ∃ b', Sum.inl b' ∈ F a n
h₁ : ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m
m : ℕ
IH : ∀ (a' : α), Sum.inr a' ∈ F a m → b ∈ f.fix a' → b ∈ f.fix a
a' : α
ba : b ∈ f.fix a'
am :
  ∃ b,
    Sum.inr b ∈
        Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.rec (fun val ↦ Part.some s) (fun val ↦ f val) s)
          m ∧
      Sum.inr a' ∈ f b
⊢ b ∈ f.fix a

Tactic:
| succ m IH =>

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

Goal state before:
pp: R : ℕ → ℕ → Prop
hf : PrimrecRel R
⊢ ∀ (a : ℕ × ℕ), (∃ a_1 ∈ range a.1, R a_1 a.2) ↔ (fun n y ↦ ∃ x < n, R x y) a.1 a.2

Tactic:
simp

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

Goal state before:
pp: R : ℕ → ℕ → Prop
hf : PrimrecRel R
⊢ ∀ (a : ℕ × ℕ), (∀ a_1 ∈ range a.1, R a_1 a.2) ↔ (fun n y ↦ ∀ x < n, R x y) a.1 a.2

Tactic:
simp

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

Goal state before:
pp: σ : Type u_3
inst✝ : Primcodable σ
n : ℕ
x✝ : (Fin n → σ) × Fin n
v : Fin n → σ
i : Fin n
⊢ (List.Vector.ofFn (v, i).1).get (v, i).2 = id (v, i).1 (v, i).2

Tactic:
simp

Goal state after: