ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>h_coe : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b<VAR>x : γ<VAR>hx : κ.rnDerivAux (κ + η) a x < 1<GOAL>0 < 1 - κ.rnDerivAux (κ + η) a x
<VAR>C : Type u_1<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>J : Type u_4<VAR>inst✝⁷ : Category.{u_5, u_1} C<VAR>inst✝⁶ : Preadditive C<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c : ComplexShape J<VAR>inst✝⁵ : TotalComplexShape c₁ c₂ c<VAR>inst✝⁴ : TotalComplexShape c₂ c₁ c<VAR>inst✝³ : TotalComplexShapeSymmetry c₁ c₂ c<VAR>inst✝² : K.HasTotal c<VAR>inst✝¹ : K.flip.HasTotal c<VAR>inst✝ : DecidableEq J<VAR>j j' : J<GOAL>(K.totalFlipIso c).hom.f j ≫ K.D₁ c j j' = K.flip.D₂ c j j' ≫ (K.totalFlipIso c).hom.f j'
<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 : V<GOAL>⟪(o.rotation ↑(π / 2)) x, x⟫_ℝ = 0
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>x : ℝ<VAR>hx : x ∈ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}<GOAL>x ∈ D f K
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>x : ℝ<VAR>hx : x ∈ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}<GOAL>∀ (i : ℕ), x ∈ ⋃ n, ⋂ p, ⋂ (_ : p ≥ n), ⋂ q, ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ i)
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>x : ℝ<VAR>hx : x ∈ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}<VAR>e : ℕ<GOAL>x ∈ ⋃ n, ⋂ p, ⋂ (_ : p ≥ n), ⋂ q, ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e)
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>x : ℝ<VAR>hx : x ∈ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}<VAR>e : ℕ<VAR>this : 0 < (1 / 2) ^ e<GOAL>x ∈ ⋃ n, ⋂ p, ⋂ (_ : p ≥ n), ⋂ q, ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e)
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>x : ℝ<VAR>hx : x ∈ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}<VAR>e : ℕ<VAR>this : 0 < (1 / 2) ^ e<VAR>R : ℝ<VAR>R_pos : R > 0<VAR>hR : ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ((1 / 2) ^ e)<GOAL>x ∈ ⋃ n, ⋂ p, ⋂ (_ : p ≥ n), ⋂ q, ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e)
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>x : ℝ<VAR>hx : x ∈ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}<VAR>e : ℕ<VAR>this : 0 < (1 / 2) ^ e<VAR>R : ℝ<VAR>R_pos : R > 0<VAR>hR : ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ((1 / 2) ^ e)<VAR>n : ℕ<VAR>hn : (1 / 2) ^ n < R<GOAL>x ∈ ⋃ n, ⋂ p, ⋂ (_ : p ≥ n), ⋂ q, ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e)
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>x : ℝ<VAR>hx : x ∈ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}<VAR>e : ℕ<VAR>this : 0 < (1 / 2) ^ e<VAR>R : ℝ<VAR>R_pos : R > 0<VAR>hR : ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ((1 / 2) ^ e)<VAR>n : ℕ<VAR>hn : (1 / 2) ^ n < R<GOAL>∃ i, ∀ i_1 ≥ i, ∀ i_3 ≥ i, ∃ i, ∃ (_ : i ∈ K), x ∈ A f i ((1 / 2) ^ i_1) ((1 / 2) ^ e) ∧ x ∈ A f i ((1 / 2) ^ i_3) ((1 / 2) ^ e)
<VAR>k : Type u_1<VAR>inst✝³ : Field k<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : NumberField K<VAR>w : InfinitePlace K<GOAL>(Finset.filter (fun φ => mk φ = w) Finset.univ).card = w.mult
<VAR>k : Type u_1<VAR>inst✝³ : Field k<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : NumberField K<VAR>w : InfinitePlace K<GOAL>(Finset.filter (fun x => x = w.embedding ∨ x = star w.embedding) Finset.univ).card = w.mult
<VAR>k : Type u_1<VAR>inst✝³ : Field k<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : NumberField K<VAR>w : InfinitePlace K<GOAL>({w.embedding} ∪ {ComplexEmbedding.conjugate w.embedding}).card = if w.IsReal then 1 else 2
<VAR>R : Type u_1<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : BinomialRing R<VAR>n k : ℕ<VAR>h : n < k<GOAL>(ascPochhammer ℕ k).smeval (-↑n) = 0
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝¹⁴ : CommSemiring S<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : NonUnitalSemiring A<VAR>inst✝¹¹ : Module R A<VAR>inst✝¹⁰ : SMulCommClass R A A<VAR>inst✝⁹ : IsScalarTower R A A<VAR>B : Type u_4<VAR>inst✝⁸ : Semiring B<VAR>inst✝⁷ : Algebra S B<VAR>inst✝⁶ : Algebra S R<VAR>inst✝⁵ : DistribMulAction S A<VAR>inst✝⁴ : IsScalarTower S R A<VAR>C : Type u_5<VAR>inst✝³ : Semiring C<VAR>inst✝² : Algebra R C<VAR>F : Type u_6<VAR>inst✝¹ : FunLike F (Unitization R A) C<VAR>inst✝ : AlgHomClass F R (Unitization R A) C<VAR>φ ψ : F<VAR>h : ∀ (a : A), φ ↑a = ψ ↑a<VAR>r : R<GOAL>φ ((algebraMap R (Unitization R A)) r) = ψ ((algebraMap R (Unitization R A)) r)
<VAR>ι : Type u_1<VAR>𝕜✝ : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f✝ g : ℝ → E<VAR>μ : Measure ℝ<VAR>𝕜 : Type u_6<VAR>inst✝ : RCLike 𝕜<VAR>r : 𝕜<VAR>f : ℝ → 𝕜<GOAL>∫ (x : ℝ) in a..b, f x * r ∂μ = (∫ (x : ℝ) in a..b, f x ∂μ) * r
<VAR>a b : Ordinal.{u}<VAR>hab : a * b = b<GOAL>b = 0 ∨ a ^ ω ≤ b
<VAR>a b : Ordinal.{u}<VAR>hab : a * b = b<VAR>ha : a = 0<GOAL>b = 0 ∨ a ^ ω ≤ b
<VAR>a b : Ordinal.{u}<VAR>hab : a * b = b<VAR>ha : 0 < a<GOAL>b = 0 ∨ a ^ ω ≤ b
<VAR>a b : Ordinal.{u}<VAR>hab : a * b = b<VAR>ha : 0 < a<GOAL>¬b = 0 → a ^ ω ≤ b
<VAR>a b : Ordinal.{u}<VAR>hab : a * b = b<VAR>ha : 0 < a<VAR>hb : ¬b = 0<GOAL>a ^ ω ≤ b
<VAR>a b : Ordinal.{u}<VAR>hab : a * b = b<VAR>ha : 0 < a<VAR>hb : ¬b = 0<GOAL>nfp (fun x => a * x) 1 ≤ b
<VAR>a b : Ordinal.{u}<VAR>hab : a * b = b<VAR>ha : 0 < a<VAR>hb : 1 ≤ b<GOAL>nfp (fun x => a * x) 1 ≤ b
<VAR>α : Type u_1<VAR>a : α<VAR>n m : Nat<VAR>l : List α<VAR>h : n < m<VAR>i : Nat<GOAL>(drop m (l.set n a))[i]? = (drop m l)[i]?
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ : Set E<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 < r<VAR>s : ℝ<GOAL>μ (ball x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 s)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ : Set E<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 < r<VAR>s : ℝ<VAR>this : ball 0 (r * s) = r • ball 0 s<GOAL>μ (ball x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 s)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<VAR>hn : 2 < n<VAR>h : ↑n ≠ 0<GOAL>0 < (W.preΨ' n).natDegree
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<VAR>hn : 2 < n<VAR>h : ↑n ≠ 0<GOAL>2 ≤ n ^ 2 - if Even n then 4 else 1
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Monoid K<VAR>inst✝³ : (i : ι) → Group (G i)<VAR>inst✝² : Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Transversal φ<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (G i)<VAR>i : ι<VAR>g : G i<VAR>w : NormalWord d<GOAL>(g • w).prod = (of i) g * w.prod
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u✝ : Multiset α<VAR>a b : α<VAR>s t u : Multiset α<GOAL>s + (t ∪ u) = s + t ∪ (s + u)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝¹⁸ : Field F<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : Algebra F K<VAR>K₁ : Type u_3<VAR>K₂ : Type u_4<VAR>K₃ : Type u_5<VAR>inst✝¹⁵ : Field F<VAR>inst✝¹⁴ : Field K₁<VAR>inst✝¹³ : Field K₂<VAR>inst✝¹² : Field K₃<VAR>inst✝¹¹ : Algebra F K₁<VAR>inst✝¹⁰ : Algebra F K₂<VAR>inst✝⁹ : Algebra F K₃<VAR>ϕ : K₁ →ₐ[F] K₂<VAR>χ : K₁ ≃ₐ[F] K₂<VAR>ψ : K₂ →ₐ[F] K₃<VAR>ω : K₂ ≃ₐ[F] K₃<VAR>E : Type u_6<VAR>inst✝⁸ : Field E<VAR>inst✝⁷ : Algebra F E<VAR>inst✝⁶ : Algebra E K₁<VAR>inst✝⁵ : Algebra E K₂<VAR>inst✝⁴ : Algebra E K₃<VAR>inst✝³ : IsScalarTower F E K₁<VAR>inst✝² : IsScalarTower F E K₂<VAR>inst✝¹ : IsScalarTower F E K₃<VAR>inst✝ : Normal F E<VAR>x✝ : E<GOAL>(algebraMap E K₃) (((χ.trans ω).restrictNormal E) x✝) = (algebraMap E K₃) (((χ.restrictNormal E).trans (ω.restrictNormal E)) x✝)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NoAtoms μ✝<VAR>h : s.Countable<VAR>μ : Measure α<VAR>inst✝ : NoAtoms μ<GOAL>μ s = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NoAtoms μ✝<VAR>h : s.Countable<VAR>μ : Measure α<VAR>inst✝ : NoAtoms μ<GOAL>∀ i ∈ s, μ {i} = 0
<VAR>α : Type u<VAR>l : List α<VAR>hl : l.Nodup<VAR>n : ℕ<GOAL>l.rotate n = l ↔ n % l.length = 0 ∨ l = []
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>x y z : E<GOAL>𝓚 ‖x + y + z‖ * 𝓚 ‖x + y + z‖ - 𝓚 ‖x + y - z‖ * 𝓚 ‖x + y - z‖ + I * 𝓚 ‖I • (x + y) + z‖ * 𝓚 ‖I • (x + y) + z‖ - I * 𝓚 ‖I • (x + y) - z‖ * 𝓚 ‖I • (x + y) - z‖ = 𝓚 ‖x + z‖ * 𝓚 ‖x + z‖ - 𝓚 ‖x - z‖ * 𝓚 ‖x - z‖ + I * 𝓚 ‖I • x + z‖ * 𝓚 ‖I • x + z‖ - I * 𝓚 ‖I • x - z‖ * 𝓚 ‖I • x - z‖ + (𝓚 ‖y + z‖ * 𝓚 ‖y + z‖ - 𝓚 ‖y - z‖ * 𝓚 ‖y - z‖ + I * 𝓚 ‖I • y + z‖ * 𝓚 ‖I • y + z‖ - I * 𝓚 ‖I • y - z‖ * 𝓚 ‖I • y - z‖)
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>x y z : E<GOAL>𝓚 (‖x + y + z‖ * ‖x + y + z‖ - ‖x + (y - z)‖ * ‖x + (y - z)‖) + I * 𝓚 (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ - ‖I • (x + y) - z‖ * ‖I • (x + y) - z‖) = 𝓚 (‖x + z‖ * ‖x + z‖ - ‖x - z‖ * ‖x - z‖) + I * 𝓚 (‖I • x + z‖ * ‖I • x + z‖ - ‖I • x - z‖ * ‖I • x - z‖) + (𝓚 (‖y + z‖ * ‖y + z‖ - ‖y - z‖ * ‖y - z‖) + I * 𝓚 (‖I • y + z‖ * ‖I • y + z‖ - ‖I • y - z‖ * ‖I • y - z‖))
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>x y z : E<GOAL>𝓚 (‖x + y + z‖ * ‖x + y + z‖ - ‖x + (y - z)‖ * ‖x + (y - z)‖) + I * 𝓚 (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ - ‖I • (x + y) - z‖ * ‖I • (x + y) - z‖) = 𝓚 (‖x + z‖ * ‖x + z‖ - ‖x - z‖ * ‖x - z‖) + 𝓚 (‖y + z‖ * ‖y + z‖ - ‖y - z‖ * ‖y - z‖) + (I * 𝓚 (‖I • x + z‖ * ‖I • x + z‖ - ‖I • x - z‖ * ‖I • x - z‖) + I * 𝓚 (‖I • y + z‖ * ‖I • y + z‖ - ‖I • y - z‖ * ‖I • y - z‖))
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>x y z : E<GOAL>𝓚 (‖x + y + z‖ * ‖x + y + z‖ - ‖x + (y - z)‖ * ‖x + (y - z)‖) + I * 𝓚 (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ - ‖I • (x + y) - z‖ * ‖I • (x + y) - z‖) = 𝓚 (‖x + z‖ * ‖x + z‖ - ‖x - z‖ * ‖x - z‖ + (‖y + z‖ * ‖y + z‖ - ‖y - z‖ * ‖y - z‖)) + I * 𝓚 (‖I • x + z‖ * ‖I • x + z‖ - ‖I • x - z‖ * ‖I • x - z‖ + (‖I • y + z‖ * ‖I • y + z‖ - ‖I • y - z‖ * ‖I • y - z‖))
<VAR>α : Type u<VAR>m n o : ℕ<VAR>m' : Type u_1<VAR>n' : Type u_2<VAR>o' : Type u_3<VAR>v : Fin n → α<VAR>i : Fin n<GOAL>vecAlt0 ⋯ (vecAppend ⋯ v v) i = (v ∘ fun n_1 => n_1 + n_1) i
<VAR>α : Type u<VAR>m n o : ℕ<VAR>m' : Type u_1<VAR>n' : Type u_2<VAR>o' : Type u_3<VAR>v : Fin n → α<VAR>i : Fin n<GOAL>(if h : ↑i + ↑i < n then v ⟨↑i + ↑i, ⋯⟩ else v ⟨↑i + ↑i - n, ⋯⟩) = v (i + i)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>r✝ r : List (List α)<VAR>l : List α<VAR>ih : sublistsAux a r = r.bind fun l => [l, a :: l]<GOAL>sublistsAux a (r ++ [l]) = (r ++ [l]).bind fun l => [l, a :: l]
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>r✝ r : List (List α)<VAR>l : List α<VAR>ih : sublistsAux a r = r.bind fun l => [l, a :: l]<GOAL>foldl (fun r l => r ++ [l, a :: l]) (foldl (fun r l => r ++ [l, a :: l]) [] r) [l] = sublistsAux a r ++ [l, a :: l]
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>r : R<VAR>x y : S<VAR>this : SMulZeroClass R S := inferInstance<GOAL>(y𝖣r • x) = r • y𝖣x
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : Add R<VAR>inst✝⁴ : Mul R<VAR>inst✝³ : Neg R<VAR>inst✝² : One R<VAR>inst✝¹ : Zero R<VAR>inst✝ : CompatibleRing R<VAR>x : ring.Term α<VAR>v : α → R<GOAL>Term.realize v (-x) = -Term.realize v x
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasInjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<VAR>n : ℕ<GOAL>whiskerRight (rightDerivedToHomotopyCategory (𝟙 F)) (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n) = 𝟙 (F.rightDerived n)
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasInjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<VAR>n : ℕ<GOAL>𝟙 (F.rightDerivedToHomotopyCategory ⋙ HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n) = 𝟙 (F.rightDerived n)
<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>k n : ℕ<VAR>f g : 𝓢(E, F)<VAR>x : E<GOAL>‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f + ⇑g) x‖ ≤ ‖x‖ ^ k * (‖iteratedFDeriv ℝ n (⇑f) x‖ + ‖iteratedFDeriv ℝ n (⇑g) x‖)
<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>k n : ℕ<VAR>f g : 𝓢(E, F)<VAR>x : E<GOAL>‖iteratedFDeriv ℝ n (⇑f + ⇑g) x‖ ≤ ‖iteratedFDeriv ℝ n (⇑f) x‖ + ‖iteratedFDeriv ℝ n (⇑g) x‖
<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>k n : ℕ<VAR>f g : 𝓢(E, F)<VAR>x : E<GOAL>‖iteratedFDeriv ℝ n (⇑f) x + iteratedFDeriv ℝ n (⇑g) x‖ ≤ ‖iteratedFDeriv ℝ n (⇑f) x‖ + ‖iteratedFDeriv ℝ n (⇑g) x‖
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>F : J ⥤ TopCat<VAR>U : Set ↑(colimit F)<GOAL>IsOpen U ↔ ∀ (j : J), IsOpen (⇑(colimit.ι F j) ⁻¹' U)
<VAR>ι✝ : Type u_1<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>γ : Type w<VAR>inst✝⁵ : PseudoEMetricSpace α✝<VAR>inst✝⁴ : PseudoEMetricSpace β✝<VAR>inst✝³ : PseudoEMetricSpace γ<VAR>f✝ : α✝ → β✝<VAR>x✝ y✝ z : α✝<VAR>s : Set α✝<VAR>ι : Type u_4<VAR>inst✝² : Fintype ι<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>inst✝¹ : (i : ι) → PseudoEMetricSpace (α i)<VAR>inst✝ : (i : ι) → PseudoEMetricSpace (β i)<VAR>f : (i : ι) → α i → β i<VAR>hf : ∀ (i : ι), Isometry (f i)<VAR>x y : (i : ι) → α i<GOAL>edist ((fun g i => f i (g i)) x) ((fun g i => f i (g i)) y) = edist x y
<VAR>a b : ℕ+<GOAL>(Icc a b).card = ↑b + 1 - ↑a
<VAR>a b : ℕ+<GOAL>(Icc a b).card = (Icc ↑a ↑b).card
<VAR>a b : ℕ+<GOAL>(Icc a b).card = (map (Embedding.subtype fun n => 0 < n) (Icc a b)).card
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>x : K_hat R K<VAR>hx : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, x v ∈ adicCompletionIntegers K v<GOAL>∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, (-x) v ∈ adicCompletionIntegers K v
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>x : K_hat R K<VAR>hx : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, x v ∈ adicCompletionIntegers K v<VAR>h : ∀ (v : HeightOneSpectrum R), -x v ∈ adicCompletionIntegers K v ↔ x v ∈ adicCompletionIntegers K v<GOAL>∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, (-x) v ∈ adicCompletionIntegers K v
<GOAL>∀ (x : ℝ), ContinuousAt (fun x => x * log x) x
<VAR>x : ℝ<GOAL>ContinuousAt (fun x => x * log x) x
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>ContinuousAt (fun x => x * log x) x
<GOAL>Filter.Tendsto (fun x => x * log x) (𝓝 0) (𝓝 0)
<GOAL>Filter.Tendsto (fun x => log x * x) (𝓝 0) (𝓝 0)
<GOAL>Filter.Tendsto (fun x => log x * x) (𝓝[Set.univ] 0) (𝓝 0)
<VAR>this : Set.univ = Set.Iio 0 ∪ Set.Ioi 0 ∪ {0}<GOAL>Filter.Tendsto (fun x => log x * x) (𝓝[Set.univ] 0) (𝓝 0)
<VAR>this : Set.univ = Set.Iio 0 ∪ Set.Ioi 0 ∪ {0}<GOAL>Filter.Tendsto (fun x => log x * x) (𝓝[<] 0 ⊔ 𝓝[>] 0 ⊔ 𝓝[{0}] 0) (𝓝 0)
<VAR>this : Set.univ = Set.Iio 0 ∪ Set.Ioi 0 ∪ {0}<GOAL>(Filter.Tendsto (fun x => log x * x) (𝓝[<] 0) (𝓝 0) ∧ Filter.Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)) ∧ Filter.Tendsto (fun x => log x * x) (pure 0) (𝓝 0)
<VAR>this : Set.univ = Set.Iio 0 ∪ Set.Ioi 0 ∪ {0}<GOAL>Filter.Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)
<VAR>this : Set.univ = Set.Iio 0 ∪ Set.Ioi 0 ∪ {0}<GOAL>Filter.Tendsto (fun x => log x * x) (pure 0) (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>C : ℝ<VAR>hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C<GOAL>eLpNorm f p μ ≤ μ Set.univ ^ p.toReal⁻¹ * ENNReal.ofReal C
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>C : ℝ<VAR>hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C<GOAL>eLpNorm f p μ ≤ ENNReal.ofReal C * μ Set.univ ^ p.toReal⁻¹
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a✝ b✝ c✝ d✝ a b c d : α<GOAL>(a \ b) \ c ≤ d ↔ a \ (b ⊔ c) ≤ d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Set β<GOAL>s ∩ r.codom ⊆ r.image (r.preimage s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Set β<GOAL>s ∩ r.inv.dom ⊆ r.inv.preimage (r.preimage s)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<VAR>x y z : α<GOAL>(⇑ofDual ⁻¹' s).ordSeparatingSet (⇑ofDual ⁻¹' t) = ⇑ofDual ⁻¹' s.ordSeparatingSet t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹³ : Zero β<VAR>inst✝¹² : One β<VAR>inst✝¹¹ : Add β<VAR>inst✝¹⁰ : Mul β<VAR>inst✝⁹ : Neg β<VAR>inst✝⁸ : Sub β<VAR>inst✝⁷ : SMul ℕ β<VAR>inst✝⁶ : SMul ℤ β<VAR>inst✝⁵ : Pow β ℕ<VAR>inst✝⁴ : NatCast β<VAR>inst✝³ : IntCast β<VAR>f : α → β<VAR>hf : Surjective f<VAR>inst✝² : Mul α<VAR>inst✝¹ : Add α<VAR>inst✝ : RightDistribClass α<VAR>add : ∀ (x y : α), f (x + y) = f x + f y<VAR>mul : ∀ (x y : α), f (x * y) = f x * f y<VAR>x y z : α<GOAL>(f x + f y) * f z = f x * f z + f y * f z
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>parent : Path α<VAR>x : α<VAR>b a : RBNode α<VAR>ha : RBNode.Ordered cmp a<VAR>hp : Ordered cmp parent<VAR>xb : All (fun x_1 => cmpLT cmp x x_1) b<VAR>xp : RootOrdered cmp parent x<VAR>bp : All (RootOrdered cmp parent) b<VAR>hb : RBNode.Ordered cmp b<VAR>H : All (RootOrdered cmp (left red parent x b)) a<GOAL>RBNode.Ordered cmp (parent.ins (node red a x b))
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>parent : Path α<VAR>x : α<VAR>b a : RBNode α<VAR>ha : RBNode.Ordered cmp a<VAR>hp : Ordered cmp parent<VAR>xb : All (fun x_1 => cmpLT cmp x x_1) b<VAR>xp : RootOrdered cmp parent x<VAR>bp : All (RootOrdered cmp parent) b<VAR>hb : RBNode.Ordered cmp b<VAR>H : All (RootOrdered cmp (left red parent x b)) a<VAR>ax : All (fun a => cmpLT cmp a x) a<VAR>ap : All (RootOrdered cmp parent) a<GOAL>RBNode.Ordered cmp (parent.ins (node red a x b))
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>a : RBNode α<VAR>x : α<VAR>parent : Path α<VAR>b : RBNode α<VAR>hb : RBNode.Ordered cmp b<VAR>hp : Ordered cmp parent<VAR>ax : All (fun x_1 => cmpLT cmp x_1 x) a<VAR>xp : RootOrdered cmp parent x<VAR>ap : All (RootOrdered cmp parent) a<VAR>ha : RBNode.Ordered cmp a<VAR>H : All (RootOrdered cmp (right red a x parent)) b<GOAL>RBNode.Ordered cmp (parent.ins (node red a x b))
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>a : RBNode α<VAR>x : α<VAR>parent : Path α<VAR>b : RBNode α<VAR>hb : RBNode.Ordered cmp b<VAR>hp : Ordered cmp parent<VAR>ax : All (fun x_1 => cmpLT cmp x_1 x) a<VAR>xp : RootOrdered cmp parent x<VAR>ap : All (RootOrdered cmp parent) a<VAR>ha : RBNode.Ordered cmp a<VAR>H : All (RootOrdered cmp (right red a x parent)) b<VAR>xb : All (cmpLT cmp x) b<VAR>bp : All (RootOrdered cmp parent) b<GOAL>RBNode.Ordered cmp (parent.ins (node red a x b))
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>parent : Path α<VAR>x : α<VAR>b a : RBNode α<VAR>ha : RBNode.Ordered cmp a<VAR>hp : Ordered cmp parent<VAR>xb : All (fun x_1 => cmpLT cmp x x_1) b<VAR>xp : RootOrdered cmp parent x<VAR>bp : All (RootOrdered cmp parent) b<VAR>hb : RBNode.Ordered cmp b<VAR>H : All (RootOrdered cmp (left black parent x b)) a<GOAL>RBNode.Ordered cmp (parent.ins (a.balance1 x b))
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>parent : Path α<VAR>x : α<VAR>b a : RBNode α<VAR>ha : RBNode.Ordered cmp a<VAR>hp : Ordered cmp parent<VAR>xb : All (fun x_1 => cmpLT cmp x x_1) b<VAR>xp : RootOrdered cmp parent x<VAR>bp : All (RootOrdered cmp parent) b<VAR>hb : RBNode.Ordered cmp b<VAR>H : All (RootOrdered cmp (left black parent x b)) a<VAR>ax : All (fun a => cmpLT cmp a x) a<VAR>ap : All (RootOrdered cmp parent) a<GOAL>RBNode.Ordered cmp (parent.ins (a.balance1 x b))
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>a : RBNode α<VAR>x : α<VAR>parent : Path α<VAR>b : RBNode α<VAR>hb : RBNode.Ordered cmp b<VAR>hp : Ordered cmp parent<VAR>ax : All (fun x_1 => cmpLT cmp x_1 x) a<VAR>xp : RootOrdered cmp parent x<VAR>ap : All (RootOrdered cmp parent) a<VAR>ha : RBNode.Ordered cmp a<VAR>H : All (RootOrdered cmp (right black a x parent)) b<GOAL>RBNode.Ordered cmp (parent.ins (a.balance2 x b))
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>a : RBNode α<VAR>x : α<VAR>parent : Path α<VAR>b : RBNode α<VAR>hb : RBNode.Ordered cmp b<VAR>hp : Ordered cmp parent<VAR>ax : All (fun x_1 => cmpLT cmp x_1 x) a<VAR>xp : RootOrdered cmp parent x<VAR>ap : All (RootOrdered cmp parent) a<VAR>ha : RBNode.Ordered cmp a<VAR>H : All (RootOrdered cmp (right black a x parent)) b<VAR>xb : All (cmpLT cmp x) b<VAR>bp : All (RootOrdered cmp parent) b<GOAL>RBNode.Ordered cmp (parent.ins (a.balance2 x b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<GOAL>∫⁻ (x : α), g x ∂μ - ∫⁻ (x : α), f x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<GOAL>∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ + ∫⁻ (x : α), f x ∂μ
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>f g : ↥A<GOAL>↑f ⊓ ↑g ∈ A.topologicalClosure