ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : CommRing L<VAR>inst✝¹ : IsDomain L<VAR>inst✝ : Algebra K L<VAR>σ : L →ₐ[K] L<VAR>hσ : IsOfFinOrder σ<VAR>this : orderOf σ = orderOf ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit)<GOAL>IsOfFinOrder ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>𝒢 : Set C<VAR>h𝒢 : IsCoseparating 𝒢<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : ∀ G ∈ 𝒢, ∀ (h : Y ⟶ G), f ≫ h = 0<GOAL>∀ G ∈ 𝒢, ∀ (h : Y ⟶ G), f ≫ h = 0 ≫ h
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>𝒢 : Set C<VAR>h𝒢 : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ G ∈ 𝒢, ∀ (h : Y ⟶ G), f ≫ h = 0) → f = 0<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>hfg : ∀ G ∈ 𝒢, ∀ (h : Y ⟶ G), f ≫ h = g ≫ h<GOAL>∀ G ∈ 𝒢, ∀ (h : Y ⟶ G), (f - g) ≫ h = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>S : Set (LowerSet α)<VAR>s t : LowerSet α<VAR>a : α<VAR>f : ι → LowerSet α<GOAL>↑(⨆ i, f i) = ⋃ i, ↑(f i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>η : Type u_5<VAR>s : η → Set E<VAR>hs : Directed (fun x x_1 => x ⊆ x_1) s<VAR>h : ∀ (i : η), Orthonormal 𝕜 fun x => ↑x<GOAL>Orthonormal 𝕜 fun x => ↑x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x✝ y : α<VAR>inst✝² : DecidableRel f✝.SameCycle<VAR>inst✝¹ : DecidableRel g.SameCycle<VAR>f : Perm α<VAR>inst✝ : DecidableRel f.SameCycle<VAR>x : α<GOAL>(f.cycleOf x) (f x) = f (f x)
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w✝ x y : V<VAR>p : G.Walk u✝ v✝<VAR>hnp : ¬p.Nil<VAR>u v w : V<VAR>huv : G.Adj u v<VAR>q : G.Walk v w<GOAL>(notNilRec (fun {u v w} x q => q) (cons huv q) ⋯).support = (cons huv q).support.tail
<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>hs : NullMeasurableSet s μ<VAR>r : ℝ<GOAL>NullMeasurableSet (r • 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>r : ℝ<VAR>hs : NullMeasurableSet ∅ μ<GOAL>NullMeasurableSet (r • ∅) μ
<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>hs : NullMeasurableSet s μ<VAR>r : ℝ<VAR>hs' : s.Nonempty<GOAL>NullMeasurableSet (r • 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>hs : NullMeasurableSet s μ<VAR>hs' : s.Nonempty<GOAL>NullMeasurableSet (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>hs : NullMeasurableSet s μ<VAR>r : ℝ<VAR>hs' : s.Nonempty<VAR>hr : r ≠ 0<GOAL>NullMeasurableSet (r • 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>r : ℝ<VAR>hs' : s.Nonempty<VAR>hr : r ≠ 0<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>hst : s =ᶠ[ae μ] t<GOAL>NullMeasurableSet (r • 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>r : ℝ<VAR>hs' : s.Nonempty<VAR>hr : r ≠ 0<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>hst : s =ᶠ[ae μ] t<GOAL>r • s =ᶠ[ae μ] r • t
<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>r : ℝ<VAR>hs' : s.Nonempty<VAR>hr : r ≠ 0<VAR>t : Set E<VAR>ht : MeasurableSet t<VAR>hst : μ (symmDiff s t) = 0<GOAL>μ (symmDiff (r • s) (r • t)) = 0
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ dt : ℝ<GOAL>IsIntegralCurveOn γ v s ↔ IsIntegralCurveOn (γ ∘ fun x => x + dt) v {t | t + dt ∈ s}
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ dt : ℝ<VAR>hγ : IsIntegralCurveOn (γ ∘ fun x => x + dt) v {t | t + dt ∈ s}<GOAL>IsIntegralCurveOn γ v s
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ dt : ℝ<VAR>hγ : IsIntegralCurveOn (γ ∘ fun x => x + dt) v {t | t + dt ∈ s}<GOAL>γ = (γ ∘ fun x => x + dt) ∘ fun x => x + -dt
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ dt : ℝ<VAR>hγ : IsIntegralCurveOn (γ ∘ fun x => x + dt) v {t | t + dt ∈ s}<GOAL>s = {t | t + -dt ∈ {t | t + dt ∈ s}}
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>s t : Set α✝<VAR>α : Type u_3<GOAL>univ.ncard = Nat.card α
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>s t : Set α✝<VAR>α : Type u_3<VAR>h : Finite α<GOAL>univ.ncard = Nat.card α
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>s t : Set α✝<VAR>α : Type u_3<VAR>h : Infinite α<GOAL>univ.ncard = Nat.card α
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>s t : Set α✝<VAR>α : Type u_3<VAR>h : Infinite α<GOAL>univ.Infinite
<VAR>a : ℕ<GOAL>Periodic a.Coprime a
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>HasDerivAt (fun x => √x * log x) ((2 + log x) / (2 * √x)) x
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>(2 + log x) / (2 * √x) = 1 / (2 * √x) * log x + √x * x⁻¹
<VAR>M : Type u_1<VAR>inst✝¹ : OrderedCancelAddCommMonoid M<VAR>inst✝ : ExistsAddOfLE M<VAR>a b c d : M<GOAL>BijOn (fun x => x + d) (Ici a) (Ici (a + d))
<VAR>M : Type u_1<VAR>inst✝¹ : OrderedCancelAddCommMonoid M<VAR>inst✝ : ExistsAddOfLE M<VAR>a b c d x✝ : M<VAR>h : x✝ ∈ Ici (a + d)<GOAL>x✝ ∈ (fun x => x + d) '' Ici a
<VAR>M : Type u_1<VAR>inst✝¹ : OrderedCancelAddCommMonoid M<VAR>inst✝ : ExistsAddOfLE M<VAR>a b c✝ d c : M<VAR>h : a + d + c ∈ Ici (a + d)<GOAL>a + d + c ∈ (fun x => x + d) '' Ici a
<VAR>M : Type u_1<VAR>inst✝¹ : OrderedCancelAddCommMonoid M<VAR>inst✝ : ExistsAddOfLE M<VAR>a b c✝ d c : M<VAR>h : a ≤ a + c<GOAL>a + d + c ∈ (fun x => x + d) '' Ici a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : Filter X<VAR>s✝ t✝ s₁ s₂ t₁ t₂ : Set X<VAR>x : X<VAR>s t : Set X<GOAL>t ∈ 𝓝ˢ s ↔ ∃ i, (IsOpen i ∧ s ⊆ i) ∧ i ⊆ t
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I B X : Set α<GOAL>M✶.Dep I ↔ (∀ (B : Set α), M.Base B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
<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>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>inst✝¹ : Nonempty ↥s<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = n<VAR>hc : Cospherical ps<GOAL>∃ r, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
<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>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>inst✝¹ : Nonempty ↥s<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = n<VAR>hc : ∃ center ∈ s, ∃ radius, ∀ p ∈ ps, dist p center = radius<GOAL>∃ r, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
<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>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>inst✝¹ : Nonempty ↥s<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = n<VAR>c : P<VAR>hc : c ∈ s<VAR>r : ℝ<VAR>hcr : ∀ p ∈ ps, dist p c = r<GOAL>∃ r, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
<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>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>inst✝¹ : Nonempty ↥s<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = n<VAR>c : P<VAR>hc : c ∈ s<VAR>r : ℝ<VAR>hcr : ∀ p ∈ ps, dist p c = r<GOAL>∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
<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>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>inst✝¹ : Nonempty ↥s<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = n<VAR>c : P<VAR>hc : c ∈ s<VAR>r : ℝ<VAR>hcr : ∀ p ∈ ps, dist p c = r<VAR>sx : Simplex ℝ P n<VAR>hsxps : Set.range sx.points ⊆ ps<GOAL>sx.circumradius = r
<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>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>inst✝¹ : Nonempty ↥s<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = n<VAR>c : P<VAR>hc : c ∈ s<VAR>r : ℝ<VAR>hcr : ∀ p ∈ ps, dist p c = r<VAR>sx : Simplex ℝ P n<VAR>hsxps : Set.range sx.points ⊆ ps<VAR>hsx : affineSpan ℝ (Set.range sx.points) = s<GOAL>sx.circumradius = r
<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>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>inst✝¹ : Nonempty ↥s<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = n<VAR>c : P<VAR>hc✝ : c ∈ s<VAR>r : ℝ<VAR>hcr : ∀ p ∈ ps, dist p c = r<VAR>sx : Simplex ℝ P n<VAR>hsxps : Set.range sx.points ⊆ ps<VAR>hsx : affineSpan ℝ (Set.range sx.points) = s<VAR>hc : c ∈ affineSpan ℝ (Set.range sx.points)<GOAL>sx.circumradius = r
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<GOAL>insepDegree F F = 1
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>r : ℝ<VAR>x : E<VAR>hr : 0 < r<GOAL>(1 + ‖x‖ ^ 2) ^ (-r / 2) = 2 ^ (r / 2) * ((√2 * √(1 + ‖x‖ ^ 2)) ^ r)⁻¹
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>r : ℝ<VAR>x : E<VAR>hr : 0 < r<GOAL>1 + ‖x‖ ≤ √2 * √(1 + ‖x‖ ^ 2)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>r : ℝ<VAR>x : E<VAR>hr : 0 < r<GOAL>2 ^ (r / 2) * ((1 + ‖x‖) ^ r)⁻¹ = 2 ^ (r / 2) * (1 + ‖x‖) ^ (-r)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>r : ℝ<VAR>x : E<VAR>hr : 0 < r<GOAL>0 ≤ 1 + ‖x‖
<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>τ : κ → Type u_8<VAR>inst✝² : (i : ι) → TopologicalSpace (σ i)<VAR>inst✝¹ : (k : κ) → TopologicalSpace (τ k)<VAR>inst✝ : TopologicalSpace X<VAR>f₁ : ι → κ<VAR>f₂ : (i : ι) → σ i → τ (f₁ i)<VAR>h : Injective f₁<GOAL>OpenEmbedding (Sigma.map f₁ f₂) ↔ ∀ (i : ι), OpenEmbedding (f₂ i)
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : Fintype α<VAR>s t : Finset α<VAR>a b : α<VAR>h : s ⊂ t<GOAL>0 < ↑(Fintype.card α)
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : Fintype α<VAR>s t : Finset α<VAR>a b : α<VAR>h : s ⊂ t<VAR>h✝ : IsEmpty α<GOAL>0 < ↑(Fintype.card α)
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : Fintype α<VAR>s t : Finset α<VAR>a b : α<VAR>h : s ⊂ t<VAR>h✝ : Nonempty α<GOAL>0 < ↑(Fintype.card α)
<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>f : E ≃ₗ[ℝ] E<VAR>s : Set E<GOAL>μ (⇑f ⁻¹' s) = ENNReal.ofReal |LinearMap.det ↑f.symm| * μ 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>f : E ≃ₗ[ℝ] E<VAR>s : Set E<VAR>A : LinearMap.det ↑f ≠ 0<GOAL>μ (⇑f ⁻¹' s) = ENNReal.ofReal |LinearMap.det ↑f.symm| * μ 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>f : E ≃ₗ[ℝ] E<VAR>s : Set E<VAR>A : LinearMap.det ↑f ≠ 0<GOAL>LinearMap.det ↑f.symm = (LinearMap.det ↑f)⁻¹
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>n : ℕ<VAR>a✝ b c a : α<GOAL>|a| ^ 2 = a ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : SuccOrder α<VAR>a b : α<VAR>n m : ℕ<VAR>h_eq : succ^[n] a = succ^[m] a<VAR>h_lt : n < m<GOAL>IsMax (succ^[n] a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : SuccOrder α<VAR>a b : α<VAR>n m : ℕ<VAR>h_eq : succ^[n] a = succ^[m] a<VAR>h_lt : n < m<GOAL>succ (succ^[n] a) ≤ succ^[m] a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : SuccOrder α<VAR>a b : α<VAR>n m : ℕ<VAR>h_eq : succ^[n] a = succ^[m] a<VAR>h_lt : n < m<VAR>this : succ (succ^[n] a) = succ^[n + 1] a<GOAL>succ (succ^[n] a) ≤ succ^[m] a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : SuccOrder α<VAR>a b : α<VAR>n m : ℕ<VAR>h_eq : succ^[n] a = succ^[m] a<VAR>h_lt : n < m<VAR>this : succ (succ^[n] a) = succ^[n + 1] a<GOAL>succ^[n + 1] a ≤ succ^[m] a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : SuccOrder α<VAR>a b : α<VAR>n m : ℕ<VAR>h_eq : succ^[n] a = succ^[m] a<VAR>h_lt : n < m<VAR>this : succ (succ^[n] a) = succ^[n + 1] a<VAR>h_le : n + 1 ≤ m<GOAL>succ^[n + 1] a ≤ succ^[m] a
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k✝ l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝ k✝<VAR>inst✝ : IsDomain R<VAR>k : ℕ+<VAR>ζ ξ : Rˣ<VAR>h : IsPrimitiveRoot ζ ↑k<VAR>hξ : ξ ∈ rootsOfUnity k R<GOAL>∃ i < ↑k, ζ ^ i = ξ
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k✝ l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝ k✝<VAR>inst✝ : IsDomain R<VAR>k : ℕ+<VAR>ζ : Rˣ<VAR>h : IsPrimitiveRoot ζ ↑k<VAR>n : ℤ<VAR>hξ : ζ ^ n ∈ rootsOfUnity k R<GOAL>∃ i < ↑k, ζ ^ i = ζ ^ n
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k✝ l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝ k✝<VAR>inst✝ : IsDomain R<VAR>k : ℕ+<VAR>ζ : Rˣ<VAR>h : IsPrimitiveRoot ζ ↑k<VAR>n : ℤ<VAR>hξ : ζ ^ n ∈ rootsOfUnity k R<VAR>hk0 : 0 < ↑↑k<GOAL>∃ i < ↑k, ζ ^ i = ζ ^ n
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k✝ l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝ k✝<VAR>inst✝ : IsDomain R<VAR>k : ℕ+<VAR>ζ : Rˣ<VAR>h : IsPrimitiveRoot ζ ↑k<VAR>n : ℤ<VAR>hξ : ζ ^ n ∈ rootsOfUnity k R<VAR>hk0 : 0 < ↑↑k<VAR>i : ℤ := n % ↑↑k<GOAL>∃ i < ↑k, ζ ^ i = ζ ^ n
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k✝ l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝ k✝<VAR>inst✝ : IsDomain R<VAR>k : ℕ+<VAR>ζ : Rˣ<VAR>h : IsPrimitiveRoot ζ ↑k<VAR>n : ℤ<VAR>hξ : ζ ^ n ∈ rootsOfUnity k R<VAR>hk0 : 0 < ↑↑k<VAR>i : ℤ := n % ↑↑k<VAR>hi0 : 0 ≤ i<GOAL>∃ i < ↑k, ζ ^ i = ζ ^ n
<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✝⁴ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>c ca cb : E<VAR>l l' la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>μ : Measure ℝ<VAR>u v ua va ub vb : ι → ℝ<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : FTCFilter a la la'<VAR>inst✝¹ : FTCFilter b lb lb'<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hab : IntervalIntegrable f μ a b<VAR>hmeas : StronglyMeasurableAtFilter f lb' μ<VAR>hf : Tendsto f (lb' ⊓ ae μ) (𝓝 c)<VAR>hu : Tendsto u lt lb<VAR>hv : Tendsto v lt lb<GOAL>(fun t => ∫ (x : ℝ) in a..v t, f x ∂μ - ∫ (x : ℝ) in a..u t, f x ∂μ - ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt] fun t => ∫ (x : ℝ) in u t..v t, 1 ∂μ
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f✝ g : Filter α<VAR>s✝ t✝ : Set α<VAR>f : Filter α<VAR>s t : Set α<GOAL>s ∈ f ⊓ 𝓟 t ↔ tᶜ ∪ s ∈ f
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ≥0<GOAL>EMetric.ball x ↑ε = ball x ↑ε
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ≥0<GOAL>EMetric.ball x ↑ε = EMetric.ball x (ENNReal.ofReal ↑ε)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_4, u_1} C<VAR>inst✝⁴ : Category.{u_6, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝³ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>φ : W.LeftFraction X Y<VAR>E : Type u_3<VAR>inst✝² : Category.{u_5, u_3} E<VAR>L₁ : C ⥤ D<VAR>L₂ : C ⥤ E<VAR>inst✝¹ : L₁.IsLocalization W<VAR>inst✝ : L₂.IsLocalization W<VAR>e : L₁ ⋙ (Localization.uniq L₁ L₂ W).functor ≅ L₂ := Localization.compUniqFunctor L₁ L₂ W<GOAL>(Localization.uniq L₁ L₂ W).functor.map (φ.map L₁ ⋯) = (Localization.compUniqFunctor L₁ L₂ W).hom.app X ≫ φ.map L₂ ⋯ ≫ (Localization.compUniqFunctor L₁ L₂ W).inv.app Y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_4, u_1} C<VAR>inst✝⁴ : Category.{u_6, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝³ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>φ : W.LeftFraction X Y<VAR>E : Type u_3<VAR>inst✝² : Category.{u_5, u_3} E<VAR>L₁ : C ⥤ D<VAR>L₂ : C ⥤ E<VAR>inst✝¹ : L₁.IsLocalization W<VAR>inst✝ : L₂.IsLocalization W<VAR>e : L₁ ⋙ (Localization.uniq L₁ L₂ W).functor ≅ L₂ := Localization.compUniqFunctor L₁ L₂ W<VAR>this : IsIso (L₂.map φ.s)<GOAL>(Localization.uniq L₁ L₂ W).functor.map (φ.map L₁ ⋯) = (Localization.compUniqFunctor L₁ L₂ W).hom.app X ≫ φ.map L₂ ⋯ ≫ (Localization.compUniqFunctor L₁ L₂ W).inv.app Y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_4, u_1} C<VAR>inst✝⁴ : Category.{u_6, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝³ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>φ : W.LeftFraction X Y<VAR>E : Type u_3<VAR>inst✝² : Category.{u_5, u_3} E<VAR>L₁ : C ⥤ D<VAR>L₂ : C ⥤ E<VAR>inst✝¹ : L₁.IsLocalization W<VAR>inst✝ : L₂.IsLocalization W<VAR>e : L₁ ⋙ (Localization.uniq L₁ L₂ W).functor ≅ L₂ := Localization.compUniqFunctor L₁ L₂ W<VAR>this : IsIso (L₂.map φ.s)<GOAL>(Localization.uniq L₁ L₂ W).functor.map (φ.map L₁ ⋯) ≫ (L₁ ⋙ (Localization.uniq L₁ L₂ W).functor).map φ.s ≫ e.hom.app φ.Y' = (Localization.compUniqFunctor L₁ L₂ W).hom.app X ≫ L₂.map φ.f
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝² : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>P : Finpartition s<VAR>Q : Finpartition t<GOAL>(interedges r s t).card = ∑ ab ∈ P.parts ×ˢ Q.parts, (interedges r ab.1 ab.2).card
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝² : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>P : Finpartition s<VAR>Q : Finpartition t<GOAL>∑ a ∈ P.parts, (interedges r a t).card = ∑ x ∈ P.parts, ∑ y ∈ Q.parts, (interedges r (x, y).1 (x, y).2).card
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝² : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>P : Finpartition s<VAR>Q : Finpartition t<VAR>x✝ : Finset α<GOAL>(interedges r x✝ t).card = ∑ y ∈ Q.parts, (interedges r (x✝, y).1 (x✝, y).2).card
<VAR>J : Type w<VAR>K : Type u_1<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>f : J → C<VAR>inst✝ : HasBiproduct f<VAR>j : J<GOAL>(isoProduct f).inv ≫ π f j = lift (Pi.π f) ≫ π f j