ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u<VAR>m₁ m₂ : X → X → X<VAR>e₁ e₂ : X<VAR>h₁ : IsUnital m₁ e₁<VAR>h₂ : IsUnital m₂ e₂<VAR>distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)<VAR>a b : X<GOAL>m₁ a b = m₂ a b
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : G ⊣ F<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>X : D<VAR>Y : C<GOAL>Function.Bijective fun g => adj.unit.app X ≫ g
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_3, u_2} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : G ⊣ F<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>X : D<VAR>Y : C<VAR>e_1✝ : ((G ⋙ F).obj X ⟶ F.obj Y) = (F.obj (G.obj X) ⟶ F.obj Y)<VAR>e_2✝ : ((𝟭 D).obj X ⟶ F.obj Y) = (X ⟶ F.obj Y)<GOAL>(fun g => adj.unit.app X ≫ g) = ⇑((Functor.FullyFaithful.ofFullyFaithful F).homEquiv.symm.trans (adj.homEquiv X Y))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>y : M<VAR>hy : y ∈ f.source<GOAL>map (↑(f.extend I).symm) (𝓝[↑(f.extend I).symm ⁻¹' s ∩ range ↑I] ↑(f.extend I) y) = 𝓝[s] y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>y : M<VAR>hy : y ∈ f.source<GOAL>↑(f.extend I).symm ∘ ↑(f.extend I) =ᶠ[𝓝[s] y] id
<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<VAR>S : Set (Set X)<VAR>hf : S.Finite<VAR>hc : ∀ s ∈ S, IsLindelof s<GOAL>IsLindelof (⋃₀ S)
<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<VAR>S : Set (Set X)<VAR>hf : S.Finite<VAR>hc : ∀ s ∈ S, IsLindelof s<GOAL>IsLindelof (⋃ i ∈ S, i)
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>t : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>h : Valid' o₂ t.dual o₁<GOAL>Valid' o₁ t o₂
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>t : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>h : Valid' o₂ t.dual o₁<VAR>this : Valid' o₁ t.dual.dual o₂<GOAL>Valid' o₁ t o₂
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π π₁✝ π₂✝ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>π₁ π₂ : Prepartition I<GOAL>J ∈ π₁ ⊓ π₂ ↔ ∃ J₁ ∈ π₁, ∃ J₂ ∈ π₂, ↑J = ↑J₁ ⊓ ↑J₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<GOAL>sup f = lsub f ↔ ∀ a < lsub f, succ a < lsub f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>h : sup f = lsub f<GOAL>∀ a < lsub f, succ a < lsub f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>hf : ∀ a < lsub f, succ a < lsub f<VAR>i : ι<GOAL>f i < sup f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>hf : ∀ a < lsub f, succ a < lsub f<VAR>i : ι<VAR>hle : sup f ≤ f i<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>hf : ∀ a < lsub f, succ a < lsub f<VAR>i : ι<VAR>hle : sup f ≤ f i<VAR>heq : succ (sup f) = lsub f<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>hf : ∀ a < lsub f, succ a < lsub f<VAR>i : ι<VAR>hle : sup f ≤ f i<VAR>heq : succ (sup f) = lsub f<VAR>this : succ (sup f) < lsub f<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>hf : ∀ a < lsub f, succ a < lsub f<VAR>i : ι<VAR>hle : sup f ≤ f i<VAR>heq : succ (sup f) = lsub f<VAR>this : lsub f < lsub f<GOAL>False
<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>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<GOAL>AEMeasurable (fun x => |(f' x).det|.toNNReal) (μ.restrict s)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝ : Zero M<VAR>f : α →₀ M<GOAL>(List.map Prod.toSigma f.graph.toList).NodupKeys
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝ : Zero M<VAR>f : α →₀ M<GOAL>∀ x ∈ f.graph.toList, ∀ y ∈ f.graph.toList, x.1 = y.1 → x = y
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝ : Zero M<VAR>f : α →₀ M<GOAL>f.graph.toList.Nodup
<VAR>n : ℕ<VAR>s : ℕ := n.sqrt<GOAL>pair (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1 (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).2 = n
<VAR>n : ℕ<VAR>s : ℕ := n.sqrt<VAR>sm : s * s + (n - s * s) = n<GOAL>pair (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1 (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).2 = n
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>q n : ℕ<VAR>hprime : Nat.Prime q<VAR>hchar✝ : CharP R q<VAR>this : Fact (Nat.Prime q)<GOAL>(-1) ^ q ^ n = -1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>M' : Type u_3<VAR>N' : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : MulOneClass M<VAR>inst✝³ : MulOneClass N<VAR>inst✝² : MulOneClass M'<VAR>inst✝¹ : MulOneClass N'<VAR>inst✝ : MulOneClass P<VAR>f : M ∗ N →* P<GOAL>MonoidHom.mrange f = MonoidHom.mrange (f.comp inl) ⊔ MonoidHom.mrange (f.comp inr)
<VAR>e : ℝ<VAR>d n : ℕ<VAR>h : NormNum.IsInt e (Int.negOfNat n)<VAR>w : Nat.blt 1 n = true<GOAL>0 < Real.log e
<VAR>e : ℝ<VAR>d n : ℕ<VAR>h : NormNum.IsInt e (Int.negOfNat n)<VAR>w : Nat.blt 1 n = true<GOAL>0 < Real.log (-↑n)
<VAR>e : ℝ<VAR>d n : ℕ<VAR>h : NormNum.IsInt e (Int.negOfNat n)<VAR>w : Nat.blt 1 n = true<GOAL>0 < Real.log ↑n
<VAR>e : ℝ<VAR>d n : ℕ<VAR>h : NormNum.IsInt e (Int.negOfNat n)<VAR>w : Nat.blt 1 n = true<GOAL>1 < ↑n
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>r : HomRel C<VAR>D : Type u_3<VAR>inst✝ : Category.{u_4, u_3} D<VAR>F : C ⥤ D<VAR>H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂<GOAL>functor r ⋙ lift r F H = F
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>r : HomRel C<VAR>D : Type u_3<VAR>inst✝ : Category.{u_4, u_3} D<VAR>F : C ⥤ D<VAR>H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂<GOAL>autoParam (∀ (X Y : C) (f : X ⟶ Y), (functor r ⋙ lift r F H).map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯) _auto✝
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>r : HomRel C<VAR>D : Type u_3<VAR>inst✝ : Category.{u_4, u_3} D<VAR>F : C ⥤ D<VAR>H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂<GOAL>∀ (X : C), (functor r ⋙ lift r F H).obj X = F.obj X
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>ι : Type u_2<VAR>H : ι → Subgroup G<VAR>g : ι → G<VAR>s : Finset ι<VAR>hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ<GOAL>∃ i ∈ s, (H i).FiniteIndex ∧ (H i).index ≤ s.card
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>ι : Type u_2<VAR>H : ι → Subgroup G<VAR>g : ι → G<VAR>s : Finset ι<VAR>hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ<VAR>h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index<GOAL>False
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>ι : Type u_2<VAR>H : ι → Subgroup G<VAR>g : ι → G<VAR>s : Finset ι<VAR>hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ<VAR>h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index<GOAL>∑ i ∈ s, (↑(H i).index)⁻¹ < 1
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>ι : Type u_2<VAR>H : ι → Subgroup G<VAR>g : ι → G<VAR>s : Finset ι<VAR>hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ<VAR>h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index<VAR>hs : ¬s = ∅<GOAL>∑ i ∈ s, (↑(H i).index)⁻¹ < 1
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>ι : Type u_2<VAR>H : ι → Subgroup G<VAR>g : ι → G<VAR>s : Finset ι<VAR>hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ<VAR>h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index<VAR>hs : s.Nonempty<GOAL>∑ i ∈ s, (↑(H i).index)⁻¹ < 1
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>ι : Type u_2<VAR>H : ι → Subgroup G<VAR>g : ι → G<VAR>s : Finset ι<VAR>hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ<VAR>h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index<VAR>hs : s.Nonempty<VAR>hs' : 0 < s.card<GOAL>∑ i ∈ s, (↑(H i).index)⁻¹ < 1
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>ι : Type u_2<VAR>H : ι → Subgroup G<VAR>g : ι → G<VAR>s : Finset ι<VAR>hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ<VAR>h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index<VAR>hs : s.Nonempty<VAR>hs' : 0 < s.card<VAR>hlt : ∀ i ∈ s, (↑(H i).index)⁻¹ < (↑s.card)⁻¹<GOAL>∑ i ∈ s, (↑(H i).index)⁻¹ < 1
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>ι : Type u_2<VAR>H : ι → Subgroup G<VAR>g : ι → G<VAR>s : Finset ι<VAR>hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ<VAR>h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index<VAR>hs : s.Nonempty<VAR>hs' : 0 < s.card<VAR>hlt : ∀ i ∈ s, (↑(H i).index)⁻¹ < (↑s.card)⁻¹<GOAL>∑ i ∈ s, (↑s.card)⁻¹ = 1
<VAR>α : Type u_1<VAR>s t : Set α<VAR>a : α<VAR>β : Type u_2<VAR>inst✝ : InvolutiveStar β<VAR>x y : β<GOAL>y ∈ {x}⋆ ↔ y ∈ {x⋆}
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : β → α<VAR>b : β<VAR>s : Set β<GOAL>ContinuousWithinAt f s b ↔ Tendsto (fun x => (f x, f b)) (𝓝[s] b) (𝓤 α)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>x : M<VAR>hy : x ∈ f.source<GOAL>map (↑(f.extend I)) (𝓝 x) = 𝓝[range ↑I] ↑(f.extend I) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>f✝ : α → β → ℝ≥0∞<VAR>inst✝¹ : Countable ι<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<VAR>f : ι → α → β → ℝ≥0∞<VAR>hf : ∀ (i : ι), Measurable (Function.uncurry (f i))<GOAL>κ.withDensity (∑' (n : ι), f n) = Kernel.sum fun n => κ.withDensity (f n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>f✝ : α → β → ℝ≥0∞<VAR>inst✝¹ : Countable ι<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<VAR>f : ι → α → β → ℝ≥0∞<VAR>hf : ∀ (i : ι), Measurable (Function.uncurry (f i))<VAR>h_sum_a : ∀ (a : α), Summable fun n => f n a<GOAL>κ.withDensity (∑' (n : ι), f n) = Kernel.sum fun n => κ.withDensity (f n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>f✝ : α → β → ℝ≥0∞<VAR>inst✝¹ : Countable ι<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<VAR>f : ι → α → β → ℝ≥0∞<VAR>hf : ∀ (i : ι), Measurable (Function.uncurry (f i))<VAR>h_sum_a : ∀ (a : α), Summable fun n => f n a<VAR>h_sum : Summable fun n => f n<GOAL>κ.withDensity (∑' (n : ι), f n) = Kernel.sum fun n => κ.withDensity (f n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>f✝ : α → β → ℝ≥0∞<VAR>inst✝¹ : Countable ι<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<VAR>f : ι → α → β → ℝ≥0∞<VAR>hf : ∀ (i : ι), Measurable (Function.uncurry (f i))<VAR>h_sum_a : ∀ (a : α), Summable fun n => f n a<VAR>h_sum : Summable fun n => f n<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>((κ.withDensity (∑' (n : ι), f n)) a) s = ((Kernel.sum fun n => κ.withDensity (f n)) a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>f✝ : α → β → ℝ≥0∞<VAR>inst✝¹ : Countable ι<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<VAR>f : ι → α → β → ℝ≥0∞<VAR>hf : ∀ (i : ι), Measurable (Function.uncurry (f i))<VAR>h_sum_a : ∀ (a : α), Summable fun n => f n a<VAR>h_sum : Summable fun n => f n<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫⁻ (b : β) in s, tsum (fun n => f n) a b ∂κ a = ∑' (n : ι), ((κ.withDensity (f n)) a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>f✝ : α → β → ℝ≥0∞<VAR>inst✝¹ : Countable ι<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<VAR>f : ι → α → β → ℝ≥0∞<VAR>hf : ∀ (i : ι), Measurable (Function.uncurry (f i))<VAR>h_sum_a : ∀ (a : α), Summable fun n => f n a<VAR>h_sum : Summable fun n => f n<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Measurable (Function.uncurry (∑' (n : ι), f n))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>f✝ : α → β → ℝ≥0∞<VAR>inst✝¹ : Countable ι<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<VAR>f : ι → α → β → ℝ≥0∞<VAR>hf : ∀ (i : ι), Measurable (Function.uncurry (f i))<VAR>h_sum_a : ∀ (a : α), Summable fun n => f n a<VAR>h_sum : Summable fun n => f n<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>this : ∫⁻ (b : β) in s, tsum (fun n => f n) a b ∂κ a = ∫⁻ (b : β) in s, ∑' (n : ι), (fun b => f n a b) b ∂κ a<GOAL>∫⁻ (b : β) in s, tsum (fun n => f n) a b ∂κ a = ∑' (n : ι), ((κ.withDensity (f n)) a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>f✝ : α → β → ℝ≥0∞<VAR>inst✝¹ : Countable ι<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<VAR>f : ι → α → β → ℝ≥0∞<VAR>hf : ∀ (i : ι), Measurable (Function.uncurry (f i))<VAR>h_sum_a : ∀ (a : α), Summable fun n => f n a<VAR>h_sum : Summable fun n => f n<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>this : ∫⁻ (b : β) in s, tsum (fun n => f n) a b ∂κ a = ∫⁻ (b : β) in s, ∑' (n : ι), (fun b => f n a b) b ∂κ a<GOAL>∑' (i : ι), ∫⁻ (a_1 : β) in s, f i a a_1 ∂κ a = ∑' (n : ι), ((κ.withDensity (f n)) a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>f✝ : α → β → ℝ≥0∞<VAR>inst✝¹ : Countable ι<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<VAR>f : ι → α → β → ℝ≥0∞<VAR>hf : ∀ (i : ι), Measurable (Function.uncurry (f i))<VAR>h_sum_a : ∀ (a : α), Summable fun n => f n a<VAR>h_sum : Summable fun n => f n<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>this : ∫⁻ (b : β) in s, tsum (fun n => f n) a b ∂κ a = ∫⁻ (b : β) in s, ∑' (n : ι), (fun b => f n a b) b ∂κ a<VAR>n : ι<GOAL>∫⁻ (a_1 : β) in s, f n a a_1 ∂κ a = ((κ.withDensity (f n)) a) s
<VAR>G : Type u_1<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : BorelSpace G<VAR>inst✝³ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>c : ℝ≥0<GOAL>(c • μ').haarScalarFactor μ = c • μ'.haarScalarFactor μ
<VAR>G : Type u_1<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : BorelSpace G<VAR>inst✝³ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>c : ℝ≥0<VAR>g : G → ℝ<VAR>g_cont : Continuous g<VAR>g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }<VAR>g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }<VAR>g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0<GOAL>(c • μ').haarScalarFactor μ = c • μ'.haarScalarFactor μ
<VAR>G : Type u_1<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : BorelSpace G<VAR>inst✝³ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>c : ℝ≥0<VAR>g : G → ℝ<VAR>g_cont : Continuous g<VAR>g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }<VAR>g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }<VAR>g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0<VAR>int_g_ne_zero : ∫ (x : G), g x ∂μ ≠ 0<GOAL>(c • μ').haarScalarFactor μ = c • μ'.haarScalarFactor μ
<VAR>G : Type u_1<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : BorelSpace G<VAR>inst✝³ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>c : ℝ≥0<VAR>g : G → ℝ<VAR>g_cont : Continuous g<VAR>g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }<VAR>g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }<VAR>g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0<VAR>int_g_ne_zero : ∫ (x : G), g x ∂μ ≠ 0<GOAL>↑((c • μ').haarScalarFactor μ) = ↑(c • μ'.haarScalarFactor μ)
<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>m n : ZNum<GOAL>↑(m - n) = ↑m - ↑n
<VAR>n✝ b n : ℕ<GOAL>(b + 2).digits (n + 1) = (n + 1) % (b + 2) :: (b + 2).digits ((n + 1) / (b + 2))
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>a : α<VAR>s : Set α<GOAL>TotallyBounded (insert a s) ↔ TotallyBounded s
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : Group G'<VAR>inst✝⁴ : Group G''<VAR>A : Type u_4<VAR>inst✝³ : AddGroup A<VAR>G₁ : Type u_5<VAR>G₂ : Type u_6<VAR>G₃ : Type u_7<VAR>inst✝² : Group G₁<VAR>inst✝¹ : Group G₂<VAR>inst✝ : Group G₃<VAR>f : G₁ →* G₂<VAR>f_inv : G₂ → G₁<VAR>hf : Function.RightInverse f_inv ⇑f<VAR>g : G₁ →* G₃<VAR>hg : f.ker ≤ g.ker<VAR>h : G₂ →* G₃<VAR>hh : h.comp f = g<GOAL>h = (f.liftOfRightInverse f_inv hf) ⟨h.comp f, ⋯⟩
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>𝒢 : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>τ π : Ω → ℕ<VAR>inst✝ : SigmaFiniteFiltration μ 𝒢<VAR>hf : Submartingale f 𝒢 μ<VAR>hτ : IsStoppingTime 𝒢 τ<VAR>hπ : IsStoppingTime 𝒢 π<VAR>hle : τ ≤ π<VAR>N : ℕ<VAR>hbdd : ∀ (ω : Ω), π ω ≤ N<GOAL>∫ (x : Ω), stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), stoppedValue f π x ∂μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>𝒢 : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>τ π : Ω → ℕ<VAR>inst✝ : SigmaFiniteFiltration μ 𝒢<VAR>hf : Submartingale f 𝒢 μ<VAR>hτ : IsStoppingTime 𝒢 τ<VAR>hπ : IsStoppingTime 𝒢 π<VAR>hle : τ ≤ π<VAR>N : ℕ<VAR>hbdd : ∀ (ω : Ω), π ω ≤ N<GOAL>0 ≤ ∫ (a : Ω), (fun ω => (∑ i ∈ Finset.range (N + 1), {ω | τ ω ≤ i ∧ i < π ω}.indicator (f (i + 1) - f i)) ω) a ∂μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>𝒢 : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>τ π : Ω → ℕ<VAR>inst✝ : SigmaFiniteFiltration μ 𝒢<VAR>hf : Submartingale f 𝒢 μ<VAR>hτ : IsStoppingTime 𝒢 τ<VAR>hπ : IsStoppingTime 𝒢 π<VAR>hle : τ ≤ π<VAR>N : ℕ<VAR>hbdd : ∀ (ω : Ω), π ω ≤ N<GOAL>Integrable (stoppedValue f π) μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>𝒢 : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>τ π : Ω → ℕ<VAR>inst✝ : SigmaFiniteFiltration μ 𝒢<VAR>hf : Submartingale f 𝒢 μ<VAR>hτ : IsStoppingTime 𝒢 τ<VAR>hπ : IsStoppingTime 𝒢 π<VAR>hle : τ ≤ π<VAR>N : ℕ<VAR>hbdd : ∀ (ω : Ω), π ω ≤ N<GOAL>Integrable (stoppedValue f τ) μ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<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>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>hf : HasFPowerSeriesAt f pf x<VAR>hg : HasFPowerSeriesAt g pg x<GOAL>HasFPowerSeriesAt (f - g) (pf - pg) x
<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>f : R →+* S<VAR>t : Subring S<VAR>h : t ≤ f.range<GOAL>map f (comap f t) = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>rα : α → α → Prop<VAR>rβ : β → β → Prop<VAR>a✝ : α<VAR>b✝ : β<VAR>C : α → α → Sort u_3<VAR>hr : WellFounded rα<VAR>IH : (a₁ b₁ : α) → ((a₂ b₂ : α) → GameAdd rα s(a₂, b₂) s(a₁, b₁) → C a₂ b₂) → C a₁ b₁<VAR>a b : α<GOAL>⋯.fix (fun x IH' => IH x.1 x.2 fun a' b' => IH' (a', b')) (a, b) = IH a b fun a' b' x => ⋯.fix (fun x IH' => IH x.1 x.2 fun a' b' => IH' (a', b')) (a', b')
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>hconn : G.Connected<GOAL>G.dist u w ≤ G.dist u v + G.dist v w
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>hconn : G.Connected<VAR>p : G.Walk u v<VAR>hp : p.length = G.dist u v<GOAL>G.dist u w ≤ G.dist u v + G.dist v w
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>hconn : G.Connected<VAR>p : G.Walk u v<VAR>hp : p.length = G.dist u v<VAR>q : G.Walk v w<VAR>hq : q.length = G.dist v w<GOAL>G.dist u w ≤ G.dist u v + G.dist v w
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>hconn : G.Connected<VAR>p : G.Walk u v<VAR>hp : p.length = G.dist u v<VAR>q : G.Walk v w<VAR>hq : q.length = G.dist v w<GOAL>G.dist u w ≤ (p.append q).length
<GOAL>(abscissaOfAbsConv fun n => ↑(ζ n)) = 1
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<GOAL>toIocMod hp a b = c ↔ c ∈ Set.Ioc a (a + p) ∧ ∃ z, b = c + z • p
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<GOAL>(c ∈ Set.Ioc a (a + p) ∧ ∃ z, b = c + z • p) → toIocMod hp a b = c
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<GOAL>(c ∈ Set.Ioc a (a + p) ∧ ∃ z, b - z • p = c) → toIocMod hp a b = c
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>n✝ n : ℤ<VAR>hc : b - n • p ∈ Set.Ioc a (a + p)<GOAL>toIocMod hp a b = b - n • p
<VAR>ι : Type u_1<VAR>X : ι → Type u_2<VAR>inst✝ : (i : ι) → TopologicalSpace (X i)<VAR>as bs cs : (i : ι) → X i<VAR>γ₀ : (i : ι) → Homotopic.Quotient (as i) (bs i)<VAR>γ₁ : (i : ι) → Homotopic.Quotient (bs i) (cs i)<GOAL>pi γ₀ ⬝ pi γ₁ = pi fun i => γ₀ i ⬝ γ₁ i
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>H : s.Nonempty<VAR>x : α<GOAL>s.min = ↑(s.min' H)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>H : s.Nonempty<VAR>x : α<GOAL>s.inf WithTop.some = s.inf (WithTop.some ∘ fun x => x)
<VAR>m n : ℕ<GOAL>0 < m → 0 < n → 0 < m.lcm n
<VAR>m n : ℕ<GOAL>m ≠ 0 → n ≠ 0 → m.lcm n ≠ 0