ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H✝ : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H✝<VAR>inst✝ : NormedSpace 𝕜 H✝<VAR>n : ℕ<VAR>a : Composition n<VAR>b : (i : Fin a.length) → Composition (a.blocksFun i)<VAR>a' : Composition n<VAR>b' : (i : Fin a'.length) → Composition (a'.blocksFun i)<VAR>H : (ofFn fun i => (b i).blocks) = ofFn fun i => (b' i).blocks<GOAL>⟨a, b⟩ = ⟨a', b'⟩
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H✝ : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H✝<VAR>inst✝ : NormedSpace 𝕜 H✝<VAR>n : ℕ<VAR>a : Composition n<VAR>b : (i : Fin a.length) → Composition (a.blocksFun i)<VAR>a' : Composition n<VAR>b' : (i : Fin a'.length) → Composition (a'.blocksFun i)<VAR>H : (ofFn fun i => (b i).blocks) = ofFn fun i => (b' i).blocks<VAR>h : a = a'<GOAL>⟨a, b⟩ = ⟨a', b'⟩
<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>ι : Type u_6<VAR>𝔸 : Type u_7<VAR>𝔸' : Type u_8<VAR>inst✝⁵ : NormedRing 𝔸<VAR>inst✝⁴ : NormedCommRing 𝔸'<VAR>inst✝³ : NormedAlgebra 𝕜 𝔸<VAR>inst✝² : NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>f : ι → E → 𝔸<VAR>f' : ι → E →L[𝕜] 𝔸<VAR>g : ι → E → 𝔸'<VAR>g' : ι → E →L[𝕜] 𝔸'<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>l : List ι<VAR>x : ι → 𝔸'<GOAL>HasStrictFDerivAt (fun x => (List.map x l).prod) (List.map (fun i => (List.map x (l.erase i)).prod • proj i) l).sum x
<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>ι : Type u_6<VAR>𝔸 : Type u_7<VAR>𝔸' : Type u_8<VAR>inst✝⁵ : NormedRing 𝔸<VAR>inst✝⁴ : NormedCommRing 𝔸'<VAR>inst✝³ : NormedAlgebra 𝕜 𝔸<VAR>inst✝² : NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>f : ι → E → 𝔸<VAR>f' : ι → E →L[𝕜] 𝔸<VAR>g : ι → E → 𝔸'<VAR>g' : ι → E →L[𝕜] 𝔸'<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>l : List ι<VAR>x : ι → 𝔸'<GOAL>∑ i : Fin l.length, (List.map x (List.take (↑i) l)).prod • (proj (l.get i)).smulRight (List.map x (List.drop (↑i).succ l)).prod = (List.map (fun i => (List.map x (l.erase i)).prod • proj i) l).sum
<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>ι : Type u_6<VAR>𝔸 : Type u_7<VAR>𝔸' : Type u_8<VAR>inst✝⁵ : NormedRing 𝔸<VAR>inst✝⁴ : NormedCommRing 𝔸'<VAR>inst✝³ : NormedAlgebra 𝕜 𝔸<VAR>inst✝² : NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>f : ι → E → 𝔸<VAR>f' : ι → E →L[𝕜] 𝔸<VAR>g : ι → E → 𝔸'<VAR>g' : ι → E →L[𝕜] 𝔸'<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>l : List ι<VAR>x : ι → 𝔸'<GOAL>∑ i : Fin l.length, (List.map x (List.take (↑i) l)).prod • (proj (l.get i)).smulRight (List.map x (List.drop (↑i).succ l)).prod = (List.map (fun i => (List.map x (l.erase i)).prod • proj i) (List.map l.get (List.finRange l.length))).sum
<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>ι : Type u_6<VAR>𝔸 : Type u_7<VAR>𝔸' : Type u_8<VAR>inst✝⁵ : NormedRing 𝔸<VAR>inst✝⁴ : NormedCommRing 𝔸'<VAR>inst✝³ : NormedAlgebra 𝕜 𝔸<VAR>inst✝² : NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>f : ι → E → 𝔸<VAR>f' : ι → E →L[𝕜] 𝔸<VAR>g : ι → E → 𝔸'<VAR>g' : ι → E →L[𝕜] 𝔸'<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>l : List ι<VAR>x : ι → 𝔸'<GOAL>∑ i : Fin l.length, (List.map x (List.take (↑i) l)).prod • (proj (l.get i)).smulRight (List.map x (List.drop (↑i).succ l)).prod = ∑ x_1 : Fin l.length, ((List.map x (List.take (↑x_1) l)).prod * (List.map x (List.drop (↑x_1 + 1) l)).prod) • proj (l.get x_1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : SuccOrder α<VAR>a b : α<VAR>ha : ¬IsMax a<VAR>hb : ¬IsMax b<GOAL>succ a ≤ succ b ↔ a ≤ b
<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>‖↑(harmonic n)‖ = 2 ^ Nat.log 2 n
<VAR>N : ℕ<VAR>inst✝ : NeZero N<VAR>Φ : ZMod N → ℂ<VAR>k : ZMod N<GOAL>𝓕 Φ k = ∑ j : ZMod N, toCircle (-(j * k)) • Φ j
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : GCDMonoid R<VAR>M : Submonoid R<VAR>inst✝ : IsLocalization M A<VAR>z : A<GOAL>∃ a b, IsUnit (gcd a b) ∧ z * (algebraMap R A) b = (algebraMap R A) a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : GCDMonoid R<VAR>M : Submonoid R<VAR>inst✝ : IsLocalization M A<VAR>x y : R<VAR>hy : y ∈ M<GOAL>∃ a b, IsUnit (gcd a b) ∧ mk' A x ⟨y, hy⟩ * (algebraMap R A) b = (algebraMap R A) a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : GCDMonoid R<VAR>M : Submonoid R<VAR>inst✝ : IsLocalization M A<VAR>x y : R<VAR>hy : y ∈ M<VAR>x' y' : R<VAR>hx' : x = gcd x y * x'<VAR>hy' : y = gcd x y * y'<VAR>hu : IsUnit (gcd x' y')<GOAL>∃ a b, IsUnit (gcd a b) ∧ mk' A x ⟨y, hy⟩ * (algebraMap R A) b = (algebraMap R A) a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : GCDMonoid R<VAR>M : Submonoid R<VAR>inst✝ : IsLocalization M A<VAR>x y : R<VAR>hy : y ∈ M<VAR>x' y' : R<VAR>hx' : x = gcd x y * x'<VAR>hy' : y = gcd x y * y'<VAR>hu : IsUnit (gcd x' y')<GOAL>mk' A x ⟨y, hy⟩ * (algebraMap R A) y' = (algebraMap R A) x'
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : GCDMonoid R<VAR>M : Submonoid R<VAR>inst✝ : IsLocalization M A<VAR>x y : R<VAR>hy : y ∈ M<VAR>x' y' : R<VAR>hx' : x = gcd x y * x'<VAR>hy' : y = gcd x y * y'<VAR>hu : IsUnit (gcd x' y')<GOAL>mk' A (y' * x) ⟨y, hy⟩ = (algebraMap R A) x'
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : GCDMonoid R<VAR>M : Submonoid R<VAR>inst✝ : IsLocalization M A<VAR>x y : R<VAR>hy : y ∈ M<VAR>x' y' : R<VAR>hx' : x = gcd x y * x'<VAR>hy' : y = gcd x y * y'<VAR>hu : IsUnit (gcd x' y')<GOAL>y' * x = ↑⟨y, hy⟩ * x'
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : GCDMonoid R<VAR>M : Submonoid R<VAR>inst✝ : IsLocalization M A<VAR>x y : R<VAR>hy : y ∈ M<VAR>x' y' : R<VAR>hx' : x = gcd x y * x'<VAR>hy' : y = gcd x y * y'<VAR>hu : IsUnit (gcd x' y')<GOAL>y' * x = y' * (gcd x y * x')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>s t : Set α<VAR>hs : s.Nontrivial<GOAL>s.infsep = ⨅ d, uncurry dist ↑d
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>f : E → F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>h : HasFPowerSeriesOnBall f p x r<VAR>y : E<VAR>x✝ : Fin 0 → E<GOAL>(iteratedFDeriv 𝕜 0 f x) x✝ = (p 0) x✝
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>f : E → F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>h : HasFPowerSeriesOnBall f p x r<VAR>y : E<VAR>x✝ : Fin 0 → E<GOAL>(iteratedFDeriv 𝕜 0 f x) x✝ = f (x + 0)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>f : E → F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>h : HasFPowerSeriesOnBall f p x r<VAR>y : E<VAR>x✝ : Fin 0 → E<GOAL>(p 0) x✝ = ∑' (b : ℕ), (p b) fun x => 0
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type w<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Semiring S<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁶ : CommSemiring R₁<VAR>inst✝⁵ : CommSemiring R₂<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R₁ A<VAR>inst✝² : Algebra R₂ A<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R₁ B<VAR>f : A →ₐ[R₁] B<VAR>r : R₁<VAR>x : A ⧸ ker f<GOAL>f.kerLift (r • x) = r • f.kerLift x
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type w<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Semiring S<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁶ : CommSemiring R₁<VAR>inst✝⁵ : CommSemiring R₂<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R₁ A<VAR>inst✝² : Algebra R₂ A<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R₁ B<VAR>f : A →ₐ[R₁] B<VAR>r : R₁<VAR>a : A<GOAL>f.kerLift (r • (Quotient.mkₐ R₁ (ker f)) a) = r • f.kerLift ((Quotient.mkₐ R₁ (ker f)) a)
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝ : CommRing R<VAR>P : R[X]<VAR>hunit : IsUnit P<GOAL>IsUnit (P.coeff 0) ∧ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝ : CommRing R<VAR>P : R[X]<VAR>hunit : IsUnit P<VAR>Q : R[X]<VAR>hQ : P * Q = 1<GOAL>IsUnit (P.coeff 0) ∧ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y z : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hz : z ≠ 0<GOAL>o.oangle y z + o.oangle x y = o.oangle x z
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>Q : QuadraticMap R M N<VAR>x : M<GOAL>Q (x + x) = 4 • Q x
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>Q : QuadraticMap R M N<VAR>x : M<GOAL>(2 * 2) • Q x = ↑4 • Q x
<VAR>α : Type u_1<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Invertible 2<VAR>a : α<GOAL>sym (a * a) = sym a * sym a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g s✝ t✝ : ι → α<VAR>a b : α<VAR>f : β → α<VAR>s t : Set β<GOAL>⨆ x ∈ s ∪ t, f x = (⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x
<VAR>α : Type u_1<VAR>x : LazyList α<GOAL>x.bind singleton = x
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Zero (α i)<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>inst✝ : DecidableEq ι<VAR>x : Π₀ (i : ι), α i<VAR>i : ι<VAR>hs : Acc (DFinsupp.Lex r s) (single i (x i))<VAR>hu : Acc (DFinsupp.Lex r s) (erase i x)<GOAL>Acc (DFinsupp.Lex r s) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>n : ℕ<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>c : Composition n<GOAL>‖q.compAlongComposition p c‖₊ ≤ ‖q c.length‖₊ * ∏ i : Fin c.length, ‖p (c.blocksFun i)‖₊
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>n : ℕ<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>c : Composition n<GOAL>↑‖q.compAlongComposition p c‖₊ ≤ ↑(‖q c.length‖₊ * ∏ i : Fin c.length, ‖p (c.blocksFun i)‖₊)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>n : ℕ<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>c : Composition n<GOAL>‖q.compAlongComposition p c‖ ≤ ‖q c.length‖ * ∏ x : Fin c.length, ‖p (c.blocksFun x)‖
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x - a) ⁻¹' Ioi b = Ioi (b + a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R S : α → β → Prop<VAR>P : γ → δ → Prop<VAR>Rₐ : α → α → Prop<VAR>a✝ : α<VAR>b✝ : β<VAR>l₁✝ : List α<VAR>l₂✝ : List β<VAR>h₁ : R a✝ b✝<VAR>h₂ : Forall₂ R l₁✝ l₂✝<VAR>x : α<VAR>y : β<VAR>hx : (x, y) ∈ (a✝ :: l₁✝).zip (b✝ :: l₂✝)<GOAL>R x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R S : α → β → Prop<VAR>P : γ → δ → Prop<VAR>Rₐ : α → α → Prop<VAR>a✝ : α<VAR>b✝ : β<VAR>l₁✝ : List α<VAR>l₂✝ : List β<VAR>h₁ : R a✝ b✝<VAR>h₂ : Forall₂ R l₁✝ l₂✝<VAR>x : α<VAR>y : β<VAR>hx : (x, y) = (a✝, b✝) ∨ (x, y) ∈ zipWith Prod.mk l₁✝ l₂✝<GOAL>R x y
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u✝ v✝ w : V<VAR>hconn : G.Connected<VAR>u v : V<GOAL>∃ p, p.IsPath ∧ p.length = G.dist u v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u✝ v✝ w : V<VAR>hconn : G.Connected<VAR>u v : V<VAR>p : G.Walk u v<VAR>h : p.length = G.dist u v<GOAL>∃ p, p.IsPath ∧ p.length = G.dist u v
<VAR>o₁ o₂ : Ordinal.{u_1}<GOAL>nim o₁ + nim o₂ ‖ 0 ↔ o₁ ≠ o₂
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalSemiring R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>f✝ g : R → R<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<VAR>hf : autoParam (ContinuousOn f✝ (spectrum R a)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝<VAR>inst✝ : UniqueContinuousFunctionalCalculus R A<VAR>f : R → R<GOAL>cfc f 1 = (algebraMap R A) (f 1)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : OrderedSMul α β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<GOAL>MonovaryOn f (⇑OrderDual.toDual ∘ g) s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i • g i + f j • g j ≤ f i • g j + f j • g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : OrderedSMul α β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<GOAL>(∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i • (⇑OrderDual.toDual ∘ g) j + f j • (⇑OrderDual.toDual ∘ g) i ≤ f i • (⇑OrderDual.toDual ∘ g) i + f j • (⇑OrderDual.toDual ∘ g) j) ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i • g i + f j • g j ≤ f i • g j + f j • g i
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>inst✝ : PseudoMetricSpace β<VAR>f : α → β<VAR>a : α<VAR>b : β<GOAL>Tendsto f (𝓝[s] a) (𝓝 b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → dist x a < δ → dist (f x) b < ε
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>inst✝ : PseudoMetricSpace β<VAR>f : α → β<VAR>a : α<VAR>b : β<GOAL>(∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → dist x a < δ → f x ∈ univ ∧ dist (f x) b < ε) ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → dist x a < δ → dist (f x) b < ε
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : SMulCommClass ℝ 𝕜 F<VAR>f : 𝓢(E, F)<VAR>n : ℕ<VAR>x₀ : E<GOAL>‖iteratedFDeriv ℝ n (⇑f) x₀‖ ≤ (SchwartzMap.seminorm 𝕜 0 n) f
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : SMulCommClass ℝ 𝕜 F<VAR>f : 𝓢(E, F)<VAR>n : ℕ<VAR>x₀ : E<VAR>this : ‖x₀‖ ^ 0 * ‖iteratedFDeriv ℝ n (⇑f) x₀‖ ≤ (SchwartzMap.seminorm 𝕜 0 n) f<GOAL>‖iteratedFDeriv ℝ n (⇑f) x₀‖ ≤ (SchwartzMap.seminorm 𝕜 0 n) f
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<GOAL>(x * y) ^ z = if (x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0) ∧ z < 0 then ⊤ else x ^ z * y ^ z
<VAR>x y : ℝ≥0∞<GOAL>(x * y) ^ 0 = if (x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0) ∧ 0 < 0 then ⊤ else x ^ 0 * y ^ 0
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<VAR>hz : z ≠ 0<GOAL>(x * y) ^ z = if (x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0) ∧ z < 0 then ⊤ else x ^ z * y ^ z
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<VAR>hz : z < 0 ∨ 0 < z<GOAL>(x * y) ^ z = if (x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0) ∧ z < 0 then ⊤ else x ^ z * y ^ z
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<VAR>hz : z < 0 ∨ 0 < z<VAR>hxy : x ≤ y<GOAL>(x * y) ^ z = if (x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0) ∧ z < 0 then ⊤ else x ^ z * y ^ z
<VAR>y : ℝ≥0∞<VAR>z : ℝ<VAR>hz : z < 0 ∨ 0 < z<VAR>hxy : 0 ≤ y<GOAL>(0 * y) ^ z = if (0 = 0 ∧ y = ⊤ ∨ 0 = ⊤ ∧ y = 0) ∧ z < 0 then ⊤ else 0 ^ z * y ^ z
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<VAR>hz : z < 0 ∨ 0 < z<VAR>hxy : x ≤ y<VAR>hx0 : x ≠ 0<GOAL>(x * y) ^ z = if (x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0) ∧ z < 0 then ⊤ else x ^ z * y ^ z
<VAR>x : ℝ≥0∞<VAR>z : ℝ<VAR>hz : z < 0 ∨ 0 < z<VAR>hx0 : x ≠ 0<VAR>hxy : x ≤ 0<GOAL>(x * 0) ^ z = if (x = 0 ∧ 0 = ⊤ ∨ x = ⊤ ∧ 0 = 0) ∧ z < 0 then ⊤ else x ^ z * 0 ^ z
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<VAR>hz : z < 0 ∨ 0 < z<VAR>hxy : x ≤ y<VAR>hx0 : x ≠ 0<VAR>hy0 : y ≠ 0<GOAL>(x * y) ^ z = if (x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0) ∧ z < 0 then ⊤ else x ^ z * y ^ z
<VAR>z : ℝ<VAR>hz : z < 0 ∨ 0 < z<VAR>x✝¹ : ℝ≥0<VAR>hx0 : ↑x✝¹ ≠ 0<VAR>x✝ : ℝ≥0<VAR>hy0 : ↑x✝ ≠ 0<VAR>hxy : ↑x✝¹ ≤ ↑x✝<GOAL>(↑x✝¹ * ↑x✝) ^ z = if (↑x✝¹ = 0 ∧ ↑x✝ = ⊤ ∨ ↑x✝¹ = ⊤ ∧ ↑x✝ = 0) ∧ z < 0 then ⊤ else ↑x✝¹ ^ z * ↑x✝ ^ z
<VAR>z : ℝ<VAR>hz : z < 0 ∨ 0 < z<VAR>x✝¹ : ℝ≥0<VAR>hx0 : ↑x✝¹ ≠ 0<VAR>x✝ : ℝ≥0<VAR>hy0 : ↑x✝ ≠ 0<VAR>hxy : ↑x✝¹ ≤ ↑x✝<GOAL>(↑x✝¹ * ↑x✝) ^ z = ↑x✝¹ ^ z * ↑x✝ ^ z
<VAR>z : ℝ<VAR>x✝¹ x✝ : ℝ≥0<VAR>hz : z < 0 ∨ 0 < z<VAR>hx0 : ¬x✝¹ = 0<VAR>hy0 : ¬x✝ = 0<VAR>hxy : x✝¹ ≤ x✝<GOAL>↑(x✝¹ * x✝) ^ z = ↑x✝¹ ^ z * ↑x✝ ^ z
<VAR>z : ℝ<VAR>x✝¹ x✝ : ℝ≥0<VAR>hz : z < 0 ∨ 0 < z<VAR>hx0 : ¬x✝¹ = 0<VAR>hy0 : ¬x✝ = 0<VAR>hxy : x✝¹ ≤ x✝<GOAL>↑(x✝¹ ^ z * x✝ ^ z) = ↑x✝¹ ^ z * ↑x✝ ^ z
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>A : Set P<VAR>inst✝ : Nonempty ↑A<GOAL>affineSpan k (Subtype.val ⁻¹' A) = ⊤
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>A : Set P<VAR>inst✝ : Nonempty ↑A<GOAL>⊤ ≤ affineSpan k (Subtype.val ⁻¹' A)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>A : Set P<VAR>inst✝ : Nonempty ↑A<VAR>x : P<VAR>hx : x ∈ ↑(affineSpan k A)<GOAL>⟨x, hx⟩ ∈ ↑(affineSpan k (Subtype.val ⁻¹' A))
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>A : Set P<VAR>inst✝ : Nonempty ↑A<VAR>x : P<VAR>hx : x ∈ ↑(affineSpan k A)<VAR>y : P<VAR>hy : y ∈ A<GOAL>⟨y, ⋯⟩ ∈ ↑(affineSpan k (Subtype.val ⁻¹' A))
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>A : Set P<VAR>inst✝ : Nonempty ↑A<VAR>x : P<VAR>hx : x ∈ ↑(affineSpan k A)<VAR>c : k<VAR>u : P<VAR>hu : u ∈ affineSpan k A<VAR>v : P<VAR>hv : v ∈ affineSpan k A<VAR>w : P<VAR>hw : w ∈ affineSpan k A<GOAL>⟨u, hu⟩ ∈ ↑(affineSpan k (Subtype.val ⁻¹' A)) → ⟨v, hv⟩ ∈ ↑(affineSpan k (Subtype.val ⁻¹' A)) → ⟨w, hw⟩ ∈ ↑(affineSpan k (Subtype.val ⁻¹' A)) → ⟨c • (u -ᵥ v) +ᵥ w, ⋯⟩ ∈ ↑(affineSpan k (Subtype.val ⁻¹' A))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : OuterMeasure α<VAR>s : Set α<VAR>h : s.Nonempty<VAR>a : α<VAR>as : a ∈ s<GOAL>⊤ ≤ (⊤ • dirac a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁴ : Norm E<VAR>inst✝¹³ : Norm F<VAR>inst✝¹² : Norm G<VAR>inst✝¹¹ : SeminormedAddCommGroup E'<VAR>inst✝¹⁰ : SeminormedAddCommGroup F'<VAR>inst✝⁹ : SeminormedAddCommGroup G'<VAR>inst✝⁸ : NormedAddCommGroup E''<VAR>inst✝⁷ : NormedAddCommGroup F''<VAR>inst✝⁶ : NormedAddCommGroup G''<VAR>inst✝⁵ : SeminormedRing R<VAR>inst✝⁴ : SeminormedAddGroup E'''<VAR>inst✝³ : SeminormedRing R'<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>inst✝¹ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f✝ : α → E<VAR>g✝ : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝ : NormOneClass R<VAR>f : α → R<VAR>g : α → 𝕜<VAR>h : IsBigOWith c l f g<GOAL>IsBigOWith (c ^ 0) l (fun x => f x ^ 0) fun x => g x ^ 0
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ : Multiset α<VAR>a : α<VAR>s t : Multiset α<GOAL>count a (s ∩ t) = min (count a s) (count a t)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ : Multiset α<VAR>a : α<VAR>s t : Multiset α<GOAL>count a (s - t) + count a (s ∩ t) = count a (s - t) + min (count a s) (count a t)
<VAR>x a r : ℝ<VAR>hx : x ≤ 0<GOAL>∫⁻ (y : ℝ) in Iio x, gammaPDF a r y = 0
<VAR>x a r : ℝ<VAR>hx : x ≤ 0<GOAL>∫⁻ (x : ℝ) in Iio x, 0 = 0
<VAR>x a r : ℝ<VAR>hx : x ≤ 0<GOAL>∀ᵐ (x_1 : ℝ), x_1 ∈ Iio x → gammaPDF a r x_1 = 0