ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F G : (Cᵒᵖ ⥤ D)ᵒᵖ<VAR>η : F ⟶ G<GOAL>((unop G).rightOpLeftOpIso.hom ≫ η.unop).op = (NatTrans.leftOp (NatTrans.rightOp η.unop.op.unop) ≫ (unop F).rightOpLeftOpIso.hom).op
<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>Y : Scheme<VAR>f : (x : 𝒰.J) → 𝒰.obj x ⟶ Y<VAR>hf : ∀ (x y : 𝒰.J), pullback.fst (𝒰.map x) (𝒰.map y) ≫ f x = pullback.snd (𝒰.map x) (𝒰.map y) ≫ f y<VAR>x : 𝒰.J<GOAL>𝒰.map x ≫ 𝒰.glueMorphisms f hf = f x
<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>Y : Scheme<VAR>f : (x : 𝒰.J) → 𝒰.obj x ⟶ Y<VAR>hf : ∀ (x y : 𝒰.J), pullback.fst (𝒰.map x) (𝒰.map y) ≫ f x = pullback.snd (𝒰.map x) (𝒰.map y) ≫ f y<VAR>x : 𝒰.J<GOAL>𝒰.gluedCover.ι x ≫ 𝒰.fromGlued ≫ 𝒰.glueMorphisms f hf = f x
<VAR>α : Type<VAR>d : ℕ<VAR>ds ds₁ ds₂ ds₃ : List ℕ<VAR>x y : Holor α (d :: ds)<VAR>h : x.slice = y.slice<VAR>t : HolorIndex (d :: ds)<VAR>i : ℕ<VAR>is : List ℕ<VAR>hiis : ↑t = i :: is<GOAL>Forall₂ (fun x x_1 => x < x_1) (↑t) (d :: ds)
<VAR>α : Type u<VAR>β : Type v<VAR>l✝ l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>hl : l.Nodup<VAR>i : Fin l.length<GOAL>l.erase (l.get i) = l.eraseIdx ↑i
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>ps : Set P<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ V<VAR>hd : finrank ℝ V = n<VAR>hc : Cospherical ps<VAR>sx₁ sx₂ : Simplex ℝ P n<VAR>hsx₁ : Set.range sx₁.points ⊆ ps<VAR>hsx₂ : Set.range sx₂.points ⊆ ps<GOAL>sx₁.circumradius = sx₂.circumradius
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>ps : Set P<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ V<VAR>hd : finrank ℝ V = n<VAR>hc : Cospherical ps<VAR>sx₁ sx₂ : Simplex ℝ P n<VAR>hsx₁ : Set.range sx₁.points ⊆ ps<VAR>hsx₂ : Set.range sx₂.points ⊆ ps<VAR>r : ℝ<VAR>hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r<GOAL>sx₁.circumradius = sx₂.circumradius
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>s t u v : Set α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TotallyDisconnectedSpace β<VAR>f✝ : α → β<VAR>S : Set α<VAR>hS : IsPreconnected S<VAR>T : Set β<VAR>inst✝ : DiscreteTopology ↑T<VAR>f : α → β<VAR>hc : ContinuousOn f S<VAR>hTm : MapsTo f S T<VAR>x y : α<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>F : ↑S → ↑T := MapsTo.restrict f S T hTm<GOAL>f x = f y
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>s t u v : Set α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TotallyDisconnectedSpace β<VAR>f✝ : α → β<VAR>S : Set α<VAR>hS : IsPreconnected S<VAR>T : Set β<VAR>inst✝ : DiscreteTopology ↑T<VAR>f : α → β<VAR>hc : ContinuousOn f S<VAR>hTm : MapsTo f S T<VAR>x y : α<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>F : ↑S → ↑T := MapsTo.restrict f S T hTm<GOAL>F ⟨x, hx⟩ = F ⟨y, hy⟩
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>x : S<GOAL>eval₂ f x p = eval x (map f p)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝ : IsProbabilityMeasure μ<VAR>p : α → Prop<VAR>f✝ : β → α<VAR>f : α → β<VAR>hf : AEMeasurable f μ<GOAL>(Measure.map f μ) univ = 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M₂<VAR>inst✝⁵ : AddCommGroup M₃<VAR>inst✝⁴ : AddCommGroup M₄<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module R M₃<VAR>inst✝ : Module R M₄<VAR>rs₁ rs₂ : List R<GOAL>IsWeaklyRegular M (rs₁ ++ rs₂) ↔ IsWeaklyRegular M rs₁ ∧ IsWeaklyRegular (M ⧸ Ideal.ofList rs₁ • ⊤) rs₂
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom<VAR>X : Augmented C<VAR>F : Arrow C<VAR>G : X ⟶ F.augmentedCechNerve<GOAL>(𝟭 C).map (G.left.app (Opposite.op (SimplexCategory.mk 0)) ≫ WidePullback.π (fun x => F.hom) 0) ≫ F.hom = (Augmented.toArrow.obj X).hom ≫ (𝟭 C).map G.right
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom<VAR>X : Augmented C<VAR>F : Arrow C<VAR>G : X ⟶ F.augmentedCechNerve<VAR>this : (𝟭 (SimplicialObject C)).map G.left ≫ F.augmentedCechNerve.hom = X.hom ≫ (const C).map G.right<GOAL>(𝟭 C).map (G.left.app (Opposite.op (SimplexCategory.mk 0)) ≫ WidePullback.π (fun x => F.hom) 0) ≫ F.hom = (Augmented.toArrow.obj X).hom ≫ (𝟭 C).map G.right
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : ι → Set α<GOAL>(⋃ i, s i).Nonempty ↔ ∃ i, (s i).Nonempty
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_4, u_1} C<VAR>inst✝¹ : Category.{u_5, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>E : Type u_3<VAR>inst✝ : Category.{?u.5143, u_3} E<VAR>h₁ : Localization.StrictUniversalPropertyFixedTarget L W D<VAR>h₂ : Localization.StrictUniversalPropertyFixedTarget L W W.Localization<GOAL>W.Q ⋙ 𝟭 W.Localization = W.Q ⋙ Localization.Construction.lift L ⋯ ⋙ h₂.lift W.Q ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_4, u_1} C<VAR>inst✝¹ : Category.{u_5, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>E : Type u_3<VAR>inst✝ : Category.{?u.5143, u_3} E<VAR>h₁ : Localization.StrictUniversalPropertyFixedTarget L W D<VAR>h₂ : Localization.StrictUniversalPropertyFixedTarget L W W.Localization<GOAL>L ⋙ h₂.lift W.Q ⋯ ⋙ Localization.Construction.lift L ⋯ = L ⋙ 𝟭 D
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddGroup A<VAR>inst✝ : HasShift C A<VAR>X✝ Y : C<VAR>f : X✝ ⟶ Y<VAR>n : A<VAR>X : C<GOAL>(shiftFunctor C (-n)).map ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app X) = (shiftFunctorCompIsoId C n (-n) ⋯).hom.app ((shiftFunctor C (-n)).obj X)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>n : Type u_3<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Semiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Finite n<VAR>b : Basis n R M<VAR>i : n<GOAL>b.equivFun.symm ((stdBasis R (fun x => R) i) 1) = b i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>n : Type u_3<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Semiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Finite n<VAR>b : Basis n R M<VAR>i : n<VAR>val✝ : Fintype n<GOAL>b.equivFun.symm ((stdBasis R (fun x => R) i) 1) = b i
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : NormedSpace 𝕜 E'<VAR>F : Type u_4<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>inst✝¹¹ : TopologicalSpace H<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>G : Type u_7<VAR>inst✝⁹ : TopologicalSpace G<VAR>G' : Type u_8<VAR>inst✝⁸ : TopologicalSpace G'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>J : ModelWithCorners 𝕜 F G<VAR>J' : ModelWithCorners 𝕜 F G'<VAR>M : Type u_9<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>M' : Type u_10<VAR>inst✝⁵ : TopologicalSpace M'<VAR>inst✝⁴ : ChartedSpace H' M'<VAR>N : Type u_11<VAR>inst✝³ : TopologicalSpace N<VAR>inst✝² : ChartedSpace G N<VAR>N' : Type u_12<VAR>inst✝¹ : TopologicalSpace N'<VAR>inst✝ : ChartedSpace G' N'<VAR>n m : ℕ∞<VAR>h : M ≃ₘ^n⟮I, J⟯ N<VAR>f : N → M'<VAR>s : Set M<VAR>hm : m ≤ n<VAR>x✝ : M<GOAL>x✝ ∈ s → ContMDiffWithinAt I I' m (f ∘ ⇑h) s x✝ ↔ h.toEquiv x✝ ∈ ⇑h.symm ⁻¹' s → ContMDiffWithinAt J I' m f (⇑h.symm ⁻¹' s) (h.toEquiv x✝)
<VAR>q a b c : ℚ<GOAL>-1 /. 1 = -1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hs : ∀ (s : Set X), closure (f '' s) ⊆ f '' closure s<VAR>c : Set X<VAR>hc : IsClosed c<GOAL>f '' closure c = f '' c
<VAR>n m : ℕ<VAR>inst✝ : NeZero n<GOAL>1 < last (n + 1)
<VAR>n m : ℕ<VAR>inst✝ : NeZero n<GOAL>n ≠ 0
<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 : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hs : StrictConvex ℝ s<VAR>hsc : IsClosed s<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : Integrable f μ<GOAL>f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ ⨍ (x : α), f x ∂μ ∈ interior s
<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 : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hs : StrictConvex ℝ s<VAR>hsc : IsClosed s<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : Integrable f μ<VAR>this : ∀ {t : Set α}, μ t ≠ 0 → ⨍ (x : α) in t, f x ∂μ ∈ s<GOAL>f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ ⨍ (x : α), f x ∂μ ∈ interior s
<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 : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hs : StrictConvex ℝ s<VAR>hsc : IsClosed s<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : Integrable f μ<VAR>this : ∀ {t : Set α}, μ t ≠ 0 → ⨍ (x : α) in t, f x ∂μ ∈ s<GOAL>(∃ t, MeasurableSet t ∧ μ t ≠ 0 ∧ μ tᶜ ≠ 0 ∧ ⨍ (x : α) in t, f x ∂μ ≠ ⨍ (x : α) in tᶜ, f x ∂μ) → ⨍ (x : α), f x ∂μ ∈ interior s
<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 : Set E<VAR>t✝ : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hs : StrictConvex ℝ s<VAR>hsc : IsClosed s<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : Integrable f μ<VAR>this : ∀ {t : Set α}, μ t ≠ 0 → ⨍ (x : α) in t, f x ∂μ ∈ s<VAR>t : Set α<VAR>hm : MeasurableSet t<VAR>h₀ : μ t ≠ 0<VAR>h₀' : μ tᶜ ≠ 0<VAR>hne : ⨍ (x : α) in t, f x ∂μ ≠ ⨍ (x : α) in tᶜ, f x ∂μ<GOAL>⨍ (x : α), f x ∂μ ∈ interior s
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝²⁵ : CommRing R<VAR>inst✝²⁴ : CommRing S<VAR>inst✝²³ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>inst✝²² : CommRing R'<VAR>inst✝²¹ : CommRing S'<VAR>inst✝²⁰ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝¹⁹ : Algebra R R'<VAR>inst✝¹⁸ : Algebra S S'<VAR>inst✝¹⁷ : Algebra R S'<VAR>inst✝¹⁶ : IsScalarTower R R' S'<VAR>inst✝¹⁵ : IsScalarTower R S S'<VAR>R'' : Type u''<VAR>S'' : Type v''<VAR>inst✝¹⁴ : CommRing R''<VAR>inst✝¹³ : CommRing S''<VAR>inst✝¹² : Algebra R'' S''<VAR>P'' : Generators R'' S''<VAR>inst✝¹¹ : Algebra R R''<VAR>inst✝¹⁰ : Algebra S S''<VAR>inst✝⁹ : Algebra R S''<VAR>inst✝⁸ : IsScalarTower R R'' S''<VAR>inst✝⁷ : IsScalarTower R S S''<VAR>inst✝⁶ : Algebra R' R''<VAR>inst✝⁵ : Algebra S' S''<VAR>inst✝⁴ : Algebra R' S''<VAR>inst✝³ : IsScalarTower R' R'' S''<VAR>inst✝² : IsScalarTower R' S' S''<VAR>inst✝¹ : IsScalarTower R R' R''<VAR>inst✝ : IsScalarTower S S' S''<VAR>f : P.Hom P'<VAR>x : P.Cotangent<GOAL>(CotangentSpace.map f ∘ₗ P.cotangentComplex) x = (↑S P'.cotangentComplex ∘ₗ Cotangent.map f) x
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<GOAL>s / ball x δ = x⁻¹ • thickening δ s
<VAR>p q x y : ℝ<VAR>r✝ : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>h : LiouvilleWith p x<VAR>r : ℚ<GOAL>LiouvilleWith p (x + ↑r)
<VAR>p q x y : ℝ<VAR>r✝ : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>h : LiouvilleWith p x<VAR>r : ℚ<VAR>C : ℝ<VAR>_hC₀ : 0 < C<VAR>hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p<GOAL>LiouvilleWith p (x + ↑r)
<VAR>p q x y : ℝ<VAR>r✝ : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>h : LiouvilleWith p x<VAR>r : ℚ<VAR>C : ℝ<VAR>_hC₀ : 0 < C<VAR>hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p<GOAL>∀ (x_1 : ℕ), (1 ≤ x_1 ∧ ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ p) → ∃ m, x + ↑r ≠ ↑m / ↑(r.den • id x_1) ∧ |x + ↑r - ↑m / ↑(r.den • id x_1)| < ↑r.den ^ p * C / ↑(r.den • id x_1) ^ p
<VAR>p q x y : ℝ<VAR>r✝ : ℚ<VAR>m✝ : ℤ<VAR>n✝ : ℕ<VAR>h : LiouvilleWith p x<VAR>r : ℚ<VAR>C : ℝ<VAR>_hC₀ : 0 < C<VAR>hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p<VAR>n : ℕ<VAR>hn : 1 ≤ n<VAR>m : ℤ<VAR>hne : x ≠ ↑m / ↑n<VAR>hlt : |x - ↑m / ↑n| < C / ↑n ^ p<GOAL>∃ m, x + ↑r ≠ ↑m / ↑(r.den • id n) ∧ |x + ↑r - ↑m / ↑(r.den • id n)| < ↑r.den ^ p * C / ↑(r.den • id n) ^ p
<VAR>p q x y : ℝ<VAR>r✝ : ℚ<VAR>m✝ : ℤ<VAR>n✝ : ℕ<VAR>h : LiouvilleWith p x<VAR>r : ℚ<VAR>C : ℝ<VAR>_hC₀ : 0 < C<VAR>hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p<VAR>n : ℕ<VAR>hn : 1 ≤ n<VAR>m : ℤ<VAR>hne : x ≠ ↑m / ↑n<VAR>hlt : |x - ↑m / ↑n| < C / ↑n ^ p<VAR>this : ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) = ↑m / ↑n + ↑r<GOAL>∃ m, x + ↑r ≠ ↑m / ↑(r.den • id n) ∧ |x + ↑r - ↑m / ↑(r.den • id n)| < ↑r.den ^ p * C / ↑(r.den • id n) ^ p
<VAR>p q x y : ℝ<VAR>r✝ : ℚ<VAR>m✝ : ℤ<VAR>n✝ : ℕ<VAR>h : LiouvilleWith p x<VAR>r : ℚ<VAR>C : ℝ<VAR>_hC₀ : 0 < C<VAR>hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p<VAR>n : ℕ<VAR>hn : 1 ≤ n<VAR>m : ℤ<VAR>hne : x ≠ ↑m / ↑n<VAR>hlt : |x - ↑m / ↑n| < C / ↑n ^ p<VAR>this : ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) = ↑m / ↑n + ↑r<GOAL>x + ↑r ≠ ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) ∧ |x + ↑r - ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n)| < ↑r.den ^ p * C / ↑(r.den • id n) ^ p
<VAR>p q x y : ℝ<VAR>r✝ : ℚ<VAR>m✝ : ℤ<VAR>n✝ : ℕ<VAR>h : LiouvilleWith p x<VAR>r : ℚ<VAR>C : ℝ<VAR>_hC₀ : 0 < C<VAR>hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p<VAR>n : ℕ<VAR>hn : 1 ≤ n<VAR>m : ℤ<VAR>hne : x ≠ ↑m / ↑n<VAR>hlt : |x - ↑m / ↑n| < C / ↑n ^ p<VAR>this : ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) = ↑m / ↑n + ↑r<GOAL>x + ↑r ≠ ↑m / ↑n + ↑r ∧ |x - ↑m / ↑n| < ↑r.den ^ p * C / ↑(r.den • id n) ^ p
<VAR>p q x y : ℝ<VAR>r✝ : ℚ<VAR>m✝ : ℤ<VAR>n✝ : ℕ<VAR>h : LiouvilleWith p x<VAR>r : ℚ<VAR>C : ℝ<VAR>_hC₀ : 0 < C<VAR>hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p<VAR>n : ℕ<VAR>hn : 1 ≤ n<VAR>m : ℤ<VAR>hne : x ≠ ↑m / ↑n<VAR>hlt : |x - ↑m / ↑n| < C / ↑n ^ p<VAR>this : ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) = ↑m / ↑n + ↑r<GOAL>C / ↑n ^ p = ↑r.den ^ p * C / ↑(r.den • id n) ^ p
<VAR>p q x y : ℝ<VAR>r✝ : ℚ<VAR>m✝ : ℤ<VAR>n✝ : ℕ<VAR>h : LiouvilleWith p x<VAR>r : ℚ<VAR>C : ℝ<VAR>_hC₀ : 0 < C<VAR>hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p<VAR>n : ℕ<VAR>hn : 1 ≤ n<VAR>m : ℤ<VAR>hne : x ≠ ↑m / ↑n<VAR>hlt : |x - ↑m / ↑n| < C / ↑n ^ p<VAR>this✝ : ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) = ↑m / ↑n + ↑r<VAR>this : ↑r.den ^ p ≠ 0<GOAL>C / ↑n ^ p = ↑r.den ^ p * C / ↑(r.den • id n) ^ p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α →. β<VAR>g : α → β → σ<VAR>hf : Partrec f<VAR>hg : Computable₂ g<GOAL>Partrec fun a => Part.map (g a) (f a)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>m✝ : α → β → γ<VAR>f✝ f₁ f₂ : Filter α<VAR>g✝ g₁ g₂ : Filter β<VAR>h h₁ h₂ : Filter γ<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>u : Set γ<VAR>v : Set δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>m : α → β → γ<VAR>f : Filter α<VAR>g : Filter β<GOAL>map₂ m f g = map₂ (fun a b => m b a) g f
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroup α<VAR>a✝ b✝ a b : α<GOAL>mabs (a * b) = mabs a * mabs b ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroup α<VAR>a✝ b✝ a b : α<VAR>ab : a ≤ b<GOAL>mabs (a * b) = mabs a * mabs b ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroup α<VAR>a✝ b✝ a b : α<VAR>ab : b ≤ a<GOAL>mabs (a * b) = mabs a * mabs b ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
<VAR>n : ℕ<VAR>c : Composition n<GOAL>c.length ≤ n
<VAR>n : ℕ<VAR>c : Composition n<GOAL>c.length ≤ c.blocks.sum
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝² : Category.{v', u'} A<VAR>inst✝¹ : ConcreteCategory A<VAR>F₁ F₂ F₃ : Cᵒᵖ ⥤ A<VAR>f₁ : F₁ ⟶ F₂<VAR>f₂ : F₂ ⟶ F₃<VAR>inst✝ : IsLocallySurjective J (f₁ ≫ f₂)<VAR>X : C<VAR>x : (forget A).obj (F₃.obj (op X))<GOAL>imageSieve f₂ x ∈ J.sieves X
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝² : Category.{v', u'} A<VAR>inst✝¹ : ConcreteCategory A<VAR>F₁ F₂ F₃ : Cᵒᵖ ⥤ A<VAR>f₁ : F₁ ⟶ F₂<VAR>f₂ : F₂ ⟶ F₃<VAR>inst✝ : IsLocallySurjective J (f₁ ≫ f₂)<VAR>X : C<VAR>x : (forget A).obj (F₃.obj (op X))<GOAL>imageSieve (f₁ ≫ f₂) x ≤ imageSieve f₂ x
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝² : Category.{v', u'} A<VAR>inst✝¹ : ConcreteCategory A<VAR>F₁ F₂ F₃ : Cᵒᵖ ⥤ A<VAR>f₁ : F₁ ⟶ F₂<VAR>f₂ : F₂ ⟶ F₃<VAR>inst✝ : IsLocallySurjective J (f₁ ≫ f₂)<VAR>X : C<VAR>x : (forget A).obj (F₃.obj (op X))<VAR>Y : C<VAR>g : Y ⟶ X<VAR>hg : (imageSieve (f₁ ≫ f₂) x).arrows g<GOAL>(imageSieve f₂ x).arrows g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>f : M →ₗ[R] M'<VAR>q : PolynomialModule R M<VAR>r : R<GOAL>(eval ((algebraMap R R') r)) ((map R' f) q) = f ((eval r) q)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>f : M →ₗ[R] M'<VAR>q : PolynomialModule R M<VAR>r : R<GOAL>(eval ((algebraMap R R') r)) ((map R' f) 0) = f ((eval r) 0)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>f : M →ₗ[R] M'<VAR>q : PolynomialModule R M<VAR>r : R<GOAL>∀ (f_1 g : PolynomialModule R M), (eval ((algebraMap R R') r)) ((map R' f) f_1) = f ((eval r) f_1) → (eval ((algebraMap R R') r)) ((map R' f) g) = f ((eval r) g) → (eval ((algebraMap R R') r)) ((map R' f) (f_1 + g)) = f ((eval r) (f_1 + g))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R' M'<VAR>inst✝² : Algebra R R'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : IsScalarTower R R' M'<VAR>f : M →ₗ[R] M'<VAR>q : PolynomialModule R M<VAR>r : R<GOAL>∀ (a : ℕ) (b : M), (eval ((algebraMap R R') r)) ((map R' f) ((single R a) b)) = f ((eval r) ((single R a) b))
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X✝ Y✝ : Ω → ℝ<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace β<VAR>X Y : Ω → β<VAR>inst✝¹ : NormedDivisionRing β<VAR>inst✝ : BorelSpace β<VAR>hXY : IndepFun X Y μ<VAR>h'XY : Integrable (X * Y) μ<VAR>hX : AEStronglyMeasurable X μ<VAR>hY : AEStronglyMeasurable Y μ<VAR>h'Y : ¬Y =ᶠ[ae μ] 0<GOAL>HasFiniteIntegral X μ
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X✝ Y✝ : Ω → ℝ<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace β<VAR>X Y : Ω → β<VAR>inst✝¹ : NormedDivisionRing β<VAR>inst✝ : BorelSpace β<VAR>hXY : IndepFun X Y μ<VAR>h'XY : Integrable (X * Y) μ<VAR>hX : AEStronglyMeasurable X μ<VAR>hY : AEStronglyMeasurable Y μ<VAR>h'Y : ¬Y =ᶠ[ae μ] 0<VAR>I : ∫⁻ (ω : Ω), ↑‖Y ω‖₊ ∂μ ≠ 0<GOAL>HasFiniteIntegral X μ
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X✝ Y✝ : Ω → ℝ<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace β<VAR>X Y : Ω → β<VAR>inst✝¹ : NormedDivisionRing β<VAR>inst✝ : BorelSpace β<VAR>hXY : IndepFun X Y μ<VAR>h'XY : Integrable (X * Y) μ<VAR>hX : AEStronglyMeasurable X μ<VAR>hY : AEStronglyMeasurable Y μ<VAR>h'Y : ¬Y =ᶠ[ae μ] 0<VAR>I : ∫⁻ (ω : Ω), ↑‖Y ω‖₊ ∂μ ≠ 0<VAR>H : ∫⁻ (a : Ω), ↑‖X a‖₊ ∂μ = ⊤<GOAL>False
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X✝ Y✝ : Ω → ℝ<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace β<VAR>X Y : Ω → β<VAR>inst✝¹ : NormedDivisionRing β<VAR>inst✝ : BorelSpace β<VAR>hXY : IndepFun X Y μ<VAR>h'XY : Integrable (X * Y) μ<VAR>hX : AEStronglyMeasurable X μ<VAR>hY : AEStronglyMeasurable Y μ<VAR>h'Y : ¬Y =ᶠ[ae μ] 0<VAR>I : ∫⁻ (ω : Ω), ↑‖Y ω‖₊ ∂μ ≠ 0<VAR>H : ∫⁻ (a : Ω), ↑‖X a‖₊ ∂μ = ⊤<VAR>J : IndepFun (fun ω => ↑‖X ω‖₊) (fun ω => ↑‖Y ω‖₊) μ<GOAL>False
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X✝ Y✝ : Ω → ℝ<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace β<VAR>X Y : Ω → β<VAR>inst✝¹ : NormedDivisionRing β<VAR>inst✝ : BorelSpace β<VAR>hXY : IndepFun X Y μ<VAR>h'XY : Integrable (X * Y) μ<VAR>hX : AEStronglyMeasurable X μ<VAR>hY : AEStronglyMeasurable Y μ<VAR>h'Y : ¬Y =ᶠ[ae μ] 0<VAR>I : ∫⁻ (ω : Ω), ↑‖Y ω‖₊ ∂μ ≠ 0<VAR>H : ∫⁻ (a : Ω), ↑‖X a‖₊ ∂μ = ⊤<VAR>J : IndepFun (fun ω => ↑‖X ω‖₊) (fun ω => ↑‖Y ω‖₊) μ<VAR>A : ∫⁻ (ω : Ω), ↑‖X ω * Y ω‖₊ ∂μ < ⊤<GOAL>False
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X✝ Y✝ : Ω → ℝ<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace β<VAR>X Y : Ω → β<VAR>inst✝¹ : NormedDivisionRing β<VAR>inst✝ : BorelSpace β<VAR>hXY : IndepFun X Y μ<VAR>h'XY : Integrable (X * Y) μ<VAR>hX : AEStronglyMeasurable X μ<VAR>hY : AEStronglyMeasurable Y μ<VAR>h'Y : ¬Y =ᶠ[ae μ] 0<VAR>I : ∫⁻ (ω : Ω), ↑‖Y ω‖₊ ∂μ ≠ 0<VAR>H : ∫⁻ (a : Ω), ↑‖X a‖₊ ∂μ = ⊤<VAR>J : IndepFun (fun ω => ↑‖X ω‖₊) (fun ω => ↑‖Y ω‖₊) μ<VAR>A : ∫⁻ (ω : Ω), ↑‖X ω‖₊ * ↑‖Y ω‖₊ ∂μ < ⊤<GOAL>False
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X✝ Y✝ : Ω → ℝ<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace β<VAR>X Y : Ω → β<VAR>inst✝¹ : NormedDivisionRing β<VAR>inst✝ : BorelSpace β<VAR>hXY : IndepFun X Y μ<VAR>h'XY : Integrable (X * Y) μ<VAR>hX : AEStronglyMeasurable X μ<VAR>hY : AEStronglyMeasurable Y μ<VAR>h'Y : ¬Y =ᶠ[ae μ] 0<VAR>I : ∫⁻ (ω : Ω), ↑‖Y ω‖₊ ∂μ ≠ 0<VAR>H : ∫⁻ (a : Ω), ↑‖X a‖₊ ∂μ = ⊤<VAR>J : IndepFun (fun ω => ↑‖X ω‖₊) (fun ω => ↑‖Y ω‖₊) μ<VAR>A : ⊤ * ∫⁻ (ω : Ω), ↑‖Y ω‖₊ ∂μ < ⊤<GOAL>False