ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>f g : α → ℝ≥0∞<VAR>hg : AEMeasurable g (μ.restrict s)<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x<VAR>f' : α → ℝ≥0∞<VAR>hf'm : Measurable f'<VAR>hle : f' ≤ f<VAR>hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ<GOAL>∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>f g : α → ℝ≥0∞<VAR>hg : AEMeasurable g (μ.restrict s)<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x<VAR>f' : α → ℝ≥0∞<VAR>hf'm : Measurable f'<VAR>hle : f' ≤ f<VAR>hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ<GOAL>∫⁻ (a : α) in s, f' a ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>f g : α → ℝ≥0∞<VAR>hg : AEMeasurable g (μ.restrict s)<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x<VAR>f' : α → ℝ≥0∞<VAR>hf'm : Measurable f'<VAR>hle : f' ≤ f<VAR>hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ<GOAL>∀ᵐ (a : α) ∂μ.restrict s, f' a ≤ g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>f g : α → ℝ≥0∞<VAR>hg : AEMeasurable g (μ.restrict s)<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x<VAR>f' : α → ℝ≥0∞<VAR>hf'm : Measurable f'<VAR>hle : f' ≤ f<VAR>hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ<GOAL>∀ᵐ (x : α) ∂μ, x ∈ s → f' x ≤ g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>f g : α → ℝ≥0∞<VAR>hg : AEMeasurable g (μ.restrict s)<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x<VAR>f' : α → ℝ≥0∞<VAR>hf'm : Measurable f'<VAR>hle : f' ≤ f<VAR>hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ<GOAL>NullMeasurableSet {x | f' x ≤ g x} (μ.restrict s)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : Nontrivial R<VAR>inst✝¹¹ : StarRing R<VAR>inst✝¹⁰ : MetricSpace R<VAR>inst✝⁹ : TopologicalRing R<VAR>inst✝⁸ : ContinuousStar R<VAR>inst✝⁷ : TopologicalSpace A<VAR>inst✝⁶ : NonUnitalRing A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : IsScalarTower R A A<VAR>inst✝² : SMulCommClass R A A<VAR>inst✝¹ : NonUnitalContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>hf✝ : autoParam (ContinuousOn f (σₙ R a)) _auto✝<VAR>hf0 : autoParam (f 0 = 0) _auto✝<VAR>hg : autoParam (ContinuousOn g (σₙ R a)) _auto✝<VAR>hg0 : autoParam (g 0 = 0) _auto✝<VAR>inst✝ : UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>hf : autoParam (ContinuousOn f ((fun x => -x) '' σₙ R a)) _auto✝<VAR>h0 : autoParam (f 0 = 0) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>cfcₙ (fun x => f (-x)) a = cfcₙ f (-a)
<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>f : ι → α<VAR>g : α → Set β<GOAL>⋂ x, ⋂ y, ⋂ (_ : f y = x), g x = ⋂ y, g (f y)
<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>ha : a ≠ 0<GOAL>(C b * X + C c).degree < (C a * X ^ 2).degree
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n✝ m : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>inst✝ : Nontrivial R<VAR>s : σ<VAR>n : ℕ<GOAL>(X s ^ n).totalDegree = n
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>κ : Type u_3<VAR>κ' : Type u_4<VAR>R : Type u_5<VAR>M : Type u_6<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>R₂ : Type u_7<VAR>M₂ : Type u_8<VAR>inst✝⁷ : CommRing R₂<VAR>inst✝⁶ : AddCommGroup M₂<VAR>inst✝⁵ : Module R₂ M₂<VAR>e : Basis ι R M<VAR>v : ι' → M<VAR>i : ι<VAR>j : ι'<VAR>R₁ : Type u_9<VAR>S : Type u_10<VAR>inst✝⁴ : CommRing R₁<VAR>inst✝³ : Ring S<VAR>inst✝² : Algebra R₁ S<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>x : S<VAR>b : Basis ι R₁ S<VAR>w : ι → S<VAR>i✝ j✝ : ι<GOAL>b.toMatrix (x • w) i✝ j✝ = ((Algebra.leftMulMatrix b) x * b.toMatrix w) i✝ j✝
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>κ : Type u_3<VAR>κ' : Type u_4<VAR>R : Type u_5<VAR>M : Type u_6<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>R₂ : Type u_7<VAR>M₂ : Type u_8<VAR>inst✝⁷ : CommRing R₂<VAR>inst✝⁶ : AddCommGroup M₂<VAR>inst✝⁵ : Module R₂ M₂<VAR>e : Basis ι R M<VAR>v : ι' → M<VAR>i : ι<VAR>j : ι'<VAR>R₁ : Type u_9<VAR>S : Type u_10<VAR>inst✝⁴ : CommRing R₁<VAR>inst✝³ : Ring S<VAR>inst✝² : Algebra R₁ S<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>x : S<VAR>b : Basis ι R₁ S<VAR>w : ι → S<VAR>i✝ j✝ : ι<GOAL>((Algebra.leftMulMatrix b) x *ᵥ ⇑(b.repr (w j✝))) i✝ = ((Algebra.leftMulMatrix b) x * b.toMatrix w) i✝ j✝
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V<VAR>f g : V →ₗ[K] V<VAR>h : Commute f g<VAR>h' : Disjoint (ker f) (ker g)<GOAL>ker (f ∘ₗ g) = ker f ⊔ ker g
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V<VAR>f g : V →ₗ[K] V<VAR>h : Commute f g<VAR>h' : Disjoint (ker f) (ker g)<GOAL>∀ (x : V), f x = 0 → f (g x) = 0
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V<VAR>f g : V →ₗ[K] V<VAR>h : Commute f g<VAR>h' : Disjoint (ker f) (ker g)<VAR>x : V<VAR>hx : f x = 0<GOAL>f (g x) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifIntegrable f p μ<VAR>hg : UnifIntegrable g p μ<VAR>hp : 1 ≤ p<VAR>hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ<GOAL>UnifIntegrable (f - g) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifIntegrable f p μ<VAR>hg : UnifIntegrable g p μ<VAR>hp : 1 ≤ p<VAR>hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ<GOAL>UnifIntegrable (f + -g) p μ
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I✝ : Box ι<VAR>i✝ : ι<VAR>x✝ : ℝ<VAR>y : ι → ℝ<VAR>I : Box ι<VAR>i : ι<VAR>x : ℝ<GOAL>I.splitLower i x ≠ I.splitUpper i x
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I✝ : Box ι<VAR>i✝ : ι<VAR>x✝ : ℝ<VAR>y : ι → ℝ<VAR>I : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>h : x ≤ I.lower i<GOAL>I.splitLower i x ≠ I.splitUpper i x
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I✝ : Box ι<VAR>i✝ : ι<VAR>x✝ : ℝ<VAR>y : ι → ℝ<VAR>I : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>h✝ : I.lower i < x<GOAL>I.splitLower i x ≠ I.splitUpper i x
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>W✝ W : Subspace K V<VAR>x : Module.Dual K ↥W<GOAL>(dualRestrict W ∘ₗ W.dualLift) x = x
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>W✝ W : Subspace K V<VAR>x : Module.Dual K ↥W<GOAL>1 x = x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>n : ℕ∞<VAR>f : E → F →L[𝕜] G<VAR>inst✝ : FiniteDimensional 𝕜 F<GOAL>ContDiff 𝕜 n f ↔ ∀ (y : F), ContDiff 𝕜 n fun x => (f x) y
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>p : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : Fintype p<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : NonUnitalRing R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : NoZeroDivisors R<VAR>v : n → R<GOAL>(∀ i ∈ Finset.univ, v i * star (v i) = 0) ↔ v = 0
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f✝ g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>inst✝ : FiniteDimensional ℝ F<VAR>f : E → F<VAR>h : LipschitzWith C f<GOAL>∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ f x
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f✝ g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>inst✝ : FiniteDimensional ℝ F<VAR>f : E → F<VAR>h : LipschitzOnWith C f univ<GOAL>∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ f x
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : FunLike F G H<VAR>a : G<VAR>b : H<VAR>inst✝² : AddCommSemigroup G<VAR>inst✝¹ : Add H<VAR>inst✝ : AddConstMapClass F G H a b<VAR>f : F<VAR>x : G<GOAL>f (a + x) = f x + b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>s s₁ : Finset β<VAR>f✝ f g : β → α<VAR>hfg : ∀ a ∈ s₁, f a = g a<GOAL>s₁.lcm f = s₁.lcm g
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<GOAL>W.φ 3 = C X * C W.Ψ₃ ^ 2 - C W.preΨ₄ * W.ψ₂ ^ 2
<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>val✝¹ : α →ₘ[μ] E<VAR>property✝¹ : val✝¹ ∈ Lp E p μ<VAR>val✝ : α →ₘ[μ] E<VAR>property✝ : val✝ ∈ Lp E p μ<VAR>h : ↑↑⟨val✝¹, property✝¹⟩ =ᶠ[ae μ] ↑↑⟨val✝, property✝⟩<GOAL>⟨val✝¹, property✝¹⟩ = ⟨val✝, property✝⟩
<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>val✝¹ : α →ₘ[μ] E<VAR>property✝¹ : val✝¹ ∈ Lp E p μ<VAR>val✝ : α →ₘ[μ] E<VAR>property✝ : val✝ ∈ Lp E p μ<VAR>h : ↑↑⟨val✝¹, property✝¹⟩ =ᶠ[ae μ] ↑↑⟨val✝, property✝⟩<GOAL>val✝¹ = val✝
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M✝ : Matrix n n R<VAR>inst✝ : Nonempty n<VAR>M : Matrix n n R<GOAL>M.trace = -M.charpoly.coeff (Fintype.card n - 1)
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M✝ : Matrix n n R<VAR>inst✝ : Nonempty n<VAR>M : Matrix n n R<GOAL>∑ i : n, M.diag i = ∑ i : n, M i i
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ a b c : α<VAR>h : c < 0<GOAL>(fun x => c * x) ⁻¹' Ioc a b = Ico (b / c) (a / c)
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>X✝ Y✝ Z✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>inst✝³ : HasImage f✝<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>inst✝² : HasImage f<VAR>g : Y ⟶ Z<VAR>inst✝¹ : HasImage g<VAR>sq : Arrow.mk f ⟶ Arrow.mk g<VAR>inst✝ : HasImageMap sq<GOAL>(imageSubobjectIso (Arrow.mk f).hom).hom ≫ image.map sq = imageSubobjectMap sq ≫ (imageSubobjectIso g).hom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Mul α<VAR>a b : α<GOAL>some a * some b = some (a * b)
<VAR>α : Type u<VAR>n : ℕ<GOAL>toPartENat ↑n = ↑n
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>θ : Real.Angle<GOAL>(o.kahler ((o.rotation θ) x)) y = ↑(-θ).expMapCircle * (o.kahler x) y
<VAR>p n k : ℕ<VAR>p_large : n < p ^ 2<GOAL>(n.choose k).factorization p ≤ 1
<VAR>p n k : ℕ<VAR>p_large : n < p ^ 2<GOAL>log p n ≤ 1
<VAR>p k : ℕ<VAR>p_large : 0 < p ^ 2<GOAL>log p 0 ≤ 1
<VAR>p n k : ℕ<VAR>p_large : n < p ^ 2<VAR>hn0 : n ≠ 0<GOAL>log p n ≤ 1
<VAR>C : Type u₁<VAR>inst✝¹⁰ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>D : Type u₂<VAR>inst✝⁹ : Category.{v₂, u₂} D<VAR>K : GrothendieckTopology D<VAR>e : C ≌ D<VAR>G : D ⥤ C<VAR>A : Type u₃<VAR>inst✝⁸ : Category.{v₃, u₃} A<VAR>inst✝⁷ : EssentiallySmall.{w, v₁, u₁} C<VAR>B : Type u_1<VAR>inst✝⁶ : Category.{?u.110647, u_1} B<VAR>F : A ⥤ B<VAR>inst✝⁵ : HasSheafify ((equivSmallModel C).inverse.inducedTopology J) A<VAR>inst✝⁴ : ((equivSmallModel C).inverse.inducedTopology J).HasSheafCompose F<VAR>inst✝³ : G.IsCoverDense J<VAR>inst✝² : G.IsContinuous K J<VAR>inst✝¹ : G.Full<VAR>inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj<VAR>P Q : Cᵒᵖ ⥤ A<VAR>f : P ⟶ Q<GOAL>K.W (whiskerLeft G.op f) ↔ J.W f
<VAR>C : Type u₁<VAR>inst✝¹⁰ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>D : Type u₂<VAR>inst✝⁹ : Category.{v₂, u₂} D<VAR>K : GrothendieckTopology D<VAR>e : C ≌ D<VAR>G : D ⥤ C<VAR>A : Type u₃<VAR>inst✝⁸ : Category.{v₃, u₃} A<VAR>inst✝⁷ : EssentiallySmall.{w, v₁, u₁} C<VAR>B : Type u_1<VAR>inst✝⁶ : Category.{?u.110647, u_1} B<VAR>F : A ⥤ B<VAR>inst✝⁵ : HasSheafify ((equivSmallModel C).inverse.inducedTopology J) A<VAR>inst✝⁴ : ((equivSmallModel C).inverse.inducedTopology J).HasSheafCompose F<VAR>inst✝³ : G.IsCoverDense J<VAR>inst✝² : G.IsContinuous K J<VAR>inst✝¹ : G.Full<VAR>inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj<VAR>P Q : Cᵒᵖ ⥤ A<VAR>f : P ⟶ Q<GOAL>K.W (whiskerLeft G.op f) ↔ K.W.inverseImage ((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op) f
<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>r✝ : α → β → Prop<VAR>p : β → γ → Prop<VAR>q : γ → δ → Prop<VAR>r : α → Prop → Prop<VAR>this : (fun x x_1 => x ↔ x_1) = fun x x_1 => x = x_1<GOAL>(r ∘r fun x x_1 => x ↔ x_1) = r
<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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ p₄ : P<VAR>h : Cospherical {p₁, p₂, p₃, p₄}<VAR>hp₂p₁ : p₂ ≠ p₁<VAR>hp₂p₄ : p₂ ≠ p₄<VAR>hp₃p₁ : p₃ ≠ p₁<VAR>hp₃p₄ : p₃ ≠ p₄<GOAL>2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
<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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ p₄ : P<VAR>h : Cospherical {p₁, p₂, p₃, p₄}<VAR>hp₂p₁ : p₂ ≠ p₁<VAR>hp₂p₄ : p₂ ≠ p₄<VAR>hp₃p₁ : p₃ ≠ p₁<VAR>hp₃p₄ : p₃ ≠ p₄<VAR>s : Sphere P<VAR>hs : {p₁, p₂, p₃, p₄} ⊆ Metric.sphere s.center s.radius<GOAL>2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
<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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ p₄ : P<VAR>h : Cospherical {p₁, p₂, p₃, p₄}<VAR>hp₂p₁ : p₂ ≠ p₁<VAR>hp₂p₄ : p₂ ≠ p₄<VAR>hp₃p₁ : p₃ ≠ p₁<VAR>hp₃p₄ : p₃ ≠ p₄<VAR>s : Sphere P<VAR>hs : p₁ ∈ s ∧ p₂ ∈ s ∧ p₃ ∈ s ∧ p₄ ∈ s<GOAL>2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R✝ : Type u_4<VAR>S : Type u_5<VAR>π : ι → Type u_6<VAR>R : Type u_7<VAR>inst✝¹ : StrictOrderedSemiring R<VAR>inst✝ : Archimedean R<VAR>s : ℕ → Set α<GOAL>limsup s atTop = {ω | Tendsto (fun n => ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) atTop atTop}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R✝ : Type u_4<VAR>S : Type u_5<VAR>π : ι → Type u_6<VAR>R : Type u_7<VAR>inst✝¹ : StrictOrderedSemiring R<VAR>inst✝ : Archimedean R<VAR>s : ℕ → Set α<GOAL>{ω | Tendsto (fun n => ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) atTop atTop} = {ω | Tendsto (fun n => ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) atTop atTop}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R✝ : Type u_4<VAR>S : Type u_5<VAR>π : ι → Type u_6<VAR>R : Type u_7<VAR>inst✝¹ : StrictOrderedSemiring R<VAR>inst✝ : Archimedean R<VAR>s : ℕ → Set α<VAR>ω : α<GOAL>ω ∈ {ω | Tendsto (fun n => ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) atTop atTop} ↔ ω ∈ {ω | Tendsto (fun n => ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) atTop atTop}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R✝ : Type u_4<VAR>S : Type u_5<VAR>π : ι → Type u_6<VAR>R : Type u_7<VAR>inst✝¹ : StrictOrderedSemiring R<VAR>inst✝ : Archimedean R<VAR>s : ℕ → Set α<VAR>ω : α<GOAL>Tendsto (fun n => ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) atTop atTop ↔ Tendsto (fun n => ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1 ω) atTop atTop
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>d : ℝ<VAR>hd : 0 < d<VAR>x : X<GOAL>μH[d] {x} = 0
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>d : ℝ<VAR>hd : 0 < d<VAR>x : X<GOAL>⨆ r, ⨆ (_ : 0 < r), ⨅ t, ⨅ (_ : {x} ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), diam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), diam (t n) ^ d ≤ 0
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>d : ℝ<VAR>hd : 0 < d<VAR>x : X<VAR>ε : ℝ≥0∞<VAR>x✝ : 0 < ε<GOAL>{x} ⊆ ⋃ n, (fun x_1 => {x}) n
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>d : ℝ<VAR>hd : 0 < d<VAR>x : X<VAR>ε : ℝ≥0∞<VAR>x✝¹ : 0 < ε<VAR>x✝ : ℕ<GOAL>diam ((fun x_1 => {x}) x✝) ≤ ε
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>d : ℝ<VAR>hd : 0 < d<VAR>x : X<VAR>ε : ℝ≥0∞<VAR>x✝ : 0 < ε<GOAL>∑' (n : ℕ), ⨆ (_ : ((fun x_1 => {x}) n).Nonempty), diam ((fun x_2 => {x}) n) ^ d ≤ 0
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z✝ : ι → E<VAR>s : Finset ι<VAR>w₁ w₂ : ι → R<VAR>z : ι → E<VAR>hw₁ : ∑ i ∈ s, w₁ i = 1<VAR>hw₂ : ∑ i ∈ s, w₂ i = 1<VAR>a b : R<VAR>hab : a + b = 1<GOAL>a • s.centerMass w₁ z + b • s.centerMass w₂ z = s.centerMass (fun i => a * w₁ i + b * w₂ i) z
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z✝ : ι → E<VAR>s : Finset ι<VAR>w₁ w₂ : ι → R<VAR>z : ι → E<VAR>hw₁ : ∑ i ∈ s, w₁ i = 1<VAR>hw₂ : ∑ i ∈ s, w₂ i = 1<VAR>a b : R<VAR>hab : a + b = 1<VAR>hw : ∑ i ∈ s, (a * w₁ i + b * w₂ i) = 1<GOAL>a • s.centerMass w₁ z + b • s.centerMass w₂ z = s.centerMass (fun i => a * w₁ i + b * w₂ i) z
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>toIocDiv hp a b = -⌊(a + p - b) / p⌋
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>b - -⌊(a + p - b) / p⌋ • p ∈ Set.Ioc a (a + p)
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>a < b + ↑⌊(a + p - b) / p⌋ * p ∧ 0 ≤ a + p - b - ↑⌊(a + p - b) / p⌋ * p
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>a < b + ↑⌊(a + p - b) / p⌋ * p
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>a + p - b - ↑⌊(a + p - b) / p⌋ * p < p
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>i : ι<GOAL>v i ≠ 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>i : ι<VAR>this : ‖v i‖ ≠ 0<GOAL>v i ≠ 0
<VAR>α : Type u_1<VAR>inst✝⁵ : AddCommSemigroup α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>ha : AddLECancellable a<VAR>h : a ≤ c<GOAL>b ≤ c - a ↔ b + a ≤ c
<VAR>α : Type u_1<VAR>inst✝⁵ : AddCommSemigroup α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>ha : AddLECancellable a<VAR>h : a ≤ c<GOAL>b ≤ c - a ↔ a + b ≤ c
<VAR>ι : Type u<VAR>ι' : Type w<VAR>f : ι → Cardinal.{v}<VAR>c : Cardinal.{v}<GOAL>(⨆ i, f i) * c = ⨆ i, f i * c
<VAR>ι : Type u<VAR>ι' : Type w<VAR>f : ι → Cardinal.{v}<VAR>c : Cardinal.{v}<VAR>h✝ : IsEmpty ι<GOAL>(⨆ i, f i) * c = ⨆ i, f i * c
<VAR>ι : Type u<VAR>ι' : Type w<VAR>f : ι → Cardinal.{v}<VAR>c : Cardinal.{v}<VAR>h✝ : Nonempty ι<GOAL>(⨆ i, f i) * c = ⨆ i, f i * c
<VAR>ι : Type u<VAR>ι' : Type w<VAR>f : ι → Cardinal.{v}<VAR>h✝ : Nonempty ι<GOAL>(⨆ i, f i) * 0 = ⨆ i, f i * 0
<VAR>ι : Type u<VAR>ι' : Type w<VAR>f : ι → Cardinal.{v}<VAR>c : Cardinal.{v}<VAR>h✝ : Nonempty ι<VAR>h0 : c ≠ 0<GOAL>(⨆ i, f i) * c = ⨆ i, f i * c
<VAR>ι : Type u<VAR>ι' : Type w<VAR>f : ι → Cardinal.{v}<VAR>c : Cardinal.{v}<VAR>h✝ : Nonempty ι<VAR>h0 : c ≠ 0<VAR>hf : BddAbove (range f)<GOAL>(⨆ i, f i) * c = ⨆ i, f i * c
<VAR>ι : Type u<VAR>ι' : Type w<VAR>f : ι → Cardinal.{v}<VAR>c : Cardinal.{v}<VAR>h✝ : Nonempty ι<VAR>h0 : c ≠ 0<VAR>hf : BddAbove (range f)<VAR>this : ∀ (i : ι), f i * c ≤ (⨆ i, f i) * c<GOAL>(⨆ i, f i) * c = ⨆ i, f i * c
<VAR>ι : Type u<VAR>ι' : Type w<VAR>f : ι → Cardinal.{v}<VAR>c : Cardinal.{v}<VAR>h✝ : Nonempty ι<VAR>h0 : c ≠ 0<VAR>hf : BddAbove (range f)<VAR>this : ∀ (i : ι), f i * c ≤ (⨆ i, f i) * c<GOAL>(⨆ i, f i) * c ≤ ⨆ i, f i * c
<VAR>ι : Type u<VAR>ι' : Type w<VAR>f : ι → Cardinal.{v}<VAR>c : Cardinal.{v}<VAR>h✝ : Nonempty ι<VAR>h0 : c ≠ 0<VAR>hf : BddAbove (range f)<VAR>this : ∀ (i : ι), f i * c ≤ (⨆ i, f i) * c<VAR>bdd : BddAbove (range fun x => f x * c)<GOAL>(⨆ i, f i) * c ≤ ⨆ i, f i * c
<VAR>ι : Type u<VAR>ι' : Type w<VAR>f : ι → Cardinal.{v}<VAR>c : Cardinal.{v}<VAR>h✝ : Nonempty ι<VAR>h0 : c ≠ 0<VAR>hf : BddAbove (range f)<VAR>this : ∀ (i : ι), f i * c ≤ (⨆ i, f i) * c<VAR>bdd : BddAbove (range fun x => f x * c)<VAR>hs : ⨆ i, f i < ℵ₀<GOAL>(⨆ i, f i) * c ≤ ⨆ i, f i * c
<VAR>ι : Type u<VAR>ι' : Type w<VAR>f : ι → Cardinal.{v}<VAR>c : Cardinal.{v}<VAR>h✝ : Nonempty ι<VAR>h0 : c ≠ 0<VAR>hf : BddAbove (range f)<VAR>this : ∀ (i : ι), f i * c ≤ (⨆ i, f i) * c<VAR>bdd : BddAbove (range fun x => f x * c)<VAR>hs : ℵ₀ ≤ ⨆ i, f i<GOAL>(⨆ i, f i) * c ≤ ⨆ i, f i * c