ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : PseudoEMetricSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>inst✝ : IsProbabilityMeasure ν<VAR>δ ε : ℝ≥0∞<VAR>B : Set Ω<VAR>ε_gt : δ < ε<VAR>ε_lt_top : ε < ⊤<VAR>B_mble : MeasurableSet B<VAR>B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ<VAR>Tc_mble : MeasurableSet (thickening ε.toReal B)ᶜ<VAR>h : 1 - μ (thickening ε.toReal B) ≤ ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) + ε<VAR>almost : 1 ≤ ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) + (ε + μ (thickening ε.toReal B))<GOAL>1 - ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) ≤ μ (thickening ε.toReal B) + ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : PseudoEMetricSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>inst✝ : IsProbabilityMeasure ν<VAR>δ ε : ℝ≥0∞<VAR>B : Set Ω<VAR>ε_gt : δ < ε<VAR>ε_lt_top : ε < ⊤<VAR>B_mble : MeasurableSet B<VAR>B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ<VAR>Tc_mble : MeasurableSet (thickening ε.toReal B)ᶜ<VAR>h : 1 - μ (thickening ε.toReal B) ≤ ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) + ε<VAR>almost : 1 ≤ ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) + (ε + μ (thickening ε.toReal B))<GOAL>ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) + (ε + μ (thickening ε.toReal B)) - ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) ≤ μ (thickening ε.toReal B) + ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : TopologicalSpace β<VAR>f✝ g✝ : α → β<VAR>γ : Type u_4<VAR>inst✝ : TopologicalSpace γ<VAR>f : α → β<VAR>g : β → γ<VAR>hg : Continuous g<VAR>hf : AEStronglyMeasurable' m f μ<VAR>x : α<VAR>hx : f x = mk f hf x<GOAL>(g ∘ f) x = (fun x => g (mk f hf x)) x
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>frontier (closedBall x r) = sphere x r
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>H1 : IsCoprime x y<VAR>H2 : IsCoprime x z<GOAL>IsCoprime x (y * z)
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>H1 : IsCoprime y x<VAR>H2 : IsCoprime z x<GOAL>IsCoprime (y * z) x
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y✝ : M<VAR>f : E →ₗ.[R] F<VAR>x : E<VAR>y : F<VAR>h : ∃ y_1, ↑y_1 = (x, y).1 ∧ ↑f y_1 = (x, y).2<GOAL>x ∈ f.domain
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y✝ : M<VAR>f : E →ₗ.[R] F<VAR>x : E<VAR>y : F<VAR>x' : ↥f.domain<VAR>h : ↑x' = x ∧ ↑f x' = y<GOAL>x ∈ f.domain
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y✝ : M<VAR>f : E →ₗ.[R] F<VAR>x : E<VAR>y : F<VAR>x' : ↥f.domain<VAR>h : ↑x' = x ∧ ↑f x' = y<GOAL>↑x' ∈ f.domain
<VAR>α : Type u_1<VAR>inst✝³ : GeneralizedBooleanAlgebra α<VAR>inst✝² : DecidableRel Disjoint<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v a b : α<VAR>inst✝ : DecidableEq α<VAR>h : a ∈ 𝓒 u v s<VAR>ha : a ∉ s<GOAL>Disjoint v a
<VAR>α : Type u_1<VAR>inst✝³ : GeneralizedBooleanAlgebra α<VAR>inst✝² : DecidableRel Disjoint<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v a b : α<VAR>inst✝ : DecidableEq α<VAR>h : a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ b ∈ s, compress u v b = a<VAR>ha : a ∉ s<GOAL>Disjoint v a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁶ : Zero α<VAR>inst✝⁵ : Zero β<VAR>inst✝⁴ : SMulWithZero α β<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : PartialOrder β<VAR>inst✝¹ : PosSMulStrictMono α β<VAR>inst✝ : SMulPosStrictMono α β<VAR>ha : a₁ ≤ a₂<VAR>hb : b₁ ≤ b₂<VAR>h₁ : 0 < a₁<VAR>h₂ : 0 < b₂<VAR>h : a₁ • b₁ = a₂ • b₂<GOAL>a₁ = a₂ ∧ b₁ = b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁶ : Zero α<VAR>inst✝⁵ : Zero β<VAR>inst✝⁴ : SMulWithZero α β<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : PartialOrder β<VAR>inst✝¹ : PosSMulStrictMono α β<VAR>inst✝ : SMulPosStrictMono α β<VAR>ha : a₁ ≤ a₂<VAR>hb : b₁ ≤ b₂<VAR>h₁ : 0 < a₁<VAR>h₂ : 0 < b₂<VAR>h : a₁ • b₁ = a₂ • b₂<GOAL>¬a₁ < a₂ ∧ ¬b₁ < b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁶ : Zero α<VAR>inst✝⁵ : Zero β<VAR>inst✝⁴ : SMulWithZero α β<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : PartialOrder β<VAR>inst✝¹ : PosSMulStrictMono α β<VAR>inst✝ : SMulPosStrictMono α β<VAR>ha✝ : a₁ ≤ a₂<VAR>hb : b₁ ≤ b₂<VAR>h₁ : 0 < a₁<VAR>h₂ : 0 < b₂<VAR>h : a₁ • b₁ = a₂ • b₂<VAR>ha : a₁ < a₂<GOAL>a₁ • b₁ < a₂ • b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁶ : Zero α<VAR>inst✝⁵ : Zero β<VAR>inst✝⁴ : SMulWithZero α β<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : PartialOrder β<VAR>inst✝¹ : PosSMulStrictMono α β<VAR>inst✝ : SMulPosStrictMono α β<VAR>ha : a₁ ≤ a₂<VAR>hb✝ : b₁ ≤ b₂<VAR>h₁ : 0 < a₁<VAR>h₂ : 0 < b₂<VAR>h : a₁ • b₁ = a₂ • b₂<VAR>hb : b₁ < b₂<GOAL>a₁ • b₁ < a₂ • b₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>n : ℕ<GOAL>(L.mapComposableArrows n).EssSurj
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>n : ℕ<VAR>this : (L.op.mapComposableArrows n).EssSurj<GOAL>(L.mapComposableArrows n).EssSurj
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>n : ℕ<VAR>this✝ : (L.op.mapComposableArrows n).EssSurj<VAR>this : (L.mapComposableArrows n ⋙ (opEquivalence D n).functor.rightOp).EssSurj<GOAL>(L.mapComposableArrows n).EssSurj
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>M : (i : ι) → Matroid (α i)<VAR>h : ∀ (i : ι), (M i).Finitary<VAR>I : Set ((i : ι) × α i)<VAR>hI : ∀ J ⊆ I, J.Finite → (Matroid.sigma M).Indep J<GOAL>(Matroid.sigma M).Indep I
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>M : (i : ι) → Matroid (α i)<VAR>h : ∀ (i : ι), (M i).Finitary<VAR>I : Set ((i : ι) × α i)<VAR>hI : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' J)<GOAL>∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>M : (i : ι) → Matroid (α i)<VAR>h : ∀ (i : ι), (M i).Finitary<VAR>I : Set ((i : ι) × α i)<VAR>hI : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' J)<VAR>i : ι<GOAL>(M i).Indep (Sigma.mk i ⁻¹' I)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>M : (i : ι) → Matroid (α i)<VAR>h : ∀ (i : ι), (M i).Finitary<VAR>I : Set ((i : ι) × α i)<VAR>hI : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' J)<VAR>i : ι<GOAL>∀ J ⊆ Sigma.mk i ⁻¹' I, J.Finite → (M i).Indep J
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>M : (i : ι) → Matroid (α i)<VAR>h : ∀ (i : ι), (M i).Finitary<VAR>I : Set ((i : ι) × α i)<VAR>hI : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' J)<VAR>i : ι<VAR>J : Set (α i)<VAR>hJI : J ⊆ Sigma.mk i ⁻¹' I<VAR>hJ : J.Finite<GOAL>(M i).Indep J
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>M : (i : ι) → Matroid (α i)<VAR>h : ∀ (i : ι), (M i).Finitary<VAR>I : Set ((i : ι) × α i)<VAR>hI : ∀ J ⊆ I, J.Finite → ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' J)<VAR>i : ι<VAR>J : Set (α i)<VAR>hJI : J ⊆ Sigma.mk i ⁻¹' I<VAR>hJ : J.Finite<GOAL>J = Sigma.mk i ⁻¹' (Sigma.mk i '' J)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>S : Type u_4<VAR>S₃ : Type u_5<VAR>inst✝³⁶ : Semiring R<VAR>inst✝³⁵ : Semiring R₂<VAR>inst✝³⁴ : Semiring R₃<VAR>inst✝³³ : Monoid S<VAR>inst✝³² : Monoid S₃<VAR>M : Type u_6<VAR>inst✝³¹ : TopologicalSpace M<VAR>inst✝³⁰ : AddCommMonoid M<VAR>inst✝²⁹ : Module R M<VAR>M₂ : Type u_7<VAR>inst✝²⁸ : TopologicalSpace M₂<VAR>inst✝²⁷ : AddCommMonoid M₂<VAR>inst✝²⁶ : Module R₂ M₂<VAR>M₃ : Type u_8<VAR>inst✝²⁵ : TopologicalSpace M₃<VAR>inst✝²⁴ : AddCommMonoid M₃<VAR>inst✝²³ : Module R₃ M₃<VAR>N₂ : Type u_9<VAR>inst✝²² : TopologicalSpace N₂<VAR>inst✝²¹ : AddCommMonoid N₂<VAR>inst✝²⁰ : Module R N₂<VAR>N₃ : Type u_10<VAR>inst✝¹⁹ : TopologicalSpace N₃<VAR>inst✝¹⁸ : AddCommMonoid N₃<VAR>inst✝¹⁷ : Module R N₃<VAR>inst✝¹⁶ : DistribMulAction S₃ M₃<VAR>inst✝¹⁵ : SMulCommClass R₃ S₃ M₃<VAR>inst✝¹⁴ : ContinuousConstSMul S₃ M₃<VAR>inst✝¹³ : DistribMulAction S N₃<VAR>inst✝¹² : SMulCommClass R S N₃<VAR>inst✝¹¹ : ContinuousConstSMul S N₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝¹⁰ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁹ : DistribMulAction S₃ M₂<VAR>inst✝⁸ : ContinuousConstSMul S₃ M₂<VAR>inst✝⁷ : SMulCommClass R₂ S₃ M₂<VAR>inst✝⁶ : DistribMulAction S N₂<VAR>inst✝⁵ : ContinuousConstSMul S N₂<VAR>inst✝⁴ : SMulCommClass R S N₂<VAR>inst✝³ : SMulCommClass R₂ R₂ M₂<VAR>inst✝² : SMulCommClass R₃ R₃ M₃<VAR>inst✝¹ : ContinuousConstSMul R₂ M₂<VAR>inst✝ : ContinuousConstSMul R₃ M₃<VAR>h : M₂ →SL[σ₂₃] M₃<VAR>c : R₂<VAR>f : M →SL[σ₁₂] M₂<VAR>x : M<GOAL>(h.comp (c • f)) x = (σ₂₃ c • h.comp f) x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>S : Type u_3<VAR>inst✝¹ : CommMonoid S<VAR>inst✝ : DistribMulAction S M<VAR>x y : M<VAR>a : S<VAR>hx : a • x = 0<VAR>b : S<VAR>hy : b • y = 0<GOAL>x + y ∈ {x | ∃ a, a • x = 0}
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>S : Type u_3<VAR>inst✝¹ : CommMonoid S<VAR>inst✝ : DistribMulAction S M<VAR>x y : M<VAR>a : S<VAR>hx : a • x = 0<VAR>b : S<VAR>hy : b • y = 0<GOAL>(b * a) • (x + y) = 0
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizedGCDMonoid α<VAR>inst✝ : DecidableEq α<VAR>s✝ : Multiset α<VAR>a : α<VAR>s : Multiset α<VAR>IH : s.dedup.lcm = s.lcm<VAR>h : a ∈ s<GOAL>fold GCDMonoid.lcm 1 s = GCDMonoid.lcm a (fold GCDMonoid.lcm 1 s)
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizedGCDMonoid α<VAR>inst✝ : DecidableEq α<VAR>s✝ : Multiset α<VAR>a : α<VAR>s : Multiset α<VAR>IH : s.dedup.lcm = s.lcm<VAR>h : a ∈ s<GOAL>GCDMonoid.lcm a (fold GCDMonoid.lcm 1 (s.erase a)) = GCDMonoid.lcm (normalize a) (fold GCDMonoid.lcm 1 (s.erase a))
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsSplittingField K L (X ^ n - C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<GOAL>adjoin K {α} = ⊤
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsSplittingField K L (X ^ n - C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<GOAL>Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm) (adjoin K {α}) = Subalgebra.map ↑(adjoinRootXPowSubCEquiv hζ H hα).symm ⊤
<VAR>α : Type u_1<VAR>inst✝¹ : Lattice α<VAR>inst✝ : OrderBot α<VAR>a : α<VAR>P : Finpartition a<GOAL>P.parts = ∅ ↔ a = ⊥
<VAR>α : Type u_1<VAR>inst✝¹ : Lattice α<VAR>inst✝ : OrderBot α<VAR>a : α<VAR>P : Finpartition a<GOAL>P.parts = ∅ ↔ P.parts.sup id = ⊥
<VAR>α : Type u_1<VAR>inst✝¹ : Lattice α<VAR>inst✝ : OrderBot α<VAR>a : α<VAR>P : Finpartition a<VAR>h : P.parts = ∅<GOAL>P.parts.sup id = ⊥
<VAR>α : Type u_1<VAR>inst✝¹ : Lattice α<VAR>inst✝ : OrderBot α<VAR>a : α<VAR>P : Finpartition a<VAR>h : P.parts.sup id = ⊥<VAR>b : α<VAR>hb : b ∈ P.parts<GOAL>⊥ ∈ P.parts
<VAR>n : ℕ<VAR>hn : n % 4 = 3<GOAL>χ₄ ↑n = -1
<VAR>n : ℕ<VAR>hn : n % 4 = 3<GOAL>χ₄ ↑3 = -1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : SemilatticeSup α<VAR>inst✝⁵ : OrderTop α<VAR>inst✝⁴ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝³ : SemilatticeSup β<VAR>inst✝² : BoundedOrder β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>hs : a ∈ lowerClosure ↑s<VAR>ht : a ∉ lowerClosure ↑t<GOAL>(s ∪ t).truncatedSup a = s.truncatedSup a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : SemilatticeSup α<VAR>inst✝⁵ : OrderTop α<VAR>inst✝⁴ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝³ : SemilatticeSup β<VAR>inst✝² : BoundedOrder β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>hs : a ∈ lowerClosure ↑s<VAR>ht : ∀ x ∈ t, ¬a ≤ x<GOAL>(s ∪ t).truncatedSup a = s.truncatedSup a
<VAR>r x : ℝ<GOAL>ENNReal.ofReal (if 0 ≤ x then r ^ 1 / Gamma 1 * x ^ (1 - 1) * rexp (-(r * x)) else 0) = ENNReal.ofReal (if 0 ≤ x then r * rexp (-(r * x)) else 0)
<VAR>τ : Type u_1<VAR>inst✝³ : TopologicalSpace τ<VAR>inst✝² : AddCommGroup τ<VAR>inst✝¹ : TopologicalAddGroup τ<VAR>α : Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>f : Filter τ<VAR>ϕ : Flow τ α<VAR>s : Set α<VAR>hf : ∀ (t : τ), Tendsto (fun x => x + t) f f<VAR>t : τ<GOAL>ω f ϕ.toFun s = ω f ϕ.toFun (ϕ.toFun (-t) '' (ϕ.toFun t '' s))
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Affine R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Equation x₁ y₁<VAR>h₂ : W.Equation x₂ y₂<VAR>hx : x₁ = x₂<GOAL>y₁ = y₂ ∨ y₁ = W.negY x₂ y₂
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Affine R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ = x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆<VAR>h₂ : y₂ ^ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂ = x₂ ^ 3 + W.a₂ * x₂ ^ 2 + W.a₄ * x₂ + W.a₆<VAR>hx : x₁ = x₂<GOAL>y₁ = y₂ ∨ y₁ = W.negY x₂ y₂
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Affine R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ = x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆<VAR>h₂ : y₂ ^ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂ = x₂ ^ 3 + W.a₂ * x₂ ^ 2 + W.a₄ * x₂ + W.a₆<VAR>hx : x₁ = x₂<GOAL>(y₁ - y₂) * (y₁ - (-y₂ - W.a₁ * x₂ - W.a₃)) = 0
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>v w : V<GOAL>Fintype.card ↑(G.commonNeighbors v w) ≤ G.degree w
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>x y✝ : E<VAR>s t : Set E<VAR>h : s ⊆ t<VAR>y : E<VAR>c : ℕ → 𝕜<VAR>d : ℕ → E<VAR>ds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s<VAR>ctop : Tendsto (fun n => ‖c n‖) atTop atTop<VAR>clim : Tendsto (fun n => c n • d n) atTop (𝓝 y)<GOAL>y ∈ tangentConeAt 𝕜 t x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>T : Set α → E →L[ℝ] F<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>c : ℝ<VAR>f : ↥(simpleFunc E 1 μ)<GOAL>SimpleFunc.setToSimpleFunc T (toSimpleFunc (c • f)) = c • SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>T : Set α → E →L[ℝ] F<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>c : ℝ<VAR>f : ↥(simpleFunc E 1 μ)<GOAL>SimpleFunc.setToSimpleFunc T (toSimpleFunc (c • f)) = SimpleFunc.setToSimpleFunc T (c • toSimpleFunc f)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>T : Set α → E →L[ℝ] F<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>c : ℝ<VAR>f : ↥(simpleFunc E 1 μ)<GOAL>↑(toSimpleFunc (c • f)) =ᶠ[ae μ] ↑(c • toSimpleFunc f)
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>MorphismProperty.StableUnderBaseChange @IsAffineHom
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>AffineTargetMorphismProperty.StableUnderBaseChange fun X x x_1 x => IsAffine X
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>this : ∀ (P : MorphismProperty Scheme) {Q : outParam AffineTargetMorphismProperty} [self : HasAffineProperty P Q], AffineTargetMorphismProperty.IsLocal Q := HasAffineProperty.isLocal_affineProperty<GOAL>AffineTargetMorphismProperty.StableUnderBaseChange fun X x x_1 x => IsAffine X
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>this : ∀ (P : MorphismProperty Scheme) {Q : outParam AffineTargetMorphismProperty} [self : HasAffineProperty P Q], AffineTargetMorphismProperty.IsLocal Q := HasAffineProperty.isLocal_affineProperty<GOAL>∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), IsAffine Y → IsAffine (Limits.pullback f g)
<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsIso f<VAR>h : IsAffine Y<GOAL>IsAffine X
<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsIso f<VAR>h : Y ∈ Scheme.Spec.essImage<GOAL>X ∈ Scheme.Spec.essImage
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>F✝ : C ⥤ D<VAR>A : Type u₃<VAR>inst✝² : Category.{v₃, u₃} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology A<VAR>G : C ⥤ D<VAR>hG : CompatiblePreserving K G<VAR>ℱ✝ : SheafOfTypes K<VAR>Z✝ : C<VAR>T✝ : Presieve Z✝<VAR>x✝ : FamilyOfElements (G.op ⋙ ℱ✝.val) T✝<VAR>h : x✝.Compatible<VAR>F : C ⥤ D<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)<VAR>ℱ : SheafOfTypes K<VAR>Z : C<VAR>T : Presieve Z<VAR>x : FamilyOfElements (F.op ⋙ ℱ.val) T<VAR>hx : x.Compatible<VAR>Y₁ Y₂ : C<VAR>X : D<VAR>f₁ : X ⟶ F.obj Y₁<VAR>f₂ : X ⟶ F.obj Y₂<VAR>g₁ : Y₁ ⟶ Z<VAR>g₂ : Y₂ ⟶ Z<VAR>hg₁ : T g₁<VAR>hg₂ : T g₂<VAR>he : f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂<VAR>X' : C<VAR>e : F.obj X' ≅ X<GOAL>ℱ.val.map f₁.op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>F✝ : C ⥤ D<VAR>A : Type u₃<VAR>inst✝² : Category.{v₃, u₃} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology A<VAR>G : C ⥤ D<VAR>hG : CompatiblePreserving K G<VAR>ℱ✝ : SheafOfTypes K<VAR>Z✝ : C<VAR>T✝ : Presieve Z✝<VAR>x✝ : FamilyOfElements (G.op ⋙ ℱ✝.val) T✝<VAR>h : x✝.Compatible<VAR>F : C ⥤ D<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)<VAR>ℱ : SheafOfTypes K<VAR>Z : C<VAR>T : Presieve Z<VAR>x : FamilyOfElements (F.op ⋙ ℱ.val) T<VAR>hx : x.Compatible<VAR>Y₁ Y₂ : C<VAR>X : D<VAR>f₁ : X ⟶ F.obj Y₁<VAR>f₂ : X ⟶ F.obj Y₂<VAR>g₁ : Y₁ ⟶ Z<VAR>g₂ : Y₂ ⟶ Z<VAR>hg₁ : T g₁<VAR>hg₂ : T g₂<VAR>he : f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂<VAR>X' : C<VAR>e : F.obj X' ≅ X<GOAL>(ℱ.val.mapIso e.op).toEquiv (ℱ.val.map f₁.op (x g₁ hg₁)) = (ℱ.val.mapIso e.op).toEquiv (ℱ.val.map f₂.op (x g₂ hg₂))
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>F✝ : C ⥤ D<VAR>A : Type u₃<VAR>inst✝² : Category.{v₃, u₃} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology A<VAR>G : C ⥤ D<VAR>hG : CompatiblePreserving K G<VAR>ℱ✝ : SheafOfTypes K<VAR>Z✝ : C<VAR>T✝ : Presieve Z✝<VAR>x✝ : FamilyOfElements (G.op ⋙ ℱ✝.val) T✝<VAR>h : x✝.Compatible<VAR>F : C ⥤ D<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)<VAR>ℱ : SheafOfTypes K<VAR>Z : C<VAR>T : Presieve Z<VAR>x : FamilyOfElements (F.op ⋙ ℱ.val) T<VAR>hx : x.Compatible<VAR>Y₁ Y₂ : C<VAR>X : D<VAR>f₁ : X ⟶ F.obj Y₁<VAR>f₂ : X ⟶ F.obj Y₂<VAR>g₁ : Y₁ ⟶ Z<VAR>g₂ : Y₂ ⟶ Z<VAR>hg₁ : T g₁<VAR>hg₂ : T g₂<VAR>he : f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂<VAR>X' : C<VAR>e : F.obj X' ≅ X<GOAL>ℱ.val.map (f₁.op ≫ e.hom.op) (x g₁ hg₁) = ℱ.val.map (f₂.op ≫ e.hom.op) (x g₂ hg₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>x : α<VAR>hx : ¬p x<GOAL>x ∉ Set.range Subtype.val
<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✝² : AddCommGroupWithOne G<VAR>inst✝¹ : AddGroup H<VAR>inst✝ : AddConstMapClass F G H 1 b<VAR>f : F<VAR>n : ℤ<VAR>x : G<GOAL>f (↑n + x) = f x + n • b
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>G : C<GOAL>IsCodetector G ↔ (yoneda.obj G).ReflectsIsomorphisms
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>G : C<VAR>hG : IsCodetector G<VAR>A✝ B✝ : Cᵒᵖ<VAR>f : A✝ ⟶ B✝<VAR>hf : IsIso ((yoneda.obj G).map f)<GOAL>IsIso f
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>G : C<VAR>h : (yoneda.obj G).ReflectsIsomorphisms<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h<GOAL>IsIso f
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : CommMonoid M<VAR>a : M<VAR>l l₁ l₂ ys : List M<GOAL>[].prod * ys.prod = (zipWith (fun x x_1 => x * x_1) [] ys).prod * (drop ys.length []).prod * (drop [].length ys).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : CommMonoid M<VAR>a : M<VAR>l l₁ l₂ xs : List M<GOAL>xs.prod * [].prod = (zipWith (fun x x_1 => x * x_1) xs []).prod * (drop [].length xs).prod * (drop xs.length []).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : CommMonoid M<VAR>a : M<VAR>l l₁ l₂ : List M<VAR>x : M<VAR>xs : List M<VAR>y : M<VAR>ys : List M<GOAL>(x :: xs).prod * (y :: ys).prod = (zipWith (fun x x_1 => x * x_1) (x :: xs) (y :: ys)).prod * (drop (y :: ys).length (x :: xs)).prod * (drop (x :: xs).length (y :: ys)).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : CommMonoid M<VAR>a : M<VAR>l l₁ l₂ : List M<VAR>x : M<VAR>xs : List M<VAR>y : M<VAR>ys : List M<GOAL>x * xs.prod * (y * ys.prod) = x * y * (zipWith (fun x x_1 => x * x_1) xs ys).prod * (drop ys.length xs).prod * (drop xs.length ys).prod