ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X✝ Y : C<VAR>S : Sieve X✝<VAR>R : Presieve X✝<VAR>B : C<VAR>I : Type u_1<VAR>X : I → C<VAR>π : (i : I) → X i ⟶ B<VAR>x : (i : I) → P.obj (op (X i))<VAR>hx : Compatible P π x<GOAL>∃ x', ∀ (i : I), x' (π i) ⋯ = x i
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X✝ Y : C<VAR>S : Sieve X✝<VAR>R : Presieve X✝<VAR>B : C<VAR>I : Type u_1<VAR>X : I → C<VAR>π : (i : I) → X i ⟶ B<VAR>x : (i : I) → P.obj (op (X i))<VAR>hx : Compatible P π x<VAR>i : {Z : C} → (g : Z ⟶ B) → ofArrows X π g → I<VAR>h : ∀ {Z : C} (g : Z ⟶ B) (hg : ofArrows X π g), X (i g hg) = Z<VAR>h' : ∀ {Z : C} (g : Z ⟶ B) (hg : ofArrows X π g), g = eqToHom ⋯ ≫ π (i g hg)<GOAL>∃ x', ∀ (i : I), x' (π i) ⋯ = x i
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<GOAL>∑ k ∈ range n.succ, ↑(n.choose (n - k)) / (↑n - ↑k + 1) * bernoulli' k = 1
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<GOAL>∑ x ∈ range n, (↑(n.choose x) / (↑n - ↑x + 1) * bernoulli' x - ↑(n.choose (n - x)) / (↑n - ↑x + 1) * bernoulli' x) = 0
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>η : ↥(rootsOfUnity ⟨n, hn⟩ K)<GOAL>(liftHom (X ^ n - C a) (↑↑η • root (X ^ n - C a)) ⋯) (root (X ^ n - C a)) = ↑↑η • root (X ^ n - C a)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f : X → (i : ι) → π i<VAR>i : Set ι<VAR>s : (a : ι) → Set (π a)<VAR>hs : ∀ a ∈ i, IsClosed (s a)<GOAL>IsClosed (i.pi s)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f : X → (i : ι) → π i<VAR>i : Set ι<VAR>s : (a : ι) → Set (π a)<VAR>hs : ∀ a ∈ i, IsClosed (s a)<GOAL>IsClosed (⋂ a ∈ i, eval a ⁻¹' s a)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y : C<GOAL>(λ_ (X ⊗ Y)).hom = (α_ (𝟙_ C) X Y).inv ≫ ((λ_ X).hom ⊗ 𝟙 Y)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>s : Set α<VAR>a : α<GOAL>(insert a s).Countable ↔ s.Countable
<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 : ℕ<VAR>X : C<VAR>inst✝ : Injective X<GOAL>IsZero ((F.rightDerived (n + 1)).obj 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 : ℕ<VAR>X : C<VAR>inst✝ : Injective X<GOAL>IsZero ((HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) (n + 1)).obj ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (InjectiveResolution.self X).cocomplex))
<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 : ℕ<VAR>X : C<VAR>inst✝ : Injective X<GOAL>((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (InjectiveResolution.self X).cocomplex).ExactAt (n + 1)
<VAR>ι : Type u_1<VAR>I J : Box ι<VAR>x y : ι → ℝ<GOAL>¬Disjoint ↑I ↑J ↔ (↑I ∩ ↑J).Nonempty
<GOAL>ord ∘ aleph = enumOrd {b | b.card.ord = b ∧ ω ≤ b}
<GOAL>StrictMono (ord ∘ aleph) ∧ range (ord ∘ aleph) = {b | b.card.ord = b ∧ ω ≤ b}
<GOAL>range (ord ∘ aleph) = {b | b.card.ord = b ∧ ω ≤ b}
<GOAL>(∀ (a : Ordinal.{u_1}), (ord ∘ aleph) a ∈ {b | b.card.ord = b ∧ ω ≤ b}) ∧ ∀ b ∈ {b | b.card.ord = b ∧ ω ≤ b}, ∃ a, (ord ∘ aleph) a = b
<VAR>a : Ordinal.{u_1}<GOAL>((ord ∘ aleph) a).card.ord = (ord ∘ aleph) a
<VAR>a : Ordinal.{u_1}<GOAL>ω ≤ (ord ∘ aleph) a
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0<GOAL>μ ≪ μ.withDensity f
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : (μ.withDensity f) s = 0<GOAL>μ s = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ {a | ¬s.indicator f a = 0 a} = 0<GOAL>μ s = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ {a | ¬s.indicator f a = 0 a} = 0<VAR>hf_ne_zero : μ {a | f a = 0} = 0<GOAL>μ s = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hf_ne_zero : μ {a | f a = 0} = 0<VAR>hμs : μ {a | a ∈ s ∧ ¬f a = 0} = 0<GOAL>μ s = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hf_ne_zero : μ {a | f a = 0} = 0<VAR>hμs : μ {a | a ∈ s ∧ ¬f a = 0} = 0<VAR>hle : s ⊆ {a | a ∈ s ∧ ¬f a = 0} ∪ {a | f a = 0}<GOAL>μ s = 0
<VAR>s : ℂ<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>(s + 1).GammaSeq n / s = ↑n / (↑n + 1 + s) * s.GammaSeq n
<VAR>s : ℂ<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>↑n ^ (s + 1) * ↑n ! / ((∏ x ∈ Finset.range n, (s + 1 + ↑x)) * (s + 1 + ↑n) * s) = ↑n / (↑n + 1 + s) * s.GammaSeq n
<VAR>s : ℂ<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>↑n ^ (s + 1) * ↑n ! / ((∏ x ∈ Finset.range n, (s + 1 + ↑x)) * (s + 1 + ↑n) * s) = ↑n * ↑n ^ s * ↑n ! / ((∏ k ∈ Finset.range n, (s + ↑(k + 1))) * (↑n + 1 + s) * s)
<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>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>hr : r' < r<GOAL>(fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[𝓟 (EMetric.ball (x, x) r')] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖
<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>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>r' : ℝ≥0<VAR>hr : ↑r' < r<GOAL>(fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[𝓟 (EMetric.ball (x, x) ↑r')] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖
<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>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>hr : ↑0 < r<GOAL>(fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[𝓟 (EMetric.ball (x, x) ↑0)] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖
<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>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>r' : ℝ≥0<VAR>hr : ↑r' < r<VAR>hr'0 : 0 < r'<GOAL>(fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[𝓟 (EMetric.ball (x, x) ↑r')] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖
<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>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>r' : ℝ≥0<VAR>hr : ↑r' < r<VAR>hr'0 : 0 < r'<VAR>a : ℝ<VAR>ha : a ∈ Ioo 0 1<VAR>C : ℝ<VAR>hC : 0 < C<VAR>hp : ∀ (n : ℕ), ‖p n‖ * ↑r' ^ n ≤ C * a ^ n<GOAL>(fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[𝓟 (EMetric.ball (x, x) ↑r')] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖
<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>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>r' : ℝ≥0<VAR>hr : ↑r' < r<VAR>hr'0 : 0 < r'<VAR>a : ℝ<VAR>ha : a ∈ Ioo 0 1<VAR>C : ℝ<VAR>hC : 0 < C<VAR>hp : ∀ (n : ℕ), ‖p n‖ ≤ C * a ^ n / ↑r' ^ n<GOAL>(fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[𝓟 (EMetric.ball (x, x) ↑r')] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖
<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>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>r' : ℝ≥0<VAR>hr : ↑r' < r<VAR>hr'0 : 0 < r'<VAR>a : ℝ<VAR>ha : a ∈ Ioo 0 1<VAR>C : ℝ<VAR>hC : 0 < C<VAR>hp : ∀ (n : ℕ), ‖p n‖ ≤ C * a ^ n / ↑r' ^ n<VAR>L : E × E → ℝ := fun y => C * (a / ↑r') ^ 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * (a / (1 - a) ^ 2 + 2 / (1 - a))<VAR>hL : ∀ y ∈ EMetric.ball (x, x) ↑r', ‖f y.1 - f y.2 - (p 1) fun x => y.1 - y.2‖ ≤ L y<GOAL>(fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[𝓟 (EMetric.ball (x, x) ↑r')] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖
<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>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>r' : ℝ≥0<VAR>hr : ↑r' < r<VAR>hr'0 : 0 < r'<VAR>a : ℝ<VAR>ha : a ∈ Ioo 0 1<VAR>C : ℝ<VAR>hC : 0 < C<VAR>hp : ∀ (n : ℕ), ‖p n‖ ≤ C * a ^ n / ↑r' ^ n<VAR>L : E × E → ℝ := fun y => C * (a / ↑r') ^ 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * (a / (1 - a) ^ 2 + 2 / (1 - a))<VAR>hL : ∀ y ∈ EMetric.ball (x, x) ↑r', ‖f y.1 - f y.2 - (p 1) fun x => y.1 - y.2‖ ≤ L y<GOAL>L =O[𝓟 (EMetric.ball (x, x) ↑r')] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖
<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>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>r' : ℝ≥0<VAR>hr : ↑r' < r<VAR>hr'0 : 0 < r'<VAR>a : ℝ<VAR>ha : a ∈ Ioo 0 1<VAR>C : ℝ<VAR>hC : 0 < C<VAR>hp : ∀ (n : ℕ), ‖p n‖ ≤ C * a ^ n / ↑r' ^ n<VAR>L : E × E → ℝ := fun y => C * (a / ↑r') ^ 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * (a / (1 - a) ^ 2 + 2 / (1 - a))<VAR>hL : ∀ y ∈ EMetric.ball (x, x) ↑r', ‖f y.1 - f y.2 - (p 1) fun x => y.1 - y.2‖ ≤ L y<GOAL>(fun y => C * (a / ↑r') ^ 2 * (a / (1 - a) ^ 2 + 2 / (1 - a)) * (‖y - (x, x)‖ * ‖y.1 - y.2‖)) =O[𝓟 (EMetric.ball (x, x) ↑r')] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖
<VAR>x y : ℝ<GOAL>sin (-(π / 2)) = -1
<VAR>p' : ℕ<GOAL>2 < q (p' + 2)
<VAR>p' : ℕ<GOAL>1 < p' + 2
<VAR>p' : ℕ<GOAL>(mersenne (p' + 2)).minFac ≠ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>f : α → β<VAR>g : α → γ<GOAL>(range fun x => (f x, g x)) ⊆ range f ×ˢ range g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>f : α → β<VAR>g : α → γ<VAR>this : (fun x => (f x, g x)) = Prod.map f g ∘ fun x => (x, x)<GOAL>(range fun x => (f x, g x)) ⊆ range f ×ˢ range g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>f : α → β<VAR>g : α → γ<VAR>this : (fun x => (f x, g x)) = Prod.map f g ∘ fun x => (x, x)<GOAL>range (Prod.map f g ∘ fun x => (x, x)) ⊆ range (Prod.map f g)
<VAR>n b m : ℕ<VAR>hm : m ≠ 0<GOAL>(b + 2) ^ ((b + 2).digits m).length ≤ (b + 2) * m
<VAR>n b m : ℕ<VAR>hm : m ≠ 0<VAR>this : (b + 2).digits m ≠ []<GOAL>(b + 2) ^ ((b + 2).digits m).length ≤ (b + 2) * m
<VAR>n b m : ℕ<VAR>hm : m ≠ 0<VAR>this : (b + 2).digits m ≠ []<GOAL>m = ofDigits (b + 2) ((b + 2).digits m)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : ∀ x ∈ interior D, 0 < deriv f x<VAR>x : ℝ<VAR>hx : x ∈ D<VAR>y : ℝ<VAR>hy : y ∈ D<GOAL>x < y → f x < f y
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : ∀ x ∈ interior D, 0 < deriv f x<VAR>x : ℝ<VAR>hx : x ∈ D<VAR>y : ℝ<VAR>hy : y ∈ D<VAR>this : DifferentiableOn ℝ f (interior D)<GOAL>x < y → f x < f y
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Semiring R<VAR>m n✝ : σ →₀ ℕ<VAR>φ ψ : MvPowerSeries σ R<VAR>n : σ →₀ ℕ<GOAL>(coeff R n) (1 * φ) = (coeff R n) φ
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S : Subgroupoid C<VAR>Sn : S.IsNormal<VAR>c : C<VAR>cS : c ∈ S.objs<VAR>x : c ⟶ c<VAR>hx : x ∈ S.vertexSubgroup cS<VAR>y : c ⟶ c<GOAL>y * x * y⁻¹ ∈ S.vertexSubgroup cS
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S : Subgroupoid C<VAR>Sn : S.IsNormal<VAR>c : C<VAR>cS : c ∈ S.objs<VAR>x : c ⟶ c<VAR>hx : x ∈ S.vertexSubgroup cS<VAR>y : c ⟶ c<GOAL>y * (x * y⁻¹) ∈ S.vertexSubgroup cS
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a b : α<GOAL>fract a + fract b ≤ fract (a + b) + 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a b : α<GOAL>↑⌊a + b⌋ - 1 ≤ ↑⌊a⌋ + ↑⌊b⌋
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>r : R<VAR>f : R[X]<VAR>i : ℕ<VAR>k : R<GOAL>(taylor r) ((monomial i) k) = C k * (X + C r) ^ i
<VAR>G : Type u<VAR>inst✝ : Group G<GOAL>Nat.card ↑(commutatorSet ↥(closureCommutatorRepresentatives G)) = Nat.card ↑(commutatorSet G)
<VAR>G : Type u<VAR>inst✝ : Group G<GOAL>Nat.card ↑(commutatorSet ↥(closureCommutatorRepresentatives G)) = Nat.card ↑(⇑(closureCommutatorRepresentatives G).subtype '' commutatorSet ↥(closureCommutatorRepresentatives G))
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>B : Set (Set α)<VAR>empty_mem : ∅ ∈ B<VAR>subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B<VAR>union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B<VAR>singleton_mem : ∀ (x : α), {x} ∈ B<GOAL>comk (fun x => x ∈ B) empty_mem subset_mem union_mem ≤ cofinite
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>h_add : FinMeasAdditive μ T<VAR>f : α →ₛ G<VAR>hf : Integrable (↑f) μ<VAR>g : G → F<VAR>hg : g 0 = 0<GOAL>setToSimpleFunc T (map g f) = ∑ x ∈ f.range, (T (↑f ⁻¹' {x})) (g x)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>h_add : FinMeasAdditive μ T<VAR>f : α →ₛ G<VAR>hf : Integrable (↑f) μ<VAR>g : G → F<VAR>hg : g 0 = 0<VAR>T_empty : T ∅ = 0<GOAL>setToSimpleFunc T (map g f) = ∑ x ∈ f.range, (T (↑f ⁻¹' {x})) (g x)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>h_add : FinMeasAdditive μ T<VAR>f : α →ₛ G<VAR>hf : Integrable (↑f) μ<VAR>g : G → F<VAR>hg : g 0 = 0<VAR>T_empty : T ∅ = 0<VAR>hfp : ∀ x ∈ f.range, x ≠ 0 → μ (↑f ⁻¹' {x}) ≠ ⊤<GOAL>setToSimpleFunc T (map g f) = ∑ x ∈ f.range, (T (↑f ⁻¹' {x})) (g x)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>h_add : FinMeasAdditive μ T<VAR>f : α →ₛ G<VAR>hf : Integrable (↑f) μ<VAR>g : G → F<VAR>hg : g 0 = 0<VAR>T_empty : T ∅ = 0<VAR>hfp : ∀ x ∈ f.range, x ≠ 0 → μ (↑f ⁻¹' {x}) ≠ ⊤<GOAL>∑ x ∈ Finset.image g f.range, (T (↑(map g f) ⁻¹' {x})) x = ∑ x ∈ f.range, (T (↑f ⁻¹' {x})) (g x)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>h_add : FinMeasAdditive μ T<VAR>f : α →ₛ G<VAR>hf : Integrable (↑f) μ<VAR>g : G → F<VAR>hg : g 0 = 0<VAR>T_empty : T ∅ = 0<VAR>hfp : ∀ x ∈ f.range, x ≠ 0 → μ (↑f ⁻¹' {x}) ≠ ⊤<VAR>b : G<VAR>hb : b ∈ f.range<GOAL>(T (↑(map g f) ⁻¹' {g b})) (g b) = ∑ x ∈ filter (fun c' => g c' = g b) f.range, (T (↑f ⁻¹' {x})) (g x)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>h_add : FinMeasAdditive μ T<VAR>f : α →ₛ G<VAR>hf : Integrable (↑f) μ<VAR>g : G → F<VAR>hg : g 0 = 0<VAR>T_empty : T ∅ = 0<VAR>hfp : ∀ x ∈ f.range, x ≠ 0 → μ (↑f ⁻¹' {x}) ≠ ⊤<VAR>a : α<VAR>hb : ↑f a ∈ f.range<GOAL>(T (↑(map g f) ⁻¹' {g (↑f a)})) (g (↑f a)) = ∑ x ∈ filter (fun c' => g c' = g (↑f a)) f.range, (T (↑f ⁻¹' {x})) (g x)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>h_add : FinMeasAdditive μ T<VAR>f : α →ₛ G<VAR>hf : Integrable (↑f) μ<VAR>g : G → F<VAR>hg : g 0 = 0<VAR>T_empty : T ∅ = 0<VAR>hfp : ∀ x ∈ f.range, x ≠ 0 → μ (↑f ⁻¹' {x}) ≠ ⊤<VAR>a : α<VAR>hb : ↑f a ∈ f.range<VAR>h0 : ¬g (↑f a) = 0<GOAL>(T (↑(map g f) ⁻¹' {g (↑f a)})) (g (↑f a)) = ∑ x ∈ filter (fun c' => g c' = g (↑f a)) f.range, (T (↑f ⁻¹' {x})) (g x)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>h_add : FinMeasAdditive μ T<VAR>f : α →ₛ G<VAR>hf : Integrable (↑f) μ<VAR>g : G → F<VAR>hg : g 0 = 0<VAR>T_empty : T ∅ = 0<VAR>hfp : ∀ x ∈ f.range, x ≠ 0 → μ (↑f ⁻¹' {x}) ≠ ⊤<VAR>a : α<VAR>hb : ↑f a ∈ f.range<VAR>h0 : ¬g (↑f a) = 0<VAR>h_left_eq : (T (↑(map g f) ⁻¹' {g (↑f a)})) (g (↑f a)) = (T (↑f ⁻¹' ↑(filter (fun b => g b = g (↑f a)) f.range))) (g (↑f a))<GOAL>(T (↑(map g f) ⁻¹' {g (↑f a)})) (g (↑f a)) = ∑ x ∈ filter (fun c' => g c' = g (↑f a)) f.range, (T (↑f ⁻¹' {x})) (g x)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>h_add : FinMeasAdditive μ T<VAR>f : α →ₛ G<VAR>hf : Integrable (↑f) μ<VAR>g : G → F<VAR>hg : g 0 = 0<VAR>T_empty : T ∅ = 0<VAR>hfp : ∀ x ∈ f.range, x ≠ 0 → μ (↑f ⁻¹' {x}) ≠ ⊤<VAR>a : α<VAR>hb : ↑f a ∈ f.range<VAR>h0 : ¬g (↑f a) = 0<VAR>h_left_eq : (T (↑(map g f) ⁻¹' {g (↑f a)})) (g (↑f a)) = (T (↑f ⁻¹' ↑(filter (fun b => g b = g (↑f a)) f.range))) (g (↑f a))<GOAL>(T (↑f ⁻¹' ↑(filter (fun b => g b = g (↑f a)) f.range))) (g (↑f a)) = ∑ x ∈ filter (fun c' => g c' = g (↑f a)) f.range, (T (↑f ⁻¹' {x})) (g x)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>h_add : FinMeasAdditive μ T<VAR>f : α →ₛ G<VAR>hf : Integrable (↑f) μ<VAR>g : G → F<VAR>hg : g 0 = 0<VAR>T_empty : T ∅ = 0<VAR>hfp : ∀ x ∈ f.range, x ≠ 0 → μ (↑f ⁻¹' {x}) ≠ ⊤<VAR>a : α<VAR>hb : ↑f a ∈ f.range<VAR>h0 : ¬g (↑f a) = 0<VAR>h_left_eq : (T (↑(map g f) ⁻¹' {g (↑f a)})) (g (↑f a)) = (T (↑f ⁻¹' ↑(filter (fun b => g b = g (↑f a)) f.range))) (g (↑f a))<VAR>h_left_eq' : (T (↑f ⁻¹' ↑(filter (fun b => g b = g (↑f a)) f.range))) (g (↑f a)) = (T (⋃ y ∈ filter (fun b => g b = g (↑f a)) f.range, ↑f ⁻¹' {y})) (g (↑f a))<GOAL>(T (↑f ⁻¹' ↑(filter (fun b => g b = g (↑f a)) f.range))) (g (↑f a)) = ∑ x ∈ filter (fun c' => g c' = g (↑f a)) f.range, (T (↑f ⁻¹' {x})) (g x)