ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>ha : 0 < a<VAR>hb : 1 < b<GOAL>a / b < a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : DivInvMonoid α<VAR>a b : α<VAR>l : List α<GOAL>(a :: b :: l).alternatingProd = a / b * l.alternatingProd
<VAR>a x z✝ z : ℂ<GOAL>z ∈ slitPlane ↔ z.arg ≠ π ∧ z ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝¹ : (i : ι) → TopologicalSpace (π i)<VAR>f g : α → β<VAR>t : Set α<VAR>inst✝ : (x : α) → Decidable (x ∈ t)<VAR>a : α<VAR>s : Set α<VAR>l : Filter β<VAR>h₀ : Tendsto f (𝓝[s ∩ t] a) l<VAR>h₁ : Tendsto g (𝓝[s ∩ tᶜ] a) l<GOAL>Tendsto (t.piecewise f g) (𝓝[s] a) l
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f g : Ultrafilter α<VAR>s t : Set α<VAR>p q : α → Prop<GOAL>sᶜ ∈ f ↔ s ∉ f
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r p : R[X]<VAR>n : ℕ<VAR>h : n < p.natTrailingDegree<GOAL>p.coeff n = 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r p : R[X]<VAR>n : ℕ<VAR>h : n < p.natTrailingDegree<GOAL>↑n < p.trailingDegree
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<GOAL>S.abelianImageToKernel ≫ kernel.ι S.g ≫ cokernel.π S.f = 0
<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>hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν<VAR>hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt g k x L₄ μ<VAR>hi : Integrable (uncurry fun x y => (L₃ (f y)) ((L₄ (g (x - y))) (k (x₀ - x)))) (μ.prod ν)<GOAL>∫ (t : G), ∫ (s : G), (L₃ (f s)) ((L₄ (g (t - s))) (k (x₀ - t))) ∂ν ∂μ = ∫ (s : G), ∫ (t : G), (L₃ (f s)) ((L₄ (g (t - s))) (k (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>hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν<VAR>hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt g k x L₄ μ<VAR>hi : Integrable (uncurry fun x y => (L₃ (f y)) ((L₄ (g (x - y))) (k (x₀ - x)))) (μ.prod ν)<VAR>t : G<GOAL>∫ (t_1 : G), (L₃ (f t)) ((L₄ (g (t_1 - t))) (k (x₀ - t_1))) ∂μ = ∫ (u : G), (L₃ (f t)) ((L₄ (g u)) (k (x₀ - t - u))) ∂μ
<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>hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν<VAR>hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt g k x L₄ μ<VAR>hi : Integrable (uncurry fun x y => (L₃ (f y)) ((L₄ (g (x - y))) (k (x₀ - x)))) (μ.prod ν)<VAR>t : G<GOAL>∫ (x : G), (L₃ (f t)) ((L₄ (g (x - t))) (k (x₀ - t - (x - t)))) ∂μ = ∫ (t_1 : G), (L₃ (f t)) ((L₄ (g (t_1 - t))) (k (x₀ - t_1))) ∂μ
<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>hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν<VAR>hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt g k x L₄ μ<VAR>hi : Integrable (uncurry fun x y => (L₃ (f y)) ((L₄ (g (x - y))) (k (x₀ - x)))) (μ.prod ν)<GOAL>∫ (s : G), ∫ (u : G), (L₃ (f s)) ((L₄ (g u)) (k (x₀ - s - u))) ∂μ ∂ν = ∫ (s : G), (L₃ (f s)) (∫ (u : G), (L₄ (g u)) (k (x₀ - s - u)) ∂μ) ∂ν
<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>hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν<VAR>hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt g k x L₄ μ<VAR>hi : Integrable (uncurry fun x y => (L₃ (f y)) ((L₄ (g (x - y))) (k (x₀ - x)))) (μ.prod ν)<GOAL>(fun s => ∫ (u : G), (L₃ (f s)) ((L₄ (g u)) (k (x₀ - s - u))) ∂μ) =ᶠ[ae ν] fun s => (L₃ (f s)) (∫ (u : G), (L₄ (g u)) (k (x₀ - s - u)) ∂μ)
<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>hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν<VAR>hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt g k x L₄ μ<VAR>hi : Integrable (uncurry fun x y => (L₃ (f y)) ((L₄ (g (x - y))) (k (x₀ - x)))) (μ.prod ν)<VAR>t : G<VAR>ht : ConvolutionExistsAt g k (x₀ - t) L₄ μ<GOAL>(fun s => ∫ (u : G), (L₃ (f s)) ((L₄ (g u)) (k (x₀ - s - u))) ∂μ) t = (fun s => (L₃ (f s)) (∫ (u : G), (L₄ (g u)) (k (x₀ - s - u)) ∂μ)) t
<VAR>E : Type u_1<VAR>PE : Type u_2<VAR>F : Type u_3<VAR>PF : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : MetricSpace PE<VAR>inst✝⁴ : NormedAddTorsor E PE<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : MetricSpace PF<VAR>inst✝ : NormedAddTorsor F PF<VAR>x y : PE<VAR>z : PE := midpoint ℝ x y<VAR>s : Set (PE ≃ᵢ PE) := {e | e x = x ∧ e y = y}<VAR>this : Nonempty ↑s<GOAL>∀ (e : PE ≃ᵢ PE), e x = x → e y = y → e z = z
<VAR>E : Type u_1<VAR>PE : Type u_2<VAR>F : Type u_3<VAR>PF : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : MetricSpace PE<VAR>inst✝⁴ : NormedAddTorsor E PE<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : MetricSpace PF<VAR>inst✝ : NormedAddTorsor F PF<VAR>x y : PE<VAR>z : PE := midpoint ℝ x y<VAR>s : Set (PE ≃ᵢ PE) := {e | e x = x ∧ e y = y}<VAR>this : Nonempty ↑s<VAR>h_bdd : BddAbove (range fun e => dist (↑e z) z)<GOAL>∀ (e : PE ≃ᵢ PE), e x = x → e y = y → e z = z
<VAR>E : Type u_1<VAR>PE : Type u_2<VAR>F : Type u_3<VAR>PF : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : MetricSpace PE<VAR>inst✝⁴ : NormedAddTorsor E PE<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : MetricSpace PF<VAR>inst✝ : NormedAddTorsor F PF<VAR>x y : PE<VAR>z : PE := midpoint ℝ x y<VAR>s : Set (PE ≃ᵢ PE) := {e | e x = x ∧ e y = y}<VAR>this : Nonempty ↑s<VAR>h_bdd : BddAbove (range fun e => dist (↑e z) z)<VAR>R : PE ≃ᵢ PE := (pointReflection ℝ z).toIsometryEquiv<VAR>f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun e => ((e.trans R).trans e.symm).trans R<GOAL>∀ (e : PE ≃ᵢ PE), e x = x → e y = y → e z = z
<VAR>E : Type u_1<VAR>PE : Type u_2<VAR>F : Type u_3<VAR>PF : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : MetricSpace PE<VAR>inst✝⁴ : NormedAddTorsor E PE<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : MetricSpace PF<VAR>inst✝ : NormedAddTorsor F PF<VAR>x y : PE<VAR>z : PE := midpoint ℝ x y<VAR>s : Set (PE ≃ᵢ PE) := {e | e x = x ∧ e y = y}<VAR>this : Nonempty ↑s<VAR>h_bdd : BddAbove (range fun e => dist (↑e z) z)<VAR>R : PE ≃ᵢ PE := (pointReflection ℝ z).toIsometryEquiv<VAR>f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun e => ((e.trans R).trans e.symm).trans R<VAR>hf_dist : ∀ (e : PE ≃ᵢ PE), dist ((f e) z) z = 2 * dist (e z) z<GOAL>∀ (e : PE ≃ᵢ PE), e x = x → e y = y → e z = z
<VAR>E : Type u_1<VAR>PE : Type u_2<VAR>F : Type u_3<VAR>PF : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : MetricSpace PE<VAR>inst✝⁴ : NormedAddTorsor E PE<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : MetricSpace PF<VAR>inst✝ : NormedAddTorsor F PF<VAR>x y : PE<VAR>z : PE := midpoint ℝ x y<VAR>s : Set (PE ≃ᵢ PE) := {e | e x = x ∧ e y = y}<VAR>this : Nonempty ↑s<VAR>h_bdd : BddAbove (range fun e => dist (↑e z) z)<VAR>R : PE ≃ᵢ PE := (pointReflection ℝ z).toIsometryEquiv<VAR>f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun e => ((e.trans R).trans e.symm).trans R<VAR>hf_dist : ∀ (e : PE ≃ᵢ PE), dist ((f e) z) z = 2 * dist (e z) z<VAR>hf_maps_to : MapsTo f s s<GOAL>∀ (e : PE ≃ᵢ PE), e x = x → e y = y → e z = z
<VAR>E : Type u_1<VAR>PE : Type u_2<VAR>F : Type u_3<VAR>PF : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : MetricSpace PE<VAR>inst✝⁴ : NormedAddTorsor E PE<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : MetricSpace PF<VAR>inst✝ : NormedAddTorsor F PF<VAR>x y : PE<VAR>z : PE := midpoint ℝ x y<VAR>s : Set (PE ≃ᵢ PE) := {e | e x = x ∧ e y = y}<VAR>this : Nonempty ↑s<VAR>h_bdd : BddAbove (range fun e => dist (↑e z) z)<VAR>R : PE ≃ᵢ PE := (pointReflection ℝ z).toIsometryEquiv<VAR>f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun e => ((e.trans R).trans e.symm).trans R<VAR>hf_dist : ∀ (e : PE ≃ᵢ PE), dist ((f e) z) z = 2 * dist (e z) z<VAR>hf_maps_to : MapsTo f s s<VAR>c : ℝ := ⨆ e, dist (↑e z) z<GOAL>∀ (e : PE ≃ᵢ PE), e x = x → e y = y → e z = z
<VAR>E : Type u_1<VAR>PE : Type u_2<VAR>F : Type u_3<VAR>PF : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : MetricSpace PE<VAR>inst✝⁴ : NormedAddTorsor E PE<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : MetricSpace PF<VAR>inst✝ : NormedAddTorsor F PF<VAR>x y : PE<VAR>z : PE := midpoint ℝ x y<VAR>s : Set (PE ≃ᵢ PE) := {e | e x = x ∧ e y = y}<VAR>this✝ : Nonempty ↑s<VAR>h_bdd : BddAbove (range fun e => dist (↑e z) z)<VAR>R : PE ≃ᵢ PE := (pointReflection ℝ z).toIsometryEquiv<VAR>f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun e => ((e.trans R).trans e.symm).trans R<VAR>hf_dist : ∀ (e : PE ≃ᵢ PE), dist ((f e) z) z = 2 * dist (e z) z<VAR>hf_maps_to : MapsTo f s s<VAR>c : ℝ := ⨆ e, dist (↑e z) z<VAR>this : c ≤ c / 2<GOAL>∀ (e : PE ≃ᵢ PE), e x = x → e y = y → e z = z
<VAR>E : Type u_1<VAR>PE : Type u_2<VAR>F : Type u_3<VAR>PF : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : MetricSpace PE<VAR>inst✝⁴ : NormedAddTorsor E PE<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : MetricSpace PF<VAR>inst✝ : NormedAddTorsor F PF<VAR>x y : PE<VAR>z : PE := midpoint ℝ x y<VAR>s : Set (PE ≃ᵢ PE) := {e | e x = x ∧ e y = y}<VAR>this✝ : Nonempty ↑s<VAR>h_bdd : BddAbove (range fun e => dist (↑e z) z)<VAR>R : PE ≃ᵢ PE := (pointReflection ℝ z).toIsometryEquiv<VAR>f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun e => ((e.trans R).trans e.symm).trans R<VAR>hf_dist : ∀ (e : PE ≃ᵢ PE), dist ((f e) z) z = 2 * dist (e z) z<VAR>hf_maps_to : MapsTo f s s<VAR>c : ℝ := ⨆ e, dist (↑e z) z<VAR>this : c ≤ 0<GOAL>∀ (e : PE ≃ᵢ PE), e x = x → e y = y → e z = z
<VAR>E : Type u_1<VAR>PE : Type u_2<VAR>F : Type u_3<VAR>PF : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : MetricSpace PE<VAR>inst✝⁴ : NormedAddTorsor E PE<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : MetricSpace PF<VAR>inst✝ : NormedAddTorsor F PF<VAR>x y : PE<VAR>z : PE := midpoint ℝ x y<VAR>s : Set (PE ≃ᵢ PE) := {e | e x = x ∧ e y = y}<VAR>this✝ : Nonempty ↑s<VAR>h_bdd : BddAbove (range fun e => dist (↑e z) z)<VAR>R : PE ≃ᵢ PE := (pointReflection ℝ z).toIsometryEquiv<VAR>f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun e => ((e.trans R).trans e.symm).trans R<VAR>hf_dist : ∀ (e : PE ≃ᵢ PE), dist ((f e) z) z = 2 * dist (e z) z<VAR>hf_maps_to : MapsTo f s s<VAR>c : ℝ := ⨆ e, dist (↑e z) z<VAR>this : c ≤ 0<VAR>e : PE ≃ᵢ PE<VAR>hx : e x = x<VAR>hy : e y = y<GOAL>dist (e z) z ≤ c
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<GOAL>finrank ℝ (({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)) = finrank ℚ K
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>hμm : SigmaFinite (μ.trim hm)<VAR>f : α → ℝ<VAR>hf : Integrable f μ<GOAL>SignedMeasure.rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm) =ᶠ[ae μ] μ[f|m]
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>hμm : SigmaFinite (μ.trim hm)<VAR>f : α → ℝ<VAR>hf : Integrable f μ<GOAL>∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (SignedMeasure.rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm)) s μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>hμm : SigmaFinite (μ.trim hm)<VAR>f : α → ℝ<VAR>hf : Integrable f μ<GOAL>∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, SignedMeasure.rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm) x ∂μ = ∫ (x : α) in s, f x ∂μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>hμm : SigmaFinite (μ.trim hm)<VAR>f : α → ℝ<VAR>hf : Integrable f μ<GOAL>AEStronglyMeasurable' m (SignedMeasure.rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm)) μ
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>hp : 0 < p.toReal<VAR>f : ↥(lp E p)<GOAL>HasSum (fun i => ‖↑f i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>hp : 0 < p.toReal<VAR>f : ↥(lp E p)<GOAL>HasSum (fun i => ‖↑f i‖ ^ p.toReal) (∑' (i : α), ‖↑f i‖ ^ p.toReal)
<VAR>G : Type u<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>M : ι → Type u_2<VAR>inst✝ : (i : ι) → Monoid (M i)<GOAL>exponent ((i : ι) → M i) = univ.lcm fun x => exponent (M x)
<VAR>G : Type u<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>M : ι → Type u_2<VAR>inst✝ : (i : ι) → Monoid (M i)<GOAL>exponent ((i : ι) → M i) ∣ univ.lcm fun x => exponent (M x)
<VAR>G : Type u<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>M : ι → Type u_2<VAR>inst✝ : (i : ι) → Monoid (M i)<GOAL>(univ.lcm fun x => exponent (M x)) ∣ exponent ((i : ι) → M i)
<VAR>n : Type u<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>A : GL n R<GOAL>(↑A).det * (↑A⁻¹).det = 1
<VAR>n : Type u<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>A : GL n R<GOAL>(↑A⁻¹).det * (↑A).det = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b✝ b₁ b₂ : β<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulStrictMono α β<VAR>a : α<VAR>b : β<GOAL>a • b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : DecidableEq (K →+* ℂ)<VAR>e : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K) := equivReindex K<VAR>N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => (integralBasis K) (e i)) RingHom.equivRatAlgHom<GOAL>(basisMatrix K).det ≠ 0
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : DecidableEq (K →+* ℂ)<VAR>e : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K) := equivReindex K<VAR>N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => (integralBasis K) (e i)) RingHom.equivRatAlgHom<GOAL>N.det ^ 2 ≠ 0
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : DecidableEq (K →+* ℂ)<VAR>e : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K) := equivReindex K<VAR>N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => (integralBasis K) (e i)) RingHom.equivRatAlgHom<GOAL>N.det ^ 2 = (algebraMap ℚ ℂ) (Algebra.discr ℚ ⇑(integralBasis K))
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : DecidableEq (K →+* ℂ)<VAR>e : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K) := equivReindex K<VAR>N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => (integralBasis K) (e i)) RingHom.equivRatAlgHom<GOAL>N.det ^ 2 = (algebraMap ℚ ℂ) (Algebra.discr ℚ (⇑(integralBasis K) ∘ ⇑e.symm.symm))
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x ≠ 0 ∨ y = 0<GOAL>‖x‖ / Real.cos (angle x (x + y)) = ‖x + y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x ≠ 0 ∨ y = 0<GOAL>‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + y‖
<VAR>ι : Type u_1<VAR>I J : Box ι<VAR>π π₁ π₂ : TaggedPrepartition I<VAR>x : ι → ℝ<VAR>r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)<VAR>inst✝ : Fintype ι<VAR>h₁ : π₁.IsSubordinate r<VAR>h₂ : π₂.IsSubordinate r<VAR>h : Disjoint π₁.iUnion π₂.iUnion<GOAL>(π₁.disjUnion π₂ h).IsSubordinate r
<VAR>ι : Type u_1<VAR>I J✝ : Box ι<VAR>π π₁ π₂ : TaggedPrepartition I<VAR>x : ι → ℝ<VAR>r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)<VAR>inst✝ : Fintype ι<VAR>h₁ : π₁.IsSubordinate r<VAR>h₂ : π₂.IsSubordinate r<VAR>h : Disjoint π₁.iUnion π₂.iUnion<VAR>J : Box ι<VAR>hJ✝ : J ∈ π₁.disjUnion π₂ h<VAR>hJ : J ∈ π₁.boxes<GOAL>Box.Icc J ⊆ closedBall ((π₁.disjUnion π₂ h).tag J) ↑(r ((π₁.disjUnion π₂ h).tag J))
<VAR>ι : Type u_1<VAR>I J✝ : Box ι<VAR>π π₁ π₂ : TaggedPrepartition I<VAR>x : ι → ℝ<VAR>r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)<VAR>inst✝ : Fintype ι<VAR>h₁ : π₁.IsSubordinate r<VAR>h₂ : π₂.IsSubordinate r<VAR>h : Disjoint π₁.iUnion π₂.iUnion<VAR>J : Box ι<VAR>hJ✝ : J ∈ π₁.disjUnion π₂ h<VAR>hJ : J ∈ π₂.boxes<GOAL>Box.Icc J ⊆ closedBall ((π₁.disjUnion π₂ h).tag J) ↑(r ((π₁.disjUnion π₂ h).tag J))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁵ : AddCommMonoid A<VAR>inst✝⁴ : AddCommMonoid B<VAR>inst✝³ : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g✝ : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : AddZeroClass M<VAR>inst✝ : CommMonoid N<VAR>f g : α →₀ M<VAR>h : α → M → N<VAR>h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1<VAR>h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂<GOAL>(f + g).prod h = f.prod h * g.prod h