ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : StrictConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' S y<GOAL>S ∈ 𝓝[<] y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : StrictConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' S y<GOAL>∃ l ∈ Iio y, Ico l y ⊆ S
<VAR>E : Type uE<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<GOAL>support ↑f = (chartAt H c).source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) f.rOut
<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>X Y : Scheme<VAR>f : X ⟶ Y<GOAL>UniversallyClosed f ↔ (topologically @IsClosedMap).universally f
<VAR>α : Type u<VAR>β✝ : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>β : Type u_3<VAR>p : β → Prop<VAR>f : β → ℝ<VAR>hf₀ : ∀ (x : β), p x → 0 < f x<VAR>hf : ∀ (ε : ℝ), 0 < ε → ∃ x, p x ∧ f x ≤ ε<GOAL>(𝓤 α).HasBasis p fun x => {p | dist p.1 p.2 ≤ f x}
<VAR>α : Type u<VAR>β✝ : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s✝ : Set α<VAR>β : Type u_3<VAR>p : β → Prop<VAR>f : β → ℝ<VAR>hf₀ : ∀ (x : β), p x → 0 < f x<VAR>hf : ∀ (ε : ℝ), 0 < ε → ∃ x, p x ∧ f x ≤ ε<VAR>s : Set (α × α)<GOAL>(∃ i, 0 < i ∧ {p | dist p.1 p.2 < i} ⊆ s) ↔ ∃ i, p i ∧ {p | dist p.1 p.2 ≤ f i} ⊆ s
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>inst✝ : Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Injective ⇑(φ i)<VAR>w : Word G<VAR>hw : Reduced φ w<VAR>h : ofCoprodI w.prod ∈ (base φ).range<GOAL>w = Word.empty
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>inst✝ : Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Injective ⇑(φ i)<VAR>w : Word G<VAR>hw : Reduced φ w<VAR>h : ofCoprodI w.prod ∈ (base φ).range<VAR>d : Transversal φ<GOAL>w = Word.empty
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>inst✝ : Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Injective ⇑(φ i)<VAR>w : Word G<VAR>hw : Reduced φ w<VAR>h : ofCoprodI w.prod ∈ (base φ).range<VAR>d : Transversal φ<VAR>w' : NormalWord d<VAR>hw'prod : w'.prod = ofCoprodI w.prod<VAR>hw'map : List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList<GOAL>w = Word.empty
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>inst✝ : Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Injective ⇑(φ i)<VAR>w : Word G<VAR>hw : Reduced φ w<VAR>d : Transversal φ<VAR>w' : NormalWord d<VAR>hw'prod : w'.prod = ofCoprodI w.prod<VAR>hw'map : List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList<VAR>h : H<VAR>heq : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = w'.prod<VAR>this : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = (base φ) h<GOAL>w = Word.empty
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>inst✝ : Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Injective ⇑(φ i)<VAR>w : Word G<VAR>hw : Reduced φ w<VAR>d : Transversal φ<VAR>w' : NormalWord d<VAR>hw'prod : w'.prod = ofCoprodI w.prod<VAR>hw'map : List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList<VAR>h : H<VAR>heq : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = w'.prod<VAR>this : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = (base φ) h<GOAL>w'.toWord = Word.empty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p a b : α<VAR>hp : Prime p<VAR>n : ℕ<VAR>h : ¬p ∣ b<VAR>h' : p ^ n ∣ a * b<GOAL>p ^ n ∣ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p a b : α<VAR>hp : Prime p<VAR>n : ℕ<VAR>h : ¬p ∣ b<VAR>h' : p ^ n ∣ b * a<GOAL>p ^ n ∣ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{?u.29963}<GOAL>o < type fun x x_1 => x < x_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{?u.29963}<GOAL>o < succ o
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>R : Type u_7<VAR>R₂ : Type u_8<VAR>M : Type u_9<VAR>M₂ : Type u_10<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring R₂<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R₂ M₂<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : TopologicalSpace M₂<VAR>σ : R →+* R₂<VAR>σ' : R₂ →+* R<VAR>inst✝¹ : RingHomInvPair σ σ'<VAR>inst✝ : RingHomInvPair σ' σ<VAR>f : ι → M<VAR>e : M ≃SL[σ] M₂<VAR>y : M₂<VAR>h : HasSum (fun b => e (f b)) y<GOAL>HasSum f (e.symm y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>R : Type u_7<VAR>R₂ : Type u_8<VAR>M : Type u_9<VAR>M₂ : Type u_10<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring R₂<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R₂ M₂<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : TopologicalSpace M₂<VAR>σ : R →+* R₂<VAR>σ' : R₂ →+* R<VAR>inst✝¹ : RingHomInvPair σ σ'<VAR>inst✝ : RingHomInvPair σ' σ<VAR>f : ι → M<VAR>e : M ≃SL[σ] M₂<VAR>y : M₂<VAR>h : HasSum f (e.symm y)<GOAL>HasSum (fun b => e (f b)) y
<VAR>c : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ c<GOAL>c ^< ℵ₀ = c
<VAR>c : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ c<GOAL>c ^< ℵ₀ ≤ c
<VAR>c : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ c<GOAL>c ≤ c ^< ℵ₀
<VAR>c : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ c<GOAL>c = c ^ 1
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>S : AddSubmonoid R<VAR>m : R<VAR>hm : m ∈ ⊥<VAR>n : R<VAR>hn : n ∈ S<GOAL>m * n ∈ ⊥
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>S : AddSubmonoid R<VAR>m : R<VAR>hm : m = 0<VAR>n : R<VAR>hn : n ∈ S<GOAL>m * n = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ l₃ : List α<VAR>a b : α<VAR>m n : ℕ<VAR>s : List α<GOAL>s ∈ [].tails ↔ s <:+ []
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ l₃ : List α<VAR>a✝ b : α<VAR>m n : ℕ<VAR>s : List α<VAR>a : α<VAR>t : List α<GOAL>s ∈ (a :: t).tails ↔ s <:+ a :: t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ l₃ : List α<VAR>a✝ b : α<VAR>m n : ℕ<VAR>s : List α<VAR>a : α<VAR>t : List α<GOAL>s = a :: t ∨ s <:+ t ↔ s <:+ a :: t
<VAR>F : Type w<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type u_1<VAR>inst✝⁴ : NonUnitalNonAssocRing R<VAR>inst✝³ : NonUnitalNonAssocRing S✝<VAR>inst✝² : NonUnitalNonAssocRing T<VAR>inst✝¹ : FunLike F R S✝<VAR>inst✝ : NonUnitalRingHomClass F R S✝<VAR>g : S✝ →ₙ+* T<VAR>f : R →ₙ+* S✝<VAR>ι : Sort u_2<VAR>S : ι → NonUnitalSubring R<VAR>x : R<GOAL>x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>s : Set E<VAR>r✝ : ℝ<VAR>x✝ : E<VAR>r : ℝ≥0<VAR>hc : Convex ℝ s<VAR>hr : 0 < r<VAR>hs : ball 0 ↑r ⊆ s<VAR>this : Absorbent ℝ (ball 0 ↑r)<VAR>x y : E<GOAL>gauge s y + ‖x - y‖ / ↑r = gauge s y + ↑r⁻¹ * dist x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<GOAL>log 2 * 2 ≤ √(log 8)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>this : 8 = 2 ^ ↑3<GOAL>log 2 * 2 ≤ √(log 8)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>this : 8 = 2 ^ ↑3<GOAL>log 2 * 2 ≤ √(↑3 * log 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>this : 8 = 2 ^ ↑3<GOAL>(log 2 * 2) ^ 2 ≤ ↑3 * log 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>this : 8 = 2 ^ ↑3<GOAL>log 2 * 2 ^ 2 * log 2 ≤ ↑3 * log 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>this : 8 = 2 ^ ↑3<GOAL>log 2 * 2 ^ 2 ≤ ↑3
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>this : 8 = 2 ^ ↑3<GOAL>log 2 ≤ ↑3 / 2 ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>this : 8 = 2 ^ ↑3<GOAL>0 < 2 ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>this : 8 = 2 ^ ↑3<GOAL>0.6931471808 ≤ ↑3 / 2 ^ 2
<VAR>f✝ f g : ℝ → ℝ<VAR>hf : GrowsPolynomially f<VAR>hfg : g =o[atTop] f<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<GOAL>∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => f x + g x) u ∈ Set.Icc (c₁ * (fun x => f x + g x) x) (c₂ * (fun x => f x + g x) x)
<VAR>f✝ f g : ℝ → ℝ<VAR>hf : GrowsPolynomially f<VAR>hfg : g =o[atTop] f<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hb_ub : b < 1<GOAL>∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => f x + g x) u ∈ Set.Icc (c₁ * (fun x => f x + g x) x) (c₂ * (fun x => f x + g x) x)
<VAR>f✝ f g : ℝ → ℝ<VAR>hf : GrowsPolynomially f<VAR>hfg : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ c * ‖f x‖<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hb_ub : b < 1<GOAL>∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => f x + g x) u ∈ Set.Icc (c₁ * (fun x => f x + g x) x) (c₂ * (fun x => f x + g x) x)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>f : ι → α → E<VAR>g : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>l : Filter ι<VAR>hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>Tendsto (fun i => μ {x | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>f : ι → α → E<VAR>g : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>l : Filter ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hfg : Tendsto (fun b => ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f b - g) p μ ^ p.toReal) l (𝓝 (ENNReal.ofReal (1 / ε ^ p.toReal) * 0 ^ p.toReal))<GOAL>Tendsto (fun i => μ {x | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>f : ι → α → E<VAR>g : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>l : Filter ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hfg : Tendsto (fun b => ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f b - g) p μ ^ p.toReal) l (𝓝 0)<GOAL>Tendsto (fun i => μ {x | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>f : ι → α → E<VAR>g : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>l : Filter ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1<GOAL>∀ ε_1 > 0, ∀ᶠ (x : ι) in l, μ {x_1 | ε ≤ dist (f x x_1) (g x_1)} ≤ ε_1
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>f : ι → α → E<VAR>g : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>l : Filter ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1<VAR>δ : ℝ≥0∞<VAR>hδ : δ > 0<GOAL>∀ᶠ (x : ι) in l, μ {x_1 | ε ≤ dist (f x x_1) (g x_1)} ≤ δ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>f : ι → α → E<VAR>g : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>l : Filter ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1<VAR>δ : ℝ≥0∞<VAR>hδ : δ > 0<VAR>n : ι<VAR>hn : ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ<GOAL>μ {x | ε ≤ dist (f n x) (g x)} ≤ δ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>f : ι → α → E<VAR>g : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>l : Filter ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1<VAR>δ : ℝ≥0∞<VAR>hδ : δ > 0<VAR>n : ι<VAR>hn : ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ<GOAL>μ {x | ε ≤ dist (f n x) (g x)} ≤ ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f n - g) p μ ^ p.toReal
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>f : ι → α → E<VAR>g : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>l : Filter ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1<VAR>δ : ℝ≥0∞<VAR>hδ : δ > 0<VAR>n : ι<VAR>hn : ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ<GOAL>ENNReal.ofReal (ε ^ p.toReal) * μ {x | ε ≤ dist (f n x) (g x)} ≤ eLpNorm (f n - g) p μ ^ p.toReal
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>f : ι → α → E<VAR>g : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>l : Filter ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1<VAR>δ : ℝ≥0∞<VAR>hδ : δ > 0<VAR>n : ι<VAR>hn : ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ<GOAL>ENNReal.ofReal (ε ^ p.toReal) ≠ 0 ∨ eLpNorm (f n - g) p μ ^ p.toReal ≠ 0
<VAR>θ : ℝ<GOAL>|(-↑θ).toReal| = θ ↔ 0 ≤ θ ∧ θ ≤ π
<VAR>θ : ℝ<VAR>h : 0 ≤ θ ∧ θ ≤ π<GOAL>|(-↑θ).toReal| = θ
<VAR>θ : ℝ<VAR>h : 0 ≤ θ ∧ θ ≤ π<VAR>hnegpi : ¬θ = π<GOAL>|(-↑θ).toReal| = θ
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>S : Set (Set α)<VAR>hS : S.Finite<GOAL>TotallyBounded (⋃₀ S) ↔ ∀ s ∈ S, TotallyBounded s
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c✝ d✝ : ℝ<VAR>f : ℝ → E<VAR>c d : ℝ<GOAL>c • ∫ (x : ℝ) in a..b, f (c * x + d) = ∫ (x : ℝ) in c * a + d..c * b + d, f x
<VAR>N : ℕ<VAR>k n : ℤ<VAR>f : SlashInvariantForm (Gamma N) k<VAR>z : ℍ<GOAL>f (↑(↑N * n) +ᵥ z) = f z
<VAR>N : ℕ<VAR>k n : ℤ<VAR>f : SlashInvariantForm (Gamma N) k<VAR>z : ℍ<GOAL>f (ModularGroup.T ^ (↑N * n) • z) = f z
<VAR>N : ℕ<VAR>k n : ℤ<VAR>f : SlashInvariantForm (Gamma N) k<VAR>z : ℍ<VAR>Hn : ModularGroup.T ^ (↑N * n) ∈ Gamma (↑N).natAbs<GOAL>f (ModularGroup.T ^ (↑N * n) • z) = f z
<VAR>N : ℕ<VAR>k n : ℤ<VAR>f : SlashInvariantForm (Gamma N) k<VAR>z : ℍ<VAR>Hn : ModularGroup.T ^ (↑N * n) ∈ Gamma N<GOAL>f (ModularGroup.T ^ (↑N * n) • z) = f z
<VAR>N : ℕ<VAR>k n : ℤ<VAR>f : SlashInvariantForm (Gamma N) k<VAR>z : ℍ<VAR>Hn : ModularGroup.T ^ (↑N * n) ∈ Gamma N<GOAL>f z = (↑(↑↑↑⟨ModularGroup.T ^ (↑N * n), Hn⟩ 1 0) * ↑z + ↑(↑↑↑⟨ModularGroup.T ^ (↑N * n), Hn⟩ 1 1)) ^ k * f z
<VAR>N : ℕ<VAR>k n : ℤ<VAR>f : SlashInvariantForm (Gamma N) k<VAR>z : ℍ<VAR>Hn : ModularGroup.T ^ (↑N * n) ∈ Gamma N<GOAL>f z = (↑(↑{ val := ↑↑⟨ModularGroup.T ^ (↑N * n), Hn⟩, inv := ↑(↑⟨ModularGroup.T ^ (↑N * n), Hn⟩)⁻¹, val_inv := ⋯, inv_val := ⋯ } 1 0) * ↑z + ↑(↑{ val := ↑↑⟨ModularGroup.T ^ (↑N * n), Hn⟩, inv := ↑(↑⟨ModularGroup.T ^ (↑N * n), Hn⟩)⁻¹, val_inv := ⋯, inv_val := ⋯ } 1 1)) ^ k * f z
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z✝ z : K<GOAL>|re z / ‖z‖| ≤ 1
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z✝ z : K<GOAL>|re z| / ‖z‖ ≤ 1
<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>⟪r • x, (o.rotation ↑(π / 2)) x⟫_ℝ = 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>S : WSeq (WSeq α)<GOAL>map f S.join = (map (map f) S).join
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>S : WSeq (WSeq α)<GOAL>Seq.IsBisimulation fun s1 s2 => ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>S : WSeq (WSeq α)<GOAL>∃ s S_1, map f S.join = s.append (map f S_1.join) ∧ (map (map f) S).join = s.append (map (map f) S_1).join
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>hc : c ≠ 0<VAR>hd : d ≠ 0<GOAL>(a * d - b * c) / (c * d) < 0 ↔ a / c < b / d
<VAR>u v : ℤ<GOAL>u * v = -1 ↔ u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type ?u.81671<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : Free R M<VAR>inst✝ : Finite R M<GOAL>(LinearMap.ker LinearMap.id).FG
<VAR>α : Type u<VAR>inst✝² : Semiring α<VAR>a b : α<VAR>inst✝¹ : Invertible a<VAR>inst✝ : Invertible b<GOAL>⅟a + ⅟b = ⅟a * (a + b) * ⅟b
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : Monoid M<VAR>a : Mˣ<VAR>ha : ↑a ∈ center M<GOAL>↑a⁻¹ ∈ center M
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : Monoid M<VAR>a : Mˣ<VAR>ha : ∀ (g : M), g * ↑a = ↑a * g<GOAL>∀ (g : M), g * ↑a⁻¹ = ↑a⁻¹ * g
<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>p : A[X]<VAR>hm : p.Monic<VAR>hp : (Polynomial.aeval x) p = 0<VAR>hl : ∀ (q : A[X]), q.degree < p.degree → q = 0 ∨ (Polynomial.aeval x) q ≠ 0<VAR>a✝ : Nontrivial A<VAR>hx : IsIntegral A x<GOAL>p = minpoly A x
<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>p : A[X]<VAR>hm : p.Monic<VAR>hp : (Polynomial.aeval x) p = 0<VAR>hl : ∀ (q : A[X]), q.degree < p.degree → q = 0 ∨ (Polynomial.aeval x) q ≠ 0<VAR>a✝ : Nontrivial A<VAR>hx : IsIntegral A x<VAR>h : minpoly A x %ₘ p = 0<GOAL>p = minpoly A x
<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>p : A[X]<VAR>hm : p.Monic<VAR>hp : (Polynomial.aeval x) p = 0<VAR>hl : ∀ (q : A[X]), q.degree < p.degree → q = 0 ∨ (Polynomial.aeval x) q ≠ 0<VAR>a✝ : Nontrivial A<VAR>hx : IsIntegral A x<VAR>h : (Polynomial.aeval x) (minpoly A x %ₘ p) ≠ 0<GOAL>p = minpoly A x
<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>p : A[X]<VAR>hm : p.Monic<VAR>hp : (Polynomial.aeval x) p = 0<VAR>hl : ∀ (q : A[X]), q.degree < p.degree → q = 0 ∨ (Polynomial.aeval x) q ≠ 0<VAR>a✝ : Nontrivial A<VAR>hx : IsIntegral A x<VAR>h : minpoly A x %ₘ p = 0<VAR>r : A[X]<VAR>hr : minpoly A x = p * r<GOAL>p = minpoly A x
<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>p : A[X]<VAR>hm : p.Monic<VAR>hp : (Polynomial.aeval x) p = 0<VAR>hl : ∀ (q : A[X]), q.degree < p.degree → q = 0 ∨ (Polynomial.aeval x) q ≠ 0<VAR>a✝ : Nontrivial A<VAR>hx : IsIntegral A x<VAR>h : minpoly A x %ₘ p = 0<VAR>r : A[X]<VAR>hr : minpoly A x = p * r<VAR>hlead : (minpoly A x).leadingCoeff = (p * r).leadingCoeff<GOAL>p = p * r
<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>p : A[X]<VAR>hm : p.Monic<VAR>hp : (Polynomial.aeval x) p = 0<VAR>hl : ∀ (q : A[X]), q.degree < p.degree → q = 0 ∨ (Polynomial.aeval x) q ≠ 0<VAR>a✝ : Nontrivial A<VAR>hx : IsIntegral A x<VAR>h : minpoly A x %ₘ p = 0<VAR>r : A[X]<VAR>hr : minpoly A x = p * r<VAR>hlead : 1 = r.leadingCoeff<GOAL>p = p * r
<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>p : A[X]<VAR>hm : p.Monic<VAR>hp : (Polynomial.aeval x) p = 0<VAR>hl : ∀ (q : A[X]), q.degree < p.degree → q = 0 ∨ (Polynomial.aeval x) q ≠ 0<VAR>a✝ : Nontrivial A<VAR>hx : IsIntegral A x<VAR>h : minpoly A x %ₘ p = 0<VAR>r : A[X]<VAR>hr : minpoly A x = p * r<VAR>hlead : 1 = r.leadingCoeff<VAR>this : r.natDegree ≤ 0<GOAL>p = p * r
<VAR>ι✝ : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : Fintype ι✝<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>inst✝³ : FiniteDimensional ℝ F<VAR>inst✝² : MeasurableSpace F<VAR>inst✝¹ : BorelSpace F<VAR>ι : Type u_4<VAR>inst✝ : Fintype ι<GOAL>MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι)) volume volume
<VAR>ι✝ : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : Fintype ι✝<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>inst✝³ : FiniteDimensional ℝ F<VAR>inst✝² : MeasurableSpace F<VAR>inst✝¹ : BorelSpace F<VAR>ι : Type u_4<VAR>inst✝ : Fintype ι<GOAL>volume = map (⇑(EuclideanSpace.measurableEquiv ι).symm) volume
<VAR>ι✝ : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : Fintype ι✝<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>inst✝³ : FiniteDimensional ℝ F<VAR>inst✝² : MeasurableSpace F<VAR>inst✝¹ : BorelSpace F<VAR>ι : Type u_4<VAR>inst✝ : Fintype ι<GOAL>volume = ((Pi.basisFun ℝ ι).map (PiLp.continuousLinearEquiv 2 ℝ fun a => ℝ).symm.toLinearEquiv).addHaar
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Group α<VAR>g : GroupTopology α<VAR>this✝ : TopologicalSpace α := g.toTopologicalSpace<VAR>this : TopologicalGroup α<GOAL>Continuous Inv.inv
<VAR>B : Type u_1<VAR>inst✝⁴ : TopologicalSpace B<VAR>F₁ : Type u_2<VAR>inst✝³ : TopologicalSpace F₁<VAR>E₁ : B → Type u_3<VAR>inst✝² : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_4<VAR>inst✝¹ : TopologicalSpace F₂<VAR>E₂ : B → Type u_5<VAR>inst✝ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>e₁ : Trivialization F₁ TotalSpace.proj<VAR>e₂ : Trivialization F₂ TotalSpace.proj<VAR>f₁ : (TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ := fun p => ({ proj := p.proj, snd := p.snd.1 }, { proj := p.proj, snd := p.snd.2 })<VAR>f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p => (↑e₁ p.1, ↑e₂ p.2)<VAR>f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p => (p.1.1, p.1.2, p.2.2)<GOAL>ContinuousOn (toFun' e₁ e₂) (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))