ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>n : Type w<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>J A B : Matrix n n R<VAR>hA : Aᵀ * J = J * -A<VAR>hB : Bᵀ * J = J * -B<GOAL>⁅A, B⁆ᵀ * J = J * -⁅A, B⁆
<VAR>R : Type u<VAR>n : Type w<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>J A B : Matrix n n R<VAR>hA : Aᵀ * J = J * -A<VAR>hB : Bᵀ * J = J * -B<GOAL>J * -B * -A - J * -A * -B = J * -(A * B - B * A)
<VAR>a✝ b✝ c✝ d m n a b c : ℤ<GOAL>a < b → ¬b < a
<VAR>a✝ b✝ c✝ d m n a b c : ℤ<GOAL>a < b → a ≤ b
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R : ℝ<VAR>z w : ℂ<VAR>f : ℂ → E<VAR>x✝ : ℝ<GOAL>circleTransformDeriv R z w f x✝ = (circleMap z R x✝ - w)⁻¹ • circleTransform R z w f x✝
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R : ℝ<VAR>z w : ℂ<VAR>f : ℂ → E<VAR>x✝ : ℝ<GOAL>((2 * ↑π * I)⁻¹ * deriv (circleMap z R) x✝ * ((circleMap z R x✝ - w) ^ 2)⁻¹) • f (circleMap z R x✝) = ((circleMap z R x✝ - w)⁻¹ * (2 * ↑π * I)⁻¹ * deriv (circleMap z R) x✝ * (circleMap z R x✝ - w)⁻¹) • f (circleMap z R x✝)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R : ℝ<VAR>z w : ℂ<VAR>f : ℂ → E<VAR>x✝ : ℝ<GOAL>((↑π)⁻¹ * I⁻¹ * deriv (circleMap z R) x✝ * (-(circleMap z R x✝ * w * 2) + circleMap z R x✝ ^ 2 + w ^ 2)⁻¹ * (1 / 2)) • f (circleMap z R x✝) = ((↑π)⁻¹ * I⁻¹ * deriv (circleMap z R) x✝ * (circleMap z R x✝ - w)⁻¹ ^ 2 * (1 / 2)) • f (circleMap z R x✝)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R : ℝ<VAR>z w : ℂ<VAR>f : ℂ → E<VAR>x✝ : ℝ<GOAL>((↑π)⁻¹ * I⁻¹ * deriv (circleMap z R) x✝ * (-(circleMap z R x✝ * w * 2) + circleMap z R x✝ ^ 2 + w ^ 2)⁻¹ * (1 / 2)) • f (circleMap z R x✝) = ((↑π)⁻¹ * I⁻¹ * deriv (circleMap z R) x✝ * ((circleMap z R x✝ - w) ^ 2)⁻¹ * (1 / 2)) • f (circleMap z R x✝)
<VAR>n : ℕ<GOAL>cos (↑n * (2 * π) - π) = -1
<VAR>x : ℝ*<VAR>r : ℝ<GOAL>x.IsSt r ↔ Germ.Tendsto x (𝓝 r)
<VAR>r : ℝ<VAR>f : ℕ → ℝ<GOAL>(ofSeq f).IsSt r ↔ Germ.Tendsto (ofSeq f) (𝓝 r)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasBinaryBiproducts C<VAR>X Y : C<GOAL>IsIso biprod.inl ↔ IsZero Y
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasBinaryBiproducts C<VAR>X Y : C<GOAL>biprod.snd ≫ biprod.inr = 0 ↔ IsZero Y
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : range f' = ⊤<VAR>hker : (LinearMap.ker f').ClosedComplemented<GOAL>implicitFunctionOfComplemented f f' hf hf' hker (f a) 0 = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>j : JordanDecomposition α<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>↑(toSignedMeasure 0) i = ↑0 i
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>inst✝³ : CommSemiring k<VAR>inst✝² : Group G<VAR>inst✝¹ : AddCommMonoid V<VAR>inst✝ : Module k V<VAR>ρ : Representation k G V<VAR>g : G<GOAL>↑(ρ.asGroupHom g) = ρ g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁴ : CommSemiring R<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹¹ : CommRing R₁<VAR>inst✝¹⁰ : AddCommGroup M₁<VAR>inst✝⁹ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module K V<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>inst✝⁵ : AddCommMonoid M'✝<VAR>inst✝⁴ : AddCommMonoid M''<VAR>inst✝³ : Module R M'✝<VAR>inst✝² : Module R M''<VAR>B : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>F : BilinForm R M<VAR>M' : Type u_9<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>B' : BilinForm R M'<VAR>f f' : M →ₗ[R] M'<VAR>g g' : M' →ₗ[R] M<VAR>x : M<VAR>y : M'<GOAL>(B' (0 x)) y = (B x) (0 y)
<VAR>n : ℕ<GOAL>antidiagonal (n + 1) = map (Prod.map id succ) (antidiagonal n) ++ [(n + 1, 0)]
<VAR>n : ℕ<GOAL>map (fun i => (i, n + 1 - i)) (range n) ++ [(n, 1), (n + 1, 0)] = map (Prod.map id succ ∘ fun i => (i, n - i)) (range n) ++ [Prod.map id succ (n, 0), (n + 1, 0)]
<VAR>n : ℕ<GOAL>map (fun i => (i, n + 1 - i)) (range n) = map (Prod.map id succ ∘ fun i => (i, n - i)) (range n)
<VAR>n : ℕ<GOAL>∀ a ∈ range n, (a, n + 1 - a) = (Prod.map id succ ∘ fun i => (i, n - i)) a
<VAR>R : Type u_1<VAR>inst✝ : CommGroupWithZero R<VAR>s : Set ℕ<VAR>hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s<VAR>f g : ℕ → R<VAR>hf : ∀ n > 0, f n ≠ 0<VAR>hg : ∀ n > 0, g n ≠ 0<GOAL>(∀ n > 0, n ∈ s → ∏ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, n ∈ s → ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ μ x.1 = f n
<VAR>R : Type u_1<VAR>inst✝ : CommGroupWithZero R<VAR>s : Set ℕ<VAR>hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s<VAR>f g : ℕ → R<VAR>hf : ∀ n > 0, f n ≠ 0<VAR>hg : ∀ n > 0, g n ≠ 0<VAR>n : ℕ<VAR>hn : n > 0<GOAL>n ∈ s → ∏ i ∈ n.divisors, f i = g n ↔ n ∈ s → ∏ i ∈ n.divisors, (fun n => if h : 0 < n then Units.mk0 (f n) ⋯ else 1) i = (fun n => if h : 0 < n then Units.mk0 (g n) ⋯ else 1) n
<VAR>R : Type u_1<VAR>inst✝ : CommGroupWithZero R<VAR>s : Set ℕ<VAR>hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s<VAR>f g : ℕ → R<VAR>hf : ∀ n > 0, f n ≠ 0<VAR>hg : ∀ n > 0, g n ≠ 0<VAR>n : ℕ<VAR>hn : n > 0<GOAL>n ∈ s → ∏ x ∈ n.divisorsAntidiagonal, (fun n => if h : 0 < n then Units.mk0 (g n) ⋯ else 1) x.2 ^ μ x.1 = (fun n => if h : 0 < n then Units.mk0 (f n) ⋯ else 1) n ↔ n ∈ s → ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ μ x.1 = f n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : DivisionMonoid α<VAR>s t : Set α<GOAL>univ / univ = univ
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>β✝² : ι → Type u_4<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>u : Set ((i : ι) × α i)<VAR>x✝ : (i : ι) × α i<VAR>i j : ι<VAR>a : α i<VAR>β✝¹ : Type u_5<VAR>inst✝ : CompleteLattice β✝¹<VAR>β✝ : Type u_6<VAR>β : ι → Type u_7<VAR>x : (i : ι) × α i<GOAL>x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁
<VAR>n : ℕ<VAR>c : Composition n<GOAL>∑ i : Fin c.length, c.blocksFun i = n
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>c : α → Code<VAR>hc : Computable c<VAR>z : α → σ<VAR>hz : Computable z<VAR>s : α → σ<VAR>hs : Computable s<VAR>l : α → σ<VAR>hl : Computable l<VAR>r : α → σ<VAR>hr : Computable r<VAR>pr : α → Code × Code × σ × σ → σ<VAR>hpr : Computable₂ pr<VAR>co : α → Code × Code × σ × σ → σ<VAR>hco : Computable₂ co<VAR>pc : α → Code × Code × σ × σ → σ<VAR>hpc : Computable₂ pc<VAR>rf : α → Code × σ → σ<VAR>hrf : Computable₂ rf<VAR>PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pr a (cf, cg, hf, hg)<VAR>CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => co a (cf, cg, hf, hg)<VAR>PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pc a (cf, cg, hf, hg)<VAR>RF✝ : α → Code → σ → σ := fun a cf hf => rf a (cf, hf)<VAR>F : α → Code → σ := fun a c => Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)<VAR>G₁ : (α × List σ) × ℕ × ℕ → Option σ := fun p => (p.1.2.get? p.2.2).bind fun s => (p.1.2.get? (unpair p.2.2).1).bind fun s₁ => Option.map (fun s₂ => bif p.2.1.bodd then bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s) else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)) (p.1.2.get? (unpair p.2.2).2)<GOAL>Computable fun a => F a (c a)
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>c : α → Code<VAR>hc : Computable c<VAR>z : α → σ<VAR>hz : Computable z<VAR>s : α → σ<VAR>hs : Computable s<VAR>l : α → σ<VAR>hl : Computable l<VAR>r : α → σ<VAR>hr : Computable r<VAR>pr : α → Code × Code × σ × σ → σ<VAR>hpr : Computable₂ pr<VAR>co : α → Code × Code × σ × σ → σ<VAR>hco : Computable₂ co<VAR>pc : α → Code × Code × σ × σ → σ<VAR>hpc : Computable₂ pc<VAR>rf : α → Code × σ → σ<VAR>hrf : Computable₂ rf<VAR>PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pr a (cf, cg, hf, hg)<VAR>CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => co a (cf, cg, hf, hg)<VAR>PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pc a (cf, cg, hf, hg)<VAR>RF✝ : α → Code → σ → σ := fun a cf hf => rf a (cf, hf)<VAR>F : α → Code → σ := fun a c => Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)<VAR>G₁ : (α × List σ) × ℕ × ℕ → Option σ := fun p => (p.1.2.get? p.2.2).bind fun s => (p.1.2.get? (unpair p.2.2).1).bind fun s₁ => Option.map (fun s₂ => bif p.2.1.bodd then bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s) else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)) (p.1.2.get? (unpair p.2.2).2)<VAR>this : Computable G₁<GOAL>Computable fun a => F a (c a)
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>c : α → Code<VAR>hc : Computable c<VAR>z : α → σ<VAR>hz : Computable z<VAR>s : α → σ<VAR>hs : Computable s<VAR>l : α → σ<VAR>hl : Computable l<VAR>r : α → σ<VAR>hr : Computable r<VAR>pr : α → Code × Code × σ × σ → σ<VAR>hpr : Computable₂ pr<VAR>co : α → Code × Code × σ × σ → σ<VAR>hco : Computable₂ co<VAR>pc : α → Code × Code × σ × σ → σ<VAR>hpc : Computable₂ pc<VAR>rf : α → Code × σ → σ<VAR>hrf : Computable₂ rf<VAR>PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pr a (cf, cg, hf, hg)<VAR>CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => co a (cf, cg, hf, hg)<VAR>PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pc a (cf, cg, hf, hg)<VAR>RF✝ : α → Code → σ → σ := fun a cf hf => rf a (cf, hf)<VAR>F : α → Code → σ := fun a c => Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)<VAR>G₁ : (α × List σ) × ℕ × ℕ → Option σ := fun p => (p.1.2.get? p.2.2).bind fun s => (p.1.2.get? (unpair p.2.2).1).bind fun s₁ => Option.map (fun s₂ => bif p.2.1.bodd then bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s) else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)) (p.1.2.get? (unpair p.2.2).2)<VAR>this : Computable G₁<VAR>G : α → List σ → Option σ := fun a IH => Nat.casesOn IH.length (some (z a)) fun n => Nat.casesOn n (some (s a)) fun n => Nat.casesOn n (some (l a)) fun n => Nat.casesOn n (some (r a)) fun n => G₁ ((a, IH), n, n.div2.div2)<GOAL>Computable fun a => F a (c a)
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>c : α → Code<VAR>hc : Computable c<VAR>z : α → σ<VAR>hz : Computable z<VAR>s : α → σ<VAR>hs : Computable s<VAR>l : α → σ<VAR>hl : Computable l<VAR>r : α → σ<VAR>hr : Computable r<VAR>pr : α → Code × Code × σ × σ → σ<VAR>hpr : Computable₂ pr<VAR>co : α → Code × Code × σ × σ → σ<VAR>hco : Computable₂ co<VAR>pc : α → Code × Code × σ × σ → σ<VAR>hpc : Computable₂ pc<VAR>rf : α → Code × σ → σ<VAR>hrf : Computable₂ rf<VAR>PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pr a (cf, cg, hf, hg)<VAR>CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => co a (cf, cg, hf, hg)<VAR>PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pc a (cf, cg, hf, hg)<VAR>RF✝ : α → Code → σ → σ := fun a cf hf => rf a (cf, hf)<VAR>F : α → Code → σ := fun a c => Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)<VAR>G₁ : (α × List σ) × ℕ × ℕ → Option σ := fun p => (p.1.2.get? p.2.2).bind fun s => (p.1.2.get? (unpair p.2.2).1).bind fun s₁ => Option.map (fun s₂ => bif p.2.1.bodd then bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s) else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)) (p.1.2.get? (unpair p.2.2).2)<VAR>this✝ : Computable G₁<VAR>G : α → List σ → Option σ := fun a IH => Nat.casesOn IH.length (some (z a)) fun n => Nat.casesOn n (some (s a)) fun n => Nat.casesOn n (some (l a)) fun n => Nat.casesOn n (some (r a)) fun n => G₁ ((a, IH), n, n.div2.div2)<VAR>this : Computable₂ G<GOAL>Computable fun a => F a (c a)
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>c : α → Code<VAR>hc : Computable c<VAR>z : α → σ<VAR>hz : Computable z<VAR>s : α → σ<VAR>hs : Computable s<VAR>l : α → σ<VAR>hl : Computable l<VAR>r : α → σ<VAR>hr : Computable r<VAR>pr : α → Code × Code × σ × σ → σ<VAR>hpr : Computable₂ pr<VAR>co : α → Code × Code × σ × σ → σ<VAR>hco : Computable₂ co<VAR>pc : α → Code × Code × σ × σ → σ<VAR>hpc : Computable₂ pc<VAR>rf : α → Code × σ → σ<VAR>hrf : Computable₂ rf<VAR>PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pr a (cf, cg, hf, hg)<VAR>CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => co a (cf, cg, hf, hg)<VAR>PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pc a (cf, cg, hf, hg)<VAR>RF✝ : α → Code → σ → σ := fun a cf hf => rf a (cf, hf)<VAR>F : α → Code → σ := fun a c => Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)<VAR>G₁ : (α × List σ) × ℕ × ℕ → Option σ := fun p => (p.1.2.get? p.2.2).bind fun s => (p.1.2.get? (unpair p.2.2).1).bind fun s₁ => Option.map (fun s₂ => bif p.2.1.bodd then bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s) else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)) (p.1.2.get? (unpair p.2.2).2)<VAR>this✝ : Computable G₁<VAR>G : α → List σ → Option σ := fun a IH => Nat.casesOn IH.length (some (z a)) fun n => Nat.casesOn n (some (s a)) fun n => Nat.casesOn n (some (l a)) fun n => Nat.casesOn n (some (r a)) fun n => G₁ ((a, IH), n, n.div2.div2)<VAR>this : Computable₂ G<VAR>a : α<VAR>n : ℕ<GOAL>G (a, List.map ((fun a n => F a (ofNat Code n)) a) (List.range n)).1 (a, List.map ((fun a n => F a (ofNat Code n)) a) (List.range n)).2 = some ((fun a n => F a (ofNat Code n)) a n)
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>c : α → Code<VAR>hc : Computable c<VAR>z : α → σ<VAR>hz : Computable z<VAR>s : α → σ<VAR>hs : Computable s<VAR>l : α → σ<VAR>hl : Computable l<VAR>r : α → σ<VAR>hr : Computable r<VAR>pr : α → Code × Code × σ × σ → σ<VAR>hpr : Computable₂ pr<VAR>co : α → Code × Code × σ × σ → σ<VAR>hco : Computable₂ co<VAR>pc : α → Code × Code × σ × σ → σ<VAR>hpc : Computable₂ pc<VAR>rf : α → Code × σ → σ<VAR>hrf : Computable₂ rf<VAR>PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pr a (cf, cg, hf, hg)<VAR>CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => co a (cf, cg, hf, hg)<VAR>PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pc a (cf, cg, hf, hg)<VAR>RF✝ : α → Code → σ → σ := fun a cf hf => rf a (cf, hf)<VAR>F : α → Code → σ := fun a c => Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)<VAR>G₁ : (α × List σ) × ℕ × ℕ → Option σ := fun p => (p.1.2.get? p.2.2).bind fun s => (p.1.2.get? (unpair p.2.2).1).bind fun s₁ => Option.map (fun s₂ => bif p.2.1.bodd then bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s) else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)) (p.1.2.get? (unpair p.2.2).2)<VAR>this✝ : Computable G₁<VAR>G : α → List σ → Option σ := fun a IH => Nat.casesOn IH.length (some (z a)) fun n => Nat.casesOn n (some (s a)) fun n => Nat.casesOn n (some (l a)) fun n => Nat.casesOn n (some (r a)) fun n => G₁ ((a, IH), n, n.div2.div2)<VAR>this : Computable₂ G<VAR>a : α<VAR>n : ℕ<GOAL>Nat.rec (some (z a)) (fun n_1 n_ih => Nat.rec (some (s a)) (fun n_2 n_ih => Nat.rec (some (l a)) (fun n_3 n_ih => Nat.rec (some (r a)) (fun n_4 n_ih => G₁ ((a, List.map (fun n => F a (ofNat Code n)) (List.range (n + 1 + 1 + 1 + 1))), n_4, n_4.div2.div2)) n_3) n_2) n_1) (List.map (fun n => F a (ofNat Code n)) (List.range (n + 1 + 1 + 1 + 1))).length = some (F a (ofNat Code (n + 1 + 1 + 1 + 1)))
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>c : α → Code<VAR>hc : Computable c<VAR>z : α → σ<VAR>hz : Computable z<VAR>s : α → σ<VAR>hs : Computable s<VAR>l : α → σ<VAR>hl : Computable l<VAR>r : α → σ<VAR>hr : Computable r<VAR>pr : α → Code × Code × σ × σ → σ<VAR>hpr : Computable₂ pr<VAR>co : α → Code × Code × σ × σ → σ<VAR>hco : Computable₂ co<VAR>pc : α → Code × Code × σ × σ → σ<VAR>hpc : Computable₂ pc<VAR>rf : α → Code × σ → σ<VAR>hrf : Computable₂ rf<VAR>PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pr a (cf, cg, hf, hg)<VAR>CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => co a (cf, cg, hf, hg)<VAR>PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pc a (cf, cg, hf, hg)<VAR>RF✝ : α → Code → σ → σ := fun a cf hf => rf a (cf, hf)<VAR>F : α → Code → σ := fun a c => Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)<VAR>G₁ : (α × List σ) × ℕ × ℕ → Option σ := fun p => (p.1.2.get? p.2.2).bind fun s => (p.1.2.get? (unpair p.2.2).1).bind fun s₁ => Option.map (fun s₂ => bif p.2.1.bodd then bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s) else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)) (p.1.2.get? (unpair p.2.2).2)<VAR>this✝ : Computable G₁<VAR>G : α → List σ → Option σ := fun a IH => Nat.casesOn IH.length (some (z a)) fun n => Nat.casesOn n (some (s a)) fun n => Nat.casesOn n (some (l a)) fun n => Nat.casesOn n (some (r a)) fun n => G₁ ((a, IH), n, n.div2.div2)<VAR>this : Computable₂ G<VAR>a : α<VAR>n : ℕ<GOAL>Nat.rec (some (z a)) (fun n_1 n_ih => Nat.rec (some (s a)) (fun n_2 n_ih => Nat.rec (some (l a)) (fun n_3 n_ih => Nat.rec (some (r a)) (fun n_4 n_ih => G₁ ((a, List.map (fun n => F a (ofNat Code n)) (List.range (n + 1 + 1 + 1 + 1))), n_4, n_4.div2.div2)) n_3) n_2) n_1) (n + 1 + 1 + 1 + 1) = some (F a (ofNat Code (n + 1 + 1 + 1 + 1)))
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>c : α → Code<VAR>hc : Computable c<VAR>z : α → σ<VAR>hz : Computable z<VAR>s : α → σ<VAR>hs : Computable s<VAR>l : α → σ<VAR>hl : Computable l<VAR>r : α → σ<VAR>hr : Computable r<VAR>pr : α → Code × Code × σ × σ → σ<VAR>hpr : Computable₂ pr<VAR>co : α → Code × Code × σ × σ → σ<VAR>hco : Computable₂ co<VAR>pc : α → Code × Code × σ × σ → σ<VAR>hpc : Computable₂ pc<VAR>rf : α → Code × σ → σ<VAR>hrf : Computable₂ rf<VAR>PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pr a (cf, cg, hf, hg)<VAR>CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => co a (cf, cg, hf, hg)<VAR>PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pc a (cf, cg, hf, hg)<VAR>RF✝ : α → Code → σ → σ := fun a cf hf => rf a (cf, hf)<VAR>F : α → Code → σ := fun a c => Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)<VAR>G₁ : (α × List σ) × ℕ × ℕ → Option σ := fun p => (p.1.2.get? p.2.2).bind fun s => (p.1.2.get? (unpair p.2.2).1).bind fun s₁ => Option.map (fun s₂ => bif p.2.1.bodd then bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s) else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)) (p.1.2.get? (unpair p.2.2).2)<VAR>this✝ : Computable G₁<VAR>G : α → List σ → Option σ := fun a IH => Nat.casesOn IH.length (some (z a)) fun n => Nat.casesOn n (some (s a)) fun n => Nat.casesOn n (some (l a)) fun n => Nat.casesOn n (some (r a)) fun n => G₁ ((a, IH), n, n.div2.div2)<VAR>this : Computable₂ G<VAR>a : α<VAR>n : ℕ<VAR>m : ℕ := n.div2.div2<GOAL>G₁ ((a, List.map (fun n => F a (ofNat Code n)) (List.range (n + 4))), n, m) = some (F a (ofNat Code (n + 4)))
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>c : α → Code<VAR>hc : Computable c<VAR>z : α → σ<VAR>hz : Computable z<VAR>s : α → σ<VAR>hs : Computable s<VAR>l : α → σ<VAR>hl : Computable l<VAR>r : α → σ<VAR>hr : Computable r<VAR>pr : α → Code × Code × σ × σ → σ<VAR>hpr : Computable₂ pr<VAR>co : α → Code × Code × σ × σ → σ<VAR>hco : Computable₂ co<VAR>pc : α → Code × Code × σ × σ → σ<VAR>hpc : Computable₂ pc<VAR>rf : α → Code × σ → σ<VAR>hrf : Computable₂ rf<VAR>PR✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pr a (cf, cg, hf, hg)<VAR>CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => co a (cf, cg, hf, hg)<VAR>PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pc a (cf, cg, hf, hg)<VAR>RF✝ : α → Code → σ → σ := fun a cf hf => rf a (cf, hf)<VAR>F : α → Code → σ := fun a c => Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)<VAR>G₁ : (α × List σ) × ℕ × ℕ → Option σ := fun p => (p.1.2.get? p.2.2).bind fun s => (p.1.2.get? (unpair p.2.2).1).bind fun s₁ => Option.map (fun s₂ => bif p.2.1.bodd then bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s) else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂) else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)) (p.1.2.get? (unpair p.2.2).2)<VAR>this✝ : Computable G₁<VAR>G : α → List σ → Option σ := fun a IH => Nat.casesOn IH.length (some (z a)) fun n => Nat.casesOn n (some (s a)) fun n => Nat.casesOn n (some (l a)) fun n => Nat.casesOn n (some (r a)) fun n => G₁ ((a, IH), n, n.div2.div2)<VAR>this : Computable₂ G<VAR>a : α<VAR>n : ℕ<VAR>m : ℕ := n.div2.div2<VAR>hm : m < n + 4<GOAL>G₁ ((a, List.map (fun n => F a (ofNat Code n)) (List.range (n + 4))), n, m) = some (F a (ofNat Code (n + 4)))