ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>x : α<VAR>z : ℤ<VAR>hx : ↑z ≤ x<GOAL>fract x ≤ |x - ↑z|
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>x : α<VAR>z : ℤ<VAR>hx : x < ↑z<GOAL>1 - fract x ≤ |x - ↑z|
<VAR>G : Type u_1<VAR>inst✝³ : MeasurableSpace G<VAR>μ : Measure G<VAR>g✝ : G<VAR>inst✝² : Group G<VAR>inst✝¹ : MeasurableMul G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>f : G → ℝ≥0∞<VAR>g : G<GOAL>∫⁻ (x : G), f (g * x) ∂μ = ∫⁻ (x : G), f x ∂μ
<VAR>G : Type u_1<VAR>inst✝³ : MeasurableSpace G<VAR>μ : Measure G<VAR>g✝ : G<VAR>inst✝² : Group G<VAR>inst✝¹ : MeasurableMul G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>f : G → ℝ≥0∞<VAR>g : G<GOAL>μ = map (⇑(MeasurableEquiv.mulLeft g)) μ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<VAR>h : ∀ (v : E), ⟪v, x⟫_𝕜 = ⟪v, y⟫_𝕜<GOAL>x = y
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a : ι → ℝ<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>volume (Metric.closedBall a r) = ofReal ((2 * r) ^ Fintype.card ι)
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a : ι → ℝ<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>ofReal (2 * r) ^ Finset.univ.card = ofReal ((2 * r) ^ Fintype.card ι)
<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>inst✝³¹ : 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>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<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>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<GOAL>ContMDiffWithinAt I I' n f s x ↔ ∀ (m : ℕ), ↑m ≤ n → ContMDiffWithinAt I I' (↑m) f s 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>inst✝³¹ : 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>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<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>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>h : ∀ (m : ℕ), ↑m ≤ n → ContMDiffWithinAt I I' (↑m) f s x<GOAL>ContMDiffWithinAt I I' n f s x
<VAR>Γ : Type u_1<VAR>inst✝³ : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝² : Inhabited Λ<VAR>σ : Type u_3<VAR>inst✝¹ : Inhabited σ<VAR>n : ℕ<VAR>enc : Γ → Vector Bool n<VAR>dec : Vector Bool n → Γ<VAR>enc0 : enc default = Vector.replicate n false<VAR>M : Λ → Stmt₁<VAR>encdec : ∀ (a : Γ), dec (enc a) = a<VAR>inst✝ : Fintype Γ<VAR>S : Finset Λ<VAR>ss : Supports M S<VAR>q : Λ'<VAR>h : q ∈ trSupp M S<GOAL>SupportsStmt (trSupp M S) (tr enc dec M q)
<VAR>Γ : Type u_1<VAR>inst✝³ : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝² : Inhabited Λ<VAR>σ : Type u_3<VAR>inst✝¹ : Inhabited σ<VAR>n : ℕ<VAR>enc : Γ → Vector Bool n<VAR>dec : Vector Bool n → Γ<VAR>enc0 : enc default = Vector.replicate n false<VAR>M : Λ → Stmt₁<VAR>encdec : ∀ (a : Γ), dec (enc a) = a<VAR>inst✝ : Fintype Γ<VAR>S : Finset Λ<VAR>ss : Supports M S<VAR>q : Λ'<VAR>h : q ∈ trSupp M S<GOAL>∀ (q : Stmt₁), SupportsStmt S q → (∀ q' ∈ writes q, q' ∈ trSupp M S) → SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : IsCyclotomicExtension {n} A B<VAR>inst✝² : Field L<VAR>ζ : L<VAR>hζ✝ : IsPrimitiveRoot ζ ↑n<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra K L<VAR>k : ℕ<VAR>hζ : IsPrimitiveRoot ζ (2 ^ k)<VAR>hk : 2 ≤ k<VAR>H : IsCyclotomicExtension {2 ^ k} K L<VAR>hirr : Irreducible (cyclotomic (2 ^ k) K)<GOAL>(Algebra.norm K) (ζ - 1) = 2
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : IsCyclotomicExtension {n} A B<VAR>inst✝² : Field L<VAR>ζ : L<VAR>hζ✝ : IsPrimitiveRoot ζ ↑n<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra K L<VAR>k : ℕ<VAR>hζ : IsPrimitiveRoot ζ (2 ^ k)<VAR>hk : 2 ≤ k<VAR>H : IsCyclotomicExtension {2 ^ k} K L<VAR>hirr : Irreducible (cyclotomic (2 ^ k) K)<VAR>this : 2 < 2 ^ k<GOAL>(Algebra.norm K) (ζ - 1) = 2
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : IsCyclotomicExtension {n} A B<VAR>inst✝² : Field L<VAR>ζ : L<VAR>hζ✝ : IsPrimitiveRoot ζ ↑n<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra K L<VAR>k : ℕ<VAR>hk : 2 ≤ k<VAR>H : IsCyclotomicExtension {2 ^ k} K L<VAR>this : 2 < 2 ^ k<VAR>hirr : Irreducible (cyclotomic (↑(2 ^ k)) K)<VAR>hζ : IsPrimitiveRoot ζ ↑(2 ^ k)<GOAL>(Algebra.norm K) (ζ - 1) = 2
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : IsCyclotomicExtension {n} A B<VAR>inst✝² : Field L<VAR>ζ : L<VAR>hζ✝ : IsPrimitiveRoot ζ ↑n<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra K L<VAR>k : ℕ<VAR>hk : 2 ≤ k<VAR>H : IsCyclotomicExtension {2 ^ k} K L<VAR>this : 2 < 2 ^ k<VAR>hirr : Irreducible (cyclotomic (↑(2 ^ k)) K)<VAR>hζ : IsPrimitiveRoot ζ ↑(2 ^ k)<VAR>k₁ : ℕ<VAR>hk₁ : k = k₁.succ<GOAL>(Algebra.norm K) (ζ - 1) = 2
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : SimplicialCategory C<VAR>K L : C<GOAL>sHomWhiskerLeft K (𝟙 L) = 𝟙 (sHom K L)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f g : ↥(lp (fun i => ℝ) ⊤)<VAR>n : ℕ<VAR>C : ℝ<VAR>inst✝ : MetricSpace α<VAR>x : ℕ → α<VAR>a✝ b✝ a b : α<GOAL>dist (embeddingOfSubset x a) (embeddingOfSubset x b) ≤ dist a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f g : ↥(lp (fun i => ℝ) ⊤)<VAR>n✝ : ℕ<VAR>C : ℝ<VAR>inst✝ : MetricSpace α<VAR>x : ℕ → α<VAR>a✝ b✝ a b : α<VAR>n : ℕ<GOAL>‖↑(embeddingOfSubset x a - embeddingOfSubset x b) n‖ ≤ dist a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f g : ↥(lp (fun i => ℝ) ⊤)<VAR>n✝ : ℕ<VAR>C : ℝ<VAR>inst✝ : MetricSpace α<VAR>x : ℕ → α<VAR>a✝ b✝ a b : α<VAR>n : ℕ<GOAL>‖dist a (x n) - dist (x 0) (x n) - (dist b (x n) - dist (x 0) (x n))‖ ≤ dist a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f g : ↥(lp (fun i => ℝ) ⊤)<VAR>n✝ : ℕ<VAR>C : ℝ<VAR>inst✝ : MetricSpace α<VAR>x : ℕ → α<VAR>a✝ b✝ a b : α<VAR>n : ℕ<GOAL>dist a (x n) - dist (x 0) (x n) - (dist b (x n) - dist (x 0) (x n)) = dist a (x n) - dist b (x n)
<VAR>α✝ : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>s t : Set α✝<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>inst✝⁴ : Finite ι<VAR>inst✝³ : Preorder ι'<VAR>inst✝² : Nonempty ι'<VAR>inst✝¹ : IsDirected ι' fun x x_1 => x ≤ x_1<VAR>inst✝ : Order.Frame α<VAR>f : ι → ι' → α<VAR>hf : ∀ (i : ι), Monotone (f i)<GOAL>⨆ j, ⨅ i, f i j = ⨅ i, ⨆ j, f i j
<VAR>R : Type u<VAR>inst✝¹ : Mul R<VAR>inst✝ : StarMul R<VAR>x y : R<GOAL>star (x * star y) = y * star x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁶ : PseudoEMetricSpace α<VAR>inst✝⁵ : PseudoEMetricSpace β<VAR>inst✝⁴ : PseudoEMetricSpace γ<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : DilationClass F α β<VAR>inst✝¹ : FunLike G β γ<VAR>inst✝ : DilationClass G β γ<VAR>f✝ : F<VAR>g✝ : G<VAR>x y z : α<VAR>s : Set α<VAR>f g : α →ᵈ α<VAR>h : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ⊤<GOAL>ratio (f * g) = ratio f * ratio g
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>L : E →L[ℝ] F →L[ℝ] G<VAR>u : ℝ → E<VAR>v : ℝ → F<VAR>u' : ℝ → E<VAR>v' : ℝ → F<VAR>m n : G<VAR>inst✝ : CompleteSpace G<VAR>hu : ∀ (x : ℝ), HasDerivAt u (u' x) x<VAR>hv : ∀ (x : ℝ), HasDerivAt v (v' x) x<VAR>huv' : Integrable (fun x => (L (u x)) (v' x)) volume<VAR>hu'v : Integrable (fun x => (L (u' x)) (v x)) volume<VAR>h_bot : Tendsto (fun x => (L (u x)) (v x)) atBot (𝓝 m)<VAR>h_top : Tendsto (fun x => (L (u x)) (v x)) atTop (𝓝 n)<GOAL>∫ (x : ℝ), (L (u x)) (v' x) = n - m - ∫ (x : ℝ), (L (u' x)) (v x)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>L : E →L[ℝ] F →L[ℝ] G<VAR>u : ℝ → E<VAR>v : ℝ → F<VAR>u' : ℝ → E<VAR>v' : ℝ → F<VAR>m n : G<VAR>inst✝ : CompleteSpace G<VAR>hu : ∀ (x : ℝ), HasDerivAt u (u' x) x<VAR>hv : ∀ (x : ℝ), HasDerivAt v (v' x) x<VAR>huv' : Integrable (fun x => (L (u x)) (v' x)) volume<VAR>hu'v : Integrable (fun x => (L (u' x)) (v x)) volume<VAR>h_bot : Tendsto (fun x => (L (u x)) (v x)) atBot (𝓝 m)<VAR>h_top : Tendsto (fun x => (L (u x)) (v x)) atTop (𝓝 n)<GOAL>∫ (a : ℝ), (L (u a)) (v' a) + (L (u' a)) (v a) = n - m
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁ p₂ p1 p2 p3 : P<VAR>h : ∠ p1 p2 p3 = 0<GOAL>dist p1 p3 = |dist p1 p2 - dist p3 p2|
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁ p₂ p1 p2 p3 : P<VAR>h : ∠ p1 p2 p3 = 0<GOAL>‖p1 -ᵥ ?p₃ - (p3 -ᵥ ?p₃)‖ = |‖p1 -ᵥ p2‖ - ‖p3 -ᵥ p2‖|
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁ p₂ p1 p2 p3 : P<VAR>h : ∠ p1 p2 p3 = 0<GOAL>P
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>α : E<VAR>p : F[X]<GOAL>IsSplittingField F E p ↔ Splits (algebraMap F E) p ∧ adjoin F (p.rootSet E) = ⊤
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>α : E<VAR>p : F[X]<GOAL>IsSplittingField F E p ↔ Splits (algebraMap F E) p ∧ Algebra.adjoin F (p.rootSet E) = ⊤.toSubalgebra
<VAR>x y : ℝ≥0∞<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>z : ℝ<GOAL>(x * y) ^ z = x ^ z * y ^ z
<VAR>F : Type u → Type u<VAR>inst✝⁵ : Applicative F<VAR>inst✝⁴ : CommApplicative F<VAR>α' β' : Type u<VAR>f✝ : α' → F β'<VAR>G H : Type u_1 → Type u_1<VAR>inst✝³ : Applicative G<VAR>inst✝² : Applicative H<VAR>inst✝¹ : CommApplicative G<VAR>inst✝ : CommApplicative H<VAR>eta : ApplicativeTransformation G H<VAR>α β : Type u_1<VAR>f : α → G β<VAR>x : Multiset α<GOAL>(fun {α} => eta.app α) (traverse f x) = traverse ((fun {α} => eta.app α) ∘ f) x
<VAR>F : Type u → Type u<VAR>inst✝⁵ : Applicative F<VAR>inst✝⁴ : CommApplicative F<VAR>α' β' : Type u<VAR>f✝ : α' → F β'<VAR>G H : Type u_1 → Type u_1<VAR>inst✝³ : Applicative G<VAR>inst✝² : Applicative H<VAR>inst✝¹ : CommApplicative G<VAR>inst✝ : CommApplicative H<VAR>eta : ApplicativeTransformation G H<VAR>α β : Type u_1<VAR>f : α → G β<VAR>x : Multiset α<GOAL>∀ (a : List α), (fun {α} => eta.app α) (traverse f ⟦a⟧) = traverse ((fun {α} => eta.app α) ∘ f) ⟦a⟧
<VAR>F : Type u → Type u<VAR>inst✝⁵ : Applicative F<VAR>inst✝⁴ : CommApplicative F<VAR>α' β' : Type u<VAR>f✝ : α' → F β'<VAR>G H : Type u_1 → Type u_1<VAR>inst✝³ : Applicative G<VAR>inst✝² : Applicative H<VAR>inst✝¹ : CommApplicative G<VAR>inst✝ : CommApplicative H<VAR>eta : ApplicativeTransformation G H<VAR>α β : Type u_1<VAR>f : α → G β<VAR>x : Multiset α<VAR>a✝ : List α<GOAL>(fun {α} => eta.app α) (traverse f ⟦a✝⟧) = traverse ((fun {α} => eta.app α) ∘ f) ⟦a✝⟧
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>W X✝ Y✝ Z✝ X Y Z : C<VAR>f₁ f₂ : X ⟶ Z<VAR>g₁ g₂ : Y ⟶ Z<VAR>h₁ : f₁ = f₂<VAR>h₂ : g₁ = g₂<VAR>inst✝¹ : HasPullback f₁ g₁<VAR>inst✝ : HasPullback f₂ g₂<GOAL>(congrHom h₁ h₂).inv = map f₂ g₂ f₁ g₁ (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : LinearOrderedRing α<GOAL>¬Tendsto (fun x => x ^ 0) atTop atBot
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : Ideal R<GOAL>Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I) ≠ 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : Ideal R<GOAL>(if h : (mulSupport fun v => v.maxPowDividing I).Finite then ∏ i ∈ h.toFinset, i.maxPowDividing I else 1) ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>b : Set (Set β)<VAR>hbc : b.Countable<VAR>this : MeasurableSpace α := generateFrom (preimage f '' b)<GOAL>CountablyGenerated α
<VAR>n✝ n : ℕ<GOAL>n = 1 ↔ ∀ (p : ℕ), Prime p → ¬p ∣ n
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A<VAR>h₁₂ : a₁ + a₂ = a₁₂<VAR>h₂₃ : a₂ + a₃ = a₂₃<VAR>h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃<VAR>X : C<GOAL>(shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ ⋯).hom.app X ≫ (shiftFunctor C a₃).map ((shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).hom.app X) = (shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ⋯).hom.app X ≫ (shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).hom.app ((shiftFunctor C a₁).obj X)
<VAR>q : ℚ<VAR>x y : ℝ<VAR>h : Irrational x<GOAL>Irrational (↑(-q) + (↑q + x))
<VAR>n : ℕ<GOAL>bernoulli n = ∑ i ∈ range (n + 1), (monomial i) (_root_.bernoulli (n - i) * ↑(n.choose i))
<VAR>n : ℕ<GOAL>∑ i ∈ range (n + 1), (monomial (n - i)) (_root_.bernoulli i * ↑(n.choose i)) = ∑ j ∈ range (n + 1), (monomial (n - j)) (_root_.bernoulli (n - (n - j)) * ↑(n.choose (n - j)))
<VAR>n : ℕ<GOAL>∀ x ∈ range (n + 1), (monomial (n - x)) (_root_.bernoulli x * ↑(n.choose x)) = (monomial (n - x)) (_root_.bernoulli (n - (n - x)) * ↑(n.choose (n - x)))
<VAR>n x : ℕ<VAR>hx : x ∈ range (n + 1)<GOAL>(monomial (n - x)) (_root_.bernoulli x * ↑(n.choose x)) = (monomial (n - x)) (_root_.bernoulli (n - (n - x)) * ↑(n.choose (n - x)))
<VAR>n x : ℕ<VAR>hx : x ≤ n<GOAL>(monomial (n - x)) (_root_.bernoulli x * ↑(n.choose x)) = (monomial (n - x)) (_root_.bernoulli (n - (n - x)) * ↑(n.choose (n - x)))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>∫⁻ (a : α) in t, ↑‖↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a‖₊ ∂μ ≤ μ (s ∩ t)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>∫⁻ (x : α) in t, ↑‖↑↑(indicatorConstLp 2 hs hμs 1) x‖₊ ∂μ = μ (s ∩ t)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<VAR>h_eq : ∫⁻ (x : α) in t, ↑‖↑↑(indicatorConstLp 2 hs hμs 1) x‖₊ ∂μ = ∫⁻ (x : α) in t, s.indicator (fun x => 1) x ∂μ<GOAL>∫⁻ (x : α) in t, ↑‖↑↑(indicatorConstLp 2 hs hμs 1) x‖₊ ∂μ = μ (s ∩ t)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<VAR>h_eq : ∫⁻ (x : α) in t, ↑‖↑↑(indicatorConstLp 2 hs hμs 1) x‖₊ ∂μ = ∫⁻ (x : α) in t, s.indicator (fun x => 1) x ∂μ<GOAL>1 * (μ.restrict (s ∩ t)) Set.univ = μ (s ∩ t)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>h : JoinedIn F x y<GOAL>JoinedIn F y x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>h : JoinedIn F x y<VAR>hx : x ∈ F<VAR>hy : y ∈ F<GOAL>JoinedIn F y x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>hx✝ : x ∈ F<VAR>hy✝ : y ∈ F<VAR>h : Joined ⟨x, ⋯⟩ ⟨y, ⋯⟩<VAR>hx : x ∈ F<VAR>hy : y ∈ F<GOAL>Joined ⟨y, ⋯⟩ ⟨x, ⋯⟩
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>f g : C(X, ℝ)<VAR>x : X<GOAL>↑(((f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal) x) = ↑(((-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal) x)
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>f g : C(X, ℝ)<VAR>x : X<GOAL>max (f x * g x) 0 + (-(f x * max (g x) 0) + max (f x) 0 * max (g x) 0) + (-(max (f x) 0 * g x) + max (f x) 0 * max (g x) 0) = -(f x * g x) + max (f x * g x) 0 + max (f x) 0 * max (g x) 0 + (-(max (f x) 0 * g x) + f x * g x + (-(f x * max (g x) 0) + max (f x) 0 * max (g x) 0))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module A M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsScalarTower R A M<VAR>d✝ : Derivation R A M<VAR>a : A<VAR>d : Derivation R A M<VAR>f : R[X]<GOAL>(AEval.of R M a).symm ((d.compAEval a) f) = (aeval a) (derivative f) • d a
<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 ((-↑(chainBotCoeff α β) - 1) • α + ⇑β) = ⊥
<VAR>ι : Type u_1<VAR>inst✝¹ : Finite ι<VAR>f : (ι → ℝ) →ₗ[ℝ] ι → ℝ<VAR>hf : LinearMap.det f ≠ 0<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : μ.IsAddHaarMeasure<GOAL>map (⇑f) μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ
<VAR>ι : Type u_1<VAR>inst✝¹ : Finite ι<VAR>f : (ι → ℝ) →ₗ[ℝ] ι → ℝ<VAR>hf : LinearMap.det f ≠ 0<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>val✝ : Fintype ι<GOAL>map (⇑f) μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ
<VAR>ι : Type u_1<VAR>inst✝¹ : Finite ι<VAR>f : (ι → ℝ) →ₗ[ℝ] ι → ℝ<VAR>hf : LinearMap.det f ≠ 0<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>val✝ : Fintype ι<VAR>this : μ = μ ↑(piIcc01 ι) • addHaarMeasure (piIcc01 ι)<GOAL>map (⇑f) μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>n m : σ →₀ ℕ<VAR>φ : MvPowerSeries σ R<GOAL>MvPolynomial.coeff m (truncFun n φ) = if m < n then (coeff R m) φ else 0
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>t : ℝ<VAR>f : AddCircle T → ℝ≥0∞<GOAL>∫⁻ (a : ℝ) in Ioc t (t + T), f ↑a = ∫⁻ (b : AddCircle T), f b
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>t : ℝ<VAR>f : AddCircle T → ℝ≥0∞<VAR>m : MeasurableSet (Ioc t (t + T))<GOAL>∫⁻ (a : ℝ) in Ioc t (t + T), f ↑a = ∫⁻ (b : AddCircle T), f b