ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<GOAL>vanishingIdeal '' {s | IsClosed s ∧ IsIrreducible s} ⊆ vanishingIdeal '' {s | IsIrreducible s}
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<GOAL>vanishingIdeal '' {s | IsIrreducible s} ⊆ vanishingIdeal '' {s | IsClosed s ∧ IsIrreducible s}
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>s : Set (PrimeSpectrum R)<VAR>hs : s ∈ {s | IsIrreducible s}<GOAL>vanishingIdeal s ∈ vanishingIdeal '' {s | IsClosed s ∧ IsIrreducible s}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>f : Filtration ℕ m<VAR>u : ℕ → Ω → β<VAR>τ π : Ω → ℕ<VAR>inst✝ : AddCommGroup β<VAR>hle : τ ≤ π<VAR>ω : Ω<GOAL>(stoppedValue u π - stoppedValue u τ) ω = (∑ i ∈ Finset.Ico (τ ω) (π ω), (u (i + 1) - u i)) ω
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>f : Filtration ℕ m<VAR>u : ℕ → Ω → β<VAR>τ π : Ω → ℕ<VAR>inst✝ : AddCommGroup β<VAR>hle : τ ≤ π<VAR>ω : Ω<GOAL>(stoppedValue u π - stoppedValue u τ) ω = (u (π ω) - u 0 - (u (τ ω) - u 0)) ω
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasZeroObject C<VAR>ι : Type u_1<VAR>inst✝ : DecidableEq ι<VAR>c : ComplexShape ι<VAR>j : ι<VAR>A B : C<VAR>f : A ⟶ B<GOAL>opcyclesMap ((single C c j).map f) j ≫ (singleObjOpcyclesSelfIso c j B).inv = (singleObjOpcyclesSelfIso c j A).inv ≫ f
<VAR>ξ : ℝ<VAR>n : ℕ<VAR>n_pos : 0 < n<VAR>f : ℤ → ℤ := fun m => ⌊fract (ξ * ↑m) * (↑n + 1)⌋<GOAL>∃ j k, 0 < k ∧ k ≤ ↑n ∧ |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
<VAR>ξ : ℝ<VAR>n : ℕ<VAR>n_pos : 0 < n<VAR>f : ℤ → ℤ := fun m => ⌊fract (ξ * ↑m) * (↑n + 1)⌋<VAR>hn : 0 < ↑n + 1<GOAL>∃ j k, 0 < k ∧ k ≤ ↑n ∧ |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
<VAR>ξ : ℝ<VAR>n : ℕ<VAR>n_pos : 0 < n<VAR>f : ℤ → ℤ := fun m => ⌊fract (ξ * ↑m) * (↑n + 1)⌋<VAR>hn : 0 < ↑n + 1<VAR>hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1<GOAL>∃ j k, 0 < k ∧ k ≤ ↑n ∧ |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
<VAR>ξ : ℝ<VAR>n : ℕ<VAR>n_pos : 0 < n<VAR>f : ℤ → ℤ := fun m => ⌊fract (ξ * ↑m) * (↑n + 1)⌋<VAR>hn : 0 < ↑n + 1<VAR>hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1<GOAL>∃ j k, 0 < k ∧ k ≤ ↑n ∧ |(ξ * ↑k - ↑j) * (↑n + 1)| ≤ 1
<VAR>R : Type u_1<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : TopologicalSpace R<VAR>inst✝⁵ : TopologicalSemiring R<VAR>A : Type u_2<VAR>inst✝⁴ : StarRing R<VAR>inst✝³ : ContinuousStar R<VAR>inst✝² : Semiring A<VAR>inst✝¹ : StarRing A<VAR>inst✝ : Algebra R A<VAR>s : Set R<VAR>φ ψ : C(↑s, R) →⋆ₐ[R] A<VAR>h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)<GOAL>(polynomialFunctions s).starClosure ≤ StarAlgHom.equalizer φ ψ
<VAR>R : Type u_1<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : TopologicalSpace R<VAR>inst✝⁵ : TopologicalSemiring R<VAR>A : Type u_2<VAR>inst✝⁴ : StarRing R<VAR>inst✝³ : ContinuousStar R<VAR>inst✝² : Semiring A<VAR>inst✝¹ : StarRing A<VAR>inst✝ : Algebra R A<VAR>s : Set R<VAR>φ ψ : C(↑s, R) →⋆ₐ[R] A<VAR>h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)<GOAL>adjoin R {(toContinuousMapOnAlgHom s) X} ≤ StarAlgHom.equalizer φ ψ
<VAR>n✝ : ℕ<VAR>c : Composition n✝<VAR>n : ℕ<VAR>i : Fin (ones n).length<GOAL>(ones n).blocksFun i = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq β<VAR>f g : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<VAR>b c : β<VAR>h : Set.EqOn f g ↑s<VAR>a✝ : β<GOAL>a✝ ∈ image f s ↔ a✝ ∈ image g s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq β<VAR>f g : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<VAR>b c : β<VAR>h : Set.EqOn f g ↑s<VAR>a✝ : β<GOAL>(∃ x, ∃ (_ : x ∈ s), f x = a✝) ↔ ∃ x, ∃ (_ : x ∈ s), g x = a✝
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G₀ : Type u_4<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : GroupWithZero G₀<VAR>inst✝⁷ : MulAction G₀ α<VAR>inst✝⁶ : ContinuousConstSMul G₀ α<VAR>inst✝⁵ : TopologicalSpace β<VAR>f : β → α<VAR>b : β<VAR>c✝ : G₀<VAR>s✝ : Set β<VAR>E : Type u_5<VAR>inst✝⁴ : Zero E<VAR>inst✝³ : MulActionWithZero G₀ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : T1Space E<VAR>inst✝ : ContinuousConstSMul G₀ E<VAR>c : G₀<VAR>s : Set E<GOAL>closure (c • s) = c • closure s
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G₀ : Type u_4<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : GroupWithZero G₀<VAR>inst✝⁷ : MulAction G₀ α<VAR>inst✝⁶ : ContinuousConstSMul G₀ α<VAR>inst✝⁵ : TopologicalSpace β<VAR>f : β → α<VAR>b : β<VAR>c : G₀<VAR>s✝ : Set β<VAR>E : Type u_5<VAR>inst✝⁴ : Zero E<VAR>inst✝³ : MulActionWithZero G₀ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : T1Space E<VAR>inst✝ : ContinuousConstSMul G₀ E<VAR>s : Set E<GOAL>closure (0 • s) = 0 • closure s
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G₀ : Type u_4<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : GroupWithZero G₀<VAR>inst✝⁷ : MulAction G₀ α<VAR>inst✝⁶ : ContinuousConstSMul G₀ α<VAR>inst✝⁵ : TopologicalSpace β<VAR>f : β → α<VAR>b : β<VAR>c✝ : G₀<VAR>s✝ : Set β<VAR>E : Type u_5<VAR>inst✝⁴ : Zero E<VAR>inst✝³ : MulActionWithZero G₀ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : T1Space E<VAR>inst✝ : ContinuousConstSMul G₀ E<VAR>c : G₀<VAR>s : Set E<VAR>hc : c ≠ 0<GOAL>closure (c • s) = c • closure s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t✝ : Set α<VAR>s : Finset ι<VAR>t : ι → Set α<VAR>h : ∀ i ∈ s, NullMeasurableSet (t i) μ<VAR>H : (↑s).Pairwise (AEDisjoint μ on t)<GOAL>∑ i ∈ s, μ (t i) ≤ μ univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t✝ : Set α<VAR>s : Finset ι<VAR>t : ι → Set α<VAR>h : ∀ i ∈ s, NullMeasurableSet (t i) μ<VAR>H : (↑s).Pairwise (AEDisjoint μ on t)<GOAL>μ (⋃ b ∈ s, t b) ≤ μ univ
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>e : S<VAR>he : e ∈ f.range<VAR>he' : IsIdempotentElem e<GOAL>∃ e', IsIdempotentElem e' ∧ f e' = e
<VAR>d : ℕ<VAR>a : ℤ√↑d<GOAL>∃ n, a ≤ ↑n
<VAR>d : ℕ<VAR>a : ℤ√↑d<VAR>x y : ℕ<VAR>h : a ≤ { re := ↑x, im := ↑y }<GOAL>∃ n, a ≤ ↑n
<VAR>d : ℕ<VAR>a : ℤ√↑d<VAR>x y : ℕ<VAR>h : a ≤ { re := ↑x, im := ↑(y + 1) }<GOAL>{ re := ↑x + ↑d * ↑(y + 1) - ↑x, im := 0 - ↑(y + 1) }.Nonneg
<VAR>d : ℕ<VAR>a : ℤ√↑d<VAR>x y : ℕ<VAR>h✝ : a ≤ { re := ↑x, im := ↑(y + 1) }<VAR>h : ∀ (y : ℕ), SqLe y d (d * y) 1<GOAL>{ re := ↑x + ↑d * ↑(y + 1) - ↑x, im := 0 - ↑(y + 1) }.Nonneg
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝²⁹ : CommRing A<VAR>inst✝²⁸ : CommRing B<VAR>inst✝²⁷ : Algebra A B<VAR>inst✝²⁶ : Field K<VAR>inst✝²⁵ : Field L<VAR>inst✝²⁴ : Algebra A K<VAR>inst✝²³ : IsFractionRing A K<VAR>inst✝²² : Algebra B L<VAR>inst✝²¹ : Algebra K L<VAR>inst✝²⁰ : Algebra A L<VAR>inst✝¹⁹ : IsScalarTower A B L<VAR>inst✝¹⁸ : IsScalarTower A K L<VAR>inst✝¹⁷ : IsIntegralClosure B A L<VAR>inst✝¹⁶ : FiniteDimensional K L<VAR>Aₘ : Type ?u.292784<VAR>Bₘ : Type ?u.292787<VAR>inst✝¹⁵ : CommRing Aₘ<VAR>inst✝¹⁴ : CommRing Bₘ<VAR>inst✝¹³ : Algebra Aₘ Bₘ<VAR>inst✝¹² : Algebra A Aₘ<VAR>inst✝¹¹ : Algebra B Bₘ<VAR>inst✝¹⁰ : Algebra A Bₘ<VAR>inst✝⁹ : IsScalarTower A Aₘ Bₘ<VAR>inst✝⁸ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁷ : IsLocalization M Aₘ<VAR>inst✝⁶ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁵ : IsDomain A<VAR>inst✝⁴ : IsIntegrallyClosed A<VAR>inst✝³ : IsDomain B<VAR>inst✝² : IsIntegrallyClosed B<VAR>inst✝¹ : Module.Finite A B<VAR>inst✝ : NoZeroSMulDivisors A B<VAR>x : B<VAR>this : IsIntegralClosure B A (FractionRing B)<GOAL>(algebraMap A (FractionRing A)) ((intTrace A B) x) = (trace (FractionRing A) (FractionRing B)) ((algebraMap B (FractionRing B)) x)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝²⁹ : CommRing A<VAR>inst✝²⁸ : CommRing B<VAR>inst✝²⁷ : Algebra A B<VAR>inst✝²⁶ : Field K<VAR>inst✝²⁵ : Field L<VAR>inst✝²⁴ : Algebra A K<VAR>inst✝²³ : IsFractionRing A K<VAR>inst✝²² : Algebra B L<VAR>inst✝²¹ : Algebra K L<VAR>inst✝²⁰ : Algebra A L<VAR>inst✝¹⁹ : IsScalarTower A B L<VAR>inst✝¹⁸ : IsScalarTower A K L<VAR>inst✝¹⁷ : IsIntegralClosure B A L<VAR>inst✝¹⁶ : FiniteDimensional K L<VAR>Aₘ : Type ?u.292784<VAR>Bₘ : Type ?u.292787<VAR>inst✝¹⁵ : CommRing Aₘ<VAR>inst✝¹⁴ : CommRing Bₘ<VAR>inst✝¹³ : Algebra Aₘ Bₘ<VAR>inst✝¹² : Algebra A Aₘ<VAR>inst✝¹¹ : Algebra B Bₘ<VAR>inst✝¹⁰ : Algebra A Bₘ<VAR>inst✝⁹ : IsScalarTower A Aₘ Bₘ<VAR>inst✝⁸ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁷ : IsLocalization M Aₘ<VAR>inst✝⁶ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁵ : IsDomain A<VAR>inst✝⁴ : IsIntegrallyClosed A<VAR>inst✝³ : IsDomain B<VAR>inst✝² : IsIntegrallyClosed B<VAR>inst✝¹ : Module.Finite A B<VAR>inst✝ : NoZeroSMulDivisors A B<VAR>x : B<VAR>this✝ : IsIntegralClosure B A (FractionRing B)<VAR>this : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<GOAL>(algebraMap A (FractionRing A)) ((intTrace A B) x) = (trace (FractionRing A) (FractionRing B)) ((algebraMap B (FractionRing B)) x)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝²⁹ : CommRing A<VAR>inst✝²⁸ : CommRing B<VAR>inst✝²⁷ : Algebra A B<VAR>inst✝²⁶ : Field K<VAR>inst✝²⁵ : Field L<VAR>inst✝²⁴ : Algebra A K<VAR>inst✝²³ : IsFractionRing A K<VAR>inst✝²² : Algebra B L<VAR>inst✝²¹ : Algebra K L<VAR>inst✝²⁰ : Algebra A L<VAR>inst✝¹⁹ : IsScalarTower A B L<VAR>inst✝¹⁸ : IsScalarTower A K L<VAR>inst✝¹⁷ : IsIntegralClosure B A L<VAR>inst✝¹⁶ : FiniteDimensional K L<VAR>Aₘ : Type ?u.292784<VAR>Bₘ : Type ?u.292787<VAR>inst✝¹⁵ : CommRing Aₘ<VAR>inst✝¹⁴ : CommRing Bₘ<VAR>inst✝¹³ : Algebra Aₘ Bₘ<VAR>inst✝¹² : Algebra A Aₘ<VAR>inst✝¹¹ : Algebra B Bₘ<VAR>inst✝¹⁰ : Algebra A Bₘ<VAR>inst✝⁹ : IsScalarTower A Aₘ Bₘ<VAR>inst✝⁸ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁷ : IsLocalization M Aₘ<VAR>inst✝⁶ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁵ : IsDomain A<VAR>inst✝⁴ : IsIntegrallyClosed A<VAR>inst✝³ : IsDomain B<VAR>inst✝² : IsIntegrallyClosed B<VAR>inst✝¹ : Module.Finite A B<VAR>inst✝ : NoZeroSMulDivisors A B<VAR>x : B<VAR>this✝¹ : IsIntegralClosure B A (FractionRing B)<VAR>this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<VAR>this : FiniteDimensional (FractionRing A) (FractionRing B)<GOAL>(algebraMap A (FractionRing A)) ((intTrace A B) x) = (trace (FractionRing A) (FractionRing B)) ((algebraMap B (FractionRing B)) x)
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>ι : Sort u_5<VAR>x : α<VAR>s : ι → Opens α<GOAL>x ∈ iSup s ↔ ∃ i, x ∈ s i
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>ι : Sort u_5<VAR>x : α<VAR>s : ι → Opens α<GOAL>x ∈ ↑(iSup s) ↔ ∃ i, x ∈ s 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>α : Type u_5<VAR>m : MeasurableSpace α<VAR>inst✝¹ : CountablyGenerated α<VAR>inst✝ : MeasurableSpace.SeparatesPoints α<GOAL>∃ τ, SecondCountableTopology α ∧ T4Space α ∧ BorelSpace α
<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>α : Type u_5<VAR>m : MeasurableSpace α<VAR>inst✝¹ : CountablyGenerated α<VAR>inst✝ : MeasurableSpace.SeparatesPoints α<VAR>s : Set (ℕ → Bool)<VAR>f : α ≃ᵐ ↑s<GOAL>∃ τ, SecondCountableTopology α ∧ T4Space α ∧ BorelSpace α
<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>α : Type u_5<VAR>m : MeasurableSpace α<VAR>inst✝¹ : CountablyGenerated α<VAR>inst✝ : MeasurableSpace.SeparatesPoints α<VAR>s : Set (ℕ → Bool)<VAR>f : α ≃ᵐ ↑s<VAR>this : TopologicalSpace α := induced (⇑f) inferInstance<GOAL>∃ τ, SecondCountableTopology α ∧ T4Space α ∧ BorelSpace α
<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>α : Type u_5<VAR>m : MeasurableSpace α<VAR>inst✝¹ : CountablyGenerated α<VAR>inst✝ : MeasurableSpace.SeparatesPoints α<VAR>s : Set (ℕ → Bool)<VAR>f : α ≃ᵐ ↑s<VAR>this : TopologicalSpace α := induced (⇑f) inferInstance<VAR>F : α ≃ₜ ↑s := f.toHomeomorphOfInducing ⋯<GOAL>∃ τ, SecondCountableTopology α ∧ T4Space α ∧ BorelSpace α
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝¹ p✝ q : R[X]<VAR>ι : Type u_1<VAR>n : ℕ<VAR>p : AddMonoidAlgebra R ℕ<GOAL>(erase n { toFinsupp := p }).degree ≤ { toFinsupp := p }.degree
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝¹ p✝ q : R[X]<VAR>ι : Type u_1<VAR>n : ℕ<VAR>p : AddMonoidAlgebra R ℕ<GOAL>(Finsupp.erase n p).support.max ≤ p.support.max
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝¹ p✝ q : R[X]<VAR>ι : Type u_1<VAR>n : ℕ<VAR>p : AddMonoidAlgebra R ℕ<GOAL>(Finsupp.erase n p).support ⊆ p.support
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝¹ p✝ q : R[X]<VAR>ι : Type u_1<VAR>n : ℕ<VAR>p : AddMonoidAlgebra R ℕ<GOAL>p.support.erase n ⊆ p.support
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c d : ℝ<VAR>r : ℂ<VAR>h : 0 ≤ r.re ∨ 0 ∉ [[a, b]]<VAR>h2 : ¬0 ∉ [[a, b]]<GOAL>IntervalIntegrable (fun x => ↑x ^ r) μ a b
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c d : ℝ<VAR>r : ℂ<VAR>h : 0 ≤ r.re<VAR>h2 : ¬0 ∉ [[a, b]]<GOAL>IntervalIntegrable (fun x => ↑x ^ r) μ a b
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c d : ℝ<VAR>r : ℂ<VAR>h : 0 ≤ r.re<VAR>h2 : ¬0 ∉ [[a, b]]<VAR>h' : 0 < r.re<GOAL>IntervalIntegrable (fun x => ↑x ^ r) μ a b
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c d : ℝ<VAR>r : ℂ<VAR>h : 0 ≤ r.re<VAR>h2 : ¬0 ∉ [[a, b]]<VAR>h' : 0 = r.re<GOAL>IntervalIntegrable (fun x => ↑x ^ r) μ a b
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c d : ℝ<VAR>r : ℂ<VAR>h : 0 ≤ r.re<VAR>h2 : ¬0 ∉ [[a, b]]<VAR>h' : 0 = r.re<GOAL>AEStronglyMeasurable (fun x => ↑x ^ r) (μ.restrict (Ι a b))
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c d : ℝ<VAR>r : ℂ<VAR>h : 0 ≤ r.re<VAR>h2 : ¬0 ∉ [[a, b]]<VAR>h' : 0 = r.re<GOAL>IntervalIntegrable (fun t => ‖↑t ^ r‖) μ a b
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c d : ℝ<VAR>r : ℂ<VAR>h : 0 ≤ r.re<VAR>h2 : ¬0 ∉ [[a, b]]<VAR>h' : 0 = r.re<GOAL>∀ (c : ℝ), IntervalIntegrable (fun x => ‖↑x ^ r‖) μ 0 c
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c✝ d : ℝ<VAR>r : ℂ<VAR>h : 0 ≤ r.re<VAR>h2 : ¬0 ∉ [[a, b]]<VAR>h' : 0 = r.re<VAR>c : ℝ<GOAL>IntervalIntegrable (fun x => ‖↑x ^ r‖) μ 0 c
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c✝ d : ℝ<VAR>r : ℂ<VAR>h : 0 ≤ r.re<VAR>h2 : ¬0 ∉ [[a, b]]<VAR>h' : 0 = r.re<VAR>c : ℝ<VAR>hc : 0 ≤ c<GOAL>IntervalIntegrable (fun x => ‖↑x ^ r‖) μ 0 c
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c✝ d : ℝ<VAR>r : ℂ<VAR>h : 0 ≤ r.re<VAR>h2 : ¬0 ∉ [[a, b]]<VAR>h' : 0 = r.re<VAR>c : ℝ<VAR>hc : c < 0<GOAL>IntervalIntegrable (fun x => ‖↑x ^ r‖) μ 0 c
<VAR>C : Type u_1<VAR>inst✝³ : Category.{?u.9007, u_1} C<VAR>J : Type u_2<VAR>inst✝² : Countable J<VAR>inst✝¹ : Preorder J<VAR>inst✝ : IsCofiltered J<VAR>j : J<GOAL>∃ n, sequentialFunctor_obj J n ≤ j
<VAR>C : Type u_1<VAR>inst✝³ : Category.{?u.9007, u_1} C<VAR>J : Type u_2<VAR>inst✝² : Countable J<VAR>inst✝¹ : Preorder J<VAR>inst✝ : IsCofiltered J<VAR>j : J<VAR>m : ℕ<VAR>h : ⋯.choose m = j<GOAL>∃ n, sequentialFunctor_obj J n ≤ j
<VAR>C : Type u_1<VAR>inst✝³ : Category.{?u.9007, u_1} C<VAR>J : Type u_2<VAR>inst✝² : Countable J<VAR>inst✝¹ : Preorder J<VAR>inst✝ : IsCofiltered J<VAR>j : J<VAR>m : ℕ<VAR>h : ⋯.choose m = j<GOAL>sequentialFunctor_obj J (m + 1) ≤ j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝¹ : Preorder α<VAR>inst✝ : SupSet α<VAR>f : ι → α<VAR>h : BddAbove (range f)<GOAL>↑(⨆ i, f i) = ⨆ i, ↑(f i)
<VAR>α : Type u_1<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>n : ℕ<GOAL>(↑n).toNNReal = ↑n
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>l : Filter β<VAR>f₁ f₂ f₃ : β → α<VAR>h₁₂ : Tendsto (fun x => (f₁ x, f₂ x)) l (𝓤 α)<VAR>h₂₃ : Tendsto (fun x => (f₂ x, f₃ x)) l (𝓤 α)<GOAL>Tendsto (fun x => (f₁ x, f₃ x)) l (𝓤 α)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>l : Filter β<VAR>f₁ f₂ f₃ : β → α<VAR>h₁₂ : Tendsto (fun x => (f₁ x, f₂ x)) l (𝓤 α)<VAR>h₂₃ : Tendsto (fun x => (f₂ x, f₃ x)) l (𝓤 α)<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<GOAL>(fun x => (f₁ x, f₃ x)) ⁻¹' (s ○ s) ∈ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NonUnitalRing α<VAR>a b c : α<VAR>h : a ∣ b - c<GOAL>a ∣ b ↔ a ∣ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f✝ f : α → β<VAR>hf : AEMeasurable f μ<VAR>s : Set β<GOAL>s ⊆ toMeasurable (map f μ) s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n : ℕ<GOAL>0 < ⌊a⌋₊ ↔ 1 ≤ a
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedAddCommGroup E''<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace 𝕜 E'<VAR>inst✝⁵ : NormedSpace 𝕜 E''<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝³ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : MeasurableAdd G<VAR>inst✝ : MeasurableNeg G<VAR>x₀ : G<VAR>s : Set G<VAR>hbg : BddAbove ((fun i => ‖g i‖) '' ((fun t => -t + x₀) ⁻¹' s))<VAR>hs : MeasurableSet s<VAR>h2s : (support fun t => (L (f t)) (g (x₀ - t))) ⊆ s<VAR>hf : IntegrableOn f s μ<VAR>hmg : AEStronglyMeasurable g (Measure.map (fun t => x₀ - t) (μ.restrict s))<GOAL>Integrable (fun t => (L (f t)) (g (x₀ - t))) μ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedAddCommGroup E''<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace 𝕜 E'<VAR>inst✝⁵ : NormedSpace 𝕜 E''<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝³ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : MeasurableAdd G<VAR>inst✝ : MeasurableNeg G<VAR>x₀ : G<VAR>s : Set G<VAR>hbg : BddAbove ((fun i => ‖g i‖) '' ((fun t => -t + x₀) ⁻¹' s))<VAR>hs : MeasurableSet s<VAR>h2s : (support fun t => (L (f t)) (g (x₀ - t))) ⊆ s<VAR>hf : IntegrableOn f s μ<VAR>hmg : AEStronglyMeasurable g (Measure.map (fun t => x₀ - t) (μ.restrict s))<GOAL>IntegrableOn (fun t => (L (f t)) (g (x₀ - t))) s μ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedAddCommGroup E''<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace 𝕜 E'<VAR>inst✝⁵ : NormedSpace 𝕜 E''<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝³ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : MeasurableAdd G<VAR>inst✝ : MeasurableNeg G<VAR>x₀ : G<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>h2s : (support fun t => (L (f t)) (g (x₀ - t))) ⊆ s<VAR>hf : IntegrableOn f s μ<VAR>hmg : AEStronglyMeasurable g (Measure.map (fun t => x₀ - t) (μ.restrict s))<VAR>s' : Set G := (fun t => -t + x₀) ⁻¹' s<VAR>hbg : BddAbove ((fun i => ‖g i‖) '' s')<VAR>this : ∀ᵐ (t : G) ∂μ.restrict s, ‖(L (f t)) (g (x₀ - t))‖ ≤ s.indicator (fun t => ‖L‖ * ‖f t‖ * ⨆ i, ‖g ↑i‖) t<GOAL>IntegrableOn (fun t => (L (f t)) (g (x₀ - t))) s μ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedAddCommGroup E''<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace 𝕜 E'<VAR>inst✝⁵ : NormedSpace 𝕜 E''<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝³ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : MeasurableAdd G<VAR>inst✝ : MeasurableNeg G<VAR>x₀ : G<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>h2s : (support fun t => (L (f t)) (g (x₀ - t))) ⊆ s<VAR>hf : IntegrableOn f s μ<VAR>hmg : AEStronglyMeasurable g (Measure.map (fun t => x₀ - t) (μ.restrict s))<VAR>s' : Set G := (fun t => -t + x₀) ⁻¹' s<VAR>hbg : BddAbove ((fun i => ‖g i‖) '' s')<VAR>this : ∀ᵐ (t : G) ∂μ.restrict s, ‖(L (f t)) (g (x₀ - t))‖ ≤ s.indicator (fun t => ‖L‖ * ‖f t‖ * ⨆ i, ‖g ↑i‖) t<GOAL>Integrable (s.indicator fun t => ‖L‖ * ‖f t‖ * ⨆ i, ‖g ↑i‖) (μ.restrict s)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedAddCommGroup E''<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace 𝕜 E'<VAR>inst✝⁵ : NormedSpace 𝕜 E''<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝³ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : MeasurableAdd G<VAR>inst✝ : MeasurableNeg G<VAR>x₀ : G<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>h2s : (support fun t => (L (f t)) (g (x₀ - t))) ⊆ s<VAR>hf : IntegrableOn f s μ<VAR>hmg : AEStronglyMeasurable g (Measure.map (fun t => x₀ - t) (μ.restrict s))<VAR>s' : Set G := (fun t => -t + x₀) ⁻¹' s<VAR>hbg : BddAbove ((fun i => ‖g i‖) '' s')<VAR>this : ∀ᵐ (t : G) ∂μ.restrict s, ‖(L (f t)) (g (x₀ - t))‖ ≤ s.indicator (fun t => ‖L‖ * ‖f t‖ * ⨆ i, ‖g ↑i‖) t<GOAL>AEStronglyMeasurable (fun t => (L (f t)) (g (x₀ - t))) (μ.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<GOAL>_root_.Disjoint (map Embedding.inl s) (map Embedding.inr t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<GOAL>∀ ⦃a : α ⊕ β⦄, (∃ a_1 ∈ s, Embedding.inl a_1 = a) → ¬∃ a_2 ∈ t, Embedding.inr a_2 = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f : α → β<VAR>μs : ι → Measure α<VAR>hμs : ∀ (i : ι), μs i ≪ ν<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hs0 : ν s = 0<GOAL>(sum μs) s = 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.84186, u_1} C<VAR>inst✝³ : Category.{?u.84190, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>inst✝ : HasZeroObject C<VAR>s : S.Splitting<GOAL>S.LeftHomologyData