ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝²⁶ : NormedAddCommGroup E<VAR>inst✝²⁵ : NormedAddCommGroup E'<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝²² : RCLike 𝕜<VAR>inst✝²¹ : NormedSpace 𝕜 E<VAR>inst✝²⁰ : NormedSpace 𝕜 E'<VAR>inst✝¹⁹ : NormedSpace 𝕜 E''<VAR>inst✝¹⁸ : NormedSpace ℝ F<VAR>inst✝¹⁷ : NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>inst✝¹⁶ : CompleteSpace F<VAR>inst✝¹⁵ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹⁴ : NormedAddCommGroup F'<VAR>inst✝¹³ : NormedSpace ℝ F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>inst✝¹¹ : CompleteSpace F'<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedSpace ℝ F''<VAR>inst✝⁸ : NormedSpace 𝕜 F''<VAR>inst✝⁷ : CompleteSpace F''<VAR>k : G → E''<VAR>L₂ : F →L[𝕜] E'' →L[𝕜] F'<VAR>L₃ : E →L[𝕜] F'' →L[𝕜] F'<VAR>L₄ : E' →L[𝕜] E'' →L[𝕜] F''<VAR>inst✝⁶ : AddGroup G<VAR>inst✝⁵ : SFinite μ<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : μ.IsAddRightInvariant<VAR>inst✝² : MeasurableAdd₂ G<VAR>inst✝¹ : ν.IsAddRightInvariant<VAR>inst✝ : MeasurableNeg G<VAR>hL : ∀ (x : E) (y : E') (z : E''), (L₂ ((L x) y)) z = (L₃ x) ((L₄ y) z)<VAR>x₀ : G<VAR>hf : AEStronglyMeasurable f ν<VAR>hg : AEStronglyMeasurable g μ<VAR>hk : AEStronglyMeasurable k μ<VAR>hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν<VAR>hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt (fun x => ‖g x‖) (fun x => ‖k x‖) x (mul ℝ ℝ) μ<VAR>hfgk : ConvolutionExistsAt (fun x => ‖f x‖) ((fun x => ‖g x‖) ⋆[mul ℝ ℝ, μ] fun x => ‖k x‖) x₀ (mul ℝ ℝ) ν<VAR>h_meas : AEStronglyMeasurable (uncurry fun x y => (L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))) (μ.prod ν)<VAR>h2_meas : AEStronglyMeasurable (fun y => ∫ (x : G), ‖(L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))‖ ∂μ) ν<VAR>h3 : Measure.map (fun z => (z.1 - z.2, z.2)) (μ.prod ν) = μ.prod ν<VAR>t : G<VAR>ht : ConvolutionExistsAt (fun x => ‖g x‖) (fun x => ‖k x‖) (x₀ - t) (mul ℝ ℝ) μ<GOAL>‖∫ (x : G), ‖uncurry (fun x y => (L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))) (x, t)‖ ∂μ‖ ≤ ‖L₃‖ * ‖L₄‖ * ((mul ℝ ℝ) ((fun x => ‖f x‖) t)) (((fun x => ‖g x‖) ⋆[mul ℝ ℝ, μ] fun x => ‖k x‖) (x₀ - t))
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝²⁶ : NormedAddCommGroup E<VAR>inst✝²⁵ : NormedAddCommGroup E'<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝²² : RCLike 𝕜<VAR>inst✝²¹ : NormedSpace 𝕜 E<VAR>inst✝²⁰ : NormedSpace 𝕜 E'<VAR>inst✝¹⁹ : NormedSpace 𝕜 E''<VAR>inst✝¹⁸ : NormedSpace ℝ F<VAR>inst✝¹⁷ : NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>inst✝¹⁶ : CompleteSpace F<VAR>inst✝¹⁵ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹⁴ : NormedAddCommGroup F'<VAR>inst✝¹³ : NormedSpace ℝ F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>inst✝¹¹ : CompleteSpace F'<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedSpace ℝ F''<VAR>inst✝⁸ : NormedSpace 𝕜 F''<VAR>inst✝⁷ : CompleteSpace F''<VAR>k : G → E''<VAR>L₂ : F →L[𝕜] E'' →L[𝕜] F'<VAR>L₃ : E →L[𝕜] F'' →L[𝕜] F'<VAR>L₄ : E' →L[𝕜] E'' →L[𝕜] F''<VAR>inst✝⁶ : AddGroup G<VAR>inst✝⁵ : SFinite μ<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : μ.IsAddRightInvariant<VAR>inst✝² : MeasurableAdd₂ G<VAR>inst✝¹ : ν.IsAddRightInvariant<VAR>inst✝ : MeasurableNeg G<VAR>hL : ∀ (x : E) (y : E') (z : E''), (L₂ ((L x) y)) z = (L₃ x) ((L₄ y) z)<VAR>x₀ : G<VAR>hf : AEStronglyMeasurable f ν<VAR>hg : AEStronglyMeasurable g μ<VAR>hk : AEStronglyMeasurable k μ<VAR>hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν<VAR>hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt (fun x => ‖g x‖) (fun x => ‖k x‖) x (mul ℝ ℝ) μ<VAR>hfgk : ConvolutionExistsAt (fun x => ‖f x‖) ((fun x => ‖g x‖) ⋆[mul ℝ ℝ, μ] fun x => ‖k x‖) x₀ (mul ℝ ℝ) ν<VAR>h_meas : AEStronglyMeasurable (uncurry fun x y => (L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))) (μ.prod ν)<VAR>h2_meas : AEStronglyMeasurable (fun y => ∫ (x : G), ‖(L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))‖ ∂μ) ν<VAR>h3 : Measure.map (fun z => (z.1 - z.2, z.2)) (μ.prod ν) = μ.prod ν<VAR>t : G<VAR>ht : ConvolutionExistsAt (fun x => ‖g x‖) (fun x => ‖k x‖) (x₀ - t) (mul ℝ ℝ) μ<GOAL>‖∫ (x : G), ‖uncurry (fun x y => (L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))) (x, t)‖ ∂μ‖ ≤ ∫ (a : G), ‖L₃‖ * ‖f t‖ * (‖L₄‖ * (‖g a‖ * ‖k (x₀ - t - a)‖)) ∂μ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝²⁶ : NormedAddCommGroup E<VAR>inst✝²⁵ : NormedAddCommGroup E'<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝²² : RCLike 𝕜<VAR>inst✝²¹ : NormedSpace 𝕜 E<VAR>inst✝²⁰ : NormedSpace 𝕜 E'<VAR>inst✝¹⁹ : NormedSpace 𝕜 E''<VAR>inst✝¹⁸ : NormedSpace ℝ F<VAR>inst✝¹⁷ : NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>inst✝¹⁶ : CompleteSpace F<VAR>inst✝¹⁵ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹⁴ : NormedAddCommGroup F'<VAR>inst✝¹³ : NormedSpace ℝ F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>inst✝¹¹ : CompleteSpace F'<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedSpace ℝ F''<VAR>inst✝⁸ : NormedSpace 𝕜 F''<VAR>inst✝⁷ : CompleteSpace F''<VAR>k : G → E''<VAR>L₂ : F →L[𝕜] E'' →L[𝕜] F'<VAR>L₃ : E →L[𝕜] F'' →L[𝕜] F'<VAR>L₄ : E' →L[𝕜] E'' →L[𝕜] F''<VAR>inst✝⁶ : AddGroup G<VAR>inst✝⁵ : SFinite μ<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : μ.IsAddRightInvariant<VAR>inst✝² : MeasurableAdd₂ G<VAR>inst✝¹ : ν.IsAddRightInvariant<VAR>inst✝ : MeasurableNeg G<VAR>hL : ∀ (x : E) (y : E') (z : E''), (L₂ ((L x) y)) z = (L₃ x) ((L₄ y) z)<VAR>x₀ : G<VAR>hf : AEStronglyMeasurable f ν<VAR>hg : AEStronglyMeasurable g μ<VAR>hk : AEStronglyMeasurable k μ<VAR>hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν<VAR>hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt (fun x => ‖g x‖) (fun x => ‖k x‖) x (mul ℝ ℝ) μ<VAR>hfgk : ConvolutionExistsAt (fun x => ‖f x‖) ((fun x => ‖g x‖) ⋆[mul ℝ ℝ, μ] fun x => ‖k x‖) x₀ (mul ℝ ℝ) ν<VAR>h_meas : AEStronglyMeasurable (uncurry fun x y => (L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))) (μ.prod ν)<VAR>h2_meas : AEStronglyMeasurable (fun y => ∫ (x : G), ‖(L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))‖ ∂μ) ν<VAR>h3 : Measure.map (fun z => (z.1 - z.2, z.2)) (μ.prod ν) = μ.prod ν<VAR>t : G<VAR>ht : ConvolutionExistsAt (fun x => ‖g x‖) (fun x => ‖k x‖) (x₀ - t) (mul ℝ ℝ) μ<GOAL>∫ (x : G), ‖uncurry (fun x y => (L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))) (x, t)‖ ∂μ ≤ ∫ (a : G), ‖L₃‖ * ‖f t‖ * (‖L₄‖ * (‖g a‖ * ‖k (x₀ - t - a)‖)) ∂μ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝²⁶ : NormedAddCommGroup E<VAR>inst✝²⁵ : NormedAddCommGroup E'<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝²² : RCLike 𝕜<VAR>inst✝²¹ : NormedSpace 𝕜 E<VAR>inst✝²⁰ : NormedSpace 𝕜 E'<VAR>inst✝¹⁹ : NormedSpace 𝕜 E''<VAR>inst✝¹⁸ : NormedSpace ℝ F<VAR>inst✝¹⁷ : NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>inst✝¹⁶ : CompleteSpace F<VAR>inst✝¹⁵ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹⁴ : NormedAddCommGroup F'<VAR>inst✝¹³ : NormedSpace ℝ F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>inst✝¹¹ : CompleteSpace F'<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedSpace ℝ F''<VAR>inst✝⁸ : NormedSpace 𝕜 F''<VAR>inst✝⁷ : CompleteSpace F''<VAR>k : G → E''<VAR>L₂ : F →L[𝕜] E'' →L[𝕜] F'<VAR>L₃ : E →L[𝕜] F'' →L[𝕜] F'<VAR>L₄ : E' →L[𝕜] E'' →L[𝕜] F''<VAR>inst✝⁶ : AddGroup G<VAR>inst✝⁵ : SFinite μ<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : μ.IsAddRightInvariant<VAR>inst✝² : MeasurableAdd₂ G<VAR>inst✝¹ : ν.IsAddRightInvariant<VAR>inst✝ : MeasurableNeg G<VAR>hL : ∀ (x : E) (y : E') (z : E''), (L₂ ((L x) y)) z = (L₃ x) ((L₄ y) z)<VAR>x₀ : G<VAR>hf : AEStronglyMeasurable f ν<VAR>hg : AEStronglyMeasurable g μ<VAR>hk : AEStronglyMeasurable k μ<VAR>hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν<VAR>hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt (fun x => ‖g x‖) (fun x => ‖k x‖) x (mul ℝ ℝ) μ<VAR>hfgk : ConvolutionExistsAt (fun x => ‖f x‖) ((fun x => ‖g x‖) ⋆[mul ℝ ℝ, μ] fun x => ‖k x‖) x₀ (mul ℝ ℝ) ν<VAR>h_meas : AEStronglyMeasurable (uncurry fun x y => (L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))) (μ.prod ν)<VAR>h2_meas : AEStronglyMeasurable (fun y => ∫ (x : G), ‖(L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))‖ ∂μ) ν<VAR>h3 : Measure.map (fun z => (z.1 - z.2, z.2)) (μ.prod ν) = μ.prod ν<VAR>t : G<VAR>ht : ConvolutionExistsAt (fun x => ‖g x‖) (fun x => ‖k x‖) (x₀ - t) (mul ℝ ℝ) μ<VAR>s : G<GOAL>(fun x => ‖uncurry (fun x y => (L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))) (x, t)‖) s ≤ (fun a => ‖L₃‖ * ‖f t‖ * (‖L₄‖ * (‖g a‖ * ‖k (x₀ - t - a)‖))) s
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝²⁶ : NormedAddCommGroup E<VAR>inst✝²⁵ : NormedAddCommGroup E'<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝²² : RCLike 𝕜<VAR>inst✝²¹ : NormedSpace 𝕜 E<VAR>inst✝²⁰ : NormedSpace 𝕜 E'<VAR>inst✝¹⁹ : NormedSpace 𝕜 E''<VAR>inst✝¹⁸ : NormedSpace ℝ F<VAR>inst✝¹⁷ : NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>inst✝¹⁶ : CompleteSpace F<VAR>inst✝¹⁵ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹⁴ : NormedAddCommGroup F'<VAR>inst✝¹³ : NormedSpace ℝ F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>inst✝¹¹ : CompleteSpace F'<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedSpace ℝ F''<VAR>inst✝⁸ : NormedSpace 𝕜 F''<VAR>inst✝⁷ : CompleteSpace F''<VAR>k : G → E''<VAR>L₂ : F →L[𝕜] E'' →L[𝕜] F'<VAR>L₃ : E →L[𝕜] F'' →L[𝕜] F'<VAR>L₄ : E' →L[𝕜] E'' →L[𝕜] F''<VAR>inst✝⁶ : AddGroup G<VAR>inst✝⁵ : SFinite μ<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : μ.IsAddRightInvariant<VAR>inst✝² : MeasurableAdd₂ G<VAR>inst✝¹ : ν.IsAddRightInvariant<VAR>inst✝ : MeasurableNeg G<VAR>hL : ∀ (x : E) (y : E') (z : E''), (L₂ ((L x) y)) z = (L₃ x) ((L₄ y) z)<VAR>x₀ : G<VAR>hf : AEStronglyMeasurable f ν<VAR>hg : AEStronglyMeasurable g μ<VAR>hk : AEStronglyMeasurable k μ<VAR>hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν<VAR>hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt (fun x => ‖g x‖) (fun x => ‖k x‖) x (mul ℝ ℝ) μ<VAR>hfgk : ConvolutionExistsAt (fun x => ‖f x‖) ((fun x => ‖g x‖) ⋆[mul ℝ ℝ, μ] fun x => ‖k x‖) x₀ (mul ℝ ℝ) ν<VAR>h_meas : AEStronglyMeasurable (uncurry fun x y => (L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))) (μ.prod ν)<VAR>h2_meas : AEStronglyMeasurable (fun y => ∫ (x : G), ‖(L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))‖ ∂μ) ν<VAR>h3 : Measure.map (fun z => (z.1 - z.2, z.2)) (μ.prod ν) = μ.prod ν<VAR>t : G<VAR>ht : ConvolutionExistsAt (fun x => ‖g x‖) (fun x => ‖k x‖) (x₀ - t) (mul ℝ ℝ) μ<VAR>s : G<GOAL>‖uncurry (fun x y => (L₃ (f y)) ((L₄ (g x)) (k (x₀ - y - x)))) (s, t)‖ ≤ ‖L₃‖ * ‖f t‖ * (‖L₄‖ * ‖g s‖ * ‖k (x₀ - t - s)‖)
<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 N : Set α<VAR>f : α → ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hμ : μ ≠ 0<VAR>hf : Integrable f μ<GOAL>0 < μ {x | ⨍ (a : α), f a ∂μ ≤ f x}
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s t u v : Set α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>hf : _root_.Embedding f<GOAL>IsTotallyDisconnected (range f) ↔ TotallyDisconnectedSpace α
<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>ιM : Type u_7<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup L<VAR>inst✝⁹ : Module R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Fintype ι'<VAR>inst✝⁴ : Fintype ιM<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : DecidableEq ι'<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>b : Basis ι R L<VAR>x : L<VAR>i : ℕ<GOAL>(MvPolynomial.eval ⇑(b.repr x)) ((φ.polyCharpoly b).coeff i) = (charpoly (φ x)).coeff i
<VAR>n : ℕ<VAR>Δ : SimplexCategory<VAR>θ : Δ ⟶ [n + 1]<VAR>hθ : ¬Function.Surjective ⇑(Hom.toOrderHom θ)<GOAL>∃ i θ', θ = θ' ≫ δ i
<VAR>n : ℕ<VAR>Δ : SimplexCategory<VAR>θ : Δ ⟶ [n + 1]<VAR>hθ : ¬Function.Surjective ⇑(Hom.toOrderHom θ)<VAR>i : Fin ([n + 1].len + 1)<VAR>hi : ¬∃ a, (Hom.toOrderHom θ) a = i<GOAL>∃ i θ', θ = θ' ≫ δ i
<VAR>n : ℕ<VAR>Δ : SimplexCategory<VAR>θ : Δ ⟶ [n + 1]<VAR>hθ : ¬Function.Surjective ⇑(Hom.toOrderHom θ)<VAR>i : Fin ([n + 1].len + 1)<VAR>hi : ¬∃ a, (Hom.toOrderHom θ) a = i<GOAL>∃ θ', θ = θ' ≫ δ i
<VAR>S X₁ X₂ : Type u<VAR>f : S ⟶ X₁<VAR>g : S ⟶ X₂<VAR>inst✝ : Mono f<VAR>x₁ : X₁<VAR>x₂ : X₂<GOAL>inl f g x₁ = inr f g x₂ ↔ ∃ s, f s = x₁ ∧ g s = x₂
<VAR>S X₁ X₂ : Type u<VAR>f : S ⟶ X₁<VAR>g : S ⟶ X₂<VAR>inst✝ : Mono f<VAR>x₁ : X₁<VAR>x₂ : X₂<GOAL>Rel' f g (Sum.inl x₁) (Sum.inr x₂) ↔ ∃ s, f s = x₁ ∧ g s = x₂
<VAR>n : ℕ<VAR>θ : [n] ⟶ [n + 1]<VAR>inst✝ : Mono θ<GOAL>∃ i, θ = δ i
<VAR>n : ℕ<VAR>θ : [n] ⟶ [n + 1]<VAR>inst✝ : Mono θ<VAR>i : Fin (n + 2)<VAR>θ' : [n] ⟶ [n]<VAR>h : θ = θ' ≫ δ i<GOAL>∃ i, θ = δ i
<VAR>n : ℕ<VAR>θ : [n] ⟶ [n + 1]<VAR>inst✝ : Mono θ<VAR>i : Fin (n + 2)<VAR>θ' : [n] ⟶ [n]<VAR>h : θ = θ' ≫ δ i<GOAL>θ = δ i
<VAR>n : ℕ<VAR>θ : [n] ⟶ [n + 1]<VAR>inst✝ : Mono θ<VAR>i : Fin (n + 2)<VAR>θ' : [n] ⟶ [n]<VAR>h : θ = θ' ≫ δ i<VAR>this : Mono (θ' ≫ δ i)<GOAL>θ = δ i
<VAR>n : ℕ<VAR>θ : [n] ⟶ [n + 1]<VAR>inst✝ : Mono θ<VAR>i : Fin (n + 2)<VAR>θ' : [n] ⟶ [n]<VAR>h : θ = θ' ≫ δ i<VAR>this✝ : Mono (θ' ≫ δ i)<VAR>this : Mono θ'<GOAL>θ = δ i
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>hcb : z ≤ y<GOAL>(x \ z) \ (y \ z) = x \ y
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>hcb : z ≤ y<GOAL>(x \ z) \ (x \ y) ≤ y \ z ∧ x \ y ≤ (x \ z) \ (y \ z)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>a b c d x y z : F<VAR>r R : ℝ<VAR>hx : x ≠ c<GOAL>HasFDerivAt (inversion c R) ((R / dist x c) ^ 2 • ↑{ toLinearEquiv := (reflection (Submodule.span ℝ {x - c})ᗮ).toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }) x
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>a b c d y z : F<VAR>r R : ℝ<VAR>x : F<VAR>hx : (fun x => c + x) x ≠ c<GOAL>HasFDerivAt (inversion c R) ((R / dist ((fun x => c + x) x) c) ^ 2 • ↑{ toLinearEquiv := (reflection (Submodule.span ℝ {(fun x => c + x) x - c})ᗮ).toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }) ((fun x => c + x) x)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>a b c d y z : F<VAR>r R : ℝ<VAR>x : F<VAR>hx : (fun x => c + x) x ≠ c<VAR>this : HasFDerivAt (inversion c R) ((R ^ 2 * ((fun y => y⁻¹) ∘ fun x => ‖_root_.id x - c‖ ^ 2) (c + x)) • ContinuousLinearMap.id ℝ F + (R ^ 2 • -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ • 2 • ((innerSL ℝ) (_root_.id (c + x) - c)).comp (ContinuousLinearMap.id ℝ F)).smulRight (_root_.id (c + x) - c)) (c + x)<GOAL>HasFDerivAt (inversion c R) ((R / dist ((fun x => c + x) x) c) ^ 2 • ↑{ toLinearEquiv := (reflection (Submodule.span ℝ {(fun x => c + x) x - c})ᗮ).toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }) ((fun x => c + x) x)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>a b c d y z : F<VAR>r R : ℝ<VAR>x : F<VAR>hx : (fun x => c + x) x ≠ c<VAR>this : HasFDerivAt (inversion c R) ((R ^ 2 * ((fun y => y⁻¹) ∘ fun x => ‖_root_.id x - c‖ ^ 2) (c + x)) • ContinuousLinearMap.id ℝ F + (R ^ 2 • -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ • 2 • ((innerSL ℝ) (_root_.id (c + x) - c)).comp (ContinuousLinearMap.id ℝ F)).smulRight (_root_.id (c + x) - c)) (c + x)<GOAL>EqOn ⇑((R ^ 2 * ((fun y => y⁻¹) ∘ fun x => ‖_root_.id x - c‖ ^ 2) (c + x)) • ContinuousLinearMap.id ℝ F + (R ^ 2 • -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ • 2 • ((innerSL ℝ) (_root_.id (c + x) - c)).comp (ContinuousLinearMap.id ℝ F)).smulRight (_root_.id (c + x) - c)) ⇑((R / dist ((fun x => c + x) x) c) ^ 2 • ↑{ toLinearEquiv := (reflection (Submodule.span ℝ {(fun x => c + x) x - c})ᗮ).toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }) {x}
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>a b c d y✝ z : F<VAR>r R : ℝ<VAR>x : F<VAR>hx : (fun x => c + x) x ≠ c<VAR>this : HasFDerivAt (inversion c R) ((R ^ 2 * ((fun y => y⁻¹) ∘ fun x => ‖_root_.id x - c‖ ^ 2) (c + x)) • ContinuousLinearMap.id ℝ F + (R ^ 2 • -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ • 2 • ((innerSL ℝ) (_root_.id (c + x) - c)).comp (ContinuousLinearMap.id ℝ F)).smulRight (_root_.id (c + x) - c)) (c + x)<VAR>y : F<VAR>hy : y ∈ ↑(Submodule.span ℝ {x})ᗮ<GOAL>((R ^ 2 * ((fun y => y⁻¹) ∘ fun x => ‖_root_.id x - c‖ ^ 2) (c + x)) • ContinuousLinearMap.id ℝ F + (R ^ 2 • -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ • 2 • ((innerSL ℝ) (_root_.id (c + x) - c)).comp (ContinuousLinearMap.id ℝ F)).smulRight (_root_.id (c + x) - c)) y = ((R / dist ((fun x => c + x) x) c) ^ 2 • ↑{ toLinearEquiv := (reflection (Submodule.span ℝ {(fun x => c + x) x - c})ᗮ).toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }) y
<VAR>V : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f g✝ : NormedAddGroupHom V₁ V₂<VAR>g : NormedAddGroupHom V₂ V₃<VAR>C₁ C₂ : ℝ<VAR>hg : ‖g‖ ≤ C₂<VAR>hf : ‖f‖ ≤ C₁<GOAL>0 ≤ C₂
<VAR>M✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹ : Monoid M✝<VAR>a : M✝<VAR>M : Type u_4<VAR>inst✝ : CommMonoid M<VAR>s : Set M<VAR>x : M<VAR>hx : x ∈ closure s<GOAL>∃ l, (∀ y ∈ l, y ∈ s) ∧ l.prod = x
<VAR>M✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹ : Monoid M✝<VAR>a : M✝<VAR>M : Type u_4<VAR>inst✝ : CommMonoid M<VAR>s : Set M<VAR>x : M<VAR>hx : x ∈ closure s<VAR>l : List M<VAR>h1 : ∀ y ∈ l, y ∈ s<VAR>h2 : l.prod = x<GOAL>∃ l, (∀ y ∈ l, y ∈ s) ∧ l.prod = x
<VAR>x : ℂ<VAR>y : ℝ<GOAL>(x ^ ↑y).re = abs x ^ y * Real.cos (x.arg * y)
<VAR>x : ℂ<VAR>y : ℝ<GOAL>(↑(abs x ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)).re = abs x ^ y * Real.cos (x.arg * y)
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>h : sSup S = ⊤<GOAL>S = {a | IsAtom a}
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>h : sSup S = ⊤<GOAL>S ≤ {a | IsAtom a}
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>h : sSup S = ⊤<GOAL>{a | IsAtom a} ≤ S
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>h : sSup S = ⊤<VAR>a : α<VAR>ha : a ∈ {a | IsAtom a}<GOAL>a ∈ S
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>h : sSup S = ⊤<VAR>T : Set α<VAR>hT : T ⊆ S<VAR>ha : sSup T ∈ {a | IsAtom a}<GOAL>sSup T ∈ S
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : CommRing α<VAR>A B : Matrix n n α<VAR>inst✝ : Invertible A<GOAL>A⁻¹⁻¹ = A
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝ : CommMonoidWithZero R'<VAR>χ : MulChar R R'<VAR>x : Rˣ<GOAL>(χ⁻¹ * χ) ↑x = 1 ↑x
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝ : CommMonoidWithZero R'<VAR>χ : MulChar R R'<VAR>x : Rˣ<GOAL>Ring.inverse (χ ↑x) * χ ↑x = 1 ↑x
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝ : CommMonoidWithZero R'<VAR>χ : MulChar R R'<VAR>x : Rˣ<GOAL>1 = 1 ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ ν μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure ν<VAR>inst✝ : ν.HaveLebesgueDecomposition μ<VAR>r : ℝ≥0∞<VAR>hr : r ≠ 0<VAR>hr_ne_top : r ≠ ⊤<GOAL>ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ ν μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure ν<VAR>inst✝ : ν.HaveLebesgueDecomposition μ<VAR>r : ℝ≥0∞<VAR>hr : r ≠ 0<VAR>hr_ne_top : r ≠ ⊤<VAR>h : ν.rnDeriv (r.toNNReal • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ<GOAL>ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ ν μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure ν<VAR>inst✝ : ν.HaveLebesgueDecomposition μ<VAR>r : ℝ≥0∞<VAR>hr : r ≠ 0<VAR>hr_ne_top : r ≠ ⊤<VAR>h : ν.rnDeriv (r.toNNReal • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ<VAR>this : r.toNNReal⁻¹ • ν.rnDeriv μ = r⁻¹ • ν.rnDeriv μ<GOAL>ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ ν μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure ν<VAR>inst✝ : ν.HaveLebesgueDecomposition μ<VAR>r : ℝ≥0∞<VAR>hr : r ≠ 0<VAR>hr_ne_top : r ≠ ⊤<VAR>this : r.toNNReal⁻¹ • ν.rnDeriv μ = r⁻¹ • ν.rnDeriv μ<VAR>h : ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ<GOAL>ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
<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>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>inst✝⁵ : CompleteSpace F<VAR>T✝ T' T'' : Set α → E →L[ℝ] F<VAR>C✝ C' C'' : ℝ<VAR>G' : Type u_7<VAR>G'' : Type u_8<VAR>inst✝⁴ : NormedLatticeAddCommGroup G''<VAR>inst✝³ : NormedSpace ℝ G''<VAR>inst✝² : CompleteSpace G''<VAR>inst✝¹ : NormedLatticeAddCommGroup G'<VAR>inst✝ : NormedSpace ℝ G'<VAR>T : Set α → G' →L[ℝ] G''<VAR>C : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f : ↥(Lp G' 1 μ)<VAR>hf : 0 ≤ f<GOAL>∀ (f : { g // 0 ≤ g }), 0 ≤ (setToL1 hT) ↑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>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>inst✝⁵ : CompleteSpace F<VAR>T✝ T' T'' : Set α → E →L[ℝ] F<VAR>C✝ C' C'' : ℝ<VAR>G' : Type u_7<VAR>G'' : Type u_8<VAR>inst✝⁴ : NormedLatticeAddCommGroup G''<VAR>inst✝³ : NormedSpace ℝ G''<VAR>inst✝² : CompleteSpace G''<VAR>inst✝¹ : NormedLatticeAddCommGroup G'<VAR>inst✝ : NormedSpace ℝ G'<VAR>T : Set α → G' →L[ℝ] G''<VAR>C : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f : ↥(Lp G' 1 μ)<VAR>hf : 0 ≤ f<VAR>g : { g // 0 ≤ g }<GOAL>IsClosed {x | (fun g => 0 ≤ (setToL1 hT) ↑g) x}