ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>h : LinearMap.range f' = ⊤<VAR>f'symm : f'.NonlinearRightInverse := f'.nonlinearRightInverseOfSurjective h<VAR>c : ℝ≥0 := f'symm.nnnorm⁻¹ / 2<VAR>hc : c = f'symm.nnnorm⁻¹ / 2<VAR>f'symm_pos : 0 < f'symm.nnnorm<VAR>cpos : 0 < c<VAR>s : Set E<VAR>s_nhds : s ∈ 𝓝 a<VAR>hs : ApproximatesLinearOn f f' s c<GOAL>map f (𝓝 a) = 𝓝 (f a)
<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>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>h : LinearMap.range f' = ⊤<VAR>f'symm : f'.NonlinearRightInverse := f'.nonlinearRightInverseOfSurjective h<VAR>c : ℝ≥0 := f'symm.nnnorm⁻¹ / 2<VAR>hc : c = f'symm.nnnorm⁻¹ / 2<VAR>f'symm_pos : 0 < f'symm.nnnorm<VAR>cpos : 0 < c<VAR>s : Set E<VAR>s_nhds : s ∈ 𝓝 a<VAR>hs : ApproximatesLinearOn f f' s c<GOAL>f'symm.nnnorm⁻¹ ≠ 0
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<GOAL>⨆ a, LinearMap.range (lsingle a) = ⊤
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>f : α →₀ M<VAR>x✝ : f ∈ ⊤<GOAL>f ∈ ⨆ a, LinearMap.range (lsingle a)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>f : α →₀ M<VAR>x✝ : f ∈ ⊤<GOAL>f.sum single ∈ ⨆ a, LinearMap.range (lsingle a)
<VAR>C : Type u_1<VAR>C' : Type ?u.85122<VAR>D : Type ?u.85125<VAR>D' : Type ?u.85128<VAR>H : Type u_2<VAR>H' : Type ?u.85134<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{?u.85142, ?u.85122} C'<VAR>inst✝⁴ : Category.{?u.85146, ?u.85125} D<VAR>inst✝³ : Category.{?u.85150, ?u.85128} D'<VAR>inst✝² : Category.{u_4, u_2} H<VAR>inst✝¹ : Category.{?u.85158, ?u.85134} H'<VAR>RF RF' RF'' : D ⥤ H<VAR>F F' F'' : C ⥤ H<VAR>e : F ≅ F'<VAR>L : C ⥤ D<VAR>α : F ⟶ L ⋙ RF<VAR>α' : F' ⟶ L ⋙ RF'<VAR>α'' : F'' ⟶ L ⋙ RF''<VAR>α'₂ : F ⟶ L ⋙ RF'<VAR>W : MorphismProperty C<VAR>inst✝ : L.IsLocalization W<GOAL>F.HasRightDerivedFunctor W ↔ F'.HasRightDerivedFunctor W
<VAR>X Y S : Type v<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>c : PullbackCone f g<VAR>hc : IsLimit c<VAR>x : Types.PullbackObj f g<GOAL>c.snd ((equivPullbackObj hc).symm x) = (↑x).2
<VAR>X Y S : Type v<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>c : PullbackCone f g<VAR>hc : IsLimit c<VAR>x : c.pt<GOAL>c.snd ((equivPullbackObj hc).symm ((equivPullbackObj hc) x)) = (↑((equivPullbackObj hc) x)).2
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p : R<VAR>k n : ℕ<GOAL>IsPrimePow n ↔ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>n : ℕ<VAR>f : α → α<VAR>a : α<GOAL>(iterate f a).get n.succ = (iterate f (f a)).get n
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹¹ : NormedField 𝕜₁<VAR>inst✝¹⁰ : NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁹ : AddCommGroup E<VAR>inst✝⁸ : Module 𝕜₁ E<VAR>inst✝⁷ : TopologicalSpace E<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module 𝕜₂ F<VAR>inst✝⁴ : RingHomSurjective σ<VAR>inst✝³ : RingHomIsometric σ<VAR>inst✝² : TopologicalSpace F<VAR>inst✝¹ : TopologicalAddGroup F<VAR>inst✝ : ContinuousSMul 𝕜₂ F<VAR>𝔖 : Set (Set E)<VAR>h𝔖₃ : ∀ S ∈ 𝔖, Bornology.IsVonNBounded 𝕜₁ S<VAR>this : UniformSpace F := TopologicalAddGroup.toUniformSpace F<GOAL>ContinuousSMul 𝕜₂ (UniformConvergenceCLM σ F 𝔖)
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹¹ : NormedField 𝕜₁<VAR>inst✝¹⁰ : NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁹ : AddCommGroup E<VAR>inst✝⁸ : Module 𝕜₁ E<VAR>inst✝⁷ : TopologicalSpace E<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module 𝕜₂ F<VAR>inst✝⁴ : RingHomSurjective σ<VAR>inst✝³ : RingHomIsometric σ<VAR>inst✝² : TopologicalSpace F<VAR>inst✝¹ : TopologicalAddGroup F<VAR>inst✝ : ContinuousSMul 𝕜₂ F<VAR>𝔖 : Set (Set E)<VAR>h𝔖₃ : ∀ S ∈ 𝔖, Bornology.IsVonNBounded 𝕜₁ S<VAR>this✝ : UniformSpace F := TopologicalAddGroup.toUniformSpace F<VAR>this : UniformAddGroup F<GOAL>ContinuousSMul 𝕜₂ (UniformConvergenceCLM σ F 𝔖)
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹¹ : NormedField 𝕜₁<VAR>inst✝¹⁰ : NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁹ : AddCommGroup E<VAR>inst✝⁸ : Module 𝕜₁ E<VAR>inst✝⁷ : TopologicalSpace E<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module 𝕜₂ F<VAR>inst✝⁴ : RingHomSurjective σ<VAR>inst✝³ : RingHomIsometric σ<VAR>inst✝² : TopologicalSpace F<VAR>inst✝¹ : TopologicalAddGroup F<VAR>inst✝ : ContinuousSMul 𝕜₂ F<VAR>𝔖 : Set (Set E)<VAR>h𝔖₃ : ∀ S ∈ 𝔖, Bornology.IsVonNBounded 𝕜₁ S<VAR>this✝ : UniformSpace F := TopologicalAddGroup.toUniformSpace F<VAR>this : UniformAddGroup F<VAR>φ : UniformConvergenceCLM σ F 𝔖 →ₗ[𝕜₂] E → F := { toFun := DFunLike.coe, map_add' := ⋯, map_smul' := ⋯ }<GOAL>ContinuousSMul 𝕜₂ (UniformConvergenceCLM σ F 𝔖)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → AddZeroClass (β i)<VAR>i : ι<VAR>f : Π₀ (i : ι), β i<GOAL>(erase i f + single i (f i)) i = f i
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → AddZeroClass (β i)<VAR>i : ι<VAR>f : Π₀ (i : ι), β i<VAR>i' : ι<VAR>h : ¬i = i'<GOAL>(erase i f + single i (f i)) i' = f i'
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>ι : Type v<VAR>hs : IsLindelof s<VAR>U : ι → Set X<VAR>hUo : ∀ (i : ι), IsOpen (U i)<VAR>hsU : s ⊆ ⋃ i, U i<GOAL>∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>ι : Type v<VAR>hs : IsLindelof s<VAR>U : ι → Set X<VAR>hUo : ∀ (i : ι), IsOpen (U i)<VAR>hsU : s ⊆ ⋃ i, U i<VAR>hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → (∃ r, r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i<GOAL>∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>ι : Type v<VAR>hs : IsLindelof s<VAR>U : ι → Set X<VAR>hUo : ∀ (i : ι), IsOpen (U i)<VAR>hsU : s ⊆ ⋃ i, U i<VAR>hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → (∃ r, r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i<VAR>hcountable_union : ∀ (S : Set (Set X)), S.Countable → (∀ s ∈ S, ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i<GOAL>∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>ι : Type v<VAR>hs : IsLindelof s<VAR>U : ι → Set X<VAR>hUo : ∀ (i : ι), IsOpen (U i)<VAR>hsU : s ⊆ ⋃ i, U i<VAR>hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → (∃ r, r.Countable ∧ t ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i<VAR>hcountable_union : ∀ (S : Set (Set X)), S.Countable → (∀ s ∈ S, ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) → ∃ r, r.Countable ∧ ⋃₀ S ⊆ ⋃ i ∈ r, U i<VAR>h_nhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∃ r, r.Countable ∧ t ⊆ ⋃ i ∈ r, U i<GOAL>∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
<VAR>A : Set ℕ<VAR>inst✝ : DecidablePred fun x => x ∈ A<VAR>k : ℕ<VAR>hk : k ∉ A<GOAL>schnirelmannDensity A ≤ 1 - (↑k)⁻¹
<VAR>A : Set ℕ<VAR>inst✝ : DecidablePred fun x => x ∈ A<VAR>hk : 0 ∉ A<GOAL>schnirelmannDensity A ≤ 1 - (↑0)⁻¹
<VAR>A : Set ℕ<VAR>inst✝ : DecidablePred fun x => x ∈ A<VAR>k : ℕ<VAR>hk : k ∉ A<VAR>hk' : k > 0<GOAL>schnirelmannDensity A ≤ 1 - (↑k)⁻¹
<VAR>A : Set ℕ<VAR>inst✝ : DecidablePred fun x => x ∈ A<VAR>k : ℕ<VAR>hk : k ∉ A<VAR>hk' : k > 0<GOAL>↑(filter (fun x => x ∈ A) (Ioc 0 k)).card / ↑k ≤ 1 - (↑k)⁻¹
<VAR>A : Set ℕ<VAR>inst✝ : DecidablePred fun x => x ∈ A<VAR>k : ℕ<VAR>hk : k ∉ A<VAR>hk' : k > 0<GOAL>↑(filter (fun x => x ∈ A) (Ioc 0 k)).card / ↑k ≤ (↑k - 1) / ↑k
<VAR>A : Set ℕ<VAR>inst✝ : DecidablePred fun x => x ∈ A<VAR>k : ℕ<VAR>hk : k ∉ A<VAR>hk' : k > 0<GOAL>↑(filter (fun x => x ∈ A) (Ioc 0 k)).card ≤ ↑k - 1
<VAR>A : Set ℕ<VAR>inst✝ : DecidablePred fun x => x ∈ A<VAR>k : ℕ<VAR>hk : k ∉ A<VAR>hk' : k > 0<GOAL>(filter (fun x => x ∈ A) (Ioc 0 k)).card ≤ k - 1
<VAR>A : Set ℕ<VAR>inst✝ : DecidablePred fun x => x ∈ A<VAR>k : ℕ<VAR>hk : k ∉ A<VAR>hk' : k > 0<GOAL>filter (fun x => x ∈ A) (Ioc 0 k) ⊆ Ioo 0 k
<VAR>A : Set ℕ<VAR>inst✝ : DecidablePred fun x => x ∈ A<VAR>k : ℕ<VAR>hk : k ∉ A<VAR>hk' : k > 0<GOAL>filter (fun x => x ∈ A) (Ioo 0 k) ⊆ Ioo 0 k
<VAR>R : Type u_1<VAR>inst✝¹ : MonoidWithZero R<VAR>inst✝ : Nontrivial R<GOAL>¬Squarefree 0
<VAR>R : Type u_1<VAR>inst✝¹ : MonoidWithZero R<VAR>inst✝ : Nontrivial R<GOAL>∃ x, ¬(x * x ∣ 0 → IsUnit x)
<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>iso : E ≃L[𝕜] F<VAR>L : G ≃L[𝕜] G'<VAR>f : E → F →L[𝕜] G<VAR>hs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderivWithin 𝕜 (⇑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘ f) s x = (↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)).comp (fderivWithin 𝕜 f s x)
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>f : End F<VAR>A : PointedGaloisObject F<GOAL>F.map ((AutGalois.π F A) ((endEquivAutGalois F) f)).hom A.pt = f.app A.obj A.pt
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>f : End F<VAR>A : PointedGaloisObject F<GOAL>F.map (↑(((sectionsFunctor (PointedGaloisObject F)).mapIso (autIsoFibers F)).symm.toEquiv ((endEquivSectionsFibers F) f)) A).hom A.pt = f.app A.obj A.pt
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>f : End F<VAR>A : PointedGaloisObject F<GOAL>F.map ((evaluationEquivOfIsGalois F A.obj A.pt).symm (↑((endEquivSectionsFibers F) f) A)).hom A.pt = f.app A.obj A.pt
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>f : End F<VAR>A : PointedGaloisObject F<GOAL>F.map ((evaluationEquivOfIsGalois F A.obj A.pt).symm (f.app A.obj A.pt)).hom A.pt = f.app A.obj A.pt
<VAR>α : Type u_1<VAR>inst✝ : AddMonoidWithOne α<VAR>n : PosNum<GOAL>↑n.succ = ↑n + 1
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f f' f'' : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x<VAR>hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x<VAR>hf''₀ : ∀ x ∈ interior D, 0 ≤ f'' x<GOAL>ConvexOn ℝ D f
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f f' f'' : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x<VAR>hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x<VAR>hf''₀ : ∀ x ∈ interior D, 0 ≤ f'' x<VAR>this : EqOn (deriv f) f' (interior D)<GOAL>ConvexOn ℝ D f
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f f' f'' : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x<VAR>hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x<VAR>hf''₀ : ∀ x ∈ interior D, 0 ≤ f'' x<VAR>this : EqOn (deriv f) f' (interior D)<GOAL>DifferentiableOn ℝ (deriv f) (interior D)
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f f' f'' : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x<VAR>hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x<VAR>hf''₀ : ∀ x ∈ interior D, 0 ≤ f'' x<VAR>this : EqOn (deriv f) f' (interior D)<GOAL>∀ x ∈ interior D, 0 ≤ deriv^[2] f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>u v : α → ℝ<GOAL>(f =O[l] fun x => ‖g' x‖) ↔ f =O[l] g'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>u v : α → ℝ<GOAL>(∃ c, IsBigOWith c l f fun x => ‖g' x‖) ↔ ∃ c, IsBigOWith c l f g'
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : SimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 2)<GOAL>X.δ i.castSucc ≫ X.δ i = X.δ i.succ ≫ X.δ i
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>S : Set (Set X)<VAR>hf : S.Finite<VAR>hc : ∀ s ∈ S, IsCompact s<GOAL>IsCompact (⋃₀ S)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>S : Set (Set X)<VAR>hf : S.Finite<VAR>hc : ∀ s ∈ S, IsCompact s<GOAL>IsCompact (⋃ i ∈ S, i)
<VAR>G : Type u_1<VAR>inst✝¹⁰ : TopologicalSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : TopologicalGroup G<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝⁴ : μ.IsHaarMeasure<VAR>inst✝³ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝² : μ'.IsMulLeftInvariant<VAR>inst✝¹ : μ.InnerRegularCompactLTTop<VAR>inst✝ : μ'.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : μ s ≠ ⊤<VAR>h's : μ' s ≠ ⊤<VAR>c : ℝ≥0 := μ'.haarScalarFactor μ<GOAL>μ' s = μ'.haarScalarFactor μ • μ s
<VAR>G : Type u_1<VAR>inst✝¹⁰ : TopologicalSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : TopologicalGroup G<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝⁴ : μ.IsHaarMeasure<VAR>inst✝³ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝² : μ'.IsMulLeftInvariant<VAR>inst✝¹ : μ.InnerRegularCompactLTTop<VAR>inst✝ : μ'.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : μ s ≠ ⊤<VAR>h's : μ' s ≠ ⊤<VAR>c : ℝ≥0 := μ'.haarScalarFactor μ<VAR>B : ∀ (s : Set G), MeasurableSet s → μ s < ⊤ → μ' s < ⊤ → μ' s = (c • μ) s<GOAL>μ' s = μ'.haarScalarFactor μ • μ s
<VAR>G : Type u_1<VAR>inst✝¹⁰ : TopologicalSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : TopologicalGroup G<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝⁴ : μ.IsHaarMeasure<VAR>inst✝³ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝² : μ'.IsMulLeftInvariant<VAR>inst✝¹ : μ.InnerRegularCompactLTTop<VAR>inst✝ : μ'.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : μ s ≠ ⊤<VAR>h's : μ' s ≠ ⊤<VAR>c : ℝ≥0 := μ'.haarScalarFactor μ<VAR>B : ∀ (s : Set G), MeasurableSet s → μ s < ⊤ → μ' s < ⊤ → μ' s = (c • μ) s<VAR>t : Set G := toMeasurable μ' s ∩ toMeasurable μ s<GOAL>μ' s = μ'.haarScalarFactor μ • μ s
<VAR>G : Type u_1<VAR>inst✝¹⁰ : TopologicalSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : TopologicalGroup G<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝⁴ : μ.IsHaarMeasure<VAR>inst✝³ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝² : μ'.IsMulLeftInvariant<VAR>inst✝¹ : μ.InnerRegularCompactLTTop<VAR>inst✝ : μ'.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : μ s ≠ ⊤<VAR>h's : μ' s ≠ ⊤<VAR>c : ℝ≥0 := μ'.haarScalarFactor μ<VAR>B : ∀ (s : Set G), MeasurableSet s → μ s < ⊤ → μ' s < ⊤ → μ' s = (c • μ) s<VAR>t : Set G := toMeasurable μ' s ∩ toMeasurable μ s<VAR>st : s ⊆ t<GOAL>μ' s = μ'.haarScalarFactor μ • μ s
<VAR>G : Type u_1<VAR>inst✝¹⁰ : TopologicalSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : TopologicalGroup G<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝⁴ : μ.IsHaarMeasure<VAR>inst✝³ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝² : μ'.IsMulLeftInvariant<VAR>inst✝¹ : μ.InnerRegularCompactLTTop<VAR>inst✝ : μ'.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : μ s ≠ ⊤<VAR>h's : μ' s ≠ ⊤<VAR>c : ℝ≥0 := μ'.haarScalarFactor μ<VAR>B : ∀ (s : Set G), MeasurableSet s → μ s < ⊤ → μ' s < ⊤ → μ' s = (c • μ) s<VAR>t : Set G := toMeasurable μ' s ∩ toMeasurable μ s<VAR>st : s ⊆ t<VAR>mu'_t : μ' t = μ' s<VAR>mu_t : μ t = μ s<GOAL>μ' s = μ'.haarScalarFactor μ • μ s
<VAR>G : Type u_1<VAR>inst✝¹⁰ : TopologicalSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : TopologicalGroup G<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝⁴ : μ.IsHaarMeasure<VAR>inst✝³ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝² : μ'.IsMulLeftInvariant<VAR>inst✝¹ : μ.InnerRegularCompactLTTop<VAR>inst✝ : μ'.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : μ s ≠ ⊤<VAR>h's : μ' s ≠ ⊤<VAR>c : ℝ≥0 := μ'.haarScalarFactor μ<VAR>B : ∀ (s : Set G), MeasurableSet s → μ s < ⊤ → μ' s < ⊤ → μ' s = (c • μ) s<VAR>t : Set G := toMeasurable μ' s ∩ toMeasurable μ s<VAR>st : s ⊆ t<VAR>mu'_t : μ' t = μ' s<VAR>mu_t : μ t = μ s<GOAL>μ' t = ↑(μ'.haarScalarFactor μ) * μ t
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra R A<VAR>θ : ℂ<VAR>n : ℤ<GOAL>eval (cos θ) (T ℂ n) = cos (↑n * θ)
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddCommMonoid A<VAR>inst✝ : HasShift C A<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>n : A<GOAL>(shiftFunctorZero C A).inv.app ((shiftFunctor C n).obj X) = (shiftFunctor C n).map ((shiftFunctorZero C A).inv.app X) ≫ (shiftFunctorComm C n 0).inv.app X
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddCommMonoid A<VAR>inst✝ : HasShift C A<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>n : A<GOAL>𝟙 ((𝟭 C).obj ((shiftFunctor C n).obj X)) = (shiftFunctor C n).map (𝟙 ((𝟭 C).obj X))
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddCommMonoid A<VAR>inst✝ : HasShift C A<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>n : A<GOAL>𝟙 ((shiftFunctor C n).obj X) = (shiftFunctor C n).map (𝟙 X)
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a : α<VAR>inst✝ : Fintype α<VAR>F : Finset (Finset α)<VAR>hs : s.Nonempty<GOAL>(atomise s ∅).parts = {s}
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a : α<VAR>inst✝ : Fintype α<VAR>F : Finset (Finset α)<VAR>hs : s.Nonempty<GOAL>(ofErase {s} ⋯ ⋯).parts = {s}
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : Fintype τ<VAR>n : ℕ<VAR>e : σ ≃ τ<GOAL>(rename ⇑e) (esymm σ R n) = ∑ x ∈ powersetCard n univ, ∏ i ∈ x, X (e i)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : Fintype τ<VAR>n : ℕ<VAR>e : σ ≃ τ<GOAL>∑ x ∈ powersetCard n univ, ∏ i ∈ x, X (e i) = ∑ t ∈ powersetCard n (Finset.map e.toEmbedding univ), ∏ i ∈ t, X i
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : Fintype τ<VAR>n : ℕ<VAR>e : σ ≃ τ<GOAL>∑ x ∈ powersetCard n univ, ∏ i ∈ x, X (e i) = ∑ x ∈ powersetCard n univ, ∏ i ∈ (mapEmbedding e.toEmbedding) x, X i
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : Fintype τ<VAR>n : ℕ<VAR>e : σ ≃ τ<GOAL>∑ t ∈ powersetCard n (Finset.map e.toEmbedding univ), ∏ i ∈ t, X i = ∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i
<VAR>n m : ℕ<VAR>a b : Fin n<GOAL>a.castSucc < b.succ ↔ a ≤ b
<VAR>R : Type u<VAR>M : Type v<VAR>M'✝ : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid M'✝<VAR>inst✝² : Module R M'✝<VAR>I J : Ideal R<VAR>N P : Submodule R M<VAR>S : Set R<VAR>T : Set M<VAR>M' : Type w<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>s : Set M<VAR>x : M<GOAL>x ∈ I • span R s ↔ x ∈ span R (⋃ a ∈ I, ⋃ b ∈ s, {a • b})
<VAR>R : Type u<VAR>M : Type v<VAR>M'✝ : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid M'✝<VAR>inst✝² : Module R M'✝<VAR>I J : Ideal R<VAR>N P : Submodule R M<VAR>S : Set R<VAR>T : Set M<VAR>M' : Type w<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>s : Set M<VAR>x : M<GOAL>x ∈ span R (⋃ s_1 ∈ ↑I, ⋃ t ∈ s, {s_1 • t}) ↔ x ∈ span R (⋃ a ∈ I, ⋃ b ∈ s, {a • b})
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>e : ι → M<VAR>ε : ι → Dual R M<VAR>inst✝¹ : DecidableEq ι<VAR>h : DualBases e ε<VAR>inst✝ : _root_.Finite ι<VAR>i j : ι<GOAL>(h.basis.dualBasis i) (h.basis j) = (ε i) (h.basis j)
<VAR>x : ℝ<GOAL>sin (arctan x) = x / √(1 + x ^ 2)
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Ioo a b, g' x ≠ 0<VAR>hfb : Tendsto f (𝓝[<] b) (𝓝 0)<VAR>hgb : Tendsto g (𝓝[<] b) (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] b) l<GOAL>Tendsto (fun x => f x / g x) (𝓝[<] b) l