ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>a : R<VAR>ha : 0 < a<VAR>c : R<VAR>hc : IsRegular c<GOAL>0 < c * a * star c
<VAR>E : Type u_1<VAR>f✝ : ℝ → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f f' g : ℝ → ℝ<VAR>a : ℝ<VAR>hf : ContinuousOn f (Ici a)<VAR>hft : Tendsto f atTop atTop<VAR>hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hg_cont : ContinuousOn g (f '' Ioi a)<VAR>hg1 : IntegrableOn g (f '' Ici a) volume<VAR>hg2 : IntegrableOn (fun x => (g ∘ f) x * f' x) (Ici a) volume<GOAL>∫ (x : ℝ) in Ioi a, (g ∘ f) x * f' x = ∫ (u : ℝ) in Ioi (f a), g u
<VAR>E : Type u_1<VAR>f✝ : ℝ → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f f' g : ℝ → ℝ<VAR>a : ℝ<VAR>hf : ContinuousOn f (Ici a)<VAR>hft : Tendsto f atTop atTop<VAR>hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hg_cont : ContinuousOn g (f '' Ioi a)<VAR>hg1 : IntegrableOn g (f '' Ici a) volume<VAR>hg2 : IntegrableOn (fun x => (g ∘ f) x * f' x) (Ici a) volume<VAR>hg2' : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a) volume<GOAL>∫ (x : ℝ) in Ioi a, (g ∘ f) x * f' x = ∫ (u : ℝ) in Ioi (f a), g u
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>P : Submodule R M<GOAL>P.toAddSubgroup = ⊤ ↔ P = ⊤
<VAR>M : Type w<VAR>A : Set M<VAR>L : Language<VAR>inst✝ : L.Structure M<VAR>α : Type u₁<VAR>β : Type u_1<VAR>B : Set M<VAR>s : Set (α → M)<GOAL>∅.Definable L s ↔ ∃ φ, s = setOf φ.Realize
<VAR>M : Type w<VAR>A : Set M<VAR>L : Language<VAR>inst✝ : L.Structure M<VAR>α : Type u₁<VAR>β : Type u_1<VAR>B : Set M<VAR>s : Set (α → M)<GOAL>(∃ φ, s = setOf φ.Realize) ↔ ∃ b, s = setOf ((LEquiv.addEmptyConstants L ↑∅).onFormula.symm b).Realize
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : ∀ x ∈ interior D, deriv f x < 0<VAR>x : ℝ<VAR>hx : x ∈ D<VAR>y : ℝ<GOAL>y ∈ D → x < y → f y < f x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t : Set α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f (μ.restrict s)<VAR>hf' : ∀ᵐ (x : α) ∂μ.restrict s, f x ≠ ⊤<GOAL>(⨍⁻ (x : α) in s, f x ∂μ).toReal = ⨍ (x : α) in s, (f x).toReal ∂μ
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>D : Type u_2<VAR>inst✝³ : Category.{?u.1522, u_2} D<VAR>inst✝² : FinitaryPreExtensive C<VAR>X : C<VAR>S : Presieve X<VAR>inst✝¹ : S.Extensive<VAR>F : Cᵒᵖ ⥤ Type w<VAR>inst✝ : PreservesFiniteProducts F<GOAL>IsSheafFor F S
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>D : Type u_2<VAR>inst✝³ : Category.{?u.1522, u_2} D<VAR>inst✝² : FinitaryPreExtensive C<VAR>X : C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>inst✝¹ : PreservesFiniteProducts F<VAR>α : Type<VAR>w✝ : Finite α<VAR>Z : α → C<VAR>π : (a : α) → Z a ⟶ X<VAR>inst✝ : (ofArrows Z π).Extensive<VAR>hc : IsColimit (Cofan.mk X π)<GOAL>IsSheafFor F (ofArrows Z π)
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>D : Type u_2<VAR>inst✝³ : Category.{?u.1522, u_2} D<VAR>inst✝² : FinitaryPreExtensive C<VAR>X : C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>inst✝¹ : PreservesFiniteProducts F<VAR>α : Type<VAR>w✝ : Finite α<VAR>Z : α → C<VAR>π : (a : α) → Z a ⟶ X<VAR>inst✝ : (ofArrows Z π).Extensive<VAR>hc : IsColimit (Cofan.mk X π)<VAR>this : (ofArrows Z (Cofan.mk X π).inj).hasPullbacks<GOAL>IsSheafFor F (ofArrows Z π)
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>D : Type u_2<VAR>inst✝³ : Category.{?u.1522, u_2} D<VAR>inst✝² : FinitaryPreExtensive C<VAR>X : C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>inst✝¹ : PreservesFiniteProducts F<VAR>α : Type<VAR>w✝ : Finite α<VAR>Z : α → C<VAR>π : (a : α) → Z a ⟶ X<VAR>inst✝ : (ofArrows Z π).Extensive<VAR>hc : IsColimit (Cofan.mk X π)<VAR>this : (ofArrows Z (Cofan.mk X π).inj).hasPullbacks<VAR>val✝ : Fintype α<GOAL>IsSheafFor F (ofArrows Z π)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : LocallyCompactSpace Y<VAR>f : X → Y<VAR>hf : OpenEmbedding f<VAR>this : ∀ (x : X), (𝓝 x).HasBasis (fun s => (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ range f) fun x => f ⁻¹' x<GOAL>LocallyCompactSpace X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>inst✝ : LocallyCompactSpace Y<VAR>f : X → Y<VAR>hf : OpenEmbedding f<VAR>this : ∀ (x : X), (𝓝 x).HasBasis (fun s => (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ range f) fun x => f ⁻¹' x<VAR>x : X<VAR>s : Set Y<VAR>hs : (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ range f<GOAL>IsCompact (f ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>inst✝ : LocallyCompactSpace Y<VAR>f : X → Y<VAR>hf : OpenEmbedding f<VAR>this : ∀ (x : X), (𝓝 x).HasBasis (fun s => (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ range f) fun x => f ⁻¹' x<VAR>x : X<VAR>s : Set Y<VAR>hs : (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ range f<GOAL>IsCompact s
<VAR>x y : ℂ<GOAL>(exp' 0).lim = 1
<VAR>x y : ℂ<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>j : ℕ<VAR>hj : j ≥ 1<GOAL>abs (↑(exp' 0 - const (⇑abs) 1) j) < ε
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasInjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>I : InjectiveResolution X<VAR>J : InjectiveResolution Y<VAR>φ : I.cocomplex ⟶ J.cocomplex<VAR>comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<GOAL>(I.isoRightDerivedToHomotopyCategoryObj F).inv ≫ F.rightDerivedToHomotopyCategory.map f = (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ)).map φ ≫ (J.isoRightDerivedToHomotopyCategoryObj F).inv
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasInjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>I : InjectiveResolution X<VAR>J : InjectiveResolution Y<VAR>φ : I.cocomplex ⟶ J.cocomplex<VAR>comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<GOAL>F.rightDerivedToHomotopyCategory.map f = (I.isoRightDerivedToHomotopyCategoryObj F).hom ≫ (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ)).map φ ≫ (J.isoRightDerivedToHomotopyCategoryObj F).inv
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasInjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>I : InjectiveResolution X<VAR>J : InjectiveResolution Y<VAR>φ : I.cocomplex ⟶ J.cocomplex<VAR>comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<GOAL>F.rightDerivedToHomotopyCategory.map f = (I.isoRightDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ) ≫ (J.isoRightDerivedToHomotopyCategoryObj F).inv
<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>α : Type u_5<VAR>inst✝¹ : TopologicalSpace α<VAR>e : PartialHomeomorph α H<VAR>h : e.source = univ<VAR>G : StructureGroupoid H<VAR>inst✝ : ClosedUnderRestriction G<VAR>e' e'' : PartialHomeomorph α H<VAR>he' : e' ∈ atlas H α<VAR>he'' : e'' ∈ atlas H α<GOAL>e'.symm ≫ₕ e'' ∈ G
<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>α : Type u_5<VAR>inst✝¹ : TopologicalSpace α<VAR>e : PartialHomeomorph α H<VAR>h : e.source = univ<VAR>G : StructureGroupoid H<VAR>inst✝ : ClosedUnderRestriction G<VAR>e' e'' : PartialHomeomorph α H<VAR>he' : e' ∈ atlas H α<VAR>he'' : e'' ∈ atlas H α<GOAL>e.symm ≫ₕ e ∈ G
<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>α : Type u_5<VAR>inst✝¹ : TopologicalSpace α<VAR>e : PartialHomeomorph α H<VAR>h : e.source = univ<VAR>G : StructureGroupoid H<VAR>inst✝ : ClosedUnderRestriction G<VAR>e' e'' : PartialHomeomorph α H<VAR>he' : e' ∈ atlas H α<VAR>he'' : e'' ∈ atlas H α<GOAL>ofSet e.target ⋯ ∈ G
<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>α : Type u_5<VAR>inst✝¹ : TopologicalSpace α<VAR>e : PartialHomeomorph α H<VAR>h : e.source = univ<VAR>G : StructureGroupoid H<VAR>inst✝ : ClosedUnderRestriction G<VAR>e' e'' : PartialHomeomorph α H<VAR>he' : e' ∈ atlas H α<VAR>he'' : e'' ∈ atlas H α<VAR>hle : idRestrGroupoid ≤ G<GOAL>ofSet e.target ⋯ ∈ G
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝¹³ : CommSemiring R✝<VAR>inst✝¹² : NonUnitalRing A✝<VAR>inst✝¹¹ : Module R✝ A✝<VAR>inst✝¹⁰ : IsScalarTower R✝ A✝ A✝<VAR>inst✝⁹ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁸ : Semifield R<VAR>inst✝⁷ : Field S<VAR>inst✝⁶ : NonUnitalRing A<VAR>inst✝⁵ : Module R A<VAR>inst✝⁴ : Module S A<VAR>inst✝³ : IsScalarTower S A A<VAR>inst✝² : SMulCommClass S A A<VAR>inst✝¹ : Algebra R S<VAR>a : A<VAR>f : S → R<VAR>inst✝ : IsScalarTower R S A<VAR>h : QuasispectrumRestricts a f<GOAL>⇑(algebraMap R S) '' quasispectrum R a = quasispectrum S a
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝¹³ : CommSemiring R✝<VAR>inst✝¹² : NonUnitalRing A✝<VAR>inst✝¹¹ : Module R✝ A✝<VAR>inst✝¹⁰ : IsScalarTower R✝ A✝ A✝<VAR>inst✝⁹ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁸ : Semifield R<VAR>inst✝⁷ : Field S<VAR>inst✝⁶ : NonUnitalRing A<VAR>inst✝⁵ : Module R A<VAR>inst✝⁴ : Module S A<VAR>inst✝³ : IsScalarTower S A A<VAR>inst✝² : SMulCommClass S A A<VAR>inst✝¹ : Algebra R S<VAR>a : A<VAR>f : S → R<VAR>inst✝ : IsScalarTower R S A<VAR>h : QuasispectrumRestricts a f<GOAL>⇑(algebraMap R S) '' quasispectrum R a ⊆ quasispectrum S a
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝¹³ : CommSemiring R✝<VAR>inst✝¹² : NonUnitalRing A✝<VAR>inst✝¹¹ : Module R✝ A✝<VAR>inst✝¹⁰ : IsScalarTower R✝ A✝ A✝<VAR>inst✝⁹ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁸ : Semifield R<VAR>inst✝⁷ : Field S<VAR>inst✝⁶ : NonUnitalRing A<VAR>inst✝⁵ : Module R A<VAR>inst✝⁴ : Module S A<VAR>inst✝³ : IsScalarTower S A A<VAR>inst✝² : SMulCommClass S A A<VAR>inst✝¹ : Algebra R S<VAR>a : A<VAR>f : S → R<VAR>inst✝ : IsScalarTower R S A<VAR>h : QuasispectrumRestricts a f<VAR>s : S<VAR>hs : s ∈ quasispectrum S a<GOAL>f s ∈ quasispectrum R a ∧ (algebraMap R S) (f s) = s
<VAR>α : Type u_1<VAR>inst✝¹ : CommMonoidWithZero α<VAR>inst✝ : WfDvdMonoid α<VAR>a : α<VAR>hn0 : a ≠ 0<VAR>hnu : ¬IsUnit a<GOAL>∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod = a ∧ f ≠ ∅
<VAR>α : Type u_1<VAR>inst✝¹ : CommMonoidWithZero α<VAR>inst✝ : WfDvdMonoid α<VAR>f : Multiset α<VAR>hi : ∀ b ∈ f, Irreducible b<VAR>u : αˣ<VAR>hn0 : f.prod * ↑u ≠ 0<VAR>hnu : ¬IsUnit (f.prod * ↑u)<GOAL>∃ f_1, (∀ b ∈ f_1, Irreducible b) ∧ f_1.prod = f.prod * ↑u ∧ f_1 ≠ ∅
<VAR>α : Type u_1<VAR>inst✝¹ : CommMonoidWithZero α<VAR>inst✝ : WfDvdMonoid α<VAR>f : Multiset α<VAR>hi : ∀ b ∈ f, Irreducible b<VAR>u : αˣ<VAR>hn0 : f.prod * ↑u ≠ 0<VAR>hnu : ¬IsUnit (f.prod * ↑u)<VAR>b : α<VAR>h : b ∈ f<GOAL>∃ f_1, (∀ b ∈ f_1, Irreducible b) ∧ f_1.prod = f.prod * ↑u ∧ f_1 ≠ ∅
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f f₁ : E → F<VAR>f' f₀' f₁' : F<VAR>s t : Set E<VAR>x v : E<GOAL>HasLineDerivWithinAt 𝕜 f f' univ x v ↔ HasLineDerivAt 𝕜 f f' x v
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>f : R[X]<VAR>x : AdjoinRoot f<GOAL>(quotMapOfEquivQuotMapCMapSpanMk I f).symm ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (span {f})) (Ideal.map C I))) x) = (Ideal.Quotient.mk (Ideal.map (of f) I)) x
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>f : R[X]<VAR>x : AdjoinRoot f<GOAL>(quotEquivOfEq ⋯) ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (span {f})) (Ideal.map C I))) x) = (Ideal.Quotient.mk (Ideal.map (of f) I)) x
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>f : Π₀ (i : ι), β i<VAR>H : f.support = ∅<GOAL>∀ (i : ι), f i = 0 i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : InnerProductSpace 𝕜 F<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : CompleteSpace F<VAR>f : E →L[𝕜] E<GOAL>0 ≤ f ↔ f.IsPositive
<VAR>a✝ b✝ c : ℕ<VAR>α : Type u_1<VAR>inst✝ : DivisionSemiring α<VAR>a : α<VAR>b : ℤ<VAR>nb ne : ℕ<VAR>pb : IsInt b (Int.negOfNat nb)<VAR>pe' : IsNat (a ^ nb)⁻¹ ne<GOAL>IsNat (a ^ b) ne
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>π : β → Type u_3<VAR>inst✝¹ : Fintype β<VAR>inst✝ : (b : β) → PseudoMetricSpace (π b)<VAR>f g : (b : β) → π b<VAR>r : ℝ≥0<GOAL>dist f g ≤ ↑r ↔ ∀ (b : β), dist (f b) (g b) ≤ ↑r
<VAR>m n k : ℕ<GOAL>m.gcd (m * k + n) = m.gcd n
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>h : f.nextCoeff ≠ 0<GOAL>f.eraseLead.natDegree = f.natDegree - 1
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>h : f.nextCoeff ≠ 0<VAR>this : 0 < f.natDegree<GOAL>f.eraseLead.natDegree = f.natDegree - 1
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>h : f.nextCoeff ≠ 0<VAR>this : 0 < f.natDegree<GOAL>f.eraseLead.coeff (f.natDegree - 1) ≠ 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>h : f.nextCoeff ≠ 0<VAR>this : 0 < f.natDegree<GOAL>0 < f.natDegree
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>h : f.nextCoeff ≠ 0<VAR>this : 0 < f.natDegree<GOAL>0 < 1
<VAR>R : Type u_1<VAR>inst✝ : NonUnitalNonAssocRing R<VAR>S : Set (TwoSidedIdeal R)<VAR>x : R<GOAL>(∀ x_1 ∈ ringCon '' S, x_1 x 0) ↔ ∀ I ∈ S, x ∈ I
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<GOAL>eLpNorm f 1 μ = ∫⁻ (x : α), ↑‖f x‖₊ ∂μ
<VAR>K : Type u<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>P : Sort v<VAR>p q : K[X]<VAR>f : K[X] → K[X] → P<VAR>f0 : ∀ (p : K[X]), f p 0 = f 0 1<VAR>H : ∀ {p q a : K[X]}, q ≠ 0 → a ≠ 0 → f (a * p) (a * q) = f p q<GOAL>(RatFunc.mk p q).liftOn' f H = f p q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν✝ μ₁ μ₂ ν : Measure α<VAR>inst✝¹ : μ₁.HaveLebesgueDecomposition ν<VAR>inst✝ : μ₂.HaveLebesgueDecomposition ν<GOAL>(μ₁ + μ₂).singularPart ν = μ₁.singularPart ν + μ₂.singularPart ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν✝ μ₁ μ₂ ν : Measure α<VAR>inst✝¹ : μ₁.HaveLebesgueDecomposition ν<VAR>inst✝ : μ₂.HaveLebesgueDecomposition ν<GOAL>μ₁ + μ₂ = μ₁.singularPart ν + μ₂.singularPart ν + ν.withDensity fun a => μ₁.rnDeriv ν a + μ₂.rnDeriv ν a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν✝ μ₁ μ₂ ν : Measure α<VAR>inst✝¹ : μ₁.HaveLebesgueDecomposition ν<VAR>inst✝ : μ₂.HaveLebesgueDecomposition ν<GOAL>μ₁ + μ₂ = μ₁.singularPart ν + μ₂.singularPart ν + (ν.withDensity (μ₁.rnDeriv ν) + ν.withDensity (μ₂.rnDeriv ν))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν✝ μ₁ μ₂ ν : Measure α<VAR>inst✝¹ : μ₁.HaveLebesgueDecomposition ν<VAR>inst✝ : μ₂.HaveLebesgueDecomposition ν<GOAL>μ₁ + μ₂ = μ₁.singularPart ν + ν.withDensity (μ₁.rnDeriv ν) + ν.withDensity (μ₂.rnDeriv ν) + μ₂.singularPart ν
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<GOAL>(thickening δ s)⁻¹ = thickening δ s⁻¹
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<GOAL>{x | EMetric.infEdist x s < ENNReal.ofReal δ}⁻¹ = {x | EMetric.infEdist x⁻¹ s < ENNReal.ofReal δ}
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>S : Seq (Seq1 α)<GOAL>Seq.map f S.join = (Seq.map (map f) S).join
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>S : Seq (Seq1 α)<GOAL>Seq.IsBisimulation fun s1 s2 => ∃ s S, s1 = s.append (Seq.map f S.join) ∧ s2 = s.append (Seq.map (map f) S).join
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>S : Seq (Seq1 α)<GOAL>∃ s S_1, Seq.map f S.join = s.append (Seq.map f S_1.join) ∧ (Seq.map (map f) S).join = s.append (Seq.map (map f) S_1).join
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a✝ b✝ c✝ d a b c : α<GOAL>(a \ b) \ c = (a \ c) \ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p a b : ℕ<VAR>hp : p ≠ 1<VAR>hle : multiplicity p a ≤ multiplicity p b<VAR>hab : a.Coprime b<GOAL>multiplicity p a = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p a b : ℕ<VAR>hp : p ≠ 1<VAR>hle : ∀ (n : ℕ), p ^ n ∣ a → p ^ n ∣ b<VAR>hab : a.Coprime b<GOAL>multiplicity p a = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p a b : ℕ<VAR>hp : p ≠ 1<VAR>hle : ∀ (n : ℕ), p ^ n ∣ a → p ^ n ∣ b<VAR>hab : a.Coprime b<GOAL>¬p ^ 1 ∣ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p a b : ℕ<VAR>hp : p ≠ 1<VAR>hle : ∀ (n : ℕ), p ^ n ∣ a → p ^ n ∣ b<VAR>hab : a.Coprime b<VAR>h : p ^ 1 ∣ a<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p a b : ℕ<VAR>hp : p ≠ 1<VAR>hle : ∀ (n : ℕ), p ^ n ∣ a → p ^ n ∣ b<VAR>hab : a.Coprime b<VAR>h : p ^ 1 ∣ a<VAR>this : p ^ 1 ∣ a.gcd b<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p a b : ℕ<VAR>hp : p ≠ 1<VAR>hle : ∀ (n : ℕ), p ^ n ∣ a → p ^ n ∣ b<VAR>hab : a.Coprime b<VAR>h : p ^ 1 ∣ a<VAR>this : p = 1<GOAL>False
<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>𝕜 : Type u_5<VAR>inst✝ : NormedDivisionRing 𝕜<VAR>f✝ f : α → 𝕜<VAR>h : Integrable f μ<VAR>c : 𝕜<GOAL>Integrable (fun x => f x / c) μ
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableEq V<VAR>u v : V<VAR>p : G.Walk u v<VAR>h : p.IsEulerian<VAR>e : Sym2 V<VAR>he : e ∈ G.edgeSet<GOAL>e ∈ p.edges
<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✝³ : Zero α<VAR>inst✝² : Zero β<VAR>inst✝¹ : DecidableEq o<VAR>inst✝ : (i : o) → DecidableEq (m' i)<VAR>d : (i : o) × m' i → α<VAR>k : o<VAR>i j : m' k<GOAL>(diagonal d).blockDiag' k i j = diagonal (fun i => d ⟨k, i⟩) 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✝³ : Zero α<VAR>inst✝² : Zero β<VAR>inst✝¹ : DecidableEq o<VAR>inst✝ : (i : o) → DecidableEq (m' i)<VAR>d : (i : o) × m' i → α<VAR>k : o<VAR>i : m' k<GOAL>(diagonal d).blockDiag' k i i = diagonal (fun i => d ⟨k, i⟩) i i
<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✝³ : Zero α<VAR>inst✝² : Zero β<VAR>inst✝¹ : DecidableEq o<VAR>inst✝ : (i : o) → DecidableEq (m' i)<VAR>d : (i : o) × m' i → α<VAR>k : o<VAR>i j : m' k<VAR>hij : i ≠ j<GOAL>(diagonal d).blockDiag' k i j = diagonal (fun i => d ⟨k, i⟩) i j
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x y : E<VAR>hx : x ∈ closure s<VAR>hy : x + y ∈ interior s<VAR>t : 𝕜<VAR>ht : t ∈ Ioc 0 1<GOAL>x + t • y ∈ interior s
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>f g : R[X]<VAR>N : ℕ<GOAL>reflect N (f - g) = reflect N f - reflect N g
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>c : E<GOAL>∫ (x : ℝ) in a..b, c ∂μ = ((μ (Ioc a b)).toReal - (μ (Ioc b a)).toReal) • c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s✝ t✝ s t : Set α<GOAL>sᶜ =ᶠ[ae μ] t ↔ s =ᶠ[ae μ] tᶜ
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : b ⟶ a<VAR>η : 𝟙 a ⟶ f ≫ g<VAR>ε : g ≫ f ⟶ 𝟙 b<VAR>h : leftZigzag η ε = (λ_ f).hom ≫ (ρ_ f).inv<GOAL>(g ◁ η ⊗≫ ε ▷ g) ⊗≫ g ◁ η ⊗≫ ε ▷ g = g ◁ η ⊗≫ ε ▷ g
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M✝ : Type u_2<VAR>inst✝⁹ : AddCommGroup M✝<VAR>inst✝⁸ : Module R M✝<VAR>M' : Type u_3<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : Module R M'<VAR>ι : Type u_4<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Fintype ι<VAR>e : Basis ι R M✝<VAR>A : Type u_5<VAR>inst✝³ : CommRing A<VAR>m : Type u_6<VAR>n : Type u_7<VAR>inst✝² : Fintype m<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>M N : Matrix n n A<GOAL>(M * N).det = (N * M).det
<VAR>V✝ : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G✝ : SimpleGraph V✝<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>p : G.Walk u v<VAR>q : G.Walk v w<VAR>h : V<GOAL>h ∈ q.support → h ∈ (p.append q).support
<VAR>α β : Type u<VAR>a : Cardinal.{u_1}<GOAL>lift.{v, u_1} (2 ^ a) = 2 ^ lift.{v, u_1} a
<VAR>b x y : ℝ<VAR>hx : 0 < x<GOAL>logb b (x ^ y) = y * logb b x
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : IsPurelyInseparable F E<VAR>ι : Type u_1<VAR>v : ι → K<VAR>hsep : ∀ (i : ι), IsSeparable F (v i)<VAR>h : LinearIndependent F v<GOAL>LinearIndependent E v
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : IsPurelyInseparable F E<VAR>ι : Type u_1<VAR>v : ι → K<VAR>hsep : ∀ (i : ι), IsSeparable F (v i)<VAR>h : LinearIndependent F v<VAR>q : ℕ<VAR>h✝ : ExpChar F q<GOAL>LinearIndependent E v
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : IsPurelyInseparable F E<VAR>ι : Type u_1<VAR>v : ι → K<VAR>hsep : ∀ (i : ι), IsSeparable F (v i)<VAR>h : LinearIndependent F v<VAR>q : ℕ<VAR>h✝ : ExpChar F q<VAR>this : ExpChar K q<GOAL>LinearIndependent E v
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : IsPurelyInseparable F E<VAR>ι : Type u_1<VAR>v : ι → K<VAR>hsep : ∀ (i : ι), IsSeparable F (v i)<VAR>h : LinearIndependent F v<VAR>q : ℕ<VAR>h✝ : ExpChar F q<VAR>this : ExpChar K q<VAR>l : ι →₀ E<VAR>hl : (Finsupp.total ι K E v) l = 0<VAR>i : ι<GOAL>l i = 0 i