ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp E 2 μ)<GOAL>(eLpNorm (↑↑↑((condexpL2 E 𝕜 hm) f)) 2 μ).toReal ≤ (eLpNorm (↑↑f) 2 μ).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp E 2 μ)<GOAL>eLpNorm (↑↑↑((condexpL2 E 𝕜 hm) f)) 2 μ ≠ ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_7<VAR>inst✝ : SeminormedAddCommGroup β<VAR>T T' : Set α → β<VAR>C C' : ℝ<VAR>c : ℝ≥0∞<VAR>hc_ne_top : c ≠ ⊤<VAR>hT : DominatedFinMeasAdditive (c • μ) T C<GOAL>DominatedFinMeasAdditive μ T (c.toReal * C)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_7<VAR>inst✝ : SeminormedAddCommGroup β<VAR>T T' : Set α → β<VAR>C C' : ℝ<VAR>c : ℝ≥0∞<VAR>hc_ne_top : c ≠ ⊤<VAR>hT : DominatedFinMeasAdditive (c • μ) T C<VAR>h : ∀ (s : Set α), MeasurableSet s → c • μ s = ⊤ → μ s = ⊤<GOAL>DominatedFinMeasAdditive μ T (c.toReal * C)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_7<VAR>inst✝ : SeminormedAddCommGroup β<VAR>T T' : Set α → β<VAR>C C' : ℝ<VAR>c : ℝ≥0∞<VAR>hc_ne_top : c ≠ ⊤<VAR>hT : DominatedFinMeasAdditive (c • μ) T C<VAR>h : ∀ (s : Set α), MeasurableSet s → c • μ s = ⊤ → μ s = ⊤<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s < ⊤<GOAL>‖T s‖ ≤ c.toReal * C * (μ s).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_7<VAR>inst✝ : SeminormedAddCommGroup β<VAR>T T' : Set α → β<VAR>C C' : ℝ<VAR>c : ℝ≥0∞<VAR>hc_ne_top : c ≠ ⊤<VAR>hT : DominatedFinMeasAdditive (c • μ) T C<VAR>h : ∀ (s : Set α), MeasurableSet s → c • μ s = ⊤ → μ s = ⊤<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s < ⊤<VAR>hcμs : c • μ s ≠ ⊤<GOAL>‖T s‖ ≤ c.toReal * C * (μ s).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_7<VAR>inst✝ : SeminormedAddCommGroup β<VAR>T T' : Set α → β<VAR>C C' : ℝ<VAR>c : ℝ≥0∞<VAR>hc_ne_top : c ≠ ⊤<VAR>hT : DominatedFinMeasAdditive (c • μ) T C<VAR>h : ∀ (s : Set α), MeasurableSet s → c • μ s = ⊤ → μ s = ⊤<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s < ⊤<VAR>hcμs : c * μ s ≠ ⊤<GOAL>‖T s‖ ≤ c.toReal * C * (μ s).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_7<VAR>inst✝ : SeminormedAddCommGroup β<VAR>T T' : Set α → β<VAR>C C' : ℝ<VAR>c : ℝ≥0∞<VAR>hc_ne_top : c ≠ ⊤<VAR>h : ∀ (s : Set α), MeasurableSet s → c • μ s = ⊤ → μ s = ⊤<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s < ⊤<VAR>hcμs : c * μ s ≠ ⊤<VAR>hT : FinMeasAdditive (c • μ) T ∧ ∀ (s : Set α), MeasurableSet s → c * μ s < ⊤ → ‖T s‖ ≤ C * (c.toReal * (μ s).toReal)<GOAL>‖T s‖ ≤ c.toReal * C * (μ s).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_7<VAR>inst✝ : SeminormedAddCommGroup β<VAR>T T' : Set α → β<VAR>C C' : ℝ<VAR>c : ℝ≥0∞<VAR>hc_ne_top : c ≠ ⊤<VAR>h : ∀ (s : Set α), MeasurableSet s → c • μ s = ⊤ → μ s = ⊤<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s < ⊤<VAR>hcμs : c * μ s ≠ ⊤<VAR>hT : FinMeasAdditive (c • μ) T ∧ ∀ (s : Set α), MeasurableSet s → c * μ s < ⊤ → ‖T s‖ ≤ C * (c.toReal * (μ s).toReal)<GOAL>C * (c.toReal * (μ s).toReal) = c.toReal * C * (μ s).toReal
<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>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>s : Set α<GOAL>(∀ (n : ℕ), μ (s ∩ spanningSets μ n) = 0) ↔ μ s = 0
<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>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>s : Set α<GOAL>(∀ (n : ℕ), μ (s ∩ spanningSets μ n) = 0) ↔ μ (⋃ n, s ∩ spanningSets μ n) = 0
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>hb : 1 < b<VAR>r : R<GOAL>r ≤ ↑b ^ clog b r
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>hb : 1 < b<VAR>r : R<VAR>hr : r ≤ 0<GOAL>r ≤ ↑b ^ clog b r
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>hb : 1 < b<VAR>r : R<VAR>hr : 0 < r<GOAL>r ≤ ↑b ^ clog b r
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>hb : 1 < b<VAR>r : R<VAR>hr : 0 < r<GOAL>↑b ^ log b r⁻¹ ≤ r⁻¹
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>hb : 1 < b<VAR>r : R<VAR>hr : 0 < r<GOAL>0 < ↑b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f✝ : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g''✝ : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f : ℕ → E<VAR>g'' : ℕ → E''<VAR>h : f =O[atTop] g''<GOAL>f =O[cofinite] g''
<VAR>a b : Cardinal.{u_1}<GOAL>a * b ≤ max (max a b) ℵ₀
<VAR>b : Cardinal.{u_1}<GOAL>0 * b ≤ max (max 0 b) ℵ₀
<VAR>a b : Cardinal.{u_1}<VAR>ha0 : a ≠ 0<GOAL>a * b ≤ max (max a b) ℵ₀
<VAR>a : Cardinal.{u_1}<VAR>ha0 : a ≠ 0<GOAL>a * 0 ≤ max (max a 0) ℵ₀
<VAR>a b : Cardinal.{u_1}<VAR>ha0 : a ≠ 0<VAR>hb0 : b ≠ 0<GOAL>a * b ≤ max (max a b) ℵ₀
<VAR>a b : Cardinal.{u_1}<VAR>ha0 : a ≠ 0<VAR>hb0 : b ≠ 0<VAR>ha : ℵ₀ ≤ a<GOAL>a * b ≤ max (max a b) ℵ₀
<VAR>a b : Cardinal.{u_1}<VAR>ha0 : a ≠ 0<VAR>hb0 : b ≠ 0<VAR>ha : a < ℵ₀<GOAL>a * b ≤ max (max a b) ℵ₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>x : Part α<GOAL>x.bind some = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>x : Part α<GOAL>map (fun a => a) x = x
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁵ : Fintype l<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : Unique ι<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>r : ℝ<VAR>hr : 0 < r<VAR>A : Matrix m n α<GOAL>‖A‖ < r ↔ ∀ (i : m) (j : n), ‖A i j‖ < r
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>ι : Type u_1<VAR>s : ι → Set α<VAR>t : Set α<VAR>tfin : t.Finite<VAR>h : t ⊆ ⋃ i, s i<VAR>I : Set ι<VAR>Ifin : I.Finite<VAR>hI : t ⊆ ⋃ i ∈ I, s i<VAR>x : α<GOAL>x ∈ t ↔ x ∈ ⋃ i, (fun x => s ↑x ∩ t) i
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>ι : Type u_1<VAR>s : ι → Set α<VAR>t : Set α<VAR>tfin : t.Finite<VAR>h : t ⊆ ⋃ i, s i<VAR>I : Set ι<VAR>Ifin : I.Finite<VAR>hI : t ⊆ ⋃ i ∈ I, s i<VAR>x : α<GOAL>x ∈ t ↔ ∃ i, x ∈ s ↑i ∩ t
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : Monoid γ<VAR>inst✝ : FunLike F β γ<VAR>s : Finset α<VAR>f g : α → β<VAR>comm_ff : (↑s).Pairwise fun x y => Commute (f x) (f y)<VAR>comm_gg : (↑s).Pairwise fun x y => Commute (g x) (g y)<VAR>comm_gf : (↑s).Pairwise fun x y => Commute (g x) (f y)<VAR>x : α<VAR>hx : x ∈ ↑s<VAR>y : α<VAR>hy : y ∈ ↑s<VAR>h : x ≠ y<GOAL>Commute ((f * g) x) ((f * g) y)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : Monoid γ<VAR>inst✝ : FunLike F β γ<VAR>s : Finset α<VAR>f g : α → β<VAR>comm_ff : (↑s).Pairwise fun x y => Commute (f x) (f y)<VAR>comm_gg : (↑s).Pairwise fun x y => Commute (g x) (g y)<VAR>comm_gf : (↑s).Pairwise fun x y => Commute (g x) (f y)<VAR>x : α<VAR>hx : x ∈ ↑s<VAR>y : α<VAR>hy : y ∈ ↑s<VAR>h : x ≠ y<GOAL>Commute (f x) (f y)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : Monoid γ<VAR>inst✝ : FunLike F β γ<VAR>s : Finset α<VAR>f g : α → β<VAR>comm_ff : (↑s).Pairwise fun x y => Commute (f x) (f y)<VAR>comm_gg : (↑s).Pairwise fun x y => Commute (g x) (g y)<VAR>comm_gf : (↑s).Pairwise fun x y => Commute (g x) (f y)<VAR>x : α<VAR>hx : x ∈ ↑s<VAR>y : α<VAR>hy : y ∈ ↑s<VAR>h : x ≠ y<GOAL>Commute (f x) (g y)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : Monoid γ<VAR>inst✝ : FunLike F β γ<VAR>s : Finset α<VAR>f g : α → β<VAR>comm_ff : (↑s).Pairwise fun x y => Commute (f x) (f y)<VAR>comm_gg : (↑s).Pairwise fun x y => Commute (g x) (g y)<VAR>comm_gf : (↑s).Pairwise fun x y => Commute (g x) (f y)<VAR>x : α<VAR>hx : x ∈ ↑s<VAR>y : α<VAR>hy : y ∈ ↑s<VAR>h : x ≠ y<GOAL>Commute (g x) (f y)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : Monoid γ<VAR>inst✝ : FunLike F β γ<VAR>s : Finset α<VAR>f g : α → β<VAR>comm_ff : (↑s).Pairwise fun x y => Commute (f x) (f y)<VAR>comm_gg : (↑s).Pairwise fun x y => Commute (g x) (g y)<VAR>comm_gf : (↑s).Pairwise fun x y => Commute (g x) (f y)<VAR>x : α<VAR>hx : x ∈ ↑s<VAR>y : α<VAR>hy : y ∈ ↑s<VAR>h : x ≠ y<GOAL>Commute (g x) (g y)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k : ℕ<VAR>f : R[X]<GOAL>(hasseDeriv 1) f = derivative f
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>h : 0 < b<GOAL>b⁻¹ * a < c ↔ a < c * b
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>S : Set (Set X)<VAR>hc : S.Countable<VAR>hcomp : ∀ s ∈ S, IsCompact s<GOAL>IsSigmaCompact (⋃₀ S)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>S : Set (Set X)<VAR>hc : S.Countable<VAR>hcomp : ∀ s ∈ S, IsCompact s<VAR>this : Countable ↑S<GOAL>IsSigmaCompact (⋃₀ S)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>S : Set (Set X)<VAR>hc : S.Countable<VAR>hcomp : ∀ s ∈ S, IsCompact s<VAR>this : Countable ↑S<GOAL>IsSigmaCompact (⋃ i, ↑i)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>f g : ArithmeticFunction R<VAR>h : ArithmeticFunction M<VAR>n : ℕ<GOAL>((f * g) • h) n = (f • g • h) n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>f g : ArithmeticFunction R<VAR>h : ArithmeticFunction M<VAR>n : ℕ<GOAL>∑ x ∈ n.divisorsAntidiagonal.sigma fun a => a.1.divisorsAntidiagonal, f x.snd.1 • g x.snd.2 • h x.fst.2 = ∑ x ∈ n.divisorsAntidiagonal.sigma fun a => a.2.divisorsAntidiagonal, f x.fst.1 • g x.snd.1 • h x.snd.2
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I J : Box ι<VAR>c c₁ c₂ : ℝ≥0<VAR>r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π π₁ π₂ : TaggedPrepartition I<VAR>l l₁ l₂ : IntegrationParams<VAR>hπ : l.MemBaseSet I c r π<VAR>p : Box ι → Prop<GOAL>l.MemBaseSet I c r (π.filter p)
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I J : Box ι<VAR>c c₁ c₂ : ℝ≥0<VAR>r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π π₁ π₂ : TaggedPrepartition I<VAR>l l₁ l₂ : IntegrationParams<VAR>hπ : l.MemBaseSet I c r π<VAR>p : Box ι → Prop<VAR>hD : l.bDistortion = true<GOAL>∃ π', π'.iUnion = ↑I \ (π.filter p).iUnion ∧ π'.distortion ≤ c
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I J : Box ι<VAR>c c₁ c₂ : ℝ≥0<VAR>r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π π₁✝ π₂ : TaggedPrepartition I<VAR>l l₁ l₂ : IntegrationParams<VAR>hπ : l.MemBaseSet I c r π<VAR>p : Box ι → Prop<VAR>hD : l.bDistortion = true<VAR>π₁ : Prepartition I<VAR>hπ₁U : π₁.iUnion = ↑I \ π.iUnion<VAR>hc : π₁.distortion ≤ c<GOAL>∃ π', π'.iUnion = ↑I \ (π.filter p).iUnion ∧ π'.distortion ≤ c
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I J : Box ι<VAR>c c₁ c₂ : ℝ≥0<VAR>r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π π₁✝ π₂✝ : TaggedPrepartition I<VAR>l l₁ l₂ : IntegrationParams<VAR>hπ : l.MemBaseSet I c r π<VAR>p : Box ι → Prop<VAR>hD : l.bDistortion = true<VAR>π₁ : Prepartition I<VAR>hπ₁U : π₁.iUnion = ↑I \ π.iUnion<VAR>hc : π₁.distortion ≤ c<VAR>π₂ : TaggedPrepartition I := π.filter fun J => ¬p J<GOAL>∃ π', π'.iUnion = ↑I \ (π.filter p).iUnion ∧ π'.distortion ≤ c
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I J : Box ι<VAR>c c₁ c₂ : ℝ≥0<VAR>r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π π₁✝ π₂✝ : TaggedPrepartition I<VAR>l l₁ l₂ : IntegrationParams<VAR>hπ : l.MemBaseSet I c r π<VAR>p : Box ι → Prop<VAR>hD : l.bDistortion = true<VAR>π₁ : Prepartition I<VAR>hπ₁U : π₁.iUnion = ↑I \ π.iUnion<VAR>hc : π₁.distortion ≤ c<VAR>π₂ : TaggedPrepartition I := π.filter fun J => ¬p J<VAR>this : Disjoint π₁.iUnion π₂.iUnion<GOAL>∃ π', π'.iUnion = ↑I \ (π.filter p).iUnion ∧ π'.distortion ≤ c
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : C ⥤ D<VAR>ε : 𝟙_ D ⟶ F.obj (𝟙_ C)<VAR>μ : (X Y : C) → F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y)<VAR>μ_natural : autoParam (∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ g)) _auto✝<VAR>associativity : autoParam (∀ (X Y Z : C), (μ X Y ⊗ 𝟙 (F.obj Z)) ≫ μ (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom = (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ (𝟙 (F.obj X) ⊗ μ Y Z) ≫ μ X (Y ⊗ Z)) _auto✝<VAR>left_unitality : autoParam (∀ (X : C), (λ_ (F.obj X)).hom = (ε ⊗ 𝟙 (F.obj X)) ≫ μ (𝟙_ C) X ≫ F.map (λ_ X).hom) _auto✝<VAR>right_unitality : autoParam (∀ (X : C), (ρ_ (F.obj X)).hom = (𝟙 (F.obj X) ⊗ ε) ≫ μ X (𝟙_ C) ≫ F.map (ρ_ X).hom) _auto✝<VAR>X✝ Y✝ : C<VAR>f : X✝ ⟶ Y✝<VAR>X' : C<GOAL>{ obj := F.obj, map := fun {X Y} => F.map, map_id := ⋯, map_comp := ⋯ }.map f ▷ { obj := F.obj, map := fun {X Y} => F.map, map_id := ⋯, map_comp := ⋯ }.obj X' ≫ μ Y✝ X' = μ X✝ X' ≫ { obj := F.obj, map := fun {X Y} => F.map, map_id := ⋯, map_comp := ⋯ }.map (f ▷ X')
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : C ⥤ D<VAR>ε : 𝟙_ D ⟶ F.obj (𝟙_ C)<VAR>μ : (X Y : C) → F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y)<VAR>μ_natural : autoParam (∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ g)) _auto✝<VAR>associativity : autoParam (∀ (X Y Z : C), (μ X Y ⊗ 𝟙 (F.obj Z)) ≫ μ (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom = (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ (𝟙 (F.obj X) ⊗ μ Y Z) ≫ μ X (Y ⊗ Z)) _auto✝<VAR>left_unitality : autoParam (∀ (X : C), (λ_ (F.obj X)).hom = (ε ⊗ 𝟙 (F.obj X)) ≫ μ (𝟙_ C) X ≫ F.map (λ_ X).hom) _auto✝<VAR>right_unitality : autoParam (∀ (X : C), (ρ_ (F.obj X)).hom = (𝟙 (F.obj X) ⊗ ε) ≫ μ X (𝟙_ C) ≫ F.map (ρ_ X).hom) _auto✝<VAR>X✝ Y✝ X' : C<VAR>f : X✝ ⟶ Y✝<GOAL>{ obj := F.obj, map := fun {X Y} => F.map, map_id := ⋯, map_comp := ⋯ }.obj X' ◁ { obj := F.obj, map := fun {X Y} => F.map, map_id := ⋯, map_comp := ⋯ }.map f ≫ μ X' Y✝ = μ X' X✝ ≫ { obj := F.obj, map := fun {X Y} => F.map, map_id := ⋯, map_comp := ⋯ }.map (X' ◁ f)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : C ⥤ D<VAR>ε : 𝟙_ D ⟶ F.obj (𝟙_ C)<VAR>μ : (X Y : C) → F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y)<VAR>μ_natural : autoParam (∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ g)) _auto✝<VAR>associativity : autoParam (∀ (X Y Z : C), (μ X Y ⊗ 𝟙 (F.obj Z)) ≫ μ (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom = (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ (𝟙 (F.obj X) ⊗ μ Y Z) ≫ μ X (Y ⊗ Z)) _auto✝<VAR>left_unitality : autoParam (∀ (X : C), (λ_ (F.obj X)).hom = (ε ⊗ 𝟙 (F.obj X)) ≫ μ (𝟙_ C) X ≫ F.map (λ_ X).hom) _auto✝<VAR>right_unitality : autoParam (∀ (X : C), (ρ_ (F.obj X)).hom = (𝟙 (F.obj X) ⊗ ε) ≫ μ X (𝟙_ C) ≫ F.map (ρ_ X).hom) _auto✝<VAR>X Y Z : C<GOAL>μ X Y ▷ { obj := F.obj, map := fun {X Y} => F.map, map_id := ⋯, map_comp := ⋯ }.obj Z ≫ μ (X ⊗ Y) Z ≫ { obj := F.obj, map := fun {X Y} => F.map, map_id := ⋯, map_comp := ⋯ }.map (α_ X Y Z).hom = (α_ ({ obj := F.obj, map := fun {X Y} => F.map, map_id := ⋯, map_comp := ⋯ }.obj X) ({ obj := F.obj, map := fun {X Y} => F.map, map_id := ⋯, map_comp := ⋯ }.obj Y) ({ obj := F.obj, map := fun {X Y} => F.map, map_id := ⋯, map_comp := ⋯ }.obj Z)).hom ≫ { obj := F.obj, map := fun {X Y} => F.map, map_id := ⋯, map_comp := ⋯ }.obj X ◁ μ Y Z ≫ μ X (Y ⊗ Z)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : C ⥤ D<VAR>ε : 𝟙_ D ⟶ F.obj (𝟙_ C)<VAR>μ : (X Y : C) → F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y)<VAR>μ_natural : autoParam (∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ g)) _auto✝<VAR>associativity : autoParam (∀ (X Y Z : C), (μ X Y ⊗ 𝟙 (F.obj Z)) ≫ μ (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom = (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ (𝟙 (F.obj X) ⊗ μ Y Z) ≫ μ X (Y ⊗ Z)) _auto✝<VAR>left_unitality : autoParam (∀ (X : C), (λ_ (F.obj X)).hom = (ε ⊗ 𝟙 (F.obj X)) ≫ μ (𝟙_ C) X ≫ F.map (λ_ X).hom) _auto✝<VAR>right_unitality : autoParam (∀ (X : C), (ρ_ (F.obj X)).hom = (𝟙 (F.obj X) ⊗ ε) ≫ μ X (𝟙_ C) ≫ F.map (ρ_ X).hom) _auto✝<VAR>X : C<GOAL>(λ_ ({ obj := F.obj, map := fun {X Y} => F.map, map_id := ⋯, map_comp := ⋯ }.obj X)).hom = ε ▷ { obj := F.obj, map := fun {X Y} => F.map, map_id := ⋯, map_comp := ⋯ }.obj X ≫ μ (𝟙_ C) X ≫ { obj := F.obj, map := fun {X Y} => F.map, map_id := ⋯, map_comp := ⋯ }.map (λ_ X).hom
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : C ⥤ D<VAR>ε : 𝟙_ D ⟶ F.obj (𝟙_ C)<VAR>μ : (X Y : C) → F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y)<VAR>μ_natural : autoParam (∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ g)) _auto✝<VAR>associativity : autoParam (∀ (X Y Z : C), (μ X Y ⊗ 𝟙 (F.obj Z)) ≫ μ (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom = (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ (𝟙 (F.obj X) ⊗ μ Y Z) ≫ μ X (Y ⊗ Z)) _auto✝<VAR>left_unitality : autoParam (∀ (X : C), (λ_ (F.obj X)).hom = (ε ⊗ 𝟙 (F.obj X)) ≫ μ (𝟙_ C) X ≫ F.map (λ_ X).hom) _auto✝<VAR>right_unitality : autoParam (∀ (X : C), (ρ_ (F.obj X)).hom = (𝟙 (F.obj X) ⊗ ε) ≫ μ X (𝟙_ C) ≫ F.map (ρ_ X).hom) _auto✝<VAR>X : C<GOAL>(ρ_ ({ obj := F.obj, map := fun {X Y} => F.map, map_id := ⋯, map_comp := ⋯ }.obj X)).hom = { obj := F.obj, map := fun {X Y} => F.map, map_id := ⋯, map_comp := ⋯ }.obj X ◁ ε ≫ μ X (𝟙_ C) ≫ { obj := F.obj, map := fun {X Y} => F.map, map_id := ⋯, map_comp := ⋯ }.map (ρ_ X).hom
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>inst✝¹ : Category.{w, v} C<VAR>inst✝ : HasTerminal C<VAR>A : C<VAR>U V : (Opens ↑X)ᵒᵖ<VAR>i : U ⟶ V<VAR>h : p₀ ∈ unop V<GOAL>(if p₀ ∈ unop U then A else ⊤_ C) = if p₀ ∈ unop V then A else ⊤_ C
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>g : σ → S₁<VAR>p : MvPolynomial σ R<GOAL>eval₂ C X p = p
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRoot S f<VAR>p : R[X]<GOAL>p ∈ RingHom.ker h.map ↔ f ∣ p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : CountableOrCountablyGenerated α β<VAR>κ : Kernel α (β × Ω)<VAR>inst✝² : IsFiniteKernel κ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>a : α<VAR>t : Set Ω<VAR>ht : MeasurableSet t<VAR>hf : IntegrableOn f (Set.univ ×ˢ t) (κ a)<GOAL>∫ (b : β), ∫ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω) in Set.univ ×ˢ t, f x ∂κ a