ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace Y<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>hs : MeasurableSet s<GOAL>LocallyIntegrable (fun x => f ↑x) (comap Subtype.val μ) ↔ ∀ (x : { a // a ∈ s }), IntegrableAtFilter f (Filter.map Subtype.val (𝓝 x)) μ
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>inst✝⁵ : T2Space β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace α<VAR>s : Set γ<VAR>f : γ → β<VAR>tγ : TopologicalSpace γ<VAR>inst✝² : PolishSpace γ<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : BorelSpace γ<GOAL>IsClopenable s ↔ MeasurableSet s
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>inst✝⁵ : T2Space β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace α<VAR>s : Set γ<VAR>f : γ → β<VAR>tγ : TopologicalSpace γ<VAR>inst✝² : PolishSpace γ<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : BorelSpace γ<VAR>hs : IsClopenable s<GOAL>MeasurableSet s
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>inst✝⁴ : T2Space β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace α<VAR>s : Set γ<VAR>f : γ → β<VAR>tγ : TopologicalSpace γ<VAR>inst✝¹ : PolishSpace γ<VAR>hs : IsClopenable s<VAR>inst✝ : BorelSpace γ<VAR>this✝ : MeasurableSpace γ := borel γ<GOAL>MeasurableSet s
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>inst✝⁴ : T2Space β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace α<VAR>s : Set γ<VAR>f : γ → β<VAR>tγ : TopologicalSpace γ<VAR>inst✝¹ : PolishSpace γ<VAR>inst✝ : BorelSpace γ<VAR>this✝ : MeasurableSpace γ := borel γ<VAR>t' : TopologicalSpace γ<VAR>t't : t' ≤ tγ<VAR>t'_polish : PolishSpace γ<VAR>left✝ : IsClosed s<VAR>s_open : IsOpen s<GOAL>MeasurableSet s
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>inst✝⁴ : T2Space β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace α<VAR>s : Set γ<VAR>f : γ → β<VAR>tγ : TopologicalSpace γ<VAR>inst✝¹ : PolishSpace γ<VAR>inst✝ : BorelSpace γ<VAR>this✝ : MeasurableSpace γ := borel γ<VAR>t' : TopologicalSpace γ<VAR>t't : t' ≤ tγ<VAR>t'_polish : PolishSpace γ<VAR>left✝ : IsClosed s<VAR>s_open : IsOpen s<GOAL>PolishSpace γ
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : TopologicalSpace β✝<VAR>inst✝ : TopologicalSpace γ<VAR>f✝ g✝ : α → β✝<VAR>β : Type u_4<VAR>f : α → β<VAR>mα : MeasurableSpace α<VAR>μa : Measure α<VAR>mβ : MeasurableSpace β<VAR>μb : Measure β<VAR>hf : MeasurePreserving f μa μb<VAR>h₂ : MeasurableEmbedding f<VAR>g : β → γ<GOAL>AEStronglyMeasurable (g ∘ f) μa ↔ AEStronglyMeasurable g μb
<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>s : Set β<VAR>hs : MeasurableSet s<GOAL>Measurable fun p => (κ p.1) (countablePartitionSet n p.2 ×ˢ s) / (ν p.1) (countablePartitionSet n p.2)
<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>s : Set β<VAR>hs : MeasurableSet s<GOAL>Measurable ((fun p => (κ p.1) (↑p.2 ×ˢ s) / (ν p.1) ↑p.2) ∘ fun p => (p.1, ⟨countablePartitionSet n p.2, ⋯⟩))
<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>s : Set β<VAR>hs : MeasurableSet s<VAR>h1 : Measurable fun p => (κ p.1) (↑p.2 ×ˢ s) / (ν p.1) ↑p.2<GOAL>Measurable ((fun p => (κ p.1) (↑p.2 ×ˢ s) / (ν p.1) ↑p.2) ∘ fun p => (p.1, ⟨countablePartitionSet n p.2, ⋯⟩))
<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>s : Set β<VAR>hs : MeasurableSet s<VAR>h1 : Measurable fun p => (κ p.1) (↑p.2 ×ˢ s) / (ν p.1) ↑p.2<GOAL>Measurable fun p => ⟨countablePartitionSet n p.2, ⋯⟩
<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>s : Set β<VAR>hs : MeasurableSet s<VAR>h1 : Measurable fun p => (κ p.1) (↑p.2 ×ˢ s) / (ν p.1) ↑p.2<GOAL>Measurable ((fun c => ⟨countablePartitionSet n c, ⋯⟩) ∘ fun p => p.2)
<VAR>α : Type u_1<VAR>inst✝² : Group α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>max a 1 / max a⁻¹ 1 = a
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>h : p.degree < q.degree<GOAL>(p - q).degree = q.degree
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>h : p.degree < (-q).degree<GOAL>(p - q).degree = q.degree
<VAR>a b : ℕ+<GOAL>(Ioc a b).card = ↑b - ↑a
<VAR>a b : ℕ+<GOAL>(Ioc a b).card = (Ioc ↑a ↑b).card
<VAR>a b : ℕ+<GOAL>(Ioc a b).card = (map (Embedding.subtype fun n => 0 < n) (Ioc a b)).card
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>a : α<VAR>as : a ∈ s<VAR>b : α<VAR>bs : b ∈ s<VAR>c : α<VAR>cs : c ∈ s<VAR>bc : b ≤ c<GOAL>variationOnFromTo f s a b ≤ variationOnFromTo f s a c
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>a : α<VAR>as : a ∈ s<VAR>b : α<VAR>bs : b ∈ s<VAR>c : α<VAR>cs : c ∈ s<VAR>bc : b ≤ c<GOAL>variationOnFromTo f s a b ≤ variationOnFromTo f s a b + variationOnFromTo f s b c
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : ℕ → R<VAR>i : Fin n<GOAL>TruncatedWittVector.coeff i ((truncate n) { coeff := f }) = TruncatedWittVector.coeff i (TruncatedWittVector.mk p fun k => f ↑k)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝ : CommMonoid β<VAR>s : Finset ι<VAR>t : ι → Finset α<VAR>h : (↑s).PairwiseDisjoint t<GOAL>∏ x ∈ s.disjiUnion t h, f x = ∏ i ∈ s, ∏ x ∈ t i, f x
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝ : CommMonoid β<VAR>s : Finset ι<VAR>t : ι → Finset α<VAR>h : (↑s).PairwiseDisjoint t<GOAL>∏ x ∈ s.disjiUnion t h, f x = fold (fun x x_1 => x * x_1) (fold (fun x x_1 => x * x_1) 1 (fun i => 1) s) (fun x => f x) (s.disjiUnion t h)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝ : CommMonoid β<VAR>s : Finset ι<VAR>t : ι → Finset α<VAR>h : (↑s).PairwiseDisjoint t<GOAL>1 = Multiset.foldr (fun x x_1 => x * x_1) ⋯ 1 (Multiset.map (fun i => 1) s.val)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.58582, u_1} C<VAR>inst✝¹ : Category.{?u.58586, u_2} D<VAR>inst✝ : Category.{?u.58590, u_3} E<VAR>F : C ⥤ Karoubi D<VAR>P : Karoubi C<GOAL>((F.map P.p).f ≫ (F.obj P.X).p) ≫ (F.map P.p).f = (F.map P.p).f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<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>p : FormalMultilinearSeries 𝕜 E F<VAR>x✝ y : E<VAR>r R : ℝ≥0<VAR>k l : ℕ<VAR>x : E<GOAL>‖(p.changeOriginSeries k l) fun x_1 => x‖₊ ≤ ∑' (x_1 : { s // s.card = l }), ‖p (k + l)‖₊ * ‖x‖₊ ^ l
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<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>p : FormalMultilinearSeries 𝕜 E F<VAR>x✝ y : E<VAR>r R : ℝ≥0<VAR>k l : ℕ<VAR>x : E<GOAL>‖(p.changeOriginSeries k l) fun x_1 => x‖₊ ≤ (∑' (x : { s // s.card = l }), ‖p (k + l)‖₊) * ∏ _i : Fin l, ‖x‖₊
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝¹ : μ.HaveLebesgueDecomposition ν<VAR>inst✝ : SigmaFinite ν<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(μ.restrict s).rnDeriv ν =ᶠ[ae ν] s.indicator (μ.rnDeriv ν)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝¹ : μ.HaveLebesgueDecomposition ν<VAR>inst✝ : SigmaFinite ν<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>μ.restrict s = (μ.restrict s).singularPart ν + ν.withDensity (s.indicator (μ.rnDeriv ν))
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<GOAL>↑(hC.diffFinset hs ht) ⊆ C
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<GOAL>(eval P) W'.polynomialY = 2 * P y + W'.a₁ * P x * P z + W'.a₃ * P z ^ 3
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<GOAL>(eval P) (C 2 * X y + C W'.a₁ * X x * X z + C W'.a₃ * X z ^ 3) = 2 * P y + W'.a₁ * P x * P z + W'.a₃ * P z ^ 3
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>hG : IsPGroup p G<VAR>hp : Fact (Nat.Prime p)<GOAL>Nat.card G = 1 ∨ p ∣ Nat.card G
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>hG : IsPGroup p G<VAR>hp : Fact (Nat.Prime p)<VAR>h✝ : Finite G<GOAL>Nat.card G = 1 ∨ p ∣ Nat.card G
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>hG : IsPGroup p G<VAR>hp : Fact (Nat.Prime p)<VAR>h✝ : Infinite G<GOAL>Nat.card G = 1 ∨ p ∣ Nat.card G
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f✝ : Filter α<VAR>s : Set α<VAR>a : α<VAR>f f' : Filter α<GOAL>⨆ g, ⨆ (_ : ↑g ≤ f), ↑g ≤ f' ↔ f ≤ f'
<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>f : E → F<VAR>x₀ : E<VAR>s : Set E<VAR>hs : s ∈ 𝓝 x₀<VAR>C : ℝ≥0<VAR>hlip : LipschitzOnWith C f s<GOAL>‖fderiv 𝕜 f x₀‖ ≤ ↑C
<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>f : E → F<VAR>x₀ : E<VAR>s : Set E<VAR>hs : s ∈ 𝓝 x₀<VAR>C : ℝ≥0<VAR>hlip : LipschitzOnWith C f s<GOAL>∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ ↑C * ‖x - x₀‖
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F G F₁ F₂ : C ⥤ Type w<VAR>τ₁ : F ⟶ F₁<VAR>τ₂ : F ⟶ F₂<VAR>x✝² x✝¹ : C<VAR>x✝ : x✝² ⟶ x✝¹<VAR>a : F.obj x✝²<GOAL>(F.map x✝ ≫ (fun x y => (τ₁.app x y, τ₂.app x y)) x✝¹) a = ((fun x y => (τ₁.app x y, τ₂.app x y)) x✝² ≫ (prod F₁ F₂).map x✝) a
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F G F₁ F₂ : C ⥤ Type w<VAR>τ₁ : F ⟶ F₁<VAR>τ₂ : F ⟶ F₂<VAR>x✝² x✝¹ : C<VAR>x✝ : x✝² ⟶ x✝¹<VAR>a : F.obj x✝²<GOAL>(F₁.map x✝ (τ₁.app x✝² a), F₂.map x✝ (τ₂.app x✝² a)) = (prod F₁ F₂).map x✝ (τ₁.app x✝² a, τ₂.app x✝² a)
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>P : Set X → Prop<VAR>c : CU P<VAR>x : X<VAR>h : x ∉ c.U<GOAL>c.lim x = 1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<VAR>h : x ⤳ y<VAR>hd : _root_.Disjoint (𝓝 x) (𝓝 y)<GOAL>¬_root_.Disjoint (𝓝 x) (𝓝 x)
<VAR>X : TopCat<VAR>U : Opens ↑X<GOAL>↑((map U.inclusion).obj U) = ↑⊤
<VAR>xl xr : Type u<VAR>xL : xl → PGame<VAR>i : xr<VAR>xR : xr → PGame<VAR>j : (xR i).RightMoves<GOAL>((xR i).moveRight j).Subsequent (mk xl xr xL xR)
<VAR>f : StieltjesFunction<GOAL>∀ᵐ (x : ℝ), HasDerivAt (↑f) (f.measure.rnDeriv volume x).toReal x
<VAR>f : StieltjesFunction<VAR>x : ℝ<VAR>hx : Tendsto (fun a => f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x))<VAR>h'x : f.measure.rnDeriv volume x < ⊤<VAR>h''x : ¬leftLim (↑f) x ≠ ↑f x<GOAL>HasDerivAt (↑f) (f.measure.rnDeriv volume x).toReal x
<VAR>f : StieltjesFunction<VAR>x : ℝ<VAR>hx : Tendsto (fun a => f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x))<VAR>h'x : f.measure.rnDeriv volume x < ⊤<VAR>h''x : ¬leftLim (↑f) x ≠ ↑f x<VAR>L1 : Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[>] x) (𝓝 (f.measure.rnDeriv volume x).toReal)<GOAL>HasDerivAt (↑f) (f.measure.rnDeriv volume x).toReal x
<VAR>f : StieltjesFunction<VAR>x : ℝ<VAR>hx : Tendsto (fun a => f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x))<VAR>h'x : f.measure.rnDeriv volume x < ⊤<VAR>h''x : ¬leftLim (↑f) x ≠ ↑f x<VAR>L1 : Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[>] x) (𝓝 (f.measure.rnDeriv volume x).toReal)<VAR>L2 : Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[<] x) (𝓝 (f.measure.rnDeriv volume x).toReal)<GOAL>HasDerivAt (↑f) (f.measure.rnDeriv volume x).toReal x
<VAR>f : StieltjesFunction<VAR>x : ℝ<VAR>hx : Tendsto (fun a => f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x))<VAR>h'x : f.measure.rnDeriv volume x < ⊤<VAR>h''x : ¬leftLim (↑f) x ≠ ↑f x<VAR>L1 : Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[>] x) (𝓝 (f.measure.rnDeriv volume x).toReal)<VAR>L2 : Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[<] x) (𝓝 (f.measure.rnDeriv volume x).toReal)<VAR>L3 : Tendsto (fun y => (leftLim (↑f) (y + 1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[<] x) (𝓝 (f.measure.rnDeriv volume x).toReal)<VAR>L4 : Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[<] x) (𝓝 (f.measure.rnDeriv volume x).toReal)<GOAL>HasDerivAt (↑f) (f.measure.rnDeriv volume x).toReal x
<VAR>f : StieltjesFunction<VAR>x : ℝ<VAR>hx : Tendsto (fun a => f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x))<VAR>h'x : f.measure.rnDeriv volume x < ⊤<VAR>h''x : ¬leftLim (↑f) x ≠ ↑f x<VAR>L1 : Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[>] x) (𝓝 (f.measure.rnDeriv volume x).toReal)<VAR>L2 : Tendsto (fun y => (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[<] x) (𝓝 (f.measure.rnDeriv volume x).toReal)<VAR>L3 : Tendsto (fun y => (leftLim (↑f) (y + 1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[<] x) (𝓝 (f.measure.rnDeriv volume x).toReal)<VAR>L4 : Tendsto (fun y => (↑f y - ↑f x) / (y - x)) (𝓝[<] x) (𝓝 (f.measure.rnDeriv volume x).toReal)<GOAL>Tendsto (fun b => (↑f b - ↑f x) / (b - x)) (𝓝[<] x) (𝓝 (f.measure.rnDeriv volume x).toReal) ∧ Tendsto (fun b => (↑f b - ↑f x) / (b - x)) (𝓝[>] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>∫ (x : ℝ) in a..b, rexp x = rexp b - rexp a
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>deriv rexp = rexp
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>∀ x ∈ [[a, b]], DifferentiableAt ℝ rexp x
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>ContinuousOn rexp [[a, b]]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>ts : List α<GOAL>ts.permutations ~ ts.permutations'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>ts : List α<VAR>n : ℕ<VAR>h : ts.length < n<GOAL>ts.permutations ~ ts.permutations'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>n : ℕ<VAR>IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'<VAR>ts✝ : List α<VAR>h✝ : ts✝.length < n + 1<VAR>ts : List α<VAR>t : α<VAR>x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'<VAR>h : (ts ++ [t]).length < n + 1<GOAL>(ts ++ [t]).permutations ~ (ts ++ [t]).permutations'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>n : ℕ<VAR>IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'<VAR>ts✝ : List α<VAR>h✝ : ts✝.length < n + 1<VAR>ts : List α<VAR>t : α<VAR>x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'<VAR>h : ts.length < n<GOAL>(ts ++ [t]).permutations ~ (ts ++ [t]).permutations'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>n : ℕ<VAR>IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'<VAR>ts✝ : List α<VAR>h✝ : ts✝.length < n + 1<VAR>ts : List α<VAR>t : α<VAR>x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'<VAR>h : ts.length < n<VAR>IH₂ : ts.reverse.permutations ~ ts.permutations'<GOAL>(ts ++ [t]).permutations ~ (ts ++ [t]).permutations'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>n : ℕ<VAR>IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'<VAR>ts✝ : List α<VAR>h✝ : ts✝.length < n + 1<VAR>ts : List α<VAR>t : α<VAR>x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'<VAR>h : ts.length < n<VAR>IH₂ : ts.reverse.permutations ~ ts.permutations'<GOAL>(map (fun x => x ++ [t]) ts.permutations ++ ts.reverse.permutations.bind fun y => (permutationsAux2 t [] [] y id).2) ~ (ts ++ [t]).permutations'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>n : ℕ<VAR>IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'<VAR>ts✝ : List α<VAR>h✝ : ts✝.length < n + 1<VAR>ts : List α<VAR>t : α<VAR>x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'<VAR>h : ts.length < n<VAR>IH₂ : ts.reverse.permutations ~ ts.permutations'<GOAL>(ts.permutations'.bind fun y => (permutationsAux2 t [] [] y id).2) ++ map (fun x => x ++ [t]) ts.permutations' ~ ([t] ++ ts).permutations'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>n : ℕ<VAR>IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'<VAR>ts✝ : List α<VAR>h✝ : ts✝.length < n + 1<VAR>ts : List α<VAR>t : α<VAR>x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'<VAR>h : ts.length < n<VAR>IH₂ : ts.reverse.permutations ~ ts.permutations'<GOAL>((ts.permutations'.bind fun y => (permutationsAux2 t [] [] y id).2) ++ ts.permutations'.bind fun x => [x ++ [t]]) ~ ts.permutations'.bind (permutations'Aux t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>n : ℕ<VAR>IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'<VAR>ts✝ : List α<VAR>h✝ : ts✝.length < n + 1<VAR>ts : List α<VAR>t : α<VAR>x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'<VAR>h : ts.length < n<VAR>IH₂ : ts.reverse.permutations ~ ts.permutations'<GOAL>(ts.permutations'.bind fun x => (permutationsAux2 t [] [] x id).2 ++ [x ++ [t]]) ~ ts.permutations'.bind (permutations'Aux t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>n : ℕ<VAR>IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'<VAR>ts✝ : List α<VAR>h✝ : ts✝.length < n + 1<VAR>ts : List α<VAR>t : α<VAR>x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'<VAR>h : ts.length < n<VAR>IH₂ : ts.reverse.permutations ~ ts.permutations'<GOAL>(ts.permutations'.bind fun x => (permutationsAux2 t [] [] x id).2 ++ [x ++ [t]]) = ts.permutations'.bind (permutations'Aux t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>n : ℕ<VAR>IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'<VAR>ts✝ : List α<VAR>h✝ : ts✝.length < n + 1<VAR>ts : List α<VAR>t : α<VAR>x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'<VAR>h : ts.length < n<VAR>IH₂ : ts.reverse.permutations ~ ts.permutations'<GOAL>(fun x => (permutationsAux2 t [] [] x id).2 ++ [x ++ [t]]) = permutations'Aux t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>n : ℕ<VAR>IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'<VAR>ts✝ : List α<VAR>h✝ : ts✝.length < n + 1<VAR>ts : List α<VAR>t : α<VAR>x✝¹ : ts.length < n + 1 → ts.permutations ~ ts.permutations'<VAR>h : ts.length < n<VAR>IH₂ : ts.reverse.permutations ~ ts.permutations'<VAR>x✝ : List α<GOAL>(permutationsAux2 t [] [] x✝ id).2 ++ [x✝ ++ [t]] = permutations'Aux t x✝
<VAR>α : Type ?u.51176<VAR>inst✝¹ : MulZeroOneClass α<VAR>inst✝ : HasDistribNeg α<VAR>x y : SignType<GOAL>{ toFun := cast, map_zero' := ⋯ }.toFun (x * y) = { toFun := cast, map_zero' := ⋯ }.toFun x * { toFun := cast, map_zero' := ⋯ }.toFun y
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s t : Subgroup α<VAR>h_le : s ≤ t<VAR>f : α ⧸ t → α<VAR>hf : Function.RightInverse f QuotientGroup.mk<VAR>a : α ⧸ s<VAR>b c : α<VAR>h : Setoid.r b c<GOAL>Setoid.r ((fun g => ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) b) ((fun g => ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) c)
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s t : Subgroup α<VAR>h_le : s ≤ t<VAR>f : α ⧸ t → α<VAR>hf : Function.RightInverse f QuotientGroup.mk<VAR>a : α ⧸ s<VAR>b c : α<VAR>h : Setoid.r b c<GOAL>((fun g => ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) b)⁻¹ * (fun g => ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) c ∈ s.subgroupOf t
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s t : Subgroup α<VAR>h_le : s ≤ t<VAR>f : α ⧸ t → α<VAR>hf : Function.RightInverse f QuotientGroup.mk<VAR>a : α ⧸ s<VAR>b c : α<VAR>h : Setoid.r b c<GOAL>((f ↑b)⁻¹ * b)⁻¹ * ((f ↑c)⁻¹ * c) ∈ s
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s t : Subgroup α<VAR>h_le : s ≤ t<VAR>f : α ⧸ t → α<VAR>hf : Function.RightInverse f QuotientGroup.mk<VAR>a : α ⧸ s<VAR>b c : α<VAR>h : Setoid.r b c<VAR>key : f ↑b = f ↑c<GOAL>((f ↑b)⁻¹ * b)⁻¹ * ((f ↑c)⁻¹ * c) ∈ s
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s t : Subgroup α<VAR>h_le : s ≤ t<VAR>f : α ⧸ t → α<VAR>hf : Function.RightInverse f QuotientGroup.mk<VAR>a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t<GOAL>α ⧸ s
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s t : Subgroup α<VAR>h_le : s ≤ t<VAR>f : α ⧸ t → α<VAR>hf : Function.RightInverse f QuotientGroup.mk<GOAL>LeftInverse (fun a => Quotient.map' (fun b => f a.1 * ↑b) ⋯ a.2) fun a => (Quotient.map' id ⋯ a, Quotient.map' (fun g => ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) ⋯ a)
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s t : Subgroup α<VAR>h_le : s ≤ t<VAR>f : α ⧸ t → α<VAR>hf : Function.RightInverse f QuotientGroup.mk<VAR>a : α<GOAL>(fun a => Quotient.map' (fun b => f a.1 * ↑b) ⋯ a.2) ((fun a => (Quotient.map' id ⋯ a, Quotient.map' (fun g => ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) ⋯ a)) (Quotient.mk'' a)) = Quotient.mk'' a
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s t : Subgroup α<VAR>h_le : s ≤ t<VAR>f : α ⧸ t → α<VAR>hf : Function.RightInverse f QuotientGroup.mk<GOAL>∀ (fst : α ⧸ t) (snd : ↥t ⧸ s.subgroupOf t), (fun a => (Quotient.map' id ⋯ a, Quotient.map' (fun g => ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) ⋯ a)) ((fun a => Quotient.map' (fun b => f a.1 * ↑b) ⋯ a.2) (fst, snd)) = (fst, snd)
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s t : Subgroup α<VAR>h_le : s ≤ t<VAR>f : α ⧸ t → α<VAR>hf : Function.RightInverse f QuotientGroup.mk<VAR>a : α<GOAL>∀ (snd : ↥t ⧸ s.subgroupOf t), (fun a => (Quotient.map' id ⋯ a, Quotient.map' (fun g => ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) ⋯ a)) ((fun a => Quotient.map' (fun b => f a.1 * ↑b) ⋯ a.2) (Quotient.mk'' a, snd)) = (Quotient.mk'' a, snd)