ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>f : α → β<VAR>hf : OpenEmbedding f<VAR>inst✝ : QuasiSober β<VAR>x : β<VAR>T : Set β<VAR>hT : IsClosed T<VAR>hS : IsIrreducible (f ⁻¹' T)<VAR>hS' : IsClosed (f ⁻¹' T)<VAR>hS'' : IsIrreducible (T ∩ range f)<VAR>hx : IsGenericPoint x (closure (T ∩ range f))<GOAL>∃ x, IsGenericPoint x (f ⁻¹' T)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>f : α → β<VAR>hf : OpenEmbedding f<VAR>inst✝ : QuasiSober β<VAR>x : β<VAR>T : Set β<VAR>hT : IsClosed T<VAR>hS : IsIrreducible (f ⁻¹' T)<VAR>hS' : IsClosed (f ⁻¹' T)<VAR>hS'' : IsIrreducible (T ∩ range f)<VAR>hx : IsGenericPoint x (closure (T ∩ range f))<VAR>hxT : x ∈ T<GOAL>∃ x, IsGenericPoint x (f ⁻¹' T)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>f : α → β<VAR>hf : OpenEmbedding f<VAR>inst✝ : QuasiSober β<VAR>T : Set β<VAR>hT : IsClosed T<VAR>hS : IsIrreducible (f ⁻¹' T)<VAR>hS' : IsClosed (f ⁻¹' T)<VAR>hS'' : IsIrreducible (T ∩ range f)<VAR>y : α<VAR>hx : IsGenericPoint (f y) (closure (T ∩ range f))<VAR>hxT : f y ∈ T<GOAL>∃ x, IsGenericPoint x (f ⁻¹' T)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>f : α → β<VAR>hf : OpenEmbedding f<VAR>inst✝ : QuasiSober β<VAR>T : Set β<VAR>hT : IsClosed T<VAR>hS : IsIrreducible (f ⁻¹' T)<VAR>hS' : IsClosed (f ⁻¹' T)<VAR>hS'' : IsIrreducible (T ∩ range f)<VAR>y : α<VAR>hx : IsGenericPoint (f y) (closure (T ∩ range f))<VAR>hxT : f y ∈ T<GOAL>IsGenericPoint y (f ⁻¹' T)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>f : α → β<VAR>hf : OpenEmbedding f<VAR>inst✝ : QuasiSober β<VAR>T : Set β<VAR>hT : IsClosed T<VAR>hS : IsIrreducible (f ⁻¹' T)<VAR>hS' : IsClosed (f ⁻¹' T)<VAR>hS'' : IsIrreducible (T ∩ range f)<VAR>y : α<VAR>hx : IsGenericPoint (f y) (closure (T ∩ range f))<VAR>hxT : f y ∈ T<GOAL>closure {y} = f ⁻¹' T
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>f : α → β<VAR>hf : OpenEmbedding f<VAR>inst✝ : QuasiSober β<VAR>T : Set β<VAR>hT : IsClosed T<VAR>hS : IsIrreducible (f ⁻¹' T)<VAR>hS' : IsClosed (f ⁻¹' T)<VAR>hS'' : IsIrreducible (T ∩ range f)<VAR>y : α<VAR>hx : IsGenericPoint (f y) (closure (T ∩ range f))<VAR>hxT : f y ∈ T<GOAL>f ⁻¹' closure (T ∩ range f) = f ⁻¹' T
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>f : α → β<VAR>hf : OpenEmbedding f<VAR>inst✝ : QuasiSober β<VAR>T : Set β<VAR>hT : IsClosed T<VAR>hS : IsIrreducible (f ⁻¹' T)<VAR>hS' : IsClosed (f ⁻¹' T)<VAR>hS'' : IsIrreducible (T ∩ range f)<VAR>y : α<VAR>hx : IsGenericPoint (f y) (closure (T ∩ range f))<VAR>hxT : f y ∈ T<GOAL>f '' (f ⁻¹' closure (T ∩ range f)) = f '' (f ⁻¹' T)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>f : α → β<VAR>hf : OpenEmbedding f<VAR>inst✝ : QuasiSober β<VAR>T : Set β<VAR>hT : IsClosed T<VAR>hS : IsIrreducible (f ⁻¹' T)<VAR>hS' : IsClosed (f ⁻¹' T)<VAR>hS'' : IsIrreducible (T ∩ range f)<VAR>y : α<VAR>hx : IsGenericPoint (f y) (closure (T ∩ range f))<VAR>hxT : f y ∈ T<VAR>z : β<GOAL>z ∈ f '' (f ⁻¹' closure (T ∩ range f)) ↔ z ∈ f '' (f ⁻¹' T)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>f : α → β<VAR>hf : OpenEmbedding f<VAR>inst✝ : QuasiSober β<VAR>T : Set β<VAR>hT : IsClosed T<VAR>hS : IsIrreducible (f ⁻¹' T)<VAR>hS' : IsClosed (f ⁻¹' T)<VAR>hS'' : IsIrreducible (T ∩ range f)<VAR>y : α<VAR>hx : IsGenericPoint (f y) (closure (T ∩ range f))<VAR>hxT : f y ∈ T<VAR>z : β<GOAL>z ∈ range f → (z ∈ closure (T ∩ range f) ↔ z ∈ T)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>hi : ¬restrict s i ≤ restrict 0 i<VAR>m : ℕ<VAR>hm : m < MeasureTheory.SignedMeasure.findExistsOneDivLT s i<GOAL>¬MeasureTheory.SignedMeasure.ExistsOneDivLT s i m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>hi : ¬restrict s i ≤ restrict 0 i<VAR>m : ℕ<VAR>hm : m < Nat.find ⋯<GOAL>¬MeasureTheory.SignedMeasure.ExistsOneDivLT s i m
<VAR>ι : Type uι<VAR>inst✝⁹ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>E' : ι → Type u_1<VAR>E'' : ι → Type u_2<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E' i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E' i)<VAR>inst✝¹ : (i : ι) → SeminormedAddCommGroup (E'' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E'' i)<VAR>g : (i : ι) → E' i →L[𝕜] E'' i<VAR>f✝ f : (i : ι) → E i →L[𝕜] E' i<GOAL>‖{ toFun := mapL, map_add' := ⋯, map_smul' := ⋯ } f‖ ≤ 1 * ∏ i : ι, ‖f i‖
<VAR>ι : Type uι<VAR>inst✝⁹ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>E' : ι → Type u_1<VAR>E'' : ι → Type u_2<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E' i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E' i)<VAR>inst✝¹ : (i : ι) → SeminormedAddCommGroup (E'' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E'' i)<VAR>g : (i : ι) → E' i →L[𝕜] E'' i<VAR>f✝ f : (i : ι) → E i →L[𝕜] E' i<GOAL>‖{ toFun := mapL, map_add' := ⋯, map_smul' := ⋯ } f‖ ≤ ∏ i : ι, ‖f i‖
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>n : ℕ<GOAL>‖newton_seq (n + 0) - newton_seq n‖ ≤ ‖Polynomial.eval a (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>n k : ℕ<GOAL>2 ^ n ≤ 2 ^ (n + k)
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>n k : ℕ<GOAL>1 ≤ 2
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>n k : ℕ<GOAL>n ≤ n + k
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>n k : ℕ<VAR>this : 2 ^ n ≤ 2 ^ (n + k)<GOAL>‖newton_seq (n + (k + 1)) - newton_seq n‖ = ‖newton_seq (n + k + 1) - newton_seq n‖
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>n k : ℕ<VAR>this : 2 ^ n ≤ 2 ^ (n + k)<GOAL>‖newton_seq (n + k + 1) - newton_seq n‖ = ‖newton_seq (n + k + 1) - newton_seq (n + k) + (newton_seq (n + k) - newton_seq n)‖
<VAR>n : ℕ<VAR>h : n ≠ 0<VAR>a✝ : ℕ<GOAL>a✝ ∈ filter (fun x => x ∣ n) (range n.succ) ↔ a✝ ∈ n.divisors
<VAR>n : ℕ<VAR>h : n ≠ 0<VAR>a✝ : ℕ<GOAL>a✝ ∣ n → a✝ < n.succ → 1 ≤ a✝
<VAR>X : Type u_1<VAR>inst✝² : NormedAddCommGroup X<VAR>M : Type u_2<VAR>inst✝¹ : Ring M<VAR>inst✝ : Module M X<VAR>P : { P // IsLprojection X P }<VAR>Q : M<GOAL>↑Pᶜ * Q = Q - ↑P * Q
<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✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : SeminormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : SecondCountableTopology G<VAR>inst✝¹ : μ.IsAddLeftInvariant<VAR>inst✝ : SFinite μ<VAR>x₀ : G<VAR>R ε : ℝ<VAR>z₀ : E'<VAR>hε : 0 ≤ ε<VAR>hif : Integrable f μ<VAR>hf : support f ⊆ ball 0 R<VAR>hmg : AEStronglyMeasurable g μ<VAR>hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε<VAR>hfg : ConvolutionExistsAt f g x₀ L μ<VAR>h2 : ∀ (t : G), dist ((L (f t)) (g (x₀ - t))) ((L (f t)) z₀) ≤ ‖L (f t)‖ * ε<GOAL>dist ((f ⋆[L, μ] g) x₀) (∫ (t : G), (L (f t)) z₀ ∂μ) ≤ (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε
<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✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : SeminormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : SecondCountableTopology G<VAR>inst✝¹ : μ.IsAddLeftInvariant<VAR>inst✝ : SFinite μ<VAR>x₀ : G<VAR>R ε : ℝ<VAR>z₀ : E'<VAR>hε : 0 ≤ ε<VAR>hif : Integrable f μ<VAR>hf : support f ⊆ ball 0 R<VAR>hmg : AEStronglyMeasurable g μ<VAR>hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε<VAR>hfg : ConvolutionExistsAt f g x₀ L μ<VAR>h2 : ∀ (t : G), dist ((L (f t)) (g (x₀ - t))) ((L (f t)) z₀) ≤ ‖L (f t)‖ * ε<GOAL>dist (∫ (t : G), (L (f t)) (g (x₀ - t)) ∂μ) (∫ (t : G), (L (f t)) z₀ ∂μ) ≤ (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε
<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✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : SeminormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : SecondCountableTopology G<VAR>inst✝¹ : μ.IsAddLeftInvariant<VAR>inst✝ : SFinite μ<VAR>x₀ : G<VAR>R ε : ℝ<VAR>z₀ : E'<VAR>hε : 0 ≤ ε<VAR>hif : Integrable f μ<VAR>hf : support f ⊆ ball 0 R<VAR>hmg : AEStronglyMeasurable g μ<VAR>hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε<VAR>hfg : ConvolutionExistsAt f g x₀ L μ<VAR>h2 : ∀ (t : G), ‖(L (f t)) (g (x₀ - t)) - (L (f t)) z₀‖ ≤ ‖L (f t)‖ * ε<GOAL>‖∫ (t : G), (L (f t)) (g (x₀ - t)) ∂μ - ∫ (t : G), (L (f t)) z₀ ∂μ‖ ≤ (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε
<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✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : SeminormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : SecondCountableTopology G<VAR>inst✝¹ : μ.IsAddLeftInvariant<VAR>inst✝ : SFinite μ<VAR>x₀ : G<VAR>R ε : ℝ<VAR>z₀ : E'<VAR>hε : 0 ≤ ε<VAR>hif : Integrable f μ<VAR>hf : support f ⊆ ball 0 R<VAR>hmg : AEStronglyMeasurable g μ<VAR>hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε<VAR>hfg : ConvolutionExistsAt f g x₀ L μ<VAR>h2 : ∀ (t : G), ‖(L (f t)) (g (x₀ - t)) - (L (f t)) z₀‖ ≤ ‖L (f t)‖ * ε<GOAL>‖∫ (a : G), (L (f a)) (g (x₀ - a)) - (L (f a)) z₀ ∂μ‖ ≤ (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε
<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✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : SeminormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : SecondCountableTopology G<VAR>inst✝¹ : μ.IsAddLeftInvariant<VAR>inst✝ : SFinite μ<VAR>x₀ : G<VAR>R ε : ℝ<VAR>z₀ : E'<VAR>hε : 0 ≤ ε<VAR>hif : Integrable f μ<VAR>hf : support f ⊆ ball 0 R<VAR>hmg : AEStronglyMeasurable g μ<VAR>hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε<VAR>hfg : ConvolutionExistsAt f g x₀ L μ<VAR>h2 : ∀ (t : G), ‖(L (f t)) (g (x₀ - t)) - (L (f t)) z₀‖ ≤ ‖L (f t)‖ * ε<GOAL>Integrable (fun t => (L (f t)) z₀) μ
<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✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : SeminormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : SecondCountableTopology G<VAR>inst✝¹ : μ.IsAddLeftInvariant<VAR>inst✝ : SFinite μ<VAR>x₀ : G<VAR>R ε : ℝ<VAR>z₀ : E'<VAR>hε : 0 ≤ ε<VAR>hif : Integrable f μ<VAR>hf : support f ⊆ ball 0 R<VAR>hmg : AEStronglyMeasurable g μ<VAR>hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε<VAR>hfg : ConvolutionExistsAt f g x₀ L μ<VAR>h2 : ∀ (t : G), ‖(L (f t)) (g (x₀ - t)) - (L (f t)) z₀‖ ≤ ‖L (f t)‖ * ε<GOAL>∫ (x : G), ‖L (f x)‖ * ε ∂μ ≤ (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε
<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✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : SeminormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : SecondCountableTopology G<VAR>inst✝¹ : μ.IsAddLeftInvariant<VAR>inst✝ : SFinite μ<VAR>x₀ : G<VAR>R ε : ℝ<VAR>z₀ : E'<VAR>hε : 0 ≤ ε<VAR>hif : Integrable f μ<VAR>hf : support f ⊆ ball 0 R<VAR>hmg : AEStronglyMeasurable g μ<VAR>hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε<VAR>hfg : ConvolutionExistsAt f g x₀ L μ<VAR>h2 : ∀ (t : G), ‖(L (f t)) (g (x₀ - t)) - (L (f t)) z₀‖ ≤ ‖L (f t)‖ * ε<GOAL>(∫ (a : G), ‖L (f a)‖ ∂μ) * ε ≤ (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε
<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✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : SeminormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : SecondCountableTopology G<VAR>inst✝¹ : μ.IsAddLeftInvariant<VAR>inst✝ : SFinite μ<VAR>x₀ : G<VAR>R ε : ℝ<VAR>z₀ : E'<VAR>hε : 0 ≤ ε<VAR>hif : Integrable f μ<VAR>hf : support f ⊆ ball 0 R<VAR>hmg : AEStronglyMeasurable g μ<VAR>hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε<VAR>hfg : ConvolutionExistsAt f g x₀ L μ<VAR>h2 : ∀ (t : G), ‖(L (f t)) (g (x₀ - t)) - (L (f t)) z₀‖ ≤ ‖L (f t)‖ * ε<GOAL>∫ (a : G), ‖L (f a)‖ ∂μ ≤ ‖L‖ * ∫ (x : G), ‖f x‖ ∂μ
<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✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : SeminormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : SecondCountableTopology G<VAR>inst✝¹ : μ.IsAddLeftInvariant<VAR>inst✝ : SFinite μ<VAR>x₀ : G<VAR>R ε : ℝ<VAR>z₀ : E'<VAR>hε : 0 ≤ ε<VAR>hif : Integrable f μ<VAR>hf : support f ⊆ ball 0 R<VAR>hmg : AEStronglyMeasurable g μ<VAR>hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε<VAR>hfg : ConvolutionExistsAt f g x₀ L μ<VAR>h2 : ∀ (t : G), ‖(L (f t)) (g (x₀ - t)) - (L (f t)) z₀‖ ≤ ‖L (f t)‖ * ε<VAR>h3 : ∀ (t : G), ‖L (f t)‖ ≤ ‖L‖ * ‖f t‖<GOAL>∫ (a : G), ‖L (f a)‖ ∂μ ≤ ‖L‖ * ∫ (x : G), ‖f x‖ ∂μ
<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✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : SeminormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : SecondCountableTopology G<VAR>inst✝¹ : μ.IsAddLeftInvariant<VAR>inst✝ : SFinite μ<VAR>x₀ : G<VAR>R ε : ℝ<VAR>z₀ : E'<VAR>hε : 0 ≤ ε<VAR>hif : Integrable f μ<VAR>hf : support f ⊆ ball 0 R<VAR>hmg : AEStronglyMeasurable g μ<VAR>hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε<VAR>hfg : ConvolutionExistsAt f g x₀ L μ<VAR>h2 : ∀ (t : G), ‖(L (f t)) (g (x₀ - t)) - (L (f t)) z₀‖ ≤ ‖L (f t)‖ * ε<VAR>h3 : ∀ (t : G), ‖L (f t)‖ ≤ ‖L‖ * ‖f t‖<GOAL>∫ (a : G), ‖L‖ * ‖f a‖ ∂μ = ‖L‖ * ∫ (x : G), ‖f x‖ ∂μ
<VAR>X✝ Y : LightCondSet<VAR>f : X✝ ⟶ Y<VAR>X : LightCondSet<VAR>S : LightProfiniteᵒᵖ<VAR>x : X.val.obj S<GOAL>∀ (i : (T : LightProfinite) × X.val.obj (Opposite.op T)), Continuous fun a => LightCondSet.coinducingCoprod X ⟨i, a⟩
<VAR>X✝ Y : LightCondSet<VAR>f : X✝ ⟶ Y<VAR>X : LightCondSet<VAR>S : LightProfiniteᵒᵖ<VAR>x : X.val.obj S<GOAL>Continuous (LightCondSet.coinducingCoprod X)
<VAR>X✝ Y : LightCondSet<VAR>f : X✝ ⟶ Y<VAR>X : LightCondSet<VAR>x✝² x✝¹ : LightProfiniteᵒᵖ<VAR>x✝ : x✝² ⟶ x✝¹<VAR>a✝ : X.val.obj x✝²<GOAL>(X.val.map x✝ ≫ (fun S x => { toFun := fun s => X.val.map (LightProfinite.const (Opposite.unop S) s).op x, continuous_toFun := ⋯ }) x✝¹) a✝ = ((fun S x => { toFun := fun s => X.val.map (LightProfinite.const (Opposite.unop S) s).op x, continuous_toFun := ⋯ }) x✝² ≫ X.toTopCat.toLightCondSet.val.map x✝) a✝
<VAR>X✝ Y : LightCondSet<VAR>f : X✝ ⟶ Y<VAR>X : LightCondSet<VAR>x✝² x✝¹ : LightProfiniteᵒᵖ<VAR>x✝ : x✝² ⟶ x✝¹<VAR>a✝ : X.val.obj x✝²<GOAL>{ toFun := fun s => X.val.map (x✝ ≫ (LightProfinite.const (Opposite.unop x✝¹) s).op) a✝, continuous_toFun := ⋯ } = { toFun := fun s => X.val.map (LightProfinite.const (Opposite.unop x✝²) s).op a✝, continuous_toFun := ⋯ }.comp x✝.unop
<VAR>θ : Angle<GOAL>(-θ).cos = θ.cos
<VAR>x✝ : ℝ<GOAL>(-↑x✝).cos = (↑x✝).cos
<VAR>q a b c : ℚ<GOAL>0 ≠ 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>s : Finset α<VAR>f : α → Set β<VAR>x : α<VAR>h : x ∈ s<GOAL>f x ≤ ⨆ (_ : x ∈ s), f x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Field K<VAR>I J : Ideal R<VAR>h : ∀ (P : Ideal R), I ≤ P → J ≤ P → ¬P.IsPrime<GOAL>IsCoprime I J
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Field K<VAR>I J : Ideal R<VAR>h : ∀ (P : Ideal R), I ≤ P → J ≤ P → ¬P.IsPrime<GOAL>I ⊔ J = ⊤
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Field K<VAR>I J : Ideal R<VAR>h : ∀ (P : Ideal R), I ≤ P → J ≤ P → ¬P.IsPrime<VAR>hIJ : ¬I ⊔ J = ⊤<GOAL>False
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Field K<VAR>I J : Ideal R<VAR>h : ∀ (P : Ideal R), I ≤ P → J ≤ P → ¬P.IsPrime<VAR>hIJ✝ : ¬I ⊔ J = ⊤<VAR>P : Ideal R<VAR>hP : P.IsMaximal<VAR>hIJ : I ⊔ J ≤ P<GOAL>False
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹ : Monoid M<VAR>a : M<VAR>inst✝ : Fintype ↥⊥<GOAL>card ↥⊥ = 1
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<GOAL>(algebraMap K E) (discr K ⇑pb.basis) = ∏ i : Fin pb.dim, ∏ j ∈ Ioi i, -(((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen))
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<GOAL>∏ i : Fin pb.dim, ∏ j ∈ Ioi i, ((e j) pb.gen - (e i) pb.gen) ^ 2 = ∏ i : Fin pb.dim, ∏ j ∈ Ioi i, -(((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁶ : DecidableEq α<VAR>inst✝⁵ : DecidableEq β<VAR>inst✝⁴ : SemilatticeSup α<VAR>inst✝³ : SemilatticeSup β<VAR>inst✝² : FunLike F α β<VAR>inst✝¹ : SupHomClass F α β<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α<VAR>a✝ b c : α<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<GOAL>filter (fun x => x ≤ a) (s ⊻ t) = filter (fun x => x ≤ a) s ⊻ filter (fun x => x ≤ a) t