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✝ n : ℕ∞<VAR>s : Set H<VAR>x : H<VAR>t : Set H<VAR>f : H → H'<VAR>hts : s ∈ 𝓝[t] x<VAR>h : ContDiffWithinAtProp I I' n f s x<GOAL>ContDiffWithinAtProp I I' n f t x
<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✝ n : ℕ∞<VAR>s : Set H<VAR>x : H<VAR>t : Set H<VAR>f : H → H'<VAR>hts : s ∈ 𝓝[t] x<VAR>h : ContDiffWithinAtProp I I' n f s x<GOAL>↑I.symm ⁻¹' s ∩ range ↑I ∈ 𝓝[↑I.symm ⁻¹' t ∩ range ↑I] ↑I x
<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✝ n : ℕ∞<VAR>s : Set H<VAR>x : H<VAR>t : Set H<VAR>f : H → H'<VAR>hts : s ∈ 𝓝[t] x<VAR>h : ContDiffWithinAtProp I I' n f s x<GOAL>↑I.symm ⁻¹' s ∈ 𝓝[↑I.symm ⁻¹' t ∩ range ↑I] ↑I x
<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>inst✝¹ : SemilatticeSup α<VAR>s✝ : Finset β<VAR>H✝ : s✝.Nonempty<VAR>f✝ : β → α<VAR>inst✝ : SemilatticeSup γ<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f : β → α<VAR>g : α → γ<VAR>g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y<GOAL>g (s.sup' H f) = s.sup' H (g ∘ f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>hf : IsCauSeq abv f<VAR>ε : α<VAR>ε0 : 0 < ε<GOAL>∃ i, ∀ j ≥ i, ∀ k ≥ i, abv (f j - f k) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>hf : IsCauSeq abv f<VAR>ε : α<VAR>ε0 : 0 < ε<VAR>i : ℕ<VAR>hi : ∀ j ≥ i, abv (f j - f i) < ε / 2<VAR>j : ℕ<VAR>ij : j ≥ i<VAR>k : ℕ<VAR>ik : k ≥ i<GOAL>abv (f j - f k) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>hf : IsCauSeq abv f<VAR>ε : α<VAR>ε0 : 0 < ε<VAR>i : ℕ<VAR>hi : ∀ j ≥ i, abv (f j - f i) < ε / 2<VAR>j : ℕ<VAR>ij : j ≥ i<VAR>k : ℕ<VAR>ik : k ≥ i<GOAL>abv (f j - f k) < ε / 2 + ε / 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>hf : IsCauSeq abv f<VAR>ε : α<VAR>ε0 : 0 < ε<VAR>i : ℕ<VAR>hi : ∀ j ≥ i, abv (f j - f i) < ε / 2<VAR>j : ℕ<VAR>ij : j ≥ i<VAR>k : ℕ<VAR>ik : k ≥ i<GOAL>abv (f i - f k) < ε / 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>hf : IsCauSeq abv f<VAR>ε : α<VAR>ε0 : 0 < ε<VAR>i : ℕ<VAR>hi : ∀ j ≥ i, abv (f j - f i) < ε / 2<VAR>j : ℕ<VAR>ij : j ≥ i<VAR>k : ℕ<VAR>ik : k ≥ i<GOAL>abv (f k - f i) < ε / 2
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : AffineSpace V P<VAR>inst✝² : Ring k<VAR>inst✝¹ : Module k V<VAR>b : AffineBasis ι k P<VAR>s : Finset ι<VAR>i✝ j : ι<VAR>e : ι ≃ ι'<VAR>inst✝ : Nontrivial ι<VAR>i : ι<GOAL>Function.Surjective ⇑(b.coord i)
<VAR>α : Type u_1<VAR>inst✝ : AddCommGroupWithOne α<VAR>m : ℤ<VAR>x✝ : ℕ<VAR>ih : ∀ (n : ℤ), ↑(↑x✝ * n) = ↑x✝ • ↑n<GOAL>∀ (n : ℤ), ↑((↑x✝ + 1) * n) = (↑x✝ + 1) • ↑n
<VAR>α : Type u_1<VAR>inst✝ : AddCommGroupWithOne α<VAR>m : ℤ<VAR>x✝ : ℕ<VAR>ih : ∀ (n : ℤ), ↑(-↑x✝ * n) = -↑x✝ • ↑n<GOAL>∀ (n : ℤ), ↑((-↑x✝ - 1) * n) = (-↑x✝ - 1) • ↑n
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p q : R[X]<VAR>hpq : q.degree ≤ p.degree<VAR>hq : ¬q = 0<GOAL>(p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p q : R[X]<VAR>hpq : q.degree ≤ p.degree<VAR>hq : ¬q = 0<GOAL>(q * C q.leadingCoeff⁻¹).degree ≤ p.degree
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝ : CommMonoidWithZero R'<VAR>χ : MulChar R R'<GOAL>χ = 1 ↔ ∀ (a : Rˣ), χ ↑a = 1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : LinearOrderedSemifield α<VAR>l : Filter β<VAR>f : β → α<VAR>r c : α<VAR>n : ℕ<VAR>inst✝ : l.NeBot<VAR>h : Tendsto f l atTop<GOAL>Tendsto (fun x => f x / r) l atTop ↔ 0 < r
<VAR>n : PosNum<GOAL>(if (match Num.pos n with | Num.zero => [] | Num.pos n => encodePosNum n) = [] then Num.zero else ↑(decodePosNum (match Num.pos n with | Num.zero => [] | Num.pos n => encodePosNum n))) = Num.pos n
<VAR>n : PosNum<GOAL>(if (match Num.pos n with | Num.zero => [] | Num.pos n => encodePosNum n) = [] then Num.zero else ↑n) = Num.pos n
<VAR>n : PosNum<GOAL>(if (match Num.pos n with | Num.zero => [] | Num.pos n => encodePosNum n) = [] then Num.zero else Num.pos n) = Num.pos n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁵ : Zero α<VAR>inst✝⁴ : Zero β<VAR>inst✝³ : SMulWithZero α β<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : SMulPosMono α β<VAR>ha : a ≤ 0<VAR>hb : 0 ≤ b<GOAL>a • b ≤ 0
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Semiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module Rᵐᵒᵖ M<VAR>x : tsze R M<VAR>r : R<GOAL>x.fst •> 0 + x.snd <• r = x.snd <• r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hf : Memℒp f 1 μ<VAR>hmeas : StronglyMeasurable f<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ M, ∫⁻ (x : α), ↑‖{x | M ≤ ↑‖f x‖₊}.indicator f x‖₊ ∂μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hf : Memℒp f 1 μ<VAR>hmeas : StronglyMeasurable f<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)<GOAL>∃ M, ∫⁻ (x : α), ↑‖{x | M ≤ ↑‖f x‖₊}.indicator f x‖₊ ∂μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hf : Memℒp f 1 μ<VAR>hmeas✝ : StronglyMeasurable f<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)<VAR>hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ<GOAL>∃ M, ∫⁻ (x : α), ↑‖{x | M ≤ ↑‖f x‖₊}.indicator f x‖₊ ∂μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hf : Memℒp f 1 μ<VAR>hmeas✝ : StronglyMeasurable f<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)<VAR>hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ<VAR>hbound : HasFiniteIntegral (fun x => ‖f x‖) μ<GOAL>∃ M, ∫⁻ (x : α), ↑‖{x | M ≤ ↑‖f x‖₊}.indicator f x‖₊ ∂μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hf : Memℒp f 1 μ<VAR>hmeas✝ : StronglyMeasurable f<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)<VAR>hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ<VAR>hbound : HasFiniteIntegral (fun x => ‖f x‖) μ<VAR>this : Tendsto (fun n => ∫⁻ (a : α), ENNReal.ofReal ‖{x | ↑n ≤ ‖f x‖₊}.indicator f a - 0‖ ∂μ) atTop (𝓝 0)<GOAL>∃ M, ∫⁻ (x : α), ↑‖{x | M ≤ ↑‖f x‖₊}.indicator f x‖₊ ∂μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hf : Memℒp f 1 μ<VAR>hmeas✝ : StronglyMeasurable f<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)<VAR>hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ<VAR>hbound : HasFiniteIntegral (fun x => ‖f x‖) μ<VAR>this : ∀ ε > 0, ∃ N, ∀ n ≥ N, ∫⁻ (a : α), ENNReal.ofReal ‖{x | ↑n ≤ ‖f x‖₊}.indicator f a - 0‖ ∂μ ≤ ε<GOAL>∃ M, ∫⁻ (x : α), ↑‖{x | M ≤ ↑‖f x‖₊}.indicator f x‖₊ ∂μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hf : Memℒp f 1 μ<VAR>hmeas✝ : StronglyMeasurable f<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)<VAR>hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ<VAR>hbound : HasFiniteIntegral (fun x => ‖f x‖) μ<VAR>this : ∀ ε > 0, ∃ N, ∀ n ≥ N, ∫⁻ (a : α), ENNReal.ofReal ‖{x | ↑n ≤ ‖f x‖₊}.indicator f a - 0‖ ∂μ ≤ ε<VAR>M : ℕ<VAR>hM : ∀ n ≥ M, ∫⁻ (a : α), ENNReal.ofReal ‖{x | ↑n ≤ ‖f x‖₊}.indicator f a - 0‖ ∂μ ≤ ENNReal.ofReal ε<GOAL>∃ M, ∫⁻ (x : α), ↑‖{x | M ≤ ↑‖f x‖₊}.indicator f x‖₊ ∂μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hf : Memℒp f 1 μ<VAR>hmeas✝ : StronglyMeasurable f<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)<VAR>hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ<VAR>hbound : HasFiniteIntegral (fun x => ‖f x‖) μ<VAR>this : ∀ ε > 0, ∃ N, ∀ n ≥ N, ∫⁻ (a : α), ENNReal.ofReal ‖{x | ↑n ≤ ‖f x‖₊}.indicator f a - 0‖ ∂μ ≤ ε<VAR>M : ℕ<VAR>hM : ∀ n ≥ M, ∫⁻ (a : α), ENNReal.ofReal ‖{x | ↑n ≤ ‖f x‖₊}.indicator f a‖ ∂μ ≤ ENNReal.ofReal ε<GOAL>∃ M, ∫⁻ (x : α), ↑‖{x | M ≤ ↑‖f x‖₊}.indicator f x‖₊ ∂μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hf : Memℒp f 1 μ<VAR>hmeas✝ : StronglyMeasurable f<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)<VAR>hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ<VAR>hbound : HasFiniteIntegral (fun x => ‖f x‖) μ<VAR>this : ∀ ε > 0, ∃ N, ∀ n ≥ N, ∫⁻ (a : α), ENNReal.ofReal ‖{x | ↑n ≤ ‖f x‖₊}.indicator f a - 0‖ ∂μ ≤ ε<VAR>M : ℕ<VAR>hM : ∀ n ≥ M, ∫⁻ (a : α), ENNReal.ofReal ‖{x | ↑n ≤ ‖f x‖₊}.indicator f a‖ ∂μ ≤ ENNReal.ofReal ε<GOAL>∫⁻ (x : α), ↑‖{x | ↑M ≤ ↑‖f x‖₊}.indicator f x‖₊ ∂μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hf : Memℒp f 1 μ<VAR>hmeas✝ : StronglyMeasurable f<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)<VAR>hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ<VAR>hbound : HasFiniteIntegral (fun x => ‖f x‖) μ<VAR>this : ∀ ε > 0, ∃ N, ∀ n ≥ N, ∫⁻ (a : α), ENNReal.ofReal ‖{x | ↑n ≤ ‖f x‖₊}.indicator f a - 0‖ ∂μ ≤ ε<VAR>M : ℕ<VAR>hM : ∀ n ≥ M, ∫⁻ (a : α), ENNReal.ofReal ‖{x | ↑n ≤ ‖f x‖₊}.indicator f a‖ ∂μ ≤ ENNReal.ofReal ε<VAR>x✝ : α<GOAL>↑‖{x | ↑M ≤ ↑‖f x‖₊}.indicator f x✝‖₊ = ENNReal.ofReal ‖{x | ↑M ≤ ‖f x‖₊}.indicator f x✝‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hf : Memℒp f 1 μ<VAR>hmeas✝ : StronglyMeasurable f<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M => {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)<VAR>hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ<VAR>hbound : HasFiniteIntegral (fun x => ‖f x‖) μ<VAR>this : ∀ ε > 0, ∃ N, ∀ n ≥ N, ∫⁻ (a : α), ENNReal.ofReal ‖{x | ↑n ≤ ‖f x‖₊}.indicator f a - 0‖ ∂μ ≤ ε<VAR>M : ℕ<VAR>hM : ∀ n ≥ M, ∫⁻ (a : α), ENNReal.ofReal ‖{x | ↑n ≤ ‖f x‖₊}.indicator f a‖ ∂μ ≤ ENNReal.ofReal ε<VAR>x✝ : α<GOAL>↑‖{x | ↑M ≤ ‖f x‖}.indicator f x✝‖₊ = ↑⟨‖{x | ↑M ≤ ‖f x‖₊}.indicator f x✝‖, ⋯⟩
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>r : ℝ<GOAL>⟪x, r • (o.rotation ↑(π / 2)) x⟫_ℝ = 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>f : α → β<VAR>a : α<VAR>h : ScottContinuous f<GOAL>Monotone f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>f : α → β<VAR>a✝ : α<VAR>h : ScottContinuous f<VAR>a b : α<VAR>hab : a ≤ b<GOAL>IsLUB {a, b} b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>f : α → β<VAR>a✝ : α<VAR>h : ScottContinuous f<VAR>a b : α<VAR>hab : a ≤ b<GOAL>IsLeast (Ici b) b
<VAR>α : Type u_1<VAR>inst✝² : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝¹ : DivisionRing β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>hf : ¬f.LimZero<GOAL>(if h : f.LimZero then 0 else f.inv h) = f.inv hf
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J₁ J₂ : GrothendieckTopology C<VAR>c : (X : C) → ClosureOperator (Sieve X)<VAR>hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), (c Y) (Sieve.pullback f S) = Sieve.pullback f ((c X) S)<VAR>X Y : C<VAR>S : Sieve X<VAR>f : Y ⟶ X<VAR>hS : S ∈ (fun X => {S | (c X) S = ⊤}) X<GOAL>Sieve.pullback f S ∈ (fun X => {S | (c X) S = ⊤}) Y
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J₁ J₂ : GrothendieckTopology C<VAR>c : (X : C) → ClosureOperator (Sieve X)<VAR>hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), (c Y) (Sieve.pullback f S) = Sieve.pullback f ((c X) S)<VAR>X Y : C<VAR>S : Sieve X<VAR>f : Y ⟶ X<VAR>hS : (c X) S = ⊤<GOAL>Sieve.pullback f S ∈ (fun X => {S | (c X) S = ⊤}) Y
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J₁ J₂ : GrothendieckTopology C<VAR>c : (X : C) → ClosureOperator (Sieve X)<VAR>hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), (c Y) (Sieve.pullback f S) = Sieve.pullback f ((c X) S)<VAR>X : C<VAR>S : Sieve X<VAR>hS : S ∈ (fun X => {S | (c X) S = ⊤}) X<VAR>R : Sieve X<VAR>hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X => {S | (c X) S = ⊤}) Y<GOAL>R ∈ (fun X => {S | (c X) S = ⊤}) X
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J₁ J₂ : GrothendieckTopology C<VAR>c : (X : C) → ClosureOperator (Sieve X)<VAR>hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), (c Y) (Sieve.pullback f S) = Sieve.pullback f ((c X) S)<VAR>X : C<VAR>S : Sieve X<VAR>hS : (c X) S = ⊤<VAR>R : Sieve X<VAR>hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X => {S | (c X) S = ⊤}) Y<GOAL>R ∈ (fun X => {S | (c X) S = ⊤}) X
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J₁ J₂ : GrothendieckTopology C<VAR>c : (X : C) → ClosureOperator (Sieve X)<VAR>hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), (c Y) (Sieve.pullback f S) = Sieve.pullback f ((c X) S)<VAR>X : C<VAR>S : Sieve X<VAR>hS : (c X) S = ⊤<VAR>R : Sieve X<VAR>hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X => {S | (c X) S = ⊤}) Y<GOAL>(c X) S ≤ (c X) ((c X) R)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J₁ J₂ : GrothendieckTopology C<VAR>c : (X : C) → ClosureOperator (Sieve X)<VAR>hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), (c Y) (Sieve.pullback f S) = Sieve.pullback f ((c X) S)<VAR>X : C<VAR>S : Sieve X<VAR>hS : (c X) S = ⊤<VAR>R : Sieve X<VAR>hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X => {S | (c X) S = ⊤}) Y<GOAL>∀ (Y : C) (f : Y ⟶ X), S.arrows f → ((c X) R).arrows f
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J₁ J₂ : GrothendieckTopology C<VAR>c : (X : C) → ClosureOperator (Sieve X)<VAR>hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), (c Y) (Sieve.pullback f S) = Sieve.pullback f ((c X) S)<VAR>X : C<VAR>S : Sieve X<VAR>hS : (c X) S = ⊤<VAR>R : Sieve X<VAR>hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X => {S | (c X) S = ⊤}) Y<VAR>Y : C<VAR>f : Y ⟶ X<VAR>hf : S.arrows f<GOAL>((c X) R).arrows f
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J₁ J₂ : GrothendieckTopology C<VAR>c : (X : C) → ClosureOperator (Sieve X)<VAR>hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), (c Y) (Sieve.pullback f S) = Sieve.pullback f ((c X) S)<VAR>X : C<VAR>S : Sieve X<VAR>hS : (c X) S = ⊤<VAR>R : Sieve X<VAR>hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X => {S | (c X) S = ⊤}) Y<VAR>Y : C<VAR>f : Y ⟶ X<VAR>hf : S.arrows f<GOAL>(c Y) (Sieve.pullback f R) = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Fintype α<VAR>n : ℕ<GOAL>Fintype.card (Vector α n) = Fintype.card α ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Fintype α<VAR>n : ℕ<GOAL>Fintype.card (Fin n → α) = Fintype.card α ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>x : G<GOAL>↑↑((condexpInd G hm μ ∅) x) =ᶠ[ae μ] ↑↑(0 x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>x : G<GOAL>↑↑(condexpIndSMul hm ⋯ ⋯ x) =ᶠ[ae μ] ↑↑(0 x)