ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝ : NormedAddCommGroup α<VAR>f : ℕ → α<VAR>g : ℕ → ℝ<VAR>h : f =o[atTop] g<VAR>hg : 0 ≤ g<VAR>h'g : Tendsto (fun n => ∑ i ∈ range n, g i) atTop atTop<VAR>A : ∀ (i : ℕ), ‖g i‖ = g i<VAR>B : ∀ (n : ℕ), ‖∑ i ∈ range n, g i‖ = ∑ i ∈ range n, g i<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>N : ℕ<VAR>hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b<VAR>this : (fun x => ∑ i ∈ range N, f i) =o[atTop] fun n => ∑ i ∈ range n, g i<VAR>n : ℕ<VAR>hn : ‖∑ i ∈ range N, f i‖ ≤ ε / 2 * ‖∑ i ∈ range n, g i‖<VAR>Nn : n ∈ Set.Ici N<GOAL>‖∑ i ∈ range n, f i‖ ≤ ε * ‖∑ i ∈ range n, g i‖
<VAR>α : Type u<VAR>i✝ : Nat<VAR>a b : Array α<VAR>i j : Nat<VAR>h : j ≤ a.size<GOAL>(a ++ b).extract i j = a.extract i j
<VAR>α : Type u<VAR>i✝ : Nat<VAR>a b : Array α<VAR>i j : Nat<VAR>h : j ≤ a.size<GOAL>((a ++ b).extract i j).size = (a.extract i j).size
<VAR>α : Type u<VAR>i✝ : Nat<VAR>a b : Array α<VAR>i j : Nat<VAR>h : j ≤ a.size<GOAL>∀ (i_1 : Nat) (hi₁ : i_1 < ((a ++ b).extract i j).size) (hi₂ : i_1 < (a.extract i j).size), ((a ++ b).extract i j)[i_1] = (a.extract i j)[i_1]
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>x : ↥(ideal R S)<GOAL>(D R S).tensorProductTo ↑x = (ideal R S).toCotangent x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>x : ↥(ideal R S)<GOAL>LinearMap.id ((ideal R S).toCotangent x) = (ideal R S).toCotangent x
<VAR>x : ℝ<VAR>n : ℤ<GOAL>sin (↑n * π - x) = -((-1) ^ n * sin x)
<VAR>a b c : Ordinal.{u_1}<VAR>h₁ : 0 < a<VAR>h₂ : b ≤ c<GOAL>a ^ b ≤ a ^ c
<VAR>a b c : Ordinal.{u_1}<VAR>h₁✝ : 0 < a<VAR>h₂ : b ≤ c<VAR>h₁ : 1 < a<GOAL>a ^ b ≤ a ^ c
<VAR>a b c : Ordinal.{u_1}<VAR>h₁✝ : 0 < a<VAR>h₂ : b ≤ c<VAR>h₁ : 1 = a<GOAL>a ^ b ≤ a ^ c
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>m n : ℕ<VAR>h : n % 2 = 1<GOAL>n % 2 + 2 * (n / 2) = 2 * (n / 2) + 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁵ : SemilatticeSup α<VAR>inst✝⁴ : OrderBot α<VAR>s✝¹ s₁ s₂ : Finset β<VAR>f✝ g✝ : β → α<VAR>a : α<VAR>inst✝³ : SemilatticeSup β<VAR>inst✝² : OrderBot β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : SupBotHomClass F α β<VAR>f : F<VAR>s✝ : Finset ι<VAR>g : ι → α<VAR>i : ι<VAR>s : Finset ι<VAR>x✝ : i ∉ s<VAR>h : f (s.sup g) = s.sup (⇑f ∘ g)<GOAL>f ((cons i s x✝).sup g) = (cons i s x✝).sup (⇑f ∘ g)
<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 : α → α → Prop<VAR>a b c d : α<GOAL>ReflTransGen (TransGen r) = ReflTransGen r
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : LinearOrderedSemifield α<VAR>l : Filter β<VAR>f : β → α<VAR>r c : α<VAR>n : ℕ<VAR>hr : 0 < r<GOAL>Tendsto (fun x => f x * r) l atTop ↔ Tendsto f l atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : PredOrder α<VAR>a b : α<VAR>ha : ¬IsMin a<VAR>hb : ¬IsMin b<GOAL>pred a < pred b ↔ a < b
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : AddZeroClass β<VAR>f g : Multiset α →+ β<VAR>h : ∀ (x : α), f {x} = g {x}<VAR>s : Multiset α<GOAL>f s = g s
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : AddZeroClass β<VAR>f g : Multiset α →+ β<VAR>h : ∀ (x : α), f {x} = g {x}<GOAL>f 0 = g 0
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : AddZeroClass β<VAR>f g : Multiset α →+ β<VAR>h : ∀ (x : α), f {x} = g {x}<VAR>a : α<VAR>s : Multiset α<VAR>ih : f s = g s<GOAL>f (a ::ₘ s) = g (a ::ₘ s)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>x : S<GOAL>eval₂ f x (C a) = f a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Seq α<GOAL>(↑s).tail = ↑s.tail
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Seq α<GOAL>Option.rec nil Prod.snd (Option.map (fun a => (a, ↑s.tail)) s.head) = ↑s.tail
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<GOAL>nil = some <$> Seq.nil
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Group M<VAR>inst✝ : MulAction M α<VAR>s : Set α<VAR>a : α<VAR>a_in_s : a ∈ s<VAR>b : α<VAR>b_in_orbit : b ∈ orbit (↥(fixingSubgroup M sᶜ)) a<GOAL>b ∈ s
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Group M<VAR>inst✝ : MulAction M α<VAR>s : Set α<VAR>a : α<VAR>a_in_s : a ∈ s<VAR>b : α<VAR>b_in_orbit : b ∈ orbit (↥(fixingSubgroup M sᶜ)) a<VAR>g : M<VAR>g_fixing : g ∈ fixingSubgroup M sᶜ<VAR>g_eq : ⟨g, g_fixing⟩ • a = b<GOAL>b ∈ s
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Group M<VAR>inst✝ : MulAction M α<VAR>s : Set α<VAR>a : α<VAR>a_in_s : a ∈ s<VAR>b : α<VAR>b_in_orbit : b ∈ orbit (↥(fixingSubgroup M sᶜ)) a<VAR>g : M<VAR>g_fixing : g ∈ fixingSubgroup M sᶜ<VAR>g_eq : g • a = b<GOAL>b ∈ s
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Group M<VAR>inst✝ : MulAction M α<VAR>s : Set α<VAR>a : α<VAR>a_in_s : a ∈ s<VAR>b : α<VAR>b_in_orbit : b ∈ orbit (↥(fixingSubgroup M sᶜ)) a<VAR>g : M<VAR>g_fixing : (fixedBy α g)ᶜ ⊆ s<VAR>g_eq : g • a = b<GOAL>b ∈ s
<VAR>R✝ : Type u_1<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : IsDomain R✝<VAR>R : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<GOAL>cyclotomic' 1 R = X - 1
<VAR>J : Type u<VAR>inst✝² : Category.{v, u} J<VAR>inst✝¹ : IsCofilteredOrEmpty J<VAR>s : Set J<VAR>inst✝ : Small.{v, u} ↑s<VAR>hs : ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)<GOAL>(fullSubcategoryInclusion fun x => x ∈ s).Initial
<VAR>J : Type u<VAR>inst✝² : Category.{v, u} J<VAR>inst✝¹ : IsCofilteredOrEmpty J<VAR>s : Set J<VAR>inst✝ : Small.{v, u} ↑s<VAR>hs : ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)<VAR>i : J<GOAL>∃ c, Nonempty ((fullSubcategoryInclusion fun x => x ∈ s).obj c ⟶ i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u : Set α<VAR>inst✝¹ : MeasurableSpace α<VAR>ι : Type u_5<VAR>inst✝ : Countable ι<VAR>f : ι → α → ℝ≥0<VAR>h : ∀ (i : ι), Measurable (f i)<GOAL>Measurable fun x => ∑' (i : ι), f i x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u : Set α<VAR>inst✝¹ : MeasurableSpace α<VAR>ι : Type u_5<VAR>inst✝ : Countable ι<VAR>f : ι → α → ℝ≥0<VAR>h : ∀ (i : ι), Measurable (f i)<GOAL>Measurable fun x => (∑' (b : ι), ↑(f b x)).toNNReal
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>η₁ η₂ : R<VAR>hη₁ : η₁ ∈ nthRootsFinset n R<VAR>hη₂ : η₂ ∈ nthRootsFinset n R<GOAL>η₁ * η₂ ∈ nthRootsFinset n R
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.91408, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>n₁ n₂ : ℤ<GOAL>(inr φ).f n₁ ≫ (mappingCone φ).d n₁ n₂ = G.d n₁ n₂ ≫ (inr φ).f n₂
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>A B X✝ X' Y Y' Z : C<VAR>inst✝² : HasFiniteProducts C<VAR>inst✝¹ : Exponentiable A<VAR>f : B ⟶ A<VAR>inst✝ : Exponentiable B<VAR>X : C<GOAL>uncurry ((pre f).app X) = prod.map f (𝟙 (A ⟹ X)) ≫ (exp.ev A).app X
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>s t : Set X<GOAL>dimH (s ∪ t) = max (dimH s) (dimH t)
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f'✝ f₀' f₁' g' : F<VAR>x✝ : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>f : E → 𝕜'<VAR>f' : E →L[𝕜] 𝕜'<VAR>x : E<VAR>hh : HasStrictFDerivAt h₂ (smulRight 1 h₂') (f x)<VAR>hf : HasStrictFDerivAt f f' x<GOAL>HasStrictFDerivAt (h₂ ∘ f) (h₂' • f') x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f'✝ f₀' f₁' g' : F<VAR>x✝ : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>f : E → 𝕜'<VAR>f' : E →L[𝕜] 𝕜'<VAR>x : E<VAR>hh : HasStrictFDerivAt h₂ (smulRight 1 h₂') (f x)<VAR>hf : HasStrictFDerivAt f f' x<GOAL>HSMul.hSMul h₂' = (ContinuousLinearMap.restrictScalars 𝕜 (smulRight 1 h₂')).comp
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f'✝ f₀' f₁' g' : F<VAR>x✝² : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>f : E → 𝕜'<VAR>f' : E →L[𝕜] 𝕜'<VAR>x✝¹ : E<VAR>hh : HasStrictFDerivAt h₂ (smulRight 1 h₂') (f x✝¹)<VAR>hf : HasStrictFDerivAt f f' x✝¹<VAR>x : E →L[𝕜] 𝕜'<VAR>x✝ : E<GOAL>(h₂' • x) x✝ = ((ContinuousLinearMap.restrictScalars 𝕜 (smulRight 1 h₂')).comp x) x✝
<VAR>x : ℝ<VAR>h : 0 < x<GOAL>sin x < x
<VAR>x : ℝ<VAR>h : 0 < x<VAR>h' : 1 < x<GOAL>sin x < x
<VAR>x : ℝ<VAR>h : 0 < x<VAR>h' : x ≤ 1<GOAL>sin x < x
<VAR>x : ℝ<VAR>h : 0 < x<VAR>h' : x ≤ 1<VAR>hx : |x| = x<GOAL>sin x < x
<VAR>x : ℝ<VAR>h : 0 < x<VAR>h' : x ≤ 1<VAR>hx : |x| = x<VAR>this : sin x - (x - x ^ 3 / 6) ≤ |x| ^ 4 * (5 / 96)<GOAL>sin x < x
<VAR>x : ℝ<VAR>h : 0 < x<VAR>h' : x ≤ 1<VAR>hx : |x| = x<VAR>this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)<GOAL>sin x < x
<VAR>x : ℝ<VAR>h : 0 < x<VAR>h' : x ≤ 1<VAR>hx : |x| = x<VAR>this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)<GOAL>x - x ^ 3 / 6 + x ^ 4 * (5 / 96) < x
<VAR>x : ℝ<VAR>h : 0 < x<VAR>h' : x ≤ 1<VAR>hx : |x| = x<VAR>this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)<GOAL>x ^ 4 * (5 / 96) < x ^ 3 * 6⁻¹
<VAR>x : ℝ<VAR>h : 0 < x<VAR>h' : x ≤ 1<VAR>hx : |x| = x<VAR>this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)<GOAL>x ^ 4 ≤ x ^ 3
<VAR>x : ℝ<VAR>h : 0 < x<VAR>h' : x ≤ 1<VAR>hx : |x| = x<VAR>this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)<GOAL>3 ≤ 4
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Lattice α<VAR>inst✝ : Lattice β<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>h : b ≤ a<GOAL>[[a, b]] = Icc b a
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>i j : n<GOAL>(A * A.adjugate) i j = (A.det • 1) i j
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>i j : n<GOAL>∑ j_1 : n, A i j_1 * A.adjugate j_1 j = if i = j then A.det else 0
<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✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f : E → F<VAR>s : Set E<VAR>x v : E<VAR>f' : F<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>h : HasLineDerivWithinAt 𝕜 f (c • f') s x (c • v)<GOAL>HasLineDerivWithinAt 𝕜 f f' s x v
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : ι), IsNormal (f i)<GOAL>derivFamily f = enumOrd (⋂ i, fixedPoints (f i))
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : ι), IsNormal (f i)<GOAL>StrictMono (derivFamily f) ∧ Set.range (derivFamily f) = ⋂ i, fixedPoints (f i)
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : ι), IsNormal (f i)<GOAL>Set.range (derivFamily f) = ⋂ i, fixedPoints (f i)
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : ι), IsNormal (f i)<GOAL>(∀ (a : Ordinal.{max u v}), derivFamily f a ∈ ⋂ i, fixedPoints (f i)) ∧ ∀ b ∈ ⋂ i, fixedPoints (f i), ∃ a, derivFamily f a = b
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : ι), IsNormal (f i)<VAR>a : Ordinal.{max u v}<VAR>ha : a ∈ ⋂ i, fixedPoints (f i)<GOAL>∃ a_1, derivFamily f a_1 = a
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : ι), IsNormal (f i)<VAR>a : Ordinal.{max u v}<VAR>ha : ∀ (i : ι), a ∈ fixedPoints (f i)<GOAL>∃ a_1, derivFamily f a_1 = a
<VAR>K : Type u<VAR>inst✝ : Field K<GOAL>X.intDegree = 1
<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>ε : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f✝ : E → F<VAR>f'✝ : E →L[𝕜] F<VAR>s✝ t : Set E<VAR>c✝ c' : ℝ≥0<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>s : Set E<VAR>c : ℝ≥0<GOAL>ApproximatesLinearOn f f' s c ↔ LipschitzOnWith c (f - ⇑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>ε : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f✝ : E → F<VAR>f'✝ : E →L[𝕜] F<VAR>s✝ t : Set E<VAR>c✝ c' : ℝ≥0<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>this : ∀ (x y : E), f x - f y - f' (x - y) = (f - ⇑f') x - (f - ⇑f') y<GOAL>ApproximatesLinearOn f f' s c ↔ LipschitzOnWith c (f - ⇑f') s
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : MulOneClass M<VAR>s : Set M<VAR>inst✝ : AddZeroClass A<VAR>t : Set A<VAR>S p₁ p₂ : Submonoid M<GOAL>Disjoint p₁ p₂ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1
<VAR>n : ℕ<GOAL>Real.log (stirlingSeq (n + 1)) - Real.log (stirlingSeq (n + 2)) ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2)
<VAR>n : ℕ<VAR>h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2<GOAL>Real.log (stirlingSeq (n + 1)) - Real.log (stirlingSeq (n + 2)) ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2)
<VAR>n : ℕ<VAR>h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2<VAR>g : HasSum (fun k => ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1)) ((1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2))<GOAL>Real.log (stirlingSeq (n + 1)) - Real.log (stirlingSeq (n + 2)) ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2)
<VAR>n : ℕ<VAR>h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2<VAR>g : HasSum (fun k => ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1)) ((1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2))<VAR>hab : ∀ (k : ℕ), 1 / (2 * ↑(k + 1) + 1) * ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1) ≤ ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1)<GOAL>Real.log (stirlingSeq (n + 1)) - Real.log (stirlingSeq (n + 2)) ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝² : FunLike F (Set α) ℝ≥0∞<VAR>inst✝¹ : OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>inst✝ : Countable α<VAR>p : α → Prop<GOAL>(∀ᵐ (x : α) ∂μ, p x) ↔ ∀ (x : α), μ {x} ≠ 0 → p x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝² : FunLike F (Set α) ℝ≥0∞<VAR>inst✝¹ : OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>inst✝ : Countable α<VAR>p : α → Prop<GOAL>(∀ x ∈ {a | ¬p a}, μ {x} = 0) ↔ ∀ (x : α), μ {x} ≠ 0 → p x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝² : FunLike F (Set α) ℝ≥0∞<VAR>inst✝¹ : OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>inst✝ : Countable α<VAR>p : α → Prop<GOAL>{a | ¬p a}.Countable
<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>h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ DifferentiableOn 𝕜 f (s ∩ u)<VAR>x : E<VAR>xs : x ∈ s<VAR>t : Set E<VAR>t_open : IsOpen t<VAR>xt : x ∈ t<VAR>ht : DifferentiableOn 𝕜 f (s ∩ t)<GOAL>DifferentiableWithinAt 𝕜 f s x
<VAR>s : ℂ<GOAL>s.GammaIntegral = mellin (fun x => ↑(rexp (-x))) s
<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 : α → α → Prop<VAR>a b c d : α<VAR>hr : Reflexive r<GOAL>ReflTransGen r = TransGen r
<VAR>m✝ n✝ m : ℕ∞<VAR>n : ℕ<VAR>h : m ≤ ↑n<GOAL>m.toNat ≤ n
<VAR>m✝ n✝ : ℕ∞<VAR>n m : ℕ<VAR>h : ↑m ≤ ↑n<GOAL>(↑m).toNat ≤ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hr : r ≠ ⊤<VAR>h : ¬r = 0<GOAL>∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (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>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hr : r ≠ ⊤<VAR>h : ¬r = 0<GOAL>∫⁻ (a : α), r * f a ∂μ ≤ r * ∫⁻ (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>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hr : r ≠ ⊤<VAR>h : ¬r = 0<VAR>rinv : r * r⁻¹ = 1<GOAL>∫⁻ (a : α), r * f a ∂μ ≤ r * ∫⁻ (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>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hr : r ≠ ⊤<VAR>h : ¬r = 0<VAR>rinv : r * r⁻¹ = 1<VAR>rinv' : r⁻¹ * r = 1<GOAL>∫⁻ (a : α), r * f a ∂μ ≤ r * ∫⁻ (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>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hr : r ≠ ⊤<VAR>h : ¬r = 0<VAR>rinv : r * r⁻¹ = 1<VAR>rinv' : r⁻¹ * r = 1<VAR>this : r⁻¹ * ∫⁻ (a : α), r * f a ∂μ ≤ ∫⁻ (a : α), r⁻¹ * (r * f a) ∂μ<GOAL>∫⁻ (a : α), r * f a ∂μ ≤ r * ∫⁻ (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>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hr : r ≠ ⊤<VAR>h : ¬r = 0<VAR>rinv : r * r⁻¹ = 1<VAR>rinv' : r⁻¹ * r = 1<VAR>this : r⁻¹ * ∫⁻ (a : α), r * f a ∂μ ≤ ∫⁻ (a : α), f a ∂μ<GOAL>∫⁻ (a : α), r * f a ∂μ ≤ r * ∫⁻ (a : α), f a ∂μ
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<GOAL>Function.Surjective ⇑(M.mulMap' N)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : Countable ι<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : Preorder ι<VAR>φ : ι → Set α<VAR>hφ : AECover μ atTop φ<VAR>x : α<VAR>h : ∀ᶠ (i : ι) in atTop, x ∈ φ i<GOAL>∀ᶠ (i : ι) in atTop, x ∈ ⋂ k ∈ Ici i, φ k
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : NonAssocRing α<VAR>inst✝ : Nontrivial α<VAR>a : α<VAR>h : a - 1 = a<GOAL>a + -1 = a + -0
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedSemiring α✝<VAR>inst✝² : FloorSemiring α✝<VAR>a✝ : α✝<VAR>n : ℕ<VAR>α : Type u_4<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorSemiring α<VAR>z : ℤ<VAR>a : ℕ<GOAL>⌈↑z⌉₊ ≤ a ↔ z.toNat ≤ a
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedSemiring α✝<VAR>inst✝² : FloorSemiring α✝<VAR>a✝ : α✝<VAR>n : ℕ<VAR>α : Type u_4<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorSemiring α<VAR>z : ℤ<VAR>a : ℕ<GOAL>↑z ≤ ↑a ↔ z ≤ ↑a
<VAR>I : Type u<VAR>inst✝³ : LinearOrder I<VAR>inst✝² : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>J K : I → Prop<VAR>h : ∀ a ∈ ↑l, J a<VAR>inst✝¹ : (j : I) → Decidable (J j)<VAR>inst✝ : (j : I) → Decidable (K j)<VAR>hJK : ∀ (i : I), J i → K i<GOAL>⇑(eval (π C J) l) ∘ ProjRestricts C hJK = ⇑(eval (π C K) l)
<VAR>I : Type u<VAR>inst✝³ : LinearOrder I<VAR>inst✝² : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>J K : I → Prop<VAR>h : ∀ a ∈ ↑l, J a<VAR>inst✝¹ : (j : I) → Decidable (J j)<VAR>inst✝ : (j : I) → Decidable (K j)<VAR>hJK : ∀ (i : I), J i → K i<VAR>this : ⇑(eval (π C J) l) ∘ ⇑(Homeomorph.setCongr ⋯) = ⇑(eval (π (π C K) J) l)<GOAL>⇑(eval (π C J) l) ∘ ProjRestricts C hJK = ⇑(eval (π C K) l)
<VAR>α : Type u_1<VAR>inst✝ : OrderedRing α<VAR>a : α<GOAL>Pairwise (Disjoint on fun n => Ico (a + ↑n) (a + ↑n + 1))
<VAR>x y : ℂ<GOAL>sinh (x - y) = sinh x * cosh y - cosh x * sinh y
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsDomain B<VAR>inst✝ : IsIntegrallyClosed A<GOAL>1 ≤ 1ᵛ
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsDomain B<VAR>inst✝ : IsIntegrallyClosed A<GOAL>map (↑A (Algebra.trace K L)) (restrictScalars A 1) ≤ 1
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsDomain B<VAR>inst✝ : IsIntegrallyClosed A<VAR>x : B<GOAL>(↑A (Algebra.trace K L)) ((Algebra.linearMap B L) x) ∈ 1
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsDomain B<VAR>inst✝ : IsIntegrallyClosed A<VAR>x : B<GOAL>IsIntegral A ((↑A (Algebra.trace K L)) ((Algebra.linearMap B L) x))