ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<GOAL>(η.withDensity (κ.rnDeriv η)) a = 0 ↔ ((η.withDensity (κ.rnDeriv η)) a) (κ.mutuallySingularSetSlice η a)ᶜ = 0
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<GOAL>((η.withDensity (κ.rnDeriv η)) a) univ = 0 ↔ ((η.withDensity (κ.rnDeriv η)) a) (κ.mutuallySingularSetSlice η a)ᶜ = 0
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>this : univ = κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ<GOAL>((η.withDensity (κ.rnDeriv η)) a) univ = 0 ↔ ((η.withDensity (κ.rnDeriv η)) a) (κ.mutuallySingularSetSlice η a)ᶜ = 0
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>x y : K<VAR>h : num A y * ↑(den A x) = num A x * ↑(den A y)<GOAL>x = y
<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_4}<VAR>x✝ : ∃ a, o = succ a<VAR>a : Ordinal.{u_4}<VAR>e : o = succ a<GOAL>succ o.pred = o
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x : L<GOAL>x ∈ rootSpace H 0 ↔ ∀ (y : ↥H), ∃ k, ((toEnd R (↥H) L) y ^ k) x = 0
<VAR>p q : ℚ≥0<VAR>n₁ n₂ d₁ d₂ d✝ a : ℕ<VAR>ha : a ≠ 0<VAR>n d : ℕ<GOAL>Rat.divInt (↑n * ↑a) (↑d * ↑a) = Rat.divInt ↑n ↑d
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>k : ℕ<VAR>f : L →ₗ⁅R⁆ L'<VAR>h : Function.Surjective ⇑f<GOAL>map f (lowerCentralSeries R L L k) = lowerCentralSeries R L' L' k
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>k : ℕ<VAR>f : L →ₗ⁅R⁆ L'<VAR>h : Function.Surjective ⇑f<VAR>h' : map f ⊤ = ⊤<GOAL>map f (lowerCentralSeries R L L k) = lowerCentralSeries R L' L' k
<VAR>S : Type u_1<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : IsDomain S<VAR>inst✝⁴ : Nontrivial S<VAR>inst✝³ : IsDedekindDomain S<VAR>inst✝² : Module.Free ℤ S<VAR>inst✝¹ : Module.Finite ℤ S<VAR>inst✝ : CharZero S<VAR>n : ℕ<VAR>hn : 0 < n<VAR>f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I<GOAL>{I | absNorm I = n}.Finite
<VAR>S : Type u_1<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : IsDomain S<VAR>inst✝⁴ : Nontrivial S<VAR>inst✝³ : IsDedekindDomain S<VAR>inst✝² : Module.Free ℤ S<VAR>inst✝¹ : Module.Finite ℤ S<VAR>inst✝ : CharZero S<VAR>n : ℕ<VAR>hn : 0 < n<VAR>f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I<GOAL>(f '' {I | absNorm I = n}).Finite
<VAR>S : Type u_1<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : IsDomain S<VAR>inst✝⁴ : Nontrivial S<VAR>inst✝³ : IsDedekindDomain S<VAR>inst✝² : Module.Free ℤ S<VAR>inst✝¹ : Module.Finite ℤ S<VAR>inst✝ : CharZero S<VAR>n : ℕ<VAR>hn : 0 < n<VAR>f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I<GOAL>Set.InjOn f {I | absNorm I = n}
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CharP R p<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>(frobenius x).coeff n = x.coeff n ^ p
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CharP R p<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>(aeval x.coeff) (frobeniusPoly p n) = x.coeff n ^ p
<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✝⁸ : Fintype 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>M₃ : Type u_7<VAR>inst✝² : AddCommMonoid M₃<VAR>inst✝¹ : Module R M₃<VAR>v₃ : Basis l R M₃<VAR>inst✝ : DecidableEq m<VAR>M : Matrix m n R<VAR>M' : Matrix n m R<VAR>hMM' : M * M' = 1<VAR>hM'M : M' * M = 1<VAR>x : M₁<GOAL>((toLin v₂ v₁) M') ({ toFun := ⇑((toLin v₁ v₂) M), map_add' := ⋯, map_smul' := ⋯ }.toFun x) = x
<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✝⁸ : Fintype 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>M₃ : Type u_7<VAR>inst✝² : AddCommMonoid M₃<VAR>inst✝¹ : Module R M₃<VAR>v₃ : Basis l R M₃<VAR>inst✝ : DecidableEq m<VAR>M : Matrix m n R<VAR>M' : Matrix n m R<VAR>hMM' : M * M' = 1<VAR>hM'M : M' * M = 1<VAR>x : M₂<GOAL>((toLin v₁ v₂) M) (((toLin v₂ v₁) M') x) = x
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>inst✝ : IsIrrefl α r<VAR>a✝ a : α<VAR>h : ∀ (y : α), r y a → Acc r y<VAR>ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}<VAR>s : Multiset α<GOAL>CutExpand r s {a} → Acc (CutExpand r) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : CompleteSpace E<GOAL>Kᗮᗮ = K.topologicalClosure
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : CompleteSpace E<GOAL>Kᗮᗮ ≤ K.topologicalClosure
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : CompleteSpace E<GOAL>K.topologicalClosure ≤ Kᗮᗮ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hsum : ∑' (x : α), f x ≠ ⊤<GOAL>HasSum (fun x => (f x).toReal) (∑' (x : α), (f x).toReal)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f : α → ℝ≥0<VAR>hsum : ∑' (x : α), (fun i => ↑(f i)) x ≠ ⊤<GOAL>HasSum (fun x => ((fun i => ↑(f i)) x).toReal) (∑' (x : α), ((fun i => ↑(f i)) x).toReal)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f : α → ℝ≥0<VAR>hsum : ∑' (x : α), (fun i => ↑(f i)) x ≠ ⊤<GOAL>HasSum f (∑' (a : α), f a)
<VAR>α : Type u_1<VAR>b : PosNum<GOAL>↑(1 + b) = ↑1 + ↑b
<VAR>α : Type u_1<VAR>a : PosNum<GOAL>↑(a + 1) = ↑a + ↑1
<VAR>α : Type u_1<VAR>a b : PosNum<GOAL>↑a + ↑b + (↑a + ↑b) + 1 = ↑a + ↑a + (↑b + ↑b + 1)
<VAR>α : Type u_1<VAR>a b : PosNum<GOAL>↑a + ↑b + (↑a + ↑b) + 1 = ↑a + ↑a + 1 + (↑b + ↑b)
<VAR>α : Type u_1<VAR>a b : PosNum<GOAL>↑(a + b).succ + ↑(a + b).succ = ↑a + ↑a + 1 + (↑b + ↑b + 1)
<VAR>α : Type u_1<VAR>a b : PosNum<GOAL>↑a + ↑b + 1 + (↑a + ↑b + 1) = ↑a + ↑a + 1 + (↑b + ↑b + 1)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>hv : LinearIndependent R v<VAR>u : ι ⊕ ι' → ↑S.X₂<VAR>hw✝ : LinearIndependent R (⇑S.g ∘ u ∘ Sum.inr)<VAR>hm : Mono S.f<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<VAR>w : ι' → ↑S.X₃<VAR>hw : LinearIndependent R w<GOAL>LinearIndependent R (Sum.elim (⇑S.f ∘ v) (Function.invFun S.g.toFun ∘ w))
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>hv : LinearIndependent R v<VAR>u : ι ⊕ ι' → ↑S.X₂<VAR>hw✝ : LinearIndependent R (⇑S.g ∘ u ∘ Sum.inr)<VAR>hm : Mono S.f<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<VAR>w : ι' → ↑S.X₃<VAR>hw : LinearIndependent R w<GOAL>LinearIndependent R (⇑S.g ∘ Sum.elim (⇑S.f ∘ v) (Function.invFun S.g.toFun ∘ w) ∘ Sum.inr)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>hv : LinearIndependent R v<VAR>u : ι ⊕ ι' → ↑S.X₂<VAR>hw✝ : LinearIndependent R (⇑S.g ∘ u ∘ Sum.inr)<VAR>hm : Mono S.f<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<VAR>w : ι' → ↑S.X₃<VAR>hw : LinearIndependent R w<VAR>x✝ : ι'<GOAL>(⇑S.g ∘ Function.invFun ⇑S.g ∘ w) x✝ = w x✝
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ inst✝ : CommSemiring R<VAR>n : ℕ<VAR>φ ψ : MvPolynomial σ R<GOAL>(homogeneousComponent n) φ = ∑ d ∈ Finset.filter (fun d => d.degree = n) φ.support, (monomial d) (coeff d φ)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ inst✝ : CommSemiring R<VAR>n : ℕ<VAR>φ ψ : MvPolynomial σ R<GOAL>(homogeneousComponent n) φ = ∑ x ∈ Finset.filter (fun d => (weight 1) d = n) φ.support, (monomial x) (coeff x φ)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : ConditionallyCompleteLinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderTopology β<VAR>inst✝ : Nonempty γ<VAR>s : Set α<VAR>hs : IsPreconnected s<GOAL>s ∈ {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : ConditionallyCompleteLinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderTopology β<VAR>inst✝ : Nonempty γ<VAR>hs : IsPreconnected ∅<GOAL>∅ ∈ {Icc (sInf ∅) (sSup ∅), Ico (sInf ∅) (sSup ∅), Ioc (sInf ∅) (sSup ∅), Ioo (sInf ∅) (sSup ∅), Ici (sInf ∅), Ioi (sInf ∅), Iic (sSup ∅), Iio (sSup ∅), univ, ∅}
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : ConditionallyCompleteLinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderTopology β<VAR>inst✝ : Nonempty γ<VAR>s : Set α<VAR>hs : IsPreconnected s<VAR>hne : s.Nonempty<GOAL>s ∈ {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>t : R<VAR>h : ‖t‖ < 1<GOAL>inverse (1 - t) = ↑(Units.oneSub t h)⁻¹
<VAR>n : ℕ<VAR>x a₁ b₁ : ℝ<VAR>m : ℕ<VAR>e₁ : n + 1 = m<VAR>a₂ b₂ : ℝ<VAR>e : |1 + x / ↑m * a₂ - a₁| ≤ b₁ - |x| / ↑m * b₂<VAR>h : |rexp x - expNear m x a₂| ≤ |x| ^ m / ↑m.factorial * b₂<GOAL>|rexp x - expNear n x a₁| ≤ |x| ^ n / ↑n.factorial * b₁
<VAR>n : ℕ<VAR>x a₁ b₁ : ℝ<VAR>m : ℕ<VAR>e₁ : n + 1 = m<VAR>a₂ b₂ : ℝ<VAR>e : |1 + x / ↑m * a₂ - a₁| ≤ b₁ - |x| / ↑m * b₂<VAR>h : |rexp x - expNear m x a₂| ≤ |x| ^ m / ↑m.factorial * b₂<GOAL>|x| ^ m / ↑m.factorial * b₂ + |expNear m x a₂ - expNear n x a₁| ≤ |x| ^ n / ↑n.factorial * b₁
<VAR>n : ℕ<VAR>x a₁ b₁ a₂ b₂ : ℝ<VAR>e : |1 + x / ↑(n + 1) * a₂ - a₁| ≤ b₁ - |x| / ↑(n + 1) * b₂<VAR>h : |rexp x - expNear (n + 1) x a₂| ≤ |x| ^ (n + 1) / ↑(n + 1).factorial * b₂<GOAL>|x| ^ (n + 1) / ↑(n + 1).factorial * b₂ + |expNear (n + 1) x a₂ - expNear n x a₁| ≤ |x| ^ n / ↑n.factorial * b₁
<VAR>n : ℕ<VAR>x a₁ b₁ a₂ b₂ : ℝ<VAR>e : |1 + x / ↑(n + 1) * a₂ - a₁| ≤ b₁ - |x| / ↑(n + 1) * b₂<VAR>h : |rexp x - expNear (n + 1) x a₂| ≤ |x| ^ (n + 1) / ↑(n + 1).factorial * b₂<GOAL>|x| ^ (n + 1) / ↑(n + 1).factorial * b₂ + |x ^ n / ↑n.factorial| * |1 + x / (↑n + 1) * a₂ - a₁| ≤ |x| ^ n / ↑n.factorial * b₁
<VAR>n : ℕ<VAR>x a₁ b₁ a₂ b₂ : ℝ<VAR>e : |1 + x / ↑(n + 1) * a₂ - a₁| ≤ b₁ - |x| / ↑(n + 1) * b₂<VAR>h : |rexp x - expNear (n + 1) x a₂| ≤ |x| ^ (n + 1) / ↑(n + 1).factorial * b₂<GOAL>|x| ^ (n + 1) / ↑(n + 1).factorial * b₂ + |x ^ n / ↑n.factorial| * |1 + x / (↑n + 1) * a₂ - a₁| = |x| ^ n / ↑n.factorial * (|x| / ↑(n + 1) * b₂ + |1 + x / ↑(n + 1) * a₂ - a₁|)
<VAR>n : ℕ<VAR>x a₁ b₁ a₂ b₂ : ℝ<VAR>e : |1 + x / ↑(n + 1) * a₂ - a₁| ≤ b₁ - |x| / ↑(n + 1) * b₂<VAR>h : |rexp x - expNear (n + 1) x a₂| ≤ |x| ^ (n + 1) / ↑(n + 1).factorial * b₂<GOAL>0 ≤ |x| ^ n / ↑n.factorial
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>inst✝¹³ : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹² : (x : B) → TopologicalSpace (E x)<VAR>EB : Type u_7<VAR>inst✝¹¹ : NormedAddCommGroup EB<VAR>inst✝¹⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>E' : B → Type u_9<VAR>inst✝⁸ : (x : B) → Zero (E' x)<VAR>EM : Type u_10<VAR>inst✝⁷ : NormedAddCommGroup EM<VAR>inst✝⁶ : NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>inst✝⁵ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : ChartedSpace HB B<VAR>inst✝ : FiberBundle F E<VAR>x : TotalSpace F E<GOAL>extChartAt (IB.prod 𝓘(𝕜, F)) x = (trivializationAt F E x.proj).toPartialEquiv ≫ (extChartAt IB x.proj).prod (PartialEquiv.refl F)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>inst✝¹³ : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹² : (x : B) → TopologicalSpace (E x)<VAR>EB : Type u_7<VAR>inst✝¹¹ : NormedAddCommGroup EB<VAR>inst✝¹⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>E' : B → Type u_9<VAR>inst✝⁸ : (x : B) → Zero (E' x)<VAR>EM : Type u_10<VAR>inst✝⁷ : NormedAddCommGroup EM<VAR>inst✝⁶ : NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>inst✝⁵ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : ChartedSpace HB B<VAR>inst✝ : FiberBundle F E<VAR>x : TotalSpace F E<GOAL>((trivializationAt F E x.proj).toPartialHomeomorph ≫ₕ (chartAt HB x.proj).prod (PartialHomeomorph.refl F)).toPartialEquiv ≫ (IB.prod 𝓘(𝕜, F)).toPartialEquiv = (trivializationAt F E x.proj).toPartialEquiv ≫ ((chartAt HB x.proj).toPartialEquiv ≫ IB.toPartialEquiv).prod (PartialEquiv.refl F)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>inst✝¹³ : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹² : (x : B) → TopologicalSpace (E x)<VAR>EB : Type u_7<VAR>inst✝¹¹ : NormedAddCommGroup EB<VAR>inst✝¹⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>E' : B → Type u_9<VAR>inst✝⁸ : (x : B) → Zero (E' x)<VAR>EM : Type u_10<VAR>inst✝⁷ : NormedAddCommGroup EM<VAR>inst✝⁶ : NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>inst✝⁵ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : ChartedSpace HB B<VAR>inst✝ : FiberBundle F E<VAR>x : TotalSpace F E<GOAL>(trivializationAt F E x.proj).toPartialEquiv ≫ (chartAt HB x.proj).prod (PartialEquiv.refl F) ≫ IB.prod (PartialEquiv.refl F) = (trivializationAt F E x.proj).toPartialEquiv ≫ ((chartAt HB x.proj).toPartialEquiv ≫ IB.toPartialEquiv).prod (PartialEquiv.refl F)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l✝ m : Language α<VAR>a b x : List α<VAR>l : Language α<GOAL>1 + l∗ * l = l∗
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type w<VAR>inst✝¹ : Category.{z, w} D<VAR>inst✝ : Abelian D<VAR>F G : C ⥤ D<VAR>α : F ⟶ G<VAR>X : C<GOAL>(coimageImageComparison α).app X = (coimageObjIso α X).hom ≫ coimageImageComparison (α.app X) ≫ (imageObjIso α X).inv
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R[X]<VAR>s : Finset R<VAR>degree_fg_lt : (f - g).degree < ↑s.card<VAR>eval_fg : ∀ x ∈ s, eval x f = eval x g<GOAL>f = g
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R[X]<VAR>s : Finset R<VAR>degree_fg_lt : (f - g).degree < ↑s.card<VAR>eval_fg : ∀ x ∈ s, eval x f = eval x g<GOAL>f - g = 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R[X]<VAR>s : Finset R<VAR>degree_fg_lt : (f - g).degree < ↑s.card<VAR>eval_fg : ∀ x ∈ s, eval x f = eval x g<GOAL>∀ x ∈ s, eval x (f - g) = 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R[X]<VAR>s : Finset R<VAR>degree_fg_lt : (f - g).degree < ↑s.card<VAR>eval_fg : ∀ x ∈ s, eval x f = eval x g<GOAL>∀ x ∈ s, eval x f = eval x g
<VAR>n : ℕ<GOAL>(filter (fun p => Prime p) (range n)).card = count Prime n
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b c d : α<GOAL>(fun x => a - x) ⁻¹' [[b, c]] = [[a - b, a - c]]
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b c d : α<GOAL>Icc (a - max b c) (a - min b c) = Icc (min (a - b) (a - c)) (max (a - b) (a - c))
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>inst✝¹ : NormedAddCommGroup α<VAR>inst✝ : CompleteSpace α<VAR>f : ℕ → α<VAR>l : ℝ<VAR>hl₁ : l < 1<VAR>hf : ∀ᶠ (n : ℕ) in atTop, f n ≠ 0<VAR>h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)<GOAL>Summable f
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>inst✝¹ : NormedAddCommGroup α<VAR>inst✝ : CompleteSpace α<VAR>f : ℕ → α<VAR>l : ℝ<VAR>hl₁ : l < 1<VAR>hf : ∀ᶠ (n : ℕ) in atTop, f n ≠ 0<VAR>h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)<VAR>r : ℝ<VAR>hr₀ : l < r<VAR>hr₁ : r < 1<GOAL>Summable f
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>inst✝¹ : NormedAddCommGroup α<VAR>inst✝ : CompleteSpace α<VAR>f : ℕ → α<VAR>l : ℝ<VAR>hl₁ : l < 1<VAR>hf : ∀ᶠ (n : ℕ) in atTop, f n ≠ 0<VAR>h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)<VAR>r : ℝ<VAR>hr₀ : l < r<VAR>hr₁ : r < 1<GOAL>∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>inst✝¹ : NormedAddCommGroup α<VAR>inst✝ : CompleteSpace α<VAR>f : ℕ → α<VAR>l : ℝ<VAR>hl₁ : l < 1<VAR>hf : ∀ᶠ (n : ℕ) in atTop, f n ≠ 0<VAR>h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)<VAR>r : ℝ<VAR>hr₀ : l < r<VAR>hr₁ : r < 1<VAR>a✝¹ : ℕ<VAR>a✝ : ‖f (a✝¹ + 1)‖ / ‖f a✝¹‖ ≤ r<VAR>h₁ : f a✝¹ ≠ 0<GOAL>‖f (a✝¹ + 1)‖ ≤ r * ‖f a✝¹‖
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{?u.132102, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝ : L.IsLocalization W<VAR>X Y : C<VAR>z₁ z₂ : W.RightFraction X Y<VAR>Z : C<VAR>t₁ : Z ⟶ z₁.X'<VAR>t₂ : Z ⟶ z₂.X'<VAR>hs : t₁ ≫ z₁.s = t₂ ≫ z₂.s<VAR>hf : t₁ ≫ z₁.f = t₂ ≫ z₂.f<VAR>ht : W (t₁ ≫ z₁.s)<GOAL>LeftFractionRel z₁.op z₂.op
<VAR>Ω : Type u_1<VAR>inst✝ : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<GOAL>μ = μ.mass • μ.normalize.toFiniteMeasure
<VAR>Ω : Type u_1<VAR>inst✝ : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<GOAL>∀ (s : Set Ω), MeasurableSet s → μ s = (μ.mass • μ.normalize.toFiniteMeasure) s
<VAR>Ω : Type u_1<VAR>inst✝ : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>s : Set Ω<VAR>_s_mble : MeasurableSet s<GOAL>μ s = (μ.mass • μ.normalize.toFiniteMeasure) s
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>s : Set (Set α)<VAR>h_open : ∀ u ∈ s, IsOpen u<VAR>h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v ∈ s, a ∈ v ∧ v ⊆ u<VAR>a : α<GOAL>∀ (i : Set α), a ∈ i ∧ IsOpen i → ∃ i', (i' ∈ s ∧ a ∈ i') ∧ id i' ⊆ i
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁵ : Fintype l<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : Unique ι<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>r : ℝ≥0<VAR>A : Matrix m n α<GOAL>‖A‖₊ ≤ r ↔ ∀ (i : m) (j : n), ‖A i j‖₊ ≤ r
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a b c d : G₀<VAR>m n : ℕ<VAR>hc : c ≠ 0<VAR>h : b⁻¹ * a = c<GOAL>a = b * c
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a b c d : G₀<VAR>m n : ℕ<VAR>hc : c ≠ 0<VAR>h : b⁻¹ * a = c<GOAL>b ≠ 0
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a c d : G₀<VAR>m n : ℕ<VAR>hc : c ≠ 0<VAR>h : 0⁻¹ * a = c<GOAL>False
<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>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s : Set P<VAR>hs : s.Nonempty<GOAL>affineSpan k s = ⊤ ↔ vectorSpan k s = ⊤
<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>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s : Set P<VAR>hs : s.Nonempty<GOAL>vectorSpan k s = ⊤ → affineSpan k s = ⊤
<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>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s : Set P<VAR>hs : s.Nonempty<VAR>h : vectorSpan k s = ⊤<GOAL>affineSpan k s = ⊤
<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>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s : Set P<VAR>hs : s.Nonempty<VAR>h : vectorSpan k s = ⊤<GOAL>Nonempty ↥(affineSpan k s)
<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>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s : Set P<VAR>h : vectorSpan k s = ⊤<VAR>x : P<VAR>hx : x ∈ s<GOAL>Nonempty ↥(affineSpan k s)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{?u.260798, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasBinaryBiproducts C<VAR>X₁ X₂ X₃ : CochainComplex C ℤ<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<GOAL>f ≫ g = 𝟙 X₁ ≫ f ≫ g
<VAR>m n : Nat<GOAL>range m ⊆ range n ↔ m ≤ n
<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<GOAL>(Filter.coprodᵢ f).NeBot ↔ (∀ (i : ι), Nonempty (α i)) ∧ ∃ d, (f d).NeBot