ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s✝ s' : Set ℝ<VAR>t₀ : ℝ<VAR>x₀ : M<VAR>hx : I.IsInteriorPoint x₀<VAR>left✝ : ContinuousAt (fun x => { proj := x, snd := v x }) x₀<VAR>hv : ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (range ↑I) (↑(extChartAt I x₀) x₀)<VAR>f : ℝ → E<VAR>hf1 : f t₀ = ↑(extChartAt I x₀) x₀<VAR>hf2 : ∀ᶠ (y : ℝ) in 𝓝 t₀, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y<VAR>a : ℝ<VAR>ha : a > 0<VAR>hf2' : ∀ y ∈ Metric.ball t₀ a, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y<VAR>hcont : ∀ A ∈ 𝓝 (↑(extChartAt I x₀) x₀), f ⁻¹' A ∈ 𝓝 t₀<VAR>hnhds : ∀ᶠ (x' : ℝ) in 𝓝 t₀, f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 x'<VAR>s : Set ℝ<VAR>hs : s ∈ 𝓝 t₀<VAR>haux : ∀ y ∈ s, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y ∧ f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 y<VAR>t : ℝ<VAR>ht : t ∈ s<VAR>xₜ : M := ↑(extChartAt I x₀).symm (f t)<VAR>h : HasDerivAt f ((tangentCoordChange I xₜ x₀ xₜ) (v xₜ)) t<VAR>hf3 : f t ∈ interior (extChartAt I x₀).target<GOAL>HasMFDerivAt 𝓘(ℝ, ℝ) I (↑(extChartAt I x₀).symm ∘ f) t (ContinuousLinearMap.smulRight 1 (v ((↑(extChartAt I x₀).symm ∘ f) t)))
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s✝ s' : Set ℝ<VAR>t₀ : ℝ<VAR>x₀ : M<VAR>hx : I.IsInteriorPoint x₀<VAR>left✝ : ContinuousAt (fun x => { proj := x, snd := v x }) x₀<VAR>hv : ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (range ↑I) (↑(extChartAt I x₀) x₀)<VAR>f : ℝ → E<VAR>hf1 : f t₀ = ↑(extChartAt I x₀) x₀<VAR>hf2 : ∀ᶠ (y : ℝ) in 𝓝 t₀, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y<VAR>a : ℝ<VAR>ha : a > 0<VAR>hf2' : ∀ y ∈ Metric.ball t₀ a, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y<VAR>hcont : ∀ A ∈ 𝓝 (↑(extChartAt I x₀) x₀), f ⁻¹' A ∈ 𝓝 t₀<VAR>hnhds : ∀ᶠ (x' : ℝ) in 𝓝 t₀, f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 x'<VAR>s : Set ℝ<VAR>hs : s ∈ 𝓝 t₀<VAR>haux : ∀ y ∈ s, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y ∧ f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 y<VAR>t : ℝ<VAR>ht : t ∈ s<VAR>xₜ : M := ↑(extChartAt I x₀).symm (f t)<VAR>h : HasDerivAt f ((tangentCoordChange I xₜ x₀ xₜ) (v xₜ)) t<VAR>hf3 : f t ∈ interior (extChartAt I x₀).target<VAR>hf3' : f t ∈ (extChartAt I x₀).target<GOAL>HasMFDerivAt 𝓘(ℝ, ℝ) I (↑(extChartAt I x₀).symm ∘ f) t (ContinuousLinearMap.smulRight 1 (v ((↑(extChartAt I x₀).symm ∘ f) t)))
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s✝ s' : Set ℝ<VAR>t₀ : ℝ<VAR>x₀ : M<VAR>hx : I.IsInteriorPoint x₀<VAR>left✝ : ContinuousAt (fun x => { proj := x, snd := v x }) x₀<VAR>hv : ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (range ↑I) (↑(extChartAt I x₀) x₀)<VAR>f : ℝ → E<VAR>hf1 : f t₀ = ↑(extChartAt I x₀) x₀<VAR>hf2 : ∀ᶠ (y : ℝ) in 𝓝 t₀, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y<VAR>a : ℝ<VAR>ha : a > 0<VAR>hf2' : ∀ y ∈ Metric.ball t₀ a, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y<VAR>hcont : ∀ A ∈ 𝓝 (↑(extChartAt I x₀) x₀), f ⁻¹' A ∈ 𝓝 t₀<VAR>hnhds : ∀ᶠ (x' : ℝ) in 𝓝 t₀, f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 x'<VAR>s : Set ℝ<VAR>hs : s ∈ 𝓝 t₀<VAR>haux : ∀ y ∈ s, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y ∧ f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 y<VAR>t : ℝ<VAR>ht : t ∈ s<VAR>xₜ : M := ↑(extChartAt I x₀).symm (f t)<VAR>h : HasDerivAt f ((tangentCoordChange I xₜ x₀ xₜ) (v xₜ)) t<VAR>hf3 : f t ∈ interior (extChartAt I x₀).target<VAR>hf3' : f t ∈ (extChartAt I x₀).target<VAR>hft1 : ↑(extChartAt I x₀).symm (f t) ∈ (extChartAt I x₀).source<GOAL>HasMFDerivAt 𝓘(ℝ, ℝ) I (↑(extChartAt I x₀).symm ∘ f) t (ContinuousLinearMap.smulRight 1 (v ((↑(extChartAt I x₀).symm ∘ f) t)))
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s✝ s' : Set ℝ<VAR>t₀ : ℝ<VAR>x₀ : M<VAR>hx : I.IsInteriorPoint x₀<VAR>left✝ : ContinuousAt (fun x => { proj := x, snd := v x }) x₀<VAR>hv : ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (range ↑I) (↑(extChartAt I x₀) x₀)<VAR>f : ℝ → E<VAR>hf1 : f t₀ = ↑(extChartAt I x₀) x₀<VAR>hf2 : ∀ᶠ (y : ℝ) in 𝓝 t₀, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y<VAR>a : ℝ<VAR>ha : a > 0<VAR>hf2' : ∀ y ∈ Metric.ball t₀ a, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y<VAR>hcont : ∀ A ∈ 𝓝 (↑(extChartAt I x₀) x₀), f ⁻¹' A ∈ 𝓝 t₀<VAR>hnhds : ∀ᶠ (x' : ℝ) in 𝓝 t₀, f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 x'<VAR>s : Set ℝ<VAR>hs : s ∈ 𝓝 t₀<VAR>haux : ∀ y ∈ s, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y ∧ f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 y<VAR>t : ℝ<VAR>ht : t ∈ s<VAR>xₜ : M := ↑(extChartAt I x₀).symm (f t)<VAR>h : HasDerivAt f ((tangentCoordChange I xₜ x₀ xₜ) (v xₜ)) t<VAR>hf3 : f t ∈ interior (extChartAt I x₀).target<VAR>hf3' : f t ∈ (extChartAt I x₀).target<VAR>hft1 : ↑(extChartAt I x₀).symm (f t) ∈ (extChartAt I x₀).source<VAR>hft2 : xₜ ∈ (extChartAt I xₜ).source<GOAL>HasMFDerivAt 𝓘(ℝ, ℝ) I (↑(extChartAt I x₀).symm ∘ f) t (ContinuousLinearMap.smulRight 1 (v ((↑(extChartAt I x₀).symm ∘ f) t)))
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s✝ s' : Set ℝ<VAR>t₀ : ℝ<VAR>x₀ : M<VAR>hx : I.IsInteriorPoint x₀<VAR>left✝ : ContinuousAt (fun x => { proj := x, snd := v x }) x₀<VAR>hv : ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (range ↑I) (↑(extChartAt I x₀) x₀)<VAR>f : ℝ → E<VAR>hf1 : f t₀ = ↑(extChartAt I x₀) x₀<VAR>hf2 : ∀ᶠ (y : ℝ) in 𝓝 t₀, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y<VAR>a : ℝ<VAR>ha : a > 0<VAR>hf2' : ∀ y ∈ Metric.ball t₀ a, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y<VAR>hcont : ∀ A ∈ 𝓝 (↑(extChartAt I x₀) x₀), f ⁻¹' A ∈ 𝓝 t₀<VAR>hnhds : ∀ᶠ (x' : ℝ) in 𝓝 t₀, f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 x'<VAR>s : Set ℝ<VAR>hs : s ∈ 𝓝 t₀<VAR>haux : ∀ y ∈ s, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y ∧ f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 y<VAR>t : ℝ<VAR>ht : t ∈ s<VAR>xₜ : M := ↑(extChartAt I x₀).symm (f t)<VAR>h : HasDerivAt f ((tangentCoordChange I xₜ x₀ xₜ) (v xₜ)) t<VAR>hf3 : f t ∈ interior (extChartAt I x₀).target<VAR>hf3' : f t ∈ (extChartAt I x₀).target<VAR>hft1 : ↑(extChartAt I x₀).symm (f t) ∈ (extChartAt I x₀).source<VAR>hft2 : xₜ ∈ (extChartAt I xₜ).source<GOAL>HasDerivWithinAt (writtenInExtChartAt 𝓘(ℝ, ℝ) I t (↑(extChartAt I x₀).symm ∘ f)) (v ((↑(extChartAt I x₀).symm ∘ f) t)) (range ↑𝓘(ℝ, ℝ)) (↑(extChartAt 𝓘(ℝ, ℝ) t) t)
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s✝ s' : Set ℝ<VAR>t₀ : ℝ<VAR>x₀ : M<VAR>hx : I.IsInteriorPoint x₀<VAR>left✝ : ContinuousAt (fun x => { proj := x, snd := v x }) x₀<VAR>hv : ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (range ↑I) (↑(extChartAt I x₀) x₀)<VAR>f : ℝ → E<VAR>hf1 : f t₀ = ↑(extChartAt I x₀) x₀<VAR>hf2 : ∀ᶠ (y : ℝ) in 𝓝 t₀, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y<VAR>a : ℝ<VAR>ha : a > 0<VAR>hf2' : ∀ y ∈ Metric.ball t₀ a, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y<VAR>hcont : ∀ A ∈ 𝓝 (↑(extChartAt I x₀) x₀), f ⁻¹' A ∈ 𝓝 t₀<VAR>hnhds : ∀ᶠ (x' : ℝ) in 𝓝 t₀, f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 x'<VAR>s : Set ℝ<VAR>hs : s ∈ 𝓝 t₀<VAR>haux : ∀ y ∈ s, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y ∧ f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 y<VAR>t : ℝ<VAR>ht : t ∈ s<VAR>xₜ : M := ↑(extChartAt I x₀).symm (f t)<VAR>h : HasDerivAt f ((tangentCoordChange I xₜ x₀ xₜ) (v xₜ)) t<VAR>hf3 : f t ∈ interior (extChartAt I x₀).target<VAR>hf3' : f t ∈ (extChartAt I x₀).target<VAR>hft1 : ↑(extChartAt I x₀).symm (f t) ∈ (extChartAt I x₀).source<VAR>hft2 : xₜ ∈ (extChartAt I xₜ).source<GOAL>HasDerivAt ((↑I ∘ ↑(chartAt H (↑(chartAt H x₀).symm (↑I.symm (f t))))) ∘ (↑(chartAt H x₀).symm ∘ ↑I.symm) ∘ f) (v (↑(chartAt H x₀).symm (↑I.symm (f t)))) t
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s✝ s' : Set ℝ<VAR>t₀ : ℝ<VAR>x₀ : M<VAR>hx : I.IsInteriorPoint x₀<VAR>left✝ : ContinuousAt (fun x => { proj := x, snd := v x }) x₀<VAR>hv : ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (range ↑I) (↑(extChartAt I x₀) x₀)<VAR>f : ℝ → E<VAR>hf1 : f t₀ = ↑(extChartAt I x₀) x₀<VAR>hf2 : ∀ᶠ (y : ℝ) in 𝓝 t₀, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y<VAR>a : ℝ<VAR>ha : a > 0<VAR>hf2' : ∀ y ∈ Metric.ball t₀ a, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y<VAR>hcont : ∀ A ∈ 𝓝 (↑(extChartAt I x₀) x₀), f ⁻¹' A ∈ 𝓝 t₀<VAR>hnhds : ∀ᶠ (x' : ℝ) in 𝓝 t₀, f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 x'<VAR>s : Set ℝ<VAR>hs : s ∈ 𝓝 t₀<VAR>haux : ∀ y ∈ s, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y ∧ f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 y<VAR>t : ℝ<VAR>ht : t ∈ s<VAR>xₜ : M := ↑(extChartAt I x₀).symm (f t)<VAR>h : HasDerivAt f ((tangentCoordChange I xₜ x₀ xₜ) (v xₜ)) t<VAR>hf3 : f t ∈ interior (extChartAt I x₀).target<VAR>hf3' : f t ∈ (extChartAt I x₀).target<VAR>hft1 : ↑(extChartAt I x₀).symm (f t) ∈ (extChartAt I x₀).source<VAR>hft2 : xₜ ∈ (extChartAt I xₜ).source<GOAL>HasDerivAt ((↑(extChartAt I xₜ) ∘ ↑(extChartAt I x₀).symm) ∘ f) (v xₜ) t
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s✝ s' : Set ℝ<VAR>t₀ : ℝ<VAR>x₀ : M<VAR>hx : I.IsInteriorPoint x₀<VAR>left✝ : ContinuousAt (fun x => { proj := x, snd := v x }) x₀<VAR>hv : ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (range ↑I) (↑(extChartAt I x₀) x₀)<VAR>f : ℝ → E<VAR>hf1 : f t₀ = ↑(extChartAt I x₀) x₀<VAR>hf2 : ∀ᶠ (y : ℝ) in 𝓝 t₀, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y<VAR>a : ℝ<VAR>ha : a > 0<VAR>hf2' : ∀ y ∈ Metric.ball t₀ a, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y<VAR>hcont : ∀ A ∈ 𝓝 (↑(extChartAt I x₀) x₀), f ⁻¹' A ∈ 𝓝 t₀<VAR>hnhds : ∀ᶠ (x' : ℝ) in 𝓝 t₀, f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 x'<VAR>s : Set ℝ<VAR>hs : s ∈ 𝓝 t₀<VAR>haux : ∀ y ∈ s, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y ∧ f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 y<VAR>t : ℝ<VAR>ht : t ∈ s<VAR>xₜ : M := ↑(extChartAt I x₀).symm (f t)<VAR>h : HasDerivAt f ((tangentCoordChange I xₜ x₀ xₜ) (v xₜ)) t<VAR>hf3 : f t ∈ interior (extChartAt I x₀).target<VAR>hf3' : f t ∈ (extChartAt I x₀).target<VAR>hft1 : ↑(extChartAt I x₀).symm (f t) ∈ (extChartAt I x₀).source<VAR>hft2 : xₜ ∈ (extChartAt I xₜ).source<GOAL>HasDerivAt ((↑(extChartAt I xₜ) ∘ ↑(extChartAt I x₀).symm) ∘ f) ((tangentCoordChange I x₀ xₜ xₜ) ((tangentCoordChange I xₜ x₀ xₜ) (v xₜ))) t
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s✝ s' : Set ℝ<VAR>t₀ : ℝ<VAR>x₀ : M<VAR>hx : I.IsInteriorPoint x₀<VAR>left✝ : ContinuousAt (fun x => { proj := x, snd := v x }) x₀<VAR>hv : ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (range ↑I) (↑(extChartAt I x₀) x₀)<VAR>f : ℝ → E<VAR>hf1 : f t₀ = ↑(extChartAt I x₀) x₀<VAR>hf2 : ∀ᶠ (y : ℝ) in 𝓝 t₀, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y<VAR>a : ℝ<VAR>ha : a > 0<VAR>hf2' : ∀ y ∈ Metric.ball t₀ a, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y<VAR>hcont : ∀ A ∈ 𝓝 (↑(extChartAt I x₀) x₀), f ⁻¹' A ∈ 𝓝 t₀<VAR>hnhds : ∀ᶠ (x' : ℝ) in 𝓝 t₀, f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 x'<VAR>s : Set ℝ<VAR>hs : s ∈ 𝓝 t₀<VAR>haux : ∀ y ∈ s, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y ∧ f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 y<VAR>t : ℝ<VAR>ht : t ∈ s<VAR>xₜ : M := ↑(extChartAt I x₀).symm (f t)<VAR>h : HasDerivAt f ((tangentCoordChange I xₜ x₀ xₜ) (v xₜ)) t<VAR>hf3 : f t ∈ interior (extChartAt I x₀).target<VAR>hf3' : f t ∈ (extChartAt I x₀).target<VAR>hft1 : ↑(extChartAt I x₀).symm (f t) ∈ (extChartAt I x₀).source<VAR>hft2 : xₜ ∈ (extChartAt I xₜ).source<GOAL>HasFDerivAt (↑(extChartAt I xₜ) ∘ ↑(extChartAt I x₀).symm) (tangentCoordChange I x₀ xₜ xₜ) (f t)
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s✝ s' : Set ℝ<VAR>t₀ : ℝ<VAR>x₀ : M<VAR>hx : I.IsInteriorPoint x₀<VAR>left✝ : ContinuousAt (fun x => { proj := x, snd := v x }) x₀<VAR>hv : ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (range ↑I) (↑(extChartAt I x₀) x₀)<VAR>f : ℝ → E<VAR>hf1 : f t₀ = ↑(extChartAt I x₀) x₀<VAR>hf2 : ∀ᶠ (y : ℝ) in 𝓝 t₀, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y<VAR>a : ℝ<VAR>ha : a > 0<VAR>hf2' : ∀ y ∈ Metric.ball t₀ a, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y<VAR>hcont : ∀ A ∈ 𝓝 (↑(extChartAt I x₀) x₀), f ⁻¹' A ∈ 𝓝 t₀<VAR>hnhds : ∀ᶠ (x' : ℝ) in 𝓝 t₀, f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 x'<VAR>s : Set ℝ<VAR>hs : s ∈ 𝓝 t₀<VAR>haux : ∀ y ∈ s, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y ∧ f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 y<VAR>t : ℝ<VAR>ht : t ∈ s<VAR>xₜ : M := ↑(extChartAt I x₀).symm (f t)<VAR>h : HasDerivAt f ((tangentCoordChange I xₜ x₀ xₜ) (v xₜ)) t<VAR>hf3 : f t ∈ interior (extChartAt I x₀).target<VAR>hf3' : f t ∈ (extChartAt I x₀).target<VAR>hft1 : ↑(extChartAt I x₀).symm (f t) ∈ (extChartAt I x₀).source<VAR>hft2 : xₜ ∈ (extChartAt I xₜ).source<GOAL>HasFDerivWithinAt (↑(extChartAt I xₜ) ∘ ↑(extChartAt I x₀).symm) (tangentCoordChange I x₀ xₜ xₜ) (range ↑I) (f t)
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s✝ s' : Set ℝ<VAR>t₀ : ℝ<VAR>x₀ : M<VAR>hx : I.IsInteriorPoint x₀<VAR>left✝ : ContinuousAt (fun x => { proj := x, snd := v x }) x₀<VAR>hv : ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (range ↑I) (↑(extChartAt I x₀) x₀)<VAR>f : ℝ → E<VAR>hf1 : f t₀ = ↑(extChartAt I x₀) x₀<VAR>hf2 : ∀ᶠ (y : ℝ) in 𝓝 t₀, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y<VAR>a : ℝ<VAR>ha : a > 0<VAR>hf2' : ∀ y ∈ Metric.ball t₀ a, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y<VAR>hcont : ∀ A ∈ 𝓝 (↑(extChartAt I x₀) x₀), f ⁻¹' A ∈ 𝓝 t₀<VAR>hnhds : ∀ᶠ (x' : ℝ) in 𝓝 t₀, f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 x'<VAR>s : Set ℝ<VAR>hs : s ∈ 𝓝 t₀<VAR>haux : ∀ y ∈ s, HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y ∧ f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 y<VAR>t : ℝ<VAR>ht : t ∈ s<VAR>xₜ : M := ↑(extChartAt I x₀).symm (f t)<VAR>h : HasDerivAt f ((tangentCoordChange I xₜ x₀ xₜ) (v xₜ)) t<VAR>hf3 : f t ∈ interior (extChartAt I x₀).target<VAR>hf3' : f t ∈ (extChartAt I x₀).target<VAR>hft1 : ↑(extChartAt I x₀).symm (f t) ∈ (extChartAt I x₀).source<VAR>hft2 : xₜ ∈ (extChartAt I xₜ).source<GOAL>HasFDerivWithinAt (↑(extChartAt I xₜ) ∘ ↑(extChartAt I x₀).symm) (tangentCoordChange I x₀ xₜ xₜ) (range ↑I) (↑(extChartAt I x₀) (↑(extChartAt I x₀).symm (f t)))
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{?u.21309, u_1} C<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{?u.21316, u_2} D<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{?u.21323, u_3} E<VAR>M : Type u_4<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : HasShift C M<VAR>inst✝¹ : HasShift D M<VAR>inst✝ : HasShift E M<VAR>X Y Z T : C<VAR>a : M<VAR>f : ShiftedHom X Y a<VAR>m₀ : M<VAR>hm₀ : m₀ = 0<VAR>g : Y ⟶ Z<GOAL>m₀ + a = a
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{?u.21316, u_2} D<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{?u.21323, u_3} E<VAR>M : Type u_4<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : HasShift C M<VAR>inst✝¹ : HasShift D M<VAR>inst✝ : HasShift E M<VAR>X Y Z T : C<VAR>a : M<VAR>f : ShiftedHom X Y a<VAR>g : Y ⟶ Z<GOAL>f.comp (mk₀ 0 ⋯ g) ⋯ = f ≫ (shiftFunctor C a).map g
<VAR>num : Int<VAR>den : Nat<VAR>nz : den ≠ 0<GOAL>∃ d, d ≠ 0 ∧ num = (normalize num den nz).num * ↑d ∧ den = (normalize num den nz).den * d
<VAR>num : Int<VAR>den : Nat<VAR>nz : den ≠ 0<GOAL>num = (normalize num den nz).num * ↑(num.natAbs.gcd den) ∧ den = (normalize num den nz).den * num.natAbs.gcd den
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b : α<VAR>hs : {a}.Nontrivial<GOAL>False
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>δ : ℝ<VAR>f : (δ : ℝ) → 0 < δ → ι → ℝ<VAR>hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ<VAR>hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior s<VAR>H : Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 0)<GOAL>False
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>δ : ℝ<VAR>f : (δ : ℝ) → 0 < δ → ι → ℝ<VAR>hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ<VAR>hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior s<VAR>H : Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>ε : ℕ → ℝ<VAR>hε' : ∀ (n : ℕ), 0 < ε n<VAR>hε₀ : Tendsto ε atTop (𝓝[>] 0)<GOAL>False
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>δ : ℝ<VAR>f : (δ : ℝ) → 0 < δ → ι → ℝ<VAR>hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ<VAR>hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior s<VAR>H : Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>ε : ℕ → ℝ<VAR>hε' : ∀ (n : ℕ), 0 < ε n<VAR>hε₀ : Tendsto ε atTop (𝓝[>] 0)<GOAL>0 < ENNReal.ofReal (4⁻¹ ^ Fintype.card ι)
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>δ : ℝ<VAR>f : (δ : ℝ) → 0 < δ → ι → ℝ<VAR>hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ<VAR>hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior s<VAR>H : Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>ε : ℕ → ℝ<VAR>hε' : ∀ (n : ℕ), 0 < ε n<VAR>hε₀ : Tendsto ε atTop (𝓝[>] 0)<VAR>n : ℕ<GOAL>ENNReal.ofReal (4⁻¹ ^ Fintype.card ι) ≤ ((fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) ∘ ε) n