ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : StrictOrderedCommRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>hx : x ∈ s<GOAL>SameRay R (x -ᵥ x) (x -ᵥ y)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : StrictOrderedCommRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>hx : x ∈ s<GOAL>SameRay R 0 (x -ᵥ y)
<VAR>z τ : ℂ<GOAL>jacobiTheta₂' z τ = 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) / τ * (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))
<VAR>z τ : ℂ<VAR>hτ : τ.im ≤ 0<GOAL>jacobiTheta₂' z τ = 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) / τ * (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<GOAL>jacobiTheta₂' z τ = 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) / τ * (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>hτ' : 0 < (-1 / τ).im<GOAL>jacobiTheta₂' z τ = 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) / τ * (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>hτ' : 0 < (-1 / τ).im<VAR>hj : HasDerivAt (fun w => jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z<GOAL>jacobiTheta₂' z τ = 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) / τ * (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<GOAL>mellin (fun t => f t⁻¹) s = mellin f (-s)
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝⁴ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝³ : NormedRing 𝕜<VAR>inst✝² : (i : α) → Module 𝕜 (E i)<VAR>inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝ : DecidableEq α<VAR>hp : 0 < p.toReal<VAR>f : ↥(lp E p)<VAR>s : Finset α<GOAL>‖f‖ ^ p.toReal - ‖f - ∑ i ∈ s, lp.single p i (↑f i)‖ ^ p.toReal = ∑ i ∈ s, ‖↑f i‖ ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝⁴ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝³ : NormedRing 𝕜<VAR>inst✝² : (i : α) → Module 𝕜 (E i)<VAR>inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝ : DecidableEq α<VAR>hp : 0 < p.toReal<VAR>f : ↥(lp E p)<VAR>s : Finset α<GOAL>HasSum (fun b => ‖↑f b‖ ^ p.toReal - ‖↑(f - ∑ i ∈ s, lp.single p i (↑f i)) b‖ ^ p.toReal) (∑ i ∈ s, ‖↑f i‖ ^ p.toReal)
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝⁴ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝³ : NormedRing 𝕜<VAR>inst✝² : (i : α) → Module 𝕜 (E i)<VAR>inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝ : DecidableEq α<VAR>hp : 0 < p.toReal<VAR>f : ↥(lp E p)<VAR>s : Finset α<VAR>F : α → ℝ := fun i => ‖↑f i‖ ^ p.toReal - ‖↑(f - ∑ i ∈ s, lp.single p i (↑f i)) i‖ ^ p.toReal<GOAL>HasSum (fun b => ‖↑f b‖ ^ p.toReal - ‖↑(f - ∑ i ∈ s, lp.single p i (↑f i)) b‖ ^ p.toReal) (∑ i ∈ s, ‖↑f i‖ ^ p.toReal)
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝⁴ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝³ : NormedRing 𝕜<VAR>inst✝² : (i : α) → Module 𝕜 (E i)<VAR>inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝ : DecidableEq α<VAR>hp : 0 < p.toReal<VAR>f : ↥(lp E p)<VAR>s : Finset α<VAR>F : α → ℝ := fun i => ‖↑f i‖ ^ p.toReal - ‖↑(f - ∑ i ∈ s, lp.single p i (↑f i)) i‖ ^ p.toReal<VAR>hF : ∀ i ∉ s, F i = 0<GOAL>HasSum (fun b => ‖↑f b‖ ^ p.toReal - ‖↑(f - ∑ i ∈ s, lp.single p i (↑f i)) b‖ ^ p.toReal) (∑ i ∈ s, ‖↑f i‖ ^ p.toReal)
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝⁴ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝³ : NormedRing 𝕜<VAR>inst✝² : (i : α) → Module 𝕜 (E i)<VAR>inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝ : DecidableEq α<VAR>hp : 0 < p.toReal<VAR>f : ↥(lp E p)<VAR>s : Finset α<VAR>F : α → ℝ := fun i => ‖↑f i‖ ^ p.toReal - ‖↑(f - ∑ i ∈ s, lp.single p i (↑f i)) i‖ ^ p.toReal<VAR>hF : ∀ i ∉ s, F i = 0<VAR>hF' : ∀ i ∈ s, F i = ‖↑f i‖ ^ p.toReal<GOAL>HasSum (fun b => ‖↑f b‖ ^ p.toReal - ‖↑(f - ∑ i ∈ s, lp.single p i (↑f i)) b‖ ^ p.toReal) (∑ i ∈ s, ‖↑f i‖ ^ p.toReal)
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝⁴ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝³ : NormedRing 𝕜<VAR>inst✝² : (i : α) → Module 𝕜 (E i)<VAR>inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝ : DecidableEq α<VAR>hp : 0 < p.toReal<VAR>f : ↥(lp E p)<VAR>s : Finset α<VAR>F : α → ℝ := fun i => ‖↑f i‖ ^ p.toReal - ‖↑(f - ∑ i ∈ s, lp.single p i (↑f i)) i‖ ^ p.toReal<VAR>hF : ∀ i ∉ s, F i = 0<VAR>hF' : ∀ i ∈ s, F i = ‖↑f i‖ ^ p.toReal<VAR>this : HasSum F (∑ i ∈ s, F i)<GOAL>HasSum (fun b => ‖↑f b‖ ^ p.toReal - ‖↑(f - ∑ i ∈ s, lp.single p i (↑f i)) b‖ ^ p.toReal) (∑ i ∈ s, ‖↑f i‖ ^ p.toReal)
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>inst✝ : L.Structure M<VAR>α : Type w'<VAR>ie : IsEmpty α<GOAL>((LHom.id L).sumElim (LHom.ofIsEmpty (constantsOn α) L)).comp (L.lhomWithConstants α) = LHom.id L
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>inst✝ : L.Structure M<VAR>α : Type w'<VAR>ie : IsEmpty α<GOAL>(L.lhomWithConstants α).comp ((LHom.id L).sumElim (LHom.ofIsEmpty (constantsOn α) L)) = LHom.id (L[[α]])
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>inst✝ : L.Structure M<VAR>α : Type w'<VAR>ie : IsEmpty α<GOAL>LHom.sumInl.sumElim (LHom.sumInl.comp (LHom.ofIsEmpty (constantsOn α) L)) = LHom.id (L[[α]])
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>m : ↥M<VAR>r : R<GOAL>↑m • mk' S r m = (algebraMap R S) r
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx0 : 0 < x<VAR>hx1 : x < 1<VAR>hyz : z < y<GOAL>x ^ y < x ^ z
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx0 : 0 < x<VAR>hx1 : x < 1<VAR>hyz : z < y<GOAL>rexp (log x * y) < rexp (log x * z)
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx0 : 0 < x<VAR>hx1 : x < 1<VAR>hyz : z < y<GOAL>log x * y < log x * z
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>h : ContfracLegendre.Ass ξ u v<GOAL>ContfracLegendre.Ass (fract ξ)⁻¹ v (u - ⌊ξ⌋ * v)
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>h : ContfracLegendre.Ass ξ u v<GOAL>IsCoprime v (u - ⌊ξ⌋ * v)
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>h : ContfracLegendre.Ass ξ u v<VAR>huv : u - ⌊ξ⌋ * v = 1<GOAL>-(1 / 2) < (fract ξ)⁻¹ - ↑v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>inst✝² : NormedSpace ℝ E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f g : G → E<VAR>f' g' : G →L[ℝ] E<VAR>s : Set G<VAR>x✝ : G<VAR>n : ℕ∞<VAR>x : F<GOAL>HasStrictFDerivAt (fun x => ‖x‖ ^ 2) (2 • (innerSL ℝ) x) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>inst✝² : NormedSpace ℝ E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f g : G → E<VAR>f' g' : G →L[ℝ] E<VAR>s : Set G<VAR>x✝ : G<VAR>n : ℕ∞<VAR>x : F<GOAL>HasStrictFDerivAt (fun x => re ⟪x, x⟫_ℝ) (2 • (innerSL ℝ) x) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>inst✝² : NormedSpace ℝ E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f g : G → E<VAR>f' g' : G →L[ℝ] E<VAR>s : Set G<VAR>x✝ : G<VAR>n : ℕ∞<VAR>x : F<VAR>e_7✝ : normedAddCommGroup = NonUnitalNormedRing.toNormedAddCommGroup<VAR>he✝ : InnerProductSpace.toNormedSpace = NormedAlgebra.toNormedSpace'<GOAL>2 • (innerSL ℝ) x = (fderivInnerCLM ℝ (id x, id x)).comp ((ContinuousLinearMap.id ℝ F).prod (ContinuousLinearMap.id ℝ F))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>inst✝² : NormedSpace ℝ E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f g : G → E<VAR>f' g' : G →L[ℝ] E<VAR>s : Set G<VAR>x✝ : G<VAR>n : ℕ∞<VAR>x : F<VAR>e_7✝ : normedAddCommGroup = NonUnitalNormedRing.toNormedAddCommGroup<VAR>he✝ : InnerProductSpace.toNormedSpace = NormedAlgebra.toNormedSpace'<VAR>y : F<GOAL>(2 • (innerSL ℝ) x) y = ((fderivInnerCLM ℝ (id x, id x)).comp ((ContinuousLinearMap.id ℝ F).prod (ContinuousLinearMap.id ℝ F))) y
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>β : Type u<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : HasBesicovitchCovering α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>x : α<VAR>s : Set (Set α)<VAR>hs : s ∈ (Besicovitch.vitaliFamily μ).filterAt x<GOAL>s ∈ map (fun r => closedBall x r) (𝓝[>] 0)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>β : Type u<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : HasBesicovitchCovering α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>x : α<VAR>s : Set (Set α)<VAR>hs : s ∈ (Besicovitch.vitaliFamily μ).filterAt x<GOAL>(fun r => closedBall x r) ⁻¹' s ∈ 𝓝[>] 0
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>β : Type u<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : HasBesicovitchCovering α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>x : α<VAR>s : Set (Set α)<VAR>hs : s ∈ (Besicovitch.vitaliFamily μ).filterAt x<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>hε : ∀ a ∈ (Besicovitch.vitaliFamily μ).setsAt x, a ⊆ closedBall x ε → a ∈ s<GOAL>(fun r => closedBall x r) ⁻¹' s ∈ 𝓝[>] 0
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>β : Type u<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : HasBesicovitchCovering α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>x : α<VAR>s : Set (Set α)<VAR>hs : s ∈ (Besicovitch.vitaliFamily μ).filterAt x<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>hε : ∀ a ∈ (Besicovitch.vitaliFamily μ).setsAt x, a ⊆ closedBall x ε → a ∈ s<VAR>this : Ioc 0 ε ∈ 𝓝[>] 0<GOAL>(fun r => closedBall x r) ⁻¹' s ∈ 𝓝[>] 0
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>β : Type u<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : HasBesicovitchCovering α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>x : α<VAR>s : Set (Set α)<VAR>hs : s ∈ (Besicovitch.vitaliFamily μ).filterAt x<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>hε : ∀ a ∈ (Besicovitch.vitaliFamily μ).setsAt x, a ⊆ closedBall x ε → a ∈ s<VAR>this : Ioc 0 ε ∈ 𝓝[>] 0<VAR>a✝ : ℝ<VAR>hr : a✝ ∈ Ioc 0 ε<GOAL>a✝ ∈ (fun r => closedBall x r) ⁻¹' s
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>T : Subring R<VAR>p : (↥T)[X]<GOAL>↑(ofSubring T p).coeffs ⊆ ↑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✝¹² : 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>f : G → E<VAR>n : ℕ∞<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 𝕜 n (↿g) (s ×ˢ univ)<VAR>eG : Type (max uG uE' uF uP) := ULift.{max uE' uF uP, uG} G<VAR>this✝¹ : MeasurableSpace eG := borel eG<VAR>this✝ : BorelSpace eG<VAR>eE' : Type (max uE' uG uF uP) := ULift.{max uG uF uP, uE'} E'<VAR>eF : Type (max uF uG uE' uP) := ULift.{max uG uE' uP, uF} F<VAR>eP : Type (max uP uG uE' uF) := ULift.{max uG uE' uF, uP} P<VAR>isoG : eG ≃L[𝕜] G<VAR>isoE' : eE' ≃L[𝕜] E'<VAR>isoF : eF ≃L[𝕜] F<VAR>isoP : eP ≃L[𝕜] P<VAR>ef : eG → E := f ∘ ⇑isoG<VAR>eμ : Measure eG := Measure.map (⇑isoG.symm) μ<VAR>eg : eP → eG → eE' := fun ep ex => isoE'.symm (g (isoP ep) (isoG ex))<VAR>eL : E →L[𝕜] eE' →L[𝕜] eF := (↑(isoE'.arrowCongr isoF).symm).comp L<VAR>R : eP × eG → eF := fun q => (ef ⋆[eL, eμ] eg q.1) q.2<VAR>R_contdiff : ContDiffOn 𝕜 n R ((⇑isoP ⁻¹' s) ×ˢ univ)<GOAL>ContDiffOn 𝕜 n (fun q => (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ)
<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>f : G → E<VAR>n : ℕ∞<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 𝕜 n (↿g) (s ×ˢ univ)<VAR>eG : Type (max uG uE' uF uP) := ULift.{max uE' uF uP, uG} G<VAR>this✝¹ : MeasurableSpace eG := borel eG<VAR>this✝ : BorelSpace eG<VAR>eE' : Type (max uE' uG uF uP) := ULift.{max uG uF uP, uE'} E'<VAR>eF : Type (max uF uG uE' uP) := ULift.{max uG uE' uP, uF} F<VAR>eP : Type (max uP uG uE' uF) := ULift.{max uG uE' uF, uP} P<VAR>isoG : eG ≃L[𝕜] G<VAR>isoE' : eE' ≃L[𝕜] E'<VAR>isoF : eF ≃L[𝕜] F<VAR>isoP : eP ≃L[𝕜] P<VAR>ef : eG → E := f ∘ ⇑isoG<VAR>eμ : Measure eG := Measure.map (⇑isoG.symm) μ<VAR>eg : eP → eG → eE' := fun ep ex => isoE'.symm (g (isoP ep) (isoG ex))<VAR>eL : E →L[𝕜] eE' →L[𝕜] eF := (↑(isoE'.arrowCongr isoF).symm).comp L<VAR>R : eP × eG → eF := fun q => (ef ⋆[eL, eμ] eg q.1) q.2<VAR>R_contdiff : ContDiffOn 𝕜 n R ((⇑isoP ⁻¹' s) ×ˢ univ)<VAR>A : ContDiffOn 𝕜 n (⇑isoF ∘ R ∘ ⇑(isoP.prod isoG).symm) (s ×ˢ univ)<GOAL>ContDiffOn 𝕜 n (fun q => (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>m : M<GOAL>(GradedAlgebra.ι R M) m * (GradedAlgebra.ι R M) m = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>m : M<GOAL>(DirectSum.of (fun i => ↥(⋀[R]^i M)) (1 + 1)) (GradedMonoid.GMul.mul ⟨(ι R) m, ⋯⟩ ⟨(ι R) m, ⋯⟩) = 0
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : LieRingModule L N<VAR>inst✝ : LieModule R L N<VAR>t : R<VAR>x y z : L<VAR>m n : M<GOAL>⁅x - y, m⁆ = ⁅x, m⁆ - ⁅y, m⁆
<VAR>M₀ : Type u_1<VAR>inst✝ : MonoidWithZero M₀<VAR>r : M₀<GOAL>r ∉ nonZeroDivisorsLeft M₀ ↔ {s | s * r = 0 ∧ s ≠ 0}.Nonempty
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : ConcreteCategory C<VAR>J : Type w<VAR>inst✝¹ : Category.{r, w} J<VAR>F : J ⥤ C<VAR>inst✝ : PreservesColimit F (forget C)<VAR>D : Cocone F<VAR>hD : IsColimit D<VAR>x : (forget C).obj D.pt<GOAL>∃ j y, (D.ι.app j) y = x
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : ConcreteCategory C<VAR>J : Type w<VAR>inst✝¹ : Category.{r, w} J<VAR>F : J ⥤ C<VAR>inst✝ : PreservesColimit F (forget C)<VAR>D : Cocone F<VAR>hD : IsColimit D<VAR>a : (j : J) × (forget C).obj (F.obj j)<GOAL>∃ j y, (D.ι.app j) y = (fun a => (D.ι.app a.fst) a.snd) a
<VAR>D : GlueData<VAR>i j : D.J<VAR>U : Set ↑(D.U i)<GOAL>⇑(D.ι j) ⁻¹' (⇑(D.ι i) '' U) = ⇑(D.f j i) '' (⇑(D.t j i ≫ D.f i j) ⁻¹' U)
<VAR>D : GlueData<VAR>i j : D.J<VAR>U : Set ↑(D.U i)<VAR>this : ⇑(D.f j i) ⁻¹' (⇑(D.ι j) ⁻¹' (⇑(D.ι i) '' U)) = ⇑(D.t j i ≫ D.f i j) ⁻¹' U<GOAL>⇑(D.ι j) ⁻¹' (⇑(D.ι i) '' U) = ⇑(D.f j i) '' (⇑(D.t j i ≫ D.f i j) ⁻¹' U)
<VAR>D : GlueData<VAR>i j : D.J<VAR>U : Set ↑(D.U i)<VAR>this : ⇑(D.f j i) ⁻¹' (⇑(D.ι j) ⁻¹' (⇑(D.ι i) '' U)) = ⇑(D.t j i ≫ D.f i j) ⁻¹' U<GOAL>⇑(D.ι j) ⁻¹' (⇑(D.ι i) '' U) = ⇑(D.ι j) ⁻¹' (⇑(D.ι i) '' U) ∩ Set.range ⇑(D.f j i)
<VAR>D : GlueData<VAR>i j : D.J<VAR>U : Set ↑(D.U i)<VAR>this : ⇑(D.f j i) ⁻¹' (⇑(D.ι j) ⁻¹' (⇑(D.ι i) '' U)) = ⇑(D.t j i ≫ D.f i j) ⁻¹' U<GOAL>⇑(D.ι j) ⁻¹' (⇑(D.ι i) '' U) ∩ Set.range ⇑(D.f j i) = ⇑(D.ι j) ⁻¹' (⇑(D.ι i) '' U)
<VAR>D : GlueData<VAR>i j : D.J<VAR>U : Set ↑(D.U i)<VAR>this : ⇑(D.f j i) ⁻¹' (⇑(D.ι j) ⁻¹' (⇑(D.ι i) '' U)) = ⇑(D.t j i ≫ D.f i j) ⁻¹' U<GOAL>⇑(D.ι j) ⁻¹' (⇑(D.ι i) '' U) ⊆ Set.range ⇑(D.f j i)
<VAR>D : GlueData<VAR>i j : D.J<VAR>U : Set ↑(D.U i)<VAR>this : ⇑(D.f j i) ⁻¹' (⇑(D.ι j) ⁻¹' (⇑(D.ι i) '' U)) = ⇑(D.t j i ≫ D.f i j) ⁻¹' U<GOAL>⇑(D.ι j) ⁻¹' (⇑(D.ι i) '' U) ⊆ ⇑(D.ι j) ⁻¹' Set.range ⇑(D.ι i)
<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>f : E → F<VAR>K✝ K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<GOAL>D f K ⊆ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
<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>f : E → F<VAR>K✝ K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<VAR>P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n<GOAL>D f K ⊆ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
<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>f : E → F<VAR>K✝ K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<VAR>P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<GOAL>D f K ⊆ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
<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>f : E → F<VAR>K✝ K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<VAR>P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>x : E<VAR>hx : x ∈ D f K<GOAL>x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
<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>f : E → F<VAR>K✝ K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<VAR>P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>x : E<VAR>hx : x ∈ D f K<VAR>this : ∀ (e : ℕ), ∃ n, ∀ (p q : ℕ), n ≤ p → n ≤ q → ∃ L ∈ K, x ∈ A f L ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f L ((1 / 2) ^ q) ((1 / 2) ^ e)<GOAL>x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
<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>f : E → F<VAR>K✝ K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<VAR>P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>x : E<VAR>hx : x ∈ D f K<VAR>n : ℕ → ℕ<VAR>L : ℕ → ℕ → ℕ → E →L[𝕜] F<VAR>hn : ∀ (e p q : ℕ), n e ≤ p → n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)<GOAL>x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
<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>f : E → F<VAR>K✝ K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<VAR>P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>x : E<VAR>hx : x ∈ D f K<VAR>n : ℕ → ℕ<VAR>L : ℕ → ℕ → ℕ → E →L[𝕜] F<VAR>hn : ∀ (e p q : ℕ), n e ≤ p → n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)<VAR>M : ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e<GOAL>x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
<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>f : E → F<VAR>K✝ K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<VAR>P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>x : E<VAR>hx : x ∈ D f K<VAR>n : ℕ → ℕ<VAR>L : ℕ → ℕ → ℕ → E →L[𝕜] F<VAR>hn : ∀ (e p q : ℕ), n e ≤ p → n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)<VAR>M : ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e<VAR>L0 : ℕ → E →L[𝕜] F := fun e => L e (n e) (n e)<GOAL>x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
<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>f : E → F<VAR>K✝ K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<VAR>P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>x : E<VAR>hx : x ∈ D f K<VAR>n : ℕ → ℕ<VAR>L : ℕ → ℕ → ℕ → E →L[𝕜] F<VAR>hn : ∀ (e p q : ℕ), n e ≤ p → n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)<VAR>M : ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e<VAR>L0 : ℕ → E →L[𝕜] F := fun e => L e (n e) (n e)<VAR>this : CauchySeq L0<GOAL>x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
<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>f : E → F<VAR>K✝ K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<VAR>P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>x : E<VAR>hx : x ∈ D f K<VAR>n : ℕ → ℕ<VAR>L : ℕ → ℕ → ℕ → E →L[𝕜] F<VAR>hn : ∀ (e p q : ℕ), n e ≤ p → n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)<VAR>M : ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e<VAR>L0 : ℕ → E →L[𝕜] F := fun e => L e (n e) (n e)<VAR>this : CauchySeq L0<VAR>f' : E →L[𝕜] F<VAR>f'K : f' ∈ K<VAR>hf' : Tendsto L0 atTop (𝓝 f')<GOAL>x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}