ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>f g : X → ℝ<VAR>s t : Set X<VAR>hf : IntegrableOn f s μ<VAR>hg : IntegrableOn g s μ<VAR>hs : MeasurableSet s<VAR>h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x<GOAL>f ≤ᶠ[ae (μ.restrict s)] g
<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>f : ℕ → β<VAR>n : ℕ<GOAL>∏ k ∈ range (n + 1 + 1), f k = (∏ k ∈ range (n + 1), f (k + 1)) * f 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : Nontrivial R<VAR>inst✝¹¹ : StarRing R<VAR>inst✝¹⁰ : MetricSpace R<VAR>inst✝⁹ : TopologicalSemiring R<VAR>inst✝⁸ : ContinuousStar R<VAR>inst✝⁷ : NonUnitalRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : TopologicalSpace 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>ha✝ : autoParam (p a) _auto✝<VAR>inst✝ : UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>h_spec : σₙ R a ⊆ {0}<VAR>ha : autoParam (p a) _auto✝<GOAL>a = 0
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>x : ↑↑X.toPresheafedSpace<VAR>hx : x ∈ U<VAR>y : PrimeSpectrum ↑Γ(X, U) := hU.primeIdealOf ⟨x, hx⟩<VAR>hy : y = hU.primeIdealOf ⟨x, hx⟩<GOAL>IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hx⟩)) y.asIdeal
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>x : ↑↑X.toPresheafedSpace<VAR>hx : x ∈ U<VAR>y : PrimeSpectrum ↑Γ(X, U) := hU.primeIdealOf ⟨x, hx⟩<VAR>hy : y = hU.primeIdealOf ⟨x, hx⟩<VAR>this : hU.fromSpec.val.base y = x<GOAL>IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hx⟩)) y.asIdeal
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>y : PrimeSpectrum ↑Γ(X, U)<VAR>hx : hU.fromSpec.val.base y ∈ U<VAR>hy : y = hU.primeIdealOf ⟨hU.fromSpec.val.base y, hx⟩<GOAL>IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨hU.fromSpec.val.base y, hx⟩)) y.asIdeal
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<GOAL>𝟙 0 = 0
<VAR>a x z : ℂ<VAR>r : ℝ<VAR>hr : 0 < r<VAR>θ : ℝ<VAR>hθ : θ ∈ Ioc (-π) π<GOAL>(↑r * (cos ↑θ + sin ↑θ * I)).arg = θ
<VAR>a x z : ℂ<VAR>r : ℝ<VAR>hr : 0 < r<VAR>θ : ℝ<VAR>hθ : θ ∈ Ioc (-π) π<GOAL>(if 0 ≤ (↑r * (cos ↑θ + sin ↑θ * I)).re then Real.arcsin ((↑r * (cos ↑θ + sin ↑θ * I)).im / r) else if 0 ≤ (↑r * (cos ↑θ + sin ↑θ * I)).im then Real.arcsin ((-(↑r * (cos ↑θ + sin ↑θ * I))).im / r) + π else Real.arcsin ((-(↑r * (cos ↑θ + sin ↑θ * I))).im / r) - π) = θ
<VAR>a x z : ℂ<VAR>r : ℝ<VAR>hr : 0 < r<VAR>θ : ℝ<VAR>hθ : θ ∈ Ioc (-π) π<GOAL>(if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ) else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) = θ
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasShift C ℤ<VAR>T₁ T₂ T₃ A B : Triangle C<VAR>e : A ≅ B<GOAL>e.hom.hom₃ ≫ e.inv.hom₃ = 𝟙 A.obj₃
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>Γ : Type u_1<VAR>Γ₁ : Type u_2<VAR>Γ₂ : Type u_3<VAR>inst✝² : LinearOrderedCommGroupWithZero Γ<VAR>inst✝¹ : LinearOrderedCommGroupWithZero Γ₁<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₂<VAR>v : Valuation K Γ<VAR>v₁ : Valuation K Γ₁<VAR>v₂ : Valuation K Γ₂<GOAL>v.IsEquiv v.valuationSubring.valuation
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>Γ : Type u_1<VAR>Γ₁ : Type u_2<VAR>Γ₂ : Type u_3<VAR>inst✝² : LinearOrderedCommGroupWithZero Γ<VAR>inst✝¹ : LinearOrderedCommGroupWithZero Γ₁<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₂<VAR>v : Valuation K Γ<VAR>v₁ : Valuation K Γ₁<VAR>v₂ : Valuation K Γ₂<GOAL>∀ {x : K}, v x ≤ 1 ↔ v.valuationSubring.valuation x ≤ 1
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>Γ : Type u_1<VAR>Γ₁ : Type u_2<VAR>Γ₂ : Type u_3<VAR>inst✝² : LinearOrderedCommGroupWithZero Γ<VAR>inst✝¹ : LinearOrderedCommGroupWithZero Γ₁<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₂<VAR>v : Valuation K Γ<VAR>v₁ : Valuation K Γ₁<VAR>v₂ : Valuation K Γ₂<VAR>x : K<GOAL>v x ≤ 1 ↔ v.valuationSubring.valuation x ≤ 1
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>Γ : Type u_1<VAR>Γ₁ : Type u_2<VAR>Γ₂ : Type u_3<VAR>inst✝² : LinearOrderedCommGroupWithZero Γ<VAR>inst✝¹ : LinearOrderedCommGroupWithZero Γ₁<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₂<VAR>v : Valuation K Γ<VAR>v₁ : Valuation K Γ₁<VAR>v₂ : Valuation K Γ₂<VAR>x : K<GOAL>v x ≤ 1 ↔ x ∈ v.valuationSubring
<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>s : Sphere P<VAR>p : P<VAR>v : V<GOAL>s.secondInter p v ∈ s ↔ p ∈ s
<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>inst✝ : HasDerivedCategory C<VAR>β : Ext 0 Y n := 0<GOAL>hom 0 = 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>inst✝ : HasDerivedCategory C<VAR>β : Ext 0 Y n := 0<VAR>hβ : β.hom = 0<GOAL>hom 0 = 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>inst✝ : HasDerivedCategory C<VAR>β : Ext 0 Y n := 0<VAR>hβ : β.hom = 0<VAR>this : 0 = comp 0 β ⋯<GOAL>hom 0 = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>f : M →ₗ[R] M'<VAR>hfv : LinearIndependent R (⇑f ∘ v)<VAR>s : Finset ι<VAR>g : ι → R<VAR>hg : ∑ i ∈ s, g i • v i = 0<VAR>i : ι<VAR>his : i ∈ s<GOAL>∑ i ∈ s, g i • f (v i) = 0
<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 c✝ d✝ : ℝ<VAR>f : ℝ → E<VAR>c d : ℝ<GOAL>c • ∫ (x : ℝ) in a..b, f (d - c * x) = ∫ (x : ℝ) in d - c * b..d - c * a, f x
<VAR>S : Type u'<VAR>T : Type u''<VAR>R : Type u<VAR>M : Type v<VAR>inst✝¹ : Group R<VAR>inst✝ : MulAction R M<VAR>p : SubMulAction R M<VAR>m : ↥p<GOAL>MulAction.stabilizer R m = MulAction.stabilizer R ↑m
<VAR>S : Type u'<VAR>T : Type u''<VAR>R : Type u<VAR>M : Type v<VAR>inst✝¹ : Group R<VAR>inst✝ : MulAction R M<VAR>p : SubMulAction R M<VAR>m : ↥p<GOAL>(MulAction.stabilizer R m).toSubmonoid = (MulAction.stabilizer R ↑m).toSubmonoid
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : 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>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I I₂ : LieIdeal R L<VAR>J : LieIdeal R L'<GOAL>map f I ≤ J ↔ I ≤ comap f J
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : 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>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I I₂ : LieIdeal R L<VAR>J : LieIdeal R L'<GOAL>⇑f '' ↑I ⊆ ↑J ↔ I ≤ comap f J
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>g : α → F α<VAR>x : α<GOAL>Quot.mk Mcongr <$> abs (corecF g x).dest = corec g <$> g x
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>g : α → F α<VAR>x : α<GOAL>(Quot.mk Mcongr ∘ corecF g) <$> g x = corec g <$> g x
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>F : ι → Submodule 𝕜 E<VAR>hV : IsHilbertSum 𝕜 G V<VAR>w : ↥(lp G 2)<GOAL>HasSum (fun i => (V i) (↑w i)) (hV.linearIsometryEquiv.symm w)
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a✝ a₁ a₂ b✝ b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>a b : E<GOAL>dist a b = ‖b / a‖
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f f₁ f₂ : (i : ι) → Filter (α i)<VAR>s✝ : (i : ι) → Set (α i)<VAR>p✝ : (i : ι) → α i → Prop<VAR>ι' : ι → Type<VAR>s : (i : ι) → ι' i → Set (α i)<VAR>p : (i : ι) → ι' i → Prop<VAR>h : ∀ (i : ι), (f i).HasBasis (p i) (s i)<GOAL>(pi f).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, p i (If.2 i)) fun If => If.1.pi fun i => s i (If.2 i)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>A F : Cᵒᵖ ⥤ Type v<VAR>η : F ⟶ A<VAR>X : Cᵒᵖ<VAR>p : YonedaCollection (restrictedYonedaObj η) (unop X)<GOAL>η.app X (unitForward η (unop X) p) = p.yonedaEquivFst
<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>p p₀ p₁✝ p₂✝ p₁ p₂ p₃ : P<VAR>h : Wbtw ℝ p₁ p₂ p₃<VAR>hp₂p₁ : p₂ ≠ p₁<GOAL>∠ p₂ p₁ p₃ = 0
<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>p p₀ p₁✝ p₂✝ p₁ p₂ p₃ : P<VAR>h : Wbtw ℝ p₁ p₂ p₃<VAR>hp₂p₁ : p₂ ≠ p₁<GOAL>p₂ -ᵥ p₁ ≠ 0 ∧ ∃ r, 0 < r ∧ p₃ -ᵥ p₁ = r • (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>p p₀ p₁✝ p₂ p₁ p₃ : P<VAR>r : ℝ<VAR>hr0 : 0 ≤ r<VAR>hr1 : r ≤ 1<VAR>hp₂p₁ : (AffineMap.lineMap p₁ p₃) r ≠ p₁<VAR>hr0' : r ≠ 0<GOAL>(AffineMap.lineMap p₁ p₃) r -ᵥ p₁ ≠ 0 ∧ ∃ r_1, 0 < r_1 ∧ p₃ -ᵥ p₁ = r_1 • ((AffineMap.lineMap p₁ p₃) r -ᵥ 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>p p₀ p₁✝ p₂ p₁ p₃ : P<VAR>r : ℝ<VAR>hr1 : r ≤ 1<VAR>hp₂p₁ : (AffineMap.lineMap p₁ p₃) r ≠ p₁<VAR>hr0' : r ≠ 0<VAR>hr0 : 0 < r<GOAL>(AffineMap.lineMap p₁ p₃) r -ᵥ p₁ ≠ 0 ∧ ∃ r_1, 0 < r_1 ∧ p₃ -ᵥ p₁ = r_1 • ((AffineMap.lineMap p₁ p₃) r -ᵥ 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>p p₀ p₁✝ p₂ p₁ p₃ : P<VAR>r : ℝ<VAR>hr1 : r ≤ 1<VAR>hp₂p₁ : (AffineMap.lineMap p₁ p₃) r ≠ p₁<VAR>hr0' : r ≠ 0<VAR>hr0 : 0 < r<GOAL>p₃ -ᵥ p₁ = r⁻¹ • ((AffineMap.lineMap p₁ p₃) r -ᵥ p₁)
<VAR>a b : ℤ<VAR>hb0 : 0 < b<VAR>h : a.natAbs.Coprime b.natAbs<GOAL>(↑a / ↑b).num = a
<VAR>𝕜 : Type u_1<VAR>S : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁶ : Field 𝕜<VAR>inst✝¹⁵ : CharZero 𝕜<VAR>inst✝¹⁴ : Ring R<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : Algebra 𝕜 R<VAR>inst✝¹¹ : Module 𝕜 M<VAR>inst✝¹⁰ : Module R M<VAR>inst✝⁹ : Module Rᵐᵒᵖ M<VAR>inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M<VAR>inst✝⁷ : IsScalarTower 𝕜 R M<VAR>inst✝⁶ : IsScalarTower 𝕜 Rᵐᵒᵖ M<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : TopologicalRing R<VAR>inst✝² : TopologicalAddGroup M<VAR>inst✝¹ : ContinuousSMul R M<VAR>inst✝ : ContinuousSMul Rᵐᵒᵖ M<VAR>x : tsze R M<VAR>hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd<VAR>n : ℕ<GOAL>((expSeries 𝕜 (tsze R M) (n + 1)) fun x_1 => x).snd = ((expSeries 𝕜 R n) fun x_1 => x.fst) • x.snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>f✝ : Filter α<VAR>g✝ : Filter β<VAR>f : Filter α<VAR>g : Filter β<GOAL>f.coprod g = f ×ˢ ⊤ ⊔ ⊤ ×ˢ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>f✝ : Filter α<VAR>g✝ : Filter β<VAR>f : Filter α<VAR>g : Filter β<GOAL>f.coprod g = comap Prod.fst f ⊔ comap Prod.snd g
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>R : ℝ≥0<VAR>f : α → ℝ<VAR>hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R<VAR>hnm : m ≤ m0<VAR>hfint : Integrable f μ<GOAL>∀ᵐ (x : α) ∂μ, |(μ[f|m]) x| ≤ ↑R
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>R : ℝ≥0<VAR>f : α → ℝ<VAR>hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R<VAR>hnm : m ≤ m0<VAR>hfint : Integrable f μ<VAR>h : ¬∀ᵐ (x : α) ∂μ, |(μ[f|m]) x| ≤ ↑R<GOAL>False
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>R : ℝ≥0<VAR>f : α → ℝ<VAR>hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R<VAR>hnm : m ≤ m0<VAR>hfint : Integrable f μ<VAR>h : μ {x | (fun x => |(μ[f|m]) x| ≤ ↑R) x}ᶜ ≠ 0<GOAL>False
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>R : ℝ≥0<VAR>f : α → ℝ<VAR>hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R<VAR>hnm : m ≤ m0<VAR>hfint : Integrable f μ<VAR>h : 0 < μ {x | ↑R < |(μ[f|m]) x|}<GOAL>False
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>R : ℝ≥0<VAR>f : α → ℝ<VAR>hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R<VAR>hnm : m ≤ m0<VAR>hfint : Integrable f μ<VAR>h : 0 < μ {x | ↑R < |(μ[f|m]) x|}<GOAL>(μ {x | ↑R < |(μ[f|m]) x|}).toReal * ↑R < (μ {x | ↑R < |(μ[f|m]) x|}).toReal * ↑R
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>R : ℝ≥0<VAR>f : α → ℝ<VAR>hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R<VAR>hnm : m ≤ m0<VAR>hfint : Integrable f μ<VAR>h : 0 < μ {x | ↑R < |(μ[f|m]) x|}<GOAL>IntegrableOn (fun x => |(μ[f|m]) x|) {x | ↑R < |(μ[f|m]) x|} μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>R : ℝ≥0<VAR>f : α → ℝ<VAR>hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R<VAR>hnm : m ≤ m0<VAR>hfint : Integrable f μ<VAR>h : 0 < μ {x | ↑R < |(μ[f|m]) x|}<GOAL>∫ (x : α) in {x | ↑R < |(μ[f|m]) x|}, |(μ[f|m]) x| ∂μ ≤ (μ {x | ↑R < |(μ[f|m]) x|}).toReal * ↑R
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>R : ℝ≥0<VAR>f : α → ℝ<VAR>hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R<VAR>hnm : m ≤ m0<VAR>hfint : Integrable f μ<VAR>h : 0 < μ {x | ↑R < |(μ[f|m]) x|}<GOAL>MeasurableSet {x | ↑R < |(μ[f|m]) x|}
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>R : ℝ≥0<VAR>f : α → ℝ<VAR>hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R<VAR>hnm : m ≤ m0<VAR>hfint : Integrable f μ<VAR>h : 0 < μ {x | ↑R < |(μ[f|m]) x|}<GOAL>∫ (x : α) in {x | ↑R < |(μ[f|m]) x|}, |f x| ∂μ ≤ (μ {x | ↑R < |(μ[f|m]) x|}).toReal * ↑R
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>R : ℝ≥0<VAR>f : α → ℝ<VAR>hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R<VAR>hnm : m ≤ m0<VAR>hfint : Integrable f μ<VAR>h : 0 < μ {x | ↑R < |(μ[f|m]) x|}<GOAL>∫ (x : α) in {x | ↑R < |(μ[f|m]) x|}, |f x| ∂μ ≤ ∫ (x : α) in {x | ↑R < |(μ[f|m]) x|}, ↑R ∂μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>R : ℝ≥0<VAR>f : α → ℝ<VAR>hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R<VAR>hnm : m ≤ m0<VAR>hfint : Integrable f μ<VAR>h : 0 < μ {x | ↑R < |(μ[f|m]) x|}<GOAL>IntegrableOn (fun x => ↑R) {x | ↑R < |(μ[f|m]) x|} μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>R : ℝ≥0<VAR>f : α → ℝ<VAR>hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R<VAR>hnm : m ≤ m0<VAR>hfint : Integrable f μ<VAR>h : 0 < μ {x | ↑R < |(μ[f|m]) x|}<GOAL>∫⁻ (a : α) in {x | ↑R < |(μ[f|m]) x|}, ↑‖(fun x => ↑R) a‖₊ ∂μ ≤ ∫⁻ (a : α) in {x | ↑R < |(μ[f|m]) x|}, ↑‖(μ[f|m]) a‖₊ ∂μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>R : ℝ≥0<VAR>f : α → ℝ<VAR>hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R<VAR>hnm : m ≤ m0<VAR>hfint : Integrable f μ<VAR>h : 0 < μ {x | ↑R < |(μ[f|m]) x|}<VAR>x : α<VAR>hx : x ∈ {x | ↑R < |(μ[f|m]) x|}<GOAL>↑‖(fun x => ↑R) x‖₊ ≤ ↑‖(μ[f|m]) x‖₊
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>R : ℝ≥0<VAR>f : α → ℝ<VAR>hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R<VAR>hnm : m ≤ m0<VAR>hfint : Integrable f μ<VAR>h : 0 < μ {x | ↑R < |(μ[f|m]) x|}<VAR>x : α<VAR>hx : x ∈ {x | ↑R < |(μ[f|m]) x|}<GOAL>⟨↑R, ⋯⟩ ≤ ‖(μ[f|m]) x‖₊
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>g g₁ g₂ : σ → S₁<VAR>h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i<GOAL>eval₂ f g₁ p = eval₂ f g₂ p
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>g g₁ g₂ : σ → S₁<VAR>h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i<GOAL>∀ x ∈ p.support, (fun s a => f a * s.prod fun n e => g₁ n ^ e) x (p x) = (fun s a => f a * s.prod fun n e => g₂ n ^ e) x (p x)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>g g₁ g₂ : σ → S₁<VAR>h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i<VAR>C : σ →₀ ℕ<VAR>hc : C ∈ p.support<GOAL>(C.prod fun n e => g₁ n ^ e) = C.prod fun n e => g₂ n ^ e
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>g g₁ g₂ : σ → S₁<VAR>h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i<VAR>C : σ →₀ ℕ<VAR>hc : C ∈ p.support<GOAL>∀ x ∈ C.support, (fun n e => g₁ n ^ e) x (C x) = (fun n e => g₂ n ^ e) x (C x)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>g g₁ g₂ : σ → S₁<VAR>h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i<VAR>C : σ →₀ ℕ<VAR>hc : C ∈ p.support<VAR>i : σ<VAR>hi : i ∈ C.support<GOAL>coeff C p ≠ 0
<VAR>n m : ℕ<VAR>inst✝ : NeZero n<VAR>k : Fin n<GOAL>0 + k = k
<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 β<GOAL>∏ x ∈ s, f x * g x = fold (fun x x_1 => x * x_1) (1 * 1) (fun x => f x * g x) s
<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 β<GOAL>∏ x ∈ s, f x * g x = fold (fun x x_1 => x * x_1) 1 (fun x => f x * g x) s
<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>0 < expNegInvGlue x
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>hs : IsCompact s<VAR>U : X → Set X<VAR>hU : ∀ x ∈ s, U x ∈ 𝓝 x<VAR>t : Finset ↑s<VAR>ht : ⋃ x ∈ t, U ↑x ∈ 𝓝ˢ s<GOAL>⋃ x ∈ Finset.image Subtype.val t, U x ∈ 𝓝ˢ s
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_4, u_1} C<VAR>inst✝ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>F : D ⥤ C<VAR>A B : C<VAR>X Y : D<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>u : G.obj A ⟶ X<VAR>v : G.obj B ⟶ Y<VAR>sq : CommSq u (G.map i) p v<VAR>adj : G ⊣ F<GOAL>(adj.homEquiv A X) u ≫ F.map p = i ≫ (adj.homEquiv B Y) v
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_4, u_1} C<VAR>inst✝ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>F : D ⥤ C<VAR>A B : C<VAR>X Y : D<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>u : G.obj A ⟶ X<VAR>v : G.obj B ⟶ Y<VAR>sq : CommSq u (G.map i) p v<VAR>adj : G ⊣ F<GOAL>adj.unit.app A ≫ F.map (G.map i ≫ v) = i ≫ adj.unit.app B ≫ F.map v
<VAR>α : Type u_1<VAR>inst✝ : AddCommGroup α<VAR>p a a₁ a₂ b b₁ b₂ c : α<VAR>n : ℕ<VAR>z : ℤ<GOAL>b ≡ a [PMOD -p] ↔ a ≡ b [PMOD p]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : DecidableEq α<VAR>f : α → β<VAR>s : Set α<VAR>x : α<VAR>y : β<GOAL>ContinuousWithinAt (update f x y) s x ↔ Tendsto (update f x y) (𝓝[s \ {x}] x) (𝓝 y)
<VAR>α : Type u_1<VAR>inst✝¹ : Semiring α<VAR>inst✝ : NoZeroDivisors α<VAR>m n : ℕ<VAR>hmn : m ∣ n<VAR>hm : FermatLastTheoremFor m<GOAL>FermatLastTheoremFor n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c✝ d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε✝ ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f g : α → ℝ≥0∞<VAR>ι : Type u_4<VAR>a : ι → ℝ≥0∞<VAR>c : ℝ≥0∞<VAR>c_ne_top : c ≠ ⊤<VAR>tsum_le_c : ∑' (i : ι), a i ≤ c<VAR>ε : ℝ≥0∞<VAR>ε_ne_zero : ε ≠ 0<GOAL>∃ (hf : {i | ε ≤ a i}.Finite), ↑hf.toFinset.card ≤ c / ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c✝ d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε✝ ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f g : α → ℝ≥0∞<VAR>ι : Type u_4<VAR>a : ι → ℝ≥0∞<VAR>c : ℝ≥0∞<VAR>c_ne_top : c ≠ ⊤<VAR>tsum_le_c : ∑' (i : ι), a i ≤ c<VAR>ε : ℝ≥0∞<VAR>ε_ne_zero : ε ≠ 0<VAR>hf : {i | ε ≤ a i}.Finite<GOAL>∃ (hf : {i | ε ≤ a i}.Finite), ↑hf.toFinset.card ≤ c / ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c✝ d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε✝ ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f g : α → ℝ≥0∞<VAR>ι : Type u_4<VAR>a : ι → ℝ≥0∞<VAR>c : ℝ≥0∞<VAR>c_ne_top : c ≠ ⊤<VAR>tsum_le_c : ∑' (i : ι), a i ≤ c<VAR>ε : ℝ≥0∞<VAR>ε_ne_zero : ε ≠ 0<VAR>hf : {i | ε ≤ a i}.Finite<GOAL>↑hf.toFinset.card * ε ≤ c
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : Group G'<VAR>inst✝⁴ : Group G''<VAR>A : Type u_4<VAR>inst✝³ : AddGroup A<VAR>N✝ : Type u_5<VAR>P : Type u_6<VAR>inst✝² : Group N✝<VAR>inst✝¹ : Group P<VAR>K : Subgroup G<VAR>N : Type u_7<VAR>inst✝ : Group N<VAR>f : G →* N<GOAL>↑f.range = ↑⊤ ↔ Set.range ⇑f = Set.univ
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>x : R<VAR>inst✝ : Away x S<GOAL>(algebraMap R S) x * invSelf x = 1
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>x : R<VAR>inst✝ : Away x S<GOAL>(algebraMap R S) x = mk' S (↑⟨x, ⋯⟩) 1
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>x : R<VAR>inst✝ : Away x S<GOAL>mk' S (↑⟨x, ⋯⟩) 1 = (algebraMap R S) x
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ : Multiset α<VAR>a : α<VAR>n : ℕ<VAR>s : Multiset α<GOAL>count a (n • s) = n * count a s
<VAR>V : Type u_1<VAR>inst✝¹ : Quiver V<VAR>W : Type u_2<VAR>σ : V → W<VAR>W' : Type u_3<VAR>inst✝ : Quiver W'<VAR>φ : V ⥤q W'<VAR>τ : W → W'<VAR>h : ∀ (x : V), φ.obj x = τ (σ x)<GOAL>of σ ⋙q lift σ φ τ h = φ
<VAR>V : Type u_1<VAR>inst✝¹ : Quiver V<VAR>W : Type u_2<VAR>σ : V → W<VAR>W' : Type u_3<VAR>inst✝ : Quiver W'<VAR>φ : V ⥤q W'<VAR>τ : W → W'<VAR>h : ∀ (x : V), φ.obj x = τ (σ x)<GOAL>∀ (X : V), (of σ ⋙q lift σ φ τ h).obj X = φ.obj X
<VAR>V : Type u_1<VAR>inst✝¹ : Quiver V<VAR>W : Type u_2<VAR>σ : V → W<VAR>W' : Type u_3<VAR>inst✝ : Quiver W'<VAR>φ : V ⥤q W'<VAR>τ : W → W'<VAR>h : ∀ (x : V), φ.obj x = τ (σ x)<GOAL>∀ (X Y : V) (f : X ⟶ Y), (of σ ⋙q lift σ φ τ h).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSemiring R<VAR>x✝ a✝ : R<GOAL>((↑↑{ toFun := fun p => p.toContinuousMap, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }).toFun ((algebraMap R R[X]) x✝)) a✝ = ((algebraMap R C(R, R)) x✝) a✝