ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>inst✝³ : Group α<VAR>inst✝² : LT α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c d : α<GOAL>a * b⁻¹ < d⁻¹ * c ↔ d * a < c * b
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>a : α<VAR>s : Set α<VAR>inst✝ : Fintype ↑s<VAR>h : a ∉ s<VAR>d : Fintype ↑(insert a s)<GOAL>Fintype.card ↑(insert a s) = Fintype.card ↑s + 1
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>a : α<VAR>s : Set α<VAR>inst✝ : Fintype ↑s<VAR>h : a ∉ s<VAR>d : Fintype ↑(insert a s)<GOAL>Fintype.card ↑(insert a s) = Fintype.card ↑(insert a s)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>b : β<GOAL>comap m (pure b) = 𝓟 (m ⁻¹' {b})
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<GOAL>⊥.relindex H = Nat.card ↥H
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>hab : a < b<VAR>hn : upcrossingsBefore a b f N ω < n<GOAL>stoppedValue f (upperCrossingTime a b f N (n + 1)) ω - stoppedValue f (lowerCrossingTime a b f N n) ω = 0
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>hab : a < b<VAR>hn : upcrossingsBefore a b f N ω < n<VAR>this : N ≤ upperCrossingTime a b f N n ω<GOAL>stoppedValue f (upperCrossingTime a b f N (n + 1)) ω - stoppedValue f (lowerCrossingTime a b f N n) ω = 0
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>s t : Set α<VAR>a x y : α<VAR>inst✝¹ : AlexandrovDiscrete α<VAR>inst✝ : AlexandrovDiscrete β<VAR>f : β → α<VAR>h : Inducing f<VAR>S : Set (Set β)<VAR>hS : ∀ s ∈ S, IsOpen s<GOAL>IsOpen (⋂₀ S)
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>s t : Set α<VAR>a x y : α<VAR>inst✝¹ : AlexandrovDiscrete α<VAR>inst✝ : AlexandrovDiscrete β<VAR>f : β → α<VAR>h : Inducing f<VAR>S : Set (Set β)<VAR>hS : ∀ s ∈ S, ∃ t, IsOpen t ∧ f ⁻¹' t = s<GOAL>∃ t, IsOpen t ∧ f ⁻¹' t = ⋂₀ S
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>s t : Set α<VAR>a x y : α<VAR>inst✝¹ : AlexandrovDiscrete α<VAR>inst✝ : AlexandrovDiscrete β<VAR>f : β → α<VAR>h : Inducing f<VAR>S : Set (Set β)<VAR>U : (s : Set β) → s ∈ S → Set α<VAR>hU : ∀ (s : Set β) (a : s ∈ S), IsOpen (U s a)<VAR>htU : ∀ (s : Set β) (a : s ∈ S), f ⁻¹' U s a = s<GOAL>∃ t, IsOpen t ∧ f ⁻¹' t = ⋂₀ S
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>s t : Set α<VAR>a x y : α<VAR>inst✝¹ : AlexandrovDiscrete α<VAR>inst✝ : AlexandrovDiscrete β<VAR>f : β → α<VAR>h : Inducing f<VAR>S : Set (Set β)<VAR>U : (s : Set β) → s ∈ S → Set α<VAR>hU : ∀ (s : Set β) (a : s ∈ S), IsOpen (U s a)<VAR>htU : ∀ (s : Set β) (a : s ∈ S), f ⁻¹' U s a = s<GOAL>f ⁻¹' ⋂ i, ⋂ (j : i ∈ S), U i j = ⋂₀ S
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : MeasurableSpace α<VAR>f : α → 𝕜<VAR>μ : MeasureTheory.Measure α<VAR>hre : Measurable fun x => RCLike.re (f x)<VAR>him : Measurable fun x => RCLike.im (f x)<GOAL>Measurable f
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : MeasurableSpace α<VAR>f : α → 𝕜<VAR>μ : MeasureTheory.Measure α<VAR>hre : Measurable fun x => RCLike.re (f x)<VAR>him : Measurable fun x => RCLike.im (f x)<VAR>x✝ : α<GOAL>f x✝ = (RCLike.ofReal ∘ fun x => RCLike.re (f x)) x✝ + (RCLike.ofReal ∘ fun x => RCLike.im (f x)) x✝ * RCLike.I
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>I : Type u_3<VAR>J : Type u_4<VAR>inst✝⁷ : Category.{u_6, u_1} C<VAR>inst✝⁶ : Category.{u_5, u_2} D<VAR>inst✝⁵ : Zero I<VAR>inst✝⁴ : DecidableEq I<VAR>inst✝³ : HasInitial C<VAR>F : C ⥤ D ⥤ D<VAR>X : C<VAR>e : F.obj X ≅ 𝟭 D<VAR>inst✝² : (Y : D) → PreservesColimit (Functor.empty C) (F.flip.obj Y)<VAR>p : I × J → J<VAR>hp : ∀ (j : J), p (0, j) = j<VAR>Y Y' : GradedObject J D<VAR>φ : Y ⟶ Y'<VAR>inst✝¹ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p<VAR>inst✝ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y').HasMap p<VAR>j : J<GOAL>φ j ≫ (mapBifunctorLeftUnitor F X e p hp Y').inv j = (mapBifunctorLeftUnitor F X e p hp Y).inv j ≫ mapBifunctorMapMap F p (𝟙 ((single₀ I).obj X)) φ j
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>I : Type u_3<VAR>J : Type u_4<VAR>inst✝⁷ : Category.{u_6, u_1} C<VAR>inst✝⁶ : Category.{u_5, u_2} D<VAR>inst✝⁵ : Zero I<VAR>inst✝⁴ : DecidableEq I<VAR>inst✝³ : HasInitial C<VAR>F : C ⥤ D ⥤ D<VAR>X : C<VAR>e : F.obj X ≅ 𝟭 D<VAR>inst✝² : (Y : D) → PreservesColimit (Functor.empty C) (F.flip.obj Y)<VAR>p : I × J → J<VAR>hp : ∀ (j : J), p (0, j) = j<VAR>Y Y' : GradedObject J D<VAR>φ : Y ⟶ Y'<VAR>inst✝¹ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p<VAR>inst✝ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y').HasMap p<VAR>j : J<GOAL>φ j ≫ e.inv.app (Y' j) ≫ (F.map (singleObjApplyIso 0 X).inv).app (Y' j) ≫ ιMapBifunctorMapObj F p ((single₀ I).obj X) Y' 0 j j ⋯ = e.inv.app (Y j) ≫ (F.map (singleObjApplyIso 0 X).inv).app (Y j) ≫ (F.map (𝟙 ((single₀ I).obj X) 0)).app (Y j) ≫ (F.obj ((single₀ I).obj X 0)).map (φ j) ≫ ιMapBifunctorMapObj F p ((single₀ I).obj X) Y' 0 j j ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>I : Type u_3<VAR>J : Type u_4<VAR>inst✝⁷ : Category.{u_6, u_1} C<VAR>inst✝⁶ : Category.{u_5, u_2} D<VAR>inst✝⁵ : Zero I<VAR>inst✝⁴ : DecidableEq I<VAR>inst✝³ : HasInitial C<VAR>F : C ⥤ D ⥤ D<VAR>X : C<VAR>e : F.obj X ≅ 𝟭 D<VAR>inst✝² : (Y : D) → PreservesColimit (Functor.empty C) (F.flip.obj Y)<VAR>p : I × J → J<VAR>hp : ∀ (j : J), p (0, j) = j<VAR>Y Y' : GradedObject J D<VAR>φ : Y ⟶ Y'<VAR>inst✝¹ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p<VAR>inst✝ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y').HasMap p<VAR>j : J<GOAL>φ j ≫ e.inv.app (Y' j) ≫ (F.map (singleObjApplyIso 0 X).inv).app (Y' j) ≫ ιMapBifunctorMapObj F p ((single₀ I).obj X) Y' 0 j j ⋯ = e.inv.app (Y j) ≫ (F.map (singleObjApplyIso 0 X).inv).app (Y j) ≫ (F.map (𝟙 ((single₀ I).obj X 0))).app (Y j) ≫ (F.obj ((single₀ I).obj X 0)).map (φ j) ≫ ιMapBifunctorMapObj F p ((single₀ I).obj X) Y' 0 j j ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>I : Type u_3<VAR>J : Type u_4<VAR>inst✝⁷ : Category.{u_6, u_1} C<VAR>inst✝⁶ : Category.{u_5, u_2} D<VAR>inst✝⁵ : Zero I<VAR>inst✝⁴ : DecidableEq I<VAR>inst✝³ : HasInitial C<VAR>F : C ⥤ D ⥤ D<VAR>X : C<VAR>e : F.obj X ≅ 𝟭 D<VAR>inst✝² : (Y : D) → PreservesColimit (Functor.empty C) (F.flip.obj Y)<VAR>p : I × J → J<VAR>hp : ∀ (j : J), p (0, j) = j<VAR>Y Y' : GradedObject J D<VAR>φ : Y ⟶ Y'<VAR>inst✝¹ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p<VAR>inst✝ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y').HasMap p<VAR>j : J<GOAL>φ j ≫ e.inv.app (Y' j) ≫ (F.map (singleObjApplyIso 0 X).inv).app (Y' j) ≫ ιMapBifunctorMapObj F p ((single₀ I).obj X) Y' 0 j j ⋯ = e.inv.app (Y j) ≫ (F.map (singleObjApplyIso 0 X).inv).app (Y j) ≫ (F.obj ((single₀ I).obj X 0)).map (φ j) ≫ ιMapBifunctorMapObj F p ((single₀ I).obj X) Y' 0 j j ⋯
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : InnerProductSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : InnerProductSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : InnerProductSpace ℝ E'<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<GOAL>(∀ (x : E), ⟪T x, x⟫_𝕜 = 0) ↔ T = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : InnerProductSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : InnerProductSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : InnerProductSpace ℝ E'<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<GOAL>(∀ (x : E), ⟪T x, x⟫_𝕜 = 0) ↔ ∀ (x : E), T x = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : InnerProductSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : InnerProductSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : InnerProductSpace ℝ E'<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>h : ∀ (x : E), ⟪T x, x⟫_𝕜 = 0<VAR>x : E<GOAL>T x = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : InnerProductSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : InnerProductSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : InnerProductSpace ℝ E'<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>h : ∀ (x : E), ⟪T x, x⟫_𝕜 = 0<VAR>x : E<GOAL>(⟪T (x + T x), x + T x⟫_𝕜 - ⟪T (x - T x), x - T x⟫_𝕜 - I * ⟪T (x + I • T x), x + I • T x⟫_𝕜 + I * ⟪T (x - I • T x), x - I • T x⟫_𝕜) / 4 = 0
<VAR>a x✝ y✝ : ℂ<VAR>ha : a ≠ 0<VAR>x y : ℂ<GOAL>angle (x * a) (y * a) = angle x y
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Add R<VAR>inst✝ : Mul R<VAR>r : R → R → Prop<VAR>c : RingCon R<VAR>h : ∀ (x y : R), r x y → c x y<GOAL>ringConGen r ≤ c
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Add R<VAR>inst✝ : Mul R<VAR>r : R → R → Prop<VAR>c : RingCon R<VAR>h : ∀ (x y : R), r x y → c x y<GOAL>sInf {s | ∀ (x y : R), r x y → s x y} ≤ c
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<GOAL>(optionEquivRight R S₁) (X none) = C Polynomial.X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f✝ : α → β<VAR>n : ℕ<VAR>f : ℕ → α<VAR>hf : ∀ i < n, f i ∈ s<VAR>f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j<VAR>hs : autoParam s.Finite _auto✝<GOAL>n ≤ s.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f✝ : α → β<VAR>n : ℕ<VAR>f : ℕ → α<VAR>hf : ∀ i < n, f i ∈ s<VAR>f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j<VAR>hs : autoParam s.Finite _auto✝<GOAL>n ≤ (Finite.toFinset hs).card
<VAR>N✝ : ℕ<VAR>N M : ℤ<VAR>hNM : N ∣ M<GOAL>ModularGroup.T ^ M ∈ Gamma N.natAbs
<VAR>N✝ : ℕ<VAR>N M : ℤ<VAR>hNM : N ∣ M<GOAL>↑M = 0
<VAR>N✝ : ℕ<VAR>N M : ℤ<VAR>hNM : N ∣ M<GOAL>↑N.natAbs ∣ M
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : FirstCountableTopology X<VAR>ν : Measure α<VAR>inst✝¹ : MeasurableSingletonClass α<VAR>inst✝ : Fintype α<VAR>f : α → E<VAR>hf : Integrable f μ<GOAL>∫ (x : α), f x ∂μ = ∑ x : α, (μ {x}).toReal • f x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : FirstCountableTopology X<VAR>ν : Measure α<VAR>inst✝¹ : MeasurableSingletonClass α<VAR>inst✝ : Fintype α<VAR>f : α → E<VAR>hf : Integrable f μ<GOAL>Integrable f (μ.restrict ↑Finset.univ)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>ps : Set P<VAR>hnps : ps.Nonempty<VAR>p : P<VAR>hps : ps ⊆ ↑s<VAR>hp : p ∉ s<VAR>hu : ∃! cs, cs.center ∈ s ∧ ps ⊆ Metric.sphere cs.center cs.radius<GOAL>∃! cs₂, cs₂.center ∈ affineSpan ℝ (insert p ↑s) ∧ insert p ps ⊆ Metric.sphere cs₂.center cs₂.radius
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>ps : Set P<VAR>hnps : ps.Nonempty<VAR>p : P<VAR>hps : ps ⊆ ↑s<VAR>hp : p ∉ s<VAR>hu : ∃! cs, cs.center ∈ s ∧ ps ⊆ Metric.sphere cs.center cs.radius<VAR>this : Nonempty ↥s<GOAL>∃! cs₂, cs₂.center ∈ affineSpan ℝ (insert p ↑s) ∧ insert p ps ⊆ Metric.sphere cs₂.center cs₂.radius
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>ps : Set P<VAR>hnps : ps.Nonempty<VAR>p : P<VAR>hps : ps ⊆ ↑s<VAR>hp : p ∉ s<VAR>this : Nonempty ↥s<VAR>cc : P<VAR>cr : ℝ<VAR>hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }<VAR>hcc : cc ∈ s<VAR>hcr : ps ⊆ Metric.sphere cc cr<VAR>x : ℝ := dist cc ↑((orthogonalProjection s) p)<VAR>y : ℝ := dist p ↑((orthogonalProjection s) p)<GOAL>∃! cs₂, cs₂.center ∈ affineSpan ℝ (insert p ↑s) ∧ insert p ps ⊆ Metric.sphere cs₂.center cs₂.radius
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>ps : Set P<VAR>hnps : ps.Nonempty<VAR>p : P<VAR>hps : ps ⊆ ↑s<VAR>hp : p ∉ s<VAR>this : Nonempty ↥s<VAR>cc : P<VAR>cr : ℝ<VAR>hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }<VAR>hcc : cc ∈ s<VAR>hcr : ps ⊆ Metric.sphere cc cr<VAR>x : ℝ := dist cc ↑((orthogonalProjection s) p)<VAR>y : ℝ := dist p ↑((orthogonalProjection s) p)<VAR>hy0 : y ≠ 0<GOAL>∃! cs₂, cs₂.center ∈ affineSpan ℝ (insert p ↑s) ∧ insert p ps ⊆ Metric.sphere cs₂.center cs₂.radius
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>ps : Set P<VAR>hnps : ps.Nonempty<VAR>p : P<VAR>hps : ps ⊆ ↑s<VAR>hp : p ∉ s<VAR>this : Nonempty ↥s<VAR>cc : P<VAR>cr : ℝ<VAR>hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }<VAR>hcc : cc ∈ s<VAR>hcr : ps ⊆ Metric.sphere cc cr<VAR>x : ℝ := dist cc ↑((orthogonalProjection s) p)<VAR>y : ℝ := dist p ↑((orthogonalProjection s) p)<VAR>hy0 : y ≠ 0<VAR>ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)<VAR>cc₂ : P := (ycc₂ / y) • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc<VAR>cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)<GOAL>∃! cs₂, cs₂.center ∈ affineSpan ℝ (insert p ↑s) ∧ insert p ps ⊆ Metric.sphere cs₂.center cs₂.radius
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>ps : Set P<VAR>hnps : ps.Nonempty<VAR>p : P<VAR>hps : ps ⊆ ↑s<VAR>hp : p ∉ s<VAR>this : Nonempty ↥s<VAR>cc : P<VAR>cr : ℝ<VAR>hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }<VAR>hcc : cc ∈ s<VAR>hcr : ps ⊆ Metric.sphere cc cr<VAR>x : ℝ := dist cc ↑((orthogonalProjection s) p)<VAR>y : ℝ := dist p ↑((orthogonalProjection s) p)<VAR>hy0 : y ≠ 0<VAR>ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)<VAR>cc₂ : P := (ycc₂ / y) • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc<VAR>cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)<GOAL>(fun cs₂ => cs₂.center ∈ affineSpan ℝ (insert p ↑s) ∧ insert p ps ⊆ Metric.sphere cs₂.center cs₂.radius) { center := cc₂, radius := cr₂ } ∧ ∀ (y : Sphere P), (fun cs₂ => cs₂.center ∈ affineSpan ℝ (insert p ↑s) ∧ insert p ps ⊆ Metric.sphere cs₂.center cs₂.radius) y → y = { center := cc₂, radius := cr₂ }
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_3}<GOAL>a ≤ a + b
<GOAL>∀ {n : ℕ}, n ≠ 0 → multiplicity 2 n ! < ↑n
<VAR>h2 : _root_.Prime 2<GOAL>∀ {n : ℕ}, n ≠ 0 → multiplicity 2 n ! < ↑n
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : CosimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>X.map (SimplexCategory.δ i.castSucc) ≫ X.map (SimplexCategory.σ i) = 𝟙 (X.obj [n])
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>I : Box ι<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hf : f =ᶠ[ae (μ.restrict ↑I)] 0<VAR>hl : l.bRiemann = false<GOAL>HasIntegral I l f μ.toBoxAdditive.toSMul 0
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>I : Box ι<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hf : f =ᶠ[ae (μ.restrict ↑I)] 0<VAR>hl : l.bRiemann = false<VAR>ε : ℝ<VAR>ε0 : ε > 0<GOAL>∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f μ.toBoxAdditive.toSMul π) 0 ≤ ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>I : Box ι<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hf : f =ᶠ[ae (μ.restrict ↑I)] 0<VAR>hl : l.bRiemann = false<VAR>ε : ℝ≥0<VAR>ε0 : ↑ε > 0<GOAL>∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f μ.toBoxAdditive.toSMul π) 0 ≤ ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>I : Box ι<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hf : f =ᶠ[ae (μ.restrict ↑I)] 0<VAR>hl : l.bRiemann = false<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<GOAL>∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f μ.toBoxAdditive.toSMul π) 0 ≤ ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>I : Box ι<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hf : f =ᶠ[ae (μ.restrict ↑I)] 0<VAR>hl : l.bRiemann = false<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>δ : ℕ → ℝ≥0<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>c : ℝ≥0<VAR>hδc : HasSum δ c<VAR>hcε : c < ε<GOAL>∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f μ.toBoxAdditive.toSMul π) 0 ≤ ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>I : Box ι<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hf : f =ᶠ[ae (μ.restrict ↑I)] 0<VAR>hl : l.bRiemann = false<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>δ : ℕ → ℝ≥0<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>c : ℝ≥0<VAR>hδc : HasSum δ c<VAR>hcε : c < ε<VAR>this : Fact (μ ↑I < ⊤)<GOAL>∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f μ.toBoxAdditive.toSMul π) 0 ≤ ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>I : Box ι<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hl : l.bRiemann = false<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>δ : ℕ → ℝ≥0<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>c : ℝ≥0<VAR>hδc : HasSum δ c<VAR>hcε : c < ε<VAR>this : Fact (μ ↑I < ⊤)<VAR>hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0<VAR>N : (ι → ℝ) → ℕ := fun x => ⌈‖f x‖⌉₊<VAR>N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0<VAR>U : ℕ → Set (ι → ℝ)<VAR>hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n<VAR>hUo : ∀ (n : ℕ), IsOpen (U n)<VAR>hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n<GOAL>∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f μ.toBoxAdditive.toSMul π) 0 ≤ ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>I : Box ι<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hl : l.bRiemann = false<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>δ : ℕ → ℝ≥0<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>c : ℝ≥0<VAR>hδc : HasSum δ c<VAR>hcε : c < ε<VAR>this✝ : Fact (μ ↑I < ⊤)<VAR>hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0<VAR>N : (ι → ℝ) → ℕ := fun x => ⌈‖f x‖⌉₊<VAR>N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0<VAR>U : ℕ → Set (ι → ℝ)<VAR>hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n<VAR>hUo : ∀ (n : ℕ), IsOpen (U n)<VAR>hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n<VAR>this : ∀ (x : ι → ℝ), ∃ r, closedBall x ↑r ⊆ U (N x)<GOAL>∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f μ.toBoxAdditive.toSMul π) 0 ≤ ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>I : Box ι<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hl : l.bRiemann = false<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>δ : ℕ → ℝ≥0<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>c : ℝ≥0<VAR>hδc : HasSum δ c<VAR>hcε : c < ε<VAR>this : Fact (μ ↑I < ⊤)<VAR>hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0<VAR>N : (ι → ℝ) → ℕ := fun x => ⌈‖f x‖⌉₊<VAR>N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0<VAR>U : ℕ → Set (ι → ℝ)<VAR>hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n<VAR>hUo : ∀ (n : ℕ), IsOpen (U n)<VAR>hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrU : ∀ (x : ι → ℝ), closedBall x ↑(r x) ⊆ U (N x)<GOAL>∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum f μ.toBoxAdditive.toSMul π) 0 ≤ ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>I : Box ι<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hl : l.bRiemann = false<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>δ : ℕ → ℝ≥0<VAR>δ0 : ∀ (i : ℕ), 0 < δ i<VAR>c✝ : ℝ≥0<VAR>hδc : HasSum δ c✝<VAR>hcε : c✝ < ε<VAR>this : Fact (μ ↑I < ⊤)<VAR>hf : (μ.restrict ↑I) {x | f x ≠ 0} = 0<VAR>N : (ι → ℝ) → ℕ := fun x => ⌈‖f x‖⌉₊<VAR>N0 : ∀ {x : ι → ℝ}, N x = 0 ↔ f x = 0<VAR>U : ℕ → Set (ι → ℝ)<VAR>hNU : ∀ (n : ℕ), N ⁻¹' {n} ⊆ U n<VAR>hUo : ∀ (n : ℕ), IsOpen (U n)<VAR>hμU : ∀ (n : ℕ), (μ.restrict ↑I) (U n) < ↑(δ n) / ↑n<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrU : ∀ (x : ι → ℝ), closedBall x ↑(r x) ⊆ U (N x)<VAR>c : ℝ≥0<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c ((fun x => r) c) π<VAR>x✝ : π.IsPartition<GOAL>dist (integralSum f μ.toBoxAdditive.toSMul π) 0 ≤ ↑ε