ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hw : w ∈ ball c R<VAR>hc : ContinuousOn f (closedBall c R)<VAR>hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x<VAR>hR : 0 < R<VAR>t : Set ℂ<VAR>ht : t ∈ 𝓝 w<VAR>g : ℝ → ℂ := fun x => w + ofReal x<VAR>this : Tendsto g (𝓝 0) (𝓝 w)<GOAL>(t ∩ (ball c R \ s)).Nonempty
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hw : w ∈ ball c R<VAR>hc : ContinuousOn f (closedBall c R)<VAR>hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x<VAR>hR : 0 < R<VAR>t : Set ℂ<VAR>ht : t ∈ 𝓝 w<VAR>g : ℝ → ℂ := fun x => w + ofReal x<VAR>this : Tendsto g (𝓝 0) (𝓝 w)<VAR>l u : ℝ<VAR>hlu₀ : 0 ∈ Ioo l u<VAR>hlu_sub : Ioo l u ⊆ g ⁻¹' (t ∩ ball c R)<GOAL>(t ∩ (ball c R \ s)).Nonempty
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hw : w ∈ ball c R<VAR>hc : ContinuousOn f (closedBall c R)<VAR>hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x<VAR>hR : 0 < R<VAR>t : Set ℂ<VAR>ht : t ∈ 𝓝 w<VAR>g : ℝ → ℂ := fun x => w + ofReal x<VAR>this : Tendsto g (𝓝 0) (𝓝 w)<VAR>l u : ℝ<VAR>hlu₀ : 0 ∈ Ioo l u<VAR>hlu_sub : Ioo l u ⊆ g ⁻¹' (t ∩ ball c R)<VAR>x : ℝ<VAR>hx : x ∈ Ioo l u \ g ⁻¹' s<GOAL>(t ∩ (ball c R \ s)).Nonempty
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝ : LT α<VAR>s t : Set α<GOAL>univ.IsWF ↔ WellFounded fun x x_1 => x < x_1
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<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>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>s : Set E<VAR>x : E<GOAL>AnalyticWithinAt 𝕜 f s x ↔ ContinuousWithinAt f s x ∧ ∃ g, f =ᶠ[𝓝[s] x] g ∧ AnalyticAt 𝕜 g x
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<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>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>s : Set E<VAR>x : E<GOAL>(∃ p, ContinuousWithinAt f s x ∧ ∃ g, f =ᶠ[𝓝[s] x] g ∧ HasFPowerSeriesAt g p x) ↔ ContinuousWithinAt f s x ∧ ∃ g, f =ᶠ[𝓝[s] x] g ∧ ∃ p, HasFPowerSeriesAt g p x
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x<VAR>hgg' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x<VAR>hg' : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0<VAR>hfa : Tendsto f (𝓝 a) (𝓝 0)<VAR>hga : Tendsto g (𝓝 a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝 a) l<GOAL>Tendsto (fun x => f x / g x) (𝓝[≠] a) l
<VAR>a b : Int<GOAL>↑(a * b) = ↑a * ↑b
<VAR>a b : Int<GOAL>↑(a * b) = normalize ((↑a).num * (↑b).num) ((↑a).den * (↑b).den) ⋯
<VAR>cs cs' : List Char<VAR>i p : Nat<VAR>hp : i + utf8Len cs = p<GOAL>utf8GetAux (cs ++ cs') { byteIdx := i } { byteIdx := p } = cs'.headD default
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝¹ : DivisionMonoid K<VAR>inst✝ : HasDistribNeg K<VAR>a✝ b✝ a b : K<GOAL>-a / -b = a / b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s t : Set α<VAR>a b : α<GOAL>IsGreatest univ a ↔ IsTop a
<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>ι : Type u_4<VAR>G : ι → Type u_5<VAR>inst✝² : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)<VAR>inst✝ : DecidableEq ι<VAR>f : (i : ι) → G i<VAR>s₁ s₂ : Finset ι<GOAL>‖∑ i ∈ s₁, (V i) (f i) - ∑ i ∈ s₂, (V i) (f i)‖ ^ 2 = ∑ i ∈ s₁ \ s₂, ‖f i‖ ^ 2 + ∑ i ∈ s₂ \ s₁, ‖f i‖ ^ 2
<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>ι : Type u_4<VAR>G : ι → Type u_5<VAR>inst✝² : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)<VAR>inst✝ : DecidableEq ι<VAR>f : (i : ι) → G i<VAR>s₁ s₂ : Finset ι<GOAL>‖∑ x ∈ s₁ \ s₂, (V x) (f x) + ∑ x ∈ s₂ \ s₁, -(V x) (f x)‖ ^ 2 = ∑ i ∈ s₁ \ s₂, ‖f i‖ ^ 2 + ∑ i ∈ s₂ \ s₁, ‖f i‖ ^ 2
<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>ι : Type u_4<VAR>G : ι → Type u_5<VAR>inst✝² : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)<VAR>inst✝ : DecidableEq ι<VAR>f : (i : ι) → G i<VAR>s₁ s₂ : Finset ι<VAR>F : (i : ι) → G i := fun i => if i ∈ s₁ then f i else -f i<GOAL>‖∑ x ∈ s₁ \ s₂, (V x) (f x) + ∑ x ∈ s₂ \ s₁, -(V x) (f x)‖ ^ 2 = ∑ i ∈ s₁ \ s₂, ‖f i‖ ^ 2 + ∑ i ∈ s₂ \ s₁, ‖f i‖ ^ 2
<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>ι : Type u_4<VAR>G : ι → Type u_5<VAR>inst✝² : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)<VAR>inst✝ : DecidableEq ι<VAR>f : (i : ι) → G i<VAR>s₁ s₂ : Finset ι<VAR>F : (i : ι) → G i := fun i => if i ∈ s₁ then f i else -f i<VAR>hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i<GOAL>‖∑ x ∈ s₁ \ s₂, (V x) (f x) + ∑ x ∈ s₂ \ s₁, -(V x) (f x)‖ ^ 2 = ∑ i ∈ s₁ \ s₂, ‖f i‖ ^ 2 + ∑ i ∈ s₂ \ s₁, ‖f i‖ ^ 2
<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>ι : Type u_4<VAR>G : ι → Type u_5<VAR>inst✝² : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)<VAR>inst✝ : DecidableEq ι<VAR>f : (i : ι) → G i<VAR>s₁ s₂ : Finset ι<VAR>F : (i : ι) → G i := fun i => if i ∈ s₁ then f i else -f i<VAR>hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i<VAR>hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i<GOAL>‖∑ x ∈ s₁ \ s₂, (V x) (f x) + ∑ x ∈ s₂ \ s₁, -(V x) (f x)‖ ^ 2 = ∑ i ∈ s₁ \ s₂, ‖f i‖ ^ 2 + ∑ i ∈ s₂ \ s₁, ‖f i‖ ^ 2
<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>ι : Type u_4<VAR>G : ι → Type u_5<VAR>inst✝² : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)<VAR>inst✝ : DecidableEq ι<VAR>f : (i : ι) → G i<VAR>s₁ s₂ : Finset ι<VAR>F : (i : ι) → G i := fun i => if i ∈ s₁ then f i else -f i<VAR>hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i<VAR>hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i<VAR>hF : ∀ (i : ι), ‖F i‖ = ‖f i‖<GOAL>‖∑ x ∈ s₁ \ s₂, (V x) (f x) + ∑ x ∈ s₂ \ s₁, -(V x) (f x)‖ ^ 2 = ∑ i ∈ s₁ \ s₂, ‖f i‖ ^ 2 + ∑ i ∈ s₂ \ s₁, ‖f i‖ ^ 2
<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>ι : Type u_4<VAR>G : ι → Type u_5<VAR>inst✝² : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)<VAR>inst✝ : DecidableEq ι<VAR>f : (i : ι) → G i<VAR>s₁ s₂ : Finset ι<VAR>F : (i : ι) → G i := fun i => if i ∈ s₁ then f i else -f i<VAR>hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i<VAR>hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i<VAR>hF : ∀ (i : ι), ‖F i‖ = ‖f i‖<VAR>this : ‖∑ i ∈ s₁ \ s₂, (V i) (F i) + ∑ i ∈ s₂ \ s₁, (V i) (F i)‖ ^ 2 = ∑ i ∈ s₁ \ s₂, ‖F i‖ ^ 2 + ∑ i ∈ s₂ \ s₁, ‖F i‖ ^ 2<GOAL>‖∑ x ∈ s₁ \ s₂, (V x) (f x) + ∑ x ∈ s₂ \ s₁, -(V x) (f x)‖ ^ 2 = ∑ i ∈ s₁ \ s₂, ‖f i‖ ^ 2 + ∑ i ∈ s₂ \ s₁, ‖f i‖ ^ 2
<VAR>x✝ y x : ℝ<GOAL>arccos x = 0 ↔ 1 ≤ x
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f✝ : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : PartialHomeomorph E E<VAR>hf' : ∀ x ∈ f.source, HasFDerivAt (↑f) (f' x) x<VAR>g : E → F<GOAL>∫ (x : E) in f.target, g x ∂μ = ∫ (x : E) in f.source, |(f' x).det| • g (↑f x) ∂μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f✝ : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : PartialHomeomorph E E<VAR>hf' : ∀ x ∈ f.source, HasFDerivAt (↑f) (f' x) x<VAR>g : E → F<VAR>this : ↑f '' f.source = f.target<GOAL>∫ (x : E) in f.target, g x ∂μ = ∫ (x : E) in f.source, |(f' x).det| • g (↑f x) ∂μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f✝ : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : PartialHomeomorph E E<VAR>hf' : ∀ x ∈ f.source, HasFDerivAt (↑f) (f' x) x<VAR>g : E → F<VAR>this : ↑f '' f.source = f.target<GOAL>∫ (x : E) in ↑f '' f.source, g x ∂μ = ∫ (x : E) in f.source, |(f' x).det| • g (↑f x) ∂μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f✝ : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : PartialHomeomorph E E<VAR>hf' : ∀ x ∈ f.source, HasFDerivAt (↑f) (f' x) x<VAR>g : E → F<VAR>this : ↑f '' f.source = f.target<GOAL>∀ x ∈ f.source, HasFDerivWithinAt (↑f) (f' x) f.source x
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f✝ : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : PartialHomeomorph E E<VAR>hf' : ∀ x ∈ f.source, HasFDerivAt (↑f) (f' x) x<VAR>g : E → F<VAR>this : ↑f '' f.source = f.target<VAR>x : E<VAR>hx : x ∈ f.source<GOAL>HasFDerivWithinAt (↑f) (f' x) f.source x
<VAR>α : Type u<VAR>inst✝¹ : Monoid α<VAR>a b c : α<VAR>inst✝ : Invertible c<GOAL>⅟c * a = b ↔ a = c * b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<GOAL>HasFiniteIntegral f μ ↔ ∫⁻ (a : α), edist (f a) 0 ∂μ < ⊤
<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>f g : α → α<VAR>h : Commute f g<VAR>hf : Monotone f<VAR>hg : StrictMono g<VAR>x : α<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>f^[n] x = g^[n] x ↔ f x = g x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a✝¹ b✝ a b c a✝ : α<GOAL>a✝ ∈ filter (fun x => x < c) (Ioo a b) ↔ a✝ ∈ Ioo a (min b c)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝¹ : PartialOrder ι✝<VAR>τ✝ : Ω → ι✝<VAR>f✝ : Filtration ι✝ m<VAR>ι : Type u_4<VAR>inst✝ : LinearOrder ι<VAR>τ : Ω → ι<VAR>f : Filtration ι m<VAR>hτ : IsStoppingTime f τ<VAR>h_countable : (Set.range τ).Countable<VAR>i : ι<GOAL>MeasurableSet {ω | i ≤ τ ω}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝¹ : PartialOrder ι✝<VAR>τ✝ : Ω → ι✝<VAR>f✝ : Filtration ι✝ m<VAR>ι : Type u_4<VAR>inst✝ : LinearOrder ι<VAR>τ : Ω → ι<VAR>f : Filtration ι m<VAR>hτ : IsStoppingTime f τ<VAR>h_countable : (Set.range τ).Countable<VAR>i : ι<VAR>this : {ω | i ≤ τ ω} = {ω | τ ω < i}ᶜ<GOAL>MeasurableSet {ω | i ≤ τ ω}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝¹ : PartialOrder ι✝<VAR>τ✝ : Ω → ι✝<VAR>f✝ : Filtration ι✝ m<VAR>ι : Type u_4<VAR>inst✝ : LinearOrder ι<VAR>τ : Ω → ι<VAR>f : Filtration ι m<VAR>hτ : IsStoppingTime f τ<VAR>h_countable : (Set.range τ).Countable<VAR>i : ι<VAR>this : {ω | i ≤ τ ω} = {ω | τ ω < i}ᶜ<GOAL>MeasurableSet {ω | τ ω < i}ᶜ
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>V₃ : Type u_5<VAR>inst✝⁴ : SeminormedAddCommGroup V<VAR>inst✝³ : SeminormedAddCommGroup W<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>s : AddSubgroup V<VAR>v : ↥s<GOAL>‖↑v‖ ≤ 1 * ‖v‖
<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>G' : Type u_7<VAR>G'' : Type u_8<VAR>inst✝³ : NormedLatticeAddCommGroup G''<VAR>inst✝² : NormedSpace ℝ G''<VAR>inst✝¹ : NormedLatticeAddCommGroup G'<VAR>inst✝ : NormedSpace ℝ G'<VAR>T : Set α → G' →L[ℝ] G''<VAR>h_add : FinMeasAdditive μ T<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f g : α →ₛ G'<VAR>hfi : Integrable (↑f) μ<VAR>hgi : Integrable (↑g) μ<VAR>hfg : f ≤ g<GOAL>setToSimpleFunc T f ≤ setToSimpleFunc T g
<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>G' : Type u_7<VAR>G'' : Type u_8<VAR>inst✝³ : NormedLatticeAddCommGroup G''<VAR>inst✝² : NormedSpace ℝ G''<VAR>inst✝¹ : NormedLatticeAddCommGroup G'<VAR>inst✝ : NormedSpace ℝ G'<VAR>T : Set α → G' →L[ℝ] G''<VAR>h_add : FinMeasAdditive μ T<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f g : α →ₛ G'<VAR>hfi : Integrable (↑f) μ<VAR>hgi : Integrable (↑g) μ<VAR>hfg : f ≤ g<GOAL>0 ≤ setToSimpleFunc T (g - f)
<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>G' : Type u_7<VAR>G'' : Type u_8<VAR>inst✝³ : NormedLatticeAddCommGroup G''<VAR>inst✝² : NormedSpace ℝ G''<VAR>inst✝¹ : NormedLatticeAddCommGroup G'<VAR>inst✝ : NormedSpace ℝ G'<VAR>T : Set α → G' →L[ℝ] G''<VAR>h_add : FinMeasAdditive μ T<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f g : α →ₛ G'<VAR>hfi : Integrable (↑f) μ<VAR>hgi : Integrable (↑g) μ<VAR>hfg : f ≤ g<GOAL>0 ≤ g - f
<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>G' : Type u_7<VAR>G'' : Type u_8<VAR>inst✝³ : NormedLatticeAddCommGroup G''<VAR>inst✝² : NormedSpace ℝ G''<VAR>inst✝¹ : NormedLatticeAddCommGroup G'<VAR>inst✝ : NormedSpace ℝ G'<VAR>T : Set α → G' →L[ℝ] G''<VAR>h_add : FinMeasAdditive μ T<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f g : α →ₛ G'<VAR>hfi : Integrable (↑f) μ<VAR>hgi : Integrable (↑g) μ<VAR>hfg : f ≤ g<VAR>x : α<GOAL>↑0 x ≤ ↑(g - f) 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>G' : Type u_7<VAR>G'' : Type u_8<VAR>inst✝³ : NormedLatticeAddCommGroup G''<VAR>inst✝² : NormedSpace ℝ G''<VAR>inst✝¹ : NormedLatticeAddCommGroup G'<VAR>inst✝ : NormedSpace ℝ G'<VAR>T : Set α → G' →L[ℝ] G''<VAR>h_add : FinMeasAdditive μ T<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f g : α →ₛ G'<VAR>hfi : Integrable (↑f) μ<VAR>hgi : Integrable (↑g) μ<VAR>hfg : f ≤ g<VAR>x : α<GOAL>↑f x ≤ ↑g x
<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<VAR>y : ℝ<VAR>hy : 0 < y<GOAL>Tendsto (fun x => c * x ^ y) (𝓝 0) (𝓝 0)
<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<VAR>y : ℝ<VAR>hy : 0 < y<GOAL>0 = c * 0 ^ y
<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<VAR>y : ℝ<VAR>hy : 0 < y<GOAL>0 ^ y ≠ 0 ∨ c ≠ ⊤
<VAR>n : ℕ<VAR>c✝ c : Composition n<GOAL>c ≠ ones n ↔ ∃ i ∈ c.blocks, 1 < i
<VAR>n : ℕ<VAR>c✝ c : Composition n<GOAL>(¬∀ i ∈ c.blocks, i = 1) ↔ ∃ i ∈ c.blocks, 1 < i
<VAR>n : ℕ<VAR>c✝ c : Composition n<VAR>this : ∀ j ∈ c.blocks, j = 1 ↔ j ≤ 1<GOAL>(¬∀ i ∈ c.blocks, i = 1) ↔ ∃ i ∈ c.blocks, 1 < i
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<GOAL>∃ a' b', a' ^ 3 + b' ^ 3 = ↑S'.u * S'.c ^ 3 ∧ IsCoprime a' b' ∧ ¬λ ∣ a' ∧ ¬λ ∣ b' ∧ λ ^ 2 ∣ a' + b'
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>h : λ ^ 2 ∣ S'.a + S'.b<GOAL>∃ a' b', a' ^ 3 + b' ^ 3 = ↑S'.u * S'.c ^ 3 ∧ IsCoprime a' b' ∧ ¬λ ∣ a' ∧ ¬λ ∣ b' ∧ λ ^ 2 ∣ a' + b'
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>h : λ ^ 2 ∣ S'.a + ↑η * S'.b<GOAL>∃ a' b', a' ^ 3 + b' ^ 3 = ↑S'.u * S'.c ^ 3 ∧ IsCoprime a' b' ∧ ¬λ ∣ a' ∧ ¬λ ∣ b' ∧ λ ^ 2 ∣ a' + b'
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>h : λ ^ 2 ∣ S'.a + ↑η ^ 2 * S'.b<GOAL>∃ a' b', a' ^ 3 + b' ^ 3 = ↑S'.u * S'.c ^ 3 ∧ IsCoprime a' b' ∧ ¬λ ∣ a' ∧ ¬λ ∣ b' ∧ λ ^ 2 ∣ a' + b'
<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>𝕜 : Type u_6<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : T2Space X<VAR>inst✝ : SecondCountableTopologyEither X E<VAR>f : X → 𝕜<VAR>hf : IntegrableOn f K μ<VAR>g : X → E<VAR>hg : ContinuousOn g K<VAR>hK : IsCompact K<GOAL>IntegrableOn (fun x => f x • g x) K μ
<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>𝕜 : Type u_6<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : T2Space X<VAR>inst✝ : SecondCountableTopologyEither X E<VAR>f : X → 𝕜<VAR>hf : IntegrableOn f K μ<VAR>g : X → E<VAR>hg : ContinuousOn g K<VAR>hK : IsCompact K<GOAL>Integrable (fun a => ‖f a • g a‖) (μ.restrict K)
<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>𝕜 : Type u_6<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : T2Space X<VAR>inst✝ : SecondCountableTopologyEither X E<VAR>f : X → 𝕜<VAR>hf : IntegrableOn f K μ<VAR>g : X → E<VAR>hg : ContinuousOn g K<VAR>hK : IsCompact K<GOAL>AEStronglyMeasurable (fun x => f x • g x) (μ.restrict K)
<VAR>a b ab : ℕ<VAR>r : ℤ<VAR>hab : a % b = ab<VAR>hr : jacobiSymNat ab b = r<GOAL>jacobiSymNat a b = r
<VAR>a b ab : ℕ<VAR>r : ℤ<VAR>hab : a % b = ab<VAR>hr : jacobiSymNat ab b = r<GOAL>jacobiSym (↑a % ↑b) b = jacobiSym (↑(a % b)) b
<VAR>x✝ y✝ x y : ℝ<VAR>a : ℕ<GOAL>√↑a < ↑a.sqrt + 1
<VAR>x✝ y✝ x y : ℝ<VAR>a : ℕ<GOAL>a < (a.sqrt + 1) ^ 2
<VAR>x✝ y✝ x y : ℝ<VAR>a : ℕ<GOAL>0 ≤ a.sqrt + 1
<VAR>μ : YoungDiagram<VAR>i1 i2 : ℕ<VAR>hi : i1 ≤ i2<GOAL>μ.rowLen i2 ≤ μ.rowLen i1
<VAR>μ : YoungDiagram<VAR>i1 i2 : ℕ<VAR>hi : i1 ≤ i2<VAR>h_lt : μ.rowLen i1 < μ.rowLen i2<GOAL>False
<VAR>μ : YoungDiagram<VAR>i1 i2 : ℕ<VAR>hi : i1 ≤ i2<VAR>h_lt : μ.rowLen i1 < μ.rowLen i2<GOAL>μ.rowLen i1 < μ.rowLen i1
<VAR>μ : YoungDiagram<VAR>i1 i2 : ℕ<VAR>hi : i1 ≤ i2<VAR>h_lt : (i2, μ.rowLen i1) ∈ μ<GOAL>(i1, μ.rowLen i1) ∈ μ
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Monoid α<VAR>a : α<GOAL>∀ {b : ConjClasses α}, a ∈ b.carrier ↔ ConjClasses.mk a = b
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Monoid α<VAR>a : α<GOAL>∀ (a_1 : α), a ∈ (ConjClasses.mk a_1).carrier ↔ ConjClasses.mk a = ConjClasses.mk a_1
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Monoid α<VAR>a b : α<GOAL>a ∈ (ConjClasses.mk b).carrier ↔ ConjClasses.mk a = ConjClasses.mk b
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Monoid α<VAR>a b : α<GOAL>a ∈ conjugatesOf b ↔ IsConj b a
<VAR>a : ℝ<GOAL>interior {z | a ≤ z.im} = {z | a < z.im}
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharZero R<VAR>n ν : ℕ<VAR>h : ν ≤ n<GOAL>eval 1 ((⇑derivative)^[n - ν] (bernsteinPolynomial R n ν)) ≠ 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharZero R<VAR>n ν : ℕ<VAR>h : ν ≤ n<GOAL>¬eval ν.succ (ascPochhammer ℕ (n - ν)) = 0