ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝¹ : CommRing R<VAR>x y z : R<VAR>inst✝ : IsPrincipal (Ideal.span {x, y})<GOAL>gcd x y ∈ {gcd x y}
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>Fintype.card ↑(Set.uIcc a b) = (↑↑b - ↑↑a).natAbs + 1
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>inst✝ : IsIso g<GOAL>pushout.inr f g ≫ inv (pushout.inl f g) = inv g ≫ f
<VAR>A : Type u_1<VAR>inst✝³ : AddCommGroup A<VAR>inst✝² : Module ℂ A<VAR>inst✝¹ : StarAddMonoid A<VAR>inst✝ : StarModule ℂ A<VAR>x : ↥(selfAdjoint A)<GOAL>↑(ℑ (I • ↑x)) = ↑x
<VAR>α : Type u_1<VAR>p q : ℚ≥0<GOAL>↑q = 0 ↔ q = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝¹ : One M<VAR>inst✝ : One N<VAR>s t : Set α<VAR>f g : α → M<VAR>a : α<VAR>this : Decidable (a ∈ s) := Classical.dec (a ∈ s)<GOAL>a ∉ s → 1 = f a ↔ a ∉ s → f a = 1
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hr : 0 ≤ r<VAR>hf0 : f 0 = 0<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>i : ℕ<GOAL>eLpNorm (stoppedValue f (leastGE f r i)) 1 μ ≤ ↑(2 * μ Set.univ * ENNReal.ofReal (r + ↑R)).toNNReal
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hr : 0 ≤ r<VAR>hf0 : f 0 = 0<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>i : ℕ<GOAL>2 * μ Set.univ * ENNReal.ofReal (r + ↑R) ≤ ↑(2 * μ Set.univ * ENNReal.ofReal (r + ↑R)).toNNReal
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>s : Opens X<VAR>hs : Nonempty ↥s<GOAL>(s.partialHomeomorphSubtypeCoe hs).target = ↑s
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>s : Opens X<VAR>hs : Nonempty ↥s<GOAL>{x | x ∈ s.carrier} = ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f : Ordinal.{u_4} → Ordinal.{u_5}<VAR>o : Ordinal.{u_5}<VAR>H : IsNormal f<VAR>p : Set Ordinal.{u_4}<VAR>p0 : p.Nonempty<VAR>b : Ordinal.{u_4}<VAR>H₂ : ∀ (o : Ordinal.{u_4}), b ≤ o ↔ ∀ a ∈ p, a ≤ o<VAR>h : ∀ a ∈ p, f a ≤ o<GOAL>f b ≤ o
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<GOAL>LiouvilleWith p (x - ↑r) ↔ LiouvilleWith p x
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>R' : Type v<VAR>inst✝² : CommMonoid R'<VAR>C : Type v<VAR>inst✝¹ : CommMonoid C<VAR>n : ℕ<VAR>inst✝ : NeZero n<VAR>ζ : C<VAR>h : IsPrimitiveRoot ζ n<GOAL>(zmodChar n ⋯).IsPrimitive
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>R' : Type v<VAR>inst✝² : CommMonoid R'<VAR>C : Type v<VAR>inst✝¹ : CommMonoid C<VAR>n : ℕ<VAR>inst✝ : NeZero n<VAR>ζ : C<VAR>h : IsPrimitiveRoot ζ n<GOAL>∀ (a : ZMod n), (zmodChar n ⋯) a = 1 → a = 0
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>R' : Type v<VAR>inst✝² : CommMonoid R'<VAR>C : Type v<VAR>inst✝¹ : CommMonoid C<VAR>n : ℕ<VAR>inst✝ : NeZero n<VAR>ζ : C<VAR>h : IsPrimitiveRoot ζ n<VAR>a : ZMod n<VAR>ha : (zmodChar n ⋯) a = 1<GOAL>a = 0
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>R' : Type v<VAR>inst✝² : CommMonoid R'<VAR>C : Type v<VAR>inst✝¹ : CommMonoid C<VAR>n : ℕ<VAR>inst✝ : NeZero n<VAR>ζ : C<VAR>h : IsPrimitiveRoot ζ n<VAR>a : ZMod n<VAR>ha : ζ ^ a.val = ζ ^ 0<GOAL>a = 0
<VAR>M : Type u_1<VAR>inst✝⁴ : Monoid M<VAR>G : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : Fintype G<VAR>R : Type u_3<VAR>inst✝¹ : CommRing R<VAR>inst✝ : MulSemiringAction G R<VAR>x : R<VAR>g : G<VAR>this : DecidableEq R := Classical.decEq R<VAR>g' : G ⧸ stabilizer G x<GOAL>g • (X - C (ofQuotientStabilizer G x g')) = X - C (ofQuotientStabilizer G x (g • g'))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : SemilatticeSup M<VAR>w : σ → M<VAR>p : MvPolynomial σ R<GOAL>weightedTotalDegree' w p = ⊥ ↔ p = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : SemilatticeSup M<VAR>w : σ → M<VAR>p : MvPolynomial σ R<GOAL>(∀ (s : σ →₀ ℕ), coeff s p ≠ 0 → False) ↔ ∀ (d : σ →₀ ℕ), coeff d p = 0
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<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>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>e : E<VAR>f : E → F<VAR>g : E → G<VAR>s : Set E<VAR>r t : ℝ≥0∞<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>q : FormalMultilinearSeries 𝕜 E G<VAR>hf : HasFPowerSeriesWithinOnBall f p s e r<VAR>hg : HasFPowerSeriesWithinOnBall g q s e t<GOAL>min r t ≤ (p.prod q).radius
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<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>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>e : E<VAR>f : E → F<VAR>g : E → G<VAR>s : Set E<VAR>r t : ℝ≥0∞<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>q : FormalMultilinearSeries 𝕜 E G<VAR>hf : HasFPowerSeriesWithinOnBall f p s e r<VAR>hg : HasFPowerSeriesWithinOnBall g q s e t<GOAL>min r t ≤ min p.radius q.radius
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<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>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>e : E<VAR>f : E → F<VAR>g : E → G<VAR>s : Set E<VAR>r t : ℝ≥0∞<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>q : FormalMultilinearSeries 𝕜 E G<VAR>hf : HasFPowerSeriesWithinOnBall f p s e r<VAR>hg : HasFPowerSeriesWithinOnBall g q s e t<VAR>y : E<VAR>m : e + y ∈ s<VAR>hy : y ∈ EMetric.ball 0 (min r t)<GOAL>HasSum (fun n => (p.prod q n) fun x => y) (f (e + y), g (e + y))
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<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>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>e : E<VAR>f : E → F<VAR>g : E → G<VAR>s : Set E<VAR>r t : ℝ≥0∞<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>q : FormalMultilinearSeries 𝕜 E G<VAR>hf : HasFPowerSeriesWithinOnBall f p s e r<VAR>hg : HasFPowerSeriesWithinOnBall g q s e t<VAR>y : E<VAR>m : e + y ∈ s<VAR>hy : y ∈ EMetric.ball 0 (min r t)<GOAL>HasSum (fun n => ((p n) fun x => y, (q n) fun x => y)) (f (e + y), g (e + y))
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<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>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>e : E<VAR>f : E → F<VAR>g : E → G<VAR>s : Set E<VAR>r t : ℝ≥0∞<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>q : FormalMultilinearSeries 𝕜 E G<VAR>hf : HasFPowerSeriesWithinOnBall f p s e r<VAR>hg : HasFPowerSeriesWithinOnBall g q s e t<VAR>y : E<VAR>m : e + y ∈ s<VAR>hy : y ∈ EMetric.ball 0 (min r t)<GOAL>y ∈ EMetric.ball 0 r
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<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>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>e : E<VAR>f : E → F<VAR>g : E → G<VAR>s : Set E<VAR>r t : ℝ≥0∞<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>q : FormalMultilinearSeries 𝕜 E G<VAR>hf : HasFPowerSeriesWithinOnBall f p s e r<VAR>hg : HasFPowerSeriesWithinOnBall g q s e t<VAR>y : E<VAR>m : e + y ∈ s<VAR>hy : y ∈ EMetric.ball 0 (min r t)<GOAL>y ∈ EMetric.ball 0 t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<VAR>S : Set (Set α)<VAR>hs : S.Countable<VAR>hd : S.Pairwise Disjoint<VAR>h : ∀ s ∈ S, MeasurableSet s<GOAL>μ (⋃₀ S) = ∑' (s : ↑S), μ ↑s
<VAR>R : Type u_1<VAR>S✝ : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S✝<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S✝ M<VAR>inst✝¹ : SMul S✝ R<VAR>inst✝ : IsScalarTower S✝ R M<VAR>p q : Submodule R M<VAR>S : Set (Submodule R M)<VAR>s : Submodule R M<VAR>hs : s ∈ S<GOAL>∀ {x : M}, x ∈ s → x ∈ sSup S
<VAR>R : Type u_1<VAR>S✝ : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S✝<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S✝ M<VAR>inst✝¹ : SMul S✝ R<VAR>inst✝ : IsScalarTower S✝ R M<VAR>p q : Submodule R M<VAR>S : Set (Submodule R M)<VAR>s : Submodule R M<VAR>hs : s ∈ S<VAR>this : s ≤ sSup S<GOAL>∀ {x : M}, x ∈ s → x ∈ sSup S
<VAR>n k : ℕ<VAR>h : k ≤ n<GOAL>n.descFactorial k = n ! / (n - k)!
<VAR>n k : ℕ<VAR>h : k ≤ n<GOAL>(n - k)! * n.descFactorial k = (n - k)! * (n ! / (n - k)!)
<VAR>n k : ℕ<VAR>h : k ≤ n<GOAL>n ! = (n - k)! * (n ! / (n - k)!)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>A : E →L[ℝ] E<VAR>m : ℝ≥0<VAR>hm : ↑m < ENNReal.ofReal |A.det|<GOAL>∀ᶠ (δ : ℝ≥0) in 𝓝[>] 0, ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * μ s ≤ μ (f '' s)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>A : E →L[ℝ] E<VAR>m : ℝ≥0<VAR>hm : ↑m < ENNReal.ofReal |A.det|<GOAL>{x | (fun δ => ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * μ s ≤ μ (f '' s)) x} ∈ 𝓝 0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>A : E →L[ℝ] E<VAR>hm : ↑0 < ENNReal.ofReal |A.det|<GOAL>{x | (fun δ => ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑0 * μ s ≤ μ (f '' s)) x} ∈ 𝓝 0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>A : E →L[ℝ] E<VAR>m : ℝ≥0<VAR>hm : ↑m < ENNReal.ofReal |A.det|<VAR>mpos : 0 < m<GOAL>{x | (fun δ => ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * μ s ≤ μ (f '' s)) x} ∈ 𝓝 0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>A : E →L[ℝ] E<VAR>m : ℝ≥0<VAR>hm : ↑m < ENNReal.ofReal |A.det|<VAR>mpos : 0 < m<VAR>hA : A.det ≠ 0<GOAL>{x | (fun δ => ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * μ s ≤ μ (f '' s)) x} ∈ 𝓝 0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>A : E →L[ℝ] E<VAR>m : ℝ≥0<VAR>hm : ↑m < ENNReal.ofReal |A.det|<VAR>mpos : 0 < m<VAR>hA : A.det ≠ 0<VAR>B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA<GOAL>{x | (fun δ => ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * μ s ≤ μ (f '' s)) x} ∈ 𝓝 0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>A : E →L[ℝ] E<VAR>m : ℝ≥0<VAR>hm : ↑m < ENNReal.ofReal |A.det|<VAR>mpos : 0 < m<VAR>hA : A.det ≠ 0<VAR>B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA<VAR>I : ENNReal.ofReal |(↑B.symm).det| < ↑m⁻¹<GOAL>{x | (fun δ => ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * μ s ≤ μ (f '' s)) x} ∈ 𝓝 0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>A : E →L[ℝ] E<VAR>m : ℝ≥0<VAR>hm : ↑m < ENNReal.ofReal |A.det|<VAR>mpos : 0 < m<VAR>hA : A.det ≠ 0<VAR>B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA<VAR>I : ENNReal.ofReal |(↑B.symm).det| < ↑m⁻¹<VAR>δ₀ : ℝ≥0<VAR>δ₀pos : 0 < δ₀<VAR>hδ₀ : ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑B.symm) t δ₀ → μ (g '' t) ≤ ↑m⁻¹ * μ t<GOAL>{x | (fun δ => ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * μ s ≤ μ (f '' s)) x} ∈ 𝓝 0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>A : E →L[ℝ] E<VAR>m : ℝ≥0<VAR>hm : ↑m < ENNReal.ofReal |A.det|<VAR>mpos : 0 < m<VAR>hA : A.det ≠ 0<VAR>B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA<VAR>I : ENNReal.ofReal |(↑B.symm).det| < ↑m⁻¹<VAR>δ₀ : ℝ≥0<VAR>δ₀pos : 0 < δ₀<VAR>hδ₀ : ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑B.symm) t δ₀ → μ (g '' t) ≤ ↑m⁻¹ * μ t<VAR>L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑B.symm‖₊⁻¹<VAR>L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑B.symm‖₊ * (‖↑B.symm‖₊⁻¹ - δ)⁻¹ * δ < δ₀<GOAL>{x | (fun δ => ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * μ s ≤ μ (f '' s)) x} ∈ 𝓝 0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>A : E →L[ℝ] E<VAR>m : ℝ≥0<VAR>hm : ↑m < ENNReal.ofReal |A.det|<VAR>mpos : 0 < m<VAR>hA : A.det ≠ 0<VAR>B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA<VAR>I : ENNReal.ofReal |(↑B.symm).det| < ↑m⁻¹<VAR>δ₀ : ℝ≥0<VAR>δ₀pos : 0 < δ₀<VAR>hδ₀ : ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑B.symm) t δ₀ → μ (g '' t) ≤ ↑m⁻¹ * μ t<VAR>L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑B.symm‖₊⁻¹<VAR>L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑B.symm‖₊ * (‖↑B.symm‖₊⁻¹ - δ)⁻¹ * δ < δ₀<GOAL>∀ (a : ℝ≥0), Subsingleton E ∨ a < ‖↑B.symm‖₊⁻¹ → ‖↑B.symm‖₊ * (‖↑B.symm‖₊⁻¹ - a)⁻¹ * a < δ₀ → ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s a → ↑m * μ s ≤ μ (f '' s)
<VAR>E : Type u_1<VAR>F✝ : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F✝<VAR>inst✝³ : NormedSpace ℝ F✝<VAR>s✝ : Set E<VAR>f✝ : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>A : E →L[ℝ] E<VAR>m : ℝ≥0<VAR>hm : ↑m < ENNReal.ofReal |A.det|<VAR>mpos : 0 < m<VAR>hA : A.det ≠ 0<VAR>B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA<VAR>I : ENNReal.ofReal |(↑B.symm).det| < ↑m⁻¹<VAR>δ₀ : ℝ≥0<VAR>δ₀pos : 0 < δ₀<VAR>hδ₀ : ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑B.symm) t δ₀ → μ (g '' t) ≤ ↑m⁻¹ * μ t<VAR>L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑B.symm‖₊⁻¹<VAR>L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑B.symm‖₊ * (‖↑B.symm‖₊⁻¹ - δ)⁻¹ * δ < δ₀<VAR>δ : ℝ≥0<VAR>h1δ : Subsingleton E ∨ δ < ‖↑B.symm‖₊⁻¹<VAR>h2δ : ‖↑B.symm‖₊ * (‖↑B.symm‖₊⁻¹ - δ)⁻¹ * δ < δ₀<VAR>s : Set E<VAR>f : E → E<VAR>hf : ApproximatesLinearOn f A s δ<VAR>hf' : ApproximatesLinearOn f (↑B) s δ<VAR>F : PartialEquiv E E := hf'.toPartialEquiv h1δ<GOAL>μ (↑F.symm '' F.target) ≤ ↑m⁻¹ * μ F.target
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : HasFiniteLimits C<VAR>F : C ⥤ D<VAR>inst✝ : PreservesFiniteLimits F<VAR>X : D<GOAL>HasFiniteLimits (StructuredArrow X F)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : HasFiniteLimits C<VAR>F : C ⥤ D<VAR>inst✝ : PreservesFiniteLimits F<VAR>X : D<GOAL>∀ (J : Type v₁) {𝒥 : SmallCategory J}, FinCategory J → HasLimitsOfShape J (StructuredArrow X F)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>inst✝ : DenselyOrdered α<GOAL>Ioi b ⊆ Ici a ↔ a ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>inst✝ : DenselyOrdered α<VAR>h : Ioi b ⊆ Ici a<GOAL>a ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>inst✝ : DenselyOrdered α<VAR>h : Ioi b ⊆ Ici a<VAR>ba : ¬a ≤ b<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c✝ d : α<VAR>inst✝ : DenselyOrdered α<VAR>h : Ioi b ⊆ Ici a<VAR>ba : ¬a ≤ b<VAR>c : α<VAR>bc : b < c<VAR>ca : c < a<GOAL>False
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : LieRingModule L N<VAR>inst✝ : LieModule R L N<VAR>t : R<VAR>x y z : L<VAR>m n : M<GOAL>⁅x, -m⁆ = -⁅x, m⁆
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : LieRingModule L N<VAR>inst✝ : LieModule R L N<VAR>t : R<VAR>x y z : L<VAR>m n : M<GOAL>⁅x, -m + m⁆ = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>T : E →ₗ[𝕜] E<VAR>x : E<GOAL>0 ≤ re ⟪x, (adjoint T * T) x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>T : E →ₗ[𝕜] E<VAR>x : E<GOAL>0 ≤ re (↑‖T x‖ ^ 2)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>T : E →ₗ[𝕜] E<VAR>x : E<GOAL>0 ≤ ‖T x‖ ^ 2
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>A : C<VAR>hA : IsSubterminal A<VAR>inst✝ : HasBinaryProduct A A<GOAL>A ⨯ A ≅ A
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>A : C<VAR>hA : IsSubterminal A<VAR>inst✝ : HasBinaryProduct A A<VAR>this : IsIso (diag A) := isIso_diag hA<GOAL>A ⨯ A ≅ A
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>s : Set M<GOAL>Submodule.span R s ≤ ↑(lieSpan R L s)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>s : Set M<GOAL>s ⊆ ↑↑(lieSpan R L s)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>K✝ : ℝ≥0<VAR>s : Set α<VAR>f✝ : α → β<VAR>f : α → ℝ<VAR>K : ℝ≥0<VAR>h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + ↑K * dist x y<GOAL>LipschitzOnWith K f s
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : b ⟶ a<VAR>f₁ : a ⟶ b<VAR>g₁ : b ⟶ a<VAR>f₂ : b ⟶ c<VAR>g₂ : c ⟶ b<VAR>adj₁ : f₁ ⊣ g₁<VAR>adj₂ : f₂ ⊣ g₂<GOAL>rightZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) = (ρ_ (g₂ ≫ g₁)).hom ≫ (λ_ (g₂ ≫ g₁)).inv
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ l₃ : List α<VAR>a b : α<VAR>m✝ n✝ n m : ℕ<VAR>l : List α<GOAL>dropSlice n m l = take n l ++ drop m (drop n l)
<VAR>R : Type u_1<VAR>inst✝¹ : NormedCommRing R<VAR>inst✝ : CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖<VAR>N : ℕ<GOAL>(Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ N.primesBelow, ∑' (n : ℕ), f (p ^ n))
<VAR>R : Type u_1<VAR>inst✝¹ : NormedCommRing R<VAR>inst✝ : CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖<VAR>N : ℕ<GOAL>(Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) (range N), ∑' (n : ℕ), f (p ^ n))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>s t : Set α<VAR>a✝ b✝ : α<VAR>inst✝¹ : SemilatticeInf γ<VAR>inst✝ : DenselyOrdered γ<VAR>a b : γ<VAR>hab : a < b<GOAL>IsLUB (Ioo a b) b
<GOAL>Module.rank ℚ ℝ = 𝔠
<GOAL>lift.{0, 0} #ℚ < lift.{0, 0} #ℝ