ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>e : C(X, Y)<VAR>he : ClosedEmbedding ⇑e<VAR>F : (X →ᵇ ℝ) → Y →ᵇ ℝ<VAR>hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3<VAR>hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖<VAR>g : ℕ → Y →ᵇ ℝ := fun n => (fun g => g + F (f - g.compContinuous e))^[n] 0<VAR>g0 : g 0 = 0<VAR>g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)<VAR>hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖<VAR>hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n<VAR>hg_cau : CauchySeq g<VAR>this : Tendsto (fun n => (g n).compContinuous e) atTop (𝓝 ((limUnder atTop g).compContinuous e))<GOAL>∃ g, ‖g‖ = ‖f‖ ∧ g.compContinuous e = f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>e : C(X, Y)<VAR>he : ClosedEmbedding ⇑e<VAR>F : (X →ᵇ ℝ) → Y →ᵇ ℝ<VAR>hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3<VAR>hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖<VAR>g : ℕ → Y →ᵇ ℝ := fun n => (fun g => g + F (f - g.compContinuous e))^[n] 0<VAR>g0 : g 0 = 0<VAR>g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)<VAR>hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖<VAR>hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n<VAR>hg_cau : CauchySeq g<VAR>this : Tendsto (fun n => (g n).compContinuous e) atTop (𝓝 ((limUnder atTop g).compContinuous e))<VAR>hge : (limUnder atTop g).compContinuous e = f<GOAL>∃ g, ‖g‖ = ‖f‖ ∧ g.compContinuous e = f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>e : C(X, Y)<VAR>he : ClosedEmbedding ⇑e<VAR>F : (X →ᵇ ℝ) → Y →ᵇ ℝ<VAR>hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3<VAR>hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖<VAR>g : ℕ → Y →ᵇ ℝ := fun n => (fun g => g + F (f - g.compContinuous e))^[n] 0<VAR>g0 : g 0 = 0<VAR>g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)<VAR>hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖<VAR>hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n<VAR>hg_cau : CauchySeq g<VAR>this : Tendsto (fun n => (g n).compContinuous e) atTop (𝓝 ((limUnder atTop g).compContinuous e))<VAR>hge : (limUnder atTop g).compContinuous e = f<GOAL>‖limUnder atTop g‖ ≤ ‖f‖
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>e : C(X, Y)<VAR>he : ClosedEmbedding ⇑e<VAR>F : (X →ᵇ ℝ) → Y →ᵇ ℝ<VAR>hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3<VAR>hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖<VAR>g : ℕ → Y →ᵇ ℝ := fun n => (fun g => g + F (f - g.compContinuous e))^[n] 0<VAR>g0 : g 0 = 0<VAR>g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)<VAR>hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖<VAR>hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n<VAR>hg_cau : CauchySeq g<VAR>this : Tendsto (fun n => (g n).compContinuous e) atTop (𝓝 ((limUnder atTop g).compContinuous e))<VAR>hge : (limUnder atTop g).compContinuous e = f<GOAL>‖f‖ ≤ ‖limUnder atTop g‖
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₀.toCompacts<GOAL>chaar K₀ K₀.toCompacts = 1
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₀.toCompacts<VAR>this : Continuous eval<GOAL>chaar K₀ K₀.toCompacts = 1
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₀.toCompacts<VAR>this : Continuous eval<GOAL>chaar K₀ ∈ eval ⁻¹' {1}
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₀.toCompacts<VAR>this : Continuous eval<GOAL>clPrehaar ↑K₀ ⊤ ⊆ eval ⁻¹' {1}
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₀.toCompacts<VAR>this : Continuous eval<GOAL>closure (prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen U ∧ 1 ∈ U}) ⊆ eval ⁻¹' {1}
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₀.toCompacts<VAR>this : Continuous eval<GOAL>prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen U ∧ 1 ∈ U} ⊆ eval ⁻¹' {1}
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₀.toCompacts<VAR>this : Continuous eval<GOAL>IsClosed (eval ⁻¹' {1})
<VAR>m n : ℕ<VAR>i : Fin n.succ<VAR>h : i ≠ Fin.last n<GOAL>↑((finRotate (n + 1)) i) = ↑i + 1
<VAR>m n : ℕ<VAR>i : Fin n.succ<VAR>h : i ≠ Fin.last n<GOAL>↑(i + 1) = ↑i + 1
<VAR>m n : ℕ<VAR>i : Fin n.succ<VAR>h : i ≠ Fin.last n<VAR>this : ↑i < n<GOAL>↑(i + 1) = ↑i + 1
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>α : Type u_4<VAR>β : Type u_5<VAR>f : R →+* S<VAR>x y : 𝕎 R<GOAL>mapFun (⇑f) (x + y) = mapFun (⇑f) x + mapFun (⇑f) y
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f g : R⟦X⟧<VAR>n✝ : ℕ<GOAL>(coeff R n✝) (f + g).derivativeFun = (coeff R n✝) (f.derivativeFun + g.derivativeFun)
<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>hv : ContMDiffAt I I.tangent 1 (fun x => { proj := x, snd := v x }) x₀<VAR>hx : I.IsInteriorPoint x₀<GOAL>∃ γ, γ t₀ = x₀ ∧ IsIntegralCurveAt γ v 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>hv : ContinuousAt (fun x => { proj := x, snd := v x }) x₀ ∧ 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>hx : I.IsInteriorPoint x₀<GOAL>∃ γ, γ t₀ = x₀ ∧ IsIntegralCurveAt γ v 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₀)<GOAL>∃ γ, γ t₀ = x₀ ∧ IsIntegralCurveAt γ v 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 : ∃ ε > 0, ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt f ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm) (f t)).2 t<GOAL>∃ γ, γ t₀ = x₀ ∧ IsIntegralCurveAt γ v 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<GOAL>∃ γ, γ t₀ = x₀ ∧ IsIntegralCurveAt γ v 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<GOAL>∃ γ, γ t₀ = x₀ ∧ IsIntegralCurveAt γ v 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 : ContinuousAt f t₀<GOAL>∃ γ, γ t₀ = x₀ ∧ IsIntegralCurveAt γ v 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₀<GOAL>∃ γ, γ t₀ = x₀ ∧ IsIntegralCurveAt γ v 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 : f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 t₀<GOAL>∃ γ, γ t₀ = x₀ ∧ IsIntegralCurveAt γ v 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'<GOAL>∃ γ, γ t₀ = x₀ ∧ IsIntegralCurveAt γ v 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<GOAL>∃ γ, γ t₀ = x₀ ∧ IsIntegralCurveAt γ v 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<GOAL>IsIntegralCurveOn (↑(extChartAt I x₀).symm ∘ f) v s
<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)<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 ((fderivWithin ℝ (↑(extChartAt I x₀) ∘ ↑(extChartAt I xₜ).symm) (range ↑I) (↑(extChartAt I xₜ) xₜ)) (v xₜ)) t<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<GOAL>HasMFDerivAt 𝓘(ℝ, ℝ) I (↑(extChartAt I x₀).symm ∘ f) t (ContinuousLinearMap.smulRight 1 (v ((↑(extChartAt I x₀).symm ∘ f) t)))