ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>p : ℕ → Prop<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>N : ℕ → ℕ<VAR>hN : ∀ k < n, ∀ b ≥ N k, p (n * b + k)<VAR>b : ℕ<VAR>hb : b ≥ (Finset.range n).sup fun x => n * N x<VAR>hlt : b % n < n<GOAL>n * N (b % n) ≤ b
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : Semiring R<VAR>φ : ι → Type u_3<VAR>inst✝² : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝¹ : (i : ι) → Module R (φ i)<VAR>inst✝ : DecidableEq ι<VAR>I : Finset ι<VAR>J : Set ι<VAR>hu : univ ⊆ ↑I ∪ J<VAR>b : (i : ι) → φ i<VAR>hb : b ∈ ⨅ i ∈ J, ker (proj i)<GOAL>b ∈ ⨆ i ∈ I, range (stdBasis R φ i)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : Semiring R<VAR>φ : ι → Type u_3<VAR>inst✝² : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝¹ : (i : ι) → Module R (φ i)<VAR>inst✝ : DecidableEq ι<VAR>I : Finset ι<VAR>J : Set ι<VAR>hu : univ ⊆ ↑I ∪ J<VAR>b : (i : ι) → φ i<VAR>hb : ∀ i ∈ J, b i = 0<GOAL>b ∈ ⨆ i ∈ I, range (stdBasis R φ i)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : Semiring R<VAR>φ : ι → Type u_3<VAR>inst✝² : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝¹ : (i : ι) → Module R (φ i)<VAR>inst✝ : DecidableEq ι<VAR>I : Finset ι<VAR>J : Set ι<VAR>hu : univ ⊆ ↑I ∪ J<VAR>b : (i : ι) → φ i<VAR>hb : ∀ i ∈ J, b i = 0<GOAL>∑ i ∈ I, (stdBasis R φ i) (b i) ∈ ⨆ i ∈ I, range (stdBasis R φ i)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>g : β → γ<VAR>hg : UniformInducing g<VAR>f : α → β<GOAL>UniformInducing (g ∘ f) ↔ UniformInducing f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>g : β → γ<VAR>hg : UniformInducing g<VAR>f : α → β<VAR>h : UniformInducing (g ∘ f)<GOAL>UniformInducing f
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>s : Multiset α<GOAL>filter p s + filter (fun a => ¬p a) s = s
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>s : Multiset α<GOAL>s + 0 = s
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>s : Multiset α<GOAL>∀ a ∈ s, ¬(p a ∧ ¬p a)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>s : Multiset α<GOAL>∀ a ∈ s, p a ∨ ¬p a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : UniformSpace β<VAR>F✝ : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace γ<VAR>x : α<VAR>U : Set α<VAR>hU : U ∈ 𝓝 x<VAR>F : α → β → γ<VAR>hF : UniformContinuousOn (↿F) (U ×ˢ univ)<GOAL>TendstoUniformly F (F x) (𝓝 x)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : NonUnitalNormedRing A<VAR>inst✝³ : NormedSpace 𝕜 A<VAR>inst✝² : IsScalarTower 𝕜 A A<VAR>inst✝¹ : SMulCommClass 𝕜 A A<VAR>inst✝ : RegularNormedAlgebra 𝕜 A<GOAL>LipschitzWith 2 ⇑(addEquiv 𝕜 A)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : NonUnitalNormedRing A<VAR>inst✝³ : NormedSpace 𝕜 A<VAR>inst✝² : IsScalarTower 𝕜 A A<VAR>inst✝¹ : SMulCommClass 𝕜 A A<VAR>inst✝ : RegularNormedAlgebra 𝕜 A<GOAL>LipschitzWith 2.toNNReal ⇑(addEquiv 𝕜 A)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : NonUnitalNormedRing A<VAR>inst✝³ : NormedSpace 𝕜 A<VAR>inst✝² : IsScalarTower 𝕜 A A<VAR>inst✝¹ : SMulCommClass 𝕜 A A<VAR>inst✝ : RegularNormedAlgebra 𝕜 A<VAR>x : Unitization 𝕜 A<GOAL>‖(addEquiv 𝕜 A) x‖ ≤ 2 * ‖x‖
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : NonUnitalNormedRing A<VAR>inst✝³ : NormedSpace 𝕜 A<VAR>inst✝² : IsScalarTower 𝕜 A A<VAR>inst✝¹ : SMulCommClass 𝕜 A A<VAR>inst✝ : RegularNormedAlgebra 𝕜 A<VAR>x : Unitization 𝕜 A<GOAL>max ‖((addEquiv 𝕜 A) x).1‖ ‖((addEquiv 𝕜 A) x).2‖ ≤ 2 * (‖x.fst‖ ⊔ ‖(algebraMap 𝕜 (A →L[𝕜] A)) x.fst + (mul 𝕜 A) x.snd‖)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : NonUnitalNormedRing A<VAR>inst✝³ : NormedSpace 𝕜 A<VAR>inst✝² : IsScalarTower 𝕜 A A<VAR>inst✝¹ : SMulCommClass 𝕜 A A<VAR>inst✝ : RegularNormedAlgebra 𝕜 A<VAR>x : Unitization 𝕜 A<GOAL>‖((addEquiv 𝕜 A) x).1‖ ≤ 2 * (‖x.fst‖ ⊔ ‖(algebraMap 𝕜 (A →L[𝕜] A)) x.fst + (mul 𝕜 A) x.snd‖)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : NonUnitalNormedRing A<VAR>inst✝³ : NormedSpace 𝕜 A<VAR>inst✝² : IsScalarTower 𝕜 A A<VAR>inst✝¹ : SMulCommClass 𝕜 A A<VAR>inst✝ : RegularNormedAlgebra 𝕜 A<VAR>x : Unitization 𝕜 A<GOAL>‖((addEquiv 𝕜 A) x).2‖ ≤ 2 * (‖x.fst‖ ⊔ ‖(algebraMap 𝕜 (A →L[𝕜] A)) x.fst + (mul 𝕜 A) x.snd‖)
<VAR>r r₁ r₂ : ℝ≥0<VAR>x y : ℝ<VAR>ι : Sort u_1<VAR>s : ι → ℝ≥0<GOAL>↑(⨅ i, s i) = ⨅ i, ↑(s i)
<VAR>r r₁ r₂ : ℝ≥0<VAR>x y : ℝ<VAR>ι : Sort u_1<VAR>s : ι → ℝ≥0<GOAL>sInf (Set.range (toReal ∘ fun i => s i)) = sInf (Set.range fun i => ↑(s i))
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>w' : InfinitePlace K<VAR>e : { w // w ≠ w' } ≃ Fin (rank K)<GOAL>regulator K = |(Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(fundSystem K (e i))))).det|
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>w' : InfinitePlace K<VAR>e : { w // w ≠ w' } ≃ Fin (rank K)<VAR>e' : { w // w ≠ w₀ } ≃ Fin (rank K) := Fintype.equivOfCardEq ⋯<GOAL>regulator K = |(Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(fundSystem K (e i))))).det|
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>w' : InfinitePlace K<VAR>e : { w // w ≠ w' } ≃ Fin (rank K)<VAR>e' : { w // w ≠ w₀ } ≃ Fin (rank K) := Fintype.equivOfCardEq ⋯<GOAL>|(Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(Additive.toMul (fundSystem K (e' i)))))).det| = |(Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(fundSystem K (e i))))).det|
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Finset α<GOAL>s.toList.Nodup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Finset α<GOAL>s.val.Nodup
<VAR>m n✝ n : ℕ<VAR>hn : Odd n<VAR>a : ZMod n<VAR>ha : a ≠ 0<GOAL>a ≠ -a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f : α → β<VAR>x : α<GOAL>Tendsto (fun M => {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f : α → β<VAR>x : α<VAR>n : ℕ<VAR>hn : n ≥ ⌈↑‖f x‖₊⌉₊ + 1<GOAL>{x | ↑n ≤ ↑‖f x‖₊}.indicator f x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f : α → β<VAR>x : α<VAR>n : ℕ<VAR>hn : n ≥ ⌈↑‖f x‖₊⌉₊ + 1<GOAL>x ∉ {x | ↑n ≤ ↑‖f x‖₊}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f : α → β<VAR>x : α<VAR>n : ℕ<VAR>hn : n ≥ ⌈↑‖f x‖₊⌉₊ + 1<GOAL>↑‖f x‖₊ < ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f : α → β<VAR>x : α<VAR>n : ℕ<VAR>hn : n ≥ ⌈↑‖f x‖₊⌉₊ + 1<GOAL>↑⌈↑‖f x‖₊⌉₊ < ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f : α → β<VAR>x : α<VAR>n : ℕ<VAR>hn : n ≥ ⌈↑‖f x‖₊⌉₊ + 1<GOAL>↑⌈↑‖f x‖₊⌉₊ + 1 ≤ ↑n
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝³ : Monoid N<VAR>hnontriv : Nontrivial ι<VAR>G : Type u_4<VAR>inst✝² : Group G<VAR>H : ι → Type u_5<VAR>inst✝¹ : (i : ι) → Group (H i)<VAR>f : (i : ι) → H i →* G<VAR>hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)<VAR>α : Type u_6<VAR>inst✝ : MulAction G α<VAR>X : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i<VAR>i : ι<VAR>w : NeWord H i i<GOAL>(lift f) w.prod ≠ 1
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝³ : Monoid N<VAR>hnontriv : Nontrivial ι<VAR>G : Type u_4<VAR>inst✝² : Group G<VAR>H : ι → Type u_5<VAR>inst✝¹ : (i : ι) → Group (H i)<VAR>f : (i : ι) → H i →* G<VAR>hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)<VAR>α : Type u_6<VAR>inst✝ : MulAction G α<VAR>X : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i<VAR>i : ι<VAR>w : NeWord H i i<VAR>k : ι<VAR>hk : k ≠ i<GOAL>(lift f) w.prod ≠ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f : ι → α<VAR>s t : Set α<GOAL>⊤ ≤ range Sum.inl ⊔ range Sum.inr
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>s t r' s' t' : R<GOAL>(if _hr : 0 = 0 then (r', s', t') else let q := r' / 0; let_fun x := ⋯; xgcdAux (r' % 0) (s' - q * s) (t' - q * t) 0 s t) = (r', s', t')
<VAR>α : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>x : α<VAR>y : β<VAR>f : α ≃ β<GOAL>f x = y ↔ x = f.symm y
<VAR>α : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>x : α<VAR>y : β<VAR>f : α ≃ β<GOAL>f x = f (f.symm y) ↔ x = f.symm y
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : MonoidWithZero M₀<VAR>u : M₀ˣ<VAR>a : M₀<VAR>h : ↑u * a = 0<GOAL>a = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν✝ : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Measurable fun x => κ.densityProcess ν n a x s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν✝ : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Measurable fun x => (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<GOAL>TensorProduct.comm R ↥⊥ ↥M ≪≫ₗ M.rTensorOne = M.lTensorOne
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>r : ↥⊥<VAR>m : ↥M<GOAL>↑(TensorProduct.comm R ↥⊥ ↥M ≪≫ₗ M.rTensorOne) (r ⊗ₜ[R] m) = ↑M.lTensorOne (r ⊗ₜ[R] m)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>r : ↥⊥<VAR>m : ↥M<VAR>x : R<VAR>h : (algebraMap R S) x = ↑r<GOAL>↑(TensorProduct.comm R ↥⊥ ↥M ≪≫ₗ M.rTensorOne) (r ⊗ₜ[R] m) = ↑M.lTensorOne (r ⊗ₜ[R] m)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>r : ↥⊥<VAR>m : ↥M<VAR>x : R<VAR>h : (algebraMap R ↥⊥) x = r<GOAL>↑(TensorProduct.comm R ↥⊥ ↥M ≪≫ₗ M.rTensorOne) (r ⊗ₜ[R] m) = ↑M.lTensorOne (r ⊗ₜ[R] m)
<VAR>a : ℤ<VAR>p : ℕ<VAR>pp : Fact (Nat.Prime p)<GOAL>↑a = 0 ↔ a.gcd ↑p ≠ 1
<VAR>s : Set ℤ<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>b : ℤ<VAR>Hb : ∀ z ∈ s, z ≤ b<VAR>Hinh : ∃ z, z ∈ s<VAR>this : s.Nonempty ∧ BddAbove s<GOAL>sSup s = ↑(b.greatestOfBdd Hb Hinh)
<VAR>s : Set ℤ<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>b : ℤ<VAR>Hb : ∀ z ∈ s, z ≤ b<VAR>Hinh : ∃ z, z ∈ s<VAR>this : s.Nonempty ∧ BddAbove s<GOAL>↑((Classical.choose ⋯).greatestOfBdd ⋯ ⋯) = ↑(b.greatestOfBdd Hb Hinh)
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>x y : α<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>x ~ᵤ y ↔ normalizedFactors x = normalizedFactors y
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>x y : α<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h : x ~ᵤ y<GOAL>normalizedFactors x = normalizedFactors y
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>x y : α<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h : x ~ᵤ y<GOAL>x ∣ y
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>x y : α<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h : x ~ᵤ y<GOAL>x ≠ 0
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>x y : α<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h : x ~ᵤ y<GOAL>y ≠ 0
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>x y : α<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h : x ~ᵤ y<GOAL>y ∣ x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>γ : Path x y<VAR>f : Y → Path x y<VAR>g : Y → Path y z<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous fun t => (f t).trans (g t)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>γ : Path x y<VAR>f : Y → Path x y<VAR>g : Y → Path y z<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous ↿fun t => (f t).trans (g t)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h : HasFDerivWithinAt f f' s x<VAR>α : Type u_6<VAR>l : Filter α<VAR>c : α → 𝕜<VAR>d : α → E<VAR>v : E<VAR>dtop : ∀ᶠ (n : α) in l, x + d n ∈ s<VAR>clim : Tendsto (fun n => ‖c n‖) l atTop<VAR>cdlim : Tendsto (fun n => c n • d n) l (𝓝 v)<VAR>tendsto_arg : Tendsto (fun n => x + d n) l (𝓝[s] x)<GOAL>Tendsto (fun n => c n • (f (x + d n) - f x)) l (𝓝 (f' v))
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h : HasFDerivWithinAt f f' s x<VAR>α : Type u_6<VAR>l : Filter α<VAR>c : α → 𝕜<VAR>d : α → E<VAR>v : E<VAR>dtop : ∀ᶠ (n : α) in l, x + d n ∈ s<VAR>clim : Tendsto (fun n => ‖c n‖) l atTop<VAR>cdlim : Tendsto (fun n => c n • d n) l (𝓝 v)<VAR>tendsto_arg : Tendsto (fun n => x + d n) l (𝓝[s] x)<VAR>this : (fun y => f y - f x - f' (y - x)) =o[𝓝[s] x] fun y => y - x<GOAL>Tendsto (fun n => c n • (f (x + d n) - f x)) l (𝓝 (f' v))
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h : HasFDerivWithinAt f f' s x<VAR>α : Type u_6<VAR>l : Filter α<VAR>c : α → 𝕜<VAR>d : α → E<VAR>v : E<VAR>dtop : ∀ᶠ (n : α) in l, x + d n ∈ s<VAR>clim : Tendsto (fun n => ‖c n‖) l atTop<VAR>cdlim : Tendsto (fun n => c n • d n) l (𝓝 v)<VAR>tendsto_arg : Tendsto (fun n => x + d n) l (𝓝[s] x)<VAR>this✝ : (fun y => f y - f x - f' (y - x)) =o[𝓝[s] x] fun y => y - x<VAR>this : (fun n => f (x + d n) - f x - f' (x + d n - x)) =o[l] fun n => x + d n - x<GOAL>Tendsto (fun n => c n • (f (x + d n) - f x)) l (𝓝 (f' v))
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h : HasFDerivWithinAt f f' s x<VAR>α : Type u_6<VAR>l : Filter α<VAR>c : α → 𝕜<VAR>d : α → E<VAR>v : E<VAR>dtop : ∀ᶠ (n : α) in l, x + d n ∈ s<VAR>clim : Tendsto (fun n => ‖c n‖) l atTop<VAR>cdlim : Tendsto (fun n => c n • d n) l (𝓝 v)<VAR>tendsto_arg : Tendsto (fun n => x + d n) l (𝓝[s] x)<VAR>this✝¹ : (fun y => f y - f x - f' (y - x)) =o[𝓝[s] x] fun y => y - x<VAR>this✝ : (fun n => f (x + d n) - f x - f' (x + d n - x)) =o[l] fun n => x + d n - x<VAR>this : (fun n => f (x + d n) - f x - f' (d n)) =o[l] d<GOAL>Tendsto (fun n => c n • (f (x + d n) - f x)) l (𝓝 (f' v))
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h : HasFDerivWithinAt f f' s x<VAR>α : Type u_6<VAR>l : Filter α<VAR>c : α → 𝕜<VAR>d : α → E<VAR>v : E<VAR>dtop : ∀ᶠ (n : α) in l, x + d n ∈ s<VAR>clim : Tendsto (fun n => ‖c n‖) l atTop<VAR>cdlim : Tendsto (fun n => c n • d n) l (𝓝 v)<VAR>tendsto_arg : Tendsto (fun n => x + d n) l (𝓝[s] x)<VAR>this✝² : (fun y => f y - f x - f' (y - x)) =o[𝓝[s] x] fun y => y - x<VAR>this✝¹ : (fun n => f (x + d n) - f x - f' (x + d n - x)) =o[l] fun n => x + d n - x<VAR>this✝ : (fun n => f (x + d n) - f x - f' (d n)) =o[l] d<VAR>this : (fun n => c n • (f (x + d n) - f x - f' (d n))) =o[l] fun n => c n • d n<GOAL>Tendsto (fun n => c n • (f (x + d n) - f x)) l (𝓝 (f' v))
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h : HasFDerivWithinAt f f' s x<VAR>α : Type u_6<VAR>l : Filter α<VAR>c : α → 𝕜<VAR>d : α → E<VAR>v : E<VAR>dtop : ∀ᶠ (n : α) in l, x + d n ∈ s<VAR>clim : Tendsto (fun n => ‖c n‖) l atTop<VAR>cdlim : Tendsto (fun n => c n • d n) l (𝓝 v)<VAR>tendsto_arg : Tendsto (fun n => x + d n) l (𝓝[s] x)<VAR>this✝³ : (fun y => f y - f x - f' (y - x)) =o[𝓝[s] x] fun y => y - x<VAR>this✝² : (fun n => f (x + d n) - f x - f' (x + d n - x)) =o[l] fun n => x + d n - x<VAR>this✝¹ : (fun n => f (x + d n) - f x - f' (d n)) =o[l] d<VAR>this✝ : (fun n => c n • (f (x + d n) - f x - f' (d n))) =o[l] fun n => c n • d n<VAR>this : (fun n => c n • (f (x + d n) - f x - f' (d n))) =o[l] fun x => 1<GOAL>Tendsto (fun n => c n • (f (x + d n) - f x)) l (𝓝 (f' v))
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h : HasFDerivWithinAt f f' s x<VAR>α : Type u_6<VAR>l : Filter α<VAR>c : α → 𝕜<VAR>d : α → E<VAR>v : E<VAR>dtop : ∀ᶠ (n : α) in l, x + d n ∈ s<VAR>clim : Tendsto (fun n => ‖c n‖) l atTop<VAR>cdlim : Tendsto (fun n => c n • d n) l (𝓝 v)<VAR>tendsto_arg : Tendsto (fun n => x + d n) l (𝓝[s] x)<VAR>this✝³ : (fun y => f y - f x - f' (y - x)) =o[𝓝[s] x] fun y => y - x<VAR>this✝² : (fun n => f (x + d n) - f x - f' (x + d n - x)) =o[l] fun n => x + d n - x<VAR>this✝¹ : (fun n => f (x + d n) - f x - f' (d n)) =o[l] d<VAR>this✝ : (fun n => c n • (f (x + d n) - f x - f' (d n))) =o[l] fun n => c n • d n<VAR>this : (fun n => c n • (f (x + d n) - f x - f' (d n))) =o[l] fun x => 1<VAR>L1 : Tendsto (fun n => c n • (f (x + d n) - f x - f' (d n))) l (𝓝 0)<GOAL>Tendsto (fun n => c n • (f (x + d n) - f x)) l (𝓝 (f' v))
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h : HasFDerivWithinAt f f' s x<VAR>α : Type u_6<VAR>l : Filter α<VAR>c : α → 𝕜<VAR>d : α → E<VAR>v : E<VAR>dtop : ∀ᶠ (n : α) in l, x + d n ∈ s<VAR>clim : Tendsto (fun n => ‖c n‖) l atTop<VAR>cdlim : Tendsto (fun n => c n • d n) l (𝓝 v)<VAR>tendsto_arg : Tendsto (fun n => x + d n) l (𝓝[s] x)<VAR>this✝³ : (fun y => f y - f x - f' (y - x)) =o[𝓝[s] x] fun y => y - x<VAR>this✝² : (fun n => f (x + d n) - f x - f' (x + d n - x)) =o[l] fun n => x + d n - x<VAR>this✝¹ : (fun n => f (x + d n) - f x - f' (d n)) =o[l] d<VAR>this✝ : (fun n => c n • (f (x + d n) - f x - f' (d n))) =o[l] fun n => c n • d n<VAR>this : (fun n => c n • (f (x + d n) - f x - f' (d n))) =o[l] fun x => 1<VAR>L1 : Tendsto (fun n => c n • (f (x + d n) - f x - f' (d n))) l (𝓝 0)<VAR>L2 : Tendsto (fun n => f' (c n • d n)) l (𝓝 (f' v))<GOAL>Tendsto (fun n => c n • (f (x + d n) - f x)) l (𝓝 (f' v))
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h : HasFDerivWithinAt f f' s x<VAR>α : Type u_6<VAR>l : Filter α<VAR>c : α → 𝕜<VAR>d : α → E<VAR>v : E<VAR>dtop : ∀ᶠ (n : α) in l, x + d n ∈ s<VAR>clim : Tendsto (fun n => ‖c n‖) l atTop<VAR>cdlim : Tendsto (fun n => c n • d n) l (𝓝 v)<VAR>tendsto_arg : Tendsto (fun n => x + d n) l (𝓝[s] x)<VAR>this✝³ : (fun y => f y - f x - f' (y - x)) =o[𝓝[s] x] fun y => y - x<VAR>this✝² : (fun n => f (x + d n) - f x - f' (x + d n - x)) =o[l] fun n => x + d n - x<VAR>this✝¹ : (fun n => f (x + d n) - f x - f' (d n)) =o[l] d<VAR>this✝ : (fun n => c n • (f (x + d n) - f x - f' (d n))) =o[l] fun n => c n • d n<VAR>this : (fun n => c n • (f (x + d n) - f x - f' (d n))) =o[l] fun x => 1<VAR>L1 : Tendsto (fun n => c n • (f (x + d n) - f x - f' (d n))) l (𝓝 0)<VAR>L2 : Tendsto (fun n => f' (c n • d n)) l (𝓝 (f' v))<VAR>L3 : Tendsto (fun n => c n • (f (x + d n) - f x - f' (d n)) + f' (c n • d n)) l (𝓝 (0 + f' v))<GOAL>Tendsto (fun n => c n • (f (x + d n) - f x)) l (𝓝 (f' v))