ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝²⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝²³ : NormedAddCommGroup E<VAR>inst✝²² : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝²¹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝²⁰ : TopologicalSpace M<VAR>inst✝¹⁹ : ChartedSpace H M<VAR>Is : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁸ : NormedAddCommGroup E'<VAR>inst✝¹⁷ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁶ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝¹⁵ : TopologicalSpace M'<VAR>inst✝¹⁴ : ChartedSpace H' M'<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<VAR>F' : Type u_11<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝⁶ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝⁵ : TopologicalSpace N'<VAR>inst✝⁴ : ChartedSpace G' N'<VAR>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>hf : ContMDiffOn I I' n f univ<VAR>hmn : m + 1 ≤ n<GOAL>tangentMap I I' f = tangentMapWithin I I' f univ
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hdf : ∀ᶠ (x : ℝ) in 𝓝[≠] a, DifferentiableAt ℝ f x<VAR>hg' : ∀ᶠ (x : ℝ) in 𝓝[≠] a, deriv g x ≠ 0<VAR>hfa : Tendsto f (𝓝[≠] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[≠] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[≠] a) l<GOAL>Tendsto (fun x => f x / g x) (𝓝[≠] a) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hdf : (∀ᶠ (x : ℝ) in 𝓝[<] a, DifferentiableAt ℝ f x) ∧ ∀ᶠ (x : ℝ) in 𝓝[>] a, DifferentiableAt ℝ f x<VAR>hg' : (∀ᶠ (x : ℝ) in 𝓝[<] a, deriv g x ≠ 0) ∧ ∀ᶠ (x : ℝ) in 𝓝[>] a, deriv g x ≠ 0<VAR>hfa : Tendsto f (𝓝[<] a) (𝓝 0) ∧ Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Tendsto g (𝓝[<] a) (𝓝 0) ∧ Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[<] a) l ∧ Tendsto (fun x => deriv f x / deriv g x) (𝓝[>] a) l<GOAL>Tendsto (fun x => f x / g x) (𝓝[<] a) l ∧ Tendsto (fun x => f x / g x) (𝓝[>] a) l
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁵ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝⁴ : TopologicalSpace M''<VAR>inst✝³ : ChartedSpace H'' M''<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>e : PartialHomeomorph M H<VAR>h : e ∈ atlas H M<VAR>x : H<VAR>hx : x ∈ e.target<GOAL>MDifferentiableAt I I (↑e.symm) x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁵ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝⁴ : TopologicalSpace M''<VAR>inst✝³ : ChartedSpace H'' M''<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>e : PartialHomeomorph M H<VAR>h : e ∈ atlas H M<VAR>x : H<VAR>hx : x ∈ e.target<GOAL>ContinuousAt (↑e.symm) x ∧ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x ↑e.symm) (range ↑I) (↑(extChartAt I x) x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁵ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝⁴ : TopologicalSpace M''<VAR>inst✝³ : ChartedSpace H'' M''<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>e : PartialHomeomorph M H<VAR>h : e ∈ atlas H M<VAR>x : H<VAR>hx : x ∈ e.target<GOAL>DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x ↑e.symm) (range ↑I) (↑(extChartAt I x) x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁵ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝⁴ : TopologicalSpace M''<VAR>inst✝³ : ChartedSpace H'' M''<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>e : PartialHomeomorph M H<VAR>h : e ∈ atlas H M<VAR>x : H<VAR>hx : x ∈ e.target<VAR>mem : ↑I x ∈ ↑I.symm ⁻¹' (e.symm ≫ₕ chartAt H (↑e.symm x)).source ∩ range ↑I<GOAL>DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x ↑e.symm) (range ↑I) (↑(extChartAt I x) x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁵ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝⁴ : TopologicalSpace M''<VAR>inst✝³ : ChartedSpace H'' M''<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>e : PartialHomeomorph M H<VAR>h : e ∈ atlas H M<VAR>x : H<VAR>hx : x ∈ e.target<VAR>mem : ↑I x ∈ ↑I.symm ⁻¹' (e.symm ≫ₕ chartAt H (↑e.symm x)).source ∩ range ↑I<VAR>this : e.symm ≫ₕ chartAt H (↑e.symm x) ∈ contDiffGroupoid ⊤ I<GOAL>DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x ↑e.symm) (range ↑I) (↑(extChartAt I x) x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁵ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝⁴ : TopologicalSpace M''<VAR>inst✝³ : ChartedSpace H'' M''<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>e : PartialHomeomorph M H<VAR>h : e ∈ atlas H M<VAR>x : H<VAR>hx : x ∈ e.target<VAR>mem : ↑I x ∈ ↑I.symm ⁻¹' (e.symm ≫ₕ chartAt H (↑e.symm x)).source ∩ range ↑I<VAR>this : e.symm ≫ₕ chartAt H (↑e.symm x) ∈ contDiffGroupoid ⊤ I<VAR>A : ContDiffOn 𝕜 ⊤ (↑I ∘ ↑(e.symm ≫ₕ chartAt H (↑e.symm x)) ∘ ↑I.symm) (↑I.symm ⁻¹' (e.symm ≫ₕ chartAt H (↑e.symm x)).source ∩ range ↑I)<GOAL>DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x ↑e.symm) (range ↑I) (↑(extChartAt I x) x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁵ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝⁴ : TopologicalSpace M''<VAR>inst✝³ : ChartedSpace H'' M''<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>e : PartialHomeomorph M H<VAR>h : e ∈ atlas H M<VAR>x : H<VAR>hx : x ∈ e.target<VAR>mem : ↑I x ∈ ↑I.symm ⁻¹' (e.symm ≫ₕ chartAt H (↑e.symm x)).source ∩ range ↑I<VAR>this : e.symm ≫ₕ chartAt H (↑e.symm x) ∈ contDiffGroupoid ⊤ I<VAR>A : ContDiffOn 𝕜 ⊤ (↑I ∘ ↑(e.symm ≫ₕ chartAt H (↑e.symm x)) ∘ ↑I.symm) (↑I.symm ⁻¹' (e.symm ≫ₕ chartAt H (↑e.symm x)).source ∩ range ↑I)<VAR>B : DifferentiableWithinAt 𝕜 (↑I ∘ ↑(e.symm ≫ₕ chartAt H (↑e.symm x)) ∘ ↑I.symm) (↑I.symm ⁻¹' (e.symm ≫ₕ chartAt H (↑e.symm x)).source ∩ range ↑I) (↑I x)<GOAL>DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x ↑e.symm) (range ↑I) (↑(extChartAt I x) x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁵ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝⁴ : TopologicalSpace M''<VAR>inst✝³ : ChartedSpace H'' M''<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>e : PartialHomeomorph M H<VAR>h : e ∈ atlas H M<VAR>x : H<VAR>hx : x ∈ e.target<VAR>mem : ↑I x ∈ ↑I.symm ⁻¹' (e.symm ≫ₕ chartAt H (↑e.symm x)).source ∩ range ↑I<VAR>this : e.symm ≫ₕ chartAt H (↑e.symm x) ∈ contDiffGroupoid ⊤ I<VAR>A : ContDiffOn 𝕜 ⊤ (↑I ∘ ↑(e.symm ≫ₕ chartAt H (↑e.symm x)) ∘ ↑I.symm) (↑I.symm ⁻¹' (e.symm ≫ₕ chartAt H (↑e.symm x)).source ∩ range ↑I)<VAR>B : DifferentiableWithinAt 𝕜 (↑I ∘ (↑(chartAt H (↑e.symm x)) ∘ ↑e.symm) ∘ ↑I.symm) (↑I.symm ⁻¹' e.target ∩ ↑I.symm ⁻¹' (↑e.symm ⁻¹' (chartAt H (↑e.symm x)).source) ∩ range ↑I) (↑I x)<GOAL>DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x ↑e.symm) (range ↑I) (↑(extChartAt I x) x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁵ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝⁴ : TopologicalSpace M''<VAR>inst✝³ : ChartedSpace H'' M''<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>e : PartialHomeomorph M H<VAR>h : e ∈ atlas H M<VAR>x : H<VAR>hx : x ∈ e.target<VAR>mem : ↑I x ∈ ↑I.symm ⁻¹' (e.symm ≫ₕ chartAt H (↑e.symm x)).source ∩ range ↑I<VAR>this : e.symm ≫ₕ chartAt H (↑e.symm x) ∈ contDiffGroupoid ⊤ I<VAR>A : ContDiffOn 𝕜 ⊤ (↑I ∘ ↑(e.symm ≫ₕ chartAt H (↑e.symm x)) ∘ ↑I.symm) (↑I.symm ⁻¹' (e.symm ≫ₕ chartAt H (↑e.symm x)).source ∩ range ↑I)<VAR>B : DifferentiableWithinAt 𝕜 (↑I ∘ (↑(chartAt H (↑e.symm x)) ∘ ↑e.symm) ∘ ↑I.symm) (range ↑I) (↑I x)<GOAL>DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x ↑e.symm) (range ↑I) (↑(extChartAt I x) x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁹ : TopologicalSpace M'<VAR>inst✝⁸ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝⁵ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝⁴ : TopologicalSpace M''<VAR>inst✝³ : ChartedSpace H'' M''<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SmoothManifoldWithCorners I' M'<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>e : PartialHomeomorph M H<VAR>h : e ∈ atlas H M<VAR>x : H<VAR>hx : x ∈ e.target<VAR>mem : ↑I x ∈ ↑I.symm ⁻¹' (e.symm ≫ₕ chartAt H (↑e.symm x)).source ∩ range ↑I<VAR>this : e.symm ≫ₕ chartAt H (↑e.symm x) ∈ contDiffGroupoid ⊤ I<VAR>A : ContDiffOn 𝕜 ⊤ (↑I ∘ ↑(e.symm ≫ₕ chartAt H (↑e.symm x)) ∘ ↑I.symm) (↑I.symm ⁻¹' (e.symm ≫ₕ chartAt H (↑e.symm x)).source ∩ range ↑I)<VAR>B : DifferentiableWithinAt 𝕜 (↑I ∘ (↑(chartAt H (↑e.symm x)) ∘ ↑e.symm) ∘ ↑I.symm) (range ↑I ∩ (↑I.symm ⁻¹' e.target ∩ ↑I.symm ⁻¹' (↑e.symm ⁻¹' (chartAt H (↑e.symm x)).source))) (↑I x)<GOAL>↑I.symm ⁻¹' e.target ∩ ↑I.symm ⁻¹' (↑e.symm ⁻¹' (chartAt H (↑e.symm x)).source) ∈ 𝓝 (↑I x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>hs₀ : StarConvex ℝ 0 s<VAR>hs₂ : Absorbs ℝ s {x}<VAR>hx : x ∉ a • s<GOAL>a ≤ gauge s x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s<VAR>hs₂ : Absorbs ℝ s {x}<VAR>hx : x ∉ a • s<GOAL>a ≤ gauge s x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s<VAR>hs₂ : Absorbs ℝ s {x}<VAR>hx : x ∉ a • s<VAR>r : ℝ<VAR>hr : r > 0<VAR>h : ∀ (c : ℝ), r ≤ ‖c‖ → {x} ⊆ c • s<GOAL>a ≤ gauge s x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s<VAR>hs₂ : Absorbs ℝ s {x}<VAR>hx : x ∉ a • s<VAR>r : ℝ<VAR>hr : r > 0<VAR>h : ∀ (c : ℝ), r ≤ ‖c‖ → {x} ⊆ c • s<GOAL>∀ b ∈ {r | 0 < r ∧ x ∈ r • s}, a ≤ b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>a : ℝ<VAR>hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s<VAR>r : ℝ<VAR>hr : r > 0<VAR>b : ℝ<VAR>hb : 0 < b<VAR>x : E<VAR>hx' : x ∈ s<VAR>hs₂ : Absorbs ℝ s {(fun x => b • x) x}<VAR>hx : (fun x => b • x) x ∉ a • s<VAR>h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun x => b • x) x} ⊆ c • s<GOAL>a ≤ b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>a : ℝ<VAR>hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s<VAR>r : ℝ<VAR>hr : r > 0<VAR>b : ℝ<VAR>hb : 0 < b<VAR>x : E<VAR>hx' : x ∈ s<VAR>hs₂ : Absorbs ℝ s {(fun x => b • x) x}<VAR>hx : (fun x => b • x) x ∉ a • s<VAR>h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun x => b • x) x} ⊆ c • s<VAR>hba : b < a<GOAL>(fun x => b • x) x ∈ a • s
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : TopologicalSpace F<VAR>inst✝⁵ : TopologicalSpace B<VAR>e✝ : Pretrivialization F TotalSpace.proj<VAR>x : TotalSpace F E<VAR>b✝ : B<VAR>y : E b✝<VAR>inst✝⁴ : AddCommMonoid F<VAR>inst✝³ : Module R F<VAR>inst✝² : (x : B) → AddCommMonoid (E x)<VAR>inst✝¹ : (x : B) → Module R (E x)<VAR>e : Pretrivialization F TotalSpace.proj<VAR>inst✝ : Pretrivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<GOAL>⇑(Pretrivialization.linearMapAt R e b) = fun y => (↑e { proj := b, snd := y }).2
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.LeftHomologyData<VAR>A : C<VAR>hf : S.f = 0<VAR>c : KernelFork S.g<VAR>hc : IsLimit c<GOAL>(ofIsLimitKernelFork S hf c hc).f' = 0
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>∑' (n : ℕ), (riemannZetaSummandHom ⋯) n = riemannZeta s
<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>hsum : Summable fun n => ‖(riemannZetaSummandHom ⋯) n‖<GOAL>∑' (n : ℕ), (riemannZetaSummandHom ⋯) n = riemannZeta s
<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>hsum : Summable fun n => ‖(riemannZetaSummandHom ⋯) n‖<GOAL>∑' (b : ℕ), (riemannZetaSummandHom ⋯) (b + 1) = ∑' (n : ℕ), 1 / (↑n + 1) ^ s
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>n : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>f : R →+* S<GOAL>(univ R n).coeff (Fintype.card n) = 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>n : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>f : R →+* S<GOAL>(univ ℤ n).coeff (Fintype.card n) = 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>n : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>f : R →+* S<GOAL>(univ ℤ n).coeff (univ ℤ n).natDegree = 1
<VAR>θ ψ : Angle<VAR>h : 2 • θ = 2 • ψ<GOAL>θ.tan = ψ.tan
<VAR>θ ψ : Angle<VAR>h : θ = ψ ∨ θ = ψ + ↑π<GOAL>θ.tan = ψ.tan
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : Module k V1<VAR>inst✝⁹ : AffineSpace V1 P1<VAR>inst✝⁸ : AddCommGroup V2<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : AffineSpace V2 P2<VAR>inst✝⁵ : AddCommGroup V3<VAR>inst✝⁴ : Module k V3<VAR>inst✝³ : AffineSpace V3 P3<VAR>inst✝² : AddCommGroup V4<VAR>inst✝¹ : Module k V4<VAR>inst✝ : AffineSpace V4 P4<VAR>f : P1 →ᵃ[k] P2<VAR>p₀ p₁ : P1<VAR>c : k<GOAL>f ((lineMap p₀ p₁) c) = (lineMap (f p₀) (f p₁)) c
<VAR>X : Type u<VAR>inst✝ : TopologicalSpace X<VAR>x y : X<VAR>γ : Path x y<GOAL>delayReflLeft 0 γ = (refl x).trans γ
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>X Y : C<VAR>inst✝¹ : HasBinaryBiproduct X Y<VAR>inst✝ : PreservesBinaryBiproduct X Y F<VAR>W : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<GOAL>lift (F.map f) (F.map g) ≫ (F.mapBiprod X Y).inv = F.map (lift f g)
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>N : Type u_4<VAR>α : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : SMul N α<VAR>inst✝ : MulAction M α<VAR>s : Set M<VAR>htop : Submonoid.closure s = ⊤<VAR>hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z<GOAL>SMulCommClass M N α
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>N : Type u_4<VAR>α : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : SMul N α<VAR>inst✝ : MulAction M α<VAR>s : Set M<VAR>htop : Submonoid.closure s = ⊤<VAR>hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z<VAR>x : M<GOAL>∀ (n : N) (a : α), 1 • n • a = n • 1 • a
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>N : Type u_4<VAR>α : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : SMul N α<VAR>inst✝ : MulAction M α<VAR>s : Set M<VAR>htop : Submonoid.closure s = ⊤<VAR>hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z<VAR>x : M<GOAL>∀ x ∈ s, ∀ (y : M), (∀ (n : N) (a : α), y • n • a = n • y • a) → ∀ (n : N) (a : α), (x * y) • n • a = n • (x * y) • a
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>Set.range (sum_to C ho) = GoodProducts (π C fun x => ord I x < o) ∪ MaxProducts C ho
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>h : Set.range (sum_to C ho) = Set.range Subtype.val ∪ Set.range Subtype.val<GOAL>Set.range (sum_to C ho) = GoodProducts (π C fun x => ord I x < o) ∪ MaxProducts C ho
<VAR>N✝ N : ℕ<VAR>g : ConjAct SL(2, ℤ)<GOAL>g • Gamma N = Gamma N
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹⁴ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹³ : TopologicalSpace β<VAR>inst✝¹² : TopologicalSpace γ<VAR>inst✝¹¹ : TopologicalSpace δ<VAR>inst✝¹⁰ : MeasurableSpace β<VAR>inst✝⁹ : PseudoMetrizableSpace β<VAR>inst✝⁸ : BorelSpace β<VAR>inst✝⁷ : MeasurableSpace γ<VAR>inst✝⁶ : PseudoMetrizableSpace γ<VAR>inst✝⁵ : BorelSpace γ<VAR>inst✝⁴ : SecondCountableTopologyEither β γ<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : PseudoMetrizableSpace δ<VAR>inst✝¹ : OpensMeasurableSpace δ<VAR>inst✝ : SecondCountableTopology δ<VAR>g : β → γ → δ<VAR>hg : Measurable (uncurry g)<VAR>f₁ : α →ₘ[μ] β<VAR>f₂ : α →ₘ[μ] γ<GOAL>comp₂Measurable g hg f₁ f₂ = mk (fun a => g (↑f₁ a) (↑f₂ a)) ⋯