ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>A : Matrix α β ℤ<VAR>v✝ : β → ℤ<VAR>hn : m < n<VAR>hm : 0 < m<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>v : β → ℤ<VAR>hv : 0 ≤ v ∧ v ≤ B'<VAR>mulVec_def : A *ᵥ v = fun i => ∑ j : β, A i j * v j<VAR>i : α<GOAL>(fun i => ∑ j : β, A i j * v j) i ≤ P i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>A : Matrix α β ℤ<VAR>v✝ : β → ℤ<VAR>hn : m < n<VAR>hm : 0 < m<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>v : β → ℤ<VAR>hv : 0 ≤ v ∧ v ≤ B'<VAR>mulVec_def : A *ᵥ v = fun i => ∑ j : β, A i j * v j<VAR>i : α<VAR>j : β<VAR>a✝ : j ∈ univ<VAR>hsign : 0 ≤ A i j<GOAL>-(↑B * (A i j)⁻) ≤ v j * A i j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>A : Matrix α β ℤ<VAR>v✝ : β → ℤ<VAR>hn : m < n<VAR>hm : 0 < m<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>v : β → ℤ<VAR>hv : 0 ≤ v ∧ v ≤ B'<VAR>mulVec_def : A *ᵥ v = fun i => ∑ j : β, A i j * v j<VAR>i : α<VAR>j : β<VAR>a✝ : j ∈ univ<VAR>hsign : A i j ≤ 0<GOAL>-(↑B * (A i j)⁻) ≤ v j * A i j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>A : Matrix α β ℤ<VAR>v✝ : β → ℤ<VAR>hn : m < n<VAR>hm : 0 < m<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>v : β → ℤ<VAR>hv : 0 ≤ v ∧ v ≤ B'<VAR>mulVec_def : A *ᵥ v = fun i => ∑ j : β, A i j * v j<VAR>i : α<VAR>j : β<VAR>a✝ : j ∈ univ<VAR>hsign : 0 ≤ A i j<GOAL>v j * A i j ≤ ↑B * (A i j)⁺
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>A : Matrix α β ℤ<VAR>v✝ : β → ℤ<VAR>hn : m < n<VAR>hm : 0 < m<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>v : β → ℤ<VAR>hv : 0 ≤ v ∧ v ≤ B'<VAR>mulVec_def : A *ᵥ v = fun i => ∑ j : β, A i j * v j<VAR>i : α<VAR>j : β<VAR>a✝ : j ∈ univ<VAR>hsign : A i j ≤ 0<GOAL>v j * A i j ≤ ↑B * (A i j)⁺
<VAR>p : ℝ[X]<GOAL>Tendsto (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) (𝓝 0) (𝓝 0)
<VAR>p : ℝ[X]<GOAL>Tendsto (fun x => if x ≤ 0 then 0 else Polynomial.eval x⁻¹ p * rexp (-x⁻¹)) (𝓝 0) (𝓝 0)
<VAR>p : ℝ[X]<GOAL>Tendsto (fun x => Polynomial.eval x⁻¹ p * rexp (-x⁻¹)) (𝓝 0 ⊓ 𝓟 {x | ¬x ≤ 0}) (𝓝 0)
<VAR>p : ℝ[X]<GOAL>Tendsto (fun x => Polynomial.eval x⁻¹ p * rexp (-x⁻¹)) (𝓝 0 ⊓ 𝓟 {x | 0 < x}) (𝓝 0)
<VAR>p : ℝ[X]<VAR>this : Tendsto (fun x => Polynomial.eval x⁻¹ p / rexp x⁻¹) (𝓝[>] 0) (𝓝 0)<GOAL>Tendsto (fun x => Polynomial.eval x⁻¹ p * rexp (-x⁻¹)) (𝓝 0 ⊓ 𝓟 {x | 0 < x}) (𝓝 0)
<VAR>p : ℝ[X]<VAR>this : Tendsto (fun x => Polynomial.eval x⁻¹ p / rexp x⁻¹) (𝓝[>] 0) (𝓝 0)<VAR>x : ℝ<VAR>hx : x ∈ {x | 0 < x}<GOAL>x ∈ {x | (fun x => Polynomial.eval x⁻¹ p / rexp x⁻¹ = (fun x => Polynomial.eval x⁻¹ p * rexp (-x⁻¹)) x) x}
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x : 𝕜<GOAL>iteratedDeriv (n + 1) f = iteratedDeriv n (deriv f)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x : 𝕜<GOAL>deriv^[n + 1] f = deriv^[n] (deriv f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>inst✝² : One M<VAR>inst✝¹ : One N<VAR>inst✝ : One P<VAR>f : α → M'<VAR>g : α → N<VAR>hf : Injective f<VAR>x : α<VAR>hx : x ∈ mulSupport g<GOAL>f x ∈ mulSupport (extend f g 1)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : MulOneClass M<VAR>inst✝² : MulOneClass N<VAR>inst✝¹ : MulOneClass P<VAR>S : Submonoid M<VAR>A : Type u_4<VAR>inst✝ : SetLike A M<VAR>hA : SubmonoidClass A M<VAR>S' : A<VAR>a : M<VAR>ha : a ∈ S<GOAL>⟨a, ha⟩ = 1 ↔ a = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x : α<VAR>l : List α<VAR>h : l.Nodup<VAR>hl : 1 < l.length<GOAL>l.formPerm (l.get ⟨0, ⋯⟩) = l.get ⟨1, hl⟩
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : NormedAddCommGroup β✝<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>β : Type u_5<VAR>inst✝ : NormedLatticeAddCommGroup β<VAR>f : α → β<VAR>hf : Integrable f μ<GOAL>Integrable (fun a => |f a|) μ
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : NormedAddCommGroup β✝<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>β : Type u_5<VAR>inst✝ : NormedLatticeAddCommGroup β<VAR>f : α → β<VAR>hf : Memℒp f 1 μ<GOAL>Memℒp (fun a => |f a|) 1 μ
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set P<GOAL>affineSpan k s = ⊥ ↔ s = ∅
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Preorder β<VAR>f g : α → β<VAR>a : α<VAR>l : Filter α<VAR>h : IsMinFilter f l a ∨ IsMaxFilter f l a<VAR>heq : f =ᶠ[l] g<VAR>hfga : f a = g a<GOAL>IsMinFilter g l a ∨ IsMaxFilter g l a
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type v'<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Module S N<VAR>inst✝³ : IsScalarTower R S N<VAR>p : Submonoid R<VAR>inst✝² : IsLocalization p S<VAR>f : M →ₗ[R] N<VAR>inst✝¹ : IsLocalizedModule p f<VAR>hp : p ≤ R⁰<VAR>inst✝ : IsDomain R<VAR>M' : Submodule R M<GOAL>Module.rank R (M ⧸ M') + Module.rank R ↥M' = Module.rank R M
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type v'<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Module S N<VAR>inst✝³ : IsScalarTower R S N<VAR>p : Submonoid R<VAR>inst✝² : IsLocalization p S<VAR>f : M →ₗ[R] N<VAR>inst✝¹ : IsLocalizedModule p f<VAR>hp : p ≤ R⁰<VAR>inst✝ : IsDomain R<VAR>M' : Submodule R M<GOAL>lift.{max u v, v} (Module.rank R (M ⧸ M') + Module.rank R ↥M') = lift.{max u v, v} (Module.rank R M)
<VAR>f : StieltjesFunction<VAR>a b : ℝ<GOAL>f.outer (Ioc a b) = ofReal (↑f b - ↑f a)
<VAR>f : StieltjesFunction<VAR>a b : ℝ<VAR>s : ℕ → Set ℝ<VAR>hs : Ioc a b ⊆ ⋃ i, s i<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>h : ∑' (i : ℕ), f.length (s i) < ⊤<GOAL>ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), f.length (s i) + ↑ε
<VAR>f : StieltjesFunction<VAR>a b : ℝ<VAR>s : ℕ → Set ℝ<VAR>hs : Ioc a b ⊆ ⋃ i, s i<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>h : ∑' (i : ℕ), f.length (s i) < ⊤<VAR>δ : ℝ≥0 := ε / 2<GOAL>ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), f.length (s i) + ↑ε
<VAR>f : StieltjesFunction<VAR>a b : ℝ<VAR>s : ℕ → Set ℝ<VAR>hs : Ioc a b ⊆ ⋃ i, s i<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>h : ∑' (i : ℕ), f.length (s i) < ⊤<VAR>δ : ℝ≥0 := ε / 2<VAR>δpos : 0 < ↑δ<GOAL>ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), f.length (s i) + ↑ε
<VAR>f : StieltjesFunction<VAR>a b : ℝ<VAR>s : ℕ → Set ℝ<VAR>hs : Ioc a b ⊆ ⋃ i, s i<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>h : ∑' (i : ℕ), f.length (s i) < ⊤<VAR>δ : ℝ≥0 := ε / 2<VAR>δpos : 0 < ↑δ<VAR>ε' : ℕ → ℝ≥0<VAR>ε'0 : ∀ (i : ℕ), 0 < ε' i<VAR>hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ<GOAL>ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), f.length (s i) + ↑ε
<VAR>f : StieltjesFunction<VAR>a b : ℝ<VAR>s : ℕ → Set ℝ<VAR>hs : Ioc a b ⊆ ⋃ i, s i<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>h : ∑' (i : ℕ), f.length (s i) < ⊤<VAR>δ : ℝ≥0 := ε / 2<VAR>δpos : 0 < ↑δ<VAR>ε' : ℕ → ℝ≥0<VAR>ε'0 : ∀ (i : ℕ), 0 < ε' i<VAR>hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ<VAR>a' : ℝ<VAR>ha' : ↑f a' - ↑f a < ↑δ<VAR>aa' : a < a'<GOAL>ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), f.length (s i) + ↑ε
<VAR>f : StieltjesFunction<VAR>a b : ℝ<VAR>s : ℕ → Set ℝ<VAR>hs : Ioc a b ⊆ ⋃ i, s i<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>h : ∑' (i : ℕ), f.length (s i) < ⊤<VAR>δ : ℝ≥0 := ε / 2<VAR>δpos : 0 < ↑δ<VAR>ε' : ℕ → ℝ≥0<VAR>ε'0 : ∀ (i : ℕ), 0 < ε' i<VAR>hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ<VAR>a' : ℝ<VAR>ha' : ↑f a' - ↑f a < ↑δ<VAR>aa' : a < a'<VAR>this : ∀ (i : ℕ), ∃ p, s i ⊆ Ioo p.1 p.2 ∧ ofReal (↑f p.2 - ↑f p.1) < f.length (s i) + ↑(ε' i)<GOAL>ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), f.length (s i) + ↑ε
<VAR>f : StieltjesFunction<VAR>a b : ℝ<VAR>s : ℕ → Set ℝ<VAR>hs : Ioc a b ⊆ ⋃ i, s i<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>h : ∑' (i : ℕ), f.length (s i) < ⊤<VAR>δ : ℝ≥0 := ε / 2<VAR>δpos : 0 < ↑δ<VAR>ε' : ℕ → ℝ≥0<VAR>ε'0 : ∀ (i : ℕ), 0 < ε' i<VAR>hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ<VAR>a' : ℝ<VAR>ha' : ↑f a' - ↑f a < ↑δ<VAR>aa' : a < a'<VAR>g : ℕ → ℝ × ℝ<VAR>hg : ∀ (i : ℕ), s i ⊆ Ioo (g i).1 (g i).2 ∧ ofReal (↑f (g i).2 - ↑f (g i).1) < f.length (s i) + ↑(ε' i)<GOAL>ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), f.length (s i) + ↑ε
<VAR>f : StieltjesFunction<VAR>a b : ℝ<VAR>s : ℕ → Set ℝ<VAR>hs : Ioc a b ⊆ ⋃ i, s i<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>h : ∑' (i : ℕ), f.length (s i) < ⊤<VAR>δ : ℝ≥0 := ε / 2<VAR>δpos : 0 < ↑δ<VAR>ε' : ℕ → ℝ≥0<VAR>ε'0 : ∀ (i : ℕ), 0 < ε' i<VAR>hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ<VAR>a' : ℝ<VAR>ha' : ↑f a' - ↑f a < ↑δ<VAR>aa' : a < a'<VAR>g : ℕ → ℝ × ℝ<VAR>hg : ∀ (i : ℕ), s i ⊆ Ioo (g i).1 (g i).2 ∧ ofReal (↑f (g i).2 - ↑f (g i).1) < f.length (s i) + ↑(ε' i)<VAR>I_subset : Icc a' b ⊆ ⋃ i, Ioo (g i).1 (g i).2<GOAL>ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), f.length (s i) + ↑ε
<VAR>R : Type u<VAR>inst✝¹¹ : Ring R<VAR>P : Type v<VAR>inst✝¹⁰ : AddCommGroup P<VAR>inst✝⁹ : Module R P<VAR>R₀ : Type ?u.49012<VAR>M : Type u_1<VAR>N : Type ?u.52304<VAR>inst✝⁸ : CommRing R₀<VAR>inst✝⁷ : Algebra R₀ R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R₀ M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : IsScalarTower R₀ R M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R₀ N<VAR>inst✝ : Projective R M<VAR>i : P →ₗ[R] M<VAR>s : M →ₗ[R] P<VAR>H : s ∘ₗ i = LinearMap.id<GOAL>Projective R P
<VAR>R : Type u<VAR>inst✝¹¹ : Ring R<VAR>P : Type v<VAR>inst✝¹⁰ : AddCommGroup P<VAR>inst✝⁹ : Module R P<VAR>R₀ : Type ?u.49012<VAR>M : Type u_1<VAR>N : Type ?u.52304<VAR>inst✝⁸ : CommRing R₀<VAR>inst✝⁷ : Algebra R₀ R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R₀ M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : IsScalarTower R₀ R M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R₀ N<VAR>inst✝ : Projective R M<VAR>i : P →ₗ[R] M<VAR>s : M →ₗ[R] P<VAR>H : s ∘ₗ i = LinearMap.id<VAR>g : M →ₗ[R] P →₀ R<VAR>hg : Finsupp.total P P R id ∘ₗ g = s<GOAL>Projective R P
<VAR>R : Type u<VAR>inst✝¹¹ : Ring R<VAR>P : Type v<VAR>inst✝¹⁰ : AddCommGroup P<VAR>inst✝⁹ : Module R P<VAR>R₀ : Type ?u.49012<VAR>M : Type u_1<VAR>N : Type ?u.52304<VAR>inst✝⁸ : CommRing R₀<VAR>inst✝⁷ : Algebra R₀ R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R₀ M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : IsScalarTower R₀ R M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R₀ N<VAR>inst✝ : Projective R M<VAR>i : P →ₗ[R] M<VAR>s : M →ₗ[R] P<VAR>H : s ∘ₗ i = LinearMap.id<VAR>g : M →ₗ[R] P →₀ R<VAR>hg : Finsupp.total P P R id ∘ₗ g = s<VAR>x : P<GOAL>(Finsupp.total P P R id) ((g ∘ₗ i) x) = x
<VAR>a b : Cardinal.{u}<VAR>n m : ℕ<GOAL>IsUnit a ↔ a = 1
<VAR>a b : Cardinal.{u}<VAR>n m : ℕ<VAR>h : IsUnit a<GOAL>a = 1
<VAR>b : Cardinal.{u}<VAR>n m : ℕ<VAR>h : IsUnit 0<GOAL>0 = 1
<VAR>a b : Cardinal.{u}<VAR>n m : ℕ<VAR>h : IsUnit a<VAR>ha : a ≠ 0<GOAL>a = 1
<VAR>a b : Cardinal.{u}<VAR>n m : ℕ<VAR>h : ∀ (y : Cardinal.{u}), a ∣ y<VAR>ha : a ≠ 0<GOAL>a = 1
<VAR>a b : Cardinal.{u}<VAR>n m : ℕ<VAR>h : ∀ (y : Cardinal.{u}), a ∣ y<VAR>ha : a ≠ 0<VAR>t : Cardinal.{u}<VAR>ht : 1 = a * t<GOAL>a = 1
<VAR>a b : Cardinal.{u}<VAR>n m : ℕ<VAR>h : ∀ (y : Cardinal.{u}), a ∣ y<VAR>ha : a ≠ 0<VAR>t : Cardinal.{u}<VAR>ht : a = 1 ∧ t = 1<GOAL>a = 1
<VAR>a b : Cardinal.{u}<VAR>n m : ℕ<VAR>h : ∀ (y : Cardinal.{u}), a ∣ y<VAR>ha : a ≠ 0<VAR>t : Cardinal.{u}<VAR>ht : a * t = 1<GOAL>1 ≤ a
<VAR>a b : Cardinal.{u}<VAR>n m : ℕ<VAR>h : ∀ (y : Cardinal.{u}), a ∣ y<VAR>ha : a ≠ 0<VAR>t : Cardinal.{u}<VAR>ht : a * t = 1<GOAL>1 ≤ t
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>N✝ : Subgroup G<VAR>nN✝ : N✝.Normal<VAR>H : Type v<VAR>inst✝¹ : Group H<VAR>M : Type x<VAR>inst✝ : Monoid M<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>x y : G<GOAL>↑x = ↑y ↔ x / y ∈ N
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>N✝ : Subgroup G<VAR>nN✝ : N✝.Normal<VAR>H : Type v<VAR>inst✝¹ : Group H<VAR>M : Type x<VAR>inst✝ : Monoid M<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>x y : G<GOAL>y⁻¹ * x ∈ N ↔ x / y ∈ N
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>map valEmbedding (Ioc a b) = Ioc ↑a ↑b
<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 g : ι → α → β<VAR>hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n<VAR>hfm : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>hunif : UnifIntegrable f p μ<VAR>C : ℝ≥0<VAR>hC : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑C<GOAL>UniformIntegrable g p μ
<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 g : ι → α → β<VAR>hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n<VAR>hfm : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>hunif : UnifIntegrable f p μ<VAR>C : ℝ≥0<VAR>hC : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑C<VAR>i : ι<GOAL>eLpNorm (g i) p μ ≤ ↑C
<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 g : ι → α → β<VAR>hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n<VAR>hfm : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>hunif : UnifIntegrable f p μ<VAR>C : ℝ≥0<VAR>hC : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑C<VAR>i : ι<GOAL>eLpNorm (f i) p μ ≤ ↑C
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f f₁ f₂ : (i : ι) → Filter (α i)<VAR>s : (i : ι) → Set (α i)<VAR>p : (i : ι) → α i → Prop<VAR>β : Type u_3<VAR>m : β → (i : ι) → α i<VAR>l : Filter β<GOAL>Tendsto m l (pi f) ↔ ∀ (i : ι), Tendsto (fun x => m x i) l (f i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f f₁ f₂ : (i : ι) → Filter (α i)<VAR>s : (i : ι) → Set (α i)<VAR>p : (i : ι) → α i → Prop<VAR>β : Type u_3<VAR>m : β → (i : ι) → α i<VAR>l : Filter β<GOAL>(∀ (i : ι), Tendsto (eval i ∘ m) l (f i)) ↔ ∀ (i : ι), Tendsto (fun x => m x i) l (f i)
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<VAR>I : Ideal R<VAR>h : ∀ (J : Ideal R) (hJ : J.IsMaximal), IsLocalization.coeSubmodule (Localization.AtPrime J) I = ⊥<VAR>P : Ideal R<VAR>hP : P.IsMaximal<VAR>x : R<VAR>hx : x ∈ I<GOAL>x ∈ RingHom.ker (algebraMap R (Localization.AtPrime P))
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<VAR>I : Ideal R<VAR>h : ∀ (J : Ideal R) (hJ : J.IsMaximal), IsLocalization.coeSubmodule (Localization.AtPrime J) I = ⊥<VAR>P : Ideal R<VAR>hP : P.IsMaximal<VAR>x : R<VAR>hx : x ∈ I<GOAL>∃ y ∈ I, (algebraMap R (Localization.AtPrime P)) y = (algebraMap R (Localization.AtPrime P)) x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x : M<VAR>l : ι →₀ R<VAR>hl : (Finsupp.total ι M R ⇑b) l = 0<GOAL>b.repr ((Finsupp.total ι M R ⇑b) l) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝¹ : ℕ<VAR>inst✝ : CommSemiring R<VAR>p : R[X]<VAR>n✝ n : ℕ<VAR>ih : derivative (p ^ (n + 1)) = C (↑n + 1) * p ^ n * derivative p<GOAL>derivative (p ^ (n.succ + 1)) = C (↑n.succ + 1) * p ^ n.succ * derivative p
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝¹ : ℕ<VAR>inst✝ : CommSemiring R<VAR>p : R[X]<VAR>n✝ n : ℕ<VAR>ih : derivative (p ^ (n + 1)) = C (↑n + 1) * p ^ n * derivative p<GOAL>(C ↑n * p ^ n * p + p ^ n * p) * derivative p + p ^ n * p * derivative p = C (↑n.succ + 1) * p ^ n * p * derivative p
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>s : KernelFork f<GOAL>Fork.ι s ≫ f = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>x : L<GOAL>x ∈ (ad R L).ker ↔ x ∈ LieAlgebra.center R L
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>x : L<GOAL>(ad R L) x = 0 ↔ ∀ (m : L), ⁅x, m⁆ = 0
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<GOAL>W.Ψ 3 = C W.Ψ₃
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasShift C ℤ<VAR>T₁ T₂ T₃ : Triangle C<VAR>J : Type u_1<VAR>T : J → Triangle C<VAR>inst✝⁴ : HasProduct fun j => (T j).obj₁<VAR>inst✝³ : HasProduct fun j => (T j).obj₂<VAR>inst✝² : HasProduct fun j => (T j).obj₃<VAR>inst✝¹ : HasProduct fun j => (shiftFunctor C 1).obj (T j).obj₁<VAR>inst✝ : HasZeroMorphisms C<VAR>h : ∀ (j : J), (T j).mor₃ ≫ (shiftFunctor C 1).map (T j).mor₁ = 0<VAR>this : HasProduct fun j => (shiftFunctor C 1).obj (T j).obj₂<GOAL>((Pi.map fun j => (T j).mor₃) ≫ inv (piComparison (shiftFunctor C 1) fun j => (T j).obj₁)) ≫ (shiftFunctor C 1).map (Pi.lift fun j => Pi.π (fun j => (T j).obj₁) j ≫ (T j).mor₁) = 0
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasShift C ℤ<VAR>T₁ T₂ T₃ : Triangle C<VAR>J : Type u_1<VAR>T : J → Triangle C<VAR>inst✝⁴ : HasProduct fun j => (T j).obj₁<VAR>inst✝³ : HasProduct fun j => (T j).obj₂<VAR>inst✝² : HasProduct fun j => (T j).obj₃<VAR>inst✝¹ : HasProduct fun j => (shiftFunctor C 1).obj (T j).obj₁<VAR>inst✝ : HasZeroMorphisms C<VAR>h : ∀ (j : J), (T j).mor₃ ≫ (shiftFunctor C 1).map (T j).mor₁ = 0<VAR>this : HasProduct fun j => (shiftFunctor C 1).obj (T j).obj₂<GOAL>((Pi.map fun j => (T j).mor₃) ≫ inv (piComparison (shiftFunctor C 1) fun j => (T j).obj₁) ≫ (shiftFunctor C 1).map (Pi.lift fun j => Pi.π (fun j => (T j).obj₁) j ≫ (T j).mor₁) ≫ piComparison (shiftFunctor C 1) fun j => (T j).obj₂) = 0
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : HasShift C ℤ<VAR>T₁ T₂ T₃ : Triangle C<VAR>J : Type u_1<VAR>T : J → Triangle C<VAR>inst✝⁴ : HasProduct fun j => (T j).obj₁<VAR>inst✝³ : HasProduct fun j => (T j).obj₂<VAR>inst✝² : HasProduct fun j => (T j).obj₃<VAR>inst✝¹ : HasProduct fun j => (shiftFunctor C 1).obj (T j).obj₁<VAR>inst✝ : HasZeroMorphisms C<VAR>h : ∀ (j : J), (T j).mor₃ ≫ (shiftFunctor C 1).map (T j).mor₁ = 0<VAR>this : HasProduct fun j => (shiftFunctor C 1).obj (T j).obj₂<VAR>j : J<GOAL>((Pi.map fun j => (T j).mor₃) ≫ inv (piComparison (shiftFunctor C 1) fun j => (T j).obj₁) ≫ (shiftFunctor C 1).map (Pi.lift fun j => Pi.π (fun j => (T j).obj₁) j ≫ (T j).mor₁) ≫ piComparison (shiftFunctor C 1) fun j => (T j).obj₂) ≫ Pi.π (fun b => (shiftFunctor C 1).obj (T b).obj₂) j = 0 ≫ Pi.π (fun b => (shiftFunctor C 1).obj (T b).obj₂) j
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁵ : LinearOrderedSemiring α<VAR>inst✝⁴ : LinearOrderedSemiring β<VAR>inst✝³ : FloorSemiring α<VAR>inst✝² : FloorSemiring β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : RingHomClass F α β<VAR>a✝ : α<VAR>b : β<VAR>f : F<VAR>hf : StrictMono ⇑f<VAR>a : α<VAR>n : ℕ<GOAL>↑n ≤ f a ↔ ↑n ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>E : Type u_3<VAR>inst✝¹ : Norm E<VAR>F : Type u_4<VAR>inst✝ : Norm F<VAR>e : α ≃ₜ β<VAR>b : β<VAR>f : β → E<VAR>g : β → F<GOAL>f =O[𝓝 b] g ↔ (f ∘ ⇑e) =O[𝓝 (e.symm b)] (g ∘ ⇑e)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>E : Type u_3<VAR>inst✝¹ : Norm E<VAR>F : Type u_4<VAR>inst✝ : Norm F<VAR>e : α ≃ₜ β<VAR>b : β<VAR>f : β → E<VAR>g : β → F<GOAL>(∃ c, IsBigOWith c (𝓝 b) f g) ↔ ∃ c, IsBigOWith c (𝓝 (e.symm b)) (f ∘ ⇑e) (g ∘ ⇑e)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>op : α → α → α<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>b₁ b₂ : α<VAR>s₁ s₂ : Multiset α<GOAL>fold op (op b₁ b₂) (s₁ + 0) = op (fold op b₁ s₁) (fold op b₂ 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>op : α → α → α<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>b₁ b₂ : α<VAR>s₁ s₂ : Multiset α<VAR>a : α<VAR>b : Multiset α<VAR>h : fold op (op b₁ b₂) (s₁ + b) = op (fold op b₁ s₁) (fold op b₂ b)<GOAL>fold op (op b₁ b₂) (s₁ + a ::ₘ b) = op (fold op b₁ s₁) (fold op b₂ (a ::ₘ b))
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<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>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp F p (μ.trim hm))<GOAL>Memℒp.toLp ↑↑f ⋯ ∈ lpMeasSubgroup F m p μ
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<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>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp F p (μ.trim hm))<VAR>hf_mem_ℒp : Memℒp (↑↑f) p μ := memℒp_of_memℒp_trim hm (Lp.memℒp f)<GOAL>Memℒp.toLp ↑↑f ⋯ ∈ lpMeasSubgroup F m p μ
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<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>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp F p (μ.trim hm))<VAR>hf_mem_ℒp : Memℒp (↑↑f) p μ := memℒp_of_memℒp_trim hm (Lp.memℒp f)<GOAL>AEStronglyMeasurable' m (↑↑(Memℒp.toLp ↑↑f ⋯)) μ
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<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>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp F p (μ.trim hm))<VAR>hf_mem_ℒp : Memℒp (↑↑f) p μ := memℒp_of_memℒp_trim hm (Lp.memℒp f)<GOAL>AEStronglyMeasurable' m (↑↑f) μ
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<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>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp F p (μ.trim hm))<VAR>hf_mem_ℒp : Memℒp (↑↑f) p μ := memℒp_of_memℒp_trim hm (Lp.memℒp f)<GOAL>AEStronglyMeasurable' m (↑↑f) (μ.trim hm)