ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>inst✝ : TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>C : ℝ<VAR>g : α → E<VAR>g' : α → F<VAR>h : ‖g x‖ ≤ C * ‖g' x‖<GOAL>IsBigOWith C (𝓝[insert x s] x) g g' ↔ IsBigOWith C (𝓝[s] x) g g'
<VAR>s : ℂ<GOAL>completedRiemannZeta₀ (1 - s) = completedRiemannZeta₀ s
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>κ : Type u_1<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>h : ι ≃ κ<VAR>f : Π₀ (k : κ), β (h.symm k)<VAR>i : ι<GOAL>HEq 0 0
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>κ : Type u_1<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>h : ι ≃ κ<VAR>f : Π₀ (i : ι), β i<VAR>i : ι<GOAL>((fun f => mapRange (fun i => ⇑(Equiv.cast ⋯)) ⋯ (comapDomain' ⇑h ⋯ f)) (comapDomain' ⇑h.symm ⋯ f)) i = f i
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>κ : Type u_1<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>h : ι ≃ κ<VAR>f : Π₀ (k : κ), β (h.symm k)<VAR>k : κ<GOAL>(comapDomain' ⇑h.symm ⋯ ((fun f => mapRange (fun i => ⇑(Equiv.cast ⋯)) ⋯ (comapDomain' ⇑h ⋯ f)) f)) k = f k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>h2f : ∫⁻ (x : α), f x ∂μ ≠ ⊤<GOAL>∀ᵐ (x : α) ∂μ, f x < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>h2f : ∫⁻ (x : α), f x ∂μ ≠ ⊤<GOAL>μ {a | f a = ⊤} = 0
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a : α<GOAL>⋃ n, Ico (n • p) ((n + 1) • p) = univ
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>g✝ : P →ₗ[R] Q<VAR>f✝ : N →ₗ[R] P<VAR>g' : Q →ₗ[R] S<VAR>f : M →ₗ[R] P<VAR>g : N →ₗ[R] Q<GOAL>lTensor P g' ∘ₗ map f g = map f (g' ∘ₗ g)
<VAR>X : Type u_1<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : OpensMeasurableSpace X<VAR>μ : Measure X<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SecondCountableTopology E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>ι : Type u_3<VAR>μs : ι → Measure X<VAR>inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)<VAR>f : X →ᵇ E<GOAL>Bornology.IsBounded (Set.range fun i => ∫ (x : X), f x ∂μs i)
<VAR>X : Type u_1<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : OpensMeasurableSpace X<VAR>μ : Measure X<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SecondCountableTopology E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>ι : Type u_3<VAR>μs : ι → Measure X<VAR>inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)<VAR>f : X →ᵇ E<VAR>v : E<VAR>hv : v ∈ Set.range fun i => ∫ (x : X), f x ∂μs i<GOAL>‖v‖ ≤ ‖f‖
<VAR>X : Type u_1<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : OpensMeasurableSpace X<VAR>μ : Measure X<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SecondCountableTopology E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>ι : Type u_3<VAR>μs : ι → Measure X<VAR>inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)<VAR>f : X →ᵇ E<VAR>v : E<VAR>i : ι<VAR>hi : (fun i => ∫ (x : X), f x ∂μs i) i = v<GOAL>‖(fun i => ∫ (x : X), f x ∂μs i) i‖ ≤ ‖f‖
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝¹ : HasAffineProperty P Q<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>𝒰 : Y.OpenCover<VAR>inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)<GOAL>P f ↔ ∀ (i : (𝒰.pullbackCover f).J), Q (𝒰.pullbackHom f i)
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝¹ : HasAffineProperty P Q<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>𝒰 : Y.OpenCover<VAR>inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)<VAR>this : Q.IsLocal := isLocal_affineProperty P<GOAL>P f ↔ ∀ (i : (𝒰.pullbackCover f).J), Q (𝒰.pullbackHom f i)
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝¹ : HasAffineProperty P Q<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>𝒰 : Y.OpenCover<VAR>inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)<VAR>this : Q.IsLocal := isLocal_affineProperty P<GOAL>(∀ (i : 𝒰.J), Q (f ∣_ ↑⟨Scheme.Hom.opensRange (𝒰.map i), ⋯⟩)) ↔ ∀ (i : (𝒰.pullbackCover f).J), Q (𝒰.pullbackHom f i)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring ι<VAR>inst✝⁸ : Module ι (Additive ℤˣ)<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>inst✝ : GradedAlgebra ℬ<VAR>i₂ : ι<VAR>a₁ : A<VAR>a₂ : ↥(𝒜 i₂)<VAR>b₂ : B<GOAL>b₂ = ↑GradedMonoid.GOne.one * b₂
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>inst✝ : HasGroupoid M G<VAR>s : Opens M<VAR>t : Opens H<VAR>ht : Nonempty ↥t<VAR>e' : PartialHomeomorph (↥t) H<VAR>xset : Set (PartialHomeomorph (↥t) H)<VAR>he' : e' ∈ xset<VAR>x : ↥t<VAR>hx : (fun x => {(chartAt H ↑x).subtypeRestr ⋯}) x = xset<GOAL>∃ x, e' = (chartAt H ↑x).subtypeRestr ht
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>r s : R<GOAL>(cast R M ⋯) (GradedMonoid.GMul.mul (algebraMap₀ r) (algebraMap₀ s)) = algebraMap₀ (r * s)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>r s : R<GOAL>(cast R M ⋯) (GradedMonoid.GMul.mul (algebraMap₀ r) (algebraMap₀ s)) = r • algebraMap₀ s
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝³ : Category.{uD', uD} D<VAR>inst✝² : HasZeroMorphisms D<VAR>P Q W X Y Z : C<VAR>inst✝¹ : HasBinaryBiproduct W X<VAR>inst✝ : HasBinaryBiproduct Y Z<VAR>f : W ⟶ Y<VAR>g : X ⟶ Z<GOAL>inr ≫ map f g = g ≫ inr
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝³ : Category.{uD', uD} D<VAR>inst✝² : HasZeroMorphisms D<VAR>P Q W X Y Z : C<VAR>inst✝¹ : HasBinaryBiproduct W X<VAR>inst✝ : HasBinaryBiproduct Y Z<VAR>f : W ⟶ Y<VAR>g : X ⟶ Z<GOAL>inr ≫ map' f g = g ≫ inr
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>as : List α<GOAL>findIdxs (fun b => decide (p b)) as = map Prod.fst (indexesValues (fun b => decide (p b)) as)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : NoetherianSpace α<VAR>s : Closeds α<GOAL>∃ S, S.Finite ∧ (∀ t ∈ S, IsClosed t) ∧ (∀ t ∈ S, IsIrreducible t) ∧ ↑s = ⋃₀ S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : NoetherianSpace α<VAR>S : Set (Closeds α)<VAR>hSf : S.Finite<VAR>hS : ∀ t ∈ S, IsIrreducible ↑t<GOAL>∃ S_1, S_1.Finite ∧ (∀ t ∈ S_1, IsClosed t) ∧ (∀ t ∈ S_1, IsIrreducible t) ∧ ↑(sSup S) = ⋃₀ S_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : NoetherianSpace α<VAR>S : Set (Closeds α)<VAR>hSf : S.Finite<VAR>hS : ∀ t ∈ S, IsIrreducible ↑t<GOAL>↑(sSup S) = ⋃₀ (SetLike.coe '' S)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : NoetherianSpace α<VAR>S : Finset (Closeds α)<VAR>hS : ∀ t ∈ ↑S, IsIrreducible ↑t<GOAL>↑(sSup ↑S) = ⋃₀ (SetLike.coe '' ↑S)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I J : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>h₁ : IsSolvable R L<VAR>h₂ : Injective ⇑f<VAR>k : ℕ<VAR>hk : derivedSeries R L k = ⊥<GOAL>IsSolvable R L'
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I J : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>h₁ : IsSolvable R L<VAR>h₂ : Injective ⇑f<VAR>k : ℕ<VAR>hk : derivedSeries R L k = ⊥<GOAL>derivedSeries R L' k = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I J : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>h₁ : IsSolvable R L<VAR>h₂ : Injective ⇑f<VAR>k : ℕ<VAR>hk : derivedSeries R L k = ⊥<GOAL>LieIdeal.map f (derivedSeries R L' k) = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I J : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>h₁ : IsSolvable R L<VAR>h₂ : Injective ⇑f<VAR>k : ℕ<VAR>hk : derivedSeries R L k = ⊥<GOAL>LieIdeal.map f (derivedSeries R L' k) ≤ derivedSeries R L k
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a✝ b c d : G₀<VAR>m n : ℕ<VAR>a : G₀<VAR>h : n < m<GOAL>a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
<VAR>E : Type u_1<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup V<VAR>inst✝⁸ : InnerProductSpace ℝ V<VAR>inst✝⁷ : MeasurableSpace V<VAR>inst✝⁶ : BorelSpace V<VAR>inst✝⁵ : FiniteDimensional ℝ V<VAR>W : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : InnerProductSpace ℝ W<VAR>inst✝² : MeasurableSpace W<VAR>inst✝¹ : BorelSpace W<VAR>inst✝ : FiniteDimensional ℝ W<VAR>f : V → E<VAR>w : V<GOAL>𝓕⁻ f w = 𝓕 f (-w)
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>X : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f g : FreeAlgebra R X →ₐ[R] A<VAR>w : ⇑f ∘ ι R = ⇑g ∘ ι R<GOAL>f = g
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>X : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f g : FreeAlgebra R X →ₐ[R] A<VAR>w : (lift R).symm f = (lift R).symm g<GOAL>f = g
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>𝒢 : Set C<VAR>h𝒢 : IsDetecting 𝒢<VAR>X : C<VAR>P Q : Subobject X<VAR>h₁ : P ≤ Q<VAR>h₂ : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f<GOAL>P = Q
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>𝒢 : Set C<VAR>h𝒢 : IsDetecting 𝒢<VAR>X : C<VAR>P Q : Subobject X<VAR>h₁ : P ≤ Q<VAR>h₂ : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f<GOAL>IsIso (P.ofLE Q h₁)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>𝒢 : Set C<VAR>h𝒢 : IsDetecting 𝒢<VAR>X : C<VAR>P Q : Subobject X<VAR>h₁ : P ≤ Q<VAR>h₂ : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f<VAR>G : C<VAR>hG : G ∈ 𝒢<VAR>f : G ⟶ underlying.obj Q<GOAL>∃! h', h' ≫ P.ofLE Q h₁ = f
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>𝒢 : Set C<VAR>h𝒢 : IsDetecting 𝒢<VAR>X : C<VAR>P Q : Subobject X<VAR>h₁ : P ≤ Q<VAR>h₂ : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f<VAR>G : C<VAR>hG : G ∈ 𝒢<VAR>f : G ⟶ underlying.obj Q<VAR>this : P.Factors (f ≫ Q.arrow)<GOAL>∃! h', h' ≫ P.ofLE Q h₁ = f
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>𝒢 : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : ℕ → Ω → ℝ<VAR>hadp : Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), Integrable (f i) μ<VAR>hf : ∀ (i : ℕ), f i ≤ᶠ[ae μ] μ[f (i + 1)|↑𝒢 i]<GOAL>Submartingale f 𝒢 μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>𝒢 : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : ℕ → Ω → ℝ<VAR>hadp : Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), Integrable (f i) μ<VAR>hf : ∀ (i : ℕ), f i ≤ᶠ[ae μ] μ[f (i + 1)|↑𝒢 i]<VAR>i : ℕ<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f (i + 1) ω ∂μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>𝒢 : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : ℕ → Ω → ℝ<VAR>hadp : Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), Integrable (f i) μ<VAR>hf : ∀ (i : ℕ), f i ≤ᶠ[ae μ] μ[f (i + 1)|↑𝒢 i]<VAR>i : ℕ<VAR>s : Set Ω<VAR>hs : MeasurableSet s<VAR>this : ∫ (ω : Ω) in s, f (i + 1) ω ∂μ = ∫ (ω : Ω) in s, (μ[f (i + 1)|↑𝒢 i]) ω ∂μ<GOAL>∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f (i + 1) ω ∂μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>𝒢 : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : ℕ → Ω → ℝ<VAR>hadp : Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), Integrable (f i) μ<VAR>hf : ∀ (i : ℕ), f i ≤ᶠ[ae μ] μ[f (i + 1)|↑𝒢 i]<VAR>i : ℕ<VAR>s : Set Ω<VAR>hs : MeasurableSet s<VAR>this : ∫ (ω : Ω) in s, f (i + 1) ω ∂μ = ∫ (ω : Ω) in s, (μ[f (i + 1)|↑𝒢 i]) ω ∂μ<GOAL>∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, (μ[f (i + 1)|↑𝒢 i]) ω ∂μ
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : LieAlgebra.IsNilpotent R L<VAR>inst✝² : NoZeroSMulDivisors ℤ R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : IsNoetherian R M<VAR>α : L → R<VAR>β : Weight R L M<VAR>hα✝ : α ≠ 0<VAR>n : ℕ<VAR>hn : n ≤ chainTopCoeff α β<VAR>hα : ¬α = 0<GOAL>weightSpace M (n • α + ⇑β) ≠ ⊥
<VAR>ι✝ : Type u_1<VAR>κ✝ : Type u_2<VAR>α✝ : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α✝<VAR>a : α✝<VAR>f✝¹ g✝¹ : α✝ → β<VAR>inst✝² : CommMonoid β<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>inst✝¹ : CommMonoid α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>f✝ : ι → α<VAR>g✝ : κ → α<VAR>inst✝ : DecidableEq κ<VAR>g : ι → κ<VAR>h : ∀ i ∈ s, g i ∈ t<VAR>f : ι → α<GOAL>∏ j ∈ t, ∏ i ∈ filter (fun i => g i = j) s, f i = ∏ i ∈ s, f i
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>A B B' X Y Y' : C<VAR>i : A ⟶ B<VAR>i' : B ⟶ B'<VAR>p : X ⟶ Y<VAR>p' : Y ⟶ Y'<VAR>h : HasLiftingProperty i p<VAR>f : Opposite.op Y ⟶ Opposite.op B<VAR>g : Opposite.op X ⟶ Opposite.op A<VAR>sq : CommSq f p.op i.op g<GOAL>sq.HasLift
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>A B B' X Y Y' : C<VAR>i : A ⟶ B<VAR>i' : B ⟶ B'<VAR>p : X ⟶ Y<VAR>p' : Y ⟶ Y'<VAR>h : HasLiftingProperty i p<VAR>f : Opposite.op Y ⟶ Opposite.op B<VAR>g : Opposite.op X ⟶ Opposite.op A<VAR>sq : CommSq f p.op i.op g<GOAL>⋯.HasLift
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : Type u_4<VAR>K₂ : Type u_5<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>V : Type u_9<VAR>V₂ : Type u_10<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : Semiring R₂<VAR>inst✝¹¹ : Semiring R₃<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R₂ M₂<VAR>inst✝⁴ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝³ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_11<VAR>inst✝² : FunLike F M M₂<VAR>inst✝¹ : SemilinearMapClass F τ₁₂ M M₂<VAR>inst✝ : RingHomSurjective τ₁₂<VAR>f : F<GOAL>range f = ⊤ ↔ Surjective ⇑f
<VAR>N✝ N : ℕ<VAR>A : ↥(Gamma0 N)<GOAL>↑(↑↑A).det = 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<GOAL>T0Space α ↔ (𝓤 α).ker = diagonal α
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<GOAL>(∀ (a b : α), (∀ s ∈ 𝓤 α, (a, b) ∈ s) → a = b) → ∀ (x : α), ∀ s ∈ 𝓤 α, (x, x) ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>x y : α<GOAL>y ∈ ConnectedComponents.mk ⁻¹' {ConnectedComponents.mk x} ↔ y ∈ connectedComponent x
<VAR>G : Type u_1<VAR>inst✝³ : LinearOrderedAddCommGroup G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : OrderTopology G<VAR>inst✝ : Archimedean G<VAR>S : AddSubgroup G<VAR>hS : ∀ ε > 0, ∃ g ∈ S, g ∈ Ioo 0 ε<GOAL>Dense ↑S
<VAR>G : Type u_1<VAR>inst✝³ : LinearOrderedAddCommGroup G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : OrderTopology G<VAR>inst✝ : Archimedean G<VAR>S : AddSubgroup G<VAR>hS : ∀ ε > 0, ∃ g ∈ S, g ∈ Ioo 0 ε<VAR>h✝ : Subsingleton G<GOAL>Dense ↑S
<VAR>G : Type u_1<VAR>inst✝³ : LinearOrderedAddCommGroup G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : OrderTopology G<VAR>inst✝ : Archimedean G<VAR>S : AddSubgroup G<VAR>hS : ∀ ε > 0, ∃ g ∈ S, g ∈ Ioo 0 ε<VAR>h✝ : Nontrivial G<GOAL>Dense ↑S
<VAR>G : Type u_1<VAR>inst✝³ : LinearOrderedAddCommGroup G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : OrderTopology G<VAR>inst✝ : Archimedean G<VAR>S : AddSubgroup G<VAR>hS : ∀ ε > 0, ∃ g ∈ S, g ∈ Ioo 0 ε<VAR>h✝ : Nontrivial G<VAR>a b : G<VAR>hlt : a < b<GOAL>∃ c ∈ ↑S, a < c ∧ c < b
<VAR>G : Type u_1<VAR>inst✝³ : LinearOrderedAddCommGroup G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : OrderTopology G<VAR>inst✝ : Archimedean G<VAR>S : AddSubgroup G<VAR>hS : ∀ ε > 0, ∃ g ∈ S, g ∈ Ioo 0 ε<VAR>h✝ : Nontrivial G<VAR>a b : G<VAR>hlt : a < b<VAR>g : G<VAR>hgS : g ∈ S<VAR>hg0 : 0 < g<VAR>hg : g < b - a<GOAL>∃ c ∈ ↑S, a < c ∧ c < b
<VAR>G : Type u_1<VAR>inst✝³ : LinearOrderedAddCommGroup G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : OrderTopology G<VAR>inst✝ : Archimedean G<VAR>S : AddSubgroup G<VAR>hS : ∀ ε > 0, ∃ g ∈ S, g ∈ Ioo 0 ε<VAR>h✝ : Nontrivial G<VAR>a b : G<VAR>hlt : a < b<VAR>g : G<VAR>hgS : g ∈ S<VAR>hg0 : 0 < g<VAR>hg : g < b - a<VAR>m : ℤ<VAR>hm : 0 + m • g ∈ Ioc a (a + g)<GOAL>∃ c ∈ ↑S, a < c ∧ c < b
<VAR>G : Type u_1<VAR>inst✝³ : LinearOrderedAddCommGroup G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : OrderTopology G<VAR>inst✝ : Archimedean G<VAR>S : AddSubgroup G<VAR>hS : ∀ ε > 0, ∃ g ∈ S, g ∈ Ioo 0 ε<VAR>h✝ : Nontrivial G<VAR>a b : G<VAR>hlt : a < b<VAR>g : G<VAR>hgS : g ∈ S<VAR>hg0 : 0 < g<VAR>hg : g < b - a<VAR>m : ℤ<VAR>hm : m • g ∈ Ioc a (a + g)<GOAL>∃ c ∈ ↑S, a < c ∧ c < b
<VAR>G : Type u_1<VAR>inst✝³ : LinearOrderedAddCommGroup G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : OrderTopology G<VAR>inst✝ : Archimedean G<VAR>S : AddSubgroup G<VAR>hS : ∀ ε > 0, ∃ g ∈ S, g ∈ Ioo 0 ε<VAR>h✝ : Nontrivial G<VAR>a b : G<VAR>hlt : a < b<VAR>g : G<VAR>hgS : g ∈ S<VAR>hg0 : 0 < g<VAR>hg : g < b - a<VAR>m : ℤ<VAR>hm : m • g ∈ Ioc a (a + g)<GOAL>a + g < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : α → Finset β<VAR>b : β<VAR>h : (↑s).PairwiseDisjoint t<GOAL>b ∈ s.disjiUnion t h ↔ ∃ a ∈ s, b ∈ t a
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>X' X : C<VAR>Y Y' : D<VAR>f : X' ⟶ X<VAR>g : F.obj X ⟶ Y'<VAR>h : F.obj X' ⟶ Y<VAR>k : Y ⟶ Y'<VAR>w : F.map f ≫ g = h ≫ k<GOAL>f ≫ (adj.homEquiv X Y') g = (adj.homEquiv X' Y) h ≫ G.map k
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : BorelSpace α<VAR>μ : Measure α<VAR>inst✝ : μ.WeaklyRegular<VAR>f : α →ₛ ℝ≥0<VAR>int_f : ∫⁻ (x : α), ↑(↑f x) ∂μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>ε0 : ε ≠ 0<GOAL>∃ g, (∀ (x : α), g x ≤ ↑f x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(↑f x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : BorelSpace α<VAR>μ : Measure α<VAR>inst✝ : μ.WeaklyRegular<VAR>c : ℝ≥0<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>int_f : ∫⁻ (x : α), ↑(↑(piecewise s hs (const α c) (const α 0)) x) ∂μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>ε0 : ε ≠ 0<GOAL>∃ g, (∀ (x : α), g x ≤ ↑(piecewise s hs (const α c) (const α 0)) x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(↑(piecewise s hs (const α c) (const α 0)) x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : BorelSpace α<VAR>μ : Measure α<VAR>inst✝ : μ.WeaklyRegular<VAR>f₁ f₂ : α →ₛ ℝ≥0<VAR>a✝ : Disjoint (Function.support ↑f₁) (Function.support ↑f₂)<VAR>h₁ : ∫⁻ (x : α), ↑(↑f₁ x) ∂μ ≠ ⊤ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ ↑f₁ x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(↑f₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε<VAR>h₂ : ∫⁻ (x : α), ↑(↑f₂ x) ∂μ ≠ ⊤ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ ↑f₂ x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(↑f₂ x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε<VAR>int_f : ∫⁻ (x : α), ↑(↑(f₁ + f₂) x) ∂μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>ε0 : ε ≠ 0<GOAL>∃ g, (∀ (x : α), g x ≤ ↑(f₁ + f₂) x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(↑(f₁ + f₂) x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : CharP R 2<GOAL>2 = 0
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasExt C<VAR>X Y Z T : C<VAR>n : ℕ<VAR>α : Ext X Y n<VAR>m : ℕ<VAR>β : Ext Y Z m<VAR>p : ℕ<VAR>h : n + m = p<VAR>this : HasDerivedCategory C := HasDerivedCategory.standard C<GOAL>(α.comp (-β) h).hom = (-α.comp β h).hom
<VAR>R : Type u_1<VAR>inst✝² : AddCommMonoid R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : BinomialRing R<VAR>r : R<GOAL>multichoose r 1 = r ^ 1
<VAR>R : Type u_1<VAR>inst✝² : AddCommMonoid R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : BinomialRing R<VAR>r : R<GOAL>(fun x => Nat.factorial 1 • x) (multichoose r 1) = (fun x => Nat.factorial 1 • x) (r ^ 1)
<VAR>R : Type u_1<VAR>inst✝² : AddCommMonoid R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : BinomialRing R<VAR>r : R<GOAL>Nat.factorial 1 • multichoose r 1 = Nat.factorial 1 • r ^ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>s✝ : Set α<VAR>inst✝ : MeasurableSingletonClass α<VAR>s : Set α<VAR>hs : s.Finite<GOAL>count s = ↑hs.toFinset.card
<VAR>x y : ℝ<GOAL>cosh (x + y) = cosh x * cosh y + sinh x * sinh y
<VAR>x y : ℝ<GOAL>↑(cosh (x + y)) = ↑(cosh x * cosh y + sinh x * sinh y)