ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<VAR>j✝ k✝ j k m : ℤ<VAR>h₁₁ : ↑k < ↑j / r<VAR>h₁₂ : (↑j + 1) / r ≤ ↑k + 1<VAR>h₂₁ : ↑m ≤ ↑j / s<VAR>h₂₂ : (↑j + 1) / s < ↑m + 1<GOAL>False
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<VAR>j✝ k✝ j k m : ℤ<VAR>h₁₁ : ↑k < ↑j / r<VAR>h₁₂ : (↑j + 1) / r ≤ ↑k + 1<VAR>h₂₁ : ↑m ≤ ↑j / s<VAR>h₂₂ : (↑j + 1) / s < ↑m + 1<VAR>h₃ : ↑k + ↑m < ↑j / r + ↑j / s<GOAL>False
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<VAR>j✝ k✝ j k m : ℤ<VAR>h₁₁ : ↑k < ↑j / r<VAR>h₁₂ : (↑j + 1) / r ≤ ↑k + 1<VAR>h₂₁ : ↑m ≤ ↑j / s<VAR>h₂₂ : (↑j + 1) / s < ↑m + 1<VAR>h₃ : ↑k + ↑m < ↑j / r + ↑j / s<VAR>h₄ : (↑j + 1) / r + (↑j + 1) / s < ↑k + 1 + (↑m + 1)<GOAL>False
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<VAR>j✝ k✝ j k m : ℤ<VAR>h₁₁ : ↑k < ↑j / r<VAR>h₁₂ : (↑j + 1) / r ≤ ↑k + 1<VAR>h₂₁ : ↑m ≤ ↑j / s<VAR>h₂₂ : (↑j + 1) / s < ↑m + 1<VAR>h₃ : ↑k + ↑m < ↑j<VAR>h₄ : ↑j + 1 < ↑k + 1 + (↑m + 1)<GOAL>False
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<VAR>j✝ k✝ j k m : ℤ<VAR>h₁₁ : ↑k < ↑j / r<VAR>h₁₂ : (↑j + 1) / r ≤ ↑k + 1<VAR>h₂₁ : ↑m ≤ ↑j / s<VAR>h₂₂ : (↑j + 1) / s < ↑m + 1<VAR>h₃ : ↑k + ↑m < ↑j<VAR>h₄ : ↑j < ↑k + ↑m + ↑1<GOAL>False
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<VAR>j✝ k✝ j k m : ℤ<VAR>h₁₁ : ↑k < ↑j / r<VAR>h₁₂ : (↑j + 1) / r ≤ ↑k + 1<VAR>h₂₁ : ↑m ≤ ↑j / s<VAR>h₂₂ : (↑j + 1) / s < ↑m + 1<VAR>h₃ : k + m < j<VAR>h₄ : j ≤ k + m<GOAL>False
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<GOAL>multiplicity E ≤ 5 ^ finrank ℝ E
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<GOAL>{N | ∃ s, s.card = N ∧ (∀ c ∈ s, ‖c‖ ≤ 2) ∧ ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖}.Nonempty
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<GOAL>∀ b ∈ {N | ∃ s, s.card = N ∧ (∀ c ∈ s, ‖c‖ ≤ 2) ∧ ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖}, b ≤ 5 ^ finrank ℝ E
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<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✝³ : Module.Free R M<VAR>inst✝² : Module.Finite R M<VAR>inst✝¹ : Module.Free R L<VAR>inst✝ : Module.Finite R L<VAR>I : LieIdeal R L<VAR>x : L<GOAL>x ∈ (lieIdealSubalgebra R L (killingCompl R L ⊤)).toSubmodule ↔ x ∈ LinearMap.ker (killingForm R L)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝² : Field A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>p : A[X]<VAR>pmonic : p.Monic<VAR>hp : (Polynomial.aeval x) p = 0<VAR>pmin : ∀ (q : A[X]), q.Monic → (Polynomial.aeval x) q = 0 → p.degree ≤ q.degree<VAR>hx : IsIntegral A x<GOAL>minpoly A x = p
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝² : Field A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>p : A[X]<VAR>pmonic : p.Monic<VAR>hp : (Polynomial.aeval x) p = 0<VAR>pmin : ∀ (q : A[X]), q.Monic → (Polynomial.aeval x) q = 0 → p.degree ≤ q.degree<VAR>hx : IsIntegral A x<GOAL>minpoly A x - p = 0
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝² : Field A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>p : A[X]<VAR>pmonic : p.Monic<VAR>hp : (Polynomial.aeval x) p = 0<VAR>pmin : ∀ (q : A[X]), q.Monic → (Polynomial.aeval x) q = 0 → p.degree ≤ q.degree<VAR>hx : IsIntegral A x<VAR>hnz : ¬minpoly A x - p = 0<GOAL>False
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝² : Field A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>p : A[X]<VAR>pmonic : p.Monic<VAR>hp : (Polynomial.aeval x) p = 0<VAR>pmin : ∀ (q : A[X]), q.Monic → (Polynomial.aeval x) q = 0 → p.degree ≤ q.degree<VAR>hx : IsIntegral A x<VAR>hnz : ¬minpoly A x - p = 0<GOAL>(minpoly A x - p).degree < (minpoly A x).degree
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝² : Field A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>p : A[X]<VAR>pmonic : p.Monic<VAR>hp : (Polynomial.aeval x) p = 0<VAR>pmin : ∀ (q : A[X]), q.Monic → (Polynomial.aeval x) q = 0 → p.degree ≤ q.degree<VAR>hx : IsIntegral A x<VAR>hnz : ¬minpoly A x - p = 0<GOAL>(minpoly A x).leadingCoeff = p.leadingCoeff
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝² : Field A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>p : A[X]<VAR>pmonic : p.Monic<VAR>hp : (Polynomial.aeval x) p = 0<VAR>pmin : ∀ (q : A[X]), q.Monic → (Polynomial.aeval x) q = 0 → p.degree ≤ q.degree<VAR>hx : IsIntegral A x<VAR>hnz : ¬minpoly A x - p = 0<GOAL>(minpoly A x).degree = p.degree
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x y : P<VAR>h : x ≠ y<GOAL>Sbtw R y x ((pointReflection R x) y)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x y : P<VAR>h : x ≠ y<GOAL>x ≠ (pointReflection R x) y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x y : P<VAR>h : x ≠ y<GOAL>(pointReflection R x) x ≠ (pointReflection R x) y
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>inst✝ : Field k<VAR>x✝ : k⟦X⟧<GOAL>x✝ ∈ RingHom.ker (constantCoeff k) ↔ x✝ ∈ maximalIdeal k⟦X⟧
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n₁ n₂ n₃ : ℕ<VAR>h1 : n₁ ≤ n₂<VAR>h2 : n₂ ≤ n₃<VAR>x : TruncatedWittVector p n₃ R<GOAL>((truncate h1).comp (truncate h2)) x = (truncate ⋯) x
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>A : Type u_2<VAR>inst✝¹ : Category.{?u.75369, u_2} A<VAR>inst✝ : Abelian A<VAR>X Y : CosimplicialObject C<VAR>n : ℕ<GOAL>objD X n ≫ objD X (n + 1) = 0
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<GOAL>cosZeta (↑x) (2 * ↑k) = (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / 2 / ↑(2 * k)! * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<GOAL>∑' (b : ℕ), ↑(Real.cos (2 * π * x * ↑b)) / ↑b ^ (2 * ↑k) = (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / 2 / ↑(2 * k)! * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<GOAL>1 < (2 * ↑k).re
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a✝ b c u a : αˣ<GOAL>↑a = 1 ↔ a = 1
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : AddMonoid B<VAR>inst✝¹ : Monoid M<VAR>inst✝ : Monoid N<VAR>ψ✝ : AddChar A M<VAR>f : M →* N<VAR>hf : Injective ⇑f<VAR>ψ χ : AddChar B M<VAR>h : (fun ψ => f.compAddChar ψ) ψ = (fun ψ => f.compAddChar ψ) χ<GOAL>ψ = χ
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : AddMonoid B<VAR>inst✝¹ : Monoid M<VAR>inst✝ : Monoid N<VAR>ψ✝ : AddChar A M<VAR>f : M →* N<VAR>hf : Injective ⇑f<VAR>ψ χ : AddChar B M<VAR>h : ⇑((fun ψ => f.compAddChar ψ) ψ) = ⇑((fun ψ => f.compAddChar ψ) χ)<GOAL>⇑ψ = ⇑χ
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set α<VAR>x y : α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : SemilatticeInf β<VAR>hf : AntitoneOn f s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>f (x ⊔ y) = f x ⊓ f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t✝ u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>t : Finset β<VAR>e : α ≃ β<VAR>hst : ∀ (i : α), i ∈ s ↔ e i ∈ t<GOAL>s.card = t.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : BorelSpace α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : BorelSpace β<VAR>inst✝¹ : MeasurableSpace δ<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasureOnCompacts μ<VAR>f : α ≃ₜ β<VAR>K : Set β<VAR>hK : IsCompact K<GOAL>(Measure.map (⇑f) μ) K < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : BorelSpace α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : BorelSpace β<VAR>inst✝¹ : MeasurableSpace δ<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasureOnCompacts μ<VAR>f : α ≃ₜ β<VAR>K : Set β<VAR>hK : IsCompact K<GOAL>μ (⇑f.toMeasurableEquiv ⁻¹' K) < ⊤
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ : Multiset α<VAR>a✝ b a : α<VAR>s t : Multiset α<VAR>h : a ∉ t<GOAL>(s + t).erase a = s.erase a + t
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : CompleteLattice β<GOAL>Continuous ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : CompleteLattice β<GOAL>Continuous (sSup ∅)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : LinearOrderedSemiring R<VAR>a b : R<VAR>m n : ℕ<VAR>ha₀ : 0 < a<VAR>ha₁ : a ≠ 1<GOAL>Injective fun x => a ^ x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : LinearOrderedSemiring R<VAR>a b : R<VAR>m n : ℕ<VAR>ha₀ : 0 < a<VAR>ha₁✝ : a ≠ 1<VAR>ha₁ : a < 1<GOAL>Injective fun x => a ^ x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : LinearOrderedSemiring R<VAR>a b : R<VAR>m n : ℕ<VAR>ha₀ : 0 < a<VAR>ha₁✝ : a ≠ 1<VAR>ha₁ : 1 < a<GOAL>Injective fun x => a ^ x
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>x : n → R<GOAL>0 ≤ star x ⬝ᵥ 1 *ᵥ x
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>x : n → R<GOAL>0 ≤ star x ⬝ᵥ x
<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>x y z : E<GOAL>⟪x - y, z⟫_𝕜 = ⟪x, z⟫_𝕜 - ⟪y, z⟫_𝕜
<VAR>α : Type u_1<VAR>l : List α<VAR>a : α<GOAL>[a] <+~ l ↔ a ∈ l
<VAR>α : Type u_1<VAR>l : List α<VAR>a : α<VAR>x✝ : [a] <+~ l<VAR>s : List α<VAR>hla : s ~ [a]<VAR>h : s <+ l<GOAL>a ∈ l
<VAR>M : Type u_1<VAR>inst✝² : Mul M<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Mul β<GOAL>commProb (α → β) = commProb β ^ card α
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<GOAL>𝟙 (X _[0]) - 𝟙 (X _[0]) = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝⁴ : LinearOrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : DenselyOrdered 𝕜<VAR>inst✝ : NoZeroSMulDivisors 𝕜 E<VAR>A B : Set E<VAR>x : E<VAR>hA : Convex 𝕜 A<GOAL>x ∈ extremePoints 𝕜 A ↔ x ∈ A ∧ Convex 𝕜 (A \ {x})
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝⁴ : LinearOrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : DenselyOrdered 𝕜<VAR>inst✝ : NoZeroSMulDivisors 𝕜 E<VAR>A B : Set E<VAR>x : E<VAR>hA : Convex 𝕜 A<GOAL>x ∈ A ∧ Convex 𝕜 (A \ {x}) → x ∈ extremePoints 𝕜 A
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝⁴ : LinearOrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : DenselyOrdered 𝕜<VAR>inst✝ : NoZeroSMulDivisors 𝕜 E<VAR>A B : Set E<VAR>x : E<VAR>hA : Convex 𝕜 A<VAR>hxA : x ∈ A<VAR>hAx : Convex 𝕜 (A \ {x})<GOAL>x ∈ extremePoints 𝕜 A
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝⁴ : LinearOrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : DenselyOrdered 𝕜<VAR>inst✝ : NoZeroSMulDivisors 𝕜 E<VAR>A B : Set E<VAR>x : E<VAR>hA : Convex 𝕜 A<VAR>hxA : x ∈ A<VAR>hAx : Convex 𝕜 (A \ {x})<VAR>x₁ : E<VAR>hx₁ : x₁ ∈ A<VAR>x₂ : E<VAR>hx₂ : x₂ ∈ A<VAR>hx : x ∈ [x₁-[𝕜]x₂]<GOAL>x₁ = x ∨ x₂ = x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝⁴ : LinearOrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : DenselyOrdered 𝕜<VAR>inst✝ : NoZeroSMulDivisors 𝕜 E<VAR>A B : Set E<VAR>x : E<VAR>hA : Convex 𝕜 A<VAR>hxA : x ∈ A<VAR>hAx : ∀ ⦃x_1 : E⦄, x_1 ∈ A \ {x} → ∀ ⦃y : E⦄, y ∈ A \ {x} → [x_1-[𝕜]y] ⊆ A \ {x}<VAR>x₁ : E<VAR>hx₁ : x₁ ∈ A<VAR>x₂ : E<VAR>hx₂ : x₂ ∈ A<VAR>hx : x ∈ [x₁-[𝕜]x₂]<GOAL>x₁ = x ∨ x₂ = x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝⁴ : LinearOrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : DenselyOrdered 𝕜<VAR>inst✝ : NoZeroSMulDivisors 𝕜 E<VAR>A B : Set E<VAR>x : E<VAR>hA : Convex 𝕜 A<VAR>hxA : x ∈ A<VAR>hAx : ∀ ⦃x_1 : E⦄, x_1 ∈ A \ {x} → ∀ ⦃y : E⦄, y ∈ A \ {x} → [x_1-[𝕜]y] ⊆ A \ {x}<VAR>x₁ : E<VAR>hx₁ : x₁ ∈ A<VAR>x₂ : E<VAR>hx₂ : x₂ ∈ A<VAR>hx : x ∈ [x₁-[𝕜]x₂]<VAR>h : x₁ ≠ x ∧ x₂ ≠ x<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r r' : α → α → Prop<VAR>inst✝ : IsStrictOrder α r<VAR>s t : Set α<GOAL>s.WellFoundedOn r ↔ ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), f n ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r r' : α → α → Prop<VAR>inst✝ : IsStrictOrder α r<VAR>s t : Set α<GOAL>Nonempty ((fun x x_1 => x > x_1) ↪r fun a b => r a b ∧ a ∈ s ∧ b ∈ s) ↔ ∃ x, ∀ (n : ℕ), x n ∈ s
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝² : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq δ<VAR>s t : Finset δ<VAR>f✝ g : ((i : δ) → π i) → ℝ≥0∞<VAR>x✝ y✝ : (i : δ) → π i<VAR>i✝ i : δ<VAR>hi : i ∈ s<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>x : (i : δ) → π i<VAR>y : π i<GOAL>(∫⋯∫⁻_s, f ∂μ) (update x i y) = (∫⋯∫⁻_s, f ∂μ) x
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝² : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq δ<VAR>s t : Finset δ<VAR>f✝ g : ((i : δ) → π i) → ℝ≥0∞<VAR>x✝ y✝ : (i : δ) → π i<VAR>i✝ i : δ<VAR>hi : i ∈ s<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>x : (i : δ) → π i<VAR>y : π i<GOAL>∀ i_1 ∉ s, update x i y i_1 = x i_1
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝² : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq δ<VAR>s t : Finset δ<VAR>f✝ g : ((i : δ) → π i) → ℝ≥0∞<VAR>x✝ y✝ : (i : δ) → π i<VAR>i✝ i : δ<VAR>hi : i ∈ s<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>x : (i : δ) → π i<VAR>y : π i<VAR>j : δ<VAR>hj : j ∉ s<VAR>this : j ≠ i<GOAL>update x i y j = x j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>a b : α<VAR>n : ℕ<GOAL>(s.sym n).Nonempty ↔ n = 0 ∨ s.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>k : ℕ<VAR>r : ℝ<VAR>hr : |r| < 1<VAR>h0 : ¬r = 0<GOAL>Tendsto (fun n => ↑n ^ k * r ^ n) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>k : ℕ<VAR>r : ℝ<VAR>hr : |r| < 1<VAR>h0 : ¬r = 0<VAR>hr' : 1 < |r|⁻¹<GOAL>Tendsto (fun n => ↑n ^ k * r ^ n) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>k : ℕ<VAR>r : ℝ<VAR>hr : |r| < 1<VAR>h0 : ¬r = 0<VAR>hr' : 1 < |r|⁻¹<GOAL>Tendsto (fun x => ‖↑x ^ k * r ^ x‖) atTop (𝓝 0)
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>S : Type u_3<VAR>inst✝ : DivisionMonoid G<VAR>a b c d : G<VAR>hab : Commute a b<GOAL>(a * b)⁻¹ = a⁻¹ * b⁻¹
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y p₁ : P<VAR>h : p₁ ∈ s<GOAL>s.SSameSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y p₁ : P<VAR>h : p₁ ∈ s<GOAL>x ∉ s → (y ∉ s ∧ (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)) ↔ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂))
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y p₁ : P<VAR>h : p₁ ∈ s<VAR>hx : x ∉ s<GOAL>y ∉ s ∧ (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)) ↔ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
<VAR>R : Type u<VAR>inst✝⁴ : CommSemiring R<VAR>M₁ : Type v<VAR>M₂ : Type v'<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : AddCommMonoid M₂<VAR>inst✝ : Module R M₂<VAR>f m : Dual R M₁<GOAL>m ∈ range (dualMap f) ↔ m ∈ Submodule.span R {f}
<VAR>R : Type u<VAR>inst✝⁴ : CommSemiring R<VAR>M₁ : Type v<VAR>M₂ : Type v'<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : AddCommMonoid M₂<VAR>inst✝ : Module R M₂<VAR>f m : Dual R M₁<GOAL>m ∈ range (dualMap f) ↔ ∃ a, a • f = m
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>x : Finset α<VAR>h0 : x.Nonempty<GOAL>∑ m ∈ x.powerset, (-1) ^ m.card = 0
<VAR>a b : ℤ<VAR>hb0 : 0 < b<VAR>h : a.natAbs.Coprime b.natAbs<GOAL>↑(↑a / ↑b).den = b
<VAR>p : ℕ → Prop<VAR>x : ℕ<VAR>h : p x<GOAL>∃ n, (∀ (hf : (setOf p).Finite), n < hf.toFinset.card) ∧ nth p n = x
<VAR>p : ℕ → Prop<VAR>x : ℕ<VAR>h : p x<VAR>hf : (setOf p).Finite<GOAL>∃ n, (∀ (hf : (setOf p).Finite), n < hf.toFinset.card) ∧ nth p n = x
<VAR>p : ℕ → Prop<VAR>x : ℕ<VAR>h : p x<VAR>hf : (setOf p).Infinite<GOAL>∃ n, (∀ (hf : (setOf p).Finite), n < hf.toFinset.card) ∧ nth p n = x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : AddCommMonoid ι<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>f : NumDenSameDeg 𝒜 x<VAR>h : f.den = 0<GOAL>mk f = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : AddCommMonoid ι<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>f : NumDenSameDeg 𝒜 x<VAR>h : f.den = 0<VAR>this : Subsingleton (HomogeneousLocalization 𝒜 x)<GOAL>mk f = 0
<VAR>re✝¹ im✝¹ re✝ im✝ : ℤ<GOAL>toComplex { re := re✝¹, im := im✝¹ } = toComplex { re := re✝, im := im✝ } ↔ { re := re✝¹, im := im✝¹ } = { re := re✝, im := im✝ }
<VAR>x y : ℝ<VAR>a : Cauchy abs<GOAL>(Real.neg { cauchy := a }).cauchy = -{ cauchy := a }.cauchy
<VAR>a b : ℝ<VAR>f : ℝ → ℝ<VAR>c : ContinuousOn f (Set.Icc a b)<VAR>ε : ℝ<VAR>pos : 0 < ε<GOAL>∃ p, ∀ x ∈ Set.Icc a b, |Polynomial.eval x p - f x| < ε
<VAR>a b : ℝ<VAR>f : ℝ → ℝ<VAR>c : ContinuousOn f (Set.Icc a b)<VAR>ε : ℝ<VAR>pos : 0 < ε<VAR>f' : C(↑(Set.Icc a b), ℝ) := { toFun := fun x => f ↑x, continuous_toFun := ⋯ }<GOAL>∃ p, ∀ x ∈ Set.Icc a b, |Polynomial.eval x p - f x| < ε
<VAR>a b✝ : ℝ<VAR>f : ℝ → ℝ<VAR>c : ContinuousOn f (Set.Icc a b✝)<VAR>ε : ℝ<VAR>pos : 0 < ε<VAR>f' : C(↑(Set.Icc a b✝), ℝ) := { toFun := fun x => f ↑x, continuous_toFun := ⋯ }<VAR>p : ℝ[X]<VAR>b : ‖p.toContinuousMapOn (Set.Icc a b✝) - f'‖ < ε<GOAL>∃ p, ∀ x ∈ Set.Icc a b✝, |Polynomial.eval x p - f x| < ε
<VAR>a b✝ : ℝ<VAR>f : ℝ → ℝ<VAR>c : ContinuousOn f (Set.Icc a b✝)<VAR>ε : ℝ<VAR>pos : 0 < ε<VAR>f' : C(↑(Set.Icc a b✝), ℝ) := { toFun := fun x => f ↑x, continuous_toFun := ⋯ }<VAR>p : ℝ[X]<VAR>b : ‖p.toContinuousMapOn (Set.Icc a b✝) - f'‖ < ε<GOAL>∀ x ∈ Set.Icc a b✝, |Polynomial.eval x p - f x| < ε
<VAR>a b✝ : ℝ<VAR>f : ℝ → ℝ<VAR>c : ContinuousOn f (Set.Icc a b✝)<VAR>ε : ℝ<VAR>pos : 0 < ε<VAR>f' : C(↑(Set.Icc a b✝), ℝ) := { toFun := fun x => f ↑x, continuous_toFun := ⋯ }<VAR>p : ℝ[X]<VAR>b : ∀ (x : ↑(Set.Icc a b✝)), ‖(p.toContinuousMapOn (Set.Icc a b✝) - f') x‖ < ε<GOAL>∀ x ∈ Set.Icc a b✝, |Polynomial.eval x p - f x| < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Ord α<VAR>inst✝ : Ord β<GOAL>compare = compareLex (compareOn fun x => x.fst) (compareOn fun x => x.snd)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Ord α<VAR>inst✝ : Ord β<VAR>a b : α × β<GOAL>compare a b = compareLex (compareOn fun x => x.fst) (compareOn fun x => x.snd) a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → ℝ≥0∞<VAR>hf0 : tsum f ≠ 0<VAR>hf : tsum f ≠ ⊤<VAR>a : α<GOAL>a ∈ (normalize f hf0 hf).support ↔ a ∈ Function.support f
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>h : 0 < ⌊a⌋₊<VAR>ha : a ≤ 0<GOAL>0 < 0
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝³ : MulZeroClass α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : PosMulMono α<VAR>inst✝ : MulPosMono α<VAR>hab : 0 < a * b<GOAL>0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝³ : MulZeroClass α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : PosMulMono α<VAR>inst✝ : MulPosMono α<VAR>hab : 0 < a * b<VAR>ha : a < 0<GOAL>0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
<VAR>α : Type u_1<VAR>b c d : α<VAR>inst✝³ : MulZeroClass α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : PosMulMono α<VAR>inst✝ : MulPosMono α<VAR>hab : 0 < 0 * b<GOAL>0 < 0 ∧ 0 < b ∨ 0 < 0 ∧ b < 0
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝³ : MulZeroClass α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : PosMulMono α<VAR>inst✝ : MulPosMono α<VAR>hab : 0 < a * b<VAR>ha : 0 < a<GOAL>0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>B : Finset (Finset α)<VAR>n : ℕ<VAR>h : ∀ a ∈ s, (filter (fun x => a ∈ x) B).card ≤ n<GOAL>∑ t ∈ B, (s ∩ t).card ≤ s.card * n
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>B : Finset (Finset α)<VAR>n : ℕ<VAR>h : ∀ a ∈ s, (filter (fun x => a ∈ x) B).card ≤ n<GOAL>∑ t ∈ B, (s ∩ t).card ≤ ∑ x ∈ s, (filter (fun x_1 => x ∈ x_1) B).card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>B : Finset (Finset α)<VAR>n : ℕ<VAR>h : ∀ a ∈ s, (filter (fun x => a ∈ x) B).card ≤ n<GOAL>(∑ x ∈ B, ∑ a ∈ s, if a ∈ x then 1 else 0) ≤ ∑ x ∈ s, ∑ a ∈ B, if x ∈ a then 1 else 0
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>inst✝⁶ : CommRing A<VAR>S : Submonoid A<VAR>hS : S ≤ A⁰<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra A K<VAR>inst✝³ : IsFractionRing A K<VAR>B : Type u_3<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : IsLocalization S B<VAR>x : K<GOAL>x ∈ (mapToFractionRing K S B hS).range ↔ ∃ a s, ∃ (_ : s ∈ S), x = (algebraMap A K) a * ((algebraMap A K) s)⁻¹
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>inst✝⁶ : CommRing A<VAR>S : Submonoid A<VAR>hS : S ≤ A⁰<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra A K<VAR>inst✝³ : IsFractionRing A K<VAR>B : Type u_3<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : IsLocalization S B<VAR>x : K<GOAL>(∃ a s, ∃ (hs : s ∈ S), x = IsLocalization.mk' K a ⟨s, ⋯⟩) ↔ ∃ a s, ∃ (_ : s ∈ S), x = (algebraMap A K) a * ((algebraMap A K) s)⁻¹
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>inst✝⁶ : CommRing A<VAR>S : Submonoid A<VAR>hS : S ≤ A⁰<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra A K<VAR>inst✝³ : IsFractionRing A K<VAR>B : Type u_3<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : IsLocalization S B<VAR>x : K<VAR>x✝² x✝¹ : A<VAR>x✝ : x✝¹ ∈ S<GOAL>(algebraMap A K) x✝² * ((algebraMap A K) x✝¹)⁻¹ = IsLocalization.mk' K x✝² ⟨x✝¹, ⋯⟩