ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Semiring k<VAR>inst✝¹ : DecidableEq G<VAR>inst✝ : Mul G<VAR>f g : MonoidAlgebra k G<VAR>x x✝¹ : G<VAR>x✝ : k<GOAL>(sum g fun a₁ b => (single (x✝¹ * a₁) (x✝ * b)) x) = sum g fun a₂ b₂ => if x✝¹ * a₂ = x then x✝ * b₂ else 0
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Semiring k<VAR>inst✝¹ : DecidableEq G<VAR>inst✝ : Mul G<VAR>f g : MonoidAlgebra k G<VAR>x x✝³ : G<VAR>x✝² : k<VAR>x✝¹ : G<VAR>x✝ : k<GOAL>(single (x✝³ * x✝¹) (x✝² * x✝)) x = if x✝³ * x✝¹ = x then x✝² * x✝ else 0
<VAR>S : Type u'<VAR>T : Type u''<VAR>R : Type u<VAR>M : Type v<VAR>inst✝¹ : Monoid R<VAR>inst✝ : MulAction R M<VAR>p : SubMulAction R M<VAR>x m : ↥p<GOAL>x ∈ MulAction.orbit R m ↔ ↑x ∈ MulAction.orbit R ↑m
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s : Cycle α<VAR>hs : s.Nodup<VAR>x : α<VAR>hx : x ∈ s<GOAL>s.prev hs x hx ∈ s
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s : Cycle α<VAR>hs : s.Nodup<VAR>x : α<VAR>hx : x ∈ s<GOAL>s.reverse.next ⋯ x ⋯ ∈ s.reverse
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>i : D ⥤ C<VAR>inst✝ : Reflective i<VAR>X Y : D<VAR>f : X ⟶ Y<GOAL>f ≫ inv ((reflectorAdjunction i).counit.app Y) = inv ((reflectorAdjunction i).counit.app X) ≫ (reflector i).map (i.map f)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>i : D ⥤ C<VAR>inst✝ : Reflective i<VAR>X Y : D<VAR>f : X ⟶ Y<GOAL>(reflectorAdjunction i).counit.app X ≫ f = (reflector i).map (i.map f) ≫ (reflectorAdjunction i).counit.app Y
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>i : D ⥤ C<VAR>inst✝ : Reflective i<VAR>X Y : i.EssImageSubcategory<VAR>f : X ⟶ Y<GOAL>((i.essImageInclusion ⋙ reflector i) ⋙ i.toEssImage).map f ≫ (equivEssImageOfReflective_counitIso_app Y).hom = (equivEssImageOfReflective_counitIso_app X).hom ≫ (𝟭 i.EssImageSubcategory).map f
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>i : D ⥤ C<VAR>inst✝ : Reflective i<VAR>X Y : i.EssImageSubcategory<VAR>f : X ⟶ Y<GOAL>i.essImageInclusion.map (((i.essImageInclusion ⋙ reflector i) ⋙ i.toEssImage).map f ≫ (equivEssImageOfReflective_counitIso_app Y).hom) = i.essImageInclusion.map ((equivEssImageOfReflective_counitIso_app X).hom ≫ (𝟭 i.EssImageSubcategory).map f)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>i : D ⥤ C<VAR>inst✝ : Reflective i<VAR>X Y : i.EssImageSubcategory<VAR>f : X ⟶ Y<VAR>h : (reflectorAdjunction i).unit.app X.obj ≫ (reflector i ⋙ i).map f = (𝟭 C).map f ≫ (reflectorAdjunction i).unit.app Y.obj<GOAL>i.essImageInclusion.map (((i.essImageInclusion ⋙ reflector i) ⋙ i.toEssImage).map f ≫ (equivEssImageOfReflective_counitIso_app Y).hom) = i.essImageInclusion.map ((equivEssImageOfReflective_counitIso_app X).hom ≫ (𝟭 i.EssImageSubcategory).map f)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>i : D ⥤ C<VAR>inst✝ : Reflective i<VAR>X Y : i.EssImageSubcategory<VAR>f : X ⟶ Y<VAR>h : (reflectorAdjunction i).unit.app X.obj ≫ (reflector i ⋙ i).map f = f ≫ (reflectorAdjunction i).unit.app Y.obj<GOAL>i.essImageInclusion.map (((i.essImageInclusion ⋙ reflector i) ⋙ i.toEssImage).map f ≫ (equivEssImageOfReflective_counitIso_app Y).hom) = i.essImageInclusion.map ((equivEssImageOfReflective_counitIso_app X).hom ≫ (𝟭 i.EssImageSubcategory).map f)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>i : D ⥤ C<VAR>inst✝ : Reflective i<VAR>X : D<GOAL>i.toEssImage.map ((NatIso.ofComponents (fun X => (asIso ((reflectorAdjunction i).counit.app X)).symm) ⋯).hom.app X) ≫ (NatIso.ofComponents equivEssImageOfReflective_counitIso_app ⋯).hom.app (i.toEssImage.obj X) = 𝟙 (i.toEssImage.obj X)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>i : D ⥤ C<VAR>inst✝ : Reflective i<VAR>X : D<GOAL>i.essImageInclusion.map (i.toEssImage.map ((NatIso.ofComponents (fun X => (asIso ((reflectorAdjunction i).counit.app X)).symm) ⋯).hom.app X) ≫ (NatIso.ofComponents equivEssImageOfReflective_counitIso_app ⋯).hom.app (i.toEssImage.obj X)) = i.essImageInclusion.map (𝟙 (i.toEssImage.obj X))
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>i : D ⥤ C<VAR>inst✝ : Reflective i<VAR>X : D<GOAL>i.essImageInclusion.map (i.toEssImage.map ((NatIso.ofComponents (fun X => (asIso ((reflectorAdjunction i).counit.app X)).symm) ⋯).hom.app X)) ≫ inv ((reflectorAdjunction i).unit.app ((𝟭 i.EssImageSubcategory).obj (i.toEssImage.obj X)).obj) = i.essImageInclusion.map (𝟙 (i.toEssImage.obj X))
<VAR>a b c x : ℕ<GOAL>x ∈ Ico a.succ b.succ ↔ x ∈ Ioc a b
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s✝ : Set α<VAR>x y z : α<VAR>s : ℕ → Set α<VAR>h0 : IsComplete (s 0)<VAR>hs : ∀ (n : ℕ), IsClosed (s n)<VAR>h's : ∀ (n : ℕ), IsBounded (s n)<VAR>h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty<VAR>h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)<VAR>u : ℕ → α := fun N => ⋯.some<GOAL>(⋂ n, s n).Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s✝ : Set α<VAR>x y z : α<VAR>s : ℕ → Set α<VAR>h0 : IsComplete (s 0)<VAR>hs : ∀ (n : ℕ), IsClosed (s n)<VAR>h's : ∀ (n : ℕ), IsBounded (s n)<VAR>h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty<VAR>h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)<VAR>u : ℕ → α := fun N => ⋯.some<VAR>I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n<GOAL>(⋂ n, s n).Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s✝ : Set α<VAR>x y z : α<VAR>s : ℕ → Set α<VAR>h0 : IsComplete (s 0)<VAR>hs : ∀ (n : ℕ), IsClosed (s n)<VAR>h's : ∀ (n : ℕ), IsBounded (s n)<VAR>h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty<VAR>h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)<VAR>u : ℕ → α := fun N => ⋯.some<VAR>I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n<VAR>this : CauchySeq u<GOAL>(⋂ n, s n).Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s✝ : Set α<VAR>x✝ y z : α<VAR>s : ℕ → Set α<VAR>h0 : IsComplete (s 0)<VAR>hs : ∀ (n : ℕ), IsClosed (s n)<VAR>h's : ∀ (n : ℕ), IsBounded (s n)<VAR>h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty<VAR>h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)<VAR>u : ℕ → α := fun N => ⋯.some<VAR>I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n<VAR>this : CauchySeq u<VAR>x : α<VAR>xlim : Tendsto (fun n => u n) atTop (𝓝 x)<GOAL>(⋂ n, s n).Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s✝ : Set α<VAR>x✝ y z : α<VAR>s : ℕ → Set α<VAR>h0 : IsComplete (s 0)<VAR>hs : ∀ (n : ℕ), IsClosed (s n)<VAR>h's : ∀ (n : ℕ), IsBounded (s n)<VAR>h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty<VAR>h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)<VAR>u : ℕ → α := fun N => ⋯.some<VAR>I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n<VAR>this : CauchySeq u<VAR>x : α<VAR>xlim : Tendsto (fun n => u n) atTop (𝓝 x)<VAR>n : ℕ<GOAL>x ∈ s n
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s✝ : Set α<VAR>x✝ y z : α<VAR>s : ℕ → Set α<VAR>h0 : IsComplete (s 0)<VAR>hs : ∀ (n : ℕ), IsClosed (s n)<VAR>h's : ∀ (n : ℕ), IsBounded (s n)<VAR>h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty<VAR>h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)<VAR>u : ℕ → α := fun N => ⋯.some<VAR>I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n<VAR>this : CauchySeq u<VAR>x : α<VAR>xlim : Tendsto (fun n => u n) atTop (𝓝 x)<VAR>n : ℕ<GOAL>∀ᶠ (x : ℕ) in atTop, u x ∈ s n
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s✝ : Set α<VAR>x✝ y z : α<VAR>s : ℕ → Set α<VAR>h0 : IsComplete (s 0)<VAR>hs : ∀ (n : ℕ), IsClosed (s n)<VAR>h's : ∀ (n : ℕ), IsBounded (s n)<VAR>h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty<VAR>h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)<VAR>u : ℕ → α := fun N => ⋯.some<VAR>I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n<VAR>this : CauchySeq u<VAR>x : α<VAR>xlim : Tendsto (fun n => u n) atTop (𝓝 x)<VAR>n p : ℕ<VAR>hp : p ∈ Ici n<GOAL>u p ∈ s n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b b₁✝ b₂✝ : β<VAR>γ : Type u_3<VAR>inst✝⁸ : Zero α<VAR>inst✝⁷ : Preorder α<VAR>inst✝⁶ : Zero β<VAR>inst✝⁵ : Preorder β<VAR>inst✝⁴ : Zero γ<VAR>inst✝³ : Preorder γ<VAR>inst✝² : SMul α β<VAR>inst✝¹ : SMul α γ<VAR>f : β → γ<VAR>inst✝ : PosSMulReflectLE α γ<VAR>hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂<VAR>smul : ∀ (a : α) (b : β), f (a • b) = a • f b<VAR>a : α<VAR>ha : 0 < a<VAR>b₁ b₂ : β<VAR>h : a • b₁ ≤ a • b₂<GOAL>a • f b₁ ≤ a • f b₂
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a b : α<VAR>x✝ : ℤ<GOAL>x✝ ∈ Int.cast ⁻¹' Icc a b ↔ x✝ ∈ Icc ⌈a⌉ ⌊b⌋
<VAR>R S Rₘ Sₘ : Type u<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : CommRing Rₘ<VAR>inst✝¹² : CommRing Sₘ<VAR>M : Submonoid R<VAR>inst✝¹¹ : Algebra R S<VAR>inst✝¹⁰ : Algebra R Sₘ<VAR>inst✝⁹ : Algebra S Sₘ<VAR>inst✝⁸ : Algebra R Rₘ<VAR>inst✝⁷ : Algebra Rₘ Sₘ<VAR>inst✝⁶ : IsScalarTower R Rₘ Sₘ<VAR>inst✝⁵ : IsScalarTower R S Sₘ<VAR>inst✝⁴ : IsLocalization M Rₘ<VAR>inst✝³ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ<VAR>inst✝² : FormallySmooth R Sₘ<VAR>Q : Type u<VAR>inst✝¹ : CommRing Q<VAR>inst✝ : Algebra Rₘ Q<VAR>I : Ideal Q<VAR>e : I ^ 2 = ⊥<VAR>f : Sₘ →ₐ[Rₘ] Q ⧸ I<VAR>this : Algebra R Q := ((algebraMap Rₘ Q).comp (algebraMap R Rₘ)).toAlgebra<GOAL>∃ a, (Ideal.Quotient.mkₐ Rₘ I).comp a = f
<VAR>R S Rₘ Sₘ : Type u<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : CommRing Rₘ<VAR>inst✝¹² : CommRing Sₘ<VAR>M : Submonoid R<VAR>inst✝¹¹ : Algebra R S<VAR>inst✝¹⁰ : Algebra R Sₘ<VAR>inst✝⁹ : Algebra S Sₘ<VAR>inst✝⁸ : Algebra R Rₘ<VAR>inst✝⁷ : Algebra Rₘ Sₘ<VAR>inst✝⁶ : IsScalarTower R Rₘ Sₘ<VAR>inst✝⁵ : IsScalarTower R S Sₘ<VAR>inst✝⁴ : IsLocalization M Rₘ<VAR>inst✝³ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ<VAR>inst✝² : FormallySmooth R Sₘ<VAR>Q : Type u<VAR>inst✝¹ : CommRing Q<VAR>inst✝ : Algebra Rₘ Q<VAR>I : Ideal Q<VAR>e : I ^ 2 = ⊥<VAR>f : Sₘ →ₐ[Rₘ] Q ⧸ I<VAR>this✝ : Algebra R Q := ((algebraMap Rₘ Q).comp (algebraMap R Rₘ)).toAlgebra<VAR>this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl<GOAL>∃ a, (Ideal.Quotient.mkₐ Rₘ I).comp a = f
<VAR>R S Rₘ Sₘ : Type u<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : CommRing Rₘ<VAR>inst✝¹² : CommRing Sₘ<VAR>M : Submonoid R<VAR>inst✝¹¹ : Algebra R S<VAR>inst✝¹⁰ : Algebra R Sₘ<VAR>inst✝⁹ : Algebra S Sₘ<VAR>inst✝⁸ : Algebra R Rₘ<VAR>inst✝⁷ : Algebra Rₘ Sₘ<VAR>inst✝⁶ : IsScalarTower R Rₘ Sₘ<VAR>inst✝⁵ : IsScalarTower R S Sₘ<VAR>inst✝⁴ : IsLocalization M Rₘ<VAR>inst✝³ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ<VAR>inst✝² : FormallySmooth R Sₘ<VAR>Q : Type u<VAR>inst✝¹ : CommRing Q<VAR>inst✝ : Algebra Rₘ Q<VAR>I : Ideal Q<VAR>e : I ^ 2 = ⊥<VAR>f✝ : Sₘ →ₐ[Rₘ] Q ⧸ I<VAR>this✝ : Algebra R Q := ((algebraMap Rₘ Q).comp (algebraMap R Rₘ)).toAlgebra<VAR>this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl<VAR>f : Sₘ →ₐ[Rₘ] Q := let __src := lift I ⋯ (AlgHom.restrictScalars R f✝); { toRingHom := __src.toRingHom, commutes' := ⋯ }<GOAL>∃ a, (Ideal.Quotient.mkₐ Rₘ I).comp a = f✝
<VAR>R S Rₘ Sₘ : Type u<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : CommRing Rₘ<VAR>inst✝¹² : CommRing Sₘ<VAR>M : Submonoid R<VAR>inst✝¹¹ : Algebra R S<VAR>inst✝¹⁰ : Algebra R Sₘ<VAR>inst✝⁹ : Algebra S Sₘ<VAR>inst✝⁸ : Algebra R Rₘ<VAR>inst✝⁷ : Algebra Rₘ Sₘ<VAR>inst✝⁶ : IsScalarTower R Rₘ Sₘ<VAR>inst✝⁵ : IsScalarTower R S Sₘ<VAR>inst✝⁴ : IsLocalization M Rₘ<VAR>inst✝³ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ<VAR>inst✝² : FormallySmooth R Sₘ<VAR>Q : Type u<VAR>inst✝¹ : CommRing Q<VAR>inst✝ : Algebra Rₘ Q<VAR>I : Ideal Q<VAR>e : I ^ 2 = ⊥<VAR>f✝ : Sₘ →ₐ[Rₘ] Q ⧸ I<VAR>this✝ : Algebra R Q := ((algebraMap Rₘ Q).comp (algebraMap R Rₘ)).toAlgebra<VAR>this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl<VAR>f : Sₘ →ₐ[Rₘ] Q := let __src := lift I ⋯ (AlgHom.restrictScalars R f✝); { toRingHom := __src.toRingHom, commutes' := ⋯ }<GOAL>(Ideal.Quotient.mkₐ Rₘ I).comp f = f✝
<VAR>n : Nat<GOAL>mkRat 0 n = 0
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α✝<VAR>α : Type u_3<VAR>inst✝² : MeasurableSpace α<VAR>A : Set α<VAR>ι : Type u_4<VAR>L : Filter ι<VAR>inst✝¹ : L.IsCountablyGenerated<VAR>As : ι → Set α<VAR>inst✝ : L.NeBot<VAR>μ : Measure α<VAR>As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ<VAR>h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A<GOAL>NullMeasurableSet A μ
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α✝<VAR>α : Type u_3<VAR>inst✝² : MeasurableSpace α<VAR>A : Set α<VAR>ι : Type u_4<VAR>L : Filter ι<VAR>inst✝¹ : L.IsCountablyGenerated<VAR>As : ι → Set α<VAR>inst✝ : L.NeBot<VAR>μ : Measure α<VAR>h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A<VAR>As_mble : ∀ (i : ι), AEMeasurable ((As i).indicator fun x => 1) μ<GOAL>AEMeasurable (A.indicator fun x => 1) μ
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α✝<VAR>α : Type u_3<VAR>inst✝² : MeasurableSpace α<VAR>A : Set α<VAR>ι : Type u_4<VAR>L : Filter ι<VAR>inst✝¹ : L.IsCountablyGenerated<VAR>As : ι → Set α<VAR>inst✝ : L.NeBot<VAR>μ : Measure α<VAR>h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A<VAR>As_mble : ∀ (i : ι), AEMeasurable ((As i).indicator fun x => 1) μ<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun n => (As n).indicator (fun x => 1) x) L (𝓝 (A.indicator (fun x => 1) x))
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : SeminormedAddCommGroup β<VAR>l : Filter α<VAR>f g : α → β<VAR>hf : l.BoundedAtFilter f<VAR>hg : l.BoundedAtFilter g<GOAL>l.BoundedAtFilter (f + g)
<VAR>α : Type u_1<VAR>P : α → Bool<VAR>l : List α<GOAL>splitOnP P l = splitOnPTR P l
<VAR>α : Type u_1<VAR>P : α → Bool<VAR>l : List α<GOAL>splitOnP P l = splitOnPTR.go P l #[] #[]
<VAR>α : Type u_1<VAR>P : α → Bool<VAR>l : List α<GOAL>∀ (xs : List α) (acc : Array α) (r : Array (List α)), splitOnPTR.go P xs acc r = r.data ++ splitOnP.go P xs acc.data.reverse
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimits C<VAR>ι : Type v<VAR>F : Discrete ι ⥤ SheafedSpace C<VAR>inst✝ : HasColimit F<VAR>i : Discrete ι<GOAL>OpenEmbedding ⇑(colimit.ι F i).base
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimits C<VAR>ι : Type v<VAR>F : Discrete ι ⥤ SheafedSpace C<VAR>inst✝ : HasColimit F<VAR>i : Discrete ι<GOAL>OpenEmbedding ⇑(colimit.ι (F ⋙ forget C) i ≫ (preservesColimitIso (forget C) F).inv)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimits C<VAR>ι : Type v<VAR>F : Discrete ι ⥤ SheafedSpace C<VAR>inst✝ : HasColimit F<VAR>i : Discrete ι<VAR>this : colimit.ι (F ⋙ forget C) i ≫ (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom = Discrete.natIsoFunctor.hom.app i ≫ colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i<GOAL>OpenEmbedding ⇑(colimit.ι (F ⋙ forget C) i ≫ (preservesColimitIso (forget C) F).inv)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimits C<VAR>ι : Type v<VAR>F : Discrete ι ⥤ SheafedSpace C<VAR>inst✝ : HasColimit F<VAR>i : Discrete ι<VAR>this : colimit.ι (F ⋙ forget C) i = (Discrete.natIsoFunctor.hom.app i ≫ colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i) ≫ (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv<GOAL>OpenEmbedding ⇑(colimit.ι (F ⋙ forget C) i ≫ (preservesColimitIso (forget C) F).inv)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimits C<VAR>ι : Type v<VAR>F : Discrete ι ⥤ SheafedSpace C<VAR>inst✝ : HasColimit F<VAR>i : Discrete ι<VAR>this : colimit.ι (F ⋙ forget C) i = (Discrete.natIsoFunctor.hom.app i ≫ colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i) ≫ (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv<GOAL>OpenEmbedding ⇑(((Discrete.natIsoFunctor.hom.app i ≫ colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i) ≫ (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv) ≫ (preservesColimitIso (forget C) F).inv)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimits C<VAR>ι : Type v<VAR>F : Discrete ι ⥤ SheafedSpace C<VAR>inst✝ : HasColimit F<VAR>i : Discrete ι<VAR>this✝ : colimit.ι (F ⋙ forget C) i = (Discrete.natIsoFunctor.hom.app i ≫ colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i) ≫ (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv<VAR>this : colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := i.as } ≫ (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom = TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) i.as<GOAL>OpenEmbedding ⇑(((Discrete.natIsoFunctor.hom.app i ≫ colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i) ≫ (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv) ≫ (preservesColimitIso (forget C) F).inv)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimits C<VAR>ι : Type v<VAR>F : Discrete ι ⥤ SheafedSpace C<VAR>inst✝ : HasColimit F<VAR>i : Discrete ι<VAR>this✝ : colimit.ι (F ⋙ forget C) i = (Discrete.natIsoFunctor.hom.app i ≫ colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i) ≫ (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv<VAR>this : colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := i.as } = TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) i.as ≫ (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).inv<GOAL>OpenEmbedding ⇑(((Discrete.natIsoFunctor.hom.app i ≫ colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i) ≫ (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv) ≫ (preservesColimitIso (forget C) F).inv)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimits C<VAR>ι : Type v<VAR>F : Discrete ι ⥤ SheafedSpace C<VAR>inst✝ : HasColimit F<VAR>as✝ : ι<VAR>this✝ : colimit.ι (F ⋙ forget C) { as := as✝ } = (Discrete.natIsoFunctor.hom.app { as := as✝ } ≫ colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := as✝ }) ≫ (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv<VAR>this : colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := { as := as✝ }.as } = TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) { as := as✝ }.as ≫ (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).inv<GOAL>OpenEmbedding ⇑(((Discrete.natIsoFunctor.hom.app { as := as✝ } ≫ colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := as✝ }) ≫ (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv) ≫ (preservesColimitIso (forget C) F).inv)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimits C<VAR>ι : Type v<VAR>F : Discrete ι ⥤ SheafedSpace C<VAR>inst✝ : HasColimit F<VAR>as✝ : ι<VAR>this✝ : colimit.ι (F ⋙ forget C) { as := as✝ } = (Discrete.natIsoFunctor.hom.app { as := as✝ } ≫ colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := as✝ }) ≫ (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv<VAR>this : colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := { as := as✝ }.as } = TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) { as := as✝ }.as ≫ (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).inv<GOAL>OpenEmbedding ⇑((((Discrete.natIsoFunctor.hom.app { as := as✝ } ≫ TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) { as := as✝ }.as) ≫ (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).inv) ≫ (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv) ≫ (preservesColimitIso (forget C) F).inv)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimits C<VAR>ι : Type v<VAR>F : Discrete ι ⥤ SheafedSpace C<VAR>inst✝ : HasColimit F<VAR>as✝ : ι<VAR>this✝ : colimit.ι (F ⋙ forget C) { as := as✝ } = (Discrete.natIsoFunctor.hom.app { as := as✝ } ≫ colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := as✝ }) ≫ (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv<VAR>this : colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := { as := as✝ }.as } = TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) { as := as✝ }.as ≫ (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).inv<GOAL>OpenEmbedding ⇑(TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) { as := as✝ }.as)
<VAR>a : Ordinal.{u_1}<GOAL>(succ a.card).ord.card.ord = (succ a.card).ord
<VAR>G : Type u<VAR>M : Type v<VAR>α : Type w<VAR>s : Set α<VAR>m : MeasurableSpace α<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G α<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : MeasurableSMul G α<VAR>c : G<VAR>μ : Measure α<VAR>inst✝³ : SMulInvariantMeasure G α μ<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : ContinuousConstSMul G α<VAR>inst✝ : MulAction.IsMinimal G α<VAR>K U : Set α<VAR>hK : IsCompact K<VAR>hμK : μ K ≠ 0<VAR>hU : IsOpen U<VAR>hne : U.Nonempty<VAR>t : Finset G<VAR>ht : K ⊆ ⋃ g ∈ t, g • U<VAR>hμU : μ U = 0<VAR>x✝¹ : G<VAR>x✝ : x✝¹ ∈ ↑t<GOAL>μ (x✝¹ • U) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>s : Multiset α<GOAL>(map f s.dedup).dedup = (map f s).dedup
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f✝ : α → ℕ<VAR>a b : α<VAR>n : ℕ<VAR>inst✝ : DecidableEq α<VAR>ha : a ∉ s<VAR>f : α → ℕ<GOAL>multinomial (insert a s) f = (f a + ∑ i ∈ s, f i).choose (f a) * multinomial s f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>ι : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure X<VAR>l : Filter X<VAR>inst✝ : l.IsMeasurablyGenerated<VAR>f : X → E<VAR>b : E<VAR>h : Tendsto f (l ⊓ ae μ) (𝓝 b)<VAR>hfm : StronglyMeasurableAtFilter f l μ<VAR>hμ : μ.FiniteAtFilter l<VAR>s : ι → Set X<VAR>li : Filter ι<VAR>hs : Tendsto s li l.smallSets<VAR>m : optParam (ι → ℝ) fun i => (μ (s i)).toReal<VAR>hsμ : autoParam ((fun i => (μ (s i)).toReal) =ᶠ[li] m) _auto✝<GOAL>(fun i => ∫ (x : X) in s i, f x ∂μ - m i • b) =o[li] m
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>ι : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure X<VAR>l : Filter X<VAR>inst✝ : l.IsMeasurablyGenerated<VAR>f : X → E<VAR>b : E<VAR>h : Tendsto f (l ⊓ ae μ) (𝓝 b)<VAR>hfm : StronglyMeasurableAtFilter f l μ<VAR>hμ : μ.FiniteAtFilter l<VAR>s : ι → Set X<VAR>li : Filter ι<VAR>hs : Tendsto s li l.smallSets<VAR>m : optParam (ι → ℝ) fun i => (μ (s i)).toReal<VAR>hsμ : autoParam ((fun i => (μ (s i)).toReal) =ᶠ[li] m) _auto✝<GOAL>(fun s => ∫ (x : X) in s, f x ∂μ - (μ s).toReal • b) =o[l.smallSets] fun s => (μ s).toReal
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>ι : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure X<VAR>l : Filter X<VAR>inst✝ : l.IsMeasurablyGenerated<VAR>f : X → E<VAR>b : E<VAR>h : Tendsto f (l ⊓ ae μ) (𝓝 b)<VAR>hfm : StronglyMeasurableAtFilter f l μ<VAR>hμ : μ.FiniteAtFilter l<VAR>s : ι → Set X<VAR>li : Filter ι<VAR>hs : Tendsto s li l.smallSets<VAR>m : optParam (ι → ℝ) fun i => (μ (s i)).toReal<VAR>hsμ : autoParam ((fun i => (μ (s i)).toReal) =ᶠ[li] m) _auto✝<VAR>ε : ℝ<VAR>ε₀ : 0 < ε<GOAL>∀ᶠ (x : Set X) in l.smallSets, ‖∫ (x : X) in x, f x ∂μ - (μ x).toReal • b‖ ≤ ε * ‖(μ x).toReal‖