ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s✝ s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>s : Set (M × N)<VAR>p : M × N<GOAL>ContMDiffWithinAt (I.prod J) J n Prod.snd s p
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s✝ s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>s : Set (M × N)<VAR>p : M × N<GOAL>ContinuousWithinAt Prod.snd s p ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt J p.2) ∘ Prod.snd ∘ ↑(extChartAt (I.prod J) p).symm) ((extChartAt (I.prod J) p).target ∩ ↑(extChartAt (I.prod J) p).symm ⁻¹' (s ∩ Prod.snd ⁻¹' (extChartAt J p.2).source)) (↑(extChartAt (I.prod J) p) p)
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s✝ s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>s : Set (M × N)<VAR>p : M × N<VAR>y : E × F<VAR>hy : y ∈ (extChartAt (I.prod J) p).target ∩ ↑(extChartAt (I.prod J) p).symm ⁻¹' (s ∩ Prod.snd ⁻¹' (extChartAt J p.2).source)<GOAL>(↑(extChartAt J p.2) ∘ Prod.snd ∘ ↑(extChartAt (I.prod J) p).symm) y = y.2
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s✝ s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>s : Set (M × N)<VAR>p : M × N<GOAL>(↑(extChartAt J p.2) ∘ Prod.snd ∘ ↑(extChartAt (I.prod J) p).symm) (↑(extChartAt (I.prod J) p) p) = (↑(extChartAt (I.prod J) p) p).2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : ℕ → Set (β × γ)<VAR>hf_meas : ∀ (i : ℕ), MeasurableSet (f i)<VAR>hf_disj : Pairwise (Disjoint on f)<GOAL>κ.compProdFun η a (⋃ i, f i) = ∑' (i : ℕ), κ.compProdFun η a (f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : ℕ → Set (β × γ)<VAR>hf_meas : ∀ (i : ℕ), MeasurableSet (f i)<VAR>hf_disj : Pairwise (Disjoint on f)<VAR>h_Union : (fun b => (η (a, b)) {c | (b, c) ∈ ⋃ i, f i}) = fun b => (η (a, b)) (⋃ i, {c | (b, c) ∈ f i})<GOAL>κ.compProdFun η a (⋃ i, f i) = ∑' (i : ℕ), κ.compProdFun η a (f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : ℕ → Set (β × γ)<VAR>hf_meas : ∀ (i : ℕ), MeasurableSet (f i)<VAR>hf_disj : Pairwise (Disjoint on f)<VAR>h_Union : (fun b => (η (a, b)) {c | (b, c) ∈ ⋃ i, f i}) = fun b => (η (a, b)) (⋃ i, {c | (b, c) ∈ f i})<VAR>h_tsum : (fun b => (η (a, b)) (⋃ i, {c | (b, c) ∈ f i})) = fun b => ∑' (i : ℕ), (η (a, b)) {c | (b, c) ∈ f i}<GOAL>∫⁻ (b : β), (η (a, b)) (⋃ i, {c | (b, c) ∈ f i}) ∂κ a = ∑' (i : ℕ), κ.compProdFun η a (f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : ℕ → Set (β × γ)<VAR>hf_meas : ∀ (i : ℕ), MeasurableSet (f i)<VAR>hf_disj : Pairwise (Disjoint on f)<VAR>h_Union : (fun b => (η (a, b)) {c | (b, c) ∈ ⋃ i, f i}) = fun b => (η (a, b)) (⋃ i, {c | (b, c) ∈ f i})<VAR>h_tsum : (fun b => (η (a, b)) (⋃ i, {c | (b, c) ∈ f i})) = fun b => ∑' (i : ℕ), (η (a, b)) {c | (b, c) ∈ f i}<GOAL>∑' (i : ℕ), ∫⁻ (a_1 : β), (η (a, a_1)) {c | (a_1, c) ∈ f i} ∂κ a = ∑' (i : ℕ), κ.compProdFun η a (f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : ℕ → Set (β × γ)<VAR>hf_meas : ∀ (i : ℕ), MeasurableSet (f i)<VAR>hf_disj : Pairwise (Disjoint on f)<VAR>h_Union : (fun b => (η (a, b)) {c | (b, c) ∈ ⋃ i, f i}) = fun b => (η (a, b)) (⋃ i, {c | (b, c) ∈ f i})<VAR>h_tsum : (fun b => (η (a, b)) (⋃ i, {c | (b, c) ∈ f i})) = fun b => ∑' (i : ℕ), (η (a, b)) {c | (b, c) ∈ f i}<GOAL>∀ (i : ℕ), AEMeasurable (fun b => (η (a, b)) {c | (b, c) ∈ f i}) (κ a)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : Ring B'<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : Algebra A B'<VAR>x : B<VAR>hx : (minpoly A x).degree = 1<GOAL>x ∈ (algebraMap A B).range
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : Ring B'<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : Algebra A B'<VAR>x : B<VAR>hx : (minpoly A x).degree = 1<VAR>h : IsIntegral A x<GOAL>x ∈ (algebraMap A B).range
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : Ring B'<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : Algebra A B'<VAR>x : B<VAR>hx : (minpoly A x).degree = 1<VAR>h : IsIntegral A x<VAR>key : (Polynomial.aeval x) (minpoly A x) = 0<GOAL>x ∈ (algebraMap A B).range
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : Ring B'<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : Algebra A B'<VAR>x : B<VAR>hx : (minpoly A x).degree = 1<VAR>h : IsIntegral A x<VAR>key : x = (algebraMap A B) (-(minpoly A x).coeff 0)<GOAL>x ∈ (algebraMap A B).range
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z✝ : ℤ<VAR>a : α<VAR>z : ℤ<GOAL>z ≤ ⌊-a⌋ ↔ z ≤ -⌈a⌉
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>U : Set α<VAR>hU : IsOpen U<GOAL>∃ F, (∀ (n : ℕ), IsClosed (F n)) ∧ (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ n, F n = U ∧ Monotone F
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>U : Set α<VAR>hU : IsOpen U<VAR>a : ℝ≥0∞<VAR>a_pos : 0 < a<VAR>a_lt_one : a < 1<GOAL>∃ F, (∀ (n : ℕ), IsClosed (F n)) ∧ (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ n, F n = U ∧ Monotone F
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>U : Set α<VAR>hU : IsOpen U<VAR>a : ℝ≥0∞<VAR>a_pos : 0 < a<VAR>a_lt_one : a < 1<VAR>F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)<GOAL>∃ F, (∀ (n : ℕ), IsClosed (F n)) ∧ (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ n, F n = U ∧ Monotone F
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>U : Set α<VAR>hU : IsOpen U<VAR>a : ℝ≥0∞<VAR>a_pos : 0 < a<VAR>a_lt_one : a < 1<VAR>F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)<VAR>F_subset : ∀ (n : ℕ), F n ⊆ U<GOAL>∃ F, (∀ (n : ℕ), IsClosed (F n)) ∧ (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ n, F n = U ∧ Monotone F
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>U : Set α<VAR>hU : IsOpen U<VAR>a : ℝ≥0∞<VAR>a_pos : 0 < a<VAR>a_lt_one : a < 1<VAR>F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)<VAR>F_subset : ∀ (n : ℕ), F n ⊆ U<GOAL>⋃ n, F n = U
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>U : Set α<VAR>hU : IsOpen U<VAR>a : ℝ≥0∞<VAR>a_pos : 0 < a<VAR>a_lt_one : a < 1<VAR>F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)<VAR>F_subset : ∀ (n : ℕ), F n ⊆ U<GOAL>Monotone F
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x✝ y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>U : Set α<VAR>hU : IsOpen U<VAR>a : ℝ≥0∞<VAR>a_pos : 0 < a<VAR>a_lt_one : a < 1<VAR>F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)<VAR>F_subset : ∀ (n : ℕ), F n ⊆ U<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>x : α<VAR>hx : x ∈ F m<GOAL>x ∈ F n
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x✝ y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>U : Set α<VAR>hU : IsOpen U<VAR>a : ℝ≥0∞<VAR>a_pos : 0 < a<VAR>a_lt_one : a < 1<VAR>F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)<VAR>F_subset : ∀ (n : ℕ), F n ⊆ U<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>x : α<VAR>hx : a ^ m ≤ infEdist x Uᶜ<GOAL>a ^ n ≤ infEdist x Uᶜ
<VAR>f : ℍ → ℂ<GOAL>(∀ (ib : ℝ), 0 < ib → ∃ ia, True ∧ ∀ x ∈ im ⁻¹' Set.Ici ia, f x ∈ Metric.closedBall 0 ib) ↔ ∀ (ε : ℝ), 0 < ε → ∃ A, ∀ (z : ℍ), A ≤ z.im → Complex.abs (f z) ≤ ε
<VAR>f : ℍ → ℂ<GOAL>(∀ (ib : ℝ), 0 < ib → ∃ ia, ∀ x ∈ im ⁻¹' Set.Ici ia, ‖f x‖ ≤ ib) ↔ ∀ (ε : ℝ), 0 < ε → ∃ A, ∀ (z : ℍ), A ≤ z.im → Complex.abs (f z) ≤ ε
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>inst✝ : IsNoetherian R M<VAR>f : M →ₗ[R] M<GOAL>∀ᶠ (n : ℕ) in atTop, ⨆ m, ker (f ^ m) = ker (f ^ n)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>inst✝ : IsNoetherian R M<VAR>f : M →ₗ[R] M<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → ker (f ^ n) = ker (f ^ m)<GOAL>∀ᶠ (n : ℕ) in atTop, ⨆ m, ker (f ^ m) = ker (f ^ n)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>inst✝ : IsNoetherian R M<VAR>f : M →ₗ[R] M<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → ker (f ^ n) = ker (f ^ m)<VAR>m : ℕ<VAR>hm : m ≥ n<GOAL>⨆ m, ker (f ^ m) = ker (f ^ m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>inst✝ : IsNoetherian R M<VAR>f : M →ₗ[R] M<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → ker (f ^ n) = ker (f ^ m)<VAR>m : ℕ<VAR>hm : m ≥ n<VAR>l : ℕ<GOAL>ker (f ^ l) ≤ ker (f ^ m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>inst✝ : IsNoetherian R M<VAR>f : M →ₗ[R] M<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → ker (f ^ n) = ker (f ^ m)<VAR>m : ℕ<VAR>hm : m ≥ n<VAR>l : ℕ<VAR>h : m ≤ l<GOAL>ker (f ^ l) ≤ ker (f ^ m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>inst✝ : IsNoetherian R M<VAR>f : M →ₗ[R] M<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → ker (f ^ n) = ker (f ^ m)<VAR>m : ℕ<VAR>hm : m ≥ n<VAR>l : ℕ<VAR>h : l < m<GOAL>ker (f ^ l) ≤ ker (f ^ m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>a b c : CauSeq α abs<VAR>εb : α<VAR>εb0 : εb > 0<VAR>ib : ℕ<VAR>hb : ∀ j ≥ ib, εb ≤ ↑(b - a) j<VAR>εc : α<VAR>εc0 : εc > 0<VAR>ic : ℕ<VAR>hc : ∀ j ≥ ic, εc ≤ ↑(c - a) j<GOAL>a < b ⊓ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>a b c : CauSeq α abs<VAR>εb : α<VAR>εb0 : εb > 0<VAR>ib : ℕ<VAR>hb : ∀ j ≥ ib, εb ≤ ↑(b - a) j<VAR>εc : α<VAR>εc0 : εc > 0<VAR>ic : ℕ<VAR>hc : ∀ j ≥ ic, εc ≤ ↑(c - a) j<VAR>i : ℕ<VAR>hi : i ≥ ib ⊔ ic<GOAL>εb ⊓ εc ≤ ↑(b ⊓ c - a) i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>a b c : CauSeq α abs<VAR>εb : α<VAR>εb0 : εb > 0<VAR>ib : ℕ<VAR>hb : ∀ j ≥ ib, εb ≤ ↑(b - a) j<VAR>εc : α<VAR>εc0 : εc > 0<VAR>ic : ℕ<VAR>hc : ∀ j ≥ ic, εc ≤ ↑(c - a) j<VAR>i : ℕ<VAR>hi : i ≥ ib ⊔ ic<VAR>this : min εb εc ≤ min (↑(b - a) i) (↑(c - a) i)<GOAL>εb ⊓ εc ≤ ↑(b ⊓ c - a) i
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>x : S<GOAL>(x𝖣1) = 0
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>E✝ : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜✝ : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁵ : Norm E✝<VAR>inst✝¹⁴ : Norm F<VAR>inst✝¹³ : Norm G<VAR>inst✝¹² : SeminormedAddCommGroup E'<VAR>inst✝¹¹ : SeminormedAddCommGroup F'<VAR>inst✝¹⁰ : SeminormedAddCommGroup G'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F''<VAR>inst✝⁷ : NormedAddCommGroup G''<VAR>inst✝⁶ : SeminormedRing R<VAR>inst✝⁵ : SeminormedAddGroup E'''<VAR>inst✝⁴ : SeminormedRing R'<VAR>inst✝³ : NormedDivisionRing 𝕜✝<VAR>inst✝² : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α✝ → E✝<VAR>g : α✝ → F<VAR>k : α✝ → G<VAR>f' : α✝ → E'<VAR>g' : α✝ → F'<VAR>k' : α✝ → G'<VAR>f'' : α✝ → E''<VAR>g'' : α✝ → F''<VAR>k'' : α✝ → G''<VAR>l✝ l' : Filter α✝<VAR>α : Type u_17<VAR>E : Type u_18<VAR>𝕜 : Type u_19<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedField 𝕜<VAR>u : α → E<VAR>v : α → 𝕜<VAR>l : Filter α<VAR>y : 𝕜<VAR>huv : u =o[l] v<VAR>hv : Tendsto v l (𝓝 y)<GOAL>Tendsto u l (𝓝 0)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>E✝ : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜✝ : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁵ : Norm E✝<VAR>inst✝¹⁴ : Norm F<VAR>inst✝¹³ : Norm G<VAR>inst✝¹² : SeminormedAddCommGroup E'<VAR>inst✝¹¹ : SeminormedAddCommGroup F'<VAR>inst✝¹⁰ : SeminormedAddCommGroup G'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F''<VAR>inst✝⁷ : NormedAddCommGroup G''<VAR>inst✝⁶ : SeminormedRing R<VAR>inst✝⁵ : SeminormedAddGroup E'''<VAR>inst✝⁴ : SeminormedRing R'<VAR>inst✝³ : NormedDivisionRing 𝕜✝<VAR>inst✝² : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α✝ → E✝<VAR>g : α✝ → F<VAR>k : α✝ → G<VAR>f' : α✝ → E'<VAR>g' : α✝ → F'<VAR>k' : α✝ → G'<VAR>f'' : α✝ → E''<VAR>g'' : α✝ → F''<VAR>k'' : α✝ → G''<VAR>l✝ l' : Filter α✝<VAR>α : Type u_17<VAR>E : Type u_18<VAR>𝕜 : Type u_19<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedField 𝕜<VAR>u : α → E<VAR>v : α → 𝕜<VAR>l : Filter α<VAR>y : 𝕜<VAR>huv : u =o[l] v<VAR>hv : Tendsto v l (𝓝 y)<GOAL>u =o[l] fun _x => 1
<VAR>i j k : ℤ<GOAL>(i * j).gcd (i * k) = i.natAbs * j.gcd k
<VAR>i j k : ℤ<GOAL>(i.natAbs * j.natAbs).gcd (i.natAbs * k.natAbs) = i.natAbs * j.natAbs.gcd k.natAbs
<VAR>E✝ : Type u_1<VAR>inst✝¹² : NormedAddCommGroup E✝<VAR>inst✝¹¹ : NormedSpace ℝ E✝<VAR>inst✝¹⁰ : MeasurableSpace E✝<VAR>inst✝⁹ : BorelSpace E✝<VAR>inst✝⁸ : FiniteDimensional ℝ E✝<VAR>μ✝ : Measure E✝<VAR>inst✝⁷ : μ✝.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>s : Set E✝<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>x : E<VAR>r : ℝ<VAR>this : closedBall 0 r = (fun x_1 => x + x_1) ⁻¹' closedBall x r<GOAL>μ (closedBall x r) = μ (closedBall 0 r)
<VAR>α : Type u_1<VAR>f : Perm α<VAR>n : ℕ<VAR>x : α<GOAL>f ((f ^ n) x) = (f ^ n) x ↔ f x = x
<VAR>m n : ℕ<GOAL>(fib m).gcd (fib (n + m)) = (fib m).gcd (fib n)
<VAR>m : ℕ<GOAL>(fib m).gcd (fib (0 + m)) = (fib m).gcd (fib 0)
<VAR>m n : ℕ<VAR>h : n > 0<GOAL>(fib m).gcd (fib (n + m)) = (fib m).gcd (fib n)
<VAR>m n : ℕ<VAR>h : n.pred.succ = n<GOAL>(fib m).gcd (fib (n + m)) = (fib m).gcd (fib n)
<VAR>m n : ℕ<VAR>h : n.pred.succ = n<GOAL>(fib m).gcd (fib (n.pred + 1 + m)) = (fib m).gcd (fib (n.pred + 1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Preorder β<VAR>a : α<VAR>f : α → β<VAR>h₁ : MonotoneOn f (Iic a)<VAR>h₂ : MonotoneOn f (Ici a)<GOAL>Monotone f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Preorder β<VAR>a : α<VAR>f : α → β<VAR>h₁ : MonotoneOn f (Iic a)<VAR>h₂ : MonotoneOn f (Ici a)<GOAL>MonotoneOn f (Iic a ∪ Ici a)