ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure α<VAR>f : α → E<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs_m : MeasurableSet s<VAR>hf_int : Integrable f μ<VAR>this : SigmaFinite ((μ.restrict s).trim hm)<GOAL>s.indicator (μ.restrict s[f|m]) =ᶠ[ae μ] s.indicator (μ[f|m])
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure α<VAR>f : α → E<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs_m : MeasurableSet s<VAR>hf_int : Integrable f μ<VAR>this : SigmaFinite ((μ.restrict s).trim hm)<GOAL>s.indicator (μ.restrict s[f|m]) =ᶠ[ae μ] μ[s.indicator f|m]
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure α<VAR>f : α → E<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs_m : MeasurableSet s<VAR>hf_int : Integrable f μ<VAR>this : SigmaFinite ((μ.restrict s).trim hm)<GOAL>∀ (s_1 : Set α), MeasurableSet s_1 → μ s_1 < ⊤ → IntegrableOn (s.indicator (μ.restrict s[f|m])) s_1 μ
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure α<VAR>f : α → E<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs_m : MeasurableSet s<VAR>hf_int : Integrable f μ<VAR>this : SigmaFinite ((μ.restrict s).trim hm)<GOAL>∀ (s_1 : Set α), MeasurableSet s_1 → μ s_1 < ⊤ → ∫ (x : α) in s_1, s.indicator (μ.restrict s[f|m]) x ∂μ = ∫ (x : α) in s_1, s.indicator f x ∂μ
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure α<VAR>f : α → E<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs_m : MeasurableSet s<VAR>hf_int : Integrable f μ<VAR>this : SigmaFinite ((μ.restrict s).trim hm)<GOAL>AEStronglyMeasurable' m (s.indicator (μ.restrict s[f|m])) μ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g✝ : ℝ → ℝ<VAR>a✝ b✝ : ℝ<VAR>μ : Measure ℝ<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Icc a b)<VAR>hgc : ContinuousOn g (Icc a b)<VAR>hle : ∀ x ∈ Ioc a b, f x ≤ g x<VAR>hlt : ∃ c ∈ Icc a b, f c < g c<GOAL>∫ (x : ℝ) in a..b, f x < ∫ (x : ℝ) in a..b, g x
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g✝ : ℝ → ℝ<VAR>a✝ b✝ : ℝ<VAR>μ : Measure ℝ<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Icc a b)<VAR>hgc : ContinuousOn g (Icc a b)<VAR>hle : ∀ x ∈ Ioc a b, f x ≤ g x<VAR>hlt : ∃ c ∈ Icc a b, f c < g c<GOAL>f ≤ᶠ[ae (volume.restrict (Ioc a b))] g
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g✝ : ℝ → ℝ<VAR>a✝ b✝ : ℝ<VAR>μ : Measure ℝ<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Icc a b)<VAR>hgc : ContinuousOn g (Icc a b)<VAR>hle : ∀ x ∈ Ioc a b, f x ≤ g x<VAR>hlt : ∃ c ∈ Icc a b, f c < g c<GOAL>(volume.restrict (Ioc a b)) {x | f x < g x} ≠ 0
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g✝ : ℝ → ℝ<VAR>a✝ b✝ : ℝ<VAR>μ : Measure ℝ<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Icc a b)<VAR>hgc : ContinuousOn g (Icc a b)<VAR>hle : ∀ x ∈ Ioc a b, f x ≤ g x<VAR>hlt : (volume.restrict (Ioc a b)) {x | f x < g x} = 0<GOAL>∀ c ∈ Icc a b, g c ≤ f c
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g✝ : ℝ → ℝ<VAR>a✝ b✝ : ℝ<VAR>μ : Measure ℝ<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Icc a b)<VAR>hgc : ContinuousOn g (Icc a b)<VAR>hle : ∀ x ∈ Ioc a b, f x ≤ g x<VAR>hlt : (volume.restrict (Ioc a b)) {x | f x < g x} = 0<VAR>h_eq : f =ᶠ[ae (volume.restrict (Ioc a b))] g<GOAL>∀ c ∈ Icc a b, g c ≤ f c
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g✝ : ℝ → ℝ<VAR>a✝ b✝ : ℝ<VAR>μ : Measure ℝ<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Icc a b)<VAR>hgc : ContinuousOn g (Icc a b)<VAR>hle : ∀ x ∈ Ioc a b, f x ≤ g x<VAR>hlt : (volume.restrict (Ioc a b)) {x | f x < g x} = 0<VAR>h_eq : f =ᶠ[ae (volume.restrict (Icc a b))] g<GOAL>∀ c ∈ Icc a b, g c ≤ f c
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : SMul 𝕜 E<VAR>inst✝ : SMul 𝕜 F<VAR>x : E<VAR>s t : Set E<VAR>S : Set (Set E)<VAR>hS : ∀ s ∈ S, StarConvex 𝕜 x s<GOAL>StarConvex 𝕜 x (⋃₀ S)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : SMul 𝕜 E<VAR>inst✝ : SMul 𝕜 F<VAR>x : E<VAR>s t : Set E<VAR>S : Set (Set E)<VAR>hS : ∀ s ∈ S, StarConvex 𝕜 x s<GOAL>StarConvex 𝕜 x (⋃ i, ↑i)
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x - a) ⁻¹' Ioo b c = Ioo (b + a) (c + a)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>f : Filter X<GOAL>ClusterPt x f ↔ ∃ u, ↑u ≤ f ∧ ↑u ≤ 𝓝 x
<VAR>s : ℕ<GOAL>(xgcd 0 s).2 = 1
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>hf : HasStrictDerivAt f f' x<VAR>hg : HasStrictDerivAt g g' x<GOAL>HasStrictDerivAt (fun x => f x - g x) (f' - g') x
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>c : R<VAR>h : c ≠ 0<GOAL>(C c * X).support = {1}
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n✝ m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>n : σ<GOAL>degreeOf n 0 = 0
<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>x : X<GOAL>pathComponentIn x univ = pathComponent x
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Group α<VAR>inst✝ : Group β<VAR>f : α → β<VAR>hf✝ hf : IsGroupHom f<VAR>a : α<GOAL>f a⁻¹ * f a = 1
<VAR>M₀ : Type u_1<VAR>inst✝² : MonoidWithZero M₀<VAR>inst✝¹ : NoZeroDivisors M₀<VAR>inst✝ : Nontrivial M₀<VAR>x : M₀<GOAL>x ∈ ↑(nonZeroDivisorsLeft M₀) ↔ x ∈ {x | x ≠ 0}
<VAR>M₀ : Type u_1<VAR>inst✝² : MonoidWithZero M₀<VAR>inst✝¹ : NoZeroDivisors M₀<VAR>inst✝ : Nontrivial M₀<VAR>x : M₀<GOAL>(∀ (a : M₀), x = 0 → a = 0) ↔ x ≠ 0
<VAR>M₀ : Type u_1<VAR>inst✝² : MonoidWithZero M₀<VAR>inst✝¹ : NoZeroDivisors M₀<VAR>inst✝ : Nontrivial M₀<VAR>x : M₀<VAR>h : ∀ (a : M₀), x = 0 → a = 0<GOAL>x ≠ 0
<VAR>M₀ : Type u_1<VAR>inst✝² : MonoidWithZero M₀<VAR>inst✝¹ : NoZeroDivisors M₀<VAR>inst✝ : Nontrivial M₀<VAR>x : M₀<VAR>h : x = 0<GOAL>∃ a, x = 0 ∧ a ≠ 0
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>X : C<GOAL>Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X)) ∈ distinguishedTriangles
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>X : C<GOAL>Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X)) ≅ (Triangle.mk 0 (𝟙 ((shiftFunctor C 1).obj X)) 0).invRotate
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>x y : α<GOAL>(𝓝 (x, y)).HasBasis (fun s => s ∈ 𝓤 α ∧ SymmetricRel s) fun s => ball x s ×ˢ ball y s
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>x y : α<GOAL>(𝓝 x ×ˢ 𝓝 y).HasBasis (fun s => s ∈ 𝓤 α ∧ SymmetricRel s) fun s => ball x s ×ˢ ball y s
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>x y : α<GOAL>∀ {i j : Set (α × α)}, i ∈ 𝓤 α ∧ SymmetricRel i → j ∈ 𝓤 α ∧ SymmetricRel j → ∃ k, (k ∈ 𝓤 α ∧ SymmetricRel k) ∧ ball x k ⊆ ball x i ∧ ball y k ⊆ ball y j
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>x y : α<VAR>U V : Set (α × α)<VAR>U_in : U ∈ 𝓤 α<VAR>U_symm : SymmetricRel U<VAR>V_in : V ∈ 𝓤 α<VAR>V_symm : SymmetricRel V<GOAL>∃ k, (k ∈ 𝓤 α ∧ SymmetricRel k) ∧ ball x k ⊆ ball x U ∧ ball y k ⊆ ball y V
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring S<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<VAR>α' : Type u_7<VAR>M' : Type u_8<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>v✝ : α → M<VAR>v' : α' → M'<VAR>v : Option α → M<VAR>f : Option α →₀ R<GOAL>(Finsupp.total (Option α) M R v) f = f none • v none + (Finsupp.total α M R (v ∘ Option.some)) f.some
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring S<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<VAR>α' : Type u_7<VAR>M' : Type u_8<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>v✝ : α → M<VAR>v' : α' → M'<VAR>v : Option α → M<VAR>f : Option α →₀ R<GOAL>(f none • v none + f.some.sum fun a r => r • v (Option.some a)) = f none • v none + f.some.sum fun i a => a • (v ∘ Option.some) i
<VAR>α : Type v<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>a : G<VAR>b : α<VAR>n : ℤ<GOAL>a ^ (n % ↑(minimalPeriod (fun x => a • x) b)) • b = a ^ n • b
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : Ring B'<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : Algebra A B'<VAR>x✝ : B<VAR>f : B →ₐ[A] B'<VAR>hf : Injective ⇑f<VAR>x : B<GOAL>minpoly A (f x) = minpoly A x
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : Ring B'<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : Algebra A B'<VAR>x✝¹ : B<VAR>f : B →ₐ[A] B'<VAR>hf : Injective ⇑f<VAR>x : B<VAR>x✝ : IsIntegral A x<GOAL>⋯.min (fun x_1 => x_1.Monic ∧ eval₂ (algebraMap A B') (f x) x_1 = 0) ⋯ = ⋯.min (fun x_1 => x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) x✝
<VAR>x y : ℝ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<GOAL>√x < y ↔ x < y ^ 2
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : ℕ → R<VAR>g : ℕ → M<VAR>m n : ℕ<VAR>hmn : m < n<GOAL>∑ i ∈ Ico m n, f i • g i = f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range m, g i - ∑ i ∈ Ico m (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : ℕ → R<VAR>g : ℕ → M<VAR>m n : ℕ<VAR>hmn : m < n<VAR>h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i<GOAL>∑ i ∈ Ico m n, f i • g i = f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range m, g i - ∑ i ∈ Ico m (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : ℕ → R<VAR>g : ℕ → M<VAR>m n : ℕ<VAR>hmn : m < n<VAR>h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i<VAR>h₂ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i = ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range (m + 1), g i<GOAL>∑ i ∈ Ico m n, f i • g i = f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range m, g i - ∑ i ∈ Ico m (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : ℕ → R<VAR>g : ℕ → M<VAR>m n : ℕ<VAR>hmn : m < n<VAR>h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i<VAR>h₂ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i = ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range (m + 1), g i<GOAL>f m • g m + ∑ k ∈ Ico (m + 1) n, f k • g k = f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range m, g i - ∑ i ∈ Ico m (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : ℕ → R<VAR>g : ℕ → M<VAR>m n : ℕ<VAR>hmn : m < n<VAR>h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i<VAR>h₂ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i = ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range (m + 1), g i<VAR>h₃ : ∑ i ∈ Ico (m + 1) n, f i • g i = ∑ i ∈ Ico (m + 1) n, f i • ((range (i + 1)).sum g - (range i).sum g)<GOAL>f m • g m + ∑ k ∈ Ico (m + 1) n, f k • g k = f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range m, g i - ∑ i ∈ Ico m (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : ℕ → R<VAR>g : ℕ → M<VAR>m n : ℕ<VAR>hmn : m < n<VAR>h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i<VAR>h₂ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i = ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range (m + 1), g i<VAR>h₃ : ∑ i ∈ Ico (m + 1) n, f i • g i = ∑ i ∈ Ico (m + 1) n, f i • ((range (i + 1)).sum g - (range i).sum g)<GOAL>f m • g m + ∑ i ∈ Ico (m + 1) n, f i • ((range (i + 1)).sum g - (range i).sum g) = f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range m, g i - ∑ i ∈ Ico m (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : ℕ → R<VAR>g : ℕ → M<VAR>m n : ℕ<VAR>hmn : m < n<VAR>h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i<VAR>h₂ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i = ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range (m + 1), g i<VAR>h₃ : ∑ i ∈ Ico (m + 1) n, f i • g i = ∑ i ∈ Ico (m + 1) n, f i • ((range (i + 1)).sum g - (range i).sum g)<GOAL>f m • g m + (∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range (m + 1), g i - ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i) = f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range m, g i - ∑ i ∈ Ico m (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : ℕ → R<VAR>g : ℕ → M<VAR>m n : ℕ<VAR>hmn : m < n<VAR>h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i<VAR>h₂ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i = ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range (m + 1), g i<VAR>h₃ : ∑ i ∈ Ico (m + 1) n, f i • g i = ∑ i ∈ Ico (m + 1) n, f i • ((range (i + 1)).sum g - (range i).sum g)<VAR>h₄ : ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range (m + 1), g i - ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i = f (n - 1) • (range n).sum g - f m • (range (m + 1)).sum g + ∑ i ∈ Ico m (n - 1), (f i • (range (i + 1)).sum g - f (i + 1) • (range (i + 1)).sum g)<GOAL>f m • g m + (∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range (m + 1), g i - ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i) = f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range m, g i - ∑ i ∈ Ico m (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : ℕ → R<VAR>g : ℕ → M<VAR>m n : ℕ<VAR>hmn : m < n<VAR>h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i<VAR>h₂ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i = ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range (m + 1), g i<VAR>h₃ : ∑ i ∈ Ico (m + 1) n, f i • g i = ∑ i ∈ Ico (m + 1) n, f i • ((range (i + 1)).sum g - (range i).sum g)<VAR>h₄ : ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range (m + 1), g i - ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i = f (n - 1) • (range n).sum g - f m • (range (m + 1)).sum g + ∑ i ∈ Ico m (n - 1), (f i • (range (i + 1)).sum g - f (i + 1) • (range (i + 1)).sum g)<GOAL>f m • g m + (f (n - 1) • (range n).sum g - f m • (range (m + 1)).sum g + ∑ i ∈ Ico m (n - 1), (f i • (range (i + 1)).sum g - f (i + 1) • (range (i + 1)).sum g)) = f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range m, g i - ∑ i ∈ Ico m (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : ℕ → R<VAR>g : ℕ → M<VAR>m n : ℕ<VAR>hmn : m < n<VAR>h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i<VAR>h₂ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i = ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range (m + 1), g i<VAR>h₃ : ∑ i ∈ Ico (m + 1) n, f i • g i = ∑ i ∈ Ico (m + 1) n, f i • ((range (i + 1)).sum g - (range i).sum g)<VAR>h₄ : ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range (m + 1), g i - ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i = f (n - 1) • (range n).sum g - f m • (range (m + 1)).sum g + ∑ i ∈ Ico m (n - 1), (f i • (range (i + 1)).sum g - f (i + 1) • (range (i + 1)).sum g)<VAR>this : ∀ (i : ℕ), f i • ∑ i ∈ range (i + 1), g i - f (i + 1) • ∑ i ∈ range (i + 1), g i = -((f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i)<GOAL>f m • g m + (f (n - 1) • (range n).sum g - f m • (range (m + 1)).sum g + ∑ i ∈ Ico m (n - 1), (f i • (range (i + 1)).sum g - f (i + 1) • (range (i + 1)).sum g)) = f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range m, g i - ∑ i ∈ Ico m (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : ℕ → R<VAR>g : ℕ → M<VAR>m n : ℕ<VAR>hmn : m < n<VAR>h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i<VAR>h₂ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i = ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range (m + 1), g i<VAR>h₃ : ∑ i ∈ Ico (m + 1) n, f i • g i = ∑ i ∈ Ico (m + 1) n, f i • ((range (i + 1)).sum g - (range i).sum g)<VAR>h₄ : ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range (m + 1), g i - ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i = f (n - 1) • (range n).sum g - f m • (range (m + 1)).sum g + ∑ i ∈ Ico m (n - 1), (f i • (range (i + 1)).sum g - f (i + 1) • (range (i + 1)).sum g)<VAR>this : ∀ (i : ℕ), f i • ∑ i ∈ range (i + 1), g i - f (i + 1) • ∑ i ∈ range (i + 1), g i = -((f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i)<GOAL>f m • g m + (f (n - 1) • (range n).sum g - (f m • ∑ x ∈ range m, g x + f m • g m) + -∑ x ∈ Ico m (n - 1), ((f (x + 1) - f x) • ∑ x ∈ range x, g x + (f (x + 1) - f x) • g x)) = f (n - 1) • ∑ x ∈ range n, g x - f m • ∑ x ∈ range m, g x - ∑ x ∈ Ico m (n - 1), ((f (x + 1) - f x) • ∑ x ∈ range x, g x + (f (x + 1) - f x) • g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Mul α<VAR>inst✝² : LinearOrder α<VAR>a b c d : α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>h : a * b ≤ c * d<GOAL>min a b ≤ max c d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Mul α<VAR>inst✝² : LinearOrder α<VAR>a b c d : α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>h : a * b ≤ c * d<GOAL>(a ≤ c ∨ a ≤ d) ∨ b ≤ c ∨ b ≤ d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Mul α<VAR>inst✝² : LinearOrder α<VAR>a b c d : α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>h : (c < a ∧ d < a) ∧ c < b ∧ d < b<GOAL>c * d < a * b
<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>(coclosedCompact X).HasBasis (fun s => IsClosed s ∧ IsCompact s) compl
<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>(⨅ s, ⨅ (_ : IsClosed s ∧ IsCompact s), 𝓟 sᶜ).HasBasis (fun s => IsClosed s ∧ IsCompact s) compl
<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>∀ (i : Set X), IsClosed i ∧ IsCompact i → ∀ (j : Set X), IsClosed j ∧ IsCompact j → ∃ k, (IsClosed k ∧ IsCompact k) ∧ kᶜ ⊆ iᶜ ∧ kᶜ ⊆ jᶜ
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t✝ s : Set X<VAR>hs₁ : IsClosed s<VAR>hs₂ : IsCompact s<VAR>t : Set X<VAR>ht₁ : IsClosed t<VAR>ht₂ : IsCompact t<GOAL>∃ k, (IsClosed k ∧ IsCompact k) ∧ kᶜ ⊆ sᶜ ∧ kᶜ ⊆ tᶜ
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>ζ : R<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>h : IsPrimitiveRoot ζ n<GOAL>X ^ n - 1 = ∏ ζ ∈ nthRootsFinset n R, (X - C ζ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι✝ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>ι : Type u_5<VAR>x✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>As : ι → Set α<VAR>As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ<VAR>As_disj : Pairwise (AEDisjoint μ on As)<GOAL>{i | 0 < μ (As i)}.Countable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι✝ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>ι : Type u_5<VAR>x✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>As : ι → Set α<VAR>As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sFiniteSeq μ))<VAR>As_disj : Pairwise (AEDisjoint (sum (sFiniteSeq μ)) on As)<GOAL>{i | 0 < (sum (sFiniteSeq μ)) (As i)}.Countable