ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>l : Language α<GOAL>l + l = l
<VAR>α : Type u_1<VAR>l : Language α<GOAL>(Language.map id) l = l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>g : β → γ<VAR>f : α → β<VAR>l : Language α<GOAL>(Language.map g) ((Language.map f) l) = (Language.map (g ∘ f)) l
<VAR>α : Type u_1<VAR>l : Language α<VAR>x : List α<GOAL>x ∈ l∗ ↔ ∃ S, x = S.join ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []
<VAR>α : Type u_1<VAR>l : Language α<GOAL>l∗ = {x | ∃ S, x = S.join ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []}
<VAR>α : Type u_1<VAR>l m : Language α<GOAL>l ≤ m ↔ l + m = m
<VAR>α : Type u_1<VAR>l₁ l₂ m₁ m₂ : Language α<GOAL>l₁ ≤ m₁ → l₂ ≤ m₂ → l₁ * l₂ ≤ m₁ * m₂
<VAR>α : Type u_1<VAR>l₁ l₂ m₁ m₂ : Language α<GOAL>l₁ ≤ m₁ → l₂ ≤ m₂ → l₁ + l₂ ≤ m₁ + m₂
<VAR>α : Type u_1<VAR>ι : Sort v<VAR>l : ι → Language α<VAR>x : List α<GOAL>x ∈ ⨆ i, l i ↔ ∃ i, x ∈ l i
<VAR>α : Type u_1<VAR>ι : Sort v<VAR>l : ι → Language α<VAR>m : Language α<GOAL>(⨆ i, l i) * m = ⨆ i, l i * m
<VAR>α : Type u_1<VAR>ι : Sort v<VAR>l : ι → Language α<VAR>m : Language α<GOAL>m * ⨆ i, l i = ⨆ i, m * l i
<VAR>α : Type u_1<VAR>ι : Sort v<VAR>Nonempty ι<VAR>l : ι → Language α<VAR>m : Language α<GOAL>(⨆ i, l i) + m = ⨆ i, l i + m
<VAR>α : Type u_1<VAR>ι : Sort v<VAR>Nonempty ι<VAR>l : ι → Language α<VAR>m : Language α<GOAL>m + ⨆ i, l i = ⨆ i, m + l i
<VAR>α : Type u_1<VAR>l : Language α<VAR>x : List α<VAR>n : ℕ<GOAL>x ∈ l ^ n ↔ ∃ S, x = S.join ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l
<VAR>α : Type u_1<VAR>l : Language α<GOAL>l∗ = ⨆ i, l ^ i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l : Language α<GOAL>(Language.map f) l∗ = ((Language.map f) l)∗
<VAR>α : Type u_1<VAR>l : Language α<GOAL>l∗ * l = l * l∗
<VAR>α : Type u_1<VAR>l : Language α<GOAL>1 + l * l∗ = l∗
<VAR>α : Type u_1<VAR>l : Language α<GOAL>1 + l∗ * l = l∗
<VAR>α : Type u_1<VAR>l : Language α<VAR>a : List α<GOAL>a ∈ l.reverse ↔ a.reverse ∈ l
<VAR>α : Type u_1<VAR>l : Language α<VAR>a : List α<GOAL>a.reverse ∈ l.reverse ↔ a ∈ l
<VAR>α : Type u_1<VAR>l : Language α<GOAL>l.reverse = List.reverse '' l
<VAR>α : Type u_1<GOAL>Language.reverse 0 = 0
<VAR>α : Type u_1<GOAL>Language.reverse 1 = 1
<VAR>α : Type u_1<GOAL>Function.Involutive Language.reverse
<VAR>α : Type u_1<GOAL>Function.Bijective Language.reverse
<VAR>α : Type u_1<GOAL>Function.Injective Language.reverse
<VAR>α : Type u_1<GOAL>Function.Surjective Language.reverse
<VAR>α : Type u_1<VAR>l : Language α<GOAL>l.reverse.reverse = l
<VAR>α : Type u_1<VAR>l m : Language α<GOAL>(l + m).reverse = l.reverse + m.reverse
<VAR>α : Type u_1<VAR>l m : Language α<GOAL>(l * m).reverse = m.reverse * l.reverse
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : ι → Language α<GOAL>(⨆ i, l i).reverse = ⨆ i, (l i).reverse
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : ι → Language α<GOAL>(⨅ i, l i).reverse = ⨅ i, (l i).reverse
<VAR>α : Type u_1<VAR>l : Language α<GOAL>(Language.reverseIso α) l = MulOpposite.op l.reverse
<VAR>α : Type u_1<VAR>l' : (Language α)ᵐᵒᵖ<GOAL>(Language.reverseIso α).symm l' = (MulOpposite.unop l').reverse
<VAR>α : Type u_1<VAR>l : Language α<VAR>n : ℕ<GOAL>(l ^ n).reverse = l.reverse ^ n
<VAR>α : Type u_1<VAR>l : Language α<GOAL>l∗.reverse = l.reverse∗
<VAR>σ : Type u_1<VAR>f : σ → Option σ<VAR>a : σ<VAR>b : Option σ<VAR>self : Turing.EvalsTo f a b<GOAL>(flip bind f)^[self.steps] (some a) = b
<VAR>σ : Type u_1<VAR>f : σ → Option σ<VAR>a : σ<VAR>b : Option σ<VAR>m : ℕ<VAR>self : Turing.EvalsToInTime f a b m<GOAL>self.steps ≤ m
<VAR>p : ℕ →. Bool<VAR>n : ℕ<VAR>h : n ∈ Nat.rfind p<GOAL>true ∈ p n
<VAR>p : ℕ →. Bool<VAR>n : ℕ<VAR>h : n ∈ Nat.rfind p<VAR>m : ℕ<GOAL>m < n → false ∈ p m
<VAR>p : ℕ →. Bool<GOAL>(Nat.rfind p).Dom ↔ ∃ n, true ∈ p n ∧ ∀ {m : ℕ}, m < n → (p m).Dom
<VAR>p : ℕ →. Bool<GOAL>(Nat.rfind p).Dom ↔ ∃ n, true ∈ p n ∧ ∀ {m : ℕ}, m ≤ n → (p m).Dom
<VAR>p : ℕ →. Bool<VAR>n : ℕ<GOAL>n ∈ Nat.rfind p ↔ true ∈ p n ∧ ∀ {m : ℕ}, m < n → false ∈ p m
<VAR>p : ℕ → Bool<VAR>m : ℕ<VAR>pm : p m = true<GOAL>∃ n ∈ Nat.rfind ↑p, n ≤ m
<VAR>p : ℕ →. Bool<VAR>p0 : p 0 = Part.none<GOAL>Nat.rfind p = Part.none
<VAR>α : Type u_1<VAR>f : ℕ → Option α<VAR>a : α<VAR>h : a ∈ Nat.rfindOpt f<GOAL>∃ n, a ∈ f n
<VAR>α : Type u_1<VAR>f : ℕ → Option α<GOAL>(Nat.rfindOpt f).Dom ↔ ∃ n a, a ∈ f n
<VAR>α : Type u_1<VAR>f : ℕ → Option α<VAR>H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n<VAR>a : α<GOAL>a ∈ Nat.rfindOpt f ↔ ∃ n, a ∈ f n
<VAR>f g : ℕ →. ℕ<VAR>hf : Nat.Partrec f<VAR>H : ∀ (n : ℕ), f n = g n<GOAL>Nat.Partrec g
<VAR>f : ℕ →. ℕ<VAR>g : ℕ → ℕ<VAR>hf : Nat.Partrec f<VAR>H : ∀ (n : ℕ), g n ∈ f n<GOAL>Nat.Partrec ↑g
<VAR>f : ℕ → ℕ<VAR>hf : Nat.Primrec f<GOAL>Nat.Partrec ↑f
<VAR>f g h : ℕ →. ℕ<VAR>hf : Nat.Partrec f<VAR>hg : Nat.Partrec g<VAR>hh : Nat.Partrec h<GOAL>Nat.Partrec fun a => (f a).bind fun n => Nat.rec (g a) (fun y IH => do let i ← IH h (Nat.pair a (Nat.pair y i))) n
<GOAL>Nat.Partrec fun n => ↑n.ppred
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>Primcodable α<VAR>Primcodable σ<VAR>f : α → σ<VAR>hf : Primrec f<GOAL>Computable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α → β → σ<VAR>hf : Primrec₂ f<GOAL>Computable₂ f
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>Primcodable α<VAR>Primcodable σ<VAR>f : α → σ<VAR>hf : Computable f<GOAL>Partrec ↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α → β → σ<VAR>hf : Computable₂ f<GOAL>Partrec₂ fun a => ↑(f a)
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<VAR>f g : α → σ<VAR>hf : Computable f<VAR>H : ∀ (n : α), f n = g n<GOAL>Computable g
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<VAR>s : σ<GOAL>Computable fun x => s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>f : α → Option β<VAR>hf : Computable f<GOAL>Partrec fun a => ↑(f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α × β → σ<VAR>hf : Computable f<GOAL>Computable₂ fun a b => f (a, b)
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Computable id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<GOAL>Computable Prod.fst
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<GOAL>Computable Prod.snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>f : α → β<VAR>g : α → γ<VAR>hf : Computable f<VAR>hg : Computable g<GOAL>Computable fun a => (f a, g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<GOAL>Computable Sum.inl
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<GOAL>Computable Sum.inr
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Computable₂ List.cons
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Computable List.reverse
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Computable₂ List.get?
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Computable₂ fun x x_1 => x ++ x_1
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Computable₂ fun l a => l ++ [a]
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Computable List.length
<VAR>α : Type u_1<VAR>Primcodable α<VAR>n : ℕ<GOAL>Computable₂ Mathlib.Vector.cons
<VAR>α : Type u_1<VAR>Primcodable α<VAR>n : ℕ<GOAL>Computable Mathlib.Vector.toList
<VAR>α : Type u_1<VAR>Primcodable α<VAR>n : ℕ<GOAL>Computable Mathlib.Vector.length
<VAR>α : Type u_1<VAR>Primcodable α<VAR>n : ℕ<GOAL>Computable Mathlib.Vector.head
<VAR>α : Type u_1<VAR>Primcodable α<VAR>n : ℕ<GOAL>Computable Mathlib.Vector.tail
<VAR>α : Type u_1<VAR>Primcodable α<VAR>n : ℕ<GOAL>Computable₂ Mathlib.Vector.get
<VAR>α : Type u_1<VAR>Primcodable α<VAR>n : ℕ<GOAL>Computable Mathlib.Vector.ofFn
<VAR>σ : Type u_4<VAR>Primcodable σ<VAR>n : ℕ<GOAL>Computable₂ id
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Computable Encodable.encode
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Computable Encodable.decode
<VAR>α : Type u_5<VAR>Denumerable α<GOAL>Computable (Denumerable.ofNat α)
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<VAR>f : α → σ<GOAL>(Computable fun a => Encodable.encode (f a)) ↔ Computable f
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Computable some
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<VAR>f g : α →. σ<VAR>hf : Partrec f<VAR>H : ∀ (n : α), f n = g n<GOAL>Partrec g
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<VAR>f : α →. σ<VAR>g : α → σ<VAR>hf : Partrec f<VAR>H : ∀ (n : α), g n ∈ f n<GOAL>Computable g
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<GOAL>Partrec fun x => Part.none
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Partrec Part.some
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<VAR>s : Part σ<VAR>Decidable s.Dom<GOAL>Partrec fun x => s
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<VAR>s : Part σ<GOAL>Partrec fun x => s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α →. β<VAR>g : α → β →. σ<VAR>hf : Partrec f<VAR>hg : Partrec₂ g<GOAL>Partrec fun a => (f a).bind (g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α →. β<VAR>g : α → β → σ<VAR>hf : Partrec f<VAR>hg : Computable₂ g<GOAL>Partrec fun a => Part.map (g a) (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α × β →. σ<VAR>hf : Partrec f<GOAL>Partrec₂ fun a b => f (a, b)
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<VAR>f : α → ℕ<VAR>g : α →. σ<VAR>h : α → ℕ × σ →. σ<VAR>hf : Computable f<VAR>hg : Partrec g<VAR>hh : Partrec₂ h<GOAL>Partrec fun a => Nat.rec (g a) (fun y IH => IH.bind fun i => h a (y, i)) (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : β →. σ<VAR>g : α → β<VAR>hf : Partrec f<VAR>hg : Computable g<GOAL>Partrec fun a => f (g a)
<VAR>f : ℕ →. ℕ<GOAL>Partrec f ↔ Nat.Partrec f
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<VAR>f : α →. σ<GOAL>(Partrec fun a => Part.map Encodable.encode (f a)) ↔ Partrec f
<VAR>α : Type u_1<VAR>Primcodable α<VAR>f : ℕ → ℕ →. α<GOAL>Partrec (Nat.unpaired f) ↔ Partrec₂ f
<VAR>f : ℕ → ℕ →. ℕ<GOAL>Nat.Partrec (Nat.unpaired f) ↔ Partrec₂ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_5<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>Primcodable σ<VAR>f : β → γ →. σ<VAR>g : α → β<VAR>h : α → γ<VAR>hf : Partrec₂ f<VAR>hg : Computable g<VAR>hh : Computable h<GOAL>Partrec fun a => f (g a) (h a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>σ : Type u_5<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>Primcodable δ<VAR>Primcodable σ<VAR>f : γ → δ →. σ<VAR>g : α → β → γ<VAR>h : α → β → δ<VAR>hf : Partrec₂ f<VAR>hg : Computable₂ g<VAR>hh : Computable₂ h<GOAL>Partrec₂ fun a b => f (g a b) (h a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : β → σ<VAR>g : α → β<VAR>hf : Computable f<VAR>hg : Computable g<GOAL>Computable fun a => f (g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>Primcodable σ<VAR>f : γ → σ<VAR>g : α → β → γ<VAR>hf : Computable f<VAR>hg : Computable₂ g<GOAL>Computable₂ fun a b => f (g a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_5<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α → β → σ<VAR>hf : Computable fun p => f p.1 p.2<GOAL>Computable₂ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_5<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>Primcodable σ<VAR>f : β → γ → σ<VAR>g : α → β<VAR>h : α → γ<VAR>hf : Computable₂ f<VAR>hg : Computable g<VAR>hh : Computable h<GOAL>Computable fun a => f (g a) (h a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>σ : Type u_5<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>Primcodable δ<VAR>Primcodable σ<VAR>f : γ → δ → σ<VAR>g : α → β → γ<VAR>h : α → β → δ<VAR>hf : Computable₂ f<VAR>hg : Computable₂ g<VAR>hh : Computable₂ h<GOAL>Computable₂ fun a b => f (g a b) (h a b)
<VAR>α : Type u_1<VAR>Primcodable α<VAR>p : α → ℕ →. Bool<VAR>hp : Partrec₂ p<GOAL>Partrec fun a => Nat.rfind (p a)
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<VAR>f : α → ℕ → Option σ<VAR>hf : Computable₂ f<GOAL>Partrec fun a => Nat.rfindOpt (f a)
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<VAR>f : α → ℕ<VAR>g : α → σ<VAR>h : α → ℕ →. σ<VAR>hf : Computable f<VAR>hg : Computable g<VAR>hh : Partrec₂ h<GOAL>Partrec fun a => Nat.casesOn (f a) (Part.some (g a)) (h a)
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<VAR>f : α →. σ<GOAL>Partrec f ↔ Nat.Partrec fun n => (↑(Encodable.decode₂ α n)).bind fun a => Part.map Encodable.encode (f a)
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<VAR>n : ℕ<VAR>f : Fin n → α →. σ<GOAL>(∀ (i : Fin n), Partrec (f i)) → Partrec fun a => Mathlib.Vector.mOfFn fun i => f i a
<VAR>α : Type u_1<VAR>n : ℕ<VAR>f : Fin n → α<GOAL>(Mathlib.Vector.mOfFn fun i => Part.some (f i)) = Part.some (Mathlib.Vector.ofFn f)
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<VAR>f : α → σ<GOAL>(Computable fun a => some (f a)) ↔ Computable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α → β → Option σ<GOAL>(Computable₂ fun a n => (Encodable.decode n).bind (f a)) ↔ Computable₂ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α → β → σ<GOAL>(Computable₂ fun a n => Option.map (f a) (Encodable.decode n)) ↔ Computable₂ f
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<VAR>f : α → ℕ<VAR>g : α → σ<VAR>h : α → ℕ × σ → σ<VAR>hf : Computable f<VAR>hg : Computable g<VAR>hh : Computable₂ h<GOAL>Computable fun a => Nat.rec (g a) (fun y IH => h a (y, IH)) (f a)
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<VAR>f : α → ℕ<VAR>g : α → σ<VAR>h : α → ℕ → σ<VAR>hf : Computable f<VAR>hg : Computable g<VAR>hh : Computable₂ h<GOAL>Computable fun a => Nat.casesOn (f a) (g a) (h a)
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<VAR>c : α → Bool<VAR>f g : α → σ<VAR>hc : Computable c<VAR>hf : Computable f<VAR>hg : Computable g<GOAL>Computable fun a => bif c a then f a else g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>o : α → Option β<VAR>f : α → σ<VAR>g : α → β → σ<VAR>ho : Computable o<VAR>hf : Computable f<VAR>hg : Computable₂ g<GOAL>Computable fun a => Option.casesOn (o a) (f a) (g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α → Option β<VAR>g : α → β → Option σ<VAR>hf : Computable f<VAR>hg : Computable₂ g<GOAL>Computable fun a => (f a).bind (g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α → Option β<VAR>g : α → β → σ<VAR>hf : Computable f<VAR>hg : Computable₂ g<GOAL>Computable fun a => Option.map (g a) (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>f : α → Option β<VAR>g : α → β<VAR>hf : Computable f<VAR>hg : Computable g<GOAL>Computable fun a => (f a).getD (g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>f : α → β<VAR>p : β → Prop<VAR>DecidablePred p<VAR>h : ∀ (a : α), p (f a)<VAR>hp : PrimrecPred p<VAR>hf : Computable f<GOAL>Computable fun a => ⟨f a, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>Primcodable σ<VAR>f : α → β ⊕ γ<VAR>g : α → β → σ<VAR>h : α → γ → σ<VAR>hf : Computable f<VAR>hg : Computable₂ g<VAR>hh : Computable₂ h<GOAL>Computable fun a => Sum.casesOn (f a) (g a) (h a)
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<VAR>f : α → ℕ → σ<VAR>g : α → List σ → Option σ<VAR>hg : Computable₂ g<VAR>H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)<GOAL>Computable₂ f
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<VAR>n : ℕ<VAR>f : Fin n → α → σ<GOAL>(∀ (i : Fin n), Computable (f i)) → Computable fun a => List.ofFn fun i => f i a
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<VAR>n : ℕ<VAR>f : Fin n → α → σ<VAR>hf : ∀ (i : Fin n), Computable (f i)<GOAL>Computable fun a => Mathlib.Vector.ofFn fun i => f i a
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<VAR>f : α →. σ<GOAL>(Partrec fun a => Part.map some (f a)) ↔ Partrec f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>o : α → Option β<VAR>f : α → σ<VAR>g : α → β →. σ<VAR>ho : Computable o<VAR>hf : Computable f<VAR>hg : Partrec₂ g<GOAL>Partrec fun a => Option.casesOn (o a) (Part.some (f a)) (g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>Primcodable σ<VAR>f : α → β ⊕ γ<VAR>g : α → β → σ<VAR>h : α → γ →. σ<VAR>hf : Computable f<VAR>hg : Computable₂ g<VAR>hh : Partrec₂ h<GOAL>Partrec fun a => Sum.casesOn (f a) (fun b => Part.some (g a b)) (h a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>Primcodable σ<VAR>f : α → β ⊕ γ<VAR>g : α → β →. σ<VAR>h : α → γ → σ<VAR>hf : Computable f<VAR>hg : Partrec₂ g<VAR>hh : Computable₂ h<GOAL>Partrec fun a => Sum.casesOn (f a) (g a) fun c => Part.some (h a c)
<VAR>α : Type u_5<VAR>σ : Type u_6<VAR>f : α →. σ ⊕ α<VAR>a : α<VAR>b : σ<GOAL>let 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, ((∃ b', Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m) ∧ Sum.inl b ∈ F a n) ↔ b ∈ f.fix a
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<VAR>f : α →. σ ⊕ α<VAR>hf : Partrec f<GOAL>Partrec f.fix
<VAR>n : ℕ<GOAL>ack 0 n = n + 1
<VAR>m : ℕ<GOAL>ack (m + 1) 0 = ack m 1
<VAR>m n : ℕ<GOAL>ack (m + 1) (n + 1) = ack m (ack (m + 1) n)
<VAR>n : ℕ<GOAL>ack 1 n = n + 2
<VAR>n : ℕ<GOAL>ack 2 n = 2 * n + 3
<VAR>n : ℕ<GOAL>ack 3 n = 2 ^ (n + 3) - 3
<VAR>m n : ℕ<GOAL>0 < ack m n
<VAR>m n : ℕ<GOAL>1 < ack (m + 1) n
<VAR>m n : ℕ<GOAL>1 < ack m (n + 1)
<VAR>m : ℕ<GOAL>StrictMono (ack m)
<VAR>m : ℕ<GOAL>Monotone (ack m)
<VAR>m : ℕ<GOAL>Function.Injective (ack m)
<VAR>m n₁ n₂ : ℕ<GOAL>ack m n₁ < ack m n₂ ↔ n₁ < n₂
<VAR>m n₁ n₂ : ℕ<GOAL>ack m n₁ ≤ ack m n₂ ↔ n₁ ≤ n₂
<VAR>m n₁ n₂ : ℕ<GOAL>ack m n₁ = ack m n₂ ↔ n₁ = n₂
<VAR>m n₁ n₂ : ℕ<GOAL>ack m (max n₁ n₂) = max (ack m n₁) (ack m n₂)
<VAR>m n : ℕ<GOAL>m + n < ack m n
<VAR>m n : ℕ<GOAL>m + n + 1 ≤ ack m n
<VAR>m n : ℕ<GOAL>m < ack m n
<VAR>m n : ℕ<GOAL>n < ack m n
<VAR>m₁ m₂ : ℕ<VAR>n : ℕ<GOAL>m₁ < m₂ → ack m₁ n < ack m₂ n
<VAR>n : ℕ<GOAL>StrictMono fun m => ack m n
<VAR>n : ℕ<GOAL>Monotone fun m => ack m n
<VAR>n : ℕ<GOAL>Function.Injective fun m => ack m n
<VAR>m₁ m₂ n : ℕ<GOAL>ack m₁ n < ack m₂ n ↔ m₁ < m₂
<VAR>m₁ m₂ n : ℕ<GOAL>ack m₁ n ≤ ack m₂ n ↔ m₁ ≤ m₂
<VAR>m₁ m₂ n : ℕ<GOAL>ack m₁ n = ack m₂ n ↔ m₁ = m₂
<VAR>m₁ m₂ n : ℕ<GOAL>ack (max m₁ m₂) n = max (ack m₁ n) (ack m₂ n)
<VAR>m₁ m₂ n₁ n₂ : ℕ<VAR>hm : m₁ ≤ m₂<VAR>hn : n₁ ≤ n₂<GOAL>ack m₁ n₁ ≤ ack m₂ n₂
<VAR>m n : ℕ<GOAL>ack m (n + 1) ≤ ack (m + 1) n
<VAR>n : ℕ<GOAL>n ^ 2 ≤ 2 ^ (n + 1) - 3
<VAR>m n : ℕ<GOAL>(ack m n + 1) ^ 2 ≤ ack (m + 3) n
<VAR>m n k : ℕ<GOAL>ack m (ack n k) < ack (max m n + 2) k
<VAR>m n : ℕ<GOAL>ack m ((n + 1) ^ 2) < ack (m + 4) n
<VAR>m n k : ℕ<GOAL>ack m (Nat.pair n k) < ack (m + 4) (max n k)
<VAR>f : ℕ → ℕ<VAR>hf : Nat.Primrec f<GOAL>∃ m, ∀ (n : ℕ), f n < ack m n
<VAR>f g : ℕ →. ℕ<VAR>hf : Nat.Partrec f<VAR>hg : Nat.Partrec g<GOAL>∃ h, Nat.Partrec h ∧ ∀ (a : ℕ), (∀ x ∈ h a, x ∈ f a ∨ x ∈ g a) ∧ ((h a).Dom ↔ (f a).Dom ∨ (g a).Dom)
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<VAR>f g : α →. σ<VAR>hf : Partrec f<VAR>hg : Partrec g<GOAL>∃ k, Partrec k ∧ ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<VAR>f g : α →. σ<VAR>hf : Partrec f<VAR>hg : Partrec g<VAR>H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y<GOAL>∃ k, Partrec k ∧ ∀ (a : α) (x : σ), x ∈ k a ↔ x ∈ f a ∨ x ∈ g a
<VAR>α : Type u_1<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable σ<VAR>c : α → Bool<VAR>f g : α →. σ<VAR>hc : Computable c<VAR>hf : Partrec f<VAR>hg : Partrec g<GOAL>Partrec fun a => bif c a then f a else g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>Primcodable σ<VAR>f : α → β ⊕ γ<VAR>g : α → β →. σ<VAR>h : α → γ →. σ<VAR>hf : Computable f<VAR>hg : Partrec₂ g<VAR>hh : Partrec₂ h<GOAL>Partrec fun a => Sum.casesOn (f a) (g a) (h a)
<VAR>α : Type u_1<VAR>Primcodable α<VAR>p q : α → Prop<VAR>hp : RePred p<VAR>H : ∀ (a : α), p a ↔ q a<GOAL>RePred q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>f : α →. β<VAR>h : Partrec f<GOAL>RePred fun a => (f a).Dom
<VAR>α : Type u_1<VAR>Primcodable α<VAR>p q : α → Prop<VAR>hp : ComputablePred p<VAR>H : ∀ (a : α), p a ↔ q a<GOAL>ComputablePred q
<VAR>α : Type u_1<VAR>Primcodable α<VAR>p : α → Prop<GOAL>ComputablePred p ↔ ∃ f, Computable f ∧ p = fun a => f a = true
<VAR>α : Type u_1<VAR>Primcodable α<VAR>p : α → Prop<VAR>hp : ComputablePred p<GOAL>ComputablePred fun a => ¬p a
<VAR>α : Type u_1<VAR>Primcodable α<VAR>p : α → Prop<VAR>hp : ComputablePred p<GOAL>RePred p
<VAR>C : Set (ℕ →. ℕ)<VAR>h : ComputablePred fun c => c.eval ∈ C<VAR>f g : ℕ →. ℕ<VAR>hf : Nat.Partrec f<VAR>hg : Nat.Partrec g<VAR>fC : f ∈ C<GOAL>g ∈ C
<VAR>C : Set Nat.Partrec.Code<VAR>H : ∀ (cf cg : Nat.Partrec.Code), cf.eval = cg.eval → (cf ∈ C ↔ cg ∈ C)<GOAL>(ComputablePred fun c => c ∈ C) ↔ C = ∅ ∨ C = Set.univ
<VAR>n : ℕ<GOAL>RePred fun c => (c.eval n).Dom
<VAR>n : ℕ<GOAL>¬ComputablePred fun c => (c.eval n).Dom
<VAR>α : Type u_1<VAR>Primcodable α<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>ComputablePred p ↔ RePred p ∧ RePred fun a => ¬p a
<VAR>α : Type u_1<VAR>Primcodable α<VAR>p : α → Prop<GOAL>ComputablePred p ↔ RePred p ∧ RePred fun a => ¬p a
<VAR>n : ℕ<GOAL>¬RePred fun c => ¬(c.eval n).Dom
<VAR>n : ℕ<VAR>f : Mathlib.Vector ℕ n →. ℕ<VAR>pf : Nat.Partrec' f<GOAL>Partrec f
<VAR>n : ℕ<VAR>f g : Mathlib.Vector ℕ n →. ℕ<VAR>hf : Nat.Partrec' f<VAR>H : ∀ (i : Mathlib.Vector ℕ n), f i = g i<GOAL>Nat.Partrec' g
<VAR>n : ℕ<VAR>f : Mathlib.Vector ℕ n → ℕ<VAR>hf : Primrec f<GOAL>Nat.Partrec' ↑f
<VAR>n : ℕ<GOAL>Nat.Partrec' ↑Mathlib.Vector.head
<VAR>n : ℕ<VAR>f : Mathlib.Vector ℕ n →. ℕ<VAR>hf : Nat.Partrec' f<GOAL>Nat.Partrec' fun v => f v.tail
<VAR>n : ℕ<VAR>f : Mathlib.Vector ℕ n →. ℕ<VAR>g : Mathlib.Vector ℕ (n + 1) →. ℕ<VAR>hf : Nat.Partrec' f<VAR>hg : Nat.Partrec' g<GOAL>Nat.Partrec' fun v => (f v).bind fun a => g (a ::ᵥ v)
<VAR>n : ℕ<VAR>f : Mathlib.Vector ℕ n →. ℕ<VAR>g : Mathlib.Vector ℕ (n + 1) → ℕ<VAR>hf : Nat.Partrec' f<VAR>hg : Nat.Partrec' ↑g<GOAL>Nat.Partrec' fun v => Part.map (fun a => g (a ::ᵥ v)) (f v)
<VAR>n m : ℕ<VAR>f : Mathlib.Vector ℕ n → Mathlib.Vector ℕ m<VAR>hf : Nat.Primrec'.Vec f<GOAL>Nat.Partrec'.Vec f
<VAR>n : ℕ<GOAL>Nat.Partrec'.Vec fun x => Mathlib.Vector.nil
<VAR>n m : ℕ<VAR>f : Mathlib.Vector ℕ n → ℕ<VAR>g : Mathlib.Vector ℕ n → Mathlib.Vector ℕ m<VAR>hf : Nat.Partrec' ↑f<VAR>hg : Nat.Partrec'.Vec g<GOAL>Nat.Partrec'.Vec fun v => f v ::ᵥ g v
<VAR>n : ℕ<GOAL>Nat.Partrec'.Vec id
<VAR>n m : ℕ<VAR>f : Mathlib.Vector ℕ m →. ℕ<VAR>g : Mathlib.Vector ℕ n → Mathlib.Vector ℕ m<VAR>hf : Nat.Partrec' f<VAR>hg : Nat.Partrec'.Vec g<GOAL>Nat.Partrec' fun v => f (g v)
<VAR>n : ℕ<VAR>f : ℕ →. ℕ<VAR>g : Mathlib.Vector ℕ n → ℕ<VAR>hf : Nat.Partrec' fun v => f v.head<VAR>hg : Nat.Partrec' ↑g<GOAL>Nat.Partrec' fun v => f (g v)
<VAR>n : ℕ<VAR>f : Mathlib.Vector ℕ (n + 1) → ℕ<VAR>hf : Nat.Partrec' ↑f<GOAL>Nat.Partrec' fun v => Nat.rfindOpt fun a => Denumerable.ofNat (Option ℕ) (f (a ::ᵥ v))
<VAR>n : ℕ<VAR>f : Mathlib.Vector ℕ n →. ℕ<GOAL>Partrec f → Nat.Partrec' f
<VAR>n : ℕ<VAR>f : Mathlib.Vector ℕ n →. ℕ<GOAL>Nat.Partrec' f ↔ Partrec f
<VAR>f : ℕ →. ℕ<GOAL>(Nat.Partrec' fun v => f v.head) ↔ Partrec f