ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>F : Jᵒᵖ ⥤ C<VAR>c : Cone F<VAR>hc : IsLimit c<VAR>s : Cocone F.rightOp<VAR>m : (coconeRightOpOfCone c).pt ⟶ s.pt<VAR>w : ∀ (j : J), (coconeRightOpOfCone c).ι.app j ≫ m = s.ι.app j<VAR>j : Jᵒᵖ<GOAL>(m.unop ≫ c.π.app j).op = (((fun s => (hc.lift (coneOfCoconeRightOp s)).op) s).unop ≫ c.π.app j).op
<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>hγt₀ : I.IsInteriorPoint (γ t₀)<VAR>hv : ContMDiffAt I I.tangent 1 (fun x => { proj := x, snd := v x }) (γ t₀)<VAR>hγ : IsIntegralCurveAt γ v t₀<VAR>hγ' : IsIntegralCurveAt γ' v t₀<VAR>h : γ t₀ = γ' t₀<VAR>v' : E → E := fun x => (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x)) (v (↑(extChartAt I (γ t₀)).symm x))<VAR>hv' : v' = fun x => (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x)) (v (↑(extChartAt I (γ t₀)).symm x))<GOAL>γ =ᶠ[𝓝 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>hγt₀ : I.IsInteriorPoint (γ t₀)<VAR>hv : ContinuousAt (fun x => { proj := x, snd := v x }) (γ t₀) ∧ ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent { proj := γ t₀, snd := v (γ t₀) }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I (γ t₀)).symm) (range ↑I) (↑(extChartAt I (γ t₀)) (γ t₀))<VAR>hγ : IsIntegralCurveAt γ v t₀<VAR>hγ' : IsIntegralCurveAt γ' v t₀<VAR>h : γ t₀ = γ' t₀<VAR>v' : E → E := fun x => (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x)) (v (↑(extChartAt I (γ t₀)).symm x))<VAR>hv' : v' = fun x => (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x)) (v (↑(extChartAt I (γ t₀)).symm x))<GOAL>γ =ᶠ[𝓝 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>hγt₀ : I.IsInteriorPoint (γ t₀)<VAR>hγ : IsIntegralCurveAt γ v t₀<VAR>hγ' : IsIntegralCurveAt γ' v t₀<VAR>h : γ t₀ = γ' t₀<VAR>v' : E → E := fun x => (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x)) (v (↑(extChartAt I (γ t₀)).symm x))<VAR>hv' : v' = fun x => (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x)) (v (↑(extChartAt I (γ t₀)).symm x))<VAR>left✝ : ContinuousAt (fun x => { proj := x, snd := v x }) (γ t₀)<VAR>hv : ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent { proj := γ t₀, snd := v (γ t₀) }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I (γ t₀)).symm) (range ↑I) (↑(extChartAt I (γ t₀)) (γ t₀))<GOAL>γ =ᶠ[𝓝 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>hγt₀ : I.IsInteriorPoint (γ t₀)<VAR>hγ : IsIntegralCurveAt γ v t₀<VAR>hγ' : IsIntegralCurveAt γ' v t₀<VAR>h : γ t₀ = γ' t₀<VAR>v' : E → E := fun x => (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x)) (v (↑(extChartAt I (γ t₀)).symm x))<VAR>hv' : v' = fun x => (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x)) (v (↑(extChartAt I (γ t₀)).symm x))<VAR>left✝ : ContinuousAt (fun x => { proj := x, snd := v x }) (γ t₀)<VAR>hv : ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent { proj := γ t₀, snd := v (γ t₀) }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I (γ t₀)).symm) (range ↑I) (↑(extChartAt I (γ t₀)) (γ t₀))<VAR>K : NNReal<VAR>s : Set E<VAR>hs : s ∈ 𝓝 (↑(extChartAt I (γ t₀)) (γ t₀))<VAR>hlip : LipschitzOnWith K v' s<GOAL>γ =ᶠ[𝓝 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>hγt₀ : I.IsInteriorPoint (γ t₀)<VAR>hγ : IsIntegralCurveAt γ v t₀<VAR>hγ' : IsIntegralCurveAt γ' v t₀<VAR>h : γ t₀ = γ' t₀<VAR>v' : E → E := fun x => (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x)) (v (↑(extChartAt I (γ t₀)).symm x))<VAR>hv' : v' = fun x => (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x)) (v (↑(extChartAt I (γ t₀)).symm x))<VAR>left✝ : ContinuousAt (fun x => { proj := x, snd := v x }) (γ t₀)<VAR>hv : ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent { proj := γ t₀, snd := v (γ t₀) }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I (γ t₀)).symm) (range ↑I) (↑(extChartAt I (γ t₀)) (γ t₀))<VAR>K : NNReal<VAR>s : Set E<VAR>hs : s ∈ 𝓝 (↑(extChartAt I (γ t₀)) (γ t₀))<VAR>hlip✝ : LipschitzOnWith K v' s<VAR>hlip : ∀ (t : ℝ), LipschitzOnWith K ((fun x => v') t) ((fun x => s) t)<GOAL>γ =ᶠ[𝓝 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>hγt₀ : I.IsInteriorPoint (γ t₀)<VAR>hγ : IsIntegralCurveAt γ v t₀<VAR>hγ' : IsIntegralCurveAt γ' v t₀<VAR>h : γ t₀ = γ' t₀<VAR>v' : E → E := fun x => (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x)) (v (↑(extChartAt I (γ t₀)).symm x))<VAR>hv' : v' = fun x => (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x)) (v (↑(extChartAt I (γ t₀)).symm x))<VAR>left✝ : ContinuousAt (fun x => { proj := x, snd := v x }) (γ t₀)<VAR>hv : ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent { proj := γ t₀, snd := v (γ t₀) }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I (γ t₀)).symm) (range ↑I) (↑(extChartAt I (γ t₀)) (γ t₀))<VAR>K : NNReal<VAR>s : Set E<VAR>hs : s ∈ 𝓝 (↑(extChartAt I (γ t₀)) (γ t₀))<VAR>hlip✝ : LipschitzOnWith K v' s<VAR>hlip : ∀ (t : ℝ), LipschitzOnWith K ((fun x => v') t) ((fun x => s) t)<VAR>hsrc : ∀ {g : ℝ → M}, IsIntegralCurveAt g v t₀ → ∀ᶠ (t : ℝ) in 𝓝 t₀, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t<GOAL>γ =ᶠ[𝓝 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>hγt₀ : I.IsInteriorPoint (γ t₀)<VAR>hγ : IsIntegralCurveAt γ v t₀<VAR>hγ' : IsIntegralCurveAt γ' v t₀<VAR>h : γ t₀ = γ' t₀<VAR>v' : E → E := fun x => (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x)) (v (↑(extChartAt I (γ t₀)).symm x))<VAR>hv' : v' = fun x => (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x)) (v (↑(extChartAt I (γ t₀)).symm x))<VAR>left✝ : ContinuousAt (fun x => { proj := x, snd := v x }) (γ t₀)<VAR>hv : ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent { proj := γ t₀, snd := v (γ t₀) }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I (γ t₀)).symm) (range ↑I) (↑(extChartAt I (γ t₀)) (γ t₀))<VAR>K : NNReal<VAR>s : Set E<VAR>hs : s ∈ 𝓝 (↑(extChartAt I (γ t₀)) (γ t₀))<VAR>hlip✝ : LipschitzOnWith K v' s<VAR>hlip : ∀ (t : ℝ), LipschitzOnWith K ((fun x => v') t) ((fun x => s) t)<VAR>hsrc : ∀ {g : ℝ → M}, IsIntegralCurveAt g v t₀ → ∀ᶠ (t : ℝ) in 𝓝 t₀, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t<VAR>hmem : ∀ {g : ℝ → M} {t : ℝ}, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t → g t ∈ (extChartAt I (g t₀)).source<GOAL>γ =ᶠ[𝓝 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>hγt₀ : I.IsInteriorPoint (γ t₀)<VAR>hγ : IsIntegralCurveAt γ v t₀<VAR>hγ' : IsIntegralCurveAt γ' v t₀<VAR>h : γ t₀ = γ' t₀<VAR>v' : E → E := fun x => (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x)) (v (↑(extChartAt I (γ t₀)).symm x))<VAR>hv' : v' = fun x => (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x)) (v (↑(extChartAt I (γ t₀)).symm x))<VAR>left✝ : ContinuousAt (fun x => { proj := x, snd := v x }) (γ t₀)<VAR>hv : ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent { proj := γ t₀, snd := v (γ t₀) }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I (γ t₀)).symm) (range ↑I) (↑(extChartAt I (γ t₀)) (γ t₀))<VAR>K : NNReal<VAR>s : Set E<VAR>hs : s ∈ 𝓝 (↑(extChartAt I (γ t₀)) (γ t₀))<VAR>hlip✝ : LipschitzOnWith K v' s<VAR>hlip : ∀ (t : ℝ), LipschitzOnWith K ((fun x => v') t) ((fun x => s) t)<VAR>hsrc : ∀ {g : ℝ → M}, IsIntegralCurveAt g v t₀ → ∀ᶠ (t : ℝ) in 𝓝 t₀, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t<VAR>hmem : ∀ {g : ℝ → M} {t : ℝ}, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t → g t ∈ (extChartAt I (g t₀)).source<VAR>hdrv : ∀ {g : ℝ → M}, IsIntegralCurveAt g v t₀ → γ t₀ = g t₀ → ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt (↑(extChartAt I (g t₀)) ∘ g) ((fun x => v') t ((↑(extChartAt I (g t₀)) ∘ g) t)) t ∧ (↑(extChartAt I (g t₀)) ∘ g) t ∈ (fun x => s) t<GOAL>γ =ᶠ[𝓝 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>hγt₀ : I.IsInteriorPoint (γ t₀)<VAR>hγ : IsIntegralCurveAt γ v t₀<VAR>hγ' : IsIntegralCurveAt γ' v t₀<VAR>h : γ t₀ = γ' t₀<VAR>v' : E → E := fun x => (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x)) (v (↑(extChartAt I (γ t₀)).symm x))<VAR>hv' : v' = fun x => (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x)) (v (↑(extChartAt I (γ t₀)).symm x))<VAR>left✝ : ContinuousAt (fun x => { proj := x, snd := v x }) (γ t₀)<VAR>hv : ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent { proj := γ t₀, snd := v (γ t₀) }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I (γ t₀)).symm) (range ↑I) (↑(extChartAt I (γ t₀)) (γ t₀))<VAR>K : NNReal<VAR>s : Set E<VAR>hs : s ∈ 𝓝 (↑(extChartAt I (γ t₀)) (γ t₀))<VAR>hlip✝ : LipschitzOnWith K v' s<VAR>hlip : ∀ (t : ℝ), LipschitzOnWith K ((fun x => v') t) ((fun x => s) t)<VAR>hsrc : ∀ {g : ℝ → M}, IsIntegralCurveAt g v t₀ → ∀ᶠ (t : ℝ) in 𝓝 t₀, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t<VAR>hmem : ∀ {g : ℝ → M} {t : ℝ}, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t → g t ∈ (extChartAt I (g t₀)).source<VAR>hdrv : ∀ {g : ℝ → M}, IsIntegralCurveAt g v t₀ → γ t₀ = g t₀ → ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt (↑(extChartAt I (g t₀)) ∘ g) ((fun x => v') t ((↑(extChartAt I (g t₀)) ∘ g) t)) t ∧ (↑(extChartAt I (g t₀)) ∘ g) t ∈ (fun x => s) t<VAR>heq : ∀ {g : ℝ → M}, IsIntegralCurveAt g v t₀ → g =ᶠ[𝓝 t₀] ↑(extChartAt I (g t₀)).symm ∘ ↑(extChartAt I (g t₀)) ∘ g<GOAL>γ =ᶠ[𝓝 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>hγt₀ : I.IsInteriorPoint (γ t₀)<VAR>hγ : IsIntegralCurveAt γ v t₀<VAR>hγ' : IsIntegralCurveAt γ' v t₀<VAR>h : γ t₀ = γ' t₀<VAR>v' : E → E := fun x => (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x)) (v (↑(extChartAt I (γ t₀)).symm x))<VAR>hv' : v' = fun x => (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x)) (v (↑(extChartAt I (γ t₀)).symm x))<VAR>left✝ : ContinuousAt (fun x => { proj := x, snd := v x }) (γ t₀)<VAR>hv : ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent { proj := γ t₀, snd := v (γ t₀) }) ∘ (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I (γ t₀)).symm) (range ↑I) (↑(extChartAt I (γ t₀)) (γ t₀))<VAR>K : NNReal<VAR>s : Set E<VAR>hs : s ∈ 𝓝 (↑(extChartAt I (γ t₀)) (γ t₀))<VAR>hlip✝ : LipschitzOnWith K v' s<VAR>hlip : ∀ (t : ℝ), LipschitzOnWith K ((fun x => v') t) ((fun x => s) t)<VAR>hsrc : ∀ {g : ℝ → M}, IsIntegralCurveAt g v t₀ → ∀ᶠ (t : ℝ) in 𝓝 t₀, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t<VAR>hmem : ∀ {g : ℝ → M} {t : ℝ}, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t → g t ∈ (extChartAt I (g t₀)).source<VAR>hdrv : ∀ {g : ℝ → M}, IsIntegralCurveAt g v t₀ → γ t₀ = g t₀ → ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt (↑(extChartAt I (g t₀)) ∘ g) ((fun x => v') t ((↑(extChartAt I (g t₀)) ∘ g) t)) t ∧ (↑(extChartAt I (g t₀)) ∘ g) t ∈ (fun x => s) t<VAR>heq : ∀ {g : ℝ → M}, IsIntegralCurveAt g v t₀ → g =ᶠ[𝓝 t₀] ↑(extChartAt I (g t₀)).symm ∘ ↑(extChartAt I (g t₀)) ∘ g<GOAL>↑(extChartAt I (γ t₀)) ∘ γ =ᶠ[𝓝 t₀] ↑(extChartAt I (γ' t₀)) ∘ γ'
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Preadditive C<VAR>X Y : C<VAR>inst✝ : HasBinaryBiproduct X Y<GOAL>fst ≫ inl + snd ≫ inr = 𝟙 (X ⊞ Y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>l₁ l₂ : ι → 𝕜<VAR>s : Finset ι<GOAL>⟪∑ i ∈ s, l₁ i • v i, ∑ i ∈ s, l₂ i • v i⟫_𝕜 = ∑ i ∈ s, (starRingEnd 𝕜) (l₁ i) * l₂ i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>l₁ l₂ : ι → 𝕜<VAR>s : Finset ι<GOAL>∑ x ∈ s, (starRingEnd 𝕜) (l₁ x) * ⟪v x, ∑ i ∈ s, l₂ i • v i⟫_𝕜 = ∑ i ∈ s, (starRingEnd 𝕜) (l₁ i) * l₂ i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>l₁ l₂ : ι → 𝕜<VAR>s : Finset ι<VAR>i : ι<VAR>hi : i ∈ s<GOAL>(starRingEnd 𝕜) (l₁ i) * ⟪v i, ∑ i ∈ s, l₂ i • v i⟫_𝕜 = (starRingEnd 𝕜) (l₁ i) * l₂ i
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : IsAlgClosed k<VAR>n : ℕ<VAR>a₁ a₂ : 𝕎 k<VAR>bs : Fin (n + 1) → k<VAR>ha₁ : a₁.coeff 0 ≠ 0<VAR>ha₂ : a₂.coeff 0 ≠ 0<GOAL>succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) + a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) + nthRemainder p n (fun v => bs v ^ p) (truncateFun (n + 1) a₁) = succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) + a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) + nthRemainder p n bs (truncateFun (n + 1) a₂)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : IsAlgClosed k<VAR>n : ℕ<VAR>a₁ a₂ : 𝕎 k<VAR>bs : Fin (n + 1) → k<VAR>ha₁ : a₁.coeff 0 ≠ 0<VAR>ha₂ : a₂.coeff 0 ≠ 0<GOAL>succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) + a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) + nthRemainder p n (fun v => bs v ^ p) (truncateFun (n + 1) a₁) - (succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) + a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) + nthRemainder p n bs (truncateFun (n + 1) a₂)) = 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : IsAlgClosed k<VAR>n : ℕ<VAR>a₁ a₂ : 𝕎 k<VAR>bs : Fin (n + 1) → k<VAR>ha₁ : a₁.coeff 0 ≠ 0<VAR>ha₂ : a₂.coeff 0 ≠ 0<VAR>this : (succNthDefiningPoly p n a₁ a₂ bs).IsRoot (succNthVal p n a₁ a₂ bs ha₁ ha₂)<GOAL>succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) + a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) + nthRemainder p n (fun v => bs v ^ p) (truncateFun (n + 1) a₁) - (succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) + a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) + nthRemainder p n bs (truncateFun (n + 1) a₂)) = 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : IsAlgClosed k<VAR>n : ℕ<VAR>a₁ a₂ : 𝕎 k<VAR>bs : Fin (n + 1) → k<VAR>ha₁ : a₁.coeff 0 ≠ 0<VAR>ha₂ : a₂.coeff 0 ≠ 0<VAR>this : succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) - succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) + (a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) + nthRemainder p n (fun v => bs v ^ p) (truncateFun (n + 1) a₁) - a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) - nthRemainder p n bs (truncateFun (n + 1) a₂)) = 0<GOAL>succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) + a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) + nthRemainder p n (fun v => bs v ^ p) (truncateFun (n + 1) a₁) - (succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) + a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) + nthRemainder p n bs (truncateFun (n + 1) a₂)) = 0
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝² : EMetricSpace X<VAR>inst✝¹ : EMetricSpace Y<VAR>inst✝ : SecondCountableTopology X<VAR>s : Set X<GOAL>⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets = dimH s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝² : EMetricSpace X<VAR>inst✝¹ : EMetricSpace Y<VAR>inst✝ : SecondCountableTopology X<VAR>s : Set X<VAR>x : X<VAR>x✝ : x ∈ s<GOAL>limsup dimH (𝓝[s] x).smallSets ≤ dimH s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝² : EMetricSpace X<VAR>inst✝¹ : EMetricSpace Y<VAR>inst✝ : SecondCountableTopology X<VAR>s : Set X<GOAL>dimH s ≤ ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>inst✝ : Finite R M<GOAL>∃ n f, Surjective ⇑f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>inst✝ : Finite R M<VAR>n : ℕ<VAR>s : Fin n → M<VAR>hs : span R (range s) = ⊤<GOAL>∃ n f, Surjective ⇑f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>inst✝ : Finite R M<VAR>n : ℕ<VAR>s : Fin n → M<VAR>hs : span R (range s) = ⊤<GOAL>Surjective ⇑(((Pi.basisFun R (Fin n)).constr ℕ) s)
<VAR>xl xr : Type u<VAR>x y z : PGame<VAR>h₁ : x ≤ y<VAR>h₂ : y ⧏ z<GOAL>x ⧏ z
<VAR>xl xr : Type u<VAR>x y z : PGame<VAR>h₁ : x ≤ y<VAR>h₂ : ¬z ≤ y<GOAL>¬z ≤ x
<VAR>Ω : Type u_1<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁴ : SMul R ℝ≥0<VAR>inst✝³ : SMul R ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝ : TopologicalSpace Ω<VAR>μ : FiniteMeasure Ω<GOAL>μ.testAgainstNN 1 = μ.mass
<VAR>Ω : Type u_1<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁴ : SMul R ℝ≥0<VAR>inst✝³ : SMul R ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝ : TopologicalSpace Ω<VAR>μ : FiniteMeasure Ω<GOAL>(↑μ univ).toNNReal = μ.mass
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{?u.132220, u_2} D<VAR>inst✝¹ : Category.{?u.132224, u_3} E<VAR>inst✝ : Preregular C<VAR>W : C<GOAL>IsSheaf (regularTopology C) (yoneda.obj W)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{?u.132220, u_2} D<VAR>inst✝¹ : Category.{?u.132224, u_3} E<VAR>inst✝ : Preregular C<VAR>W : C<GOAL>∀ {X : C}, ∀ R ∈ (regularCoverage C).covering X, IsSheafFor (yoneda.obj W) R
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{?u.132220, u_2} D<VAR>inst✝¹ : Category.{?u.132224, u_3} E<VAR>inst✝ : Preregular C<VAR>W X : C<VAR>S : Presieve X<VAR>w✝ : C<VAR>hS : ∃ f, (S = ofArrows (fun x => w✝) fun x => f) ∧ EffectiveEpi f<VAR>this : S.regular<GOAL>IsSheafFor (yoneda.obj W) S
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{?u.132220, u_2} D<VAR>inst✝¹ : Category.{?u.132224, u_3} E<VAR>inst✝ : Preregular C<VAR>W X w✝ Y : C<VAR>f : Y ⟶ X<VAR>hf : EffectiveEpi f<VAR>hS : ∃ f_1, ((ofArrows (fun x => Y) fun x => f) = ofArrows (fun x => w✝) fun x => f_1) ∧ EffectiveEpi f_1<VAR>this : (ofArrows (fun x => Y) fun x => f).regular<GOAL>IsSheafFor (yoneda.obj W) (ofArrows (fun x => Y) fun x => f)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{?u.132220, u_2} D<VAR>inst✝¹ : Category.{?u.132224, u_3} E<VAR>inst✝ : Preregular C<VAR>W X w✝ Y : C<VAR>f : Y ⟶ X<VAR>hf : EffectiveEpi f<VAR>hS : ∃ f_1, ((ofArrows (fun x => Y) fun x => f) = ofArrows (fun x => w✝) fun x => f_1) ∧ EffectiveEpi f_1<VAR>this : (ofArrows (fun x => Y) fun x => f).regular<VAR>h_colim : IsColimit (Sieve.generateSingleton f).arrows.cocone<GOAL>IsSheafFor (yoneda.obj W) (ofArrows (fun x => Y) fun x => f)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{?u.132220, u_2} D<VAR>inst✝¹ : Category.{?u.132224, u_3} E<VAR>inst✝ : Preregular C<VAR>W X w✝ Y : C<VAR>f : Y ⟶ X<VAR>hf : EffectiveEpi f<VAR>hS : ∃ f_1, ((ofArrows (fun x => Y) fun x => f) = ofArrows (fun x => w✝) fun x => f_1) ∧ EffectiveEpi f_1<VAR>this : (ofArrows (fun x => Y) fun x => f).regular<VAR>h_colim : IsColimit (Sieve.generate (ofArrows (fun x => Y) fun x => f)).arrows.cocone<GOAL>IsSheafFor (yoneda.obj W) (ofArrows (fun x => Y) fun x => f)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{?u.132220, u_2} D<VAR>inst✝¹ : Category.{?u.132224, u_3} E<VAR>inst✝ : Preregular C<VAR>W X w✝ Y : C<VAR>f : Y ⟶ X<VAR>hf : EffectiveEpi f<VAR>hS : ∃ f_1, ((ofArrows (fun x => Y) fun x => f) = ofArrows (fun x => w✝) fun x => f_1) ∧ EffectiveEpi f_1<VAR>this : (ofArrows (fun x => Y) fun x => f).regular<VAR>h_colim : IsColimit (Sieve.generate (ofArrows (fun x => Y) fun x => f)).arrows.cocone<VAR>x : FamilyOfElements (yoneda.obj W) (ofArrows (fun x => Y) fun x => f)<VAR>hx : x.Compatible<VAR>x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows (fun x => Y) fun x => f)).arrows := x.sieveExtend<GOAL>∃! t, x.IsAmalgamation t