mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
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
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
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
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
p : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp : p.IsCycle ∧ p.toSubgraph.verts = (cycles.connectedComponentMk c).supp
p' : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp' : p'.IsCycle ∧ p'.snd = c ∧ p'.toSubgraph.verts = p.toSubgraph.verts
x' : V
hx' : x' ∈ {x, b}
hx'p : x' ∈ p'.support
htw : ∀ t ∈ {x, b}, t ∈ (p'.takeUntil x' hx'p).support → t = x'
h : (p'.takeUntil x' hx'p).toSubgraph.Adj x b
⊢ b ∈ {x, b}

Tactic:
by

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

Goal state before:
pp: α : 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 (o a)) (encode (f a)) fun b ↦
      (encode ((decode (encode (a, b).1)).bind fun a ↦ Option.map (g a) (decode b))).pred) =
    encode (Option.casesOn (o a) (f a) (g a))

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
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
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
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
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
p : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp : p.IsCycle ∧ p.toSubgraph.verts = (cycles.connectedComponentMk c).supp
p' : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp' : p'.IsCycle ∧ p'.snd = c ∧ p'.toSubgraph.verts = p.toSubgraph.verts
x' : V
hx' : x' ∈ {x, b}
hx'p : x' ∈ p'.support
htw : ∀ t ∈ {x, b}, t ∈ (p'.takeUntil x' hx'p).support → t = x'
h : (p'.takeUntil x' hx'p).toSubgraph.Adj x b
⊢ x ∈ {x, b}

Tactic:
by

Goal state after:
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 : α → Option β
g : α → β → Option σ
hf : Primrec f
hg : Primrec₂ g
a : α
⊢ Option.casesOn (f a) none (g a) = (f a).bind (g a)

Tactic:
by

Goal state after:
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 : α → Option β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
x : α
⊢ ((f x).bind fun b ↦ some (g x b)) = Option.map (g x) (f x)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
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 : α → β → Option σ
h : Primrec₂ fun a n ↦ (decode n).bind (f a)
⊢ Primrec₂ f

Tactic:
by

Goal state after:
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 a n ↦ Option.map (f a) (decode n)) ↔ Primrec₂ f

Tactic:
by

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

Goal state before:
pp: α : 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 (c a)) (g a) fun b ↦ f (a, b).1) = bif c a then f a else g a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable σ
c : α → Prop
inst✝ : DecidablePred c
f g : α → σ
hc : PrimrecPred c
hf : Primrec f
hg : Primrec g
⊢ Primrec fun a ↦ if c a then f a else g a

Tactic:
by

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

Goal state before:
pp: p : ℕ × ℕ
⊢ (Nat.casesOn ((fun x1 x2 ↦ x1 - x2) p.1 p.2) true fun b ↦ false) = (fun a b ↦ decide (a ≤ b)) p.1 p.2

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
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
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
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
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
p : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp : p.IsCycle ∧ p.toSubgraph.verts = (cycles.connectedComponentMk c).supp
p' : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp' : p'.IsCycle ∧ p'.snd = c ∧ p'.toSubgraph.verts = p.toSubgraph.verts
x' : V
hx' : x' ∈ {x, b}
hx'p : x' ∈ p'.support
htw : ∀ t ∈ {x, b}, t ∈ (p'.takeUntil x' hx'p).support → t = x'
⊢ (p'.takeUntil x' hx'p).toSubgraph.Adj a (p'.takeUntil x' hx'p).snd

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
p : α → Prop
w✝ : DecidablePred p
hp : Primrec fun a ↦ decide (p a)
⊢ ∀ (n : α), (!decide (p n)) = decide ¬p n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
p q : α → Prop
w✝¹ : DecidablePred p
hp : Primrec fun a ↦ decide (p a)
w✝ : DecidablePred q
hq : Primrec fun a ↦ decide (q a)
⊢ ∀ (n : α), (decide (p n) && decide (q n)) = decide (p n ∧ q n)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
p q : α → Prop
w✝¹ : DecidablePred p
hp : Primrec fun a ↦ decide (p a)
w✝ : DecidablePred q
hq : Primrec fun a ↦ decide (q a)
⊢ ∀ (n : α), (decide (p n) || decide (q n)) = decide (p n ∨ q n)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
a : ℕ × ℕ
⊢ (fun x1 x2 ↦ x1 ≤ x2) a.1 a.2 ∧ swap (fun x1 x2 ↦ x1 ≤ x2) a.1 a.2 ↔ (fun a b ↦ a = b) a.1 a.2

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : α → β → Prop
inst✝ : DecidableRel p
hp : PrimrecRel p
f : α → β
hf : Primrec f
⊢ PrimrecPred fun a ↦ (fun b ↦ decide (p a b)) (f a) = true

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
⊢ Primrec₂ fun p ↦ encode

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
⊢ Primrec₂ fun p a ↦ p.1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
hp : Primrec₂ p
a : β
l : List β
n : α
⊢ (bif p (id n) a then 0 else (List.findIdx (p n) l).succ) = List.findIdx (p n) (a :: l)

Tactic:
by

Goal state after:
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
this : ∀ (m k : ℕ), n ≤ k + m → Acc (lbp p) k
⊢ ∀ (a : ℕ), Acc (lbp p) a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable σ
inst✝ : Finite α
f : α → σ
l : List α
left✝ : l.Nodup
m : ∀ (x : α), x ∈ l
⊢ Primrec fun a ↦ some (f a)

Tactic:
by

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

Goal state before:
pp: α : 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 : ℕ
⊢ encode
      (List.foldl (fun o m ↦ (decode m).bind fun a ↦ Option.map (List.cons (encode a)) o) (some [])
        (ofNat (List ℕ) n).reverse) =
    encode (decode n)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : 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) (f x) = Nat.findGreatest (p x) (f x)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
f : α → ℕ
h₁ : PrimrecBounded f
h₂ : PrimrecRel fun a b ↦ f a = b
⊢ Primrec f

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : 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 : α
this : F a = (f a, List.recOn (f a) (g a) fun b l IH ↦ h a (b, l, IH))
⊢ (F a).2 = List.recOn (f a) (g a) fun b l IH ↦ h a (b, l, IH)

Tactic:
by

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

Goal state before:
pp: this : PrimrecRel fun a b ↦ a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2
a k q : ℕ
H : ¬k = 0
⊢ q * k ≤ a ∧ a < (q + 1) * k ↔ q = a / k

Tactic:
by

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

Goal state before:
pp: ⊢ Primrec₂ fun x1 x2 ↦ x1 / x2

Tactic:
by

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

Goal state before:
pp: m n : ℕ
⊢ (m, n).1 - (m, n).2 * (fun x1 x2 ↦ x1 / x2) (m, n).1 (m, n).2 = m % n

Tactic:
by

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

Goal state before:
pp: α : 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 : α
⊢ (F a).2 = List.recOn (f a) (g a) fun b l IH ↦ h a (b, l, IH)

Tactic:
by

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

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

Tactic:
by

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

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
⊢ ∀ (a : ℕ), Acc (lbp p) a

Tactic:
by

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

Goal state before:
pp: α : 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 : α
⊢ (bif (encode (f a)).bodd then Option.map (h a) (decode (encode (f a)).div2)
    else Option.map (g a) (decode (encode (f a)).div2)) =
    some (Sum.casesOn (f a) (g a) (h a))

Tactic:
by

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

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

Tactic:
rcases @decode α _ n with - | a

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.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.casesOn (F (l, n).1 (l, n).2) (fun x ↦ none) some = l[n]?

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
d : α
⊢ Primrec₂ fun l n ↦ l.getD n d

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
n : ℕ
⊢ fin.toEncodable = Fin.encodable n

Tactic:
by

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

Goal state before:
pp: α : 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) [] (f a) = List.map (g a) (f a)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
⊢ PrimrecPred fun p ↦ (fun a ↦ decide (encode a = p.1)) p.2 = true

Tactic:
by

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:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
⊢ Primrec Subtype.val

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
l : List α
⊢ List.foldr (fun b s ↦ (fun a b ↦ (a, b).2.2.succ) (l, b, s).1 (l, b, s).2) 0 (id l) = l.length

Tactic:
by

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

Goal state before:
pp: α : 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)) (decode n)) = encode (Option.map f (decode n))

Tactic:
rcases @decode α _ n with - | a

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

Goal state before:
pp: p : ℕ →. Bool
H : ∃ n, true ∈ p n ∧ ∀ k < n, (p k).Dom
m : ℕ
IH : (y : ℕ) → lbp p y m → (∀ n < y, false ∈ p n) → { n // true ∈ p n ∧ ∀ m < n, false ∈ p m }
al : ∀ n < m, false ∈ p n
⊢ (p m).Dom

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Primcodable α
p : α → Prop
inst✝ : DecidablePred p
hf : PrimrecPred p
⊢ Primrec fun L ↦ List.filter (fun x ↦ decide (p x)) L

Tactic:
by

Goal state after:
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, s).1 (a, b, s).2.1 then 0 else (a, b, s).2.2.succ) 0 (f a) =
    List.findIdx (p a) (f a)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
⊢ (Primrec fun a ↦ ↑(f a)) ↔ Primrec f

Tactic:
by

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)
a : α
n : ℕ
⊢ Nat.rec (some [])
      (fun n IH ↦
        (a, n, IH).2.2.bind fun b ↦
          Option.map (fun b_1 ↦ (((a, n, IH), b), b_1).1.2 ++ [(((a, n, IH), b), b_1).2])
            (g ((a, n, IH), b).1.1 ((a, n, IH), b).2))
      n =
    some (List.map (f a) (List.range n))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
h : ∀ (a : α), (f a).isSome = true
⊢ Primrec f → Primrec fun a ↦ (f a).get ⋯

Tactic:
by

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:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
n : ℕ
f : α → Fin n
this : Primcodable { a // a < n } := Primcodable.subtype ⋯
⊢ (Primrec fun a ↦ ↑(f a)) ↔ Primrec fun a ↦ ↑(Fin.equivSubtype (f a))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
n : ℕ
f : α → Fin n
⊢ (Primrec fun a ↦ ↑(f a)) ↔ Primrec f

Tactic:
by

Goal state after: