ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r'✝ : ℝ≥0∞<VAR>r' : ℝ≥0<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑r' < r<VAR>a : ℝ<VAR>ha : a ∈ Ioo 0 1<VAR>C : ℝ<VAR>hC : C > 0<VAR>hp : ∀ (n : ℕ), ‖p n‖ * ↑r' ^ n ≤ C * a ^ n<VAR>y : E<VAR>hy : y ∈ Metric.ball 0 ↑r'<VAR>n : ℕ<VAR>yr' : ‖y‖ < ↑r'<VAR>hr'0 : 0 < ↑r'<VAR>this : y ∈ EMetric.ball 0 r<GOAL>‖f (x + y) - p.partialSum n y‖ ≤ C / (1 - a) * (a * (‖y‖ / ↑r')) ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r'✝ : ℝ≥0∞<VAR>r' : ℝ≥0<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑r' < r<VAR>a : ℝ<VAR>ha : a ∈ Ioo 0 1<VAR>C : ℝ<VAR>hC : C > 0<VAR>hp : ∀ (n : ℕ), ‖p n‖ * ↑r' ^ n ≤ C * a ^ n<VAR>y : E<VAR>hy : y ∈ Metric.ball 0 ↑r'<VAR>n : ℕ<VAR>yr' : ‖y‖ < ↑r'<VAR>hr'0 : 0 < ↑r'<VAR>this : y ∈ EMetric.ball 0 r<GOAL>‖p.partialSum n y - f (x + y)‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n / (1 - a)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r'✝ : ℝ≥0∞<VAR>r' : ℝ≥0<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑r' < r<VAR>a : ℝ<VAR>ha : a ∈ Ioo 0 1<VAR>C : ℝ<VAR>hC : C > 0<VAR>hp : ∀ (n : ℕ), ‖p n‖ * ↑r' ^ n ≤ C * a ^ n<VAR>y : E<VAR>hy : y ∈ Metric.ball 0 ↑r'<VAR>n : ℕ<VAR>yr' : ‖y‖ < ↑r'<VAR>hr'0 : 0 < ↑r'<VAR>this : y ∈ EMetric.ball 0 r<VAR>ya : a * (‖y‖ / ↑r') ≤ a<GOAL>‖p.partialSum n y - f (x + y)‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n / (1 - a)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r'✝ : ℝ≥0∞<VAR>r' : ℝ≥0<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑r' < r<VAR>a : ℝ<VAR>ha : a ∈ Ioo 0 1<VAR>C : ℝ<VAR>hC : C > 0<VAR>hp : ∀ (n : ℕ), ‖p n‖ * ↑r' ^ n ≤ C * a ^ n<VAR>y : E<VAR>hy : y ∈ Metric.ball 0 ↑r'<VAR>n : ℕ<VAR>yr' : ‖y‖ < ↑r'<VAR>hr'0 : 0 < ↑r'<VAR>this : y ∈ EMetric.ball 0 r<VAR>ya : a * (‖y‖ / ↑r') ≤ a<GOAL>‖p.partialSum n y - f (x + y)‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n / (1 - a * (‖y‖ / ↑r'))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r'✝ : ℝ≥0∞<VAR>r' : ℝ≥0<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑r' < r<VAR>a : ℝ<VAR>ha : a ∈ Ioo 0 1<VAR>C : ℝ<VAR>hC : C > 0<VAR>hp : ∀ (n : ℕ), ‖p n‖ * ↑r' ^ n ≤ C * a ^ n<VAR>y : E<VAR>hy : y ∈ Metric.ball 0 ↑r'<VAR>n : ℕ<VAR>yr' : ‖y‖ < ↑r'<VAR>hr'0 : 0 < ↑r'<VAR>this : y ∈ EMetric.ball 0 r<VAR>ya : a * (‖y‖ / ↑r') ≤ a<GOAL>∀ (n : ℕ), ‖(p n) fun x => y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r'✝ : ℝ≥0∞<VAR>r' : ℝ≥0<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑r' < r<VAR>a : ℝ<VAR>ha : a ∈ Ioo 0 1<VAR>C : ℝ<VAR>hC : C > 0<VAR>hp : ∀ (n : ℕ), ‖p n‖ * ↑r' ^ n ≤ C * a ^ n<VAR>y : E<VAR>hy : y ∈ Metric.ball 0 ↑r'<VAR>n✝ : ℕ<VAR>yr' : ‖y‖ < ↑r'<VAR>hr'0 : 0 < ↑r'<VAR>this : y ∈ EMetric.ball 0 r<VAR>ya : a * (‖y‖ / ↑r') ≤ a<VAR>n : ℕ<GOAL>‖(p n) fun x => y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>I✝ I' : Ideal R<VAR>J✝ J' : Ideal S<VAR>I : Ideal R<VAR>J : Ideal S<GOAL>(I.prod J).IsPrime → I = ⊤ ∨ J = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>I✝ I' : Ideal R<VAR>J✝ J' : Ideal S<VAR>I : Ideal R<VAR>J : Ideal S<GOAL>I ≠ ⊤ ∧ J ≠ ⊤ → ¬(I.prod J).IsPrime
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>I✝ I' : Ideal R<VAR>J✝ J' : Ideal S<VAR>I : Ideal R<VAR>J : Ideal S<GOAL>1 ∉ I ∧ 1 ∉ J → 1 ∉ I.prod J → ∃ x x_1, ∃ (_ : x * x_1 ∈ I.prod J), x ∉ I.prod J ∧ x_1 ∉ I.prod J
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : abscissaOfAbsConv f < ↑s.re<GOAL>LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : abscissaOfAbsConv f < ↑s.re<VAR>x : ℝ<VAR>hxs : x < s.re<VAR>hf : LSeriesSummable f ↑x<GOAL>LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : abscissaOfAbsConv f < ↑s.re<VAR>x : ℝ<VAR>hxs : x < s.re<VAR>hf : LSeriesSummable f ↑x<VAR>y : ℝ<VAR>hxy : x < y<VAR>hys : y < s.re<GOAL>LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : abscissaOfAbsConv f < ↑s.re<VAR>x : ℝ<VAR>hxs : x < s.re<VAR>hf : LSeriesSummable f ↑x<VAR>y : ℝ<VAR>hxy : x < y<VAR>hys : y < s.re<VAR>S : Set ℂ := {z | y < z.re}<GOAL>LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : abscissaOfAbsConv f < ↑s.re<VAR>x : ℝ<VAR>hxs : x < s.re<VAR>hf : LSeriesSummable f ↑x<VAR>y : ℝ<VAR>hxy : x < y<VAR>hys : y < s.re<VAR>S : Set ℂ := {z | y < z.re}<VAR>h₀ : Summable fun n => ‖term f (↑x) n‖<GOAL>LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : abscissaOfAbsConv f < ↑s.re<VAR>x : ℝ<VAR>hxs : x < s.re<VAR>hf : LSeriesSummable f ↑x<VAR>y : ℝ<VAR>hxy : x < y<VAR>hys : y < s.re<VAR>S : Set ℂ := {z | y < z.re}<VAR>h₀ : Summable fun n => ‖term f (↑x) n‖<VAR>h₁ : ∀ (n : ℕ), DifferentiableOn ℂ (fun x => term f x n) S<GOAL>LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : abscissaOfAbsConv f < ↑s.re<VAR>x : ℝ<VAR>hxs : x < s.re<VAR>hf : LSeriesSummable f ↑x<VAR>y : ℝ<VAR>hxy : x < y<VAR>hys : y < s.re<VAR>S : Set ℂ := {z | y < z.re}<VAR>h₀ : Summable fun n => ‖term f (↑x) n‖<VAR>h₁ : ∀ (n : ℕ), DifferentiableOn ℂ (fun x => term f x n) S<VAR>h₂ : IsOpen S<GOAL>LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : abscissaOfAbsConv f < ↑s.re<VAR>x : ℝ<VAR>hxs : x < s.re<VAR>hf : LSeriesSummable f ↑x<VAR>y : ℝ<VAR>hxy : x < y<VAR>hys : y < s.re<VAR>S : Set ℂ := {z | y < z.re}<VAR>h₀ : Summable fun n => ‖term f (↑x) n‖<VAR>h₁ : ∀ (n : ℕ), DifferentiableOn ℂ (fun x => term f x n) S<VAR>h₂ : IsOpen S<VAR>h₃ : ∀ (n : ℕ), ∀ z ∈ S, ‖term f z n‖ ≤ ‖term f (↑x) n‖<GOAL>LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : abscissaOfAbsConv f < ↑s.re<VAR>x : ℝ<VAR>hxs : x < s.re<VAR>hf : LSeriesSummable f ↑x<VAR>y : ℝ<VAR>hxy : x < y<VAR>hys : y < s.re<VAR>S : Set ℂ := {z | y < z.re}<VAR>h₀ : Summable fun n => ‖term f (↑x) n‖<VAR>h₁ : ∀ (n : ℕ), DifferentiableOn ℂ (fun x => term f x n) S<VAR>h₂ : IsOpen S<VAR>h₃ : ∀ (n : ℕ), ∀ z ∈ S, ‖term f z n‖ ≤ ‖term f (↑x) n‖<VAR>H : HasSum (fun i => deriv (fun x => term f x i) s) (deriv (fun w => ∑' (i : ℕ), term f w i) s)<GOAL>LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : abscissaOfAbsConv f < ↑s.re<VAR>x : ℝ<VAR>hxs : x < s.re<VAR>hf : LSeriesSummable f ↑x<VAR>y : ℝ<VAR>hxy : x < y<VAR>hys : y < s.re<VAR>S : Set ℂ := {z | y < z.re}<VAR>h₀ : Summable fun n => ‖term f (↑x) n‖<VAR>h₁ : ∀ (n : ℕ), DifferentiableOn ℂ (fun x => term f x n) S<VAR>h₂ : IsOpen S<VAR>h₃ : ∀ (n : ℕ), ∀ z ∈ S, ‖term f z n‖ ≤ ‖term f (↑x) n‖<VAR>H : HasSum (fun i => -term (logMul f) s i) (deriv (fun w => ∑' (i : ℕ), term f w i) s)<GOAL>LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : abscissaOfAbsConv f < ↑s.re<VAR>x : ℝ<VAR>hxs : x < s.re<VAR>hf : LSeriesSummable f ↑x<VAR>y : ℝ<VAR>hxy : x < y<VAR>hys : y < s.re<VAR>S : Set ℂ := {z | y < z.re}<VAR>h₀ : Summable fun n => ‖term f (↑x) n‖<VAR>h₁ : ∀ (n : ℕ), DifferentiableOn ℂ (fun x => term f x n) S<VAR>h₂ : IsOpen S<VAR>h₃ : ∀ (n : ℕ), ∀ z ∈ S, ‖term f z n‖ ≤ ‖term f (↑x) n‖<VAR>H : HasSum (fun i => -term (logMul f) s i) (deriv (fun w => ∑' (i : ℕ), term f w i) s)<GOAL>HasDerivAt (LSeries f) (-LSeries (logMul f) s) s
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : abscissaOfAbsConv f < ↑s.re<VAR>x : ℝ<VAR>hxs : x < s.re<VAR>hf : LSeriesSummable f ↑x<VAR>y : ℝ<VAR>hxy : x < y<VAR>hys : y < s.re<VAR>S : Set ℂ := {z | y < z.re}<VAR>h₀ : Summable fun n => ‖term f (↑x) n‖<VAR>h₁ : ∀ (n : ℕ), DifferentiableOn ℂ (fun x => term f x n) S<VAR>h₂ : IsOpen S<VAR>h₃ : ∀ (n : ℕ), ∀ z ∈ S, ‖term f z n‖ ≤ ‖term f (↑x) n‖<VAR>H : HasSum (fun i => -term (logMul f) s i) (deriv (fun w => ∑' (i : ℕ), term f w i) s)<VAR>H' : DifferentiableOn ℂ (fun w => ∑' (i : ℕ), term f w i) S<GOAL>HasDerivAt (LSeries f) (-LSeries (logMul f) s) s
<VAR>α✝ : Type u_1<VAR>inst✝¹ : OrderedCancelCommMonoid α✝<VAR>s✝ t✝ : Set α✝<VAR>hs✝ : s✝.IsPWO<VAR>ht✝ : t✝.IsPWO<VAR>a✝ : α✝<VAR>u : Set α✝<VAR>hu : u.IsPWO<VAR>x : α✝ × α✝<VAR>α : Type u_2<VAR>inst✝ : LinearOrderedCancelCommMonoid α<VAR>s t : Set α<VAR>hs : s.IsWF<VAR>ht : t.IsWF<VAR>hns : s.Nonempty<VAR>hnt : t.Nonempty<VAR>a b : α<GOAL>(a, b) ∈ mulAntidiagonal ⋯ ⋯ (hs.min hns * ht.min hnt) ↔ (a, b) ∈ {(hs.min hns, ht.min hnt)}
<VAR>α✝ : Type u_1<VAR>inst✝¹ : OrderedCancelCommMonoid α✝<VAR>s✝ t✝ : Set α✝<VAR>hs✝ : s✝.IsPWO<VAR>ht✝ : t✝.IsPWO<VAR>a✝ : α✝<VAR>u : Set α✝<VAR>hu : u.IsPWO<VAR>x : α✝ × α✝<VAR>α : Type u_2<VAR>inst✝ : LinearOrderedCancelCommMonoid α<VAR>s t : Set α<VAR>hs : s.IsWF<VAR>ht : t.IsWF<VAR>hns : s.Nonempty<VAR>hnt : t.Nonempty<VAR>a b : α<GOAL>a ∈ s ∧ b ∈ t ∧ a * b = hs.min hns * ht.min hnt ↔ a = hs.min hns ∧ b = ht.min hnt
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>s s₁ t u : Set E<VAR>f : E → F →L[𝕜] G<VAR>c : F<VAR>x : E<VAR>N : ℕ∞<VAR>n : ℕ<VAR>hf : ContDiff 𝕜 N f<VAR>hn : ↑n ≤ N<GOAL>‖iteratedFDeriv 𝕜 n (fun y => (f y) c) x‖ ≤ ‖c‖ * ‖iteratedFDeriv 𝕜 n f x‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>s s₁ t u : Set E<VAR>f : E → F →L[𝕜] G<VAR>c : F<VAR>x : E<VAR>N : ℕ∞<VAR>n : ℕ<VAR>hf : ContDiff 𝕜 N f<VAR>hn : ↑n ≤ N<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => (f y) c) univ x‖ ≤ ‖c‖ * ‖iteratedFDerivWithin 𝕜 n f univ x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : Preorder α<VAR>s : LowerSet α<VAR>t : Set α<VAR>a : α<GOAL>s.sdiff t = s ↔ Disjoint (↑s) t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>inst✝¹ : PartialOrder X<VAR>x y : X<VAR>inst✝ : NoAtoms μ<GOAL>∫ (t : X) in Icc x y, f t ∂μ = ∫ (t : X) in Ioo x y, f t ∂μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f g✝ : α → β<VAR>μ ν : Measure α<VAR>g : β → γ<VAR>hf : MeasurableEmbedding f<GOAL>AEMeasurable g (Measure.map f μ) ↔ AEMeasurable (g ∘ f) μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f g✝ : α → β<VAR>μ ν : Measure α<VAR>g : β → γ<VAR>hf : MeasurableEmbedding f<GOAL>AEMeasurable (g ∘ f) μ → AEMeasurable g (Measure.map f μ)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f g✝ : α → β<VAR>μ ν : Measure α<VAR>g : β → γ<VAR>hf : MeasurableEmbedding f<VAR>g₁ : α → γ<VAR>hgm₁ : Measurable g₁<VAR>heq : g ∘ f =ᶠ[ae μ] g₁<GOAL>AEMeasurable g (Measure.map f μ)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f g✝ : α → β<VAR>μ ν : Measure α<VAR>g : β → γ<VAR>hf : MeasurableEmbedding f<VAR>g₂ : β → γ<VAR>hgm₂ : Measurable g₂<VAR>hgm₁ : Measurable (g₂ ∘ f)<VAR>heq : g ∘ f =ᶠ[ae μ] g₂ ∘ f<GOAL>AEMeasurable g (Measure.map f μ)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>hc : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<GOAL>ContinuousAt (gauge s) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>hc : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<VAR>ha : Absorbent ℝ s<GOAL>ContinuousAt (gauge s) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>hc : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<VAR>ha : Absorbent ℝ s<VAR>ε : ℝ<VAR>hε₀ : 0 < ε<GOAL>∀ᶠ (x_1 : E) in 𝓝 x, gauge s x_1 ∈ Icc (gauge s x - ε) (gauge s x + ε)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>hc : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<VAR>ha : Absorbent ℝ s<VAR>ε : ℝ<VAR>hε₀ : 0 < ε<GOAL>∀ᶠ (a : E) in 𝓝 0, gauge s (x + a) ∈ Icc (gauge s x - ε) (gauge s x + ε)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>hc : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<VAR>ha : Absorbent ℝ s<VAR>ε : ℝ<VAR>hε₀ : 0 < ε<VAR>this : ε • s ∩ -(ε • s) ∈ 𝓝 0<GOAL>∀ᶠ (a : E) in 𝓝 0, gauge s (x + a) ∈ Icc (gauge s x - ε) (gauge s x + ε)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>hc : Convex ℝ s<VAR>hs₀ : s ∈ 𝓝 0<VAR>ha : Absorbent ℝ s<VAR>ε : ℝ<VAR>hε₀ : 0 < ε<VAR>this : ε • s ∩ -(ε • s) ∈ 𝓝 0<VAR>y : E<VAR>hy : y ∈ ε • s ∩ -(ε • s)<GOAL>gauge s (x + y) ∈ Icc (gauge s x - ε) (gauge s x + ε)
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>s : Set F<VAR>L : Filter F<VAR>g : 𝕜 → 𝕜<VAR>g' u : 𝕜<VAR>L' : Filter 𝕜<VAR>h : HasDerivAt g g' u<GOAL>HasGradientAt g ((starRingEnd 𝕜) g') u
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>s : Set F<VAR>L : Filter F<VAR>g : 𝕜 → 𝕜<VAR>g' u : 𝕜<VAR>L' : Filter 𝕜<VAR>h : HasDerivAt g g' u<GOAL>HasDerivAt g (((toDual 𝕜 𝕜) ((starRingEnd 𝕜) g')) 1) u
<VAR>C : Type uC<VAR>inst✝¹ : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝ : Category.{uD', uD} D<VAR>G : C ⥤ D<VAR>hG : W.IsInvertedBy G<VAR>G₁ G₂ : W.Localization ⥤ D<VAR>h : W.Q ⋙ G₁ = W.Q ⋙ G₂<GOAL>Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
<VAR>C : Type uC<VAR>inst✝¹ : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝ : Category.{uD', uD} D<VAR>G : C ⥤ D<VAR>hG : W.IsInvertedBy G<VAR>G₁ G₂ : W.Localization ⥤ D<VAR>h : W.Q ⋙ G₁ = W.Q ⋙ G₂<GOAL>(Quotient.functor (relations W) ⋙ G₁).obj = (Quotient.functor (relations W) ⋙ G₂).obj
<VAR>C : Type uC<VAR>inst✝¹ : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝ : Category.{uD', uD} D<VAR>G : C ⥤ D<VAR>hG : W.IsInvertedBy G<VAR>G₁ G₂ : W.Localization ⥤ D<VAR>h : W.Q ⋙ G₁ = W.Q ⋙ G₂<GOAL>∀ (a b : LocQuiver W) (e : a ⟶ b), (Quotient.functor (relations W) ⋙ G₁).map e.toPath = eqToHom ⋯ ≫ (Quotient.functor (relations W) ⋙ G₂).map e.toPath ≫ eqToHom ⋯
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁶ : Semiring α<VAR>inst✝⁵ : PartialOrder α<VAR>a b c d : α<VAR>inst✝⁴ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : MulPosStrictMono α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>hab : a < b<VAR>hcd : c < d<GOAL>a * d + b * c < a * c + b * d
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁶ : Semiring α<VAR>inst✝⁵ : PartialOrder α<VAR>a c d : α<VAR>inst✝⁴ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : MulPosStrictMono α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>hcd : c < d<VAR>b : α<VAR>hab : a < a + b<GOAL>a * d + (a + b) * c < a * c + (a + b) * d
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁶ : Semiring α<VAR>inst✝⁵ : PartialOrder α<VAR>a c : α<VAR>inst✝⁴ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : MulPosStrictMono α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>b : α<VAR>hab : a < a + b<VAR>d : α<VAR>hcd : c < c + d<GOAL>a * (c + d) + (a + b) * c < a * c + (a + b) * (c + d)
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁶ : Semiring α<VAR>inst✝⁵ : PartialOrder α<VAR>a c : α<VAR>inst✝⁴ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : MulPosStrictMono α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>b : α<VAR>hab : a < a + b<VAR>d : α<VAR>hcd : c < c + d<GOAL>a * c + (a + b) * c + a * d < a * c + (a + b) * c + (a + b) * d
<VAR>J : Type v'<VAR>inst✝⁵ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝³ : Category.{?u.260730, u_1} K<VAR>D : Type u_2<VAR>inst✝² : Category.{?u.260737, u_2} D<VAR>inst✝¹ : HasStrictInitialObjects C<VAR>inst✝ : IsEmpty J<VAR>F : J ⥤ C<VAR>c : Cocone F<VAR>hc : IsColimit c<VAR>this : IsInitial c.pt<GOAL>IsVanKampenColimit c
<VAR>J : Type v'<VAR>inst✝⁵ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝³ : Category.{?u.260730, u_1} K<VAR>D : Type u_2<VAR>inst✝² : Category.{?u.260737, u_2} D<VAR>inst✝¹ : HasStrictInitialObjects C<VAR>inst✝ : IsEmpty J<VAR>F : J ⥤ C<VAR>c : Cocone F<VAR>hc : IsColimit c<VAR>this : IsVanKampenColimit (asEmptyCocone c.pt)<GOAL>IsVanKampenColimit c
<VAR>J : Type v'<VAR>inst✝⁵ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝³ : Category.{?u.260730, u_1} K<VAR>D : Type u_2<VAR>inst✝² : Category.{?u.260737, u_2} D<VAR>inst✝¹ : HasStrictInitialObjects C<VAR>inst✝ : IsEmpty J<VAR>F : J ⥤ C<VAR>c : Cocone F<VAR>hc : IsColimit c<VAR>this : IsVanKampenColimit (asEmptyCocone c.pt)<GOAL>IsVanKampenColimit (Cocone.whisker (equivalenceOfIsEmpty (Discrete PEmpty.{1}) J).functor c)
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedField 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>s t : Set E<VAR>x✝ y x : E<GOAL>↑‖x‖₊ ≤ egauge 𝕜 (ball 0 1) x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : StarRing R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : StarRing A<VAR>inst✝ : StarModule R A<VAR>S₁ S₂ : StarSubalgebra R A<VAR>h : S₁ ≤ S₂<VAR>hS₁ : IsClosed ↑S₁<GOAL>Subtype.val ⁻¹' ↑S₁ = range ⇑(inclusion h)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : StarRing R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : StarRing A<VAR>inst✝ : StarModule R A<VAR>S₁ S₂ : StarSubalgebra R A<VAR>h : S₁ ≤ S₂<VAR>hS₁ : IsClosed ↑S₁<GOAL>↑S₁ = id '' {x | x ∈ S₁}
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : StarRing R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : StarRing A<VAR>inst✝ : StarModule R A<VAR>S₁ S₂ : StarSubalgebra R A<VAR>h : S₁ ≤ S₂<VAR>hS₁ : IsClosed ↑S₁<GOAL>∀ x ∈ S₁, id x ∈ S₂
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>v : Vector α (n + 1)<VAR>f : α → β<GOAL>(map f v).head = f v.head
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>v : Vector α (n + 1)<VAR>f : α → β<VAR>a : α<VAR>v' : Vector α n<VAR>h : v = a ::ᵥ v'<GOAL>(map f v).head = f v.head
<VAR>α : Sort u_1<VAR>r p✝ q✝ : α → Prop<VAR>P Q : (x : α) → p✝ x → Prop<VAR>b : Prop<VAR>inst✝ : Nonempty α<VAR>q : Prop<VAR>p : α → Prop<GOAL>(∀ (x : α), q ∧ p x) ↔ q ∧ ∀ (x : α), p x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : SuccOrder α<VAR>a b : α<VAR>h₁ : a < b<VAR>h₂ : ¬IsMax b<GOAL>Ioo a (succ b) = insert b (Ioo a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E✝ I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>E B I : Set α<GOAL>(N.comapOn E f).Base B ↔ N.Basis' (f '' B) (f '' E) ∧ InjOn f B ∧ B ⊆ E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>n : ℕ<GOAL>range (n + 1) = insert 0 (map { toFun := fun i => i + 1, inj' := ⋯ } (range n))
<VAR>z : ℂ<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<GOAL>IsClosed {p | p.1 ≤ p.2}
<VAR>z : ℂ<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<GOAL>IsClosed ({a | a.1.re ≤ a.2.re} ∩ {a | a.1.im = a.2.im})