ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>v : ↑(sphere 0 1)<GOAL>Injective ⇑(fderivWithin ℝ (writtenInExtChartAt 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) 𝓘(ℝ, E) v Subtype.val) (Set.range ↑𝓘(ℝ, EuclideanSpace ℝ (Fin n))) (↑(extChartAt 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) v) v))
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>v : ↑(sphere 0 1)<GOAL>Injective ⇑(fderiv ℝ (Subtype.val ∘ ↑(ChartedSpace.chartAt v).symm) (↑(ChartedSpace.chartAt v) v))
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>v : ↑(sphere 0 1)<VAR>U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr<GOAL>Injective ⇑(fderiv ℝ (Subtype.val ∘ ↑(ChartedSpace.chartAt v).symm) (↑(ChartedSpace.chartAt v) v))
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>v : ↑(sphere 0 1)<VAR>U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr<GOAL>Injective ⇑(fderiv ℝ ((stereoInvFunAux (-↑v) ∘ Subtype.val) ∘ ⇑U.symm) 0)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>v : ↑(sphere 0 1)<VAR>U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr<VAR>this : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (Submodule.span ℝ {↑(-v)})ᗮ.subtypeL (U.symm 0)<GOAL>Injective ⇑(fderiv ℝ ((stereoInvFunAux (-↑v) ∘ Subtype.val) ∘ ⇑U.symm) 0)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>v : ↑(sphere 0 1)<VAR>U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr<VAR>this✝ : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (Submodule.span ℝ {↑(-v)})ᗮ.subtypeL (U.symm 0)<VAR>this : ⇑(fderiv ℝ ((stereoInvFunAux (-↑v) ∘ Subtype.val) ∘ ⇑U.symm) 0) = ⇑((Submodule.span ℝ {↑(-v)})ᗮ.subtypeL.comp ↑U.symm.toContinuousLinearEquiv)<GOAL>Injective ⇑(fderiv ℝ ((stereoInvFunAux (-↑v) ∘ Subtype.val) ∘ ⇑U.symm) 0)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>v : ↑(sphere 0 1)<VAR>U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr<VAR>this✝ : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (Submodule.span ℝ {↑(-v)})ᗮ.subtypeL (U.symm 0)<VAR>this : ⇑(fderiv ℝ ((stereoInvFunAux (-↑v) ∘ Subtype.val) ∘ ⇑U.symm) 0) = ⇑((Submodule.span ℝ {↑(-v)})ᗮ.subtypeL.comp ↑U.symm.toContinuousLinearEquiv)<GOAL>Injective ⇑((Submodule.span ℝ {↑(-v)})ᗮ.subtypeL.comp ↑U.symm.toContinuousLinearEquiv)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>v : ↑(sphere 0 1)<VAR>U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr<VAR>this✝ : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (Submodule.span ℝ {↑(-v)})ᗮ.subtypeL (U.symm 0)<VAR>this : ⇑(fderiv ℝ ((stereoInvFunAux (-↑v) ∘ Subtype.val) ∘ ⇑U.symm) 0) = ⇑((Submodule.span ℝ {↑(-v)})ᗮ.subtypeL.comp ↑U.symm.toContinuousLinearEquiv)<GOAL>Injective (⇑(Submodule.span ℝ {↑(-v)})ᗮ.subtypeL ∘ ⇑U.symm.toContinuousLinearEquiv)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>ν : Measure α<VAR>ι : Type u_7<VAR>m : MeasurableSpace α<VAR>f : α → G<VAR>μ : ι → Measure α<VAR>s : Finset ι<VAR>hf : ∀ i ∈ s, Integrable f (μ i)<GOAL>∫ (a : α), f a ∂∑ i ∈ s, μ i = ∑ i ∈ s, ∫ (a : α), f a ∂μ i
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u : Multiset α<VAR>a✝ b a : α<VAR>s t : Multiset α<VAR>h : t ≤ s<GOAL>a ::ₘ s - t = a ::ₘ (s - t)
<VAR>G : Type u<VAR>M : Type v<VAR>α : Type w<VAR>s : Set α<VAR>m : MeasurableSpace α<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : MulAction G α<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : MeasurableSMul G α<VAR>c : G<VAR>μ : Measure α<VAR>inst✝⁴ : SMulInvariantMeasure G α μ<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : ContinuousConstSMul G α<VAR>inst✝¹ : MulAction.IsMinimal G α<VAR>K U : Set α<VAR>inst✝ : μ.Regular<VAR>hμ : μ ≠ 0<VAR>hU : IsOpen U<GOAL>μ U = 0 ↔ U = ∅
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs cs1 cs2 : CoxeterSystem M W<VAR>h : cs1.simple = cs2.simple<GOAL>cs1.mulEquiv = cs2.mulEquiv
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs cs1 cs2 : CoxeterSystem M W<VAR>h : cs1.simple = cs2.simple<GOAL>cs1.mulEquiv.toMonoidHom = cs2.mulEquiv.toMonoidHom
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs cs1 cs2 : CoxeterSystem M W<VAR>h : cs1.simple = cs2.simple<GOAL>∀ (i : B), cs1.mulEquiv.toMonoidHom (cs1.simple i) = cs2.mulEquiv.toMonoidHom (cs1.simple i)
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f✝ f : V → E<VAR>hf : Continuous f<VAR>n : ℕ<GOAL>Continuous fun v => VectorFourier.fourierPowSMulRight L f v n
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f✝ f : V → E<VAR>hf : Continuous f<VAR>n : ℕ<GOAL>Continuous fun v => (-(2 * ↑π * I)) ^ n • ((smulRightL ℝ (fun x => W) E) ((ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight fun x => L v)) (f v)
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f✝ f : V → E<VAR>hf : Continuous f<VAR>n : ℕ<GOAL>Continuous fun x => ((smulRightL ℝ (fun x => W) E) ((ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight fun x_1 => L x)) (f x)
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f✝ f : V → E<VAR>hf : Continuous f<VAR>n : ℕ<GOAL>Continuous fun w => (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight fun x => L w
<VAR>R : Type u<VAR>inst✝³ : Semiring R<VAR>inst✝² : RankCondition R<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>f : (α →₀ R) →ₗ[R] β →₀ R<VAR>i : Surjective ⇑f<VAR>P : (β →₀ R) ≃ₗ[R] β → R := Finsupp.linearEquivFunOnFinite R R β<VAR>Q : (α → R) ≃ₗ[R] α →₀ R := (Finsupp.linearEquivFunOnFinite R R α).symm<GOAL>Fintype.card β ≤ Fintype.card α
<VAR>y : ℝ<VAR>hy : y ≠ 0<VAR>x : ℝ≥0∞<GOAL>(x ^ y⁻¹) ^ y = x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : DecidableEq α<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableRel Disjoint<VAR>s s₁ s₂ t t₁ t₂ u : Finset α<VAR>a b c : α<VAR>p : α → Prop<GOAL>(∀ c ∈ s ○ t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : DecidableEq α<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableRel Disjoint<VAR>s s₁ s₂ t t₁ t₂ u : Finset α<VAR>a b c : α<VAR>p : α → Prop<GOAL>(∀ (c : α), (∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = c) → p c) ↔ ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b)
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)<VAR>M : HomologicalComplex C c<VAR>α : K ⟶ M<VAR>β : L ⟶ M<VAR>i : ι<GOAL>biprod.inr.f i ≫ (biprod.desc α β).f i = β.f i
<VAR>a x z : ℂ<GOAL>(-1).arg = π
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g✝ : ι → α<VAR>h : TendstoUniformly F f p<VAR>g : γ → α<GOAL>TendstoUniformly (fun n => F n ∘ g) (f ∘ g) p
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g✝ : ι → α<VAR>h : TendstoUniformlyOnFilter F f p ⊤<VAR>g : γ → α<GOAL>TendstoUniformlyOnFilter (fun n => F n ∘ g) (f ∘ g) p ⊤
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>f✝¹ : ℝ → E<VAR>g' g✝ φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝² : CompleteSpace E<VAR>f✝ f'✝ : ℝ → E<VAR>G : Type u_6<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f f' : ℝ → ℝ<VAR>g : ℝ → G<VAR>hf : ContinuousOn f [[a, b]]<VAR>hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hf' : ContinuousOn f' [[a, b]]<VAR>hg : ContinuousOn g (f '' [[a, b]])<GOAL>∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>f✝¹ : ℝ → E<VAR>g' g✝ φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝² : CompleteSpace E<VAR>f✝ f'✝ : ℝ → E<VAR>G : Type u_6<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f f' : ℝ → ℝ<VAR>g : ℝ → G<VAR>hf : ContinuousOn f [[a, b]]<VAR>hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hf' : ContinuousOn f' [[a, b]]<VAR>hg : ContinuousOn g (f '' [[a, b]])<GOAL>IntegrableOn g (f '' [[a, b]]) volume
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>f✝¹ : ℝ → E<VAR>g' g✝ φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝² : CompleteSpace E<VAR>f✝ f'✝ : ℝ → E<VAR>G : Type u_6<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f f' : ℝ → ℝ<VAR>g : ℝ → G<VAR>hf : ContinuousOn f [[a, b]]<VAR>hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hf' : ContinuousOn f' [[a, b]]<VAR>hg : ContinuousOn g [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]]<GOAL>IntegrableOn g [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]] volume
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>s✝ t✝ r s t : Set α<VAR>h : Disjoint s t<GOAL>range ⇑(sumSet h) = s ∪ t
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq p<VAR>inst✝ : CommRing R<VAR>r : ℕ<VAR>M✝ : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>IH : ∀ (M : Matrix (Fin r) (Fin r) 𝕜), ∃ L₀ L₀' D₀, (List.map toMatrix L₀).prod * M * (List.map toMatrix L₀').prod = diagonal D₀<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<GOAL>∃ L L' D, (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq p<VAR>inst✝ : CommRing R<VAR>r : ℕ<VAR>M✝ : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>IH : ∀ (M : Matrix (Fin r) (Fin r) 𝕜), ∃ L₀ L₀' D₀, (List.map toMatrix L₀).prod * M * (List.map toMatrix L₀').prod = diagonal D₀<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>L₁ L₁' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)<VAR>hM : ((List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod).IsTwoBlockDiagonal<GOAL>∃ L L' D, (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq p<VAR>inst✝ : CommRing R<VAR>r : ℕ<VAR>M✝ : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>IH : ∀ (M : Matrix (Fin r) (Fin r) 𝕜), ∃ L₀ L₀' D₀, (List.map toMatrix L₀).prod * M * (List.map toMatrix L₀').prod = diagonal D₀<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>L₁ L₁' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)<VAR>hM : ((List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod).IsTwoBlockDiagonal<VAR>M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := (List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod<VAR>M'' : Matrix (Fin r) (Fin r) 𝕜 := M'.toBlocks₁₁<VAR>L₀ L₀' : List (TransvectionStruct (Fin r) 𝕜)<VAR>D₀ : Fin r → 𝕜<VAR>h₀ : (List.map toMatrix L₀).prod * M'' * (List.map toMatrix L₀').prod = diagonal D₀<VAR>c : 𝕜 := M' (inr ()) (inr ())<GOAL>(List.map toMatrix (List.map (sumInl Unit) L₀ ++ L₁)).prod * M * (List.map toMatrix (L₁' ++ List.map (sumInl Unit) L₀')).prod = diagonal (Sum.elim D₀ fun x => M' (inr ()) (inr ()))
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq p<VAR>inst✝ : CommRing R<VAR>r : ℕ<VAR>M✝ : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>IH : ∀ (M : Matrix (Fin r) (Fin r) 𝕜), ∃ L₀ L₀' D₀, (List.map toMatrix L₀).prod * M * (List.map toMatrix L₀').prod = diagonal D₀<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>L₁ L₁' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)<VAR>hM : ((List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod).IsTwoBlockDiagonal<VAR>M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := (List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod<VAR>M'' : Matrix (Fin r) (Fin r) 𝕜 := M'.toBlocks₁₁<VAR>L₀ L₀' : List (TransvectionStruct (Fin r) 𝕜)<VAR>D₀ : Fin r → 𝕜<VAR>h₀ : (List.map toMatrix L₀).prod * M'' * (List.map toMatrix L₀').prod = diagonal D₀<VAR>c : 𝕜 := M' (inr ()) (inr ())<GOAL>(List.map (toMatrix ∘ sumInl Unit) L₀).prod * M' * (List.map (toMatrix ∘ sumInl Unit) L₀').prod = diagonal (Sum.elim D₀ fun x => c)
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq p<VAR>inst✝ : CommRing R<VAR>r : ℕ<VAR>M✝ : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>IH : ∀ (M : Matrix (Fin r) (Fin r) 𝕜), ∃ L₀ L₀' D₀, (List.map toMatrix L₀).prod * M * (List.map toMatrix L₀').prod = diagonal D₀<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>L₁ L₁' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)<VAR>hM : ((List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod).IsTwoBlockDiagonal<VAR>M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := (List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod<VAR>M'' : Matrix (Fin r) (Fin r) 𝕜 := M'.toBlocks₁₁<VAR>L₀ L₀' : List (TransvectionStruct (Fin r) 𝕜)<VAR>D₀ : Fin r → 𝕜<VAR>h₀ : (List.map toMatrix L₀).prod * M'' * (List.map toMatrix L₀').prod = diagonal D₀<VAR>c : 𝕜 := M' (inr ()) (inr ())<VAR>this : M' = fromBlocks M'' 0 0 (diagonal fun x => c)<GOAL>(List.map (toMatrix ∘ sumInl Unit) L₀).prod * M' * (List.map (toMatrix ∘ sumInl Unit) L₀').prod = diagonal (Sum.elim D₀ fun x => c)
<VAR>n : ℤ<GOAL>↑n.toNat + ↑(-n).toNat = ‖n‖₊
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type x<VAR>k : Type y<VAR>A✝ : Type z<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r : R[X]<VAR>M : R[X] → Prop<VAR>p : R[X]<VAR>h_C : ∀ (a : R), M (C a)<VAR>h_add : ∀ (p q : R[X]), M p → M q → M (p + q)<VAR>h_monomial : ∀ (n : ℕ) (a : R), M (C a * X ^ n) → M (C a * X ^ (n + 1))<VAR>A : ∀ {n : ℕ} {a : R}, M (C a * X ^ n)<VAR>B : ∀ (s : Finset ℕ), M (∑ n ∈ s, C (p.coeff n) * X ^ n)<GOAL>M p
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type x<VAR>k : Type y<VAR>A✝ : Type z<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r : R[X]<VAR>M : R[X] → Prop<VAR>p : R[X]<VAR>h_C : ∀ (a : R), M (C a)<VAR>h_add : ∀ (p q : R[X]), M p → M q → M (p + q)<VAR>h_monomial : ∀ (n : ℕ) (a : R), M (C a * X ^ n) → M (C a * X ^ (n + 1))<VAR>A : ∀ {n : ℕ} {a : R}, M (C a * X ^ n)<VAR>B : ∀ (s : Finset ℕ), M (∑ n ∈ s, C (p.coeff n) * X ^ n)<GOAL>M (∑ n ∈ p.support, C (p.coeff n) * X ^ n)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>j : ℕ<GOAL>(cs.leftInvSeq ω).getD j 1 * cs.wordProd ω = cs.wordProd (ω.eraseIdx j)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>j : ℕ<GOAL>cs.wordProd (take j ω) * (Option.map cs.simple (ω.get? j)).getD 1 * (cs.wordProd (take j ω))⁻¹ * cs.wordProd ω = cs.wordProd (take j ω ++ drop (j + 1) ω)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>j : ℕ<GOAL>cs.wordProd (take j ω) * (Option.map cs.simple (ω.get? j)).getD 1 * (cs.wordProd (take j ω))⁻¹ * cs.wordProd (take (j + 1) ω ++ drop (j + 1) ω) = cs.wordProd (take j ω ++ drop (j + 1) ω)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>j : ℕ<GOAL>cs.wordProd (take j ω) * (Option.map cs.simple (ω.get? j)).getD 1 * (cs.wordProd (take j ω))⁻¹ * cs.wordProd (take j ω ++ ω[j]?.toList ++ drop (j + 1) ω) = cs.wordProd (take j ω ++ drop (j + 1) ω)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>j : ℕ<VAR>lt : j < ω.length<GOAL>cs.wordProd (take j ω) * (Option.map cs.simple (ω.get? j)).getD 1 * (cs.wordProd (take j ω))⁻¹ * cs.wordProd (take j ω ++ ω[j]?.toList ++ drop (j + 1) ω) = cs.wordProd (take j ω ++ drop (j + 1) ω)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>j : ℕ<VAR>le : ω.length ≤ j<GOAL>cs.wordProd (take j ω) * (Option.map cs.simple (ω.get? j)).getD 1 * (cs.wordProd (take j ω))⁻¹ * cs.wordProd (take j ω ++ ω[j]?.toList ++ drop (j + 1) ω) = cs.wordProd (take j ω ++ drop (j + 1) ω)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (completedSinZeta (↑a) s / (s + 1).Gammaℝ)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>n : ℤ<GOAL>-I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2 = (s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2 / (s + 1).Gammaℝ
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>n : ℤ<VAR>this : 0 < (s + 1).re<GOAL>-I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2 = (s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2 / (s + 1).Gammaℝ
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A B : M<VAR>h : Commute A B<VAR>m : ℤ<GOAL>Commute A (B ^ m)
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A B : M<VAR>h : Commute A B<VAR>m : ℤ<VAR>hB : B⁻¹ * B = 1<VAR>right✝ : B * B⁻¹ = 1<GOAL>Commute A (B ^ m)
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A B : M<VAR>h : Commute A B<VAR>m : ℤ<VAR>hB : B⁻¹ = 0<GOAL>Commute A (B ^ m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s✝ t✝ s t : SignedMeasure α<VAR>μ : Measure α<VAR>inst✝¹ : s.HaveLebesgueDecomposition μ<VAR>inst✝ : t.HaveLebesgueDecomposition μ<GOAL>(s - t).singularPart μ = s.singularPart μ - t.singularPart μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u}<GOAL>type (Subrel (fun x x_1 => x < x_1) {o' | o' < o}) = lift.{u + 1, u} o
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u}<GOAL>∀ (a : WellOrder), type (Subrel (fun x x_1 => x < x_1) {o' | o' < ⟦a⟧}) = lift.{u + 1, u} ⟦a⟧
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α✝ → α✝ → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u}<VAR>α : Type u<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<GOAL>type (Subrel (fun x x_1 => x < x_1) {o' | o' < ⟦{ α := α, r := r, wo := wo }⟧}) = lift.{u + 1, u} ⟦{ α := α, r := r, wo := wo }⟧
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α✝ → α✝ → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u}<VAR>α : Type u<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<GOAL>{ α := ↑{o' | o' < ⟦{ α := α, r := r, wo := wo }⟧}, r := Subrel (fun x x_1 => x < x_1) {o' | o' < ⟦{ α := α, r := r, wo := wo }⟧}, wo := ⋯ } ≈ { α := ULift.{u + 1, u} { α := α, r := r, wo := wo }.α, r := ULift.down ⁻¹'o { α := α, r := r, wo := wo }.r, wo := ⋯ }
<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>a : ℝ≥0∞<GOAL>a / 3 + a / 3 + a / 3 = a