ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : NonUnitalNormedRing A<VAR>inst✝³ : NormedSpace 𝕜 A<VAR>inst✝² : IsScalarTower 𝕜 A A<VAR>inst✝¹ : SMulCommClass 𝕜 A A<VAR>inst✝ : RegularNormedAlgebra 𝕜 A<VAR>x : Unitization 𝕜 A<GOAL>‖x‖ = ‖x.fst‖ ⊔ ‖(algebraMap 𝕜 (A →L[𝕜] A)) x.fst + (mul 𝕜 A) x.snd‖
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a✝ b✝ c✝ d a b c : α<GOAL>a ⇨ b ⇨ c = b ⇨ a ⇨ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s✝ t u : Set α<VAR>inst✝³ : PseudoEMetricSpace α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>x : α<VAR>ε : ℝ≥0∞<VAR>μ : Measure α<VAR>s : Set α<VAR>hs : ∃ R > 0, μ (cthickening R s) ≠ ⊤<VAR>h's : IsClosed s<GOAL>Tendsto (fun r => μ (cthickening r s)) (𝓝 0) (𝓝 (μ s))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s✝ t u : Set α<VAR>inst✝³ : PseudoEMetricSpace α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>x : α<VAR>ε : ℝ≥0∞<VAR>μ : Measure α<VAR>s : Set α<VAR>hs : ∃ R > 0, μ (cthickening R s) ≠ ⊤<VAR>h's : IsClosed s<GOAL>s = closure s
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>hx : AlgebraicIndependent R x<GOAL>Injective ⇑(algebraMap R A)
<VAR>α : Type u_1<VAR>inst✝ : SizeOf α<VAR>l₁ l₂ : List α<VAR>h : l₁ ~ l₂<GOAL>sizeOf l₁ = sizeOf l₂
<VAR>x : ℤ[i]<GOAL>toComplex x = { re := ↑x.re, im := ↑x.im }
<VAR>r : ℝ<GOAL>1 ≤ r.toNNReal ↔ 1 ≤ r
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>a : R<VAR>n : ℕ<VAR>h : p ≠ 0<GOAL>rootMultiplicity a (p * (X - C a) ^ n) = rootMultiplicity a p + n
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>a : R<VAR>n : ℕ<VAR>h : p ≠ 0<VAR>h2 : p * (X - C a) ^ n ≠ 0<GOAL>rootMultiplicity a (p * (X - C a) ^ n) = rootMultiplicity a p + n
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>a : R<VAR>n : ℕ<VAR>h : p ≠ 0<VAR>h2 : p * (X - C a) ^ n ≠ 0<GOAL>rootMultiplicity a (p * (X - C a) ^ n) ≤ rootMultiplicity a p + n
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>a : R<VAR>n : ℕ<VAR>h : p ≠ 0<VAR>h2 : p * (X - C a) ^ n ≠ 0<GOAL>rootMultiplicity a p + n ≤ rootMultiplicity a (p * (X - C a) ^ n)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 0<VAR>hc : P.c ≠ 0<GOAL>P.toPoly.natDegree = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>F : ι → α →ᵤ β<VAR>f : α →ᵤ β<GOAL>Tendsto F p (𝓝 f) ↔ TendstoUniformly (⇑toFun ∘ F) (toFun f) p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>F : ι → α →ᵤ β<VAR>f : α →ᵤ β<GOAL>(∀ i ∈ 𝓤 β, ∀ᶠ (x : ι) in p, F x ∈ {g | (f, g) ∈ UniformFun.gen α β i}) ↔ ∀ u ∈ 𝓤 β, ∀ᶠ (n : ι) in p, ∀ (x : α), (toFun f x, (⇑toFun ∘ F) n x) ∈ u
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>Z X✝ Y P : C<VAR>f : Z ⟶ X✝<VAR>g : Z ⟶ Y<VAR>inl : X✝ ⟶ P<VAR>inr : Y ⟶ P<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>X : C<VAR>s : Cocone (span 0 (𝟙 X))<GOAL>∀ (j : WalkingSpan), (PushoutCocone.mk 0 0 ⋯).ι.app j ≫ (fun s => 0) s = s.ι.app j
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>Z X✝ Y P : C<VAR>f : Z ⟶ X✝<VAR>g : Z ⟶ Y<VAR>inl : X✝ ⟶ P<VAR>inr : Y ⟶ P<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>X : C<VAR>s : Cocone (span 0 (𝟙 X))<VAR>c : ∀ (j : WalkingSpan), s.ι.app j ≫ 0 = s.ι.app j ≫ 𝟙 s.pt<GOAL>∀ (j : WalkingSpan), (PushoutCocone.mk 0 0 ⋯).ι.app j ≫ (fun s => 0) s = s.ι.app j
<VAR>𝕜 : Type u_1<VAR>inst✝²⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝²³ : NormedAddCommGroup E<VAR>inst✝²² : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝²¹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝²⁰ : TopologicalSpace M<VAR>inst✝¹⁹ : ChartedSpace H M<VAR>Is : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁸ : NormedAddCommGroup E'<VAR>inst✝¹⁷ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁶ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝¹⁵ : TopologicalSpace M'<VAR>inst✝¹⁴ : ChartedSpace H' M'<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N✝ : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N✝<VAR>inst✝⁹ : ChartedSpace G N✝<VAR>Js : SmoothManifoldWithCorners J N✝<VAR>F' : Type u_11<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝⁶ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝⁵ : TopologicalSpace N'<VAR>inst✝⁴ : ChartedSpace G' N'<VAR>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>x : M<VAR>v : TangentSpace I x<VAR>N : ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (↑I (↑(chartAt H x) x))<GOAL>tangentMap I I.tangent (zeroSection E (TangentSpace I)) { proj := x, snd := v } = { proj := { proj := { proj := x, snd := v }.proj, snd := 0 }, snd := ({ proj := x, snd := v }.snd, 0) }
<VAR>𝕜 : Type u_1<VAR>inst✝²⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝²³ : NormedAddCommGroup E<VAR>inst✝²² : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝²¹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝²⁰ : TopologicalSpace M<VAR>inst✝¹⁹ : ChartedSpace H M<VAR>Is : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁸ : NormedAddCommGroup E'<VAR>inst✝¹⁷ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁶ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝¹⁵ : TopologicalSpace M'<VAR>inst✝¹⁴ : ChartedSpace H' M'<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N✝ : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N✝<VAR>inst✝⁹ : ChartedSpace G N✝<VAR>Js : SmoothManifoldWithCorners J N✝<VAR>F' : Type u_11<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝⁶ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝⁵ : TopologicalSpace N'<VAR>inst✝⁴ : ChartedSpace G' N'<VAR>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>x : M<VAR>v : TangentSpace I x<VAR>N : ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (↑I (↑(chartAt H x) x))<VAR>A : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := 0 }) x<GOAL>tangentMap I I.tangent (zeroSection E (TangentSpace I)) { proj := x, snd := v } = { proj := { proj := { proj := x, snd := v }.proj, snd := 0 }, snd := ({ proj := x, snd := v }.snd, 0) }
<VAR>𝕜 : Type u_1<VAR>inst✝²⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝²³ : NormedAddCommGroup E<VAR>inst✝²² : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝²¹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝²⁰ : TopologicalSpace M<VAR>inst✝¹⁹ : ChartedSpace H M<VAR>Is : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁸ : NormedAddCommGroup E'<VAR>inst✝¹⁷ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁶ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝¹⁵ : TopologicalSpace M'<VAR>inst✝¹⁴ : ChartedSpace H' M'<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N✝ : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N✝<VAR>inst✝⁹ : ChartedSpace G N✝<VAR>Js : SmoothManifoldWithCorners J N✝<VAR>F' : Type u_11<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝⁶ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝⁵ : TopologicalSpace N'<VAR>inst✝⁴ : ChartedSpace G' N'<VAR>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>x : M<VAR>v : TangentSpace I x<VAR>N : ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (↑I (↑(chartAt H x) x))<VAR>A : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := 0 }) x<VAR>B : (fderivWithin 𝕜 (fun x' => (x', 0)) (range ↑I) (↑I (↑(chartAt H x) x))) v = (v, 0)<GOAL>tangentMap I I.tangent (zeroSection E (TangentSpace I)) { proj := x, snd := v } = { proj := { proj := { proj := x, snd := v }.proj, snd := 0 }, snd := ({ proj := x, snd := v }.snd, 0) }
<VAR>𝕜 : Type u_1<VAR>inst✝²⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝²³ : NormedAddCommGroup E<VAR>inst✝²² : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝²¹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝²⁰ : TopologicalSpace M<VAR>inst✝¹⁹ : ChartedSpace H M<VAR>Is : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁸ : NormedAddCommGroup E'<VAR>inst✝¹⁷ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁶ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝¹⁵ : TopologicalSpace M'<VAR>inst✝¹⁴ : ChartedSpace H' M'<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N✝ : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N✝<VAR>inst✝⁹ : ChartedSpace G N✝<VAR>Js : SmoothManifoldWithCorners J N✝<VAR>F' : Type u_11<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝⁶ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝⁵ : TopologicalSpace N'<VAR>inst✝⁴ : ChartedSpace G' N'<VAR>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>x : M<VAR>v : TangentSpace I x<VAR>N : ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (↑I (↑(chartAt H x) x))<VAR>A : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := 0 }) x<VAR>B : (fderivWithin 𝕜 (fun x' => (x', 0)) (range ↑I) (↑I (↑(chartAt H x) x))) v = (v, 0)<GOAL>(fderivWithin 𝕜 (fun x_1 => (↑I (↑(ChartedSpace.chartAt x) (↑(ChartedSpace.chartAt x).symm (↑I.symm x_1))), 0)) (range ↑I) (↑I (↑(ChartedSpace.chartAt x) x))) v = (v, 0)
<VAR>𝕜 : Type u_1<VAR>inst✝²⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝²³ : NormedAddCommGroup E<VAR>inst✝²² : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝²¹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝²⁰ : TopologicalSpace M<VAR>inst✝¹⁹ : ChartedSpace H M<VAR>Is : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁸ : NormedAddCommGroup E'<VAR>inst✝¹⁷ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁶ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝¹⁵ : TopologicalSpace M'<VAR>inst✝¹⁴ : ChartedSpace H' M'<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N✝ : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N✝<VAR>inst✝⁹ : ChartedSpace G N✝<VAR>Js : SmoothManifoldWithCorners J N✝<VAR>F' : Type u_11<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝⁶ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝⁵ : TopologicalSpace N'<VAR>inst✝⁴ : ChartedSpace G' N'<VAR>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>x : M<VAR>v : TangentSpace I x<VAR>N : ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (↑I (↑(chartAt H x) x))<VAR>A : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := 0 }) x<VAR>B : (fderivWithin 𝕜 (fun x' => (x', 0)) (range ↑I ∩ ↑I.symm ⁻¹' (chartAt H x).target) (↑I (↑(chartAt H x) x))) v = (v, 0)<GOAL>(fderivWithin 𝕜 (fun x_1 => (↑I (↑(ChartedSpace.chartAt x) (↑(ChartedSpace.chartAt x).symm (↑I.symm x_1))), 0)) (range ↑I) (↑I (↑(ChartedSpace.chartAt x) x))) v = (v, 0)
<VAR>𝕜 : Type u_1<VAR>inst✝²⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝²³ : NormedAddCommGroup E<VAR>inst✝²² : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝²¹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝²⁰ : TopologicalSpace M<VAR>inst✝¹⁹ : ChartedSpace H M<VAR>Is : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁸ : NormedAddCommGroup E'<VAR>inst✝¹⁷ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁶ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝¹⁵ : TopologicalSpace M'<VAR>inst✝¹⁴ : ChartedSpace H' M'<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N✝ : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N✝<VAR>inst✝⁹ : ChartedSpace G N✝<VAR>Js : SmoothManifoldWithCorners J N✝<VAR>F' : Type u_11<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝⁶ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝⁵ : TopologicalSpace N'<VAR>inst✝⁴ : ChartedSpace G' N'<VAR>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>x : M<VAR>v : TangentSpace I x<VAR>N : ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (↑I (↑(chartAt H x) x))<VAR>A : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := 0 }) x<VAR>B : (fderivWithin 𝕜 (fun x' => (x', 0)) (range ↑I ∩ ↑I.symm ⁻¹' (chartAt H x).target) (↑I (↑(chartAt H x) x))) v = (v, 0)<GOAL>(fderivWithin 𝕜 (fun x_1 => (↑I (↑(ChartedSpace.chartAt x) (↑(ChartedSpace.chartAt x).symm (↑I.symm x_1))), 0)) (range ↑I ∩ ↑I.symm ⁻¹' (chartAt H x).target) (↑I (↑(chartAt H x) x))) v = (fderivWithin 𝕜 (fun x' => (x', 0)) (range ↑I ∩ ↑I.symm ⁻¹' (chartAt H x).target) (↑I (↑(chartAt H x) x))) v
<VAR>𝕜 : Type u_1<VAR>inst✝²⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝²³ : NormedAddCommGroup E<VAR>inst✝²² : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝²¹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝²⁰ : TopologicalSpace M<VAR>inst✝¹⁹ : ChartedSpace H M<VAR>Is : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁸ : NormedAddCommGroup E'<VAR>inst✝¹⁷ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁶ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝¹⁵ : TopologicalSpace M'<VAR>inst✝¹⁴ : ChartedSpace H' M'<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N✝ : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N✝<VAR>inst✝⁹ : ChartedSpace G N✝<VAR>Js : SmoothManifoldWithCorners J N✝<VAR>F' : Type u_11<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝⁶ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝⁵ : TopologicalSpace N'<VAR>inst✝⁴ : ChartedSpace G' N'<VAR>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>x : M<VAR>v : TangentSpace I x<VAR>N : ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (↑I (↑(chartAt H x) x))<VAR>A : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := 0 }) x<VAR>B : (fderivWithin 𝕜 (fun x' => (x', 0)) (range ↑I ∩ ↑I.symm ⁻¹' (chartAt H x).target) (↑I (↑(chartAt H x) x))) v = (v, 0)<GOAL>fderivWithin 𝕜 (fun x_1 => (↑I (↑(ChartedSpace.chartAt x) (↑(ChartedSpace.chartAt x).symm (↑I.symm x_1))), 0)) (range ↑I ∩ ↑I.symm ⁻¹' (chartAt H x).target) (↑I (↑(chartAt H x) x)) = fderivWithin 𝕜 (fun x' => (x', 0)) (range ↑I ∩ ↑I.symm ⁻¹' (chartAt H x).target) (↑I (↑(chartAt H x) x))
<VAR>𝕜 : Type u_1<VAR>inst✝²⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝²³ : NormedAddCommGroup E<VAR>inst✝²² : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝²¹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝²⁰ : TopologicalSpace M<VAR>inst✝¹⁹ : ChartedSpace H M<VAR>Is : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁸ : NormedAddCommGroup E'<VAR>inst✝¹⁷ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁶ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝¹⁵ : TopologicalSpace M'<VAR>inst✝¹⁴ : ChartedSpace H' M'<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N✝ : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N✝<VAR>inst✝⁹ : ChartedSpace G N✝<VAR>Js : SmoothManifoldWithCorners J N✝<VAR>F' : Type u_11<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝⁶ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝⁵ : TopologicalSpace N'<VAR>inst✝⁴ : ChartedSpace G' N'<VAR>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>x : M<VAR>v : TangentSpace I x<VAR>N : ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (↑I (↑(chartAt H x) x))<VAR>A : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := 0 }) x<VAR>B : (fderivWithin 𝕜 (fun x' => (x', 0)) (range ↑I ∩ ↑I.symm ⁻¹' (chartAt H x).target) (↑I (↑(chartAt H x) x))) v = (v, 0)<VAR>y : E<VAR>hy : y ∈ range ↑I ∩ ↑I.symm ⁻¹' (chartAt H x).target<GOAL>(↑I (↑(ChartedSpace.chartAt x) (↑(ChartedSpace.chartAt x).symm (↑I.symm y))), 0) = (y, 0)
<VAR>𝕜 : Type u_1<VAR>inst✝²⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝²³ : NormedAddCommGroup E<VAR>inst✝²² : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝²¹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝²⁰ : TopologicalSpace M<VAR>inst✝¹⁹ : ChartedSpace H M<VAR>Is : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁸ : NormedAddCommGroup E'<VAR>inst✝¹⁷ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁶ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝¹⁵ : TopologicalSpace M'<VAR>inst✝¹⁴ : ChartedSpace H' M'<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N✝ : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N✝<VAR>inst✝⁹ : ChartedSpace G N✝<VAR>Js : SmoothManifoldWithCorners J N✝<VAR>F' : Type u_11<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝⁶ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝⁵ : TopologicalSpace N'<VAR>inst✝⁴ : ChartedSpace G' N'<VAR>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>x : M<VAR>v : TangentSpace I x<VAR>N : ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (↑I (↑(chartAt H x) x))<VAR>A : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := 0 }) x<VAR>B : (fderivWithin 𝕜 (fun x' => (x', 0)) (range ↑I ∩ ↑I.symm ⁻¹' (chartAt H x).target) (↑I (↑(chartAt H x) x))) v = (v, 0)<GOAL>(↑I (↑(ChartedSpace.chartAt x) (↑(ChartedSpace.chartAt x).symm (↑I.symm (↑I (↑(chartAt H x) x))))), 0) = (↑I (↑(chartAt H x) x), 0)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<GOAL>(cocompact X).coprod (cocompact Y) = cocompact (X × Y)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<GOAL>(cocompact X).coprod (cocompact Y) ≤ cocompact (X × Y)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<GOAL>cocompact (X × Y) ≤ (cocompact X).coprod (cocompact Y)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e : I → R<VAR>he : OrthogonalIdempotents e<GOAL>OrthogonalIdempotents (⇑f ∘ e)
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<GOAL>cosZeta (↑x) (2 * ↑k) = (-1) ^ (k + 1) / (2 * ↑k) / (2 * ↑k).Gammaℂ * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<GOAL>(-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / 2 / ↑(2 * k)! * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k))) = (-1) ^ (k + 1) / (2 * ↑k) / (2 * ↑k).Gammaℂ * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<GOAL>(-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / 2 / ↑(2 * k)! = (-1) ^ (k + 1) / (2 * ↑k) / (2 * ↑k).Gammaℂ
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<VAR>this : ↑(2 * k)! = 2 * ↑k * Complex.Gamma (2 * ↑k)<GOAL>(-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / 2 / ↑(2 * k)! = (-1) ^ (k + 1) / (2 * ↑k) / (2 * ↑k).Gammaℂ
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<VAR>this : ↑(2 * k)! = 2 * ↑k * Complex.Gamma (2 * ↑k)<GOAL>(-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / (2 * 2 * ↑k * Complex.Gamma (2 * ↑k)) = (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * ↑k) / (2 * 2 * ↑k * Complex.Gamma (2 * ↑k))
<VAR>x y : ℝ<GOAL>Real.toEReal ⁻¹' Ico ↑x ↑y = Ico x y
<VAR>x y : ℝ<GOAL>Real.toEReal ⁻¹' (Ici ↑x ∩ Iio ↑y) = Ici x ∩ Iio y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝¹¹ : MeasurableSpace X<VAR>inst✝¹⁰ : TopologicalSpace X<VAR>inst✝⁹ : MeasurableSpace Y<VAR>inst✝⁸ : TopologicalSpace Y<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>f✝ g✝ : X → E<VAR>μ : Measure X<VAR>s✝ : Set X<VAR>inst✝⁵ : OpensMeasurableSpace X<VAR>A K : Set X<VAR>inst✝⁴ : LocallyCompactSpace X<VAR>inst✝³ : T2Space X<VAR>𝕜 : Type u_6<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SecondCountableTopologyEither X E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : X → 𝕜<VAR>g : X → E<VAR>s : Set X<VAR>hs : IsOpen s<VAR>hf : LocallyIntegrableOn f s μ<VAR>hg : ContinuousOn g s<GOAL>LocallyIntegrableOn (fun x => f x • g x) s μ