ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝³ : (i : ι) → MeasurableSpace (α i)<VAR>μ✝ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>β : Option ι → Type u_4<VAR>inst✝¹ : (i : Option ι) → MeasurableSpace (β i)<VAR>μ : (i : Option ι) → Measure (β i)<VAR>inst✝ : ∀ (i : Option ι), SigmaFinite (μ i)<VAR>s : (i : Option ι) → Set (β i)<VAR>x✝ : ∀ (i : Option ι), MeasurableSet (s i)<VAR>e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) := (MeasurableEquiv.piOptionEquivProd β).symm<VAR>me : MeasurableEmbedding ⇑e_meas<VAR>this : ⇑e_meas ⁻¹' univ.pi s = (univ.pi fun i => s (some i)) ×ˢ s none<GOAL>(map (⇑(MeasurableEquiv.piOptionEquivProd β).symm) ((Measure.pi fun i => μ (some i)).prod (μ none))) (univ.pi s) = ∏ i : Option ι, (μ i) (s i)
<VAR>S : Type u<VAR>inst✝ : State S<VAR>s t : S<VAR>m : t ∈ l s<VAR>h : turnBound s = 0<GOAL>False
<VAR>S : Type u<VAR>inst✝ : State S<VAR>s t✝ : S<VAR>m : t✝ ∈ l s<VAR>h : turnBound s = 0<VAR>t : turnBound t✝ < turnBound s<GOAL>False
<VAR>S : Type u<VAR>inst✝ : State S<VAR>s t✝ : S<VAR>m : t✝ ∈ l s<VAR>h : turnBound s = 0<VAR>t : turnBound t✝ < 0<GOAL>False
<VAR>n x y : ℤ<VAR>h : n = x ^ 2 + y ^ 2<VAR>hc : IsCoprime x y<GOAL>IsSquare (-1)
<VAR>n x y : ℤ<VAR>h : n = x ^ 2 + y ^ 2<VAR>hc : IsCoprime x y<VAR>u v : ℤ<VAR>huv : u * x + v * n = 1<GOAL>IsSquare (-1)
<VAR>n x y : ℤ<VAR>h : n = x ^ 2 + y ^ 2<VAR>hc : IsCoprime x y<VAR>u v : ℤ<VAR>huv : u * x + v * n = 1<VAR>H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)<GOAL>IsSquare (-1)
<VAR>n x y : ℤ<VAR>h : n = x ^ 2 + y ^ 2<VAR>hc : IsCoprime x y<VAR>u v : ℤ<VAR>huv : u * x + v * n = 1<VAR>H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)<GOAL>↑(-1) = ↑(u * y * (u * y))
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>P : Karoubi (Karoubi C)<GOAL>P.p.f ≫ P.p.f = P.p.f
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>J : Type w₁<VAR>f : J → C<VAR>inst✝¹ : HasBiproduct f<VAR>inst✝ : PreservesBiproduct f F<VAR>W : C<VAR>g : (j : J) → f j ⟶ W<GOAL>((F.mapBiproduct f).hom ≫ desc fun j => F.map (g j)) = F.map (desc g)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<VAR>Δ✝ Δ'✝ Δ'' : SimplexCategory<VAR>inst✝¹ : HasFiniteCoproducts C<VAR>Δ Δ' : SimplexCategory<VAR>e : Δ' ⟶ Δ<VAR>inst✝ : Epi e<GOAL>((splitting K).cofan (op Δ)).inj (Splitting.IndexSet.id (op Δ)) ≫ (obj K).map e.op = ((splitting K).cofan (op Δ')).inj (Splitting.IndexSet.mk e)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : LieAlgebra.IsNilpotent R L<VAR>inst✝² : NoZeroSMulDivisors ℤ R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : IsNoetherian R M<VAR>α : L → R<VAR>β : Weight R L M<VAR>hα : α ≠ 0<GOAL>weightSpace M ((chainTopCoeff α β + 1) • α + ⇑β) = ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a✝ b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q : R[X]<VAR>a : R<VAR>hq : q.natDegree ≠ 0<GOAL>(p.comp q).leadingCoeff = p.leadingCoeff * q.leadingCoeff ^ p.natDegree
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{?u.31876, u_1} C<VAR>inst✝⁴ : Category.{?u.31880, u_2} D<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.RightHomologyData<VAR>F : C ⥤ D<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : h.IsPreservedBy F<VAR>this✝ : PreservesColimit (parallelPair S.f 0) F<VAR>this : PreservesLimit (parallelPair h.g' 0) F<GOAL>(S.map F).RightHomologyData
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{?u.31876, u_1} C<VAR>inst✝⁴ : Category.{?u.31880, u_2} D<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.RightHomologyData<VAR>F : C ⥤ D<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : h.IsPreservedBy F<VAR>this✝ : PreservesColimit (parallelPair S.f 0) F<VAR>this : PreservesLimit (parallelPair h.g' 0) F<VAR>wp : F.map S.f ≫ F.map h.p = 0<GOAL>(S.map F).RightHomologyData
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{?u.31876, u_1} C<VAR>inst✝⁴ : Category.{?u.31880, u_2} D<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.RightHomologyData<VAR>F : C ⥤ D<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : h.IsPreservedBy F<VAR>this✝ : PreservesColimit (parallelPair S.f 0) F<VAR>this : PreservesLimit (parallelPair h.g' 0) F<VAR>wp : F.map S.f ≫ F.map h.p = 0<VAR>hp : IsColimit ((CokernelCofork.ofπ h.p ⋯).map F)<GOAL>(S.map F).RightHomologyData
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{?u.31876, u_1} C<VAR>inst✝⁴ : Category.{?u.31880, u_2} D<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.RightHomologyData<VAR>F : C ⥤ D<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : h.IsPreservedBy F<VAR>this✝ : PreservesColimit (parallelPair S.f 0) F<VAR>this : PreservesLimit (parallelPair h.g' 0) F<VAR>wp : F.map S.f ≫ F.map h.p = 0<VAR>hp : IsColimit ((CokernelCofork.ofπ h.p ⋯).map F)<VAR>g' : F.obj h.Q ⟶ F.obj S.X₃ := hp.desc (CokernelCofork.ofπ (S.map F).g ⋯)<GOAL>(S.map F).RightHomologyData
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{?u.31876, u_1} C<VAR>inst✝⁴ : Category.{?u.31880, u_2} D<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.RightHomologyData<VAR>F : C ⥤ D<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : h.IsPreservedBy F<VAR>this✝ : PreservesColimit (parallelPair S.f 0) F<VAR>this : PreservesLimit (parallelPair h.g' 0) F<VAR>wp : F.map S.f ≫ F.map h.p = 0<VAR>hp : IsColimit ((CokernelCofork.ofπ h.p ⋯).map F)<VAR>g' : F.obj h.Q ⟶ F.obj S.X₃ := hp.desc (CokernelCofork.ofπ (S.map F).g ⋯)<VAR>hg' : g' = F.map h.g'<GOAL>(S.map F).RightHomologyData
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{?u.31876, u_1} C<VAR>inst✝⁴ : Category.{?u.31880, u_2} D<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.RightHomologyData<VAR>F : C ⥤ D<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : h.IsPreservedBy F<VAR>this✝ : PreservesColimit (parallelPair S.f 0) F<VAR>this : PreservesLimit (parallelPair h.g' 0) F<VAR>wp : F.map S.f ≫ F.map h.p = 0<VAR>hp : IsColimit ((CokernelCofork.ofπ h.p ⋯).map F)<VAR>g' : F.obj h.Q ⟶ F.obj S.X₃ := hp.desc (CokernelCofork.ofπ (S.map F).g ⋯)<VAR>hg' : g' = F.map h.g'<VAR>wι : F.map h.ι ≫ g' = 0<GOAL>(S.map F).RightHomologyData
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>inst✝⁷ : Fintype l<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : CommRing α<VAR>A : Matrix m m α<VAR>B : Matrix m n α<VAR>C : Matrix n m α<VAR>D : Matrix n n α<VAR>inst✝ : Invertible A<GOAL>IsUnit (fromBlocks A B C D) ↔ IsUnit (D - C * ⅟A * B)
<VAR>R✝ : Type u<VAR>inst✝¹ : CommSemiring R✝<VAR>x y z : R✝<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>a b u v : ℤ<VAR>H : u * a + v * b = 1<GOAL>IsCoprime ↑a ↑b
<VAR>R✝ : Type u<VAR>inst✝¹ : CommSemiring R✝<VAR>x y z : R✝<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>a b u v : ℤ<VAR>H : u * a + v * b = 1<GOAL>↑u * ↑a + ↑v * ↑b = 1
<VAR>R✝ : Type u<VAR>inst✝¹ : CommSemiring R✝<VAR>x y z : R✝<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>a b u v : ℤ<VAR>H : u * a + v * b = 1<GOAL>↑1 = 1
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>F✝ F' : C ⥤ D<VAR>G✝ : D ⥤ E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>H : C ⥤ E<VAR>inst✝¹ : H.Full<VAR>inst✝ : G.Faithful<VAR>h : F ⋙ G ≅ H<GOAL>F.Full
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>F✝ F' : C ⥤ D<VAR>G✝ : D ⥤ E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>H : C ⥤ E<VAR>inst✝¹ : H.Full<VAR>inst✝ : G.Faithful<VAR>h : F ⋙ G ≅ H<VAR>this : (F ⋙ G).Full<GOAL>F.Full
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>k✝ : ℕ<VAR>N N₁ N₂ : LieSubmodule R L M<VAR>h : N₁ ≤ N₂<VAR>k : ℕ<VAR>ih : ucs k N₁ ≤ ucs k N₂<GOAL>ucs (k + 1) N₁ ≤ ucs (k + 1) N₂
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>k✝ : ℕ<VAR>N N₁ N₂ : LieSubmodule R L M<VAR>h : N₁ ≤ N₂<VAR>k : ℕ<VAR>ih : ucs k N₁ ≤ ucs k N₂<GOAL>(ucs k N₁).normalizer ≤ (ucs k N₂).normalizer
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝¹ : NonUnitalNonAssocRing α<VAR>inst✝ : Fintype n<VAR>M M' : Matrix m n α<VAR>N : Matrix n o α<GOAL>(M - M') * N = M * N - M' * N
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : M →ₗ[R] M<VAR>p q : R[X]<VAR>hpq : IsCoprime p q<GOAL>Disjoint (LinearMap.ker ((aeval f) p)) (LinearMap.ker ((aeval f) q))
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : M →ₗ[R] M<VAR>p q : R[X]<VAR>hpq : IsCoprime p q<GOAL>LinearMap.ker ((aeval f) p) ⊓ LinearMap.ker ((aeval f) q) ≤ ⊥
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : M →ₗ[R] M<VAR>p q : R[X]<VAR>v : M<VAR>hv : v ∈ LinearMap.ker ((aeval f) p) ⊓ LinearMap.ker ((aeval f) q)<VAR>p' q' : R[X]<VAR>hpq' : p' * p + q' * q = 1<GOAL>v ∈ ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<GOAL>BddBelow s.measureOfNegatives
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<GOAL>∃ x, ∀ x_1 ∈ s.measureOfNegatives, x ≤ x_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x<VAR>f : ℕ → ℝ<VAR>hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -↑n<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x<VAR>f : ℕ → ℝ<VAR>hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -↑n<VAR>hf' : ∀ (n : ℕ), ∃ B, MeasurableSet B ∧ restrict s B ≤ restrict 0 B ∧ ↑s B < -↑n<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x<VAR>f : ℕ → ℝ<VAR>hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -↑n<VAR>B : ℕ → Set α<VAR>hmeas : ∀ (n : ℕ), MeasurableSet (B n)<VAR>hr : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)<VAR>h_lt : ∀ (n : ℕ), ↑s (B n) < -↑n<VAR>A : Set α := ⋃ n, B n<VAR>hA : A = ⋃ n, B n<VAR>hfalse : ∀ (n : ℕ), ↑s A ≤ -↑n<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x<VAR>f : ℕ → ℝ<VAR>hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -↑n<VAR>B : ℕ → Set α<VAR>hmeas : ∀ (n : ℕ), MeasurableSet (B n)<VAR>hr : ∀ (n : ℕ), restrict s (B n) ≤ restrict 0 (B n)<VAR>h_lt : ∀ (n : ℕ), ↑s (B n) < -↑n<VAR>A : Set α := ⋃ n, B n<VAR>hA : A = ⋃ n, B n<VAR>hfalse : ∀ (n : ℕ), ↑s A ≤ -↑n<VAR>n : ℕ<VAR>hn : -↑s A < ↑n<GOAL>False
<VAR>x✝ y x : ℝ<GOAL>sinh (arsinh x) = x
<VAR>x✝ y x : ℝ<GOAL>(x + √(1 + x ^ 2) - (-x + √(1 + x ^ 2))) / 2 = x
<VAR>x✝ y x : ℝ<VAR>hx : 1 ≤ x<GOAL>arccos x = 0
<VAR>F✝ : Type u_1<VAR>E✝ : Type u_2<VAR>inst✝⁸ : Field F✝<VAR>inst✝⁷ : Field E✝<VAR>inst✝⁶ : Algebra F✝ E✝<VAR>inst✝⁵ : FiniteDimensional F✝ E✝<VAR>inst✝⁴ : Algebra.IsSeparable F✝ E✝<VAR>F : Type u_3<VAR>E : Type u_4<VAR>inst✝³ : Field F<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : FiniteDimensional F E<VAR>α : E<GOAL>F⟮α⟯ = ⊤ ↔ (minpoly F α).degree = ↑(finrank F E)
<VAR>F✝ : Type u_1<VAR>E✝ : Type u_2<VAR>inst✝⁸ : Field F✝<VAR>inst✝⁷ : Field E✝<VAR>inst✝⁶ : Algebra F✝ E✝<VAR>inst✝⁵ : FiniteDimensional F✝ E✝<VAR>inst✝⁴ : Algebra.IsSeparable F✝ E✝<VAR>F : Type u_3<VAR>E : Type u_4<VAR>inst✝³ : Field F<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : FiniteDimensional F E<VAR>α : E<GOAL>minpoly F α ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b c : Ordinal.{u_4}<VAR>h : b ≤ a<GOAL>c ≤ a - b ↔ b + c ≤ a
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>p : ℕ → ℝ<VAR>hp : ∀ (k : ℕ), 0 ≤ p k<VAR>r a : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<GOAL>∑ k ∈ Ico 2 (n + 1), a ^ k * ∑ c ∈ {c | 1 < c.length}.toFinset, r ^ c.length * ∏ j : Fin c.length, p (c.blocksFun j) = ∑ k ∈ Ico 2 (n + 1), ∑ c ∈ {c | 1 < c.length}.toFinset, ∏ j : Fin c.length, r * (a ^ c.blocksFun j * p (c.blocksFun j))
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>p : ℕ → ℝ<VAR>hp : ∀ (k : ℕ), 0 ≤ p k<VAR>r a : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<GOAL>∑ x ∈ Ico 2 (n + 1), ∑ i ∈ {c | 1 < c.length}.toFinset, a ^ x * (r ^ i.length * ∏ j : Fin i.length, p (i.blocksFun j)) = ∑ k ∈ Ico 2 (n + 1), ∑ c ∈ {c | 1 < c.length}.toFinset, ∏ j : Fin c.length, r * (a ^ c.blocksFun j * p (c.blocksFun j))
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>p : ℕ → ℝ<VAR>hp : ∀ (k : ℕ), 0 ≤ p k<VAR>r a : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<VAR>k : ℕ<VAR>a✝¹ : k ∈ Ico 2 (n + 1)<VAR>c : Composition k<VAR>a✝ : c ∈ {c | 1 < c.length}.toFinset<GOAL>a ^ k * (r ^ c.length * ∏ j : Fin c.length, p (c.blocksFun j)) = ∏ j : Fin c.length, r * (a ^ c.blocksFun j * p (c.blocksFun j))
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>p : ℕ → ℝ<VAR>hp : ∀ (k : ℕ), 0 ≤ p k<VAR>r a : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<VAR>k : ℕ<VAR>a✝¹ : k ∈ Ico 2 (n + 1)<VAR>c : Composition k<VAR>a✝ : c ∈ {c | 1 < c.length}.toFinset<GOAL>a ^ k * (r ^ c.length * ∏ j : Fin c.length, p (c.blocksFun j)) = r ^ c.length * (a ^ k * ∏ x : Fin c.length, p (c.blocksFun x))
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>p : ℕ → ℝ<VAR>hp : ∀ (k : ℕ), 0 ≤ p k<VAR>r a : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<GOAL>∑ k ∈ Ico 2 (n + 1), ∑ c ∈ {c | 1 < c.length}.toFinset, ∏ j : Fin c.length, r * (a ^ c.blocksFun j * p (c.blocksFun j)) ≤ ∑ d ∈ compPartialSumTarget 2 (n + 1) n, ∏ j : Fin d.snd.length, r * (a ^ d.snd.blocksFun j * p (d.snd.blocksFun j))
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>p : ℕ → ℝ<VAR>hp : ∀ (k : ℕ), 0 ≤ p k<VAR>r a : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<GOAL>∑ x ∈ (Ico 2 (n + 1)).sigma fun k => {c | 1 < c.length}.toFinset, ∏ j : Fin x.snd.length, r * (a ^ x.snd.blocksFun j * p (x.snd.blocksFun j)) ≤ ∑ d ∈ compPartialSumTarget 2 (n + 1) n, ∏ j : Fin d.snd.length, r * (a ^ d.snd.blocksFun j * p (d.snd.blocksFun j))
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>p : ℕ → ℝ<VAR>hp : ∀ (k : ℕ), 0 ≤ p k<VAR>r a : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<GOAL>((Ico 2 (n + 1)).sigma fun k => {c | 1 < c.length}.toFinset) ⊆ compPartialSumTarget 2 (n + 1) n
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>p : ℕ → ℝ<VAR>hp : ∀ (k : ℕ), 0 ≤ p k<VAR>r a : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<VAR>k : ℕ<VAR>c : Composition k<VAR>hd : ⟨k, c⟩ ∈ (Ico 2 (n + 1)).sigma fun k => {c | 1 < c.length}.toFinset<GOAL>⟨k, c⟩ ∈ compPartialSumTarget 2 (n + 1) n
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>p : ℕ → ℝ<VAR>hp : ∀ (k : ℕ), 0 ≤ p k<VAR>r a : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<VAR>k : ℕ<VAR>c : Composition k<VAR>hd : (2 ≤ k ∧ k < n + 1) ∧ 1 < c.length<GOAL>⟨k, c⟩ ∈ compPartialSumTarget 2 (n + 1) n
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>p : ℕ → ℝ<VAR>hp : ∀ (k : ℕ), 0 ≤ p k<VAR>r a : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<VAR>k : ℕ<VAR>c : Composition k<VAR>hd : (2 ≤ k ∧ k < n + 1) ∧ 1 < c.length<GOAL>2 ≤ c.length ∧ c.length < n + 1 ∧ ∀ (j : Fin c.length), c.blocksFun j < n
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>p : ℕ → ℝ<VAR>hp : ∀ (k : ℕ), 0 ≤ p k<VAR>r a : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<VAR>k : ℕ<VAR>c : Composition k<VAR>hd : (2 ≤ k ∧ k < n + 1) ∧ 1 < c.length<VAR>j : Fin c.length<GOAL>c.blocksFun j < n
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>p : ℕ → ℝ<VAR>hp : ∀ (k : ℕ), 0 ≤ p k<VAR>r a : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<VAR>k : ℕ<VAR>c : Composition k<VAR>hd : (2 ≤ k ∧ k < n + 1) ∧ 1 < c.length<VAR>j : Fin c.length<VAR>this : c ≠ Composition.single k ⋯<GOAL>c.blocksFun j < n
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>p : ℕ → ℝ<VAR>hp : ∀ (k : ℕ), 0 ≤ p k<VAR>r a : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<VAR>k : ℕ<VAR>c : Composition k<VAR>hd : (2 ≤ k ∧ k < n + 1) ∧ 1 < c.length<VAR>j : Fin c.length<VAR>this : ∀ (i : Fin c.length), c.blocksFun i < k<GOAL>c.blocksFun j < n
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>p : ℕ → ℝ<VAR>hp : ∀ (k : ℕ), 0 ≤ p k<VAR>r a : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<GOAL>∑ e ∈ compPartialSumSource 2 (n + 1) n, ∏ j : Fin e.fst, r * (a ^ e.snd j * p (e.snd j)) = ∑ d ∈ compPartialSumTarget 2 (n + 1) n, ∏ j : Fin d.snd.length, r * (a ^ d.snd.blocksFun j * p (d.snd.blocksFun j))
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>p : ℕ → ℝ<VAR>hp : ∀ (k : ℕ), 0 ≤ p k<VAR>r a : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<GOAL>∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource 2 (n + 1) n), ∏ j : Fin e.fst, r * (a ^ e.snd j * p (e.snd j)) = ∏ j : Fin (compChangeOfVariables 2 (n + 1) n e he).snd.length, r * (a ^ (compChangeOfVariables 2 (n + 1) n e he).snd.blocksFun j * p ((compChangeOfVariables 2 (n + 1) n e he).snd.blocksFun j))
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>p : ℕ → ℝ<VAR>hp : ∀ (k : ℕ), 0 ≤ p k<VAR>r a : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<VAR>k : ℕ<VAR>blocks_fun : Fin k → ℕ<VAR>H : ⟨k, blocks_fun⟩ ∈ compPartialSumSource 2 (n + 1) n<VAR>K : (compChangeOfVariables 2 (n + 1) n ⟨k, blocks_fun⟩ H).snd.length = k<GOAL>HEq (fun j => r * (a ^ ⟨k, blocks_fun⟩.snd j * p (⟨k, blocks_fun⟩.snd j))) fun j => r * (a ^ (compChangeOfVariables 2 (n + 1) n ⟨k, blocks_fun⟩ H).snd.blocksFun j * p ((compChangeOfVariables 2 (n + 1) n ⟨k, blocks_fun⟩ H).snd.blocksFun j))
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>p : ℕ → ℝ<VAR>hp : ∀ (k : ℕ), 0 ≤ p k<VAR>r a : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<VAR>k : ℕ<VAR>blocks_fun : Fin k → ℕ<VAR>H : ⟨k, blocks_fun⟩ ∈ compPartialSumSource 2 (n + 1) n<VAR>K : (compChangeOfVariables 2 (n + 1) n ⟨k, blocks_fun⟩ H).snd.length = k<GOAL>∀ (i : Fin k), r * (a ^ ⟨k, blocks_fun⟩.snd i * p (⟨k, blocks_fun⟩.snd i)) = r * (a ^ (compChangeOfVariables 2 (n + 1) n ⟨k, blocks_fun⟩ H).snd.blocksFun ⟨↑i, ⋯⟩ * p ((compChangeOfVariables 2 (n + 1) n ⟨k, blocks_fun⟩ H).snd.blocksFun ⟨↑i, ⋯⟩))
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>n : ℕ<VAR>p : ℕ → ℝ<VAR>hp : ∀ (k : ℕ), 0 ≤ p k<VAR>r a : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<VAR>k : ℕ<VAR>blocks_fun : Fin k → ℕ<VAR>H : ⟨k, blocks_fun⟩ ∈ compPartialSumSource 2 (n + 1) n<VAR>K : (compChangeOfVariables 2 (n + 1) n ⟨k, blocks_fun⟩ H).snd.length = k<VAR>j : Fin k<GOAL>r * (a ^ ⟨k, blocks_fun⟩.snd j * p (⟨k, blocks_fun⟩.snd j)) = r * (a ^ (compChangeOfVariables 2 (n + 1) n ⟨k, blocks_fun⟩ H).snd.blocksFun ⟨↑j, ⋯⟩ * p ((compChangeOfVariables 2 (n + 1) n ⟨k, blocks_fun⟩ H).snd.blocksFun ⟨↑j, ⋯⟩))