ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>inst✝²⁴ : Semifield R<VAR>inst✝²³ : StarRing R<VAR>inst✝²² : MetricSpace R<VAR>inst✝²¹ : TopologicalSemiring R<VAR>inst✝²⁰ : ContinuousStar R<VAR>inst✝¹⁹ : Field S<VAR>inst✝¹⁸ : StarRing S<VAR>inst✝¹⁷ : MetricSpace S<VAR>inst✝¹⁶ : TopologicalRing S<VAR>inst✝¹⁵ : ContinuousStar S<VAR>inst✝¹⁴ : TopologicalSpace A<VAR>inst✝¹³ : NonUnitalRing A<VAR>inst✝¹² : StarRing A<VAR>inst✝¹¹ : Module S A<VAR>inst✝¹⁰ : IsScalarTower S A A<VAR>inst✝⁹ : SMulCommClass S A A<VAR>inst✝⁸ : NonUnitalContinuousFunctionalCalculus S q<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Module R A<VAR>inst✝⁵ : IsScalarTower R S A<VAR>inst✝⁴ : StarModule R S<VAR>inst✝³ : ContinuousSMul R S<VAR>inst✝² : CompleteSpace R<VAR>inst✝¹ : IsScalarTower R A A<VAR>inst✝ : SMulCommClass R A A<VAR>f : C(S, R)<VAR>halg : UniformEmbedding ⇑(algebraMap R S)<VAR>h0 : p 0<VAR>h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f<VAR>h_cpct : ∀ (a : A), q a → CompactSpace ↑(σₙ S a)<VAR>a : A<VAR>ha : p a<GOAL>(nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯) { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := ⋯ } = a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>inst✝²⁴ : Semifield R<VAR>inst✝²³ : StarRing R<VAR>inst✝²² : MetricSpace R<VAR>inst✝²¹ : TopologicalSemiring R<VAR>inst✝²⁰ : ContinuousStar R<VAR>inst✝¹⁹ : Field S<VAR>inst✝¹⁸ : StarRing S<VAR>inst✝¹⁷ : MetricSpace S<VAR>inst✝¹⁶ : TopologicalRing S<VAR>inst✝¹⁵ : ContinuousStar S<VAR>inst✝¹⁴ : TopologicalSpace A<VAR>inst✝¹³ : NonUnitalRing A<VAR>inst✝¹² : StarRing A<VAR>inst✝¹¹ : Module S A<VAR>inst✝¹⁰ : IsScalarTower S A A<VAR>inst✝⁹ : SMulCommClass S A A<VAR>inst✝⁸ : NonUnitalContinuousFunctionalCalculus S q<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Module R A<VAR>inst✝⁵ : IsScalarTower R S A<VAR>inst✝⁴ : StarModule R S<VAR>inst✝³ : ContinuousSMul R S<VAR>inst✝² : CompleteSpace R<VAR>inst✝¹ : IsScalarTower R A A<VAR>inst✝ : SMulCommClass R A A<VAR>f : C(S, R)<VAR>halg : UniformEmbedding ⇑(algebraMap R S)<VAR>h0 : p 0<VAR>h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f<VAR>h_cpct : ∀ (a : A), q a → CompactSpace ↑(σₙ S a)<VAR>a : A<VAR>ha : p a<GOAL>∀ (f_1 : C(↑(σₙ R a), R)₀), σₙ R ((nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯) f_1) = range ⇑f_1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>inst✝²⁴ : Semifield R<VAR>inst✝²³ : StarRing R<VAR>inst✝²² : MetricSpace R<VAR>inst✝²¹ : TopologicalSemiring R<VAR>inst✝²⁰ : ContinuousStar R<VAR>inst✝¹⁹ : Field S<VAR>inst✝¹⁸ : StarRing S<VAR>inst✝¹⁷ : MetricSpace S<VAR>inst✝¹⁶ : TopologicalRing S<VAR>inst✝¹⁵ : ContinuousStar S<VAR>inst✝¹⁴ : TopologicalSpace A<VAR>inst✝¹³ : NonUnitalRing A<VAR>inst✝¹² : StarRing A<VAR>inst✝¹¹ : Module S A<VAR>inst✝¹⁰ : IsScalarTower S A A<VAR>inst✝⁹ : SMulCommClass S A A<VAR>inst✝⁸ : NonUnitalContinuousFunctionalCalculus S q<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Module R A<VAR>inst✝⁵ : IsScalarTower R S A<VAR>inst✝⁴ : StarModule R S<VAR>inst✝³ : ContinuousSMul R S<VAR>inst✝² : CompleteSpace R<VAR>inst✝¹ : IsScalarTower R A A<VAR>inst✝ : SMulCommClass R A A<VAR>f : C(S, R)<VAR>halg : UniformEmbedding ⇑(algebraMap R S)<VAR>h0 : p 0<VAR>h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f<VAR>h_cpct : ∀ (a : A), q a → CompactSpace ↑(σₙ S a)<VAR>a : A<VAR>ha : p a<GOAL>∀ (f_1 : C(↑(σₙ R a), R)₀), p ((nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯) f_1)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ t₁ t₂ : TopologicalSpace X<GOAL>t₁ = t₂ ↔ ∀ (s : Set X), IsClosed s ↔ IsClosed s
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ t₁ t₂ : TopologicalSpace X<GOAL>(∀ (x : Set X), IsOpen xᶜ ↔ IsOpen xᶜ) ↔ ∀ (s : Set X), IsClosed s ↔ IsClosed s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : AddCommMonoid M<VAR>w : σ → M<VAR>n : M<VAR>φ ψ : MvPolynomial σ R<VAR>h : ∀ d ∈ φ.support, (weight w) d ≠ n<GOAL>(weightedHomogeneousComponent w n) φ = 0
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : MonoidalCategory C<VAR>inst✝³ : Abelian C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasProjectiveResolutions C<VAR>X Y : C<VAR>inst✝ : Projective Y<VAR>n : ℕ<GOAL>IsZero (((Tor C (n + 1)).obj X).obj Y)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>V : Set (α × α)<GOAL>SymmetricRel (symmetrizeRel V)
<VAR>M : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero M<VAR>q : Associates M<VAR>n : ℕ<VAR>c : Fin (n + 1) → Associates M<VAR>h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i<VAR>m : Finset (Associates M)<VAR>hm : ∀ r ∈ m, r ≤ q<GOAL>m.card ≤ n + 1
<VAR>n : Type u_1<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>inst✝ : Fintype K<VAR>M : Matrix n n K<GOAL>(M ^ Fintype.card K).charpoly = M.charpoly
<VAR>n : Type u_1<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>inst✝ : Fintype K<VAR>M : Matrix n n K<VAR>h✝ : Nonempty n<GOAL>(M ^ Fintype.card K).charpoly = M.charpoly
<VAR>n : Type u_1<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>inst✝ : Fintype K<VAR>M : Matrix n n K<VAR>h✝ : IsEmpty n<GOAL>(M ^ Fintype.card K).charpoly = M.charpoly
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticForm R M<VAR>f : M →ₗ[R] N →ₗ[R] N<VAR>hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x<VAR>n : N<GOAL>((foldl Q f hf) n) 1 = n
<VAR>K : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : DivisionRing L<VAR>inst✝ : DivisionRing M<VAR>s : Set (Subfield K)<VAR>x : K<GOAL>x ∈ (sInf s).toSubring ↔ x ∈ ⨅ t ∈ s, t.toSubring
<VAR>K : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : DivisionRing L<VAR>inst✝ : DivisionRing M<VAR>s : Set (Subfield K)<VAR>x : K<GOAL>(∀ p ∈ s, x ∈ p) ↔ x ∈ ⨅ t ∈ s, t.toSubring
<VAR>K : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : DivisionRing L<VAR>inst✝ : DivisionRing M<VAR>s : Set (Subfield K)<VAR>x : K<GOAL>(∀ p ∈ s, x ∈ p) ↔ ∀ p ∈ Set.range fun t => ⨅ (_ : t ∈ s), t.toSubring, x ∈ p
<VAR>k✝ : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>A : Type u_4<VAR>G₁ : Type u_5<VAR>G₂ : Type u_6<VAR>G₃ : Type u_7<VAR>inst✝⁵ : CommSemiring k<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : Algebra k A<VAR>inst✝² : AddMonoid G₁<VAR>inst✝¹ : AddMonoid G₂<VAR>inst✝ : AddMonoid G₃<VAR>f : G₁ →+ G₂<VAR>g : G₂ →+ G₃<VAR>x✝ : A[G₁]<GOAL>(mapDomainAlgHom k A (g.comp f)) x✝ = ((mapDomainAlgHom k A g).comp (mapDomainAlgHom k A f)) x✝
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>x : E<GOAL>x +ᵥ r • closedBall 0 1 = closedBall x r
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝² : Category.{?u.51683, u_1} C<VAR>inst✝¹ : Category.{?u.51687, u_2} D<VAR>inst✝ : Category.{?u.51691, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>E✝ E'✝ : L.RightExtension F<VAR>Y : D<VAR>E E' : L.RightExtension F<VAR>φ : E ⟶ E'<VAR>G : StructuredArrow Y L<GOAL>φ.left.app Y ≫ E'.left.map G.hom ≫ E'.hom.app G.right = E.left.map G.hom ≫ E.hom.app G.right
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝² : Category.{?u.51683, u_1} C<VAR>inst✝¹ : Category.{?u.51687, u_2} D<VAR>inst✝ : Category.{?u.51691, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>E✝ E'✝ : L.RightExtension F<VAR>Y : D<VAR>E E' : L.RightExtension F<VAR>φ : E ⟶ E'<VAR>G : StructuredArrow Y L<GOAL>φ.left.app Y ≫ E'.left.map G.hom ≫ E'.hom.app G.right = E.left.map G.hom ≫ (((whiskeringLeft C D H).obj L).map φ.left ≫ E'.hom).app G.right
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<GOAL>PerfectSpace X ↔ ∀ (x : X), (𝓝[≠] x).NeBot
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝¹ : CompleteLattice α<VAR>f✝ g s✝ t : ι → α<VAR>a b : α<VAR>inst✝ : CompleteLattice β<VAR>f : α ≃o β<VAR>s : Set α<GOAL>f (sSup s) = sSup (⇑f.symm ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : Countable β<VAR>s : β → Set α<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (a : α) in ⋃ i, s i, f a ∂μ ≤ ∑' (i : β), ∫⁻ (a : α) in s i, f a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : Countable β<VAR>s : β → Set α<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (a : α) in ⋃ i, s i, f a ∂μ ≤ ∫⁻ (a : α), f a ∂sum fun i => μ.restrict (s i)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁵ : CommMonoid M<VAR>inst✝⁴ : CommMonoid N<VAR>inst✝³ : DivisionCommMonoid G<VAR>k✝ l : ℕ+<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsReduced R<VAR>p k : ℕ<VAR>m : ℕ+<VAR>inst✝ : ExpChar R p<VAR>ζ : Rˣ<GOAL>ζ ∈ rootsOfUnity (⟨p, ⋯⟩ ^ k * m) R ↔ ζ ∈ rootsOfUnity m R
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<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>f g : E → F<VAR>p✝¹ pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x✝ : E<VAR>r✝ r' : ℝ≥0∞<VAR>n✝ m : ℕ<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r R : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → p m = 0<VAR>k l : ℕ<VAR>s : Finset (Fin (k + l))<VAR>hs : s.card = l<VAR>hkl : n ≤ k + l<GOAL>p.changeOriginSeriesTerm k l s hs = 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>t✝ : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s t : Set α<VAR>hB : IsTopologicalBasis B<VAR>hs : IsOpen s<VAR>h : ∀ U ∈ B, U ⊆ s → U ⊆ t<GOAL>s ⊆ t
<VAR>α : Type u<VAR>β : Type u_1<VAR>t✝ : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s t : Set α<VAR>hB : IsTopologicalBasis B<VAR>hs : IsOpen s<VAR>h : ∀ U ∈ B, U ⊆ s → U ⊆ t<GOAL>⋃₀ {s_1 | s_1 ∈ B ∧ s_1 ⊆ s} ⊆ t
<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>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>x : E<VAR>hx : x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}<GOAL>x ∈ D f K
<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>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>x : E<VAR>hx : x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}<GOAL>∀ (i : ℕ), x ∈ ⋃ n, ⋂ p, ⋂ (_ : p ≥ n), ⋂ q, ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ i)
<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>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>x : E<VAR>hx : x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}<VAR>e : ℕ<VAR>this : 0 < (1 / 2) ^ e<GOAL>x ∈ ⋃ n, ⋂ p, ⋂ (_ : p ≥ n), ⋂ q, ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e)
<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>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>x : E<VAR>hx : x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}<VAR>e : ℕ<VAR>this : 0 < (1 / 2) ^ e<VAR>R : ℝ<VAR>R_pos : R > 0<VAR>hR : ∀ r ∈ Ioo 0 R, x ∈ A f (fderiv 𝕜 f x) r ((1 / 2) ^ e)<GOAL>x ∈ ⋃ n, ⋂ p, ⋂ (_ : p ≥ n), ⋂ q, ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e)
<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>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>x : E<VAR>hx : x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}<VAR>e : ℕ<VAR>this : 0 < (1 / 2) ^ e<VAR>R : ℝ<VAR>R_pos : R > 0<VAR>hR : ∀ r ∈ Ioo 0 R, x ∈ A f (fderiv 𝕜 f x) r ((1 / 2) ^ e)<VAR>n : ℕ<VAR>hn : (1 / 2) ^ n < R<GOAL>x ∈ ⋃ n, ⋂ p, ⋂ (_ : p ≥ n), ⋂ q, ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e)
<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>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>x : E<VAR>hx : x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}<VAR>e : ℕ<VAR>this : 0 < (1 / 2) ^ e<VAR>R : ℝ<VAR>R_pos : R > 0<VAR>hR : ∀ r ∈ Ioo 0 R, x ∈ A f (fderiv 𝕜 f x) r ((1 / 2) ^ e)<VAR>n : ℕ<VAR>hn : (1 / 2) ^ n < R<GOAL>∃ i, ∀ i_1 ≥ i, ∀ i_3 ≥ i, ∃ i, ∃ (_ : i ∈ K), x ∈ A f i ((1 / 2) ^ i_1) ((1 / 2) ^ e) ∧ x ∈ A f i ((1 / 2) ^ i_3) ((1 / 2) ^ e)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : PartialOrder M<VAR>v w : VectorMeasure α M<VAR>j : Set α<VAR>a✝ : MeasurableSet j<GOAL>↑(v.restrict ∅) j ≤ ↑(w.restrict ∅) j
<VAR>x y : ℝ<VAR>h : 0 ≤ x<GOAL>√(x ^ 2) = x
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>γ : ι → Type u_4<VAR>inst✝ : DecidableEq ι<VAR>f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)<VAR>a✝ : (i : ι) × α i<VAR>b✝ : (i : ι) × β i<VAR>h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b<VAR>a : (i : ι) × α i<VAR>b : (i : ι) × β i<VAR>x : Sigma γ<VAR>hx : x ∈ sigmaLift f a b<GOAL>x ∈ sigmaLift g a b
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>γ : ι → Type u_4<VAR>inst✝ : DecidableEq ι<VAR>f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)<VAR>a✝ : (i : ι) × α i<VAR>b✝ : (i : ι) × β i<VAR>h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b<VAR>a : (i : ι) × α i<VAR>b : (i : ι) × β i<VAR>x : Sigma γ<VAR>hx : ∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)<GOAL>∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ g (ha ▸ a.snd) (hb ▸ b.snd)
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s : Subgroup α<VAR>x y : α<GOAL>(∃ a, y * ↑a = x) ↔ ∃ a, x⁻¹ * y = ↑a⁻¹
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s : Subgroup α<VAR>x y : α<GOAL>(∃ a, x⁻¹ * y = ↑a⁻¹) ↔ x⁻¹ * y ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f g : ↥(Lp β 1 μ)<GOAL>‖f - g‖ = (∫⁻ (x : α), ↑‖↑↑f x - ↑↑g x‖₊ ∂μ).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f g : ↥(Lp β 1 μ)<GOAL>(∫⁻ (a : α), ↑‖↑↑(f - g) a‖₊ ∂μ).toReal = (∫⁻ (x : α), ↑‖↑↑f x - ↑↑g x‖₊ ∂μ).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f g : ↥(Lp β 1 μ)<GOAL>∫⁻ (a : α), ↑‖↑↑(f - g) a‖₊ ∂μ = ∫⁻ (x : α), ↑‖↑↑f x - ↑↑g x‖₊ ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f g : ↥(Lp β 1 μ)<GOAL>(fun a => ↑‖↑↑(f - g) a‖₊) =ᶠ[ae μ] fun a => ↑‖↑↑f a - ↑↑g a‖₊
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f g : ↥(Lp β 1 μ)<VAR>a✝ : α<VAR>ha : ↑↑(f - g) a✝ = (↑↑f - ↑↑g) a✝<GOAL>↑‖↑↑(f - g) a✝‖₊ = ↑‖↑↑f a✝ - ↑↑g a✝‖₊
<VAR>a b : ℤ<VAR>h : a < b<GOAL>↑(Fintype.card ↑(Set.Ioo a b)) = b - a - 1
<VAR>α : Type u_1<VAR>inst✝ : AddCommGroup α<VAR>p a a₁ a₂ b b₁ b₂ c : α<VAR>n✝ : ℕ<VAR>z : ℤ<VAR>n : ℕ<GOAL>a - (n • p + a) = -↑n • p
<VAR>R : Type u_1<VAR>inst✝⁷ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁶ : CommSemiring S<VAR>inst✝⁵ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁴ : CommSemiring P<VAR>inst✝³ : IsLocalization M S<VAR>g : R →+* P<VAR>hg : ∀ (y : ↥M), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>Q : Type u_4<VAR>inst✝² : CommSemiring Q<VAR>hy : M ≤ Submonoid.comap g T<VAR>inst✝¹ : Algebra P Q<VAR>inst✝ : IsLocalization T Q<VAR>j : R ≃+* P<VAR>H : Submonoid.map j.toMonoidHom M = T<VAR>x : R<VAR>y : ↥M<GOAL>(ringEquivOfRingEquiv S Q j H) (mk' S x y) = mk' Q (j x) ⟨j ↑y, ⋯⟩
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>a b : R<VAR>H : (C R) a = (C R) b<GOAL>a = b
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>a b : R<VAR>H : (C R) a = (C R) b<VAR>this : (coeff R 0) ((C R) a) = (coeff R 0) ((C R) b)<GOAL>a = b
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝¹ : DecidableEq o<VAR>inst✝ : AddZeroClass α<VAR>M N : (i : o) → Matrix (m' i) (n' i) α<VAR>i✝ : (i : o) × m' i<VAR>j✝ : (i : o) × n' i<GOAL>blockDiagonal' (M + N) i✝ j✝ = (blockDiagonal' M + blockDiagonal' N) i✝ j✝
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝¹ : DecidableEq o<VAR>inst✝ : AddZeroClass α<VAR>M N : (i : o) → Matrix (m' i) (n' i) α<VAR>i✝ : (i : o) × m' i<VAR>j✝ : (i : o) × n' i<GOAL>(if h : i✝.fst = j✝.fst then M i✝.fst i✝.snd (cast ⋯ j✝.snd) + N i✝.fst i✝.snd (cast ⋯ j✝.snd) else 0) = (if h : i✝.fst = j✝.fst then M i✝.fst i✝.snd (cast ⋯ j✝.snd) else 0) + if h : i✝.fst = j✝.fst then N i✝.fst i✝.snd (cast ⋯ j✝.snd) else 0
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>i k : ι<VAR>inst✝ : K.HasHomology i<VAR>h : K.d i (c.next i) = 0<GOAL>IsIso (K.iCycles i)
<VAR>f✝ f : ℝ → ℝ<VAR>hf : GrowsPolynomially f<GOAL>GrowsPolynomially fun x => (f x)⁻¹
<VAR>f : StieltjesFunction<VAR>l : ℝ<VAR>hf : Tendsto (↑f) atTop (𝓝 l)<VAR>x : ℝ<GOAL>f.measure (Ici x) = ofReal (l - leftLim (↑f) x)
<VAR>f : StieltjesFunction<VAR>l : ℝ<VAR>hf : Tendsto (↑f) atTop (𝓝 l)<VAR>x : ℝ<GOAL>Tendsto (fun x_1 => f.measure (Ico x x_1)) atTop (𝓝 (ofReal (l - leftLim (↑f) x)))
<VAR>f : StieltjesFunction<VAR>l : ℝ<VAR>hf : Tendsto (↑f) atTop (𝓝 l)<VAR>x : ℝ<GOAL>Tendsto (fun x_1 => ofReal (leftLim (↑f) x_1 - leftLim (↑f) x)) atTop (𝓝 (ofReal (l - leftLim (↑f) x)))
<VAR>f : StieltjesFunction<VAR>l : ℝ<VAR>hf : Tendsto (↑f) atTop (𝓝 l)<VAR>x : ℝ<GOAL>Tendsto (leftLim ↑f) atTop (𝓝 l)
<VAR>f : StieltjesFunction<VAR>l : ℝ<VAR>hf : Tendsto (↑f) atTop (𝓝 l)<VAR>x : ℝ<VAR>h_le1 : ∀ (x : ℝ), ↑f (x - 1) ≤ leftLim (↑f) x<GOAL>Tendsto (leftLim ↑f) atTop (𝓝 l)
<VAR>f : StieltjesFunction<VAR>l : ℝ<VAR>hf : Tendsto (↑f) atTop (𝓝 l)<VAR>x : ℝ<VAR>h_le1 : ∀ (x : ℝ), ↑f (x - 1) ≤ leftLim (↑f) x<VAR>h_le2 : ∀ (x : ℝ), leftLim (↑f) x ≤ ↑f x<GOAL>Tendsto (leftLim ↑f) atTop (𝓝 l)
<VAR>f : StieltjesFunction<VAR>l : ℝ<VAR>hf : Tendsto (↑f) atTop (𝓝 l)<VAR>x : ℝ<VAR>h_le1 : ∀ (x : ℝ), ↑f (x - 1) ≤ leftLim (↑f) x<VAR>h_le2 : ∀ (x : ℝ), leftLim (↑f) x ≤ ↑f x<GOAL>Tendsto (fun i => i - 1) atTop atTop
<VAR>f : StieltjesFunction<VAR>l : ℝ<VAR>hf : Tendsto (↑f) atTop (𝓝 l)<VAR>x : ℝ<VAR>h_le1 : ∀ (x : ℝ), ↑f (x - 1) ≤ leftLim (↑f) x<VAR>h_le2 : ∀ (x : ℝ), leftLim (↑f) x ≤ ↑f x<GOAL>∀ (b : ℝ), ∃ i, ∀ (a : ℝ), i ≤ a → b ≤ a - 1
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>x : α<VAR>V : Set (α × α)<VAR>V_in : V ∈ 𝓤 α<GOAL>ball x V ∈ 𝓝 x
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>x : α<VAR>V : Set (α × α)<VAR>V_in : V ∈ 𝓤 α<GOAL>∃ V_1 ∈ 𝓤 α, ball x V_1 ⊆ ball x V
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : PartialOrder α<VAR>a b c d : α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : PosMulStrictMono α<VAR>inst✝¹ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>ha : a < 0<VAR>h : 1 < b<GOAL>a * b < a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : InnerProductSpace ℝ H<VAR>s t : Set H<VAR>K : ConvexCone ℝ H<VAR>hc : IsClosed ↑K<VAR>x : H<VAR>hx : x ∈ ↑K<VAR>f : ℝ → H := fun x_1 => x_1 • x<GOAL>K.Pointed
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : InnerProductSpace ℝ H<VAR>s t : Set H<VAR>K : ConvexCone ℝ H<VAR>hc : IsClosed ↑K<VAR>x : H<VAR>hx : x ∈ ↑K<VAR>f : ℝ → H := fun x_1 => x_1 • x<VAR>fI : f '' Ioi 0 ⊆ ↑K<GOAL>K.Pointed
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : InnerProductSpace ℝ H<VAR>s t : Set H<VAR>K : ConvexCone ℝ H<VAR>hc : IsClosed ↑K<VAR>x : H<VAR>hx : x ∈ ↑K<VAR>f : ℝ → H := fun x_1 => x_1 • x<VAR>fI : f '' Ioi 0 ⊆ ↑K<VAR>clf : closure (f '' Ioi 0) ⊆ ↑K<GOAL>K.Pointed
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : InnerProductSpace ℝ H<VAR>s t : Set H<VAR>K : ConvexCone ℝ H<VAR>hc : IsClosed ↑K<VAR>x : H<VAR>hx : x ∈ ↑K<VAR>f : ℝ → H := fun x_1 => x_1 • x<VAR>fI : f '' Ioi 0 ⊆ ↑K<VAR>clf : closure (f '' Ioi 0) ⊆ ↑K<VAR>fc : ContinuousWithinAt f (Ioi 0) 0<GOAL>K.Pointed
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : InnerProductSpace ℝ H<VAR>s t : Set H<VAR>K : ConvexCone ℝ H<VAR>hc : IsClosed ↑K<VAR>x : H<VAR>hx : x ∈ ↑K<VAR>f : ℝ → H := fun x_1 => x_1 • x<VAR>fI : f '' Ioi 0 ⊆ ↑K<VAR>clf : closure (f '' Ioi 0) ⊆ ↑K<VAR>fc : ContinuousWithinAt f (Ioi 0) 0<VAR>mem₀ : f 0 ∈ closure (f '' Ioi 0)<GOAL>K.Pointed
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : InnerProductSpace ℝ H<VAR>s t : Set H<VAR>K : ConvexCone ℝ H<VAR>hc : IsClosed ↑K<VAR>x : H<VAR>hx : x ∈ ↑K<VAR>f : ℝ → H := fun x_1 => x_1 • x<VAR>fI : f '' Ioi 0 ⊆ ↑K<VAR>clf : closure (f '' Ioi 0) ⊆ ↑K<VAR>fc : ContinuousWithinAt f (Ioi 0) 0<VAR>mem₀ : f 0 ∈ closure (f '' Ioi 0)<VAR>f₀ : f 0 = 0<GOAL>K.Pointed
<VAR>R : Type u_1<VAR>inst✝¹ : NormedCommRing R<VAR>inst✝ : CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : Summable f<VAR>hf₀ : f 0 = 0<VAR>ε : ℝ<VAR>εpos : 0 < ε<GOAL>∃ N, ∀ (s : Finset ℕ), N.primesBelow ≤ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε
<VAR>R : Type u_1<VAR>inst✝¹ : NormedCommRing R<VAR>inst✝ : CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : Summable f<VAR>hf₀ : f 0 = 0<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>N : ℕ<VAR>hN : ∀ t ⊆ {n | N ≤ n}, ∑' (n : ↑t), f ↑n ∈ Metric.ball 0 ε<GOAL>∃ N, ∀ (s : Finset ℕ), N.primesBelow ≤ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε
<VAR>R : Type u_1<VAR>inst✝¹ : NormedCommRing R<VAR>inst✝ : CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : Summable f<VAR>hf₀ : f 0 = 0<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>N : ℕ<VAR>hN : ∀ t ⊆ {n | N ≤ n}, ‖∑' (n : ↑t), f ↑n‖ < ε<GOAL>∃ N, ∀ (s : Finset ℕ), N.primesBelow ≤ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε