ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ : Set α<VAR>f : α → β<VAR>s t : Set α<VAR>ht : t.Infinite<VAR>hst : s ⊆ t<VAR>hs : s.Finite<VAR>k : ℕ<VAR>hsk : s.ncard ≤ k<VAR>s₁ : Set α<VAR>hs₁ : s₁ ⊆ t \ s<VAR>hs₁fin : s₁.Finite<VAR>hs₁card : s₁.ncard = k - s.ncard<GOAL>(s ∪ s₁).ncard = k
<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 : a ≤ b<VAR>hb : 0 ≤ b<GOAL>a ≤ 1 * b
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : CompactSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>s : Set β<VAR>hs : IsCompact s<VAR>A : Set (α →ᵇ β)<VAR>closed : IsClosed A<VAR>in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s<VAR>H : Equicontinuous fun x => ⇑↑x<GOAL>IsCompact A
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : CompactSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>s : Set β<VAR>hs : IsCompact s<VAR>A : Set (α →ᵇ β)<VAR>closed : IsClosed A<VAR>in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s<VAR>H : Equicontinuous fun x => ⇑↑x<VAR>M : LipschitzWith 1 Subtype.val<GOAL>IsCompact A
<VAR>F✝ : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : CompactSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>s : Set β<VAR>hs : IsCompact s<VAR>A : Set (α →ᵇ β)<VAR>closed : IsClosed A<VAR>in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s<VAR>H : Equicontinuous fun x => ⇑↑x<VAR>M : LipschitzWith 1 Subtype.val<VAR>F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M<GOAL>IsCompact A
<VAR>F✝ : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : CompactSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>s : Set β<VAR>hs : IsCompact s<VAR>A : Set (α →ᵇ β)<VAR>closed : IsClosed A<VAR>in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s<VAR>H : Equicontinuous fun x => ⇑↑x<VAR>M : LipschitzWith 1 Subtype.val<VAR>F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M<GOAL>IsCompact (F ⁻¹' A)
<VAR>F✝ : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : CompactSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>f✝ g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>s : Set β<VAR>hs : IsCompact s<VAR>A : Set (α →ᵇ β)<VAR>closed : IsClosed A<VAR>in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s<VAR>H : Equicontinuous fun x => ⇑↑x<VAR>M : LipschitzWith 1 Subtype.val<VAR>F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M<VAR>f : α →ᵇ β<VAR>hf : f ∈ A<GOAL>f ∈ comp Subtype.val M '' (F ⁻¹' A)
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>g : P ≃ₗ[R] Q<VAR>f : N ≃ₗ[R] P<VAR>m : M<VAR>n : N<VAR>p : P<VAR>x : M ⊗[R] N<VAR>y : N ⊗[R] M<GOAL>(rTensor M (refl R N)) y = y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T25Space X<VAR>x y : X<VAR>h : x ≠ y<GOAL>∃ u, x ∈ u ∧ IsOpen u ∧ ∃ v, y ∈ v ∧ IsOpen v ∧ Disjoint (closure u) (closure v)
<VAR>z✝ w✝ : ℍ<VAR>r R : ℝ<VAR>z w : ℍ<GOAL>dist (mk { re := 0, im := z.im } ⋯) (mk { re := 0, im := w.im } ⋯) ≤ dist z w
<VAR>z✝ w✝ : ℍ<VAR>r R : ℝ<VAR>z w : ℍ<GOAL>2 * arsinh (dist ↑(mk { re := 0, im := z.im } ⋯) ↑(mk { re := 0, im := w.im } ⋯) / (2 * √((mk { re := 0, im := z.im } ⋯).im * (mk { re := 0, im := w.im } ⋯).im))) ≤ 2 * arsinh (dist ↑z ↑w / (2 * √(z.im * w.im)))
<VAR>z✝ w✝ : ℍ<VAR>r R : ℝ<VAR>z w : ℍ<GOAL>2 * arsinh (dist { re := 0, im := z.im } { re := 0, im := w.im } / (2 * √(z.im * w.im))) ≤ 2 * arsinh (dist ↑z ↑w / (2 * √(z.im * w.im)))
<VAR>z✝ w✝ : ℍ<VAR>r R : ℝ<VAR>z w : ℍ<GOAL>dist { re := 0, im := z.im } { re := 0, im := w.im } ≤ dist ↑z ↑w
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : CompleteSpace G<VAR>inst✝ : CompleteSpace F<VAR>A : E →L[𝕜] F<VAR>x : E<GOAL>‖A x‖ = √(re ⟪x, ((adjoint A).comp A) x⟫_𝕜)
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>K : ℝ<GOAL>∃ R, 0 < R ∧ ∀ (x : α) (t r : ℝ), t ∈ Ioc 0 K → r ≤ R → μ (closedBall x (t * r)) ≤ ↑(scalingConstantOf μ K) * μ (closedBall x r)
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>K : ℝ<VAR>h : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)<GOAL>∃ R, 0 < R ∧ ∀ (x : α) (t r : ℝ), t ∈ Ioc 0 K → r ≤ R → μ (closedBall x (t * r)) ≤ ↑(scalingConstantOf μ K) * μ (closedBall x r)
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>K : ℝ<VAR>h : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)<VAR>R : ℝ<VAR>Rpos : R ∈ Ioi 0<VAR>hR : Ioc 0 R ⊆ {x | (fun ε => ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)) x}<GOAL>∃ R, 0 < R ∧ ∀ (x : α) (t r : ℝ), t ∈ Ioc 0 K → r ≤ R → μ (closedBall x (t * r)) ≤ ↑(scalingConstantOf μ K) * μ (closedBall x r)
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>K : ℝ<VAR>h : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)<VAR>R : ℝ<VAR>Rpos : R ∈ Ioi 0<VAR>hR : Ioc 0 R ⊆ {x | (fun ε => ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)) x}<VAR>x : α<VAR>t r : ℝ<VAR>ht : t ∈ Ioc 0 K<VAR>hr : r ≤ R<GOAL>μ (closedBall x (t * r)) ≤ ↑(scalingConstantOf μ K) * μ (closedBall x r)
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>K : ℝ<VAR>h : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)<VAR>R : ℝ<VAR>Rpos : R ∈ Ioi 0<VAR>hR : Ioc 0 R ⊆ {x | (fun ε => ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)) x}<VAR>x : α<VAR>t r : ℝ<VAR>ht : t ∈ Ioc 0 K<VAR>hr : r ≤ R<VAR>rneg : r < 0<GOAL>μ (closedBall x (t * r)) ≤ ↑(scalingConstantOf μ K) * μ (closedBall x r)
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>K : ℝ<VAR>h : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)<VAR>R : ℝ<VAR>Rpos : R ∈ Ioi 0<VAR>hR : Ioc 0 R ⊆ {x | (fun ε => ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)) x}<VAR>x : α<VAR>t : ℝ<VAR>ht : t ∈ Ioc 0 K<VAR>hr : 0 ≤ R<GOAL>μ (closedBall x (t * 0)) ≤ ↑(scalingConstantOf μ K) * μ (closedBall x 0)
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>K : ℝ<VAR>h : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)<VAR>R : ℝ<VAR>Rpos : R ∈ Ioi 0<VAR>hR : Ioc 0 R ⊆ {x | (fun ε => ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)) x}<VAR>x : α<VAR>t r : ℝ<VAR>ht : t ∈ Ioc 0 K<VAR>hr : r ≤ R<VAR>rpos : 0 < r<GOAL>μ (closedBall x (t * r)) ≤ ↑(scalingConstantOf μ K) * μ (closedBall x r)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : PartialOrder β<VAR>inst✝ : OrderBot β<VAR>f : α → β<VAR>H : StrictMono f<VAR>a : α<VAR>h_bot : f a = ⊥<VAR>x : α<VAR>p : β<GOAL>⊥ ≤ p
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>g : P →ₗ[R] Q<VAR>f : N →ₗ[R] P<VAR>m : N<VAR>n : M<GOAL>(((TensorProduct.mk R N M).compr₂ (rTensor M (g ∘ₗ f))) m) n = (((TensorProduct.mk R N M).compr₂ (rTensor M g ∘ₗ rTensor M f)) m) n
<VAR>x y : ℝ<VAR>h : 1 < x * y<VAR>hx : x < 0<GOAL>arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π
<VAR>x y : ℝ<VAR>h : 1 < -x * -y<VAR>hx : x < 0<GOAL>arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π
<VAR>x y : ℝ<VAR>h : 1 < -x * -y<VAR>hx : x < 0<VAR>k : arctan (-x) + arctan (-y) = arctan ((-x + -y) / (1 - -x * -y)) + π<GOAL>arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π
<VAR>x y : ℝ<VAR>h : 1 < -x * -y<VAR>hx : x < 0<VAR>k : -(arctan (-x) + arctan (-y)) = -(arctan (-((x + y) / (1 - x * y))) + π)<GOAL>arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π
<VAR>x y : ℝ<VAR>h : 1 < -x * -y<VAR>hx : x < 0<VAR>k : arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π<GOAL>arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π
<VAR>n k : ℕ<VAR>x✝ : 2 ≤ k + 2<VAR>h : k + 2 ≤ n<GOAL>(n + 1 - (k + 2)) ^ (k + 2) < n.descFactorial (k + 2)
<VAR>n k : ℕ<VAR>x✝ : 2 ≤ k + 2<VAR>h : k + 2 ≤ n<GOAL>(n - (k + 1)) ^ (k + 2) < n.descFactorial (k + 2)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>h : ¬DifferentiableWithinAt 𝕜 f s x<GOAL>fderivWithin 𝕜 (fun y => -f y) s x = -fderivWithin 𝕜 f s x
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>h : ¬DifferentiableWithinAt 𝕜 f s x<GOAL>¬DifferentiableWithinAt 𝕜 (fun y => -f y) s x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>c : 𝕜<GOAL>c • closedBall 0 1 = closedBall 0 ‖c‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace β<VAR>f : α → β<VAR>a : α<GOAL>map f (𝓝 a) = 𝓝[range f] f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f✝ : α → β<VAR>inst✝ : Finite ι<VAR>hp_one : 1 ≤ p<VAR>hp_top : p ≠ ⊤<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), Memℒp (f i) p μ<GOAL>UnifIntegrable f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f✝ : α → β<VAR>inst✝ : Finite ι<VAR>hp_one : 1 ≤ p<VAR>hp_top : p ≠ ⊤<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), Memℒp (f i) p μ<VAR>n : ℕ<VAR>hn : Nonempty (ι ≃ Fin n)<GOAL>UnifIntegrable f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f✝ : α → β<VAR>inst✝ : Finite ι<VAR>hp_one : 1 ≤ p<VAR>hp_top : p ≠ ⊤<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), Memℒp (f i) p μ<VAR>n : ℕ<VAR>hn : Nonempty (ι ≃ Fin n)<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>g : Fin n → α → β := f ∘ ⇑hn.some.symm<VAR>hg : ∀ (i : Fin n), Memℒp (g i) p μ<GOAL>∃ δ, ∃ (_ : 0 < δ), ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f✝ : α → β<VAR>inst✝ : Finite ι<VAR>hp_one : 1 ≤ p<VAR>hp_top : p ≠ ⊤<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), Memℒp (f i) p μ<VAR>n : ℕ<VAR>hn : Nonempty (ι ≃ Fin n)<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>g : Fin n → α → β := f ∘ ⇑hn.some.symm<VAR>hg : ∀ (i : Fin n), Memℒp (g i) p μ<VAR>δ : ℝ<VAR>hδpos : 0 < δ<VAR>hδ : ∀ (i : Fin n) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε<GOAL>∃ δ, ∃ (_ : 0 < δ), ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f✝ : α → β<VAR>inst✝ : Finite ι<VAR>hp_one : 1 ≤ p<VAR>hp_top : p ≠ ⊤<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), Memℒp (f i) p μ<VAR>n : ℕ<VAR>hn : Nonempty (ι ≃ Fin n)<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>g : Fin n → α → β := f ∘ ⇑hn.some.symm<VAR>hg : ∀ (i : Fin n), Memℒp (g i) p μ<VAR>δ : ℝ<VAR>hδpos : 0 < δ<VAR>i : ι<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≤ ENNReal.ofReal δ<VAR>hδ : eLpNorm (s.indicator (g (hn.some i))) p μ ≤ ENNReal.ofReal ε<GOAL>eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f✝ : α → β<VAR>inst✝ : Finite ι<VAR>hp_one : 1 ≤ p<VAR>hp_top : p ≠ ⊤<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), Memℒp (f i) p μ<VAR>n : ℕ<VAR>hn : Nonempty (ι ≃ Fin n)<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>g : Fin n → α → β := f ∘ ⇑hn.some.symm<VAR>hg : ∀ (i : Fin n), Memℒp (g i) p μ<VAR>δ : ℝ<VAR>hδpos : 0 < δ<VAR>i : ι<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≤ ENNReal.ofReal δ<VAR>hδ : eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε<GOAL>eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>inst✝ : AddCommGroup α<VAR>p a a₁ a₂ b b₁ b₂ c : α<VAR>n : ℕ<VAR>z : ℤ<GOAL>a + b ≡ b [PMOD p] ↔ a ≡ 0 [PMOD p]
<VAR>R✝ : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R✝<VAR>e : ℕ<VAR>n m : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝² : CommSemiring R✝<VAR>p q : MvPolynomial σ R✝<VAR>R : Type u_3<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Nontrivial R<VAR>s : σ<GOAL>(X s).totalDegree = 1
<VAR>R✝ : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R✝<VAR>e : ℕ<VAR>n m : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝² : CommSemiring R✝<VAR>p q : MvPolynomial σ R✝<VAR>R : Type u_3<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Nontrivial R<VAR>s : σ<GOAL>({Finsupp.single s 1}.sup fun s => s.sum fun x e => e) = 1
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Ring R<VAR>inst✝¹ : LinearOrderedField k<VAR>abv : R → k<VAR>inst✝ : IsAbsoluteValue abv<VAR>p : R[X]<VAR>h : 0 < p.degree<VAR>l : Filter α<VAR>z : α → R<VAR>hz : Tendsto (abv ∘ z) l atTop<GOAL>Tendsto (fun x => abv (eval (z x) p)) l atTop
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Ring R<VAR>inst✝¹ : LinearOrderedField k<VAR>abv : R → k<VAR>inst✝ : IsAbsoluteValue abv<VAR>p : R[X]<VAR>h : 0 < p.degree<VAR>l : Filter α<VAR>z : α → R<VAR>hz : Tendsto (abv ∘ z) l atTop<GOAL>(RingHom.id R) p.leadingCoeff ≠ 0
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : (i : ι) → DecidableEq (α i)<VAR>inst✝² : (i : ι) → Lattice (α i)<VAR>inst✝¹ : (i : ι) → Zero (α i)<VAR>inst✝ : (i : ι) → LocallyFiniteOrder (α i)<VAR>f g : Π₀ (i : ι), α i<GOAL>(uIcc f g).card = ∏ i ∈ f.support ∪ g.support, (uIcc (f i) (g i)).card
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : (i : ι) → DecidableEq (α i)<VAR>inst✝² : (i : ι) → Lattice (α i)<VAR>inst✝¹ : (i : ι) → Zero (α i)<VAR>inst✝ : (i : ι) → LocallyFiniteOrder (α i)<VAR>f g : Π₀ (i : ι), α i<GOAL>(uIcc f g).card = ∏ i ∈ (f ⊓ g).support ∪ (f ⊔ g).support, (uIcc (f i) (g i)).card
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝¹ : Category.{u_3, u_1} D<VAR>P : MorphismProperty C<VAR>F : C ⥤ D<VAR>E : Type u_2<VAR>inst✝ : Category.{u_4, u_2} E<VAR>G : D ⥤ E<GOAL>(P.map F).map G = P.map (F ⋙ G)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝¹ : Category.{u_3, u_1} D<VAR>P : MorphismProperty C<VAR>F : C ⥤ D<VAR>E : Type u_2<VAR>inst✝ : Category.{u_4, u_2} E<VAR>G : D ⥤ E<GOAL>(P.map F).map G ≤ P.map (F ⋙ G)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝¹ : Category.{u_3, u_1} D<VAR>P : MorphismProperty C<VAR>F : C ⥤ D<VAR>E : Type u_2<VAR>inst✝ : Category.{u_4, u_2} E<VAR>G : D ⥤ E<GOAL>P.map (F ⋙ G) ≤ (P.map F).map G
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝ : Category.{u_2, u_1} D<VAR>P : MorphismProperty C<GOAL>∀ {F G : C ⥤ D}, (F ≅ G) → P.map F = P.map G
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝ : Category.{u_2, u_1} D<VAR>P : MorphismProperty C<GOAL>∀ {F G : C ⥤ D}, (F ≅ G) → P.map F ≤ P.map G
<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>κ : Kernel (α × β) Ω<VAR>inst✝ : IsFiniteKernel κ<VAR>hκ : ρ.fst ⊗ₖ κ = ρ<VAR>a : α<GOAL>∀ᵐ (x : β) ∂ρ.fst a, κ (a, x) = ρ.condKernel (a, x)
<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>κ : Kernel (α × β) Ω<VAR>inst✝ : IsFiniteKernel κ<VAR>hκ : ρ.fst ⊗ₖ κ = ρ<VAR>a✝ : α<VAR>a : β<VAR>h1 : ρ.condKernel (a✝, a) = (ρ a✝).condKernel a<VAR>h2 : κ (a✝, a) = (ρ a✝).condKernel a<GOAL>κ (a✝, a) = ρ.condKernel (a✝, a)
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<GOAL>1 = Nat.unaryCast 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>p₁ p₂ p₃ : P<GOAL>AffineIndependent k ![p₁, p₂, p₃] ↔ ¬Collinear k {p₁, p₂, p₃}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>p₁ p₂ p₃ : P<GOAL>¬Collinear k (Set.range ![p₁, p₂, p₃]) ↔ ¬Collinear k {p₁, p₂, p₃}
<VAR>α✝ : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : MeasurableSpace M<VAR>inst✝ : MeasurableMul₂ M<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : ι → α → M<VAR>s : Multiset (α → M)<VAR>hs : ∀ f ∈ s, AEMeasurable f μ<GOAL>AEMeasurable (fun x => (map (fun f => f x) s).prod) μ
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<GOAL>ball 1 δ * {x} = ball x δ
<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>G' : Type u_7<VAR>G'' : Type u_8<VAR>inst✝³ : NormedLatticeAddCommGroup G''<VAR>inst✝² : NormedSpace ℝ G''<VAR>inst✝¹ : NormedLatticeAddCommGroup G'<VAR>inst✝ : NormedSpace ℝ G'<VAR>T : Set α → G' →L[ℝ] G''<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f : α →ₛ G'<VAR>hf : 0 ≤ f<VAR>hfi : Integrable (↑f) μ<GOAL>0 ≤ setToSimpleFunc T f
<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>G' : Type u_7<VAR>G'' : Type u_8<VAR>inst✝³ : NormedLatticeAddCommGroup G''<VAR>inst✝² : NormedSpace ℝ G''<VAR>inst✝¹ : NormedLatticeAddCommGroup G'<VAR>inst✝ : NormedSpace ℝ G'<VAR>T : Set α → G' →L[ℝ] G''<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f : α →ₛ G'<VAR>hf : 0 ≤ f<VAR>hfi : Integrable (↑f) μ<VAR>i : G'<VAR>hi : i ∈ f.range<GOAL>0 ≤ (T (↑f ⁻¹' {i})) i
<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>G' : Type u_7<VAR>G'' : Type u_8<VAR>inst✝³ : NormedLatticeAddCommGroup G''<VAR>inst✝² : NormedSpace ℝ G''<VAR>inst✝¹ : NormedLatticeAddCommGroup G'<VAR>inst✝ : NormedSpace ℝ G'<VAR>T : Set α → G' →L[ℝ] G''<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f : α →ₛ G'<VAR>hf : 0 ≤ f<VAR>hfi : Integrable (↑f) μ<VAR>i : G'<VAR>hi : i ∈ f.range<VAR>h0 : ¬i = 0<GOAL>0 ≤ (T (↑f ⁻¹' {i})) i
<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>G' : Type u_7<VAR>G'' : Type u_8<VAR>inst✝³ : NormedLatticeAddCommGroup G''<VAR>inst✝² : NormedSpace ℝ G''<VAR>inst✝¹ : NormedLatticeAddCommGroup G'<VAR>inst✝ : NormedSpace ℝ G'<VAR>T : Set α → G' →L[ℝ] G''<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f : α →ₛ G'<VAR>hf : 0 ≤ f<VAR>hfi : Integrable (↑f) μ<VAR>i : G'<VAR>hi : i ∈ f.range<VAR>h0 : ¬i = 0<GOAL>0 ≤ i
<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>G' : Type u_7<VAR>G'' : Type u_8<VAR>inst✝³ : NormedLatticeAddCommGroup G''<VAR>inst✝² : NormedSpace ℝ G''<VAR>inst✝¹ : NormedLatticeAddCommGroup G'<VAR>inst✝ : NormedSpace ℝ G'<VAR>T : Set α → G' →L[ℝ] G''<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f : α →ₛ G'<VAR>hf : 0 ≤ f<VAR>hfi : Integrable (↑f) μ<VAR>i : G'<VAR>hi : i ∈ Set.range ↑f<VAR>h0 : ¬i = 0<GOAL>0 ≤ i