ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>inst✝¹ : BorelSpace E<VAR>f : β → E<VAR>μ : Measure β<VAR>fmeas : Measurable f<VAR>hf : Memℒp f p μ<VAR>s : Set E<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>hi₀ : Memℒp (fun x => y₀) p μ<VAR>n : ℕ<GOAL>eLpNorm (↑(approxOn f fmeas s y₀ h₀ n)) p μ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>inst✝¹ : BorelSpace E<VAR>f : β → E<VAR>μ : Measure β<VAR>fmeas : Measurable f<VAR>hf : Memℒp f p μ<VAR>s : Set E<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>hi₀ : Memℒp (fun x => y₀) p μ<VAR>n : ℕ<GOAL>eLpNorm (fun x => ↑(approxOn f fmeas s y₀ h₀ n) x - y₀) p μ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>inst✝¹ : BorelSpace E<VAR>f : β → E<VAR>μ : Measure β<VAR>fmeas : Measurable f<VAR>hf : Memℒp f p μ<VAR>s : Set E<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>hi₀ : Memℒp (fun x => y₀) p μ<VAR>n : ℕ<VAR>hf' : Memℒp (fun x => ‖f x - y₀‖) p μ<GOAL>eLpNorm (fun x => ↑(approxOn f fmeas s y₀ h₀ n) x - y₀) p μ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>inst✝¹ : BorelSpace E<VAR>f : β → E<VAR>μ : Measure β<VAR>fmeas : Measurable f<VAR>hf : Memℒp f p μ<VAR>s : Set E<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>hi₀ : Memℒp (fun x => y₀) p μ<VAR>n : ℕ<VAR>hf' : Memℒp (fun x => ‖f x - y₀‖) p μ<VAR>this : ∀ᵐ (x : β) ∂μ, ‖↑(approxOn f fmeas s y₀ h₀ n) x - y₀‖ ≤ ‖‖f x - y₀‖ + ‖f x - y₀‖‖<GOAL>eLpNorm (fun x => ↑(approxOn f fmeas s y₀ h₀ n) x - y₀) p μ < ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>N : Type u_4<VAR>N' : Type u_5<VAR>P : Type u_6<VAR>P' : Type u_7<VAR>f : M → N<VAR>g : N → P<VAR>g' : P → P'<VAR>inst✝¹ : Zero P<VAR>inst✝ : Zero P'<VAR>exact : Exact f g<VAR>inj : Injective g'<VAR>h0 : g' 0 = 0<VAR>x : N<GOAL>(g' ∘ g) x = 0 ↔ x ∈ Set.range f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>N : Type u_4<VAR>N' : Type u_5<VAR>P : Type u_6<VAR>P' : Type u_7<VAR>f : M → N<VAR>g : N → P<VAR>g' : P → P'<VAR>inst✝¹ : Zero P<VAR>inst✝ : Zero P'<VAR>exact : Exact f g<VAR>inj : Injective g'<VAR>h0 : g' 0 = 0<VAR>x : N<GOAL>x ∈ Set.range f → (g' ∘ g) x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>N : Type u_4<VAR>N' : Type u_5<VAR>P : Type u_6<VAR>P' : Type u_7<VAR>f : M → N<VAR>g : N → P<VAR>g' : P → P'<VAR>inst✝¹ : Zero P<VAR>inst✝ : Zero P'<VAR>exact : Exact f g<VAR>inj : Injective g'<VAR>h0 : g' 0 = 0<VAR>x : N<VAR>H : x ∈ Set.range f<GOAL>(g' ∘ g) x = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : LinearOrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>x✝ y z : E<VAR>hf : ConvexOn 𝕜 ((convexHull 𝕜) s) f<VAR>x : E<VAR>hx : x ∈ (convexHull 𝕜) s<GOAL>∃ y ∈ s, f x ≤ f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : LinearOrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>x✝ y z : E<VAR>hf : ConvexOn 𝕜 ((convexHull 𝕜) s) f<VAR>x : E<VAR>hx : x ∈ {x | ∃ ι t w z, (∀ i ∈ t, 0 ≤ w i) ∧ ∑ i ∈ t, w i = 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x}<GOAL>∃ y ∈ s, f x ≤ f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : LinearOrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t✝ : Finset ι<VAR>w✝ : ι → 𝕜<VAR>p✝ : ι → E<VAR>x y z : E<VAR>hf : ConvexOn 𝕜 ((convexHull 𝕜) s) f<VAR>α : Type<VAR>t : Finset α<VAR>w : α → 𝕜<VAR>p : α → E<VAR>hw₀ : ∀ i ∈ t, 0 ≤ w i<VAR>hw₁ : ∑ i ∈ t, w i = 1<VAR>hp : ∀ i ∈ t, p i ∈ s<GOAL>∃ y ∈ s, f (t.centerMass w p) ≤ f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : LinearOrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t✝ : Finset ι<VAR>w✝ : ι → 𝕜<VAR>p✝ : ι → E<VAR>x y z : E<VAR>hf : ConvexOn 𝕜 ((convexHull 𝕜) s) f<VAR>α : Type<VAR>t : Finset α<VAR>w : α → 𝕜<VAR>p : α → E<VAR>hw₀ : ∀ i ∈ t, 0 ≤ w i<VAR>hw₁ : ∑ i ∈ t, w i = 1<VAR>hp : ∀ i ∈ t, p i ∈ s<VAR>i : α<VAR>hit : i ∈ t<VAR>Hi : f (t.centerMass w p) ≤ f (p i)<GOAL>∃ y ∈ s, f (t.centerMass w p) ≤ f y
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ✝ : Type x<VAR>γ : Type u_1<VAR>P : γ → Set γ → Prop<VAR>h : ∀ (t : Set γ), t.Finite → ∃ c, P c t<GOAL>∃ u, ∀ (n : ℕ), P (u n) (u '' Iio n)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ✝ : Type x<VAR>γ : Type u_1<VAR>P : γ → Set γ → Prop<VAR>h : ∀ (t : Set γ), t.Finite → ∃ c, P c t<VAR>this : Nonempty γ<GOAL>∃ u, ∀ (n : ℕ), P (u n) (u '' Iio n)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ✝ : Type x<VAR>γ : Type u_1<VAR>P : γ → Set γ → Prop<VAR>this : Nonempty γ<VAR>c : Set γ → γ<VAR>hc : ∀ (t : Set γ), t.Finite → P (c t) t<GOAL>∃ u, ∀ (n : ℕ), P (u n) (u '' Iio n)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ✝ : Type x<VAR>γ : Type u_1<VAR>P : γ → Set γ → Prop<VAR>this : Nonempty γ<VAR>c : Set γ → γ<VAR>hc : ∀ (t : Set γ), t.Finite → P (c t) t<VAR>f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g => c (range fun k => g ↑k ⋯)<GOAL>∃ u, ∀ (n : ℕ), P (u n) (u '' Iio n)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ✝ : Type x<VAR>γ : Type u_1<VAR>P : γ → Set γ → Prop<VAR>this : Nonempty γ<VAR>c : Set γ → γ<VAR>hc : ∀ (t : Set γ), t.Finite → P (c t) t<VAR>f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g => c (range fun k => g ↑k ⋯)<VAR>u : ℕ → γ := fun n => n.strongRecOn' f<VAR>n : ℕ<GOAL>P (u n) (u '' Iio n)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ✝ : Type x<VAR>γ : Type u_1<VAR>P : γ → Set γ → Prop<VAR>this : Nonempty γ<VAR>c : Set γ → γ<VAR>hc : ∀ (t : Set γ), t.Finite → P (c t) t<VAR>f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g => c (range fun k => g ↑k ⋯)<VAR>u : ℕ → γ := fun n => n.strongRecOn' f<VAR>n : ℕ<GOAL>u n = c (u '' Iio n)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ✝ : Type x<VAR>γ : Type u_1<VAR>P : γ → Set γ → Prop<VAR>this : Nonempty γ<VAR>c : Set γ → γ<VAR>hc : ∀ (t : Set γ), t.Finite → P (c t) t<VAR>f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g => c (range fun k => g ↑k ⋯)<VAR>u : ℕ → γ := fun n => n.strongRecOn' f<VAR>n : ℕ<GOAL>u n = c (range fun x => u ↑x)
<VAR>α : Type u_1<VAR>g : GenContFract α<VAR>n : ℕ<GOAL>g.TerminatedAt n ↔ g.partDens.get? n = none
<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>s : Finset α<VAR>n : ℕ<VAR>f : α → ℕ<GOAL>(Multiset.map (fun x => x % n) (Multiset.map (fun i => f i) s.val)).sum % n = (∑ i ∈ s, f i % n) % n
<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>s : Finset α<VAR>n : ℕ<VAR>f : α → ℕ<GOAL>(Multiset.map ((fun x => x % n) ∘ fun i => f i) s.val).sum % n = (Multiset.map (fun i => f i % n) s.val).sum % n
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f✝ f : V → E<VAR>k : ℕ∞<VAR>hf : ContDiff ℝ k f<VAR>n : ℕ<GOAL>ContDiff ℝ k fun v => VectorFourier.fourierPowSMulRight L f v n
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f✝ f : V → E<VAR>k : ℕ∞<VAR>hf : ContDiff ℝ k f<VAR>n : ℕ<GOAL>ContDiff ℝ k fun v => (-(2 * ↑π * I)) ^ n • ((smulRightL ℝ (fun x => W) E) ((ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight fun x => L v)) (f v)
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f✝ f : V → E<VAR>k : ℕ∞<VAR>hf : ContDiff ℝ k f<VAR>n : ℕ<GOAL>ContDiff ℝ k fun y => ((smulRightL ℝ (fun x => W) E) ((ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight fun x => L y)) (f y)
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f✝ f : V → E<VAR>k : ℕ∞<VAR>hf : ContDiff ℝ k f<VAR>n : ℕ<GOAL>ContDiff ℝ k fun x => (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight fun x_1 => L x
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f✝ f : V → E<VAR>k : ℕ∞<VAR>hf : ContDiff ℝ k f<VAR>n : ℕ<GOAL>ContDiff ℝ k fun x x_1 => L x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f✝ g✝ : α → M<VAR>a b : α<VAR>s✝ t✝ s : Set α<VAR>t : Set β<VAR>f : α → M<VAR>g : β → M<VAR>e : α → β<VAR>he₀ : BijOn e s t<VAR>he₁ : ∀ x ∈ s, f x = g (e x)<GOAL>∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (j : β) (_ : j ∈ t), g j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f✝ g✝ : α → M<VAR>a b : α<VAR>s✝ t✝ s : Set α<VAR>t : Set β<VAR>f : α → M<VAR>g : β → M<VAR>e : α → β<VAR>he₀ : BijOn e s t<VAR>he₁ : ∀ x ∈ s, f x = g (e x)<GOAL>∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (j : α) (_ : j ∈ s), g (e j)
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w✝ x✝ y : V<VAR>inst✝ : DecidableEq V<VAR>u v w : V<VAR>p : G.Walk v w<VAR>h : u ∈ p.support<VAR>x : G.Dart<VAR>hx : x ∈ (p.takeUntil u h).darts<GOAL>x ∈ p.darts
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w✝ x✝ y : V<VAR>inst✝ : DecidableEq V<VAR>u v w : V<VAR>p : G.Walk v w<VAR>h : u ∈ p.support<VAR>x : G.Dart<VAR>hx : x ∈ (p.takeUntil u h).darts<GOAL>x ∈ (p.takeUntil u h).darts ∨ x ∈ (p.dropUntil u h).darts
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : Fintype m<VAR>inst✝¹ : CommRing α<VAR>inst✝ : Subsingleton n<VAR>A : Matrix n n α<VAR>i j : n<GOAL>A.adjugate i j = 1 i j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>h_surj : Surjective f<VAR>a : α<GOAL>SurjOn f (Ici a) (Ici (f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>h_surj : Surjective f<VAR>a : α<GOAL>SurjOn f (Ioi a ∪ {a}) (Ioi (f a) ∪ {f a})
<VAR>f g : ℂ → ℂ<VAR>s : Set ℂ<VAR>f' g' x c : ℂ<VAR>hf : HasStrictDerivAt f f' x<VAR>hg : HasStrictDerivAt g g' x<VAR>h0 : f x ∈ slitPlane<GOAL>HasStrictDerivAt (fun x => f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') x
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>f : α → β<VAR>inst✝ : Zero β<VAR>hs : MeasurableSet s<VAR>hf : f =ᶠ[ae (μ.restrict sᶜ)] 0<GOAL>s.indicator f =ᶠ[ae μ] f
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>f : α → β<VAR>inst✝ : Zero β<VAR>hs : MeasurableSet s<VAR>hf : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → f x = 0 x<GOAL>s.indicator f =ᶠ[ae μ] f
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>f : α → β<VAR>inst✝ : Zero β<VAR>hs : MeasurableSet s<VAR>hf : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → f x = 0 x<VAR>x : α<VAR>hx : x ∈ sᶜ → f x = 0 x<GOAL>s.indicator f x = f x
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m : (s : Set α) → MeasurableSet s → ℝ≥0∞<VAR>m0 : m ∅ ⋯ = 0<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<GOAL>∀ (s : ℕ → Set α), extend m (⋃ i, s i) ≤ ∑' (i : ℕ), extend m (s i)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m : (s : Set α) → MeasurableSet s → ℝ≥0∞<VAR>m0 : m ∅ ⋯ = 0<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<GOAL>∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m : (s : Set α) → MeasurableSet s → ℝ≥0∞<VAR>m0 : m ∅ ⋯ = 0<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>f : ℕ → Set α<VAR>h : ∀ (i : ℕ), MeasurableSet (f i)<GOAL>m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m : (s : Set α) → MeasurableSet s → ℝ≥0∞<VAR>m0 : m ∅ ⋯ = 0<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>f : ℕ → Set α<VAR>h : ∀ (i : ℕ), MeasurableSet (f i)<GOAL>m (⋃ n, disjointed f n) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m : (s : Set α) → MeasurableSet s → ℝ≥0∞<VAR>m0 : m ∅ ⋯ = 0<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>f : ℕ → Set α<VAR>h : ∀ (i : ℕ), MeasurableSet (f i)<GOAL>∑' (i : ℕ), m (disjointed f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m : (s : Set α) → MeasurableSet s → ℝ≥0∞<VAR>m0 : m ∅ ⋯ = 0<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>f : ℕ → Set α<VAR>h : ∀ (i : ℕ), MeasurableSet (f i)<VAR>i : ℕ<GOAL>m (disjointed f i) ⋯ ≤ m (f i) ⋯
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m : (s : Set α) → MeasurableSet s → ℝ≥0∞<VAR>m0 : m ∅ ⋯ = 0<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>f : ℕ → Set α<VAR>h : ∀ (i : ℕ), MeasurableSet (f i)<VAR>i : ℕ<GOAL>extend m (disjointed f i) ≤ extend m (f i)
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α : Type v<VAR>inst✝¹ : CommRing α<VAR>inst✝ : StarRing α<VAR>A✝ : Matrix n n α<VAR>A B : ↥(unitaryGroup n α)<GOAL>↑(toGL (A * B)) = ↑(toGL A * toGL B)
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α : Type v<VAR>inst✝¹ : CommRing α<VAR>inst✝ : StarRing α<VAR>A✝ : Matrix n n α<VAR>A B : ↥(unitaryGroup n α)<GOAL>toLin' A ∘ₗ toLin' B = ↑(toGL A * toGL B)
<VAR>x y z : ℝ<GOAL>0 ≤ sinh x ↔ 0 ≤ x
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>inst✝⁵ : Category.{v₁, u₁} C₁<VAR>inst✝⁴ : Category.{v₂, u₂} C₂<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>D₁ : Type u_1<VAR>D₂ : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} D₁<VAR>inst✝² : Category.{u_3, u_2} D₂<VAR>L₁ : C₁ ⥤ D₁<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝¹ : L₁.IsLocalization W₁<VAR>inst✝ : L₂.IsLocalization W₂<VAR>F : D₁ ⥤ D₂<VAR>h : Φ.IsRightDerivabilityStructure<VAR>e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ F<GOAL>TwoSquare.GuitartExact e.hom
<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>f : α →. β ⊕ α<VAR>b : β<VAR>a a' : α<VAR>hb : b ∈ f.fix a<VAR>ha' : Sum.inr a' ∈ f a<GOAL>b ∈ f.fix a'
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>inst✝⁵ : NormedAddCommGroup H<VAR>inst✝⁴ : NormedSpace 𝕜 H<VAR>𝕝 : Type u_7<VAR>inst✝³ : NontriviallyNormedField 𝕝<VAR>inst✝² : NormedAlgebra 𝕜 𝕝<VAR>A : Type u_8<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>e : E<VAR>f : E → F<VAR>g : E → G<VAR>r s : ℝ≥0∞<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>q : FormalMultilinearSeries 𝕜 E G<VAR>hf : HasFPowerSeriesOnBall f p e r<VAR>hg : HasFPowerSeriesOnBall g q e s<GOAL>min r s ≤ (p.prod q).radius
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>inst✝⁵ : NormedAddCommGroup H<VAR>inst✝⁴ : NormedSpace 𝕜 H<VAR>𝕝 : Type u_7<VAR>inst✝³ : NontriviallyNormedField 𝕝<VAR>inst✝² : NormedAlgebra 𝕜 𝕝<VAR>A : Type u_8<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>e : E<VAR>f : E → F<VAR>g : E → G<VAR>r s : ℝ≥0∞<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>q : FormalMultilinearSeries 𝕜 E G<VAR>hf : HasFPowerSeriesOnBall f p e r<VAR>hg : HasFPowerSeriesOnBall g q e s<GOAL>min r s ≤ min p.radius q.radius
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>inst✝⁵ : NormedAddCommGroup H<VAR>inst✝⁴ : NormedSpace 𝕜 H<VAR>𝕝 : Type u_7<VAR>inst✝³ : NontriviallyNormedField 𝕝<VAR>inst✝² : NormedAlgebra 𝕜 𝕝<VAR>A : Type u_8<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>e : E<VAR>f : E → F<VAR>g : E → G<VAR>r s : ℝ≥0∞<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>q : FormalMultilinearSeries 𝕜 E G<VAR>hf : HasFPowerSeriesOnBall f p e r<VAR>hg : HasFPowerSeriesOnBall g q e s<VAR>y : E<VAR>hy : y ∈ EMetric.ball 0 (min r s)<GOAL>HasSum (fun n => (p.prod q n) fun x => y) (f (e + y), g (e + y))
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>inst✝⁵ : NormedAddCommGroup H<VAR>inst✝⁴ : NormedSpace 𝕜 H<VAR>𝕝 : Type u_7<VAR>inst✝³ : NontriviallyNormedField 𝕝<VAR>inst✝² : NormedAlgebra 𝕜 𝕝<VAR>A : Type u_8<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>e : E<VAR>f : E → F<VAR>g : E → G<VAR>r s : ℝ≥0∞<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>q : FormalMultilinearSeries 𝕜 E G<VAR>hf : HasFPowerSeriesOnBall f p e r<VAR>hg : HasFPowerSeriesOnBall g q e s<VAR>y : E<VAR>hy : y ∈ EMetric.ball 0 (min r s)<GOAL>HasSum (fun n => ((p n) fun x => y, (q n) fun x => y)) (f (e + y), g (e + y))
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>inst✝⁵ : NormedAddCommGroup H<VAR>inst✝⁴ : NormedSpace 𝕜 H<VAR>𝕝 : Type u_7<VAR>inst✝³ : NontriviallyNormedField 𝕝<VAR>inst✝² : NormedAlgebra 𝕜 𝕝<VAR>A : Type u_8<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>e : E<VAR>f : E → F<VAR>g : E → G<VAR>r s : ℝ≥0∞<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>q : FormalMultilinearSeries 𝕜 E G<VAR>hf : HasFPowerSeriesOnBall f p e r<VAR>hg : HasFPowerSeriesOnBall g q e s<VAR>y : E<VAR>hy : y ∈ EMetric.ball 0 (min r s)<GOAL>y ∈ EMetric.ball 0 r
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>inst✝⁵ : NormedAddCommGroup H<VAR>inst✝⁴ : NormedSpace 𝕜 H<VAR>𝕝 : Type u_7<VAR>inst✝³ : NontriviallyNormedField 𝕝<VAR>inst✝² : NormedAlgebra 𝕜 𝕝<VAR>A : Type u_8<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>e : E<VAR>f : E → F<VAR>g : E → G<VAR>r s : ℝ≥0∞<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>q : FormalMultilinearSeries 𝕜 E G<VAR>hf : HasFPowerSeriesOnBall f p e r<VAR>hg : HasFPowerSeriesOnBall g q e s<VAR>y : E<VAR>hy : y ∈ EMetric.ball 0 (min r s)<GOAL>y ∈ EMetric.ball 0 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>A B : E →WOT[𝕜]F<VAR>h : ∀ (x : E) (y : NormedSpace.Dual 𝕜 F), y (A x) = y (B x)<GOAL>A = B
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>A B : E →WOT[𝕜]F<VAR>h : ∀ (x : E) (y : NormedSpace.Dual 𝕜 F), y (A x) = y (B x)<GOAL>∀ (x : E), A x = B x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>A B : E →WOT[𝕜]F<VAR>x : E<VAR>h : ∀ (y : NormedSpace.Dual 𝕜 F), y (A x) = y (B x)<GOAL>A x = B x
<VAR>𝒮 : Type u₁<VAR>inst✝ : Category.{v₁, u₁} 𝒮<VAR>𝒳 : BasedCategory 𝒮<VAR>𝒴 : BasedCategory 𝒮<VAR>F : 𝒳 ⥤ᵇ 𝒴<VAR>a : 𝒳.obj<GOAL>𝒴.p.obj (F.obj a) = 𝒳.p.obj a
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁶ : AddCommMonoid A<VAR>inst✝⁵ : AddCommMonoid B<VAR>inst✝⁴ : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝³ : Zero M<VAR>inst✝² : Zero M'<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DecidableEq α<VAR>f : α →₀ M<VAR>a : α<VAR>b : α → M → N<GOAL>(∏ a_1 ∈ f.support, if a = a_1 then b a_1 (f a_1) else 1) = if a ∈ f.support then b a (f a) else 1