ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<VAR>f : M →ₗ[R] M<VAR>hf : IsNilpotent f<VAR>b : Basis (Module.Free.ChooseBasisIndex R M) R M := Module.Free.chooseBasis R M<GOAL>IsNilpotent ((trace R M) f)
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<VAR>f : M →ₗ[R] M<VAR>hf : IsNilpotent f<VAR>b : Basis (Module.Free.ChooseBasisIndex R M) R M := Module.Free.chooseBasis R M<GOAL>IsNilpotent ((toMatrix b b) f).trace
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<VAR>f : M →ₗ[R] M<VAR>hf : IsNilpotent f<VAR>b : Basis (Module.Free.ChooseBasisIndex R M) R M := Module.Free.chooseBasis R M<GOAL>IsNilpotent ((toMatrix b b) f)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Fintype F<VAR>inst✝ : DecidableEq F<VAR>a : F<VAR>ha : ¬IsUnit a<GOAL>(↑{ toFun := quadraticCharFun F, map_one' := ⋯, map_mul' := ⋯ }).toFun a = 0
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Fintype F<VAR>inst✝ : DecidableEq F<VAR>a : F<VAR>ha : ¬IsUnit a<GOAL>(↑{ toFun := quadraticCharFun F, map_one' := ⋯, map_mul' := ⋯ }).toFun 0 = 0
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>α✝ : E<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>α : E<GOAL>minpoly F (AdjoinSimple.gen F α) = minpoly F α
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l : List α<GOAL>count a (a :: l) = count a l + 1
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : β → α → β<VAR>b : β<VAR>a✝ : α<VAR>l✝ : List α<VAR>a : β<VAR>x : α<VAR>l : List α<GOAL>(scanl f a (x :: l)).length = (x :: l).length + 1
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : β → α → β<VAR>b : β<VAR>a✝ : α<VAR>l✝ : List α<VAR>a : β<VAR>x : α<VAR>l : List α<GOAL>(scanl f (f a x) l).length = l.length + 1
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>cR : Type u<VAR>inst✝¹ : CommRing cR<VAR>s✝ : Set R<VAR>S : Type u_1<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>s : Set R<GOAL>⇑f '' closure s = closure (⇑f '' s)
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>cR : Type u<VAR>inst✝¹ : CommRing cR<VAR>s✝ : Set R<VAR>S : Type u_1<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>s : Set R<GOAL>⇑f '' closure s ≤ closure (⇑f '' s)
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : Module k V1<VAR>inst✝⁹ : AffineSpace V1 P1<VAR>inst✝⁸ : AddCommGroup V2<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : AffineSpace V2 P2<VAR>inst✝⁵ : AddCommGroup V3<VAR>inst✝⁴ : Module k V3<VAR>inst✝³ : AffineSpace V3 P3<VAR>inst✝² : AddCommGroup V4<VAR>inst✝¹ : Module k V4<VAR>inst✝ : AffineSpace V4 P4<VAR>f g : P1 →ᵃ[k] P2<VAR>h₁ : f.linear = g.linear<VAR>p : P1<VAR>h₂ : f p = g p<VAR>q : P1<VAR>hgl : g.linear (q -ᵥ p) = g.toFun (q -ᵥ p +ᵥ q) -ᵥ g.toFun q<GOAL>f q = g q
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : Module k V1<VAR>inst✝⁹ : AffineSpace V1 P1<VAR>inst✝⁸ : AddCommGroup V2<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : AffineSpace V2 P2<VAR>inst✝⁵ : AddCommGroup V3<VAR>inst✝⁴ : Module k V3<VAR>inst✝³ : AffineSpace V3 P3<VAR>inst✝² : AddCommGroup V4<VAR>inst✝¹ : Module k V4<VAR>inst✝ : AffineSpace V4 P4<VAR>f g : P1 →ᵃ[k] P2<VAR>h₁ : f.linear = g.linear<VAR>p : P1<VAR>h₂ : f p = g p<VAR>q : P1<VAR>hgl : g.linear (q -ᵥ p) = g.toFun (q -ᵥ p +ᵥ q) -ᵥ g.toFun q<VAR>this : f.toFun (q -ᵥ p +ᵥ q) = f.linear (q -ᵥ p) +ᵥ f.toFun q<GOAL>f q = g q
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : Module k V1<VAR>inst✝⁹ : AffineSpace V1 P1<VAR>inst✝⁸ : AddCommGroup V2<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : AffineSpace V2 P2<VAR>inst✝⁵ : AddCommGroup V3<VAR>inst✝⁴ : Module k V3<VAR>inst✝³ : AffineSpace V3 P3<VAR>inst✝² : AddCommGroup V4<VAR>inst✝¹ : Module k V4<VAR>inst✝ : AffineSpace V4 P4<VAR>f g : P1 →ᵃ[k] P2<VAR>h₁ : f.linear = g.linear<VAR>p : P1<VAR>h₂ : f p = g p<VAR>q : P1<VAR>hgl : g.linear (q -ᵥ p) = g.toFun (q -ᵥ p +ᵥ q) -ᵥ g.toFun q<VAR>this : f q -ᵥ g p +ᵥ f q = g.toFun (q -ᵥ p +ᵥ q) -ᵥ g.toFun q +ᵥ f q<GOAL>f q = g q
<VAR>p : ℝ<VAR>hp : Fact (0 < p)<VAR>u : AddCircle p<VAR>hu : IsOfFinAddOrder u<VAR>n : ℕ := addOrderOf u<GOAL>∃ k, ‖u‖ = p * (↑k / ↑n)
<VAR>p : ℝ<VAR>hp : Fact (0 < p)<VAR>u : AddCircle p<VAR>hu : IsOfFinAddOrder u<VAR>n : ℕ := addOrderOf u<VAR>m : ℕ<VAR>hm : ↑(↑m / ↑(addOrderOf u) * p) = u<GOAL>∃ k, ‖u‖ = p * (↑k / ↑n)
<VAR>p : ℝ<VAR>hp : Fact (0 < p)<VAR>u : AddCircle p<VAR>hu : IsOfFinAddOrder u<VAR>n : ℕ := addOrderOf u<VAR>m : ℕ<VAR>hm : ↑(↑m / ↑(addOrderOf u) * p) = u<GOAL>‖u‖ = p * (↑(min (m % n) (n - m % n)) / ↑n)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>h_countable : (Set.range τ).Countable<VAR>i : ι<GOAL>MeasurableSet {ω | τ ω < i}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>h_countable : (Set.range τ).Countable<VAR>i : ι<VAR>this : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i}<GOAL>MeasurableSet {ω | τ ω < i}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>h_countable : (Set.range τ).Countable<VAR>i : ι<VAR>this : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i}<GOAL>MeasurableSet ({ω | τ ω ≤ i} \ {ω | τ ω = i})
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝² : Category.{?u.60069, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>F : J ⥤ C<VAR>c : Cocone F<VAR>inst✝ : G.IsEquivalence<VAR>hc : IsVanKampenColimit c<VAR>e : F ⋙ G ⋙ G.inv ≅ F := NatIso.hcomp (Iso.refl F) G.asEquivalence.unitIso.symm<GOAL>IsVanKampenColimit (G.mapCocone c)
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝² : Category.{?u.60069, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>F : J ⥤ C<VAR>c : Cocone F<VAR>inst✝ : G.IsEquivalence<VAR>hc : IsVanKampenColimit c<VAR>e : F ⋙ G ⋙ G.inv ≅ F := NatIso.hcomp (Iso.refl F) G.asEquivalence.unitIso.symm<GOAL>IsVanKampenColimit (G.inv.mapCocone (G.mapCocone c))
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝² : Category.{?u.60069, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>F : J ⥤ C<VAR>c : Cocone F<VAR>inst✝ : G.IsEquivalence<VAR>hc : IsVanKampenColimit c<VAR>e : F ⋙ G ⋙ G.inv ≅ F := NatIso.hcomp (Iso.refl F) G.asEquivalence.unitIso.symm<GOAL>IsVanKampenColimit ((Cocones.precompose e.inv).obj (G.inv.mapCocone (G.mapCocone c)))
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε<VAR>f : Ω →ᵇ ℝ<VAR>f_nn : 0 ≤ᶠ[ae μ] ⇑f<GOAL>∫ (ω : Ω), f ω ∂μ ≤ (∫ (t : ℝ) in Ioc 0 ‖f‖, (ν (thickening ε {a | t ≤ f a})).toReal) + ε * ‖f‖
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε<VAR>f : Ω →ᵇ ℝ<VAR>f_nn : 0 ≤ᶠ[ae μ] ⇑f<GOAL>∫ (t : ℝ) in Ioc 0 ‖f‖, (μ {a | t ≤ f a}).toReal ≤ (∫ (t : ℝ) in Ioc 0 ‖f‖, (ν (thickening ε {a | t ≤ f a})).toReal) + ε * ‖f‖
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε<VAR>f : Ω →ᵇ ℝ<VAR>f_nn : 0 ≤ᶠ[ae μ] ⇑f<VAR>key : (fun t => (μ {a | t ≤ f a}).toReal) ≤ fun t => (ν (thickening ε {a | t ≤ f a})).toReal + ε<VAR>intble₁ : IntegrableOn (fun t => (μ {a | t ≤ f a}).toReal) (Ioc 0 ‖f‖) volume<VAR>intble₂ : IntegrableOn (fun t => (ν (thickening ε {a | t ≤ f a})).toReal) (Ioc 0 ‖f‖) volume<GOAL>∫ (t : ℝ) in Ioc 0 ‖f‖, (μ {a | t ≤ f a}).toReal ≤ (∫ (t : ℝ) in Ioc 0 ‖f‖, (ν (thickening ε {a | t ≤ f a})).toReal) + ε * ‖f‖
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε<VAR>f : Ω →ᵇ ℝ<VAR>f_nn : 0 ≤ᶠ[ae μ] ⇑f<VAR>key : (fun t => (μ {a | t ≤ f a}).toReal) ≤ fun t => (ν (thickening ε {a | t ≤ f a})).toReal + ε<VAR>intble₁ : IntegrableOn (fun t => (μ {a | t ≤ f a}).toReal) (Ioc 0 ‖f‖) volume<VAR>intble₂ : IntegrableOn (fun t => (ν (thickening ε {a | t ≤ f a})).toReal) (Ioc 0 ‖f‖) volume<GOAL>∫ (x : ℝ) in Ioc 0 ‖f‖, (ν (thickening ε {a | x ≤ f a})).toReal + ε ∂volume ≤ (∫ (t : ℝ) in Ioc 0 ‖f‖, (ν (thickening ε {a | t ≤ f a})).toReal) + ε * ‖f‖
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε<VAR>f : Ω →ᵇ ℝ<VAR>f_nn : 0 ≤ᶠ[ae μ] ⇑f<VAR>key : (fun t => (μ {a | t ≤ f a}).toReal) ≤ fun t => (ν (thickening ε {a | t ≤ f a})).toReal + ε<VAR>intble₁ : IntegrableOn (fun t => (μ {a | t ≤ f a}).toReal) (Ioc 0 ‖f‖) volume<VAR>intble₂ : IntegrableOn (fun t => (ν (thickening ε {a | t ≤ f a})).toReal) (Ioc 0 ‖f‖) volume<GOAL>IntegrableOn (fun t => (μ {a | t ≤ f a}).toReal) (Ioc 0 ‖f‖) volume
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε<VAR>f : Ω →ᵇ ℝ<VAR>f_nn : 0 ≤ᶠ[ae μ] ⇑f<VAR>key : (fun t => (μ {a | t ≤ f a}).toReal) ≤ fun t => (ν (thickening ε {a | t ≤ f a})).toReal + ε<VAR>intble₁ : IntegrableOn (fun t => (μ {a | t ≤ f a}).toReal) (Ioc 0 ‖f‖) volume<VAR>intble₂ : IntegrableOn (fun t => (ν (thickening ε {a | t ≤ f a})).toReal) (Ioc 0 ‖f‖) volume<GOAL>IntegrableOn (fun t => (ν (thickening ε {a | t ≤ f a})).toReal + ε) (Ioc 0 ‖f‖) volume
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : CompactSpace α<VAR>inst✝¹ : MetricSpace β<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : C(α, β)<VAR>C : ℝ<VAR>C0 : 0 ≤ C<GOAL>dist f g ≤ C ↔ ∀ (x : α), dist (f x) (g x) ≤ C
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>hm : m ≤ m0<VAR>f : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>hf : FinStronglyMeasurable f (μ.trim hm)<GOAL>f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>hm : m ≤ m0<VAR>f : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>hf : FinStronglyMeasurable f (μ.trim hm)<VAR>t : Set α<VAR>ht_meas : MeasurableSet t<VAR>htf_zero : ∀ x ∈ tᶜ, f x = 0<VAR>htμ : SigmaFinite ((μ.trim hm).restrict t)<GOAL>f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>hm : m ≤ m0<VAR>f : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>hf : FinStronglyMeasurable f (μ.trim hm)<VAR>t : Set α<VAR>ht_meas : MeasurableSet t<VAR>htf_zero : ∀ x ∈ tᶜ, f x = 0<VAR>htμ : SigmaFinite ((μ.trim hm).restrict t)<VAR>this : SigmaFinite ((μ.restrict t).trim hm)<GOAL>f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>hm : m ≤ m0<VAR>f : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>hf : FinStronglyMeasurable f (μ.trim hm)<VAR>t : Set α<VAR>ht_meas : MeasurableSet t<VAR>htf_zero✝ : ∀ x ∈ tᶜ, f x = 0<VAR>htμ : SigmaFinite ((μ.trim hm).restrict t)<VAR>this : SigmaFinite ((μ.restrict t).trim hm)<VAR>htf_zero : f =ᶠ[ae (μ.restrict tᶜ)] 0<GOAL>f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>hm : m ≤ m0<VAR>f : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>hf : FinStronglyMeasurable f (μ.trim hm)<VAR>t : Set α<VAR>ht_meas : MeasurableSet t<VAR>htf_zero✝ : ∀ x ∈ tᶜ, f x = 0<VAR>htμ : SigmaFinite ((μ.trim hm).restrict t)<VAR>this : SigmaFinite ((μ.restrict t).trim hm)<VAR>htf_zero : f =ᶠ[ae (μ.restrict tᶜ)] 0<VAR>hf_meas_m : StronglyMeasurable f<GOAL>f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>hm : m ≤ m0<VAR>f : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>hf : FinStronglyMeasurable f (μ.trim hm)<VAR>t : Set α<VAR>ht_meas : MeasurableSet t<VAR>htf_zero✝ : ∀ x ∈ tᶜ, f x = 0<VAR>htμ : SigmaFinite ((μ.trim hm).restrict t)<VAR>this : SigmaFinite ((μ.restrict t).trim hm)<VAR>htf_zero : f =ᶠ[ae (μ.restrict tᶜ)] 0<VAR>hf_meas_m : StronglyMeasurable f<GOAL>f =ᶠ[ae (μ.restrict t)] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>hm : m ≤ m0<VAR>f : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>hf : FinStronglyMeasurable f (μ.trim hm)<VAR>t : Set α<VAR>ht_meas : MeasurableSet t<VAR>htf_zero✝ : ∀ x ∈ tᶜ, f x = 0<VAR>htμ : SigmaFinite ((μ.trim hm).restrict t)<VAR>this : SigmaFinite ((μ.restrict t).trim hm)<VAR>htf_zero : f =ᶠ[ae (μ.restrict tᶜ)] 0<VAR>hf_meas_m : StronglyMeasurable f<GOAL>((μ.restrict t).trim hm) {x | (fun x => f x = 0 x) x}ᶜ = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>hm : m ≤ m0<VAR>f : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>hf : FinStronglyMeasurable f (μ.trim hm)<VAR>t : Set α<VAR>ht_meas : MeasurableSet t<VAR>htf_zero✝ : ∀ x ∈ tᶜ, f x = 0<VAR>htμ : SigmaFinite ((μ.trim hm).restrict t)<VAR>this : SigmaFinite ((μ.restrict t).trim hm)<VAR>htf_zero : f =ᶠ[ae (μ.restrict tᶜ)] 0<VAR>hf_meas_m : StronglyMeasurable f<GOAL>∀ (s : Set α), MeasurableSet s → ((μ.restrict t).trim hm) s < ⊤ → IntegrableOn f s ((μ.restrict t).trim hm)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>hm : m ≤ m0<VAR>f : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>hf : FinStronglyMeasurable f (μ.trim hm)<VAR>t : Set α<VAR>ht_meas : MeasurableSet t<VAR>htf_zero✝ : ∀ x ∈ tᶜ, f x = 0<VAR>htμ : SigmaFinite ((μ.trim hm).restrict t)<VAR>this : SigmaFinite ((μ.restrict t).trim hm)<VAR>htf_zero : f =ᶠ[ae (μ.restrict tᶜ)] 0<VAR>hf_meas_m : StronglyMeasurable f<GOAL>∀ (s : Set α), MeasurableSet s → ((μ.restrict t).trim hm) s < ⊤ → ∫ (x : α) in s, f x ∂(μ.restrict t).trim hm = 0
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>∫ (x : ℝ) in a..b, sin x = cos a - cos b
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>-cos b - -cos a = cos a - cos b
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>(deriv fun x => -cos x) = sin
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>∀ x ∈ [[a, b]], DifferentiableAt ℝ (fun x => -cos x) x
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>ContinuousOn sin [[a, b]]
<VAR>J : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>F : J ⥤ C<VAR>inst✝¹ : HasColimit F<VAR>E : K ⥤ J<VAR>inst✝ : HasColimit (E ⋙ F)<VAR>c : Cocone F<VAR>j✝ : K<GOAL>ι (E ⋙ F) j✝ ≫ pre F E ≫ desc F c = ι (E ⋙ F) j✝ ≫ desc (E ⋙ F) (Cocone.whisker E c)
<VAR>J : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>F : J ⥤ C<VAR>inst✝¹ : HasColimit F<VAR>E : K ⥤ J<VAR>inst✝ : HasColimit (E ⋙ F)<VAR>c : Cocone F<VAR>j✝ : K<GOAL>ι F (E.obj j✝) ≫ desc F c = ι (E ⋙ F) j✝ ≫ desc (E ⋙ F) (Cocone.whisker E c)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>γ : Type w<VAR>inst✝¹ : MetricSpace γ<VAR>x : γ<VAR>s : Set γ<VAR>inst✝ : MetricSpace β<VAR>f : γ → β<GOAL>UniformEmbedding f ↔ (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, dist a b < δ → dist (f a) (f b) < ε) ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 E'<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁴ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝³ : AddGroup G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : BorelSpace G<VAR>hcf : HasCompactSupport f<VAR>hf : LocallyIntegrable f μ<VAR>hg : Continuous g<VAR>x₀ : G<GOAL>ConvolutionExistsAt f g x₀ L μ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 E'<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁴ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝³ : AddGroup G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : BorelSpace G<VAR>hcf : HasCompactSupport f<VAR>hf : LocallyIntegrable f μ<VAR>hg : Continuous g<VAR>x₀ : G<GOAL>HasCompactSupport fun t => (L (f t)) (g (x₀ - t))
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 E'<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁴ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝³ : AddGroup G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : BorelSpace G<VAR>hcf : HasCompactSupport f<VAR>hf : LocallyIntegrable f μ<VAR>hg : Continuous g<VAR>x₀ : G<GOAL>(support fun t => (L (f t)) (g (x₀ - t))) ⊆ support f
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 E'<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁴ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝³ : AddGroup G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : BorelSpace G<VAR>hcf : HasCompactSupport f<VAR>hf : LocallyIntegrable f μ<VAR>hg : Continuous g<VAR>x₀ t : G<VAR>ht : f t = 0<GOAL>(fun t => (L (f t)) (g (x₀ - t))) t = 0