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>P : Cᵒᵖ ⥤ Type v₁<GOAL>(∀ (x : FamilyOfElements P S.arrows), x.Compatible → ∃! t, x.IsAmalgamation t) ↔ ∀ (f : S.functor ⟶ P), ∃! g, (↑(natTransEquivCompatibleFamily f)).IsAmalgamation (yonedaEquiv g)
<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>P : Cᵒᵖ ⥤ Type v₁<GOAL>(∀ (x : FamilyOfElements P S.arrows), x.Compatible → ∃! t, x.IsAmalgamation t) ↔ ∀ (b : { x // x.Compatible }), ∃! g, (↑(natTransEquivCompatibleFamily (natTransEquivCompatibleFamily.symm b))).IsAmalgamation (yonedaEquiv g)
<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>P : Cᵒᵖ ⥤ Type v₁<GOAL>(∀ (x : FamilyOfElements P S.arrows), x.Compatible → ∃! t, x.IsAmalgamation t) ↔ ∀ (a : FamilyOfElements P S.arrows) (b : a.Compatible), ∃! g, (↑(natTransEquivCompatibleFamily (natTransEquivCompatibleFamily.symm ⟨a, b⟩))).IsAmalgamation (yonedaEquiv g)
<VAR>Ω : Type u_1<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝³ : SMul R ℝ≥0<VAR>inst✝² : SMul R ℝ≥0∞<VAR>inst✝¹ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>μ : FiniteMeasure Ω<VAR>A : Set Ω<GOAL>μ.restrict A ≠ 0 ↔ μ A ≠ 0
<VAR>m n✝ n : ℕ<GOAL>(bif n.succ.bodd then 1 else 0) + 2 * n.succ.div2 = n.succ
<VAR>m n✝ n : ℕ<GOAL>(bif n.bodd then 0 else 1) + (bif n.bodd then n.div2.succ else n.div2) * 2 = n.succ
<VAR>m n✝ n : ℕ<GOAL>(bif n.bodd then 0 else 1) + (bif n.bodd then n.div2.succ else n.div2) * 2 = ((bif n.bodd then 1 else 0) + 2 * n.div2).succ
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq p<VAR>inst✝ : CommRing R<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>i : Fin r ⊕ Unit<VAR>k : ℕ<VAR>hk : k ≤ r<GOAL>((List.drop k (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : Ring R<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x y z : R<VAR>h : v x < 1<GOAL>v (1 - x) = 1
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : Ring R<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x y z : R<VAR>h : v (-x) < v 1<GOAL>v (1 - x) = 1
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : Ring R<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x y z : R<VAR>h : v (-x) < v 1<GOAL>v (1 + -x) = 1
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>inst✝ : T2Space M<VAR>hi : Fintype ι<VAR>s : Set M<VAR>f : SmoothBumpCovering ι I M s<VAR>x : M<VAR>hx : x ∈ s<VAR>y : M<VAR>a✝ : y ∈ s<VAR>h : f.embeddingPiTangent x = f.embeddingPiTangent y<GOAL>x = y
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>inst✝ : T2Space M<VAR>hi : Fintype ι<VAR>s : Set M<VAR>f : SmoothBumpCovering ι I M s<VAR>x : M<VAR>hx : x ∈ s<VAR>y : M<VAR>a✝ : y ∈ s<VAR>h : ∀ (a : ι), (↑(f.toFun a) x • ↑(extChartAt I (f.c a)) x, ↑(f.toFun a) x) = (↑(f.toFun a) y • ↑(extChartAt I (f.c a)) y, ↑(f.toFun a) y)<GOAL>x = y
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>inst✝ : T2Space M<VAR>hi : Fintype ι<VAR>s : Set M<VAR>f : SmoothBumpCovering ι I M s<VAR>x : M<VAR>hx : x ∈ s<VAR>y : M<VAR>a✝ : y ∈ s<VAR>h : ∀ (a : ι), (↑(f.toFun a) x • ↑(extChartAt I (f.c a)) x, ↑(f.toFun a) x) = (↑(f.toFun a) y • ↑(extChartAt I (f.c a)) y, ↑(f.toFun a) y)<VAR>h₁ : ↑(f.toFun (f.ind x hx)) x • ↑(extChartAt I (f.c (f.ind x hx))) x = ↑(f.toFun (f.ind x hx)) y • ↑(extChartAt I (f.c (f.ind x hx))) y<VAR>h₂ : ↑(f.toFun (f.ind x hx)) x = ↑(f.toFun (f.ind x hx)) y<GOAL>x = y
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>inst✝ : T2Space M<VAR>hi : Fintype ι<VAR>s : Set M<VAR>f : SmoothBumpCovering ι I M s<VAR>x : M<VAR>hx : x ∈ s<VAR>y : M<VAR>a✝ : y ∈ s<VAR>h : ∀ (a : ι), (↑(f.toFun a) x • ↑(extChartAt I (f.c a)) x, ↑(f.toFun a) x) = (↑(f.toFun a) y • ↑(extChartAt I (f.c a)) y, ↑(f.toFun a) y)<VAR>h₁ : ↑(f.toFun (f.ind x hx)) x • ↑(extChartAt I (f.c (f.ind x hx))) x = ↑(f.toFun (f.ind x hx)) y • ↑(extChartAt I (f.c (f.ind x hx))) y<VAR>h₂ : 1 = ↑(f.toFun (f.ind x hx)) y<GOAL>x = y
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>inst✝ : T2Space M<VAR>hi : Fintype ι<VAR>s : Set M<VAR>f : SmoothBumpCovering ι I M s<VAR>x : M<VAR>hx : x ∈ s<VAR>y : M<VAR>a✝ : y ∈ s<VAR>h : ∀ (a : ι), (↑(f.toFun a) x • ↑(extChartAt I (f.c a)) x, ↑(f.toFun a) x) = (↑(f.toFun a) y • ↑(extChartAt I (f.c a)) y, ↑(f.toFun a) y)<VAR>h₁ : ↑(extChartAt I (f.c (f.ind x hx))) x = ↑(extChartAt I (f.c (f.ind x hx))) y<VAR>h₂ : 1 = ↑(f.toFun (f.ind x hx)) y<GOAL>x = y
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>inst✝ : T2Space M<VAR>hi : Fintype ι<VAR>s : Set M<VAR>f : SmoothBumpCovering ι I M s<VAR>x : M<VAR>hx : x ∈ s<VAR>y : M<VAR>a✝ : y ∈ s<VAR>h : ∀ (a : ι), (↑(f.toFun a) x • ↑(extChartAt I (f.c a)) x, ↑(f.toFun a) x) = (↑(f.toFun a) y • ↑(extChartAt I (f.c a)) y, ↑(f.toFun a) y)<VAR>h₁ : ↑(extChartAt I (f.c (f.ind x hx))) x = ↑(extChartAt I (f.c (f.ind x hx))) y<VAR>h₂ : 1 = ↑(f.toFun (f.ind x hx)) y<VAR>this : y ∈ (extChartAt I (f.c (f.ind x hx))).source<GOAL>x = y
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>R : Type u_3<VAR>inst✝³ : Semiring R<VAR>inst✝² : Module R F<VAR>inst✝¹ : SMulCommClass 𝕜 R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>n : ℕ<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<VAR>h : UniqueDiffOn 𝕜 s<VAR>f g : 𝕜 → F<VAR>hn : 0 < n<VAR>c : F<GOAL>iteratedDerivWithin n (fun z => c - f z) s x = iteratedDerivWithin n (fun z => -f z) s x
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>R : Type u_3<VAR>inst✝³ : Semiring R<VAR>inst✝² : Module R F<VAR>inst✝¹ : SMulCommClass 𝕜 R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<VAR>h : UniqueDiffOn 𝕜 s<VAR>f g : 𝕜 → F<VAR>c : F<VAR>n : ℕ<VAR>hn : 0 < n.succ<GOAL>iteratedDerivWithin n.succ (fun z => c - f z) s x = iteratedDerivWithin n.succ (fun z => -f z) s x
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>R : Type u_3<VAR>inst✝³ : Semiring R<VAR>inst✝² : Module R F<VAR>inst✝¹ : SMulCommClass 𝕜 R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<VAR>h : UniqueDiffOn 𝕜 s<VAR>f g : 𝕜 → F<VAR>c : F<VAR>n : ℕ<VAR>hn : 0 < n.succ<GOAL>iteratedDerivWithin n (derivWithin (fun z => c - f z) s) s x = iteratedDerivWithin n (derivWithin (fun z => -f z) s) s x
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>R : Type u_3<VAR>inst✝³ : Semiring R<VAR>inst✝² : Module R F<VAR>inst✝¹ : SMulCommClass 𝕜 R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<VAR>h : UniqueDiffOn 𝕜 s<VAR>f g : 𝕜 → F<VAR>c : F<VAR>n : ℕ<VAR>hn : 0 < n.succ<GOAL>Set.EqOn (derivWithin (fun z => c - f z) s) (derivWithin (fun z => -f z) s) s
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>R : Type u_3<VAR>inst✝³ : Semiring R<VAR>inst✝² : Module R F<VAR>inst✝¹ : SMulCommClass 𝕜 R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<VAR>h : UniqueDiffOn 𝕜 s<VAR>f g : 𝕜 → F<VAR>c : F<VAR>n : ℕ<VAR>hn : 0 < n.succ<VAR>y : 𝕜<VAR>hy : y ∈ s<GOAL>derivWithin (fun z => c - f z) s y = derivWithin (fun z => -f z) s y
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>R : Type u_3<VAR>inst✝³ : Semiring R<VAR>inst✝² : Module R F<VAR>inst✝¹ : SMulCommClass 𝕜 R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<VAR>h : UniqueDiffOn 𝕜 s<VAR>f g : 𝕜 → F<VAR>c : F<VAR>n : ℕ<VAR>hn : 0 < n.succ<VAR>y : 𝕜<VAR>hy : y ∈ s<VAR>this : UniqueDiffWithinAt 𝕜 s y<GOAL>derivWithin (fun z => c - f z) s y = derivWithin (fun z => -f z) s y
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>R : Type u_3<VAR>inst✝³ : Semiring R<VAR>inst✝² : Module R F<VAR>inst✝¹ : SMulCommClass 𝕜 R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<VAR>h : UniqueDiffOn 𝕜 s<VAR>f g : 𝕜 → F<VAR>c : F<VAR>n : ℕ<VAR>hn : 0 < n.succ<VAR>y : 𝕜<VAR>hy : y ∈ s<VAR>this : UniqueDiffWithinAt 𝕜 s y<GOAL>derivWithin (fun z => c - f z) s y = -derivWithin f s y
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J X Y : Set α<VAR>N : Matroid α<VAR>h : N <r M<GOAL>N.E ⊂ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R✝ I J X Y R : Set α<VAR>h : M ↾ R <r M<GOAL>(M ↾ R).E ⊂ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R✝ I J X Y R : Set α<VAR>h : M ↾ R <r M<VAR>h' : (M ↾ R).E = M.E<GOAL>M = M ↾ R ↾ R
<VAR>F✝ : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝⁴ : CommMonoid α<VAR>inst✝³ : CommMonoid β<VAR>s✝ t : Multiset α<VAR>a : α<VAR>m : Multiset ι<VAR>f✝ g : ι → α<VAR>inst✝² : CommMonoid β<VAR>s : Multiset α<VAR>F : Type u_6<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : MonoidHomClass F α β<VAR>f : F<VAR>l : List α<GOAL>(map ⇑f ⟦l⟧).prod = f (prod ⟦l⟧)
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>a⁻¹ < 1 ↔ 1 < a
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>t : ↑(Icc v.tMin v.tMax)<GOAL>dist t v.t₀ ≤ v.tDist
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>t : ↑(Icc v.tMin v.tMax)<GOAL>|↑t - ↑v.t₀| ≤ v.tDist
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>t : ↑(Icc v.tMin v.tMax)<VAR>ht : t ≤ v.t₀<GOAL>|↑t - ↑v.t₀| ≤ v.tDist
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>t : ↑(Icc v.tMin v.tMax)<VAR>ht : v.t₀ ≤ t<GOAL>|↑t - ↑v.t₀| ≤ v.tDist
<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<GOAL>μ (closedBall 0 1) = μ (ball 0 1)
<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<GOAL>μ (closedBall 0 1) ≤ μ (ball 0 1)
<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>A : Tendsto (fun r => ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 1)) (𝓝[<] 1) (𝓝 (ENNReal.ofReal (1 ^ finrank ℝ E) * μ (closedBall 0 1)))<GOAL>μ (closedBall 0 1) ≤ μ (ball 0 1)
<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>A : Tendsto (fun r => ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 1)) (𝓝[<] 1) (𝓝 (μ (closedBall 0 1)))<GOAL>μ (closedBall 0 1) ≤ μ (ball 0 1)
<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>A : Tendsto (fun r => ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 1)) (𝓝[<] 1) (𝓝 (μ (closedBall 0 1)))<GOAL>∀ᶠ (c : ℝ) in 𝓝[<] 1, ENNReal.ofReal (c ^ finrank ℝ E) * μ (closedBall 0 1) ≤ μ (ball 0 1)
<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>A : Tendsto (fun r => ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 1)) (𝓝[<] 1) (𝓝 (μ (closedBall 0 1)))<VAR>r : ℝ<VAR>hr : r ∈ Ioo 0 1<GOAL>r ∈ {x | (fun c => ENNReal.ofReal (c ^ finrank ℝ E) * μ (closedBall 0 1) ≤ μ (ball 0 1)) x}
<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>A : Tendsto (fun r => ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 1)) (𝓝[<] 1) (𝓝 (μ (closedBall 0 1)))<VAR>r : ℝ<VAR>hr : r ∈ Ioo 0 1<GOAL>ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 1) ≤ μ (ball 0 1)
<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>A : Tendsto (fun r => ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 1)) (𝓝[<] 1) (𝓝 (μ (closedBall 0 1)))<VAR>r : ℝ<VAR>hr : r ∈ Ioo 0 1<GOAL>μ (closedBall 0 r) ≤ μ (ball 0 1)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : SimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 3)<VAR>j : Fin (n + 2)<VAR>H : i ≤ j.castSucc<GOAL>X.map (SimplexCategory.δ j.succ).op ≫ X.map (SimplexCategory.δ (i.castLT ⋯)).op = X.map (SimplexCategory.δ i).op ≫ X.map (SimplexCategory.δ j).op
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : ClosedIicTopology α<VAR>s : Set α<VAR>hs : IsCompact s<VAR>ne_s : s.Nonempty<GOAL>∃ x, IsLeast s x
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : ClosedIicTopology α<VAR>s : Set α<VAR>hs : IsCompact s<VAR>ne_s : s.Nonempty<VAR>this : Nonempty ↑s<GOAL>∃ x, IsLeast s x
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : ClosedIicTopology α<VAR>s : Set α<VAR>hs : IsCompact s<VAR>ne_s : s.Nonempty<VAR>this : Nonempty ↑s<GOAL>(s ∩ ⋂ x ∈ s, Iic x).Nonempty
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : ClosedIicTopology α<VAR>s : Set α<VAR>hs : IsCompact s<VAR>ne_s : s.Nonempty<VAR>this : Nonempty ↑s<GOAL>(s ∩ ⋂ x, Iic ↑x).Nonempty
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : ClosedIicTopology α<VAR>s : Set α<VAR>hs : IsCompact s<VAR>ne_s : s.Nonempty<VAR>this : Nonempty ↑s<VAR>H : ¬(s ∩ ⋂ x, Iic ↑x).Nonempty<GOAL>False
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : ClosedIicTopology α<VAR>s : Set α<VAR>hs : IsCompact s<VAR>ne_s : s.Nonempty<VAR>this : Nonempty ↑s<VAR>H : s ∩ ⋂ x, Iic ↑x = ∅<GOAL>False
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : ClosedIicTopology α<VAR>s : Set α<VAR>hs : IsCompact s<VAR>ne_s : s.Nonempty<VAR>this : Nonempty ↑s<VAR>H : s ∩ ⋂ x, Iic ↑x = ∅<VAR>x : ↑s<VAR>hx : s ∩ Iic ↑x = ∅<GOAL>False
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : SeminormedRing 𝕜<VAR>inst✝ : SMul 𝕜 E<VAR>s t u v A B : Set E<GOAL>(∃ i, True ∧ ∀ ⦃x : 𝕜⦄, x ∈ norm ⁻¹' Ici i → B ⊆ x • A) ↔ ∃ r, ∀ (c : 𝕜), r ≤ ‖c‖ → B ⊆ c • A
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : SeminormedRing 𝕜<VAR>inst✝ : SMul 𝕜 E<VAR>s t u v A B : Set E<GOAL>(∃ i, ∀ ⦃x : 𝕜⦄, x ∈ norm ⁻¹' Ici i → B ⊆ x • A) ↔ ∃ r, ∀ (c : 𝕜), r ≤ ‖c‖ → B ⊆ c • A
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>x : β<GOAL>x ∈ r.inv.dom ↔ x ∈ r.codom
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>inst✝² : HasImage f<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroObject C<GOAL>(imageSubobject 0).arrow = 0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>inst✝² : HasImage f<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroObject C<GOAL>(imageSubobjectIso 0).hom ≫ image.ι 0 = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>hc : c < 0<GOAL>a < b / c ↔ b < c * a
<VAR>p n : ℕ<VAR>hn : n ≠ 0<GOAL>log 2 n ≠ padicValNat 2 (n + 1)
<VAR>p n : ℕ<VAR>hn : n ≠ 0<GOAL>¬(2 ^ padicValNat 2 (n + 1) ≤ n ∧ n < 2 ^ (padicValNat 2 (n + 1) + 1))
<VAR>p n : ℕ<VAR>hn : n ≠ 0<VAR>h1 : 2 ^ padicValNat 2 (n + 1) ≤ n<VAR>h2 : n < 2 ^ (padicValNat 2 (n + 1) + 1)<GOAL>False
<VAR>p n : ℕ<VAR>hn : n ≠ 0<VAR>h1 : 2 ^ padicValNat 2 (n + 1) * 1 < n + 1<VAR>h2 : n < 2 ^ (padicValNat 2 (n + 1) + 1)<GOAL>False
<VAR>p n : ℕ<VAR>hn : n ≠ 0<VAR>h1 : 2 ^ padicValNat 2 (n + 1) * 1 < n + 1<VAR>h2 : n + 1 ≤ 2 ^ padicValNat 2 (n + 1) * 2<GOAL>False
<VAR>p n : ℕ<VAR>hn : n ≠ 0<VAR>h1 : 2 ^ padicValNat 2 (n + 1) * 1 < n + 1<VAR>h2 : n + 1 ≤ 2 ^ padicValNat 2 (n + 1) * 2<GOAL>2 ^ padicValNat 2 (n + 1) * (1 + 1) ≠ n + 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>f✝ : α → β<VAR>x y : α<VAR>r : ℝ≥0∞<VAR>f : α → β → γ<VAR>Kα Kβ : ℝ≥0<VAR>hα : ∀ (b : β), LipschitzWith Kα fun a => f a b<VAR>hβ : ∀ (a : α), LipschitzWith Kβ (f a)<VAR>a₁ : α<VAR>b₁ : β<VAR>a₂ : α<VAR>b₂ : β<GOAL>edist (uncurry f (a₁, b₁)) (uncurry f (a₂, b₂)) ≤ ↑(Kα + Kβ) * edist (a₁, b₁) (a₂, b₂)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>f✝ : α → β<VAR>x y : α<VAR>r : ℝ≥0∞<VAR>f : α → β → γ<VAR>Kα Kβ : ℝ≥0<VAR>hα : ∀ (b : β), LipschitzWith Kα fun a => f a b<VAR>hβ : ∀ (a : α), LipschitzWith Kβ (f a)<VAR>a₁ : α<VAR>b₁ : β<VAR>a₂ : α<VAR>b₂ : β<GOAL>edist (f a₁ b₁) (f a₂ b₂) ≤ ↑Kα * edist (a₁, b₁) (a₂, b₂) + ↑Kβ * edist (a₁, b₁) (a₂, b₂)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>f✝ : α → β<VAR>x y : α<VAR>r : ℝ≥0∞<VAR>f : α → β → γ<VAR>Kα Kβ : ℝ≥0<VAR>hα : ∀ (b : β), LipschitzWith Kα fun a => f a b<VAR>hβ : ∀ (a : α), LipschitzWith Kβ (f a)<VAR>a₁ : α<VAR>b₁ : β<VAR>a₂ : α<VAR>b₂ : β<GOAL>edist (f a₁ b₁) (f a₂ b₁) + edist (f a₂ b₁) (f a₂ b₂) ≤ ↑Kα * edist (a₁, b₁) (a₂, b₂) + ↑Kβ * edist (a₁, b₁) (a₂, b₂)
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ ψ : L.BoundedFormula α (n + 1)<VAR>h : T.SemanticallyEquivalent φ ψ<GOAL>T.SemanticallyEquivalent (∀'φ) (∀'ψ)
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ ψ : L.BoundedFormula α (n + 1)<VAR>h : T.SemanticallyEquivalent φ ψ<GOAL>∀ (M : T.ModelType) (v : α → ↑M) (xs : Fin n → ↑M), (∀ (a : ↑M), φ.Realize v (Fin.snoc xs a)) ↔ ∀ (a : ↑M), ψ.Realize v (Fin.snoc xs a)
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α β : TypeVec.{u_1} n<VAR>F' : TypeVec.{u_1} n → Type u<VAR>inst✝¹ : MvFunctor F'<VAR>inst✝ : LawfulMvFunctor F'<VAR>R : β ⊗ β ⟹ repeat n Prop<VAR>x : F' α<VAR>f g : α ⟹ β<VAR>h : α ⟹ Subtype_ R<VAR>hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag<GOAL>LiftR' R (f <$$> x) (g <$$> x)
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α β : TypeVec.{u_1} n<VAR>F' : TypeVec.{u_1} n → Type u<VAR>inst✝¹ : MvFunctor F'<VAR>inst✝ : LawfulMvFunctor F'<VAR>R : β ⊗ β ⟹ repeat n Prop<VAR>x : F' α<VAR>f g : α ⟹ β<VAR>h : α ⟹ Subtype_ R<VAR>hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag<GOAL>∃ u, (prod.fst ⊚ subtypeVal R) <$$> u = f <$$> x ∧ (prod.snd ⊚ subtypeVal R) <$$> u = g <$$> x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α β : TypeVec.{u_1} n<VAR>F' : TypeVec.{u_1} n → Type u<VAR>inst✝¹ : MvFunctor F'<VAR>inst✝ : LawfulMvFunctor F'<VAR>R : β ⊗ β ⟹ repeat n Prop<VAR>x : F' α<VAR>f g : α ⟹ β<VAR>h : α ⟹ Subtype_ R<VAR>hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag<GOAL>(prod.fst ⊚ subtypeVal R) <$$> h <$$> x = f <$$> x ∧ (prod.snd ⊚ subtypeVal R) <$$> h <$$> x = g <$$> x