ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>I : Box ι<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hl : l.bRiemann = false<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>δ : ℕ → ℝ≥0<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>c✝ : ℝ≥0<VAR>hδc : HasSum δ c✝<VAR>hcε : c✝ < ε<VAR>this : Fact (μ ↑I < ⊤)<VAR>hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0<VAR>N : (ι → ℝ) → ℕ := fun x => ⌈‖f x‖⌉₊<VAR>N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0<VAR>U : ℕ → Set (ι → ℝ)<VAR>hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n<VAR>hUo : ∀ (n : ℕ), IsOpen (U n)<VAR>hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrU : ∀ (x : ι → ℝ), closedBall x ↑(r x) ⊆ U (N x)<VAR>c : ℝ≥0<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c ((fun x => r) c) π<VAR>x✝ : π.IsPartition<GOAL>‖∑ y ∈ Finset.image (fun J => N (π.tag J)) π.boxes, integralSum f μ.toBoxAdditive.toSMul (π.filter fun x => N (π.tag x) = y)‖ ≤ ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>I : Box ι<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hl : l.bRiemann = false<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>δ : ℕ → ℝ≥0<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>c✝ : ℝ≥0<VAR>hδc : HasSum δ c✝<VAR>hcε : c✝ < ε<VAR>this : Fact (μ ↑I < ⊤)<VAR>hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0<VAR>N : (ι → ℝ) → ℕ := fun x => ⌈‖f x‖⌉₊<VAR>N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0<VAR>U : ℕ → Set (ι → ℝ)<VAR>hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n<VAR>hUo : ∀ (n : ℕ), IsOpen (U n)<VAR>hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrU : ∀ (x : ι → ℝ), closedBall x ↑(r x) ⊆ U (N x)<VAR>c : ℝ≥0<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c ((fun x => r) c) π<VAR>x✝ : π.IsPartition<GOAL>‖∑ y ∈ Finset.image (fun J => N (π.tag J)) π.boxes, integralSum f μ.toBoxAdditive.toSMul (π.filter fun x => N (π.tag x) = y)‖ ≤ ↑c✝
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>I : Box ι<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hl : l.bRiemann = false<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>δ : ℕ → ℝ≥0<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>c✝ : ℝ≥0<VAR>hδc : HasSum δ c✝<VAR>hcε : c✝ < ε<VAR>this : Fact (μ ↑I < ⊤)<VAR>hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0<VAR>N : (ι → ℝ) → ℕ := fun x => ⌈‖f x‖⌉₊<VAR>N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0<VAR>U : ℕ → Set (ι → ℝ)<VAR>hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n<VAR>hUo : ∀ (n : ℕ), IsOpen (U n)<VAR>hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrU : ∀ (x : ι → ℝ), closedBall x ↑(r x) ⊆ U (N x)<VAR>c : ℝ≥0<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c ((fun x => r) c) π<VAR>x✝ : π.IsPartition<GOAL>∀ b ∈ Finset.image (fun J => N (π.tag J)) π.boxes, ‖integralSum f μ.toBoxAdditive.toSMul (π.filter fun x => N (π.tag x) = b)‖ ≤ ↑(δ b)
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>I : Box ι<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hl : l.bRiemann = false<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>δ : ℕ → ℝ≥0<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>c✝ : ℝ≥0<VAR>hδc : HasSum δ c✝<VAR>hcε : c✝ < ε<VAR>this : Fact (μ ↑I < ⊤)<VAR>hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0<VAR>N : (ι → ℝ) → ℕ := fun x => ⌈‖f x‖⌉₊<VAR>N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0<VAR>U : ℕ → Set (ι → ℝ)<VAR>hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n<VAR>hUo : ∀ (n : ℕ), IsOpen (U n)<VAR>hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrU : ∀ (x : ι → ℝ), closedBall x ↑(r x) ⊆ U (N x)<VAR>c : ℝ≥0<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c ((fun x => r) c) π<VAR>x✝ : π.IsPartition<VAR>n : ℕ<GOAL>‖∑ J ∈ (π.filter fun x => N (π.tag x) = n).boxes, (μ ↑J).toReal • f (π.tag J)‖ ≤ ↑(δ n)
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>I : Box ι<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hl : l.bRiemann = false<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>δ : ℕ → ℝ≥0<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>c✝ : ℝ≥0<VAR>hδc : HasSum δ c✝<VAR>hcε : c✝ < ε<VAR>this✝ : Fact (μ ↑I < ⊤)<VAR>hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0<VAR>N : (ι → ℝ) → ℕ := fun x => ⌈‖f x‖⌉₊<VAR>N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0<VAR>U : ℕ → Set (ι → ℝ)<VAR>hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n<VAR>hUo : ∀ (n : ℕ), IsOpen (U n)<VAR>hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrU : ∀ (x : ι → ℝ), closedBall x ↑(r x) ⊆ U (N x)<VAR>c : ℝ≥0<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c ((fun x => r) c) π<VAR>x✝ : π.IsPartition<VAR>n : ℕ<VAR>this : ∀ J ∈ π.filter fun J => N (π.tag J) = n, ‖(μ ↑J).toReal • f (π.tag J)‖ ≤ (μ ↑J).toReal * ↑n<GOAL>‖∑ J ∈ (π.filter fun x => N (π.tag x) = n).boxes, (μ ↑J).toReal • f (π.tag J)‖ ≤ ↑(δ n)
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>I : Box ι<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hl : l.bRiemann = false<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>δ : ℕ → ℝ≥0<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>c✝ : ℝ≥0<VAR>hδc : HasSum δ c✝<VAR>hcε : c✝ < ε<VAR>this✝ : Fact (μ ↑I < ⊤)<VAR>hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0<VAR>N : (ι → ℝ) → ℕ := fun x => ⌈‖f x‖⌉₊<VAR>N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0<VAR>U : ℕ → Set (ι → ℝ)<VAR>hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n<VAR>hUo : ∀ (n : ℕ), IsOpen (U n)<VAR>hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrU : ∀ (x : ι → ℝ), closedBall x ↑(r x) ⊆ U (N x)<VAR>c : ℝ≥0<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c ((fun x => r) c) π<VAR>x✝ : π.IsPartition<VAR>n : ℕ<VAR>this : ∀ J ∈ π.filter fun J => N (π.tag J) = n, ‖(μ ↑J).toReal • f (π.tag J)‖ ≤ (μ ↑J).toReal * ↑n<GOAL>∑ b ∈ (π.filter fun J => N (π.tag J) = n).boxes, (μ ↑b).toReal * ↑n ≤ ↑(δ n)
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>I : Box ι<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hl : l.bRiemann = false<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>δ : ℕ → ℝ≥0<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>c✝ : ℝ≥0<VAR>hδc : HasSum δ c✝<VAR>hcε : c✝ < ε<VAR>this : Fact (μ ↑I < ⊤)<VAR>hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0<VAR>N : (ι → ℝ) → ℕ := fun x => ⌈‖f x‖⌉₊<VAR>N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0<VAR>U : ℕ → Set (ι → ℝ)<VAR>hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n<VAR>hUo : ∀ (n : ℕ), IsOpen (U n)<VAR>hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrU : ∀ (x : ι → ℝ), closedBall x ↑(r x) ⊆ U (N x)<VAR>c : ℝ≥0<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c ((fun x => r) c) π<VAR>x✝ : π.IsPartition<VAR>n : ℕ<GOAL>∑ b ∈ (π.filter fun J => N (π.tag J) = n).boxes, (μ ↑b).toReal * ↑n ≤ ↑(δ n)
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>I : Box ι<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hl : l.bRiemann = false<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>δ : ℕ → ℝ≥0<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>c✝ : ℝ≥0<VAR>hδc : HasSum δ c✝<VAR>hcε : c✝ < ε<VAR>this : Fact (μ ↑I < ⊤)<VAR>hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0<VAR>N : (ι → ℝ) → ℕ := fun x => ⌈‖f x‖⌉₊<VAR>N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0<VAR>U : ℕ → Set (ι → ℝ)<VAR>hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n<VAR>hUo : ∀ (n : ℕ), IsOpen (U n)<VAR>hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrU : ∀ (x : ι → ℝ), closedBall x ↑(r x) ⊆ U (N x)<VAR>c : ℝ≥0<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c ((fun x => r) c) π<VAR>x✝ : π.IsPartition<VAR>n : ℕ<GOAL>(μ (π.filter fun J => N (π.tag J) = n).iUnion).toReal * ↑n ≤ ↑(δ n)
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>I : Box ι<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hl : l.bRiemann = false<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>δ : ℕ → ℝ≥0<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>c✝ : ℝ≥0<VAR>hδc : HasSum δ c✝<VAR>hcε : c✝ < ε<VAR>this : Fact (μ ↑I < ⊤)<VAR>hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0<VAR>N : (ι → ℝ) → ℕ := fun x => ⌈‖f x‖⌉₊<VAR>N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0<VAR>U : ℕ → Set (ι → ℝ)<VAR>hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n<VAR>hUo : ∀ (n : ℕ), IsOpen (U n)<VAR>hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrU : ∀ (x : ι → ℝ), closedBall x ↑(r x) ⊆ U (N x)<VAR>c : ℝ≥0<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c ((fun x => r) c) π<VAR>x✝ : π.IsPartition<VAR>n : ℕ<VAR>m : ℝ≥0∞ := μ (π.filter fun J => N (π.tag J) = n).iUnion<GOAL>m.toReal * ↑n ≤ ↑(δ n)
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>I : Box ι<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hl : l.bRiemann = false<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>δ : ℕ → ℝ≥0<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>c✝ : ℝ≥0<VAR>hδc : HasSum δ c✝<VAR>hcε : c✝ < ε<VAR>this✝ : Fact (μ ↑I < ⊤)<VAR>hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0<VAR>N : (ι → ℝ) → ℕ := fun x => ⌈‖f x‖⌉₊<VAR>N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0<VAR>U : ℕ → Set (ι → ℝ)<VAR>hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n<VAR>hUo : ∀ (n : ℕ), IsOpen (U n)<VAR>hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrU : ∀ (x : ι → ℝ), closedBall x ↑(r x) ⊆ U (N x)<VAR>c : ℝ≥0<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c ((fun x => r) c) π<VAR>x✝ : π.IsPartition<VAR>n : ℕ<VAR>m : ℝ≥0∞ := μ (π.filter fun J => N (π.tag J) = n).iUnion<VAR>this : m < ↑(δ n) / ↑n<GOAL>m.toReal * ↑n ≤ ↑(δ n)
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>I : Box ι<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hl : l.bRiemann = false<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>δ : ℕ → ℝ≥0<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>c✝ : ℝ≥0<VAR>hδc : HasSum δ c✝<VAR>hcε : c✝ < ε<VAR>this✝ : Fact (μ ↑I < ⊤)<VAR>hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0<VAR>N : (ι → ℝ) → ℕ := fun x => ⌈‖f x‖⌉₊<VAR>N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0<VAR>U : ℕ → Set (ι → ℝ)<VAR>hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n<VAR>hUo : ∀ (n : ℕ), IsOpen (U n)<VAR>hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrU : ∀ (x : ι → ℝ), closedBall x ↑(r x) ⊆ U (N x)<VAR>c : ℝ≥0<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c ((fun x => r) c) π<VAR>x✝ : π.IsPartition<VAR>n : ℕ<VAR>m : ℝ≥0∞<VAR>this : m < ↑(δ n) / ↑n<GOAL>m.toReal * ↑n ≤ ↑(δ n)
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>I : Box ι<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hl : l.bRiemann = false<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>δ : ℕ → ℝ≥0<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>c✝ : ℝ≥0<VAR>hδc : HasSum δ c✝<VAR>hcε : c✝ < ε<VAR>this✝ : Fact (μ ↑I < ⊤)<VAR>hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0<VAR>N : (ι → ℝ) → ℕ := fun x => ⌈‖f x‖⌉₊<VAR>N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0<VAR>U : ℕ → Set (ι → ℝ)<VAR>hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n<VAR>hUo : ∀ (n : ℕ), IsOpen (U n)<VAR>hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrU : ∀ (x : ι → ℝ), closedBall x ↑(r x) ⊆ U (N x)<VAR>c : ℝ≥0<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c ((fun x => r) c) π<VAR>x✝ : π.IsPartition<VAR>n : ℕ<VAR>m : ℝ≥0<VAR>this : ↑m < ↑(δ n) / ↑n<GOAL>(↑m).toReal * ↑n ≤ ↑(δ n)
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>I : Box ι<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hl : l.bRiemann = false<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>δ : ℕ → ℝ≥0<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>c✝ : ℝ≥0<VAR>hδc : HasSum δ c✝<VAR>hcε : c✝ < ε<VAR>this✝ : Fact (μ ↑I < ⊤)<VAR>hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0<VAR>N : (ι → ℝ) → ℕ := fun x => ⌈‖f x‖⌉₊<VAR>N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0<VAR>U : ℕ → Set (ι → ℝ)<VAR>hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n<VAR>hUo : ∀ (n : ℕ), IsOpen (U n)<VAR>hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrU : ∀ (x : ι → ℝ), closedBall x ↑(r x) ⊆ U (N x)<VAR>c : ℝ≥0<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c ((fun x => r) c) π<VAR>x✝ : π.IsPartition<VAR>n : ℕ<VAR>m : ℝ≥0<VAR>this : ↑m < ↑(δ n) / ↑n<GOAL>↑n * ↑m ≤ ↑(δ n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<GOAL>⨅ l, ⨅ (_ : l < ⊤), 𝓟 (Ioi l) = ⨅ a, ⨅ (_ : a ≠ ⊤), 𝓟 (Ioi a)
<VAR>m : ℝ<VAR>hm : 1 < m<VAR>k : ℕ<GOAL>Summable fun i => 1 / m ^ (i + (k + 1))!
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<GOAL>⁅I, ⊥⁆ = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<GOAL>∀ m ∈ ⁅I, ⊥⁆, m = 0
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.3951, u_1} C<VAR>Δ : SimplexCategoryᵒᵖ<VAR>A : IndexSet Δ<GOAL>A.EqId ↔ (unop Δ).len ≤ (unop A.fst).len
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.3951, u_1} C<VAR>Δ : SimplexCategoryᵒᵖ<VAR>A : IndexSet Δ<GOAL>(unop A.fst).len = (unop Δ).len ↔ (unop Δ).len ≤ (unop A.fst).len
<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>N : Type u_5<VAR>inst✝ : Group N<VAR>f✝ : G →* N<VAR>H : Subgroup G<VAR>f : N →* G<VAR>hf : Surjective ⇑f<VAR>x : N<VAR>hx : x ∈ (comap f H).normalizer<GOAL>x ∈ comap f H.normalizer
<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>N : Type u_5<VAR>inst✝ : Group N<VAR>f✝ : G →* N<VAR>H : Subgroup G<VAR>f : N →* G<VAR>hf : Surjective ⇑f<VAR>x : N<VAR>hx : ∀ (h : N), f h ∈ H ↔ f (x * h * x⁻¹) ∈ H<GOAL>∀ (h : G), h ∈ H ↔ f x * h * (f x)⁻¹ ∈ H
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>hr : r ≠ 0<GOAL>LiouvilleWith p (↑r * x) ↔ LiouvilleWith p x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : MulOneClass M<VAR>inst✝¹ : MulOneClass N<VAR>inst✝ : MulOneClass P<VAR>c : Con M<VAR>x✝ y : M<VAR>f✝ f : M →* P<VAR>g : P → M<VAR>hf : Function.RightInverse g ⇑f<VAR>x : (ker f).Quotient<GOAL>(kerLift f) ((toQuotient ∘ g) ((kerLift f) x)) = (kerLift f) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : EDist α<VAR>x y : α<VAR>s t : Set α<GOAL>s.einfsep < ⊤ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < ⊤
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>m n m' n' : M<VAR>f : m ⟶ m'<VAR>g : n ⟶ n'<VAR>X : C<GOAL>(F.map g).app ((F.obj m).obj X) ≫ (F.obj n').map ((F.map f).app X) ≫ (F.μ m' n').app X = (F.μ m n).app X ≫ (F.map (f ⊗ g)).app X
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>m n m' n' : M<VAR>f : m ⟶ m'<VAR>g : n ⟶ n'<VAR>X : C<VAR>this : ((F.map f ⊗ F.map g) ≫ F.μ m' n').app X = (F.μ m n ≫ F.map (f ⊗ g)).app X<GOAL>(F.map g).app ((F.obj m).obj X) ≫ (F.obj n').map ((F.map f).app X) ≫ (F.μ m' n').app X = (F.μ m n).app X ≫ (F.map (f ⊗ g)).app X
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : AddCommMonoid M<VAR>s : Multiset (ι →₀ M)<GOAL>s.sum.support ⊆ (map Finsupp.support s).sup
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : AddCommMonoid M<VAR>a✝ : List (ι →₀ M)<GOAL>(sum (Quot.mk Setoid.r a✝)).support ⊆ (map Finsupp.support (Quot.mk Setoid.r a✝)).sup
<VAR>b : Bool<VAR>m n : ℕ<VAR>IH : shiftLeft' b m n ≠ 0 → (shiftLeft' b m n).size = m.size + n<VAR>h : shiftLeft' b m (n + 1) ≠ 0<GOAL>(shiftLeft' b m (n + 1)).size = m.size + (n + 1)
<VAR>b : Bool<VAR>m n : ℕ<VAR>IH : shiftLeft' b m n ≠ 0 → (shiftLeft' b m n).size = m.size + n<VAR>h : ¬bit b (shiftLeft' b m n) = 0<GOAL>(bit b (shiftLeft' b m n)).size = m.size + (n + 1)
<VAR>b : Bool<VAR>m n : ℕ<VAR>IH : shiftLeft' b m n ≠ 0 → (shiftLeft' b m n).size = m.size + n<VAR>h : ¬bit b (shiftLeft' b m n) = 0<GOAL>(shiftLeft' b m n).size.succ = (m.size + n).succ
<VAR>m n : ℕ<VAR>IH : shiftLeft' true m n ≠ 0 → (shiftLeft' true m n).size = m.size + n<VAR>h : ¬bit true 0 = 0<VAR>s0 : shiftLeft' true m n = 0<VAR>this : shiftLeft' true m n + 1 = 1<GOAL>(size 0).succ = (m.size + n).succ
<VAR>m n : ℕ<VAR>IH : shiftLeft' true m n ≠ 0 → (shiftLeft' true m n).size = m.size + n<VAR>h : ¬bit true 0 = 0<VAR>s0 : shiftLeft' true m n = 0<VAR>this : (m + 1) * 2 ^ n = 1<GOAL>(size 0).succ = (m.size + n).succ
<VAR>n : ℕ<VAR>h : ¬bit true 0 = 0<VAR>IH : shiftLeft' true 0 n ≠ 0 → (shiftLeft' true 0 n).size = size 0 + n<VAR>s0 : shiftLeft' true 0 n = 0<VAR>this : (0 + 1) * 2 ^ n = 1<GOAL>(size 0).succ = (size 0 + n).succ
<VAR>n : ℕ<VAR>h : ¬bit true 0 = 0<VAR>IH : shiftLeft' true 0 n ≠ 0 → (shiftLeft' true 0 n).size = size 0 + n<VAR>s0 : shiftLeft' true 0 n = 0<VAR>this : 2 ^ n = 1<GOAL>(size 0).succ = (size 0 + n).succ
<VAR>h : ¬bit true 0 = 0<VAR>IH : shiftLeft' true 0 0 ≠ 0 → (shiftLeft' true 0 0).size = size 0 + 0<VAR>s0 : shiftLeft' true 0 0 = 0<VAR>this : 2 ^ 0 = 1<GOAL>(size 0).succ = (size 0 + 0).succ
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a : α<GOAL>⋃ n, Ioc (a + n • p) (a + (n + 1) • p) = univ
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>∃ i, b ∈ Ioc (a + i • p) (a + (i + 1) • p)
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>hl : a < b - toIocDiv hp a b • p<VAR>hr : b - toIocDiv hp a b • p ≤ a + p<GOAL>∃ i, b ∈ Ioc (a + i • p) (a + (i + 1) • p)
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>hl : a < b - toIocDiv hp a b • p<VAR>hr : b - toIocDiv hp a b • p ≤ a + p<GOAL>b ≤ a + (toIocDiv hp a b + 1) • p
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>hl : a < b - toIocDiv hp a b • p<VAR>hr : b - toIocDiv hp a b • p ≤ a + p<GOAL>b ≤ a + toIocDiv hp a b • p + p
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>hl : a < b - toIocDiv hp a b • p<VAR>hr : b - toIocDiv hp a b • p ≤ a + p<GOAL>a + toIocDiv hp a b • p + p = a + p + toIocDiv hp a b • p
<VAR>R : Type u_1<VAR>inst✝ : MulZeroClass R<VAR>a b : R<GOAL>¬IsLeftRegular 0 ↔ Nontrivial R
<VAR>R : Type u_1<VAR>inst✝ : MulZeroClass R<VAR>a b : R<GOAL>(¬∃ x y, x ≠ y) ↔ ∀ (x y : R), x = y
<VAR>R : Type u_1<VAR>inst✝ : MulZeroClass R<VAR>a b : R<GOAL>(∀ (x y : R), x = y) ↔ ∀ (x y : R), x = y
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t : Set α<VAR>f g : α → ℝ≥0∞<VAR>hs₀ : μ s ≠ 0<VAR>hs : μ s ≠ ⊤<VAR>c : ℝ≥0∞<GOAL>⨍⁻ (_x : α) in s, c ∂μ = c
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>B : Set (Set α)<VAR>empty_mem : ∅ ∈ B<VAR>subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B<VAR>union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B<VAR>sUnion_univ : ⋃₀ B = univ<VAR>x : α<GOAL>{x} ∈ B
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>B : Set (Set α)<VAR>empty_mem : ∅ ∈ B<VAR>subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B<VAR>union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B<VAR>sUnion_univ : ∀ (a : α), ∃ b ∈ B, a ∈ b<VAR>x : α<GOAL>{x} ∈ B
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>B : Set (Set α)<VAR>empty_mem : ∅ ∈ B<VAR>subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B<VAR>union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B<VAR>sUnion_univ : ∀ (a : α), ∃ b ∈ B, a ∈ b<VAR>x : α<VAR>s : Set α<VAR>hs : s ∈ B<VAR>hxs : x ∈ s<GOAL>{x} ∈ B
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>inst✝ : (F ⋙ G).ReflectsIsomorphisms<VAR>A✝ B✝ : C<VAR>f : A✝ ⟶ B✝<VAR>x✝ : IsIso (F.map f)<GOAL>IsIso f
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>inst✝ : (F ⋙ G).ReflectsIsomorphisms<VAR>A✝ B✝ : C<VAR>f : A✝ ⟶ B✝<VAR>x✝ : IsIso (F.map f)<GOAL>IsIso ((F ⋙ G).map f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁸ : TopologicalSpace α<VAR>inst✝⁷ : TopologicalSpace β<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : LinearOrder β<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : OrderTopology β<VAR>inst✝² : DenselyOrdered α<VAR>inst✝¹ : NoMinOrder α<VAR>inst✝ : FirstCountableTopology α<VAR>x : α<GOAL>∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁸ : TopologicalSpace α<VAR>inst✝⁷ : TopologicalSpace β<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : LinearOrder β<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : OrderTopology β<VAR>inst✝² : DenselyOrdered α<VAR>inst✝¹ : NoMinOrder α<VAR>inst✝ : FirstCountableTopology α<VAR>x y : α<VAR>hy : y < x<GOAL>∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁸ : TopologicalSpace α<VAR>inst✝⁷ : TopologicalSpace β<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : LinearOrder β<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : OrderTopology β<VAR>inst✝² : DenselyOrdered α<VAR>inst✝¹ : NoMinOrder α<VAR>inst✝ : FirstCountableTopology α<VAR>x y : α<VAR>hy : y < x<VAR>u : ℕ → α<VAR>hu_mono : StrictMono u<VAR>hu_mem : ∀ (n : ℕ), u n ∈ Ioo y x<VAR>hux : Tendsto u atTop (𝓝 x)<GOAL>∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x)