ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>inst✝⁹ : NormedSpace 𝕜 E''<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : CompleteSpace F<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup P<VAR>inst✝ : NormedSpace 𝕜 P<VAR>μ : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>g : P → G → E'<VAR>s : Set P<VAR>k : Set G<VAR>hs : IsOpen s<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ univ)<VAR>q₀ : P × G<VAR>hq₀ : q₀.1 ∈ s<VAR>g' : P × G → P × G →L[𝕜] E' := fderiv 𝕜 ↿g<VAR>A : ∀ p ∈ s, Continuous (g p)<VAR>A' : ∀ (q : P × G), q.1 ∈ s → s ×ˢ univ ∈ 𝓝 q<VAR>g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0<VAR>ε C : ℝ<VAR>εpos : 0 < ε<VAR>h₀ε : ball q₀.1 ε ⊆ s<VAR>hε : ∀ (p : P) (x : G), ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C<VAR>I1 : ∀ᶠ (x : P × G) in 𝓝 q₀, AEStronglyMeasurable (fun a => (L (f a)) (g x.1 (x.2 - a))) μ<VAR>I2 : Integrable (fun a => (L (f a)) (g q₀.1 (q₀.2 - a))) μ<VAR>I3 : AEStronglyMeasurable (fun a => (L (f a)).comp (g' (q₀.1, q₀.2 - a))) μ<VAR>K' : Set G := -k + {q₀.2}<VAR>K'_def : K' = -k + {q₀.2}<VAR>hK' : IsCompact K'<VAR>U : Set G<VAR>U_open : IsOpen U<VAR>K'U : K' ⊆ U<VAR>hU : IntegrableOn f U μ<GOAL>HasFDerivAt (fun q => (f ⋆[L, μ] g q.1) q.2) ((f ⋆[precompR (P × G) L, μ] fun x => fderiv 𝕜 (↿g) (q₀.1, x)) q₀.2) q₀
<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✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>inst✝⁹ : NormedSpace 𝕜 E''<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : CompleteSpace F<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup P<VAR>inst✝ : NormedSpace 𝕜 P<VAR>μ : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>g : P → G → E'<VAR>s : Set P<VAR>k : Set G<VAR>hs : IsOpen s<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ univ)<VAR>q₀ : P × G<VAR>hq₀ : q₀.1 ∈ s<VAR>g' : P × G → P × G →L[𝕜] E' := fderiv 𝕜 ↿g<VAR>A : ∀ p ∈ s, Continuous (g p)<VAR>A' : ∀ (q : P × G), q.1 ∈ s → s ×ˢ univ ∈ 𝓝 q<VAR>g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0<VAR>ε C : ℝ<VAR>εpos : 0 < ε<VAR>h₀ε : ball q₀.1 ε ⊆ s<VAR>hε : ∀ (p : P) (x : G), ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C<VAR>I1 : ∀ᶠ (x : P × G) in 𝓝 q₀, AEStronglyMeasurable (fun a => (L (f a)) (g x.1 (x.2 - a))) μ<VAR>I2 : Integrable (fun a => (L (f a)) (g q₀.1 (q₀.2 - a))) μ<VAR>I3 : AEStronglyMeasurable (fun a => (L (f a)).comp (g' (q₀.1, q₀.2 - a))) μ<VAR>K' : Set G := -k + {q₀.2}<VAR>K'_def : K' = -k + {q₀.2}<VAR>hK' : IsCompact K'<VAR>U : Set G<VAR>U_open : IsOpen U<VAR>K'U : K' ⊆ U<VAR>hU : IntegrableOn f U μ<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>δε : δ ≤ ε<VAR>hδ : K' + ball 0 δ ⊆ U<GOAL>HasFDerivAt (fun q => (f ⋆[L, μ] g q.1) q.2) ((f ⋆[precompR (P × G) L, μ] fun x => fderiv 𝕜 (↿g) (q₀.1, x)) q₀.2) q₀
<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✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>inst✝⁹ : NormedSpace 𝕜 E''<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : CompleteSpace F<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup P<VAR>inst✝ : NormedSpace 𝕜 P<VAR>μ : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>g : P → G → E'<VAR>s : Set P<VAR>k : Set G<VAR>hs : IsOpen s<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ univ)<VAR>q₀ : P × G<VAR>hq₀ : q₀.1 ∈ s<VAR>g' : P × G → P × G →L[𝕜] E' := fderiv 𝕜 ↿g<VAR>A : ∀ p ∈ s, Continuous (g p)<VAR>A' : ∀ (q : P × G), q.1 ∈ s → s ×ˢ univ ∈ 𝓝 q<VAR>g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0<VAR>ε C : ℝ<VAR>εpos : 0 < ε<VAR>h₀ε : ball q₀.1 ε ⊆ s<VAR>hε : ∀ (p : P) (x : G), ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C<VAR>I1 : ∀ᶠ (x : P × G) in 𝓝 q₀, AEStronglyMeasurable (fun a => (L (f a)) (g x.1 (x.2 - a))) μ<VAR>I2 : Integrable (fun a => (L (f a)) (g q₀.1 (q₀.2 - a))) μ<VAR>I3 : AEStronglyMeasurable (fun a => (L (f a)).comp (g' (q₀.1, q₀.2 - a))) μ<VAR>K' : Set G := -k + {q₀.2}<VAR>K'_def : K' = -k + {q₀.2}<VAR>hK' : IsCompact K'<VAR>U : Set G<VAR>U_open : IsOpen U<VAR>K'U : K' ⊆ U<VAR>hU : IntegrableOn f U μ<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>δε : δ ≤ ε<VAR>hδ : K' + ball 0 δ ⊆ U<VAR>this : Norm (E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) := hasOpNorm<VAR>bound : G → ℝ := U.indicator fun t => ‖precompR (P × G) L‖ * ‖f t‖ * C<VAR>I4 : ∀ᵐ (a : G) ∂μ, ∀ (x : P × G), dist x q₀ < δ → ‖((precompR (P × G) L) (f a)) (g' (x.1, x.2 - a))‖ ≤ bound a<GOAL>HasFDerivAt (fun q => (f ⋆[L, μ] g q.1) q.2) ((f ⋆[precompR (P × G) L, μ] fun x => fderiv 𝕜 (↿g) (q₀.1, x)) q₀.2) q₀
<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✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>inst✝⁹ : NormedSpace 𝕜 E''<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : CompleteSpace F<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup P<VAR>inst✝ : NormedSpace 𝕜 P<VAR>μ : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>g : P → G → E'<VAR>s : Set P<VAR>k : Set G<VAR>hs : IsOpen s<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ univ)<VAR>q₀ : P × G<VAR>hq₀ : q₀.1 ∈ s<VAR>g' : P × G → P × G →L[𝕜] E' := fderiv 𝕜 ↿g<VAR>A : ∀ p ∈ s, Continuous (g p)<VAR>A' : ∀ (q : P × G), q.1 ∈ s → s ×ˢ univ ∈ 𝓝 q<VAR>g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0<VAR>ε C : ℝ<VAR>εpos : 0 < ε<VAR>h₀ε : ball q₀.1 ε ⊆ s<VAR>hε : ∀ (p : P) (x : G), ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C<VAR>I1 : ∀ᶠ (x : P × G) in 𝓝 q₀, AEStronglyMeasurable (fun a => (L (f a)) (g x.1 (x.2 - a))) μ<VAR>I2 : Integrable (fun a => (L (f a)) (g q₀.1 (q₀.2 - a))) μ<VAR>I3 : AEStronglyMeasurable (fun a => (L (f a)).comp (g' (q₀.1, q₀.2 - a))) μ<VAR>K' : Set G := -k + {q₀.2}<VAR>K'_def : K' = -k + {q₀.2}<VAR>hK' : IsCompact K'<VAR>U : Set G<VAR>U_open : IsOpen U<VAR>K'U : K' ⊆ U<VAR>hU : IntegrableOn f U μ<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>δε : δ ≤ ε<VAR>hδ : K' + ball 0 δ ⊆ U<VAR>this : Norm (E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) := hasOpNorm<VAR>bound : G → ℝ := U.indicator fun t => ‖precompR (P × G) L‖ * ‖f t‖ * C<VAR>I4 : ∀ᵐ (a : G) ∂μ, ∀ (x : P × G), dist x q₀ < δ → ‖((precompR (P × G) L) (f a)) (g' (x.1, x.2 - a))‖ ≤ bound a<VAR>I5 : Integrable bound μ<GOAL>HasFDerivAt (fun q => (f ⋆[L, μ] g q.1) q.2) ((f ⋆[precompR (P × G) L, μ] fun x => fderiv 𝕜 (↿g) (q₀.1, x)) q₀.2) q₀
<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✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>inst✝⁹ : NormedSpace 𝕜 E''<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : CompleteSpace F<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup P<VAR>inst✝ : NormedSpace 𝕜 P<VAR>μ : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>g : P → G → E'<VAR>s : Set P<VAR>k : Set G<VAR>hs : IsOpen s<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ univ)<VAR>q₀ : P × G<VAR>hq₀ : q₀.1 ∈ s<VAR>g' : P × G → P × G →L[𝕜] E' := fderiv 𝕜 ↿g<VAR>A : ∀ p ∈ s, Continuous (g p)<VAR>A' : ∀ (q : P × G), q.1 ∈ s → s ×ˢ univ ∈ 𝓝 q<VAR>g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0<VAR>ε C : ℝ<VAR>εpos : 0 < ε<VAR>h₀ε : ball q₀.1 ε ⊆ s<VAR>hε : ∀ (p : P) (x : G), ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C<VAR>I1 : ∀ᶠ (x : P × G) in 𝓝 q₀, AEStronglyMeasurable (fun a => (L (f a)) (g x.1 (x.2 - a))) μ<VAR>I2 : Integrable (fun a => (L (f a)) (g q₀.1 (q₀.2 - a))) μ<VAR>I3 : AEStronglyMeasurable (fun a => (L (f a)).comp (g' (q₀.1, q₀.2 - a))) μ<VAR>K' : Set G := -k + {q₀.2}<VAR>K'_def : K' = -k + {q₀.2}<VAR>hK' : IsCompact K'<VAR>U : Set G<VAR>U_open : IsOpen U<VAR>K'U : K' ⊆ U<VAR>hU : IntegrableOn f U μ<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>δε : δ ≤ ε<VAR>hδ : K' + ball 0 δ ⊆ U<VAR>this : Norm (E →L[𝕜] (P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F) := hasOpNorm<VAR>bound : G → ℝ := U.indicator fun t => ‖precompR (P × G) L‖ * ‖f t‖ * C<VAR>I4 : ∀ᵐ (a : G) ∂μ, ∀ (x : P × G), dist x q₀ < δ → ‖((precompR (P × G) L) (f a)) (g' (x.1, x.2 - a))‖ ≤ bound a<VAR>I5 : Integrable bound μ<VAR>I6 : ∀ᵐ (a : G) ∂μ, ∀ (x : P × G), dist x q₀ < δ → HasFDerivAt (fun x => (L (f a)) (g x.1 (x.2 - a))) ((L (f a)).comp (g' (x.1, x.2 - a))) x<GOAL>HasFDerivAt (fun q => (f ⋆[L, μ] g q.1) q.2) ((f ⋆[precompR (P × G) L, μ] fun x => fderiv 𝕜 (↿g) (q₀.1, x)) q₀.2) q₀
<VAR>α : Type u<VAR>γ : Type u_1<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : T2Space γ<VAR>f : α → γ<VAR>this✝ : TopologicalSpace α := ⊥<VAR>this : DiscreteTopology α<GOAL>Ultrafilter.extend f ∘ pure = f
<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>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set α<VAR>t : Set β<VAR>hs : μ s ≠ 0<VAR>u : Set (α × β)<VAR>hum : MeasurableSet u<VAR>hu : s ×ˢ t =ᶠ[ae (μ.prod ν)] u<GOAL>NullMeasurableSet t ν
<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>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set α<VAR>t : Set β<VAR>hs : μ s ≠ 0<VAR>u : Set (α × β)<VAR>hum : MeasurableSet u<VAR>hu : s ×ˢ t =ᶠ[ae (μ.prod ν)] u<VAR>x : α<VAR>hxs : x ∈ s<VAR>hx : Prod.mk x ⁻¹' s ×ˢ t =ᶠ[ae ν] Prod.mk x ⁻¹' u<GOAL>NullMeasurableSet t ν
<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>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set α<VAR>t : Set β<VAR>hs : μ s ≠ 0<VAR>u : Set (α × β)<VAR>hum : MeasurableSet u<VAR>hu : s ×ˢ t =ᶠ[ae (μ.prod ν)] u<VAR>x : α<VAR>hxs : x ∈ s<VAR>hx : Prod.mk x ⁻¹' s ×ˢ t =ᶠ[ae ν] Prod.mk x ⁻¹' u<GOAL>t =ᶠ[ae ν] Prod.mk x ⁻¹' u
<VAR>F : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>inst✝² : CompleteSpace F<VAR>inst✝¹ : MeasurableSpace F<VAR>inst✝ : BorelSpace F<GOAL>Measurable fun x => derivWithin f (Ici x) x
<VAR>F : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>inst✝² : CompleteSpace F<VAR>inst✝¹ : MeasurableSpace F<VAR>inst✝ : BorelSpace F<VAR>s : Set F<VAR>hs : IsClosed s<GOAL>MeasurableSet ((fun x => derivWithin f (Ici x) x) ⁻¹' s)
<VAR>F : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>inst✝² : CompleteSpace F<VAR>inst✝¹ : MeasurableSpace F<VAR>inst✝ : BorelSpace F<VAR>s : Set F<VAR>hs : IsClosed s<VAR>this : (fun x => derivWithin f (Ici x) x) ⁻¹' s = {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ s} ∪ {x | ¬DifferentiableWithinAt ℝ f (Ici x) x} ∩ {_x | 0 ∈ s}<GOAL>MeasurableSet ((fun x => derivWithin f (Ici x) x) ⁻¹' s)
<VAR>F : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>inst✝² : CompleteSpace F<VAR>inst✝¹ : MeasurableSpace F<VAR>inst✝ : BorelSpace F<VAR>s : Set F<VAR>hs : IsClosed s<VAR>this : (fun x => derivWithin f (Ici x) x) ⁻¹' s = {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ s} ∪ {x | ¬DifferentiableWithinAt ℝ f (Ici x) x} ∩ {_x | 0 ∈ s}<GOAL>MeasurableSet ({x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ s} ∪ {x | ¬DifferentiableWithinAt ℝ f (Ici x) x} ∩ {_x | 0 ∈ s})
<VAR>m : Type u → Type u<VAR>inst✝¹ : Monad m<VAR>α β : Type u<VAR>inst✝ : LawfulMonad m<VAR>f : α → β → m β<VAR>x✝ y✝ : FreeMonoid α<GOAL>{ toFun := fun xs => flip (List.foldrM f) (FreeMonoid.toList xs), map_one' := ⋯ }.toFun (x✝ * y✝) = { toFun := fun xs => flip (List.foldrM f) (FreeMonoid.toList xs), map_one' := ⋯ }.toFun x✝ * { toFun := fun xs => flip (List.foldrM f) (FreeMonoid.toList xs), map_one' := ⋯ }.toFun y✝
<VAR>m : Type u → Type u<VAR>inst✝¹ : Monad m<VAR>α β : Type u<VAR>inst✝ : LawfulMonad m<VAR>f : α → β → m β<VAR>x✝¹ y✝ : FreeMonoid α<VAR>x✝ : KleisliCat.mk m β<GOAL>{ toFun := fun xs => flip (List.foldrM f) (FreeMonoid.toList xs), map_one' := ⋯ }.toFun (x✝¹ * y✝) x✝ = ({ toFun := fun xs => flip (List.foldrM f) (FreeMonoid.toList xs), map_one' := ⋯ }.toFun x✝¹ * { toFun := fun xs => flip (List.foldrM f) (FreeMonoid.toList xs), map_one' := ⋯ }.toFun y✝) x✝
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R[X]<VAR>ι : Type u_2<VAR>v : ι → R<VAR>s : Finset ι<VAR>hvs : Set.InjOn v ↑s<VAR>degree_fg_lt : (f - g).degree < ↑s.card<VAR>eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g<GOAL>f = g
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R[X]<VAR>ι : Type u_2<VAR>v : ι → R<VAR>s : Finset ι<VAR>hvs : Set.InjOn v ↑s<VAR>degree_fg_lt : (f - g).degree < ↑s.card<VAR>eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g<GOAL>f - g = 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R[X]<VAR>ι : Type u_2<VAR>v : ι → R<VAR>s : Finset ι<VAR>hvs : Set.InjOn v ↑s<VAR>degree_fg_lt : (f - g).degree < ↑s.card<VAR>eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g<GOAL>∀ i ∈ s, eval (v i) (f - g) = 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R[X]<VAR>ι : Type u_2<VAR>v : ι → R<VAR>s : Finset ι<VAR>hvs : Set.InjOn v ↑s<VAR>degree_fg_lt : (f - g).degree < ↑s.card<VAR>eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g<GOAL>∀ i ∈ s, eval (v i) f = eval (v i) g
<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>g : Submodule R (E × F)<VAR>hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0<VAR>x : ↥(map (LinearMap.fst R E F) g)<GOAL>(↑x, ↑g.toLinearPMap x) ∈ g
<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>g : Submodule R (E × F)<VAR>hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0<VAR>x : ↥(map (LinearMap.fst R E F) g)<GOAL>(↑x, valFromGraph hg ⋯) ∈ g
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>X Y : R<GOAL>W'.Equation ![X, Y, 1] ↔ W'.toAffine.Equation X Y
<VAR>k : ℤ<GOAL>(2 * k + 1).negOnePow = -1
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hfg : f ≤ᶠ[ae μ] g<GOAL>μ.withDensity f ≤ μ.withDensity g
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hfg : f ≤ᶠ[ae μ] g<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(μ.withDensity f) s ≤ (μ.withDensity g) s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hfg : f ≤ᶠ[ae μ] g<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hfg : f ≤ᶠ[ae μ] g<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>e : α ≃o β<VAR>a b : α<GOAL>⇑e '' Ioc a b = Ioc (e a) (e b)
<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>m : ℕ<VAR>inst✝ : CharP R m<VAR>n✝ : ℕ<VAR>h : m ∣ n✝ + 1<VAR>a b : ZMod (n✝ + 1)<GOAL>↑a.val * ↑b.val = ↑(val (a * b))
<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>m : ℕ<VAR>inst✝ : CharP R m<VAR>n✝ : ℕ<VAR>h : m ∣ n✝ + 1<VAR>a b : ZMod (n✝ + 1)<GOAL>m ∣ a.val * b.val - a.val * b.val % n✝.succ
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>p : Sort u_4<VAR>f : M → ↥S → M → ↥S → p<VAR>H : ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S}, (r S) (a, b) (a', b') → (r S) (c, d) (c', d') → f a b c d = f a' b' c' d'<VAR>a c : M<VAR>b d : ↥S<GOAL>((monoidOf S).mk' a b).liftOn₂ ((monoidOf S).mk' c d) f H = f a b c d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝¹ : DivisionMonoid K<VAR>inst✝ : HasDistribNeg K<VAR>a✝ b a : K<GOAL>a / -b = -(a / b)
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>φ ψ : A →ₐ[R] B<VAR>s : Set A<GOAL>Set.EqOn ⇑φ ⇑ψ ↑(adjoin R s) ↔ Set.EqOn (⇑φ) (⇑ψ) s
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>φ ψ : A →ₐ[R] B<VAR>s : Set A<VAR>this : ∀ (S : Set A), S ≤ ↑(equalizer φ ψ) ↔ Set.EqOn (⇑φ) (⇑ψ) S<GOAL>Set.EqOn ⇑φ ⇑ψ ↑(adjoin R s) ↔ Set.EqOn (⇑φ) (⇑ψ) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c c₁ c₂ c₃ s t : Set α<VAR>a b x y : α<VAR>hs : IsChain r s<VAR>h : ¬∃ t, IsChain r s ∧ SuperChain r s t<GOAL>IsChain r (SuccChain r s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c c₁ c₂ c₃ s t : Set α<VAR>a b x y : α<VAR>hs : IsChain r s<VAR>h : ¬(IsChain r s ∧ ∃ x, SuperChain r s x)<GOAL>IsChain r (SuccChain r s)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 2<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.Exact<VAR>hR₂ : R₂.Exact<VAR>hR₁' : Epi (R₁.map' 1 2 ⋯ ⋯)<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₁ : Mono (app' φ 1 ⋯)<GOAL>R₁.map' 0 2 ⋯ ⋯ = 0
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E → F<VAR>h'f : Function.HasTemperateGrowth (fderiv ℝ f)<VAR>hf : Differentiable ℝ f<VAR>k : ℕ<VAR>C : ℝ<VAR>h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k<GOAL>Function.HasTemperateGrowth f
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E → F<VAR>h'f : Function.HasTemperateGrowth (fderiv ℝ f)<VAR>hf : Differentiable ℝ f<VAR>k : ℕ<VAR>C : ℝ<VAR>h : ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ k<VAR>n : ℕ<GOAL>∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n f x‖ ≤ C * (1 + ‖x‖) ^ k
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<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>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<GOAL>(-p).radius = p.radius
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s t : Set α<VAR>a b : α<VAR>h : IsLUB s a<GOAL>a ≤ b ↔ b ∈ upperBounds s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s t : Set α<VAR>a b : α<VAR>h : IsLUB s a<GOAL>a ≤ b ↔ b ∈ Ici a
<VAR>a b c d m n✝ k : ℕ<VAR>p q P Q : ℕ → Prop<VAR>inst✝ : DecidablePred P<VAR>n : ℕ<GOAL>0 < findGreatest P k ↔ ∃ n, 0 < n ∧ n ≤ k ∧ P n
<VAR>a b c d m n✝ k : ℕ<VAR>p q P Q : ℕ → Prop<VAR>inst✝ : DecidablePred P<VAR>n : ℕ<GOAL>(¬∀ ⦃n : ℕ⦄, 0 < n → n ≤ k → ¬P n) ↔ ∃ n, 0 < n ∧ n ≤ k ∧ P n
<VAR>a b c d m n✝ k : ℕ<VAR>p q P Q : ℕ → Prop<VAR>inst✝ : DecidablePred P<VAR>n : ℕ<GOAL>(Exists fun ⦃n⦄ => 0 < n ∧ n ≤ k ∧ P n) ↔ ∃ n, 0 < n ∧ n ≤ k ∧ P n
<VAR>M : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero M<VAR>p : Associates M<VAR>h₁ : p ≠ 0<VAR>hp : IsAtom p<GOAL>¬IsUnit p
<VAR>M : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero M<VAR>p : Associates M<VAR>h₁ : p ≠ 0<VAR>hp : IsAtom p<VAR>a b : Associates M<VAR>h : p = p * b<VAR>ha : a = p<GOAL>IsUnit b
<VAR>M : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero M<VAR>p : Associates M<VAR>h₁ : p ≠ 0<VAR>hp : Irreducible p<GOAL>p ≠ ⊥
<VAR>M : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero M<VAR>p : Associates M<VAR>h₁ : p ≠ 0<VAR>hp : Irreducible p<VAR>b : Associates M<VAR>x✝ : b < p<VAR>a : Associates M<VAR>hab : p = b * a<VAR>hb✝ : ¬p ∣ b<VAR>hb : IsUnit b<GOAL>b = ⊥
<VAR>M : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero M<VAR>p : Associates M<VAR>h₁ : p ≠ 0<VAR>hp : Irreducible p<VAR>b : Associates M<VAR>x✝ : b < p<VAR>a : Associates M<VAR>hab : p = b * a<VAR>hb : ¬p ∣ b<VAR>ha : IsUnit a<GOAL>b = p * ↑ha.unit⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<GOAL>Ioi b ⊆ Ioi a ↔ a ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h : Ioi b ⊆ Ioi a<GOAL>a ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h : Ioi b ⊆ Ioi a<VAR>ba : ¬a ≤ b<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>U : Set (PrimeSpectrum R)<GOAL>IsOpen U ↔ ∃ s, Uᶜ = zeroLocus s
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>U : Set (PrimeSpectrum R)<GOAL>IsOpen U ↔ ∃ s, zeroLocus s = Uᶜ
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : Ring R<VAR>inst✝² : Monoid M<VAR>inst✝¹ : LinearOrder M<VAR>inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>f : R →* M<VAR>x : R<GOAL>f (-x) = f x
<VAR>x y : ℝ<VAR>hx✝ : 0 ≤ x<VAR>hx : 0 < x<GOAL>log x ≤ 0 ↔ x ≤ 1
<VAR>x n : ℂ<GOAL>x⁻¹ ^ n = if x.arg = π then (starRingEnd ℂ) (x ^ (starRingEnd ℂ) n)⁻¹ else (x ^ n)⁻¹