ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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✝ : IsSFiniteKernel κ<VAR>f g : α → β → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>hg : Measurable (Function.uncurry g)<VAR>a : α<VAR>s✝ : Set β<VAR>a✝ : MeasurableSet s✝<GOAL>((κ.withDensity (f + g)) a) s✝ = ((κ.withDensity f + κ.withDensity g) 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✝ : IsSFiniteKernel κ<VAR>f g : α → β → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>hg : Measurable (Function.uncurry g)<VAR>a : α<VAR>s✝ : Set β<VAR>a✝ : MeasurableSet s✝<GOAL>Measurable (g a)
<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✝ : IsSFiniteKernel κ<VAR>f g : α → β → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>hg : Measurable (Function.uncurry g)<VAR>a : α<VAR>s✝ : Set β<VAR>a✝ : MeasurableSet s✝<GOAL>Measurable (Function.uncurry (f + g))
<VAR>C : Type u<VAR>inst✝¹² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝¹¹ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝¹⁰ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁸ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝⁷ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝⁶ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝⁵ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>inst✝⁴ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P : Cᵒᵖ ⥤ D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : PreservesLimits (forget D)<VAR>inst✝¹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>inst✝ : (forget D).ReflectsIsomorphisms<GOAL>(J.sheafifyCompIso F P).inv = J.sheafifyLift (whiskerRight (J.toSheafify P) F) ⋯
<VAR>C : Type u<VAR>inst✝¹² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝¹¹ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝¹⁰ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁸ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝⁷ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝⁶ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝⁵ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>inst✝⁴ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P : Cᵒᵖ ⥤ D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : PreservesLimits (forget D)<VAR>inst✝¹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>inst✝ : (forget D).ReflectsIsomorphisms<GOAL>J.toSheafify (P ⋙ F) ≫ (J.sheafifyCompIso F P).inv = whiskerRight (J.toSheafify P) F
<VAR>C : Type u<VAR>inst✝¹² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝¹¹ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝¹⁰ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁸ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝⁷ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝⁶ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝⁵ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>inst✝⁴ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P : Cᵒᵖ ⥤ D<VAR>inst✝³ : ConcreteCategory D<VAR>inst✝² : PreservesLimits (forget D)<VAR>inst✝¹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>inst✝ : (forget D).ReflectsIsomorphisms<GOAL>J.toSheafify (P ⋙ F) = whiskerRight (J.toSheafify P) F ≫ (J.sheafifyCompIso F P).hom
<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>𝕝 : Type u_7<VAR>inst✝³ : NontriviallyNormedField 𝕝<VAR>inst✝² : NormedAlgebra 𝕜 𝕝<VAR>A : Type u_8<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>e : E<VAR>f : E → F<VAR>g : E → G<VAR>w✝¹ : FormalMultilinearSeries 𝕜 E F<VAR>hf : HasFPowerSeriesAt f w✝¹ e<VAR>w✝ : FormalMultilinearSeries 𝕜 E G<VAR>hg : HasFPowerSeriesAt g w✝ e<GOAL>AnalyticAt 𝕜 (fun x => (f x, g x)) e
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t : Set α<GOAL>IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ball x ε ⊆ s
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ_[p] ⇑padicNormE<VAR>ε : ℚ<VAR>hε : 0 < ε<GOAL>∃ N, ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ_[p] ⇑padicNormE<VAR>ε : ℚ<VAR>hε : 0 < ε<VAR>N : ℕ<VAR>hN : 1 / ε < ↑N<VAR>i : ℕ<VAR>hi : i ≥ N<GOAL>padicNormE (↑f i - ↑(limSeq f i)) < ε
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ_[p] ⇑padicNormE<VAR>ε : ℚ<VAR>hε : 0 < ε<VAR>N : ℕ<VAR>hN : 1 / ε < ↑N<VAR>i : ℕ<VAR>hi : i ≥ N<VAR>h : padicNormE (↑f i - ↑(Classical.choose ⋯)) < 1 / (↑i + 1)<GOAL>padicNormE (↑f i - ↑(limSeq f i)) < ε
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ_[p] ⇑padicNormE<VAR>ε : ℚ<VAR>hε : 0 < ε<VAR>N : ℕ<VAR>hN : 1 / ε < ↑N<VAR>i : ℕ<VAR>hi : i ≥ N<VAR>h : padicNormE (↑f i - ↑(Classical.choose ⋯)) < 1 / (↑i + 1)<GOAL>1 ≤ (↑i + 1) * ε
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ_[p] ⇑padicNormE<VAR>ε : ℚ<VAR>hε : 0 < ε<VAR>N : ℕ<VAR>hN : 1 / ε < ↑N<VAR>i : ℕ<VAR>hi : i ≥ N<VAR>h : padicNormE (↑f i - ↑(Classical.choose ⋯)) < 1 / (↑i + 1)<GOAL>1 ≤ ↑i * ε + 1 * ε
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ_[p] ⇑padicNormE<VAR>ε : ℚ<VAR>hε : 0 < ε<VAR>N : ℕ<VAR>hN : 1 / ε < ↑N<VAR>i : ℕ<VAR>hi : i ≥ N<VAR>h : padicNormE (↑f i - ↑(Classical.choose ⋯)) < 1 / (↑i + 1)<GOAL>1 ≤ ↑i * ε
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ_[p] ⇑padicNormE<VAR>ε : ℚ<VAR>hε : 0 < ε<VAR>N : ℕ<VAR>hN : 1 / ε < ↑N<VAR>i : ℕ<VAR>hi : i ≥ N<VAR>h : padicNormE (↑f i - ↑(Classical.choose ⋯)) < 1 / (↑i + 1)<GOAL>0 ≤ 1 * ε
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>h : MeasurableSet s<GOAL>(μ.restrict s).toOuterMeasure = (OuterMeasure.restrict s) μ.toOuterMeasure
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a : Ordinal.{u}<GOAL>a.cof.ord.cof = a.cof
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < a.cof.ord → Ordinal.{u}<VAR>hf : a.IsFundamentalSequence a.cof.ord f<GOAL>a.cof.ord.cof = a.cof
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < a.cof.ord → Ordinal.{u}<VAR>hf : a.IsFundamentalSequence a.cof.ord f<VAR>g : (b : Ordinal.{u}) → b < a.cof.ord.cof.ord → Ordinal.{u}<VAR>hg : a.cof.ord.IsFundamentalSequence a.cof.ord.cof.ord g<GOAL>a.cof.ord.cof = a.cof
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{u₂, u₁} C<VAR>inst✝³ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝² : FiberFunctor F<VAR>X A : C<VAR>inst✝¹ : IsConnected A<VAR>u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X<VAR>inst✝ : Mono u<VAR>a : ↑(F.obj A)<VAR>h : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X<VAR>b : ↑(F.obj A)<GOAL>∃ f, F.map f.hom b = a
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{u₂, u₁} C<VAR>inst✝³ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝² : FiberFunctor F<VAR>X A : C<VAR>inst✝¹ : IsConnected A<VAR>u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X<VAR>inst✝ : Mono u<VAR>a : ↑(F.obj A)<VAR>h : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X<VAR>b : ↑(F.obj A)<GOAL>F.map u b = F.map (CategoryTheory.PreGaloisCategory.selfProdPermIncl h b) a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : Filter X<VAR>s t s₁ s₂ t₁ t₂ : Set X<VAR>x : X<GOAL>Disjoint (𝓟 s) (𝓝ˢ t) ↔ Disjoint (closure s) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>inst✝² : One M<VAR>inst✝¹ : One N<VAR>inst✝ : One P<VAR>f : α → M<GOAL>(mulSupport f).Nonempty ↔ f ≠ 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Ring S<VAR>inst✝⁷ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : Algebra A B<VAR>K : Type u_6<VAR>inst✝² : Field K<VAR>S' : Type u_7<VAR>inst✝¹ : CommRing S'<VAR>inst✝ : Algebra R S'<VAR>pb : PowerBasis R S<VAR>e : S ≃ₐ[R] S'<VAR>i : Fin pb.dim<GOAL>(pb.basis.map e.toLinearEquiv) i = e pb.gen ^ ↑i
<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>inst✝ : CommMonoid α<VAR>n : ℕ<VAR>f : ℕ → α<VAR>hn : ¬n = 0<GOAL>∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f
<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>inst✝ : CommMonoid α<VAR>n : ℕ<VAR>f : ℕ → α<VAR>hn : ¬n = 0<GOAL>∏ x ∈ image (HDiv.hDiv n) n.divisors, f x = n.divisors.prod f
<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>inst✝ : CommMonoid α<VAR>n : ℕ<VAR>f : ℕ → α<VAR>hn : ¬n = 0<GOAL>∀ x ∈ n.divisors, ∀ y ∈ n.divisors, n / x = n / y → x = y
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁸ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝³ : TopologicalSpace H'<VAR>N : Type u_7<VAR>inst✝² : TopologicalSpace N<VAR>inst✝¹ : ChartedSpace H' N<VAR>J : ModelWithCorners 𝕜 E' H'<VAR>inst✝ : SmoothManifoldWithCorners J N<VAR>x : M<VAR>y : N<GOAL>(I.prod J).boundary (M × N) = univ.prod (J.boundary N) ∪ (I.boundary M).prod univ
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁸ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝³ : TopologicalSpace H'<VAR>N : Type u_7<VAR>inst✝² : TopologicalSpace N<VAR>inst✝¹ : ChartedSpace H' N<VAR>J : ModelWithCorners 𝕜 E' H'<VAR>inst✝ : SmoothManifoldWithCorners J N<VAR>x : M<VAR>y : N<VAR>h : (I.prod J).boundary (M × N) = (I.interior M)ᶜ ×ˢ univ ∪ univ ×ˢ (J.interior N)ᶜ := Trans.trans (Trans.trans (Trans.trans rfl (boundary_eq_complement_interior (I.prod J))) (Eq.mpr (id (congrArg (fun _a => _aᶜ = (I.interior M ×ˢ J.interior N)ᶜ) (interior_prod J))) (Eq.refl (I.interior M ×ˢ J.interior N)ᶜ))) (Eq.mpr (id (congrArg (fun _a => _a = (I.interior M)ᶜ ×ˢ univ ∪ univ ×ˢ (J.interior N)ᶜ) (compl_prod_eq_union (I.interior M) (J.interior N)))) (Eq.refl ((I.interior M)ᶜ ×ˢ univ ∪ univ ×ˢ (J.interior N)ᶜ)))<GOAL>(I.prod J).boundary (M × N) = univ.prod (J.boundary N) ∪ (I.boundary M).prod univ
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁸ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝³ : TopologicalSpace H'<VAR>N : Type u_7<VAR>inst✝² : TopologicalSpace N<VAR>inst✝¹ : ChartedSpace H' N<VAR>J : ModelWithCorners 𝕜 E' H'<VAR>inst✝ : SmoothManifoldWithCorners J N<VAR>x : M<VAR>y : N<VAR>h : (I.prod J).boundary (M × N) = (I.interior M)ᶜ ×ˢ univ ∪ univ ×ˢ (J.interior N)ᶜ := Trans.trans (Trans.trans (Trans.trans rfl (boundary_eq_complement_interior (I.prod J))) (Eq.mpr (id (congrArg (fun _a => _aᶜ = (I.interior M ×ˢ J.interior N)ᶜ) (interior_prod J))) (Eq.refl (I.interior M ×ˢ J.interior N)ᶜ))) (Eq.mpr (id (congrArg (fun _a => _a = (I.interior M)ᶜ ×ˢ univ ∪ univ ×ˢ (J.interior N)ᶜ) (compl_prod_eq_union (I.interior M) (J.interior N)))) (Eq.refl ((I.interior M)ᶜ ×ˢ univ ∪ univ ×ˢ (J.interior N)ᶜ)))<GOAL>univ ×ˢ (J.interior N)ᶜ ∪ (I.interior M)ᶜ ×ˢ univ = univ.prod (J.interior N)ᶜ ∪ (I.interior M)ᶜ.prod univ
<VAR>α : Type u_1<VAR>inst✝ : OrderedRing α<VAR>a : α<GOAL>Pairwise (Disjoint on fun n => Ioc (↑n) (↑n + 1))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>z : ℤ<VAR>n : ℕ<GOAL>constantCoeff (wittZSMul p z n) = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>z : ℤ<VAR>n : ℕ<GOAL>constantCoeff (z • X 0) = 0
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>μ : ι → Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : Set α<VAR>ht : MeasurableSet t<GOAL>((sum μ).restrict s) t = (sum fun i => (μ i).restrict s) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>l : Filter α<VAR>f : α → β<VAR>p : α → Prop<GOAL>EventuallyConst p l ↔ (∀ᶠ (x : α) in l, p x) ∨ ∀ᶠ (x : α) in l, ¬p x
<VAR>r r₁ r₂ : ℝ≥0<VAR>x y : ℝ<GOAL>1 < ↑r ↔ 1 < r
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : PseudoMetricSpace β<VAR>inst✝² : AddMonoid β<VAR>inst✝¹ : BoundedAdd β<VAR>inst✝ : ContinuousAdd β<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<GOAL>⇑(nsmulRec 0 f) = 0 • ⇑f
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : PseudoMetricSpace β<VAR>inst✝² : AddMonoid β<VAR>inst✝¹ : BoundedAdd β<VAR>inst✝ : ContinuousAdd β<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>n : ℕ<GOAL>⇑(nsmulRec (n + 1) f) = (n + 1) • ⇑f
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<GOAL>inl.range ⊔ inr.range = ⊤
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<GOAL>SheafedSpace.forgetToPresheafedSpace.preimage (PresheafedSpace.IsOpenImmersion.isoRestrict f.val).hom ≫ (Y.ofRestrict ⋯).val = f.val
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<GOAL>SheafedSpace.forgetToPresheafedSpace.map (SheafedSpace.forgetToPresheafedSpace.preimage (PresheafedSpace.IsOpenImmersion.isoRestrict f.val).hom ≫ (Y.ofRestrict ⋯).val) = SheafedSpace.forgetToPresheafedSpace.map f.val
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<GOAL>(PresheafedSpace.IsOpenImmersion.isoRestrict f.val).hom ≫ SheafedSpace.forgetToPresheafedSpace.map (Y.ofRestrict ⋯).val = SheafedSpace.forgetToPresheafedSpace.map f.val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>hf : (mulSupport f).Finite<GOAL>∏ᶠ (i : α), f i = ∏ i ∈ hf.toFinset, f i
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<GOAL>H.relindex (K ⊓ L) * K.relindex L = (H ⊓ K).relindex L
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>e : X ≃ₜ Y<VAR>x✝ : LocallyConstant X Z<GOAL>comap e.toContinuousMap (comap e.symm.toContinuousMap x✝) = x✝
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>e : X ≃ₜ Y<VAR>x✝ : LocallyConstant Y Z<GOAL>comap e.symm.toContinuousMap (comap e.toContinuousMap x✝) = x✝
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>a : α<VAR>s : l₁ ⊆ l₂<VAR>x✝ : α<GOAL>x✝ ∈ a :: l₁ → x✝ ∈ a :: l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>a : α<VAR>s : l₁ ⊆ l₂<VAR>x✝ : α<GOAL>x✝ = a ∨ x✝ ∈ l₁ → x✝ = a ∨ x✝ ∈ l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>f : CompleteLatticeHom α α<VAR>a : α<GOAL>f (limsup (fun n => (⇑f)^[n] a) atTop) = limsup (fun n => (⇑f)^[n] a) atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>f : CompleteLatticeHom α α<VAR>a : α<GOAL>⨅ i, f (⨆ i_1, (⇑f)^[i_1 + i] a) = ⨅ n, ⨆ i, (⇑f)^[i + n] a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>f : CompleteLatticeHom α α<VAR>a : α<GOAL>⨅ i, ⨆ i_1, (⇑f)^[i_1 + i.succ] a = ⨅ n, ⨆ i, (⇑f)^[i + n] a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>f : CompleteLatticeHom α α<VAR>a : α<GOAL>⨅ i, ⨆ i_1, (⇑f)^[i_1 + i.succ] a = (⨅ i, ⨅ (_ : 0 < i), ⨆ i_1, (⇑f)^[i_1 + i] a) ⊓ ⨅ i, ⨅ (_ : ¬0 < i), ⨆ i_1, (⇑f)^[i_1 + i] a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>f : CompleteLatticeHom α α<VAR>a : α<GOAL>⨅ i, ⨆ i_1, (⇑f)^[i_1 + i.succ] a ≤ ⨆ i, (⇑f)^[i] a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>f : CompleteLatticeHom α α<VAR>a : α<GOAL>⨆ j, (⇑f)^[j + (0 + 1)] a ≤ ⨆ i, (⇑f)^[i] a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>f : CompleteLatticeHom α α<VAR>a : α<GOAL>∀ (i : ℕ), (⇑f)^[i + 1] a ≤ ⨆ i, (⇑f)^[i] a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u : Set α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : BorelSpace α<VAR>inst✝⁷ : TopologicalSpace β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : BorelSpace β<VAR>inst✝⁴ : MeasurableSpace δ<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : SecondCountableTopology α<VAR>ι : Sort u_5<VAR>inst✝ : Countable ι<VAR>f : ι → δ → α<VAR>hf : ∀ (i : ι), Measurable (f i)<GOAL>MeasurableSet {b | BddAbove (range fun i => f i b)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u : Set α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : BorelSpace α<VAR>inst✝⁷ : TopologicalSpace β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : BorelSpace β<VAR>inst✝⁴ : MeasurableSpace δ<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : SecondCountableTopology α<VAR>ι : Sort u_5<VAR>inst✝ : Countable ι<VAR>f : ι → δ → α<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>hα : IsEmpty α<GOAL>MeasurableSet {b | BddAbove (range fun i => f i b)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u : Set α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : BorelSpace α<VAR>inst✝⁷ : TopologicalSpace β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : BorelSpace β<VAR>inst✝⁴ : MeasurableSpace δ<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : SecondCountableTopology α<VAR>ι : Sort u_5<VAR>inst✝ : Countable ι<VAR>f : ι → δ → α<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>hα : Nonempty α<GOAL>MeasurableSet {b | BddAbove (range fun i => f i b)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u : Set α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : BorelSpace α<VAR>inst✝⁷ : TopologicalSpace β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : BorelSpace β<VAR>inst✝⁴ : MeasurableSpace δ<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : SecondCountableTopology α<VAR>ι : Sort u_5<VAR>inst✝ : Countable ι<VAR>f : ι → δ → α<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>hα : Nonempty α<VAR>A : ∀ (i : ι) (c : α), MeasurableSet {x | f i x ≤ c}<GOAL>MeasurableSet {b | BddAbove (range fun i => f i b)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u : Set α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : BorelSpace α<VAR>inst✝⁷ : TopologicalSpace β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : BorelSpace β<VAR>inst✝⁴ : MeasurableSpace δ<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : SecondCountableTopology α<VAR>ι : Sort u_5<VAR>inst✝ : Countable ι<VAR>f : ι → δ → α<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>hα : Nonempty α<VAR>A : ∀ (i : ι) (c : α), MeasurableSet {x | f i x ≤ c}<VAR>B : ∀ (c : α), MeasurableSet {x | ∀ (i : ι), f i x ≤ c}<GOAL>MeasurableSet {b | BddAbove (range fun i => f i b)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u✝ : Set α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : BorelSpace α<VAR>inst✝⁷ : TopologicalSpace β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : BorelSpace β<VAR>inst✝⁴ : MeasurableSpace δ<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : SecondCountableTopology α<VAR>ι : Sort u_5<VAR>inst✝ : Countable ι<VAR>f : ι → δ → α<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>hα : Nonempty α<VAR>A : ∀ (i : ι) (c : α), MeasurableSet {x | f i x ≤ c}<VAR>B : ∀ (c : α), MeasurableSet {x | ∀ (i : ι), f i x ≤ c}<VAR>u : ℕ → α<VAR>hu : Tendsto u atTop atTop<GOAL>MeasurableSet {b | BddAbove (range fun i => f i b)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u✝ : Set α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : BorelSpace α<VAR>inst✝⁷ : TopologicalSpace β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : BorelSpace β<VAR>inst✝⁴ : MeasurableSpace δ<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : SecondCountableTopology α<VAR>ι : Sort u_5<VAR>inst✝ : Countable ι<VAR>f : ι → δ → α<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>hα : Nonempty α<VAR>A : ∀ (i : ι) (c : α), MeasurableSet {x | f i x ≤ c}<VAR>B : ∀ (c : α), MeasurableSet {x | ∀ (i : ι), f i x ≤ c}<VAR>u : ℕ → α<VAR>hu : Tendsto u atTop atTop<VAR>this : {b | BddAbove (range fun i => f i b)} = {x | ∃ n, ∀ (i : ι), f i x ≤ u n}<GOAL>MeasurableSet {b | BddAbove (range fun i => f i b)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u✝ : Set α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : BorelSpace α<VAR>inst✝⁷ : TopologicalSpace β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : BorelSpace β<VAR>inst✝⁴ : MeasurableSpace δ<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : SecondCountableTopology α<VAR>ι : Sort u_5<VAR>inst✝ : Countable ι<VAR>f : ι → δ → α<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>hα : Nonempty α<VAR>A : ∀ (i : ι) (c : α), MeasurableSet {x | f i x ≤ c}<VAR>B : ∀ (c : α), MeasurableSet {x | ∀ (i : ι), f i x ≤ c}<VAR>u : ℕ → α<VAR>hu : Tendsto u atTop atTop<VAR>this : {b | BddAbove (range fun i => f i b)} = {x | ∃ n, ∀ (i : ι), f i x ≤ u n}<GOAL>MeasurableSet (⋃ i, {x | ∀ (i_1 : ι), f i_1 x ≤ u i})
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : OrderedRing k<VAR>inst✝² : OrderedAddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : OrderedSMul k E<VAR>a a' b b' : E<VAR>r r' : k<VAR>ha : a < a'<VAR>hr : r < 1<GOAL>(lineMap a b) r < (lineMap a' b) r
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : OrderedRing k<VAR>inst✝² : OrderedAddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : OrderedSMul k E<VAR>a a' b b' : E<VAR>r r' : k<VAR>ha : a < a'<VAR>hr : r < 1<GOAL>(1 - r) • a + r • b < (1 - r) • a' + r • b