ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u_1<VAR>inst✝ : OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>u : ℕ → ℕ<VAR>C : ℕ<VAR>hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>h_nonneg : ∀ (n : ℕ), 0 ≤ f n<VAR>hu : Monotone u<VAR>h_succ_diff : SuccDiffBounded C u<VAR>n : ℕ<GOAL>(u (0 + 1) - u 0) • f (u 0) + ∑ k ∈ range n, (u (k + 1 + 1) - u (k + 1)) • f (u (k + 1)) ≤ (u 1 - u 0) • f (u 0) + C • ∑ k ∈ Ico (u 0 + 1) (u n + 1), f k
<VAR>M : Type u_1<VAR>inst✝ : OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>u : ℕ → ℕ<VAR>C : ℕ<VAR>hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>h_nonneg : ∀ (n : ℕ), 0 ≤ f n<VAR>hu : Monotone u<VAR>h_succ_diff : SuccDiffBounded C u<VAR>n : ℕ<GOAL>∑ k ∈ range n, (u (k + 1 + 1) - u (k + 1)) • f (u (k + 1)) ≤ C • ∑ k ∈ Ico (u 0 + 1) (u n + 1), f k
<VAR>M : Type u_1<VAR>inst✝ : OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>u : ℕ → ℕ<VAR>C : ℕ<VAR>hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>h_nonneg : ∀ (n : ℕ), 0 ≤ f n<VAR>hu : Monotone u<VAR>h_succ_diff : SuccDiffBounded C u<VAR>n : ℕ<GOAL>∑ k ∈ range n, (u (k + 2) - u (k + 1)) • f (u (k + 1)) ≤ C • ∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1))
<VAR>M : Type u_1<VAR>inst✝ : OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>u : ℕ → ℕ<VAR>C : ℕ<VAR>hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>h_nonneg : ∀ (n : ℕ), 0 ≤ f n<VAR>hu : Monotone u<VAR>h_succ_diff : SuccDiffBounded C u<VAR>n : ℕ<VAR>this : ∀ k ∈ range n, (u (k + 2) - u (k + 1)) • f (u (k + 1)) ≤ C • (u (k + 1) - u k) • f (u (k + 1))<GOAL>∑ k ∈ range n, (u (k + 2) - u (k + 1)) • f (u (k + 1)) ≤ C • ∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1))
<VAR>M : Type u_1<VAR>inst✝ : OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>u : ℕ → ℕ<VAR>C : ℕ<VAR>hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>h_nonneg : ∀ (n : ℕ), 0 ≤ f n<VAR>hu : Monotone u<VAR>h_succ_diff : SuccDiffBounded C u<VAR>n : ℕ<VAR>this : ∀ k ∈ range n, (u (k + 2) - u (k + 1)) • f (u (k + 1)) ≤ C • (u (k + 1) - u k) • f (u (k + 1))<GOAL>C • ∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1)) = ∑ i ∈ range n, C • (u (i + 1) - u i) • f (u (i + 1))
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h : Irreducible (cyclotomic (↑n) K)<GOAL>(fromZetaAut hμ h) (zeta n K L) = μ
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h : Irreducible (cyclotomic (↑n) K)<GOAL>((IsPrimitiveRoot.powerBasis K ⋯).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) ⋯) (zeta n K L) = μ
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ✝ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h✝ : Irreducible (cyclotomic (↑n) K)<VAR>hζ : IsPrimitiveRoot (zeta n K L) ↑n<VAR>h : ∃ i < ↑n, zeta n K L ^ i = μ<VAR>pf✝¹ : h.choose.Coprime ↑n<VAR>hμ : IsPrimitiveRoot (zeta n K L ^ (↑(ZMod.unitOfCoprime h.choose pf✝¹)).val) ↑n<VAR>pf✝ : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K hμ).gen<GOAL>((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K hμ) pf✝) (zeta n K L) = μ
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ✝ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h✝ : Irreducible (cyclotomic (↑n) K)<VAR>hζ : IsPrimitiveRoot (zeta n K L) ↑n<VAR>h : ∃ i < ↑n, zeta n K L ^ i = μ<VAR>pf✝¹ : h.choose.Coprime ↑n<VAR>hμ : IsPrimitiveRoot (zeta n K L ^ (↑(ZMod.unitOfCoprime h.choose pf✝¹)).val) ↑n<VAR>pf✝ : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K hμ).gen<GOAL>((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K hμ) pf✝) (IsPrimitiveRoot.powerBasis K hζ).gen = μ
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ✝ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h✝ : Irreducible (cyclotomic (↑n) K)<VAR>hζ : IsPrimitiveRoot (zeta n K L) ↑n<VAR>h : ∃ i < ↑n, zeta n K L ^ i = μ<VAR>pf✝¹ : h.choose.Coprime ↑n<VAR>hμ : IsPrimitiveRoot (zeta n K L ^ (↑(ZMod.unitOfCoprime h.choose pf✝¹)).val) ↑n<VAR>pf✝ : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K hμ).gen<GOAL>zeta n K L ^ (↑(ZMod.unitOfCoprime h.choose pf✝¹)).val = μ
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ✝ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h✝ : Irreducible (cyclotomic (↑n) K)<VAR>hζ : IsPrimitiveRoot (zeta n K L) ↑n<VAR>h : ∃ i < ↑n, zeta n K L ^ i = μ<VAR>pf✝¹ : h.choose.Coprime ↑n<VAR>hμ : IsPrimitiveRoot (zeta n K L ^ (↑(ZMod.unitOfCoprime h.choose pf✝¹)).val) ↑n<VAR>pf✝ : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K hμ).gen<GOAL>(↑(ZMod.unitOfCoprime h.choose pf✝¹)).val = h.choose
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : TopologicalSpace 𝕜<VAR>inst✝¹ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>inst✝ : Archimedean 𝕜<VAR>x : AddCircle p<VAR>hx : x ≠ ↑a<GOAL>ContinuousAt (⇑(equivIco p a)) x
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : TopologicalSpace 𝕜<VAR>inst✝¹ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>inst✝ : Archimedean 𝕜<VAR>x : AddCircle p<VAR>z✝ : 𝕜<VAR>hx : ↑z✝ ≠ ↑a<GOAL>ContinuousAt ⇑(equivIco p a) ↑z✝
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : TopologicalSpace 𝕜<VAR>inst✝¹ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>inst✝ : Archimedean 𝕜<VAR>x : AddCircle p<VAR>z✝ : 𝕜<VAR>hx : ↑z✝ ≠ ↑a<GOAL>Filter.map (⇑(equivIco p a) ∘ QuotientAddGroup.mk) (𝓝 z✝) ≤ 𝓝 ((equivIco p a) ↑z✝)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t u : Set α<VAR>inst✝ : MeasurableSpace α<VAR>s : ℕ → Set α<VAR>hs : ∀ (n : ℕ), MeasurableSet (s n)<GOAL>MeasurableSet (limsup s atTop)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : _root_.RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>G : ι → Type u_5<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>i j : ι<VAR>hij : i ≠ j<VAR>a : (fun _i => 𝕜) i<VAR>b : (fun _i => 𝕜) j<GOAL>⟪((fun i => LinearIsometry.toSpanSingleton 𝕜 E ⋯) i) a, ((fun i => LinearIsometry.toSpanSingleton 𝕜 E ⋯) j) b⟫_𝕜 = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CanonicallyOrderedAddCommMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<GOAL>↑(((decompose 𝒜) 0) 0) = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CanonicallyOrderedAddCommMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<GOAL>↑(0 0) = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CanonicallyOrderedAddCommMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>x✝¹ x✝ : A<GOAL>↑(((decompose 𝒜) (x✝¹ + x✝)) 0) = ↑(((decompose 𝒜) x✝¹) 0) + ↑(((decompose 𝒜) x✝) 0)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CanonicallyOrderedAddCommMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>x✝¹ x✝ : A<GOAL>↑(((decompose 𝒜) x✝¹ + (decompose 𝒜) x✝) 0) = ↑(((decompose 𝒜) x✝¹) 0) + ↑(((decompose 𝒜) x✝) 0)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CanonicallyOrderedAddCommMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<GOAL>∀ (x y : A), { toFun := fun a => ↑(((decompose 𝒜) a) 0), map_one' := ⋯ }.toFun (x * y) = { toFun := fun a => ↑(((decompose 𝒜) a) 0), map_one' := ⋯ }.toFun x * { toFun := fun a => ↑(((decompose 𝒜) a) 0), map_one' := ⋯ }.toFun y
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CanonicallyOrderedAddCommMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>x : A<GOAL>{ toFun := fun a => ↑(((decompose 𝒜) a) 0), map_one' := ⋯ }.toFun (0 * x) = { toFun := fun a => ↑(((decompose 𝒜) a) 0), map_one' := ⋯ }.toFun 0 * { toFun := fun a => ↑(((decompose 𝒜) a) 0), map_one' := ⋯ }.toFun x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CanonicallyOrderedAddCommMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<GOAL>∀ {i : ι} (m : ↥(𝒜 i)) (y : A), { toFun := fun a => ↑(((decompose 𝒜) a) 0), map_one' := ⋯ }.toFun (↑m * y) = { toFun := fun a => ↑(((decompose 𝒜) a) 0), map_one' := ⋯ }.toFun ↑m * { toFun := fun a => ↑(((decompose 𝒜) a) 0), map_one' := ⋯ }.toFun y
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CanonicallyOrderedAddCommMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<GOAL>∀ (m m' : A), (∀ (y : A), { toFun := fun a => ↑(((decompose 𝒜) a) 0), map_one' := ⋯ }.toFun (m * y) = { toFun := fun a => ↑(((decompose 𝒜) a) 0), map_one' := ⋯ }.toFun m * { toFun := fun a => ↑(((decompose 𝒜) a) 0), map_one' := ⋯ }.toFun y) → (∀ (y : A), { toFun := fun a => ↑(((decompose 𝒜) a) 0), map_one' := ⋯ }.toFun (m' * y) = { toFun := fun a => ↑(((decompose 𝒜) a) 0), map_one' := ⋯ }.toFun m' * { toFun := fun a => ↑(((decompose 𝒜) a) 0), map_one' := ⋯ }.toFun y) → ∀ (y : A), { toFun := fun a => ↑(((decompose 𝒜) a) 0), map_one' := ⋯ }.toFun ((m + m') * y) = { toFun := fun a => ↑(((decompose 𝒜) a) 0), map_one' := ⋯ }.toFun (m + m') * { toFun := fun a => ↑(((decompose 𝒜) a) 0), map_one' := ⋯ }.toFun y
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hf : HasStrictFDerivAt f f' x<VAR>K : ℝ≥0<VAR>hK : ‖f'‖₊ < K<GOAL>∃ s ∈ 𝓝 x, LipschitzOnWith K f s
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hf : HasStrictFDerivAt f f' x<VAR>K : ℝ≥0<VAR>hK : ‖f'‖₊ < K<VAR>this : IsBigOWith ((fun a => ↑a) K) (𝓝 (x, x)) (fun x => f x.1 - f x.2 - f' (x.1 - x.2) + f' (x.1 - x.2)) fun p => p.1 - p.2<GOAL>∃ s ∈ 𝓝 x, LipschitzOnWith K f s
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hf : HasStrictFDerivAt f f' x<VAR>K : ℝ≥0<VAR>hK : ‖f'‖₊ < K<VAR>this : ∀ᶠ (x : E × E) in 𝓝 (x, x), ‖f x.1 - f x.2‖ ≤ ↑K * ‖x.1 - x.2‖<GOAL>∃ s ∈ 𝓝 x, LipschitzOnWith K f s
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hf : HasStrictFDerivAt f f' x<VAR>K : ℝ≥0<VAR>hK : ‖f'‖₊ < K<VAR>this : ∀ᶠ (x : E × E) in 𝓝 (x, x), ‖f x.1 - f x.2‖ ≤ ↑K * ‖x.1 - x.2‖<VAR>U : Set E<VAR>Uo : IsOpen U<VAR>xU : x ∈ U<VAR>hU : U ×ˢ U ⊆ {x | (fun x => ‖f x.1 - f x.2‖ ≤ ↑K * ‖x.1 - x.2‖) x}<GOAL>∃ s ∈ 𝓝 x, LipschitzOnWith K f s
<VAR>R : Type u_1<VAR>inst✝⁷ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : Finite m<VAR>inst✝⁴ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>i j : n<GOAL>(toMatrix v₁ v₁) id i j = 1 i j
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>s : Set α<GOAL>IsComplete s ↔ ∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ 𝓟 s → ∃ x ∈ s, ↑l ≤ 𝓝 x
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>s : Set α<VAR>H : ∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ 𝓟 s → ∃ x ∈ s, ↑l ≤ 𝓝 x<VAR>l : Filter α<VAR>hl : Cauchy l<VAR>hls : l ≤ 𝓟 s<GOAL>∃ x ∈ s, ClusterPt x l
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>s : Set α<VAR>H : ∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ 𝓟 s → ∃ x ∈ s, ↑l ≤ 𝓝 x<VAR>l : Filter α<VAR>hl : Cauchy l<VAR>hls : l ≤ 𝓟 s<VAR>this : l.NeBot<GOAL>∃ x ∈ s, ClusterPt x l
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>s : Set α<VAR>H : ∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ 𝓟 s → ∃ x ∈ s, ↑l ≤ 𝓝 x<VAR>l : Filter α<VAR>hl : Cauchy l<VAR>hls : l ≤ 𝓟 s<VAR>this : l.NeBot<VAR>x : α<VAR>hxs : x ∈ s<VAR>hxl : ↑(Ultrafilter.of l) ≤ 𝓝 x<GOAL>∃ x ∈ s, ClusterPt x l
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝ : NormedLatticeAddCommGroup E<VAR>f g : ↥(Lp E p μ)<GOAL>↑↑f ≤ᶠ[ae μ] ↑↑g ↔ f ≤ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹¹ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹⁰ : TopologicalSpace β<VAR>inst✝⁹ : TopologicalSpace γ<VAR>f g : α → β<VAR>M : Type u_5<VAR>G : Type u_6<VAR>G₀ : Type u_7<VAR>inst✝⁸ : Monoid M<VAR>inst✝⁷ : MulAction M β<VAR>inst✝⁶ : ContinuousConstSMul M β<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MulAction G β<VAR>inst✝³ : ContinuousConstSMul G β<VAR>inst✝² : GroupWithZero G₀<VAR>inst✝¹ : MulAction G₀ β<VAR>inst✝ : ContinuousConstSMul G₀ β<VAR>c : G<VAR>h : AEStronglyMeasurable (fun x => c • f x) μ<GOAL>AEStronglyMeasurable f μ
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝³ : Fintype ι<VAR>m✝¹ : (i : ι) → OuterMeasure (α i)<VAR>m✝ : (i : ι) → MeasurableSpace (α i)<VAR>μ✝ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>inst✝¹ : Fintype ι'<VAR>π : ι → Type u_4<VAR>inst✝ : Unique ι<VAR>m : (i : ι) → MeasurableSpace (π i)<VAR>μ : (i : ι) → Measure (π i)<VAR>e : ((i : ι) → π i) ≃ᵐ π default := MeasurableEquiv.piUnique π<GOAL>Measure.map (⇑e) (Measure.pi μ) = μ default
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝³ : Fintype ι<VAR>m✝¹ : (i : ι) → OuterMeasure (α i)<VAR>m✝ : (i : ι) → MeasurableSpace (α i)<VAR>μ✝ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>inst✝¹ : Fintype ι'<VAR>π : ι → Type u_4<VAR>inst✝ : Unique ι<VAR>m : (i : ι) → MeasurableSpace (π i)<VAR>μ : (i : ι) → Measure (π i)<VAR>e : ((i : ι) → π i) ≃ᵐ π default := MeasurableEquiv.piUnique π<VAR>this : (piPremeasure fun i => (μ i).toOuterMeasure) = ⇑(Measure.map (⇑e.symm) (μ default))<GOAL>Measure.map (⇑e) (Measure.pi μ) = μ default
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m✝ : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>i : σ<VAR>f : MvPolynomial σ R<VAR>m : σ →₀ ℕ<VAR>h_m : m ∈ f.support<GOAL>m i ≤ degreeOf i f
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m✝ : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>i : σ<VAR>f : MvPolynomial σ R<VAR>m : σ →₀ ℕ<VAR>h_m : m ∈ f.support<GOAL>m i ≤ f.support.sup fun m => m i
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝¹ : DecidableRel r<VAR>inst✝ : DecidableEq α<VAR>L : List α<VAR>a b : α<GOAL>count a (orderedInsert r b L) = count a L + if a = b then 1 else 0
<VAR>α : Sort u_1<VAR>a : α<VAR>motive : (a' : α) → a = a' → Sort u_2<VAR>x : motive a ⋯<VAR>β : Sort u_2<VAR>y : β<GOAL>HEq (⋯ ▸ x) y ↔ HEq x y
<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>f : α → ℝ<VAR>hf : Integrable f μ<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<GOAL>μ {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>f : α → ℝ<VAR>hf : Integrable f μ<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<GOAL>{a | ε ≤ f a} ⊆ {x | ε ≤ ‖f x‖}
<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>f : α → ℝ<VAR>hf : Integrable f μ<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>x : α<VAR>hx : x ∈ {a | ε ≤ f a}<GOAL>x ∈ {x | ε ≤ ‖f x‖}
<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>f : α → ℝ<VAR>hf : Integrable f μ<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>x : α<VAR>hx : ε ≤ f x<GOAL>ε ≤ |f x|
<VAR>t : Type u → Type u<VAR>inst✝⁵ : Traversable t<VAR>inst✝⁴ : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : LawfulApplicative F<VAR>inst✝¹ : Applicative G<VAR>inst✝ : LawfulApplicative G<VAR>α β γ : Type u<VAR>g : α → F β<VAR>h : β → G γ<VAR>f✝ : β → γ<VAR>x : t β<VAR>f : β → γ<VAR>x✝ : t β<GOAL>traverse (pure ∘ f) x✝ = (pure ∘ map f) x✝
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z✝ : ℤ<VAR>a✝ a : α<VAR>z : ℤ<GOAL>⌊a - ↑z⌋ = ⌊a + ↑(-z)⌋
<VAR>α : Sort u_1<VAR>inst✝ : DecidableEq α<VAR>i j x : α<GOAL>(swap i j) x = update (update id j i) i j x
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>f : G ⧸ H → G<VAR>hf : ∀ (q : G ⧸ H), ↑(f q) = q<VAR>q : G ⧸ H<GOAL>↑((toEquiv ⋯) q) = f q
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>f : G ⧸ H → G<VAR>hf : ∀ (q : G ⧸ H), ↑(f q) = q<VAR>q : G ⧸ H<GOAL>(toEquiv ⋯) q = ⟨f q, ⋯⟩
<VAR>s : Set ℝ<VAR>t : Set ℝ≥0<VAR>h : s.OrdConnected<GOAL>(toNNReal '' s).OrdConnected
<VAR>s : Set ℝ<VAR>t : Set ℝ≥0<VAR>h : s.OrdConnected<VAR>x : ℝ<VAR>hx : x ∈ s<VAR>y : ℝ<VAR>hy : y ∈ s<VAR>z : ℝ≥0<VAR>hz : z ∈ Icc x.toNNReal y.toNNReal<GOAL>z ∈ toNNReal '' s
<VAR>s : Set ℝ<VAR>t : Set ℝ≥0<VAR>h : s.OrdConnected<VAR>x : ℝ<VAR>hx : x ∈ s<VAR>y : ℝ<VAR>hy : y ∈ s<VAR>z : ℝ≥0<VAR>hz : z ∈ Icc x.toNNReal y.toNNReal<VAR>hy₀ : y ≤ 0<GOAL>z ∈ toNNReal '' s
<VAR>s : Set ℝ<VAR>t : Set ℝ≥0<VAR>h : s.OrdConnected<VAR>x : ℝ<VAR>hx : x ∈ s<VAR>y : ℝ<VAR>hy : y ∈ s<VAR>z : ℝ≥0<VAR>hz : z ∈ Icc x.toNNReal y.toNNReal<VAR>hy₀ : 0 ≤ y<GOAL>z ∈ toNNReal '' s
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>inst✝ : DecidableRel R<VAR>neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z<VAR>a : α<VAR>l : List α<GOAL>(∀ (b : α), b ∈ pwFilter R l → R a b) ↔ ∀ (b : α), b ∈ l → R a b
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>inst✝ : DecidableRel R<VAR>neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z<VAR>a : α<VAR>l : List α<GOAL>(∀ (b : α), b ∈ pwFilter R l → R a b) → ∀ (b : α), b ∈ l → R a b
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R J : Set α<GOAL>(freeOn E).Basis I X ↔ I = X ∧ X ⊆ E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R J : Set α<GOAL>I = X ∧ X ⊆ E → (freeOn E).Basis I X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I R J : Set α<VAR>hIE : I ⊆ E<GOAL>(freeOn E).Basis I I
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>hμ : μ ≠ 0<VAR>h_int_X : Integrable (fun ω => rexp (t * X ω)) μ<GOAL>0 < ∫ (x : Ω), rexp (t * X x) ∂μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>hμ : μ ≠ 0<VAR>h_int_X : Integrable (fun ω => rexp (t * X ω)) μ<VAR>this : ∫ (x : Ω), rexp (t * X x) ∂μ = ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ<GOAL>0 < ∫ (x : Ω), rexp (t * X x) ∂μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>hμ : μ ≠ 0<VAR>h_int_X : Integrable (fun ω => rexp (t * X ω)) μ<VAR>this : ∫ (x : Ω), rexp (t * X x) ∂μ = ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ<GOAL>0 < μ ((Function.support fun x => rexp (t * X x)) ∩ Set.univ)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>hμ : μ ≠ 0<VAR>h_int_X : Integrable (fun ω => rexp (t * X ω)) μ<VAR>this : ∫ (x : Ω), rexp (t * X x) ∂μ = ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ<GOAL>0 ≤ᶠ[ae (μ.restrict Set.univ)] fun x => rexp (t * X x)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>hμ : μ ≠ 0<VAR>h_int_X : Integrable (fun ω => rexp (t * X ω)) μ<VAR>this : ∫ (x : Ω), rexp (t * X x) ∂μ = ∫ (x : Ω) in Set.univ, rexp (t * X x) ∂μ<GOAL>IntegrableOn (fun x => rexp (t * X x)) Set.univ μ
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : LE G<VAR>inst✝² : Preorder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>a b : G<VAR>c d : P<VAR>h₁ : a ≤ b<VAR>h₂ : c < d<GOAL>a • c < b • d
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : LE G<VAR>inst✝² : Preorder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>a b : G<VAR>c d : P<VAR>h₁ : a ≤ b<VAR>h₂ : c < d<GOAL>b • c < b • d
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : LE G<VAR>inst✝² : Preorder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>a b : G<VAR>c d : P<VAR>h₁ : a ≤ b<VAR>h₂ : c < d<GOAL>¬b • d ≤ b • c
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : LE G<VAR>inst✝² : Preorder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>a b : G<VAR>c d : P<VAR>h₁ : a ≤ b<VAR>h₂ : c < d<VAR>hbdc : b • d ≤ b • c<GOAL>False
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : LE G<VAR>inst✝² : Preorder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>a b : G<VAR>c d : P<VAR>h₁ : a ≤ b<VAR>h₂ : c < d<VAR>hbdc : b • d ≤ b • c<VAR>h : d ≤ c<GOAL>False