ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>inst✝⁶ : CommRing A<VAR>S : Submonoid A<VAR>hS✝ : S ≤ A⁰<VAR>inst✝⁵ : CommRing K<VAR>inst✝⁴ : Algebra A K<VAR>inst✝³ : IsFractionRing A K<VAR>B : Type u_3<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : IsLocalization S B<VAR>hS : S ≤ A⁰<VAR>a s : A<VAR>hs : s ∈ S<GOAL>IsLocalization.mk' K a ⟨s, ⋯⟩ ∈ (mapToFractionRing K S B hS).range
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>inst✝⁶ : CommRing A<VAR>S : Submonoid A<VAR>hS✝ : S ≤ A⁰<VAR>inst✝⁵ : CommRing K<VAR>inst✝⁴ : Algebra A K<VAR>inst✝³ : IsFractionRing A K<VAR>B : Type u_3<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : IsLocalization S B<VAR>hS : S ≤ A⁰<VAR>a s : A<VAR>hs : s ∈ S<GOAL>(mapToFractionRing K S B hS).toRingHom (IsLocalization.mk' B a ⟨s, hs⟩) = IsLocalization.mk' K a ⟨s, ⋯⟩
<VAR>F : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : E → F<VAR>R : ℝ<VAR>hR : R ≠ 0<GOAL>Integrable (fun x => f (R • x)) μ ↔ Integrable f μ
<VAR>F : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : E → F<VAR>R : ℝ<VAR>hR : R ≠ 0<GOAL>∀ {g : E → F}, Integrable g μ → ∀ {S : ℝ}, S ≠ 0 → Integrable (fun x => g (S • x)) μ
<VAR>F : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : E → F<VAR>R : ℝ<VAR>hR : R ≠ 0<VAR>g : E → F<VAR>hg : Integrable g μ<VAR>S : ℝ<VAR>hS : S ≠ 0<GOAL>Integrable (fun x => g (S • x)) μ
<VAR>F : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : E → F<VAR>R : ℝ<VAR>hR : R ≠ 0<VAR>g : E → F<VAR>hg : Integrable g μ<VAR>S : ℝ<VAR>hS : S ≠ 0<VAR>t : E ≃ᵐ E := (Homeomorph.smul ⋯.unit).toMeasurableEquiv<GOAL>Integrable (fun x => g (S • x)) μ
<VAR>F : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : E → F<VAR>R : ℝ<VAR>hR : R ≠ 0<VAR>g : E → F<VAR>hg : Integrable g μ<VAR>S : ℝ<VAR>hS : S ≠ 0<VAR>t : E ≃ᵐ E := (Homeomorph.smul ⋯.unit).toMeasurableEquiv<GOAL>Integrable g (Measure.map (fun x => S • x) μ)
<VAR>F : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : E → F<VAR>R : ℝ<VAR>hR : R ≠ 0<VAR>g : E → F<VAR>hg : Integrable g μ<VAR>S : ℝ<VAR>hS : S ≠ 0<VAR>t : E ≃ᵐ E := (Homeomorph.smul ⋯.unit).toMeasurableEquiv<GOAL>ENNReal.ofReal |(S ^ finrank ℝ E)⁻¹| ≠ 0
<VAR>α : Type u_1<VAR>inst✝⁸ : TopologicalSpace α<VAR>inst✝⁷ : NormalSpace α<VAR>inst✝⁶ : R1Space α<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : WeaklyLocallyCompactSpace α<VAR>inst✝ : μ.Regular<VAR>f : α → E<VAR>hf : Integrable f μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ g, HasCompactSupport g ∧ ∫⁻ (x : α), ↑‖f x - g x‖₊ ∂μ ≤ ε ∧ Continuous g ∧ Integrable g μ
<VAR>α : Type u_1<VAR>inst✝⁸ : TopologicalSpace α<VAR>inst✝⁷ : NormalSpace α<VAR>inst✝⁶ : R1Space α<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : WeaklyLocallyCompactSpace α<VAR>inst✝ : μ.Regular<VAR>f : α → E<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>hf : Memℒp f 1 μ<GOAL>∃ g, HasCompactSupport g ∧ eLpNorm (fun x => f x - g x) 1 μ ≤ ε ∧ Continuous g ∧ Memℒp g 1 μ
<VAR>x✝ x : ℝ<VAR>h1 : 0 ≤ x<VAR>h2 : x < π / 2<GOAL>x ≤ tan x
<VAR>x : ℝ<VAR>h1 : 0 ≤ 0<VAR>h2 : 0 < π / 2<GOAL>0 ≤ tan 0
<VAR>x✝ x : ℝ<VAR>h1 : 0 ≤ x<VAR>h2 : x < π / 2<VAR>h1' : 0 < x<GOAL>x ≤ tan x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ht : MeasurableSet t<VAR>hfs : IntegrableOn f s μ<VAR>hts : t ⊆ s<GOAL>∫ (x : X) in s \ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ - ∫ (x : X) in t, f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ht : MeasurableSet t<VAR>hfs : IntegrableOn f s μ<VAR>hts : t ⊆ s<GOAL>Disjoint (s \ t) t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ht : MeasurableSet t<VAR>hfs : IntegrableOn f s μ<VAR>hts : t ⊆ s<GOAL>MeasurableSet t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ht : MeasurableSet t<VAR>hfs : IntegrableOn f s μ<VAR>hts : t ⊆ s<GOAL>IntegrableOn f (s \ t) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ht : MeasurableSet t<VAR>hfs : IntegrableOn f s μ<VAR>hts : t ⊆ s<GOAL>IntegrableOn f t μ
<VAR>x : ℝ<GOAL>abs (cexp (↑x * I)) = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>n : Type u_4<VAR>m : Type u_5<VAR>inst✝ : Zero α<VAR>A : Matrix n n α<VAR>h : A.IsDiag<VAR>i j : n<VAR>g : ¬i = j<GOAL>Aᵀ i j = A i j
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>s t : Set α<GOAL>(s ∪ t).Countable ↔ s.Countable ∧ t.Countable
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁴ : (i : ι) → Module R (M₁ i)<VAR>inst✝³ : Module R M₂<VAR>f✝ f' : MultilinearMap R M₁ M₂<VAR>M₁' : ι → Type u_1<VAR>inst✝² : (i : ι) → AddCommMonoid (M₁' i)<VAR>inst✝¹ : (i : ι) → Module R (M₁' i)<VAR>inst✝ : DecidableEq ι<VAR>f : (i : ι) → M₁ i →ₗ[R] M₁' i<VAR>i : ι<VAR>f₁ f₂ : M₁ i →ₗ[R] M₁' i<VAR>g : MultilinearMap R M₁' M₂<VAR>x : (i : ι) → M₁ i<VAR>c : (i : ι) → (M₁ i →ₗ[R] M₁' i) → M₁' i := fun i f => f (x i)<GOAL>(g fun j => (update f i (f₁ + f₂) j) (x j)) = (g fun j => (update f i f₁ j) (x j)) + g fun j => (update f i f₂ j) (x j)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁴ : (i : ι) → Module R (M₁ i)<VAR>inst✝³ : Module R M₂<VAR>f✝ f' : MultilinearMap R M₁ M₂<VAR>M₁' : ι → Type u_1<VAR>inst✝² : (i : ι) → AddCommMonoid (M₁' i)<VAR>inst✝¹ : (i : ι) → Module R (M₁' i)<VAR>inst✝ : DecidableEq ι<VAR>f : (i : ι) → M₁ i →ₗ[R] M₁' i<VAR>i : ι<VAR>f₁ f₂ : M₁ i →ₗ[R] M₁' i<VAR>g : MultilinearMap R M₁' M₂<VAR>x : (i : ι) → M₁ i<VAR>c : (i : ι) → (M₁ i →ₗ[R] M₁' i) → M₁' i := fun i f => f (x i)<VAR>j : ι<GOAL>(update f i (f₁ + f₂) j) (x j) = update (fun j => (f j) (x j)) i (f₁ (x i) + f₂ (x i)) j
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁴ : (i : ι) → Module R (M₁ i)<VAR>inst✝³ : Module R M₂<VAR>f✝ f' : MultilinearMap R M₁ M₂<VAR>M₁' : ι → Type u_1<VAR>inst✝² : (i : ι) → AddCommMonoid (M₁' i)<VAR>inst✝¹ : (i : ι) → Module R (M₁' i)<VAR>inst✝ : DecidableEq ι<VAR>f : (i : ι) → M₁ i →ₗ[R] M₁' i<VAR>i : ι<VAR>f₁ f₂ : M₁ i →ₗ[R] M₁' i<VAR>g : MultilinearMap R M₁' M₂<VAR>x : (i : ι) → M₁ i<VAR>c : (i : ι) → (M₁ i →ₗ[R] M₁' i) → M₁' i := fun i f => f (x i)<VAR>j : ι<GOAL>(update f i f₁ j) (x j) = update (fun j => (f j) (x j)) i (f₁ (x i)) j
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁴ : (i : ι) → Module R (M₁ i)<VAR>inst✝³ : Module R M₂<VAR>f✝ f' : MultilinearMap R M₁ M₂<VAR>M₁' : ι → Type u_1<VAR>inst✝² : (i : ι) → AddCommMonoid (M₁' i)<VAR>inst✝¹ : (i : ι) → Module R (M₁' i)<VAR>inst✝ : DecidableEq ι<VAR>f : (i : ι) → M₁ i →ₗ[R] M₁' i<VAR>i : ι<VAR>f₁ f₂ : M₁ i →ₗ[R] M₁' i<VAR>g : MultilinearMap R M₁' M₂<VAR>x : (i : ι) → M₁ i<VAR>c : (i : ι) → (M₁ i →ₗ[R] M₁' i) → M₁' i := fun i f => f (x i)<VAR>j : ι<GOAL>(update f i f₂ j) (x j) = update (fun j => (f j) (x j)) i (f₂ (x i)) j
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁴ : (i : ι) → Module R (M₁ i)<VAR>inst✝³ : Module R M₂<VAR>f✝ f' : MultilinearMap R M₁ M₂<VAR>M₁' : ι → Type u_1<VAR>inst✝² : (i : ι) → AddCommMonoid (M₁' i)<VAR>inst✝¹ : (i : ι) → Module R (M₁' i)<VAR>inst✝ : DecidableEq ι<VAR>f : (i : ι) → M₁ i →ₗ[R] M₁' i<VAR>i : ι<VAR>a : R<VAR>f₀ : M₁ i →ₗ[R] M₁' i<VAR>g : MultilinearMap R M₁' M₂<VAR>x : (i : ι) → M₁ i<VAR>c : (i : ι) → (M₁ i →ₗ[R] M₁' i) → M₁' i := fun i f => f (x i)<GOAL>(g fun j => (update f i (a • f₀) j) (x j)) = a • g fun j => (update f i f₀ j) (x j)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁴ : (i : ι) → Module R (M₁ i)<VAR>inst✝³ : Module R M₂<VAR>f✝ f' : MultilinearMap R M₁ M₂<VAR>M₁' : ι → Type u_1<VAR>inst✝² : (i : ι) → AddCommMonoid (M₁' i)<VAR>inst✝¹ : (i : ι) → Module R (M₁' i)<VAR>inst✝ : DecidableEq ι<VAR>f : (i : ι) → M₁ i →ₗ[R] M₁' i<VAR>i : ι<VAR>a : R<VAR>f₀ : M₁ i →ₗ[R] M₁' i<VAR>g : MultilinearMap R M₁' M₂<VAR>x : (i : ι) → M₁ i<VAR>c : (i : ι) → (M₁ i →ₗ[R] M₁' i) → M₁' i := fun i f => f (x i)<VAR>j : ι<GOAL>(update f i (a • f₀) j) (x j) = update (fun j => (f j) (x j)) i (a • f₀ (x i)) j
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁴ : (i : ι) → Module R (M₁ i)<VAR>inst✝³ : Module R M₂<VAR>f✝ f' : MultilinearMap R M₁ M₂<VAR>M₁' : ι → Type u_1<VAR>inst✝² : (i : ι) → AddCommMonoid (M₁' i)<VAR>inst✝¹ : (i : ι) → Module R (M₁' i)<VAR>inst✝ : DecidableEq ι<VAR>f : (i : ι) → M₁ i →ₗ[R] M₁' i<VAR>i : ι<VAR>a : R<VAR>f₀ : M₁ i →ₗ[R] M₁' i<VAR>g : MultilinearMap R M₁' M₂<VAR>x : (i : ι) → M₁ i<VAR>c : (i : ι) → (M₁ i →ₗ[R] M₁' i) → M₁' i := fun i f => f (x i)<VAR>j : ι<GOAL>(update f i f₀ j) (x j) = update (fun j => (f j) (x j)) i (f₀ (x i)) j
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>f : E → F<VAR>s : Set E<VAR>x : E<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>hp : HasFPowerSeriesOnBall f p x r<GOAL>AnalyticWithinAt 𝕜 f s x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<VAR>x✝ : M<VAR>h : x✝ ∈ torsionBy R M 1<GOAL>x✝ ∈ ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<VAR>x✝ : M<VAR>h : x✝ = 0<GOAL>x✝ ∈ ⊥
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>f : 𝓢(E, F)<VAR>inst✝ : ProperSpace E<VAR>s : ℝ<VAR>k : ℕ := ⌈-s⌉₊<GOAL>⇑f =O[cocompact E] fun x => ‖x‖ ^ s
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>f : 𝓢(E, F)<VAR>inst✝ : ProperSpace E<VAR>s : ℝ<VAR>k : ℕ := ⌈-s⌉₊<VAR>hk : -↑k ≤ s<GOAL>⇑f =O[cocompact E] fun x => ‖x‖ ^ s
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>f : 𝓢(E, F)<VAR>inst✝ : ProperSpace E<VAR>s : ℝ<VAR>k : ℕ := ⌈-s⌉₊<VAR>hk : -↑k ≤ s<GOAL>(fun x => ‖x‖ ^ (-↑k)) =O[cocompact E] fun x => ‖x‖ ^ s
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>f : 𝓢(E, F)<VAR>inst✝ : ProperSpace E<VAR>s : ℝ<VAR>k : ℕ := ⌈-s⌉₊<VAR>hk : -↑k ≤ s<GOAL>(fun x => x ^ (-↑k)) =O[atTop] fun x => x ^ s
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>f : 𝓢(E, F)<VAR>inst✝ : ProperSpace E<VAR>s : ℝ<VAR>k : ℕ := ⌈-s⌉₊<VAR>hk : -↑k ≤ s<GOAL>∃ c, ∀ᶠ (x : ℝ) in atTop, ‖x ^ (-↑k)‖ ≤ c * ‖x ^ s‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>f : 𝓢(E, F)<VAR>inst✝ : ProperSpace E<VAR>s : ℝ<VAR>k : ℕ := ⌈-s⌉₊<VAR>hk : -↑k ≤ s<VAR>x : ℝ<VAR>hx : 1 ≤ x<GOAL>‖x ^ (-↑k)‖ ≤ 1 * ‖x ^ s‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>f : 𝓢(E, F)<VAR>inst✝ : ProperSpace E<VAR>s : ℝ<VAR>k : ℕ := ⌈-s⌉₊<VAR>hk : -↑k ≤ s<VAR>x : ℝ<VAR>hx : 1 ≤ x<GOAL>x ^ (-↑k) ≤ x ^ s
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁✝ l₂✝ : List α<VAR>inst✝ : Inhabited α<VAR>l₁ l₂ : List α<VAR>n : ℕ<VAR>h : l₁.length = n<GOAL>takeI l₁.length (l₁ ++ l₂) = l₁
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝² : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>U V W X Y Z : C<GOAL>(α_ W X Y).inv ▷ Z ≫ (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom = (α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>G : Comonad C<VAR>X : G.Coalgebra<VAR>Y : C<VAR>f : G.forget.obj X ⟶ Y<GOAL>(X.a ≫ G.map f) ≫ G.ε.app Y = f
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>G : Comonad C<VAR>X : G.Coalgebra<VAR>Y : C<VAR>g : X ⟶ G.cofree.obj Y<GOAL>X.a ≫ G.map (g.f ≫ G.ε.app Y) = g.f
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>G : Comonad C<VAR>X : G.Coalgebra<VAR>Y : C<VAR>g : X ⟶ G.cofree.obj Y<GOAL>g.f ≫ 𝟙 (G.obj Y) = g.f
<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<GOAL>HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)
<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<VAR>this : HasSum (fun n => jacobiTheta₂_term n 0 τ) (jacobiTheta₂ 0 τ)<GOAL>HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)
<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<VAR>this : HasSum (fun n => cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)<GOAL>HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)
<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<VAR>this✝ : HasSum (fun n => cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)<VAR>this : HasSum (fun n => cexp (↑π * I * ↑↑n ^ 2 * τ) + cexp (↑π * I * ↑(-↑n) ^ 2 * τ)) (jacobiTheta τ + cexp (↑π * I * ↑0 ^ 2 * τ))<GOAL>HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)
<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<VAR>this✝ : HasSum (fun n => cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)<VAR>this : HasSum (fun n => cexp (↑π * I * ↑↑(n + 1) ^ 2 * τ) + cexp (↑π * I * ↑(-↑(n + 1)) ^ 2 * τ)) (jacobiTheta τ + cexp (↑π * I * ↑0 ^ 2 * τ) - ∑ i ∈ Finset.range 1, (cexp (↑π * I * ↑↑i ^ 2 * τ) + cexp (↑π * I * ↑(-↑i) ^ 2 * τ)))<GOAL>HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)
<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<VAR>this✝ : HasSum (fun n => cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)<VAR>this : HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * τ) * 2) (jacobiTheta τ - 1)<GOAL>HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)
<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<VAR>this✝ : HasSum (fun n => cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)<VAR>this : HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * τ) * 2) (jacobiTheta τ - 1)<GOAL>(fun n => cexp (↑π * I * (↑n + 1) ^ 2 * τ)) = fun i => cexp (↑π * I * (↑i + 1) ^ 2 * τ) * 2 / 2
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>s : Set G<VAR>t : Set P<VAR>a✝ : P<VAR>inst✝³ : PartialOrder G<VAR>inst✝² : PartialOrder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>x y : ↑(s.smulAntidiagonal t a✝)<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : P<GOAL>(s.smulAntidiagonal t a).Finite
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>s : Set G<VAR>t : Set P<VAR>a✝ : P<VAR>inst✝³ : PartialOrder G<VAR>inst✝² : PartialOrder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>x y : ↑(s.smulAntidiagonal t a✝)<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : P<VAR>h : (s.smulAntidiagonal t a).Infinite<GOAL>False
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>s : Set G<VAR>t : Set P<VAR>a✝ : P<VAR>inst✝³ : PartialOrder G<VAR>inst✝² : PartialOrder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>x y : ↑(s.smulAntidiagonal t a✝)<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : P<VAR>h : (s.smulAntidiagonal t a).Infinite<VAR>h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)<VAR>h2 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun x x_1 => x ≤ x_1)<GOAL>False
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>s : Set G<VAR>t : Set P<VAR>a✝ : P<VAR>inst✝³ : PartialOrder G<VAR>inst✝² : PartialOrder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>x y : ↑(s.smulAntidiagonal t a✝)<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : P<VAR>h : (s.smulAntidiagonal t a).Infinite<VAR>h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)<VAR>h2 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun x x_1 => x ≤ x_1)<VAR>isrfl : IsRefl (G × P) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)<GOAL>False
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>s : Set G<VAR>t : Set P<VAR>a✝ : P<VAR>inst✝³ : PartialOrder G<VAR>inst✝² : PartialOrder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>x y : ↑(s.smulAntidiagonal t a✝)<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : P<VAR>h : (s.smulAntidiagonal t a).Infinite<VAR>h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)<VAR>h2 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun x x_1 => x ≤ x_1)<VAR>isrfl : IsRefl (G × P) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)<VAR>istrns : IsTrans (G × P) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)<GOAL>False
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>s : Set G<VAR>t : Set P<VAR>a✝ : P<VAR>inst✝³ : PartialOrder G<VAR>inst✝² : PartialOrder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>x y : ↑(s.smulAntidiagonal t a✝)<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : P<VAR>h : (s.smulAntidiagonal t a).Infinite<VAR>h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)<VAR>h2 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun x x_1 => x ≤ x_1)<VAR>isrfl : IsRefl (G × P) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)<VAR>istrns : IsTrans (G × P) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)<VAR>g : ℕ ↪o ℕ<VAR>hg : ∀ (m n : ℕ), m ≤ n → (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1) ↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h) (g m)) ↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h) (g n))<GOAL>False
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>s : Set G<VAR>t : Set P<VAR>a✝ : P<VAR>inst✝³ : PartialOrder G<VAR>inst✝² : PartialOrder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>x y : ↑(s.smulAntidiagonal t a✝)<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : P<VAR>h : (s.smulAntidiagonal t a).Infinite<VAR>h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)<VAR>h2 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun x x_1 => x ≤ x_1)<VAR>isrfl : IsRefl (G × P) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)<VAR>istrns : IsTrans (G × P) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)<VAR>g : ℕ ↪o ℕ<VAR>hg : ∀ (m n : ℕ), m ≤ n → (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1) ↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h) (g m)) ↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h) (g n))<VAR>m n : ℕ<VAR>mn : m < n<VAR>h2' : (Prod.snd ⁻¹'o fun x x_1 => x ≤ x_1) ↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h) (g m)) ↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h) (g n))<GOAL>False