ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>a b m n✝ p✝ n p k : ℕ<VAR>hn : n ≠ 0<VAR>h : n.factorization = single p k<GOAL>p ^ 0 = 1
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : range f' = ⊤<VAR>hker : (LinearMap.ker f').ClosedComplemented<GOAL>(f a, 0) ∈ (implicitToPartialHomeomorphOfComplemented f f' hf hf' hker).target
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<GOAL>Continuous fun p => edist p.1 p.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<GOAL>∀ (x y : α × α), edist x.1 x.2 ≤ edist y.1 y.2 + 2 * edist x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y x' y' : α<GOAL>edist (x, y).1 (x, y).2 ≤ edist (x', y').1 (x', y').2 + 2 * edist (x, y) (x', y')
<VAR>R : Type u_1<VAR>inst✝³ : AddMonoidWithOne R<VAR>inst✝² : CharZero R<VAR>k : Type u_2<VAR>inst✝¹ : DivisionSemiring k<VAR>inst✝ : CharZero k<VAR>m n : ℕ<VAR>n_dvd : n ∣ m<GOAL>↑(m / n) = ↑m / ↑n
<VAR>R : Type u_1<VAR>inst✝³ : AddMonoidWithOne R<VAR>inst✝² : CharZero R<VAR>k : Type u_2<VAR>inst✝¹ : DivisionSemiring k<VAR>inst✝ : CharZero k<VAR>m : ℕ<VAR>n_dvd : 0 ∣ m<GOAL>↑(m / 0) = ↑m / ↑0
<VAR>R : Type u_1<VAR>inst✝³ : AddMonoidWithOne R<VAR>inst✝² : CharZero R<VAR>k : Type u_2<VAR>inst✝¹ : DivisionSemiring k<VAR>inst✝ : CharZero k<VAR>m n : ℕ<VAR>n_dvd : n ∣ m<VAR>hn : n ≠ 0<GOAL>↑(m / n) = ↑m / ↑n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<VAR>x y z w : α<GOAL>{x, y} = {z, w} ↔ x = z ∧ y = w ∨ x = w ∧ y = z
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<VAR>x y z w : α<GOAL>((x = z ∨ x = w) ∧ (y = z ∨ y = w)) ∧ (z = x ∨ z = y) ∧ (w = x ∨ w = y) ↔ x = z ∧ y = w ∨ x = w ∧ y = z
<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>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>U : Set E<VAR>hf : AnalyticOn 𝕜 f U<VAR>hU : IsPreconnected U<VAR>z₀ : E<VAR>h₀ : z₀ ∈ U<VAR>hfz₀ : f =ᶠ[𝓝 z₀] 0<VAR>u : Set E := {x | f =ᶠ[𝓝 x] 0}<GOAL>EqOn f 0 U
<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>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>U : Set E<VAR>hf : AnalyticOn 𝕜 f U<VAR>hU : IsPreconnected U<VAR>z₀ : E<VAR>h₀ : z₀ ∈ U<VAR>hfz₀ : f =ᶠ[𝓝 z₀] 0<VAR>u : Set E := {x | f =ᶠ[𝓝 x] 0}<GOAL>closure u ∩ U ⊆ u
<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>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>U : Set E<VAR>hf : AnalyticOn 𝕜 f U<VAR>hU : IsPreconnected U<VAR>z₀ : E<VAR>h₀ : z₀ ∈ U<VAR>hfz₀ : f =ᶠ[𝓝 z₀] 0<VAR>u : Set E := {x | f =ᶠ[𝓝 x] 0}<VAR>x : E<VAR>xu : x ∈ closure u<VAR>xU : x ∈ U<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>hp : HasFPowerSeriesOnBall f p x r<GOAL>x ∈ u
<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>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>U : Set E<VAR>hf : AnalyticOn 𝕜 f U<VAR>hU : IsPreconnected U<VAR>z₀ : E<VAR>h₀ : z₀ ∈ U<VAR>hfz₀ : f =ᶠ[𝓝 z₀] 0<VAR>u : Set E := {x | f =ᶠ[𝓝 x] 0}<VAR>x : E<VAR>xu : x ∈ closure u<VAR>xU : x ∈ U<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>hp : HasFPowerSeriesOnBall f p x r<VAR>y : E<VAR>yu : y ∈ u<VAR>hxy : edist x y < r / 2<GOAL>x ∈ u
<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>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>U : Set E<VAR>hf : AnalyticOn 𝕜 f U<VAR>hU : IsPreconnected U<VAR>z₀ : E<VAR>h₀ : z₀ ∈ U<VAR>hfz₀ : f =ᶠ[𝓝 z₀] 0<VAR>u : Set E := {x | f =ᶠ[𝓝 x] 0}<VAR>x : E<VAR>xu : x ∈ closure u<VAR>xU : x ∈ U<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>hp : HasFPowerSeriesOnBall f p x r<VAR>y : E<VAR>yu : y ∈ u<VAR>hxy : edist x y < r / 2<VAR>q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)<GOAL>x ∈ u
<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>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>U : Set E<VAR>hf : AnalyticOn 𝕜 f U<VAR>hU : IsPreconnected U<VAR>z₀ : E<VAR>h₀ : z₀ ∈ U<VAR>hfz₀ : f =ᶠ[𝓝 z₀] 0<VAR>u : Set E := {x | f =ᶠ[𝓝 x] 0}<VAR>x : E<VAR>xu : x ∈ closure u<VAR>xU : x ∈ U<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>hp : HasFPowerSeriesOnBall f p x r<VAR>y : E<VAR>yu : y ∈ u<VAR>hxy : edist x y < r / 2<VAR>q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)<VAR>has_series : HasFPowerSeriesOnBall f q y (r / 2)<GOAL>x ∈ u
<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>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>U : Set E<VAR>hf : AnalyticOn 𝕜 f U<VAR>hU : IsPreconnected U<VAR>z₀ : E<VAR>h₀ : z₀ ∈ U<VAR>hfz₀ : f =ᶠ[𝓝 z₀] 0<VAR>u : Set E := {x | f =ᶠ[𝓝 x] 0}<VAR>x : E<VAR>xu : x ∈ closure u<VAR>xU : x ∈ U<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>hp : HasFPowerSeriesOnBall f p x r<VAR>y : E<VAR>yu : y ∈ u<VAR>hxy : edist x y < r / 2<VAR>q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)<VAR>has_series : HasFPowerSeriesOnBall f q y (r / 2)<VAR>M : EMetric.ball y (r / 2) ∈ 𝓝 x<GOAL>x ∈ u
<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>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>U : Set E<VAR>hf : AnalyticOn 𝕜 f U<VAR>hU : IsPreconnected U<VAR>z₀ : E<VAR>h₀ : z₀ ∈ U<VAR>hfz₀ : f =ᶠ[𝓝 z₀] 0<VAR>u : Set E := {x | f =ᶠ[𝓝 x] 0}<VAR>x : E<VAR>xu : x ∈ closure u<VAR>xU : x ∈ U<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>hp : HasFPowerSeriesOnBall f p x r<VAR>y : E<VAR>yu : y ∈ u<VAR>hxy : edist x y < r / 2<VAR>q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)<VAR>has_series : HasFPowerSeriesOnBall f q y (r / 2)<VAR>M : EMetric.ball y (r / 2) ∈ 𝓝 x<VAR>z : E<VAR>hz : z ∈ EMetric.ball y (r / 2)<GOAL>f z = 0 z
<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>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>U : Set E<VAR>hf : AnalyticOn 𝕜 f U<VAR>hU : IsPreconnected U<VAR>z₀ : E<VAR>h₀ : z₀ ∈ U<VAR>hfz₀ : f =ᶠ[𝓝 z₀] 0<VAR>u : Set E := {x | f =ᶠ[𝓝 x] 0}<VAR>x : E<VAR>xu : x ∈ closure u<VAR>xU : x ∈ U<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>hp : HasFPowerSeriesOnBall f p x r<VAR>y : E<VAR>yu : y ∈ u<VAR>hxy : edist x y < r / 2<VAR>q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)<VAR>has_series : HasFPowerSeriesOnBall f q y (r / 2)<VAR>M : EMetric.ball y (r / 2) ∈ 𝓝 x<VAR>z : E<VAR>hz : z ∈ EMetric.ball y (r / 2)<VAR>A : HasSum (fun n => (q n) fun x => z - y) (f z)<GOAL>f z = 0 z
<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>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>U : Set E<VAR>hf : AnalyticOn 𝕜 f U<VAR>hU : IsPreconnected U<VAR>z₀ : E<VAR>h₀ : z₀ ∈ U<VAR>hfz₀ : f =ᶠ[𝓝 z₀] 0<VAR>u : Set E := {x | f =ᶠ[𝓝 x] 0}<VAR>x : E<VAR>xu : x ∈ closure u<VAR>xU : x ∈ U<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>hp : HasFPowerSeriesOnBall f p x r<VAR>y : E<VAR>yu : y ∈ u<VAR>hxy : edist x y < r / 2<VAR>q : FormalMultilinearSeries 𝕜 E F := p.changeOrigin (y - x)<VAR>has_series : HasFPowerSeriesOnBall f q y (r / 2)<VAR>M : EMetric.ball y (r / 2) ∈ 𝓝 x<VAR>z : E<VAR>hz : z ∈ EMetric.ball y (r / 2)<VAR>A : HasSum (fun n => (q n) fun x => z - y) (f z)<VAR>B : HasSum (fun n => (q n) fun x => z - y) 0<GOAL>f z = 0 z
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<VAR>p q : R[X]<VAR>n : ℕ<VAR>hp : p ≠ 0<GOAL>(p * X).natDegree = p.natDegree + 1
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasShift C ℤ<VAR>T₁ T₂ T₃ A B : Triangle C<VAR>e : A ≅ B<GOAL>e.hom.hom₂ ≫ e.inv.hom₂ = 𝟙 A.obj₂
<VAR>a r : ℝ<VAR>ha : 0 < a<VAR>hr : 0 < r<VAR>x : ℝ<GOAL>↑(gammaCDFReal a r) x = ∫ (x : ℝ) in Iic x, gammaPDFReal a r x
<VAR>a r : ℝ<VAR>ha : 0 < a<VAR>hr : 0 < r<VAR>x : ℝ<VAR>this : IsProbabilityMeasure (gammaMeasure a r)<GOAL>↑(gammaCDFReal a r) x = ∫ (x : ℝ) in Iic x, gammaPDFReal a r x
<VAR>a r : ℝ<VAR>ha : 0 < a<VAR>hr : 0 < r<VAR>x : ℝ<VAR>this : IsProbabilityMeasure (gammaMeasure a r)<GOAL>(∫⁻ (a_1 : ℝ) in Iic x, gammaPDF a r a_1).toReal = ∫ (x : ℝ) in Iic x, gammaPDFReal a r x
<VAR>a r : ℝ<VAR>ha : 0 < a<VAR>hr : 0 < r<VAR>x : ℝ<VAR>this : IsProbabilityMeasure (gammaMeasure a r)<GOAL>0 ≤ᶠ[ae (ℙ.restrict (Iic x))] gammaPDFReal a r
<VAR>a r : ℝ<VAR>ha : 0 < a<VAR>hr : 0 < r<VAR>x : ℝ<VAR>this : IsProbabilityMeasure (gammaMeasure a r)<GOAL>AEStronglyMeasurable (gammaPDFReal a r) (ℙ.restrict (Iic x))
<VAR>G : Type u<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Finite G<GOAL>∃ ι x p, ∃ (_ : ∀ (i : ι), Nat.Prime (p i)), ∃ e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))
<VAR>G : Type u<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Finite G<VAR>val✝ : Fintype G<GOAL>∃ ι x p, ∃ (_ : ∀ (i : ι), Nat.Prime (p i)), ∃ e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))
<VAR>G : Type u<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Finite G<VAR>val✝ : Fintype G<VAR>n : ℕ<VAR>ι : Type<VAR>fι : Fintype ι<VAR>p : ι → ℕ<VAR>hp : ∀ (i : ι), Nat.Prime (p i)<VAR>e : ι → ℕ<VAR>f : G ≃+ (Fin n →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)<GOAL>∃ ι x p, ∃ (_ : ∀ (i : ι), Nat.Prime (p i)), ∃ e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>v : ↑(sphere 0 1)<GOAL>LinearMap.range (mfderiv 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) 𝓘(ℝ, E) Subtype.val v) = (Submodule.span ℝ {↑v})ᗮ
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>v : ↑(sphere 0 1)<GOAL>LinearMap.range (fderivWithin ℝ (writtenInExtChartAt 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) 𝓘(ℝ, E) v Subtype.val) (Set.range ↑𝓘(ℝ, EuclideanSpace ℝ (Fin n))) (↑(extChartAt 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) v) v)) = (Submodule.span ℝ {↑v})ᗮ
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>v : ↑(sphere 0 1)<GOAL>LinearMap.range (fderivWithin ℝ (Subtype.val ∘ ↑(ChartedSpace.chartAt v).symm) (Set.range id) (↑(ChartedSpace.chartAt v) v)) = (Submodule.span ℝ {↑v})ᗮ
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>v : ↑(sphere 0 1)<GOAL>LinearMap.range (fderiv ℝ (Subtype.val ∘ ↑(ChartedSpace.chartAt v).symm) (↑(ChartedSpace.chartAt v) v)) = (Submodule.span ℝ {↑v})ᗮ
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>v : ↑(sphere 0 1)<VAR>U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr<GOAL>LinearMap.range (fderiv ℝ (Subtype.val ∘ ↑(ChartedSpace.chartAt v).symm) (↑(ChartedSpace.chartAt v) v)) = (Submodule.span ℝ {↑v})ᗮ
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>v : ↑(sphere 0 1)<VAR>U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr<GOAL>LinearMap.range (fderiv ℝ ((stereoInvFunAux (-↑v) ∘ Subtype.val) ∘ ⇑U.symm) 0) = (Submodule.span ℝ {↑v})ᗮ
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>v : ↑(sphere 0 1)<VAR>U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr<VAR>this : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (Submodule.span ℝ {↑(-v)})ᗮ.subtypeL (U.symm 0)<GOAL>LinearMap.range (fderiv ℝ ((stereoInvFunAux (-↑v) ∘ Subtype.val) ∘ ⇑U.symm) 0) = (Submodule.span ℝ {↑v})ᗮ
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>v : ↑(sphere 0 1)<VAR>U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr<VAR>this : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (Submodule.span ℝ {↑(-v)})ᗮ.subtypeL (U.symm 0)<GOAL>(Submodule.span ℝ {↑v})ᗮ = LinearMap.range ((Submodule.span ℝ {↑(-v)})ᗮ.subtypeL.comp ↑U.symm.toContinuousLinearEquiv)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>v : ↑(sphere 0 1)<VAR>U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr<VAR>this : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (Submodule.span ℝ {↑(-v)})ᗮ.subtypeL (U.symm 0)<GOAL>LinearMap.range ((Submodule.span ℝ {↑(-v)})ᗮ.subtypeL.comp ↑U.symm.toContinuousLinearEquiv) = (Submodule.span ℝ {↑v})ᗮ
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>v : ↑(sphere 0 1)<VAR>U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr<VAR>this : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (Submodule.span ℝ {↑(-v)})ᗮ.subtypeL (U.symm 0)<GOAL>(Submodule.span ℝ {↑v})ᗮ = LinearMap.range (Submodule.span ℝ {↑(-v)})ᗮ.subtype
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>v : ↑(sphere 0 1)<VAR>U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr<VAR>this : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (Submodule.span ℝ {↑(-v)})ᗮ.subtypeL (U.symm 0)<GOAL>(Submodule.span ℝ {↑v})ᗮ = (Submodule.span ℝ {-↑v})ᗮ
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>v : ↑(sphere 0 1)<VAR>U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr<VAR>this : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (Submodule.span ℝ {↑(-v)})ᗮ.subtypeL (U.symm 0)<GOAL>Submodule.span ℝ {↑v} = Submodule.span ℝ {-↑v}
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>v : ↑(sphere 0 1)<VAR>U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr<VAR>this : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (Submodule.span ℝ {↑(-v)})ᗮ.subtypeL (U.symm 0)<GOAL>{↑v} ⊆ ↑(Submodule.span ℝ {-↑v})
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>H : Type u_3<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>inst✝ : Fact (finrank ℝ E = n + 1)<VAR>v : ↑(sphere 0 1)<VAR>U : ↥(Submodule.span ℝ {↑(-v)})ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr<VAR>this : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (Submodule.span ℝ {↑(-v)})ᗮ.subtypeL (U.symm 0)<GOAL>{-↑v} ⊆ ↑(Submodule.span ℝ {↑v})
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>i : ι<VAR>b : β i<VAR>hb : b ≠ 0<VAR>j : ι<VAR>h : ¬i = j<GOAL>j ∈ (single i b).support ↔ j ∈ {i}
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c✝ : E<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>s✝ s : Set α<VAR>c : G<VAR>hμs : μ s ≠ 0<GOAL>eLpNormEssSup (s.indicator fun x => c) μ = ↑‖c‖₊
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c✝ : E<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>s✝ s : Set α<VAR>c : G<VAR>hμs : μ s ≠ 0<GOAL>↑‖c‖₊ ≤ eLpNormEssSup (s.indicator fun x => c) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c✝ : E<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>s✝ s : Set α<VAR>c : G<VAR>hμs : μ s ≠ 0<VAR>h : eLpNormEssSup (s.indicator fun x => c) μ < ↑‖c‖₊<GOAL>False
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c✝ : E<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>s✝ s : Set α<VAR>c : G<VAR>hμs : μ s ≠ 0<VAR>h : eLpNormEssSup (s.indicator fun x => c) μ < ↑‖c‖₊<VAR>h' : μ {a | ¬↑‖s.indicator (fun x => c) a‖₊ < ↑‖c‖₊} = 0<GOAL>False
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c✝ : E<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>s✝ s : Set α<VAR>c : G<VAR>hμs : μ s ≠ 0<VAR>h : eLpNormEssSup (s.indicator fun x => c) μ < ↑‖c‖₊<VAR>h' : μ {a | ↑‖c‖₊ ≤ ↑‖s.indicator (fun x => c) a‖₊} = 0<GOAL>False
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c✝ : E<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>s✝ s : Set α<VAR>c : G<VAR>hμs : μ s ≠ 0<VAR>h : eLpNormEssSup (s.indicator fun x => c) μ < ↑‖c‖₊<VAR>h' : μ {a | ↑‖c‖₊ ≤ ↑‖s.indicator (fun x => c) a‖₊} = 0<VAR>x : α<VAR>hx_mem : x ∈ s<GOAL>x ∈ {a | ↑‖c‖₊ ≤ ↑‖s.indicator (fun x => c) a‖₊}
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>[] = l.rotate n ↔ [] = l
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>a : R<VAR>x : σ<GOAL>degreeOf x (C a) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder β<VAR>s t : Finset α<VAR>f : Finset α → β<VAR>inst✝ : DecidableEq α<GOAL>StrictMono f ↔ ∀ (s : Finset α) ⦃a : α⦄, a ∉ s → f s < f (insert a s)