ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>L : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝⁷ : AddCommMonoid L<VAR>inst✝⁶ : TopologicalSpace L<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : TopologicalSpace N<VAR>v✝ v₁ v₂ : VectorMeasure α M<VAR>w w₁ w₂ : VectorMeasure α N<VAR>inst✝¹ : T2Space N<VAR>inst✝ : ContinuousAdd M<VAR>u : Set α<VAR>hmu : MeasurableSet u<VAR>hu₁ : ∀ t ⊆ u, ↑v₁ t = 0<VAR>hu₂ : ∀ t ⊆ uᶜ, ↑w t = 0<VAR>v : Set α<VAR>hmv : MeasurableSet v<VAR>hv₁ : ∀ t ⊆ v, ↑v₂ t = 0<VAR>hv₂ : ∀ t ⊆ vᶜ, ↑w t = 0<VAR>t : Set α<VAR>ht : t ⊆ u ∩ v<VAR>x✝ : MeasurableSet t<GOAL>↑(v₁ + v₂) t = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>L : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝⁷ : AddCommMonoid L<VAR>inst✝⁶ : TopologicalSpace L<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : TopologicalSpace N<VAR>v✝ v₁ v₂ : VectorMeasure α M<VAR>w w₁ w₂ : VectorMeasure α N<VAR>inst✝¹ : T2Space N<VAR>inst✝ : ContinuousAdd M<VAR>u : Set α<VAR>hmu : MeasurableSet u<VAR>hu₁ : ∀ t ⊆ u, ↑v₁ t = 0<VAR>hu₂ : ∀ t ⊆ uᶜ, ↑w t = 0<VAR>v : Set α<VAR>hmv : MeasurableSet v<VAR>hv₁ : ∀ t ⊆ v, ↑v₂ t = 0<VAR>hv₂ : ∀ t ⊆ vᶜ, ↑w t = 0<VAR>t : Set α<VAR>ht : t ⊆ (u ∩ v)ᶜ<VAR>hmt : MeasurableSet t<GOAL>↑w t = 0
<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 ζ ↑(p ^ (k + 1))<VAR>hpri : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L<VAR>hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)<VAR>s : ℕ<VAR>hs : s ≤ k<VAR>hodd : p ≠ 2<GOAL>(Algebra.norm K) (ζ ^ ↑p ^ s - 1) = ↑↑p ^ ↑p ^ s
<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 ζ ↑(p ^ (k + 1))<VAR>hpri : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L<VAR>hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)<VAR>s : ℕ<VAR>hs : s ≤ k<VAR>hodd : p ≠ 2<VAR>h : p ^ (k - s + 1) = 2<GOAL>False
<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 ζ ↑(p ^ (k + 1))<VAR>hpri : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L<VAR>hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)<VAR>s : ℕ<VAR>hs : s ≤ k<VAR>hodd : p ≠ 2<VAR>h : p ^ (k - s + 1) = 2<VAR>coe_two : ↑2 = 2<GOAL>False
<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 ζ ↑(p ^ (k + 1))<VAR>hpri : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L<VAR>hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)<VAR>s : ℕ<VAR>hs : s ≤ k<VAR>hodd : p ≠ 2<VAR>h : ↑p ^ (k - s + 1) = 2 ^ 1<VAR>coe_two : ↑2 = 2<GOAL>False
<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 ζ ↑(p ^ (k + 1))<VAR>hpri : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L<VAR>hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)<VAR>s : ℕ<VAR>hs : s ≤ k<VAR>hodd : p ≠ 2<VAR>coe_two : ↑2 = 2<VAR>h : ↑p = 2<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : PartialOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>{ ofColex := s.erase a } ≤ { ofColex := s.erase b } ↔ b ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : PartialOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>ha hb : a ∈ s<GOAL>{ ofColex := s.erase a } ≤ { ofColex := s.erase a } ↔ a ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : PartialOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>hab : a ≠ b<GOAL>{ ofColex := s.erase a } ≤ { ofColex := s.erase b } ↔ b ≤ a
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝⁹ : DecidableEq ι<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra A B<VAR>inst✝⁵ : CommRing C<VAR>inst✝⁴ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝³ : Fintype ι'<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : DecidableEq ι'<VAR>inst✝ : Fintype ι<VAR>b b' : Basis ι ℤ A<GOAL>discr ℤ ⇑b = discr ℤ ⇑b'
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝⁹ : DecidableEq ι<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra A B<VAR>inst✝⁵ : CommRing C<VAR>inst✝⁴ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝³ : Fintype ι'<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : DecidableEq ι'<VAR>inst✝ : Fintype ι<VAR>b b' : Basis ι ℤ A<GOAL>⇑b = ⇑b' ᵥ* (b'.toMatrix ⇑b).map ⇑(algebraMap ℤ A)
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝⁹ : DecidableEq ι<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra A B<VAR>inst✝⁵ : CommRing C<VAR>inst✝⁴ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝³ : Fintype ι'<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : DecidableEq ι'<VAR>inst✝ : Fintype ι<VAR>b b' : Basis ι ℤ A<GOAL>discr ℤ ⇑b' = (b'.toMatrix ⇑b).det ^ 2 * discr ℤ ⇑b'
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>f : α ≃. β<VAR>g : β ≃. γ<VAR>a : α<GOAL>(f.trans g) a = none ↔ ∀ (b : β) (c : γ), b ∉ f a ∨ c ∉ g b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>f : α ≃. β<VAR>g : β ≃. γ<VAR>a : α<GOAL>(∀ (a_1 : γ), ¬∃ b ∈ f a, a_1 ∈ g b) ↔ ∀ (b : β) (c : γ), b ∈ f a → c ∉ g b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>f : α ≃. β<VAR>g : β ≃. γ<VAR>a : α<GOAL>(∀ (a_1 : γ), ∀ b ∈ f a, a_1 ∉ g b) ↔ ∀ (b : β) (c : γ), b ∈ f a → c ∉ g b
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<GOAL>HasFTaylorSeriesUpToOn 0 f p s ↔ ContinuousOn f s ∧ ∀ x ∈ s, (p x 0).uncurry0 = f x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m✝ n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>H : ContinuousOn f s ∧ ∀ x ∈ s, (p x 0).uncurry0 = f x<VAR>m : ℕ<VAR>hm : ↑m ≤ 0<GOAL>ContinuousOn (fun x => p x m) s
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>H : ContinuousOn f s ∧ ∀ x ∈ s, (p x 0).uncurry0 = f x<VAR>hm : ↑0 ≤ 0<GOAL>ContinuousOn (fun x => p x 0) s
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>H : ContinuousOn f s ∧ ∀ x ∈ s, (p x 0).uncurry0 = f x<VAR>hm : ↑0 ≤ 0<VAR>this : EqOn (fun x => p x 0) (⇑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f) s<GOAL>ContinuousOn (fun x => p x 0) s
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>H : ContinuousOn f s ∧ ∀ x ∈ s, (p x 0).uncurry0 = f x<VAR>hm : ↑0 ≤ 0<VAR>this : EqOn (fun x => p x 0) (⇑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f) s<GOAL>ContinuousOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>T : Set (Set β)<VAR>hT : T.Nonempty<VAR>s : Set α<GOAL>s ×ˢ ⋂₀ T = ⋂ t ∈ T, s ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>T : Set (Set β)<VAR>hT : T.Nonempty<VAR>s : Set α<GOAL>⋂ r ∈ {s} ×ˢ T, r.1 ×ˢ r.2 = ⋂ t ∈ T, s ×ˢ t
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<GOAL>‖setToL1 hT‖ ≤ ↑1 * ‖setToL1SCLM α E μ hT‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>x : ↥(simpleFunc E 1 μ)<GOAL>‖x‖ = ↑1 * ‖(coeToLp α E ℝ) x‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>x : ↥(simpleFunc E 1 μ)<GOAL>‖x‖ = ‖(coeToLp α E ℝ) x‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<GOAL>↑1 * ‖setToL1SCLM α E μ hT‖ = ‖setToL1SCLM α E μ hT‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<VAR>s : Set α<VAR>t : Set β<VAR>x : α<VAR>y : β<GOAL>e.IsImage s t ↔ e.source ∩ ↑e ⁻¹' t = e.source ∩ s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type w<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<GOAL>(∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬M' < I) ↔ IsNoetherian R M
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<GOAL>Iio b \ Iio a = Ico a b
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>N : Type u_4<VAR>N' : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : Module R M<VAR>inst✝⁹ : TopologicalSpace M<VAR>inst✝⁸ : AddCommMonoid M'<VAR>inst✝⁷ : Module R M'<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : TopologicalSpace N<VAR>inst✝² : AddCommMonoid N'<VAR>inst✝¹ : Module R N'<VAR>inst✝ : TopologicalSpace N'<VAR>n : ℕ<VAR>f✝ g✝ f g : M [⋀^ι]→L[R] N<VAR>h : f.toAlternatingMap = g.toAlternatingMap<GOAL>⇑f = ⇑g
<VAR>z : ℂ<VAR>x : ℝ<GOAL>z / ↑x = { re := z.re / x, im := z.im / x }
<VAR>a b k✝ m n✝ p n k : ℕ<GOAL>(n ^ (k + 1)).primeFactors = n.primeFactors
<VAR>a b k✝ m n p k : ℕ<GOAL>(0 ^ (k + 1)).primeFactors = primeFactors 0
<VAR>a b k✝ m n✝ p n k : ℕ<VAR>hn : n ≠ 0<GOAL>(n ^ (k + 1)).primeFactors = n.primeFactors
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a✝ b✝ c d a b : α<GOAL>a ∆ b = ⊥ ↔ a = b
<VAR>α : Type u_1<VAR>a b c d : ℝ≥0∞<VAR>r✝ p q r : ℝ≥0<GOAL>∃ n, ↑r < ↑n
<VAR>α : Type u_1<VAR>a b c d : ℝ≥0∞<VAR>r✝ p q r : ℝ≥0<VAR>n : ℕ<VAR>hn : r < ↑n<GOAL>∃ n, ↑r < ↑n
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>𝕜 : Type u_5<VAR>inst✝⁴ : NormedDivisionRing 𝕜<VAR>inst✝³ : MulActionWithZero 𝕜 E<VAR>inst✝² : Module 𝕜 F<VAR>inst✝¹ : BoundedSMul 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜 F<VAR>f : α → F<VAR>c : 𝕜<VAR>hq_pos : 0 < q<GOAL>eLpNorm' (c • f) q μ = ‖c‖₊ • eLpNorm' f q μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>𝕜 : Type u_5<VAR>inst✝⁴ : NormedDivisionRing 𝕜<VAR>inst✝³ : MulActionWithZero 𝕜 E<VAR>inst✝² : Module 𝕜 F<VAR>inst✝¹ : BoundedSMul 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜 F<VAR>f : α → F<VAR>hq_pos : 0 < q<GOAL>eLpNorm' (0 • f) q μ = ‖0‖₊ • eLpNorm' f q μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>𝕜 : Type u_5<VAR>inst✝⁴ : NormedDivisionRing 𝕜<VAR>inst✝³ : MulActionWithZero 𝕜 E<VAR>inst✝² : Module 𝕜 F<VAR>inst✝¹ : BoundedSMul 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜 F<VAR>f : α → F<VAR>c : 𝕜<VAR>hq_pos : 0 < q<VAR>hc : c ≠ 0<GOAL>eLpNorm' (c • f) q μ = ‖c‖₊ • eLpNorm' f q μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>𝕜 : Type u_5<VAR>inst✝⁴ : NormedDivisionRing 𝕜<VAR>inst✝³ : MulActionWithZero 𝕜 E<VAR>inst✝² : Module 𝕜 F<VAR>inst✝¹ : BoundedSMul 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜 F<VAR>f : α → F<VAR>c : 𝕜<VAR>hq_pos : 0 < q<VAR>hc : c ≠ 0<GOAL>‖c‖₊ • eLpNorm' f q μ ≤ eLpNorm' (c • f) q μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>𝕜 : Type u_5<VAR>inst✝⁴ : NormedDivisionRing 𝕜<VAR>inst✝³ : MulActionWithZero 𝕜 E<VAR>inst✝² : Module 𝕜 F<VAR>inst✝¹ : BoundedSMul 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜 F<VAR>f : α → F<VAR>c : 𝕜<VAR>hq_pos : 0 < q<VAR>hc : c ≠ 0<VAR>this : eLpNorm' (c⁻¹ • c • f) q μ ≤ ‖c⁻¹‖₊ • eLpNorm' (c • f) q μ<GOAL>‖c‖₊ • eLpNorm' f q μ ≤ eLpNorm' (c • f) q μ
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>q : ℕ<VAR>inst✝ : ExpChar F q<GOAL>IsPurelyInseparable F E ↔ ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>q : ℕ<VAR>inst✝ : ExpChar F q<GOAL>(∀ (x : E), IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)) ↔ ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>q : ℕ<VAR>inst✝ : ExpChar F q<VAR>h : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range<VAR>x : E<GOAL>IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>q : ℕ<VAR>inst✝ : ExpChar F q<VAR>h : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range<VAR>x : E<VAR>hdeg : (minpoly F x).natSepDegree = 1<GOAL>IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>q : ℕ<VAR>inst✝ : ExpChar F q<VAR>h : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range<VAR>x : E<VAR>hdeg : (minpoly F x).natSepDegree = 1<VAR>halg : IsIntegral F x<GOAL>IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>q : ℕ<VAR>inst✝ : ExpChar F q<VAR>h : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range<VAR>x : E<VAR>hdeg : (minpoly F x).natSepDegree = 1<VAR>halg : IsIntegral F x<VAR>hsep : IsSeparable F x<GOAL>x ∈ (algebraMap F E).range
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>q : ℕ<VAR>inst✝ : ExpChar F q<VAR>h : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range<VAR>x : E<VAR>hdeg : F⟮x⟯ = ⊥<VAR>halg : IsIntegral F x<VAR>hsep : IsSeparable F x<GOAL>x ∈ (algebraMap F E).range
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>x : 𝕎 R<VAR>hx : x ≠ 0<GOAL>∃ n x', x'.coeff 0 ≠ 0 ∧ x = (⇑verschiebung)^[n] x'
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>x : 𝕎 R<VAR>hx : x ≠ 0<VAR>hex : ∃ k, x.coeff k ≠ 0<GOAL>∃ n x', x'.coeff 0 ≠ 0 ∧ x = (⇑verschiebung)^[n] x'
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>x : 𝕎 R<VAR>hx : x ≠ 0<VAR>hex : ∃ k, x.coeff k ≠ 0<VAR>n : ℕ := Nat.find hex<GOAL>∃ n x', x'.coeff 0 ≠ 0 ∧ x = (⇑verschiebung)^[n] x'
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>x : 𝕎 R<VAR>hx : x ≠ 0<VAR>hex : ∃ k, x.coeff k ≠ 0<VAR>n : ℕ := Nat.find hex<GOAL>(x.shift n).coeff 0 ≠ 0 ∧ x = (⇑verschiebung)^[n] (x.shift n)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>x : 𝕎 R<VAR>hx : x ≠ 0<VAR>hex : ∃ k, x.coeff k ≠ 0<VAR>n : ℕ := Nat.find hex<VAR>i : ℕ<VAR>hi : i < n<GOAL>¬¬x.coeff i = 0
<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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ¬p₁ = p₂<GOAL>∡ (midpoint ℝ p₁ p₂) p₂ p₃ = ∡ p₁ p₂ p₃
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n : ℤ<GOAL>a / b = b⁻¹ ↔ a = 1
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>f✝ g✝ : Arrow C<VAR>inst✝³ : HasImage f✝.hom<VAR>inst✝² : HasImage g✝.hom<VAR>sq✝ : f✝ ⟶ g✝<VAR>f g : Arrow C<VAR>inst✝¹ : HasImage f.hom<VAR>inst✝ : HasImage g.hom<VAR>sq : f ⟶ g<VAR>map : image f.hom ⟶ image g.hom<VAR>map_ι : autoParam (map ≫ image.ι g.hom = image.ι f.hom ≫ sq.right) _auto✝<VAR>map' : image f.hom ⟶ image g.hom<VAR>map_ι' : map' ≫ image.ι g.hom = image.ι f.hom ≫ sq.right<VAR>this : map ≫ image.ι g.hom = map' ≫ image.ι g.hom<GOAL>map = map'
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S✝<VAR>inst✝ : Ring T<VAR>S : Set (Subring R)<VAR>Sne : S.Nonempty<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<VAR>x : R<GOAL>x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S✝<VAR>inst✝ : Ring T<VAR>S : Set (Subring R)<VAR>Sne : S.Nonempty<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<VAR>x : R<VAR>this : Nonempty ↑S<GOAL>x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : SheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>U : Opens ↑↑X.toPresheafedSpace<GOAL>(Opens.map f.base).op.obj (op ((opensFunctor f).obj U)) = op U
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e✝ : Sym2 V<VAR>inst✝² : DecidableEq V<VAR>inst✝¹ : Fintype ↑G.edgeSet<VAR>s : Finset (Sym2 V)<VAR>inst✝ : Fintype ↑(G.deleteEdges ↑s).edgeSet<VAR>e : Sym2 V<GOAL>e ∈ (G.deleteEdges ↑s).edgeFinset ↔ e ∈ G.edgeFinset \ s
<VAR>A : Type u_1<VAR>inst✝⁸ : TopologicalSpace A<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : Algebra ℂ A<VAR>inst✝⁴ : StarModule ℂ A<VAR>inst✝³ : ContinuousFunctionalCalculus ℂ IsStarNormal<VAR>inst✝² : ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>inst✝¹ : UniqueContinuousFunctionalCalculus ℝ A<VAR>inst✝ : UniqueContinuousFunctionalCalculus ℂ A<VAR>a : A<VAR>f : ℝ → ℝ<VAR>ha : autoParam (IsSelfAdjoint a) _auto✝<GOAL>cfc f a = cfc (fun x => ↑(f x.re)) a
<VAR>A : Type u_1<VAR>inst✝⁸ : TopologicalSpace A<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : Algebra ℂ A<VAR>inst✝⁴ : StarModule ℂ A<VAR>inst✝³ : ContinuousFunctionalCalculus ℂ IsStarNormal<VAR>inst✝² : ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>inst✝¹ : UniqueContinuousFunctionalCalculus ℝ A<VAR>inst✝ : UniqueContinuousFunctionalCalculus ℂ A<VAR>a : A<VAR>f : ℝ → ℝ<VAR>ha : autoParam (IsSelfAdjoint a) _auto✝<VAR>this : CompactSpace ↑(σ ℂ a)<GOAL>cfc f a = cfc (fun x => ↑(f x.re)) a