ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>hi : ↑s i < 0<VAR>hi₁ : MeasurableSet i<VAR>h : ¬restrict s i ≤ restrict 0 i<VAR>hn : ∀ (n : ℕ), ¬restrict s (i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤ restrict 0 (i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<VAR>A : Set α := i \ ⋃ l, MeasureTheory.SignedMeasure.restrictNonposSeq s i l<VAR>hA : A = i \ ⋃ l, MeasureTheory.SignedMeasure.restrictNonposSeq s i l<VAR>bdd : ℕ → ℕ := fun n => MeasureTheory.SignedMeasure.findExistsOneDivLT s (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)<VAR>hn' : ∀ (n : ℕ), ¬restrict s (i \ ⋃ l, ⋃ (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤ restrict 0 (i \ ⋃ l, ⋃ (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<VAR>h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<VAR>h₂ : ↑s A ≤ ↑s i<VAR>h₃' : Summable fun n => 1 / (↑(bdd n) + 1)<VAR>h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop<VAR>h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop<VAR>A_meas : MeasurableSet A<VAR>E : Set α<VAR>hE₁ : MeasurableSet E<VAR>hE₂ : E ⊆ A<VAR>hE₃ : ↑0 E < ↑s E<VAR>k : ℕ<VAR>hk₁ : 1 ≤ bdd k<VAR>hk₂ : 1 / ↑(bdd k) < ↑s E<VAR>hA' : A ⊆ i \ ⋃ l, ⋃ (_ : l ≤ k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>hi : ↑s i < 0<VAR>hi₁ : MeasurableSet i<VAR>h : ¬restrict s i ≤ restrict 0 i<VAR>hn : ∀ (n : ℕ), ¬restrict s (i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤ restrict 0 (i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<VAR>A : Set α := i \ ⋃ l, MeasureTheory.SignedMeasure.restrictNonposSeq s i l<VAR>hA : A = i \ ⋃ l, MeasureTheory.SignedMeasure.restrictNonposSeq s i l<VAR>bdd : ℕ → ℕ := fun n => MeasureTheory.SignedMeasure.findExistsOneDivLT s (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)<VAR>hn' : ∀ (n : ℕ), ¬restrict s (i \ ⋃ l, ⋃ (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤ restrict 0 (i \ ⋃ l, ⋃ (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<VAR>h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<VAR>h₂ : ↑s A ≤ ↑s i<VAR>h₃' : Summable fun n => 1 / (↑(bdd n) + 1)<VAR>h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop<VAR>h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop<VAR>A_meas : MeasurableSet A<VAR>E : Set α<VAR>hE₁ : MeasurableSet E<VAR>hE₂ : E ⊆ A<VAR>hE₃ : ↑0 E < ↑s E<VAR>k : ℕ<VAR>hk₁ : 1 ≤ bdd k<VAR>hk₂ : 1 / ↑(bdd k) < ↑s E<VAR>hA' : A ⊆ i \ ⋃ l, ⋃ (_ : l ≤ k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l<GOAL>1 / (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT s (i \ ⋃ l, ⋃ (_ : l ≤ k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) - 1) + 1) < ↑s E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s : SignedMeasure α<VAR>i j : Set α<VAR>hi : ↑s i < 0<VAR>hi₁ : MeasurableSet i<VAR>h : ¬restrict s i ≤ restrict 0 i<VAR>hn : ∀ (n : ℕ), ¬restrict s (i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤ restrict 0 (i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<VAR>A : Set α := i \ ⋃ l, MeasureTheory.SignedMeasure.restrictNonposSeq s i l<VAR>hA : A = i \ ⋃ l, MeasureTheory.SignedMeasure.restrictNonposSeq s i l<VAR>bdd : ℕ → ℕ := fun n => MeasureTheory.SignedMeasure.findExistsOneDivLT s (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)<VAR>hn' : ∀ (n : ℕ), ¬restrict s (i \ ⋃ l, ⋃ (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤ restrict 0 (i \ ⋃ l, ⋃ (_ : l ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<VAR>h₁ : ↑s i = ↑s A + ∑' (l : ℕ), ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<VAR>h₂ : ↑s A ≤ ↑s i<VAR>h₃' : Summable fun n => 1 / (↑(bdd n) + 1)<VAR>h₃ : Tendsto (fun n => ↑(bdd n) + 1) atTop atTop<VAR>h₄ : Tendsto (fun n => ↑(bdd n)) atTop atTop<VAR>A_meas : MeasurableSet A<VAR>E : Set α<VAR>hE₁ : MeasurableSet E<VAR>hE₂ : E ⊆ A<VAR>hE₃ : ↑0 E < ↑s E<VAR>k : ℕ<VAR>hk₁ : 1 ≤ bdd k<VAR>hk₂ : 1 / ↑(bdd k) < ↑s E<VAR>hA' : A ⊆ i \ ⋃ l, ⋃ (_ : l ≤ k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l<GOAL>MeasureTheory.SignedMeasure.findExistsOneDivLT s (i \ ⋃ l, ⋃ (_ : l ≤ k), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) - 1 + 1 = bdd k
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>1 ≤ a⁻¹ ↔ a ≤ 1
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>a * 1 ≤ a * a⁻¹ ↔ a ≤ 1
<VAR>X : Scheme<VAR>U : X.Opens<GOAL>(Scheme.ΓSpecIso Γ(X, U)).hom = Scheme.Hom.app (Spec.map U.topIso.inv) ⊤ ≫ Scheme.Hom.app (ΓSpec.adjunction.unit.app ↑U) ⊤ ≫ U.topIso.hom
<VAR>X : Scheme<VAR>U : X.Opens<GOAL>(Scheme.ΓSpecIso Γ(X, U)).hom = Scheme.Hom.app (Spec.map U.topIso.inv) ⊤ ≫ (Scheme.ΓSpecIso Γ(↑U, ⊤)).hom ≫ U.topIso.hom
<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₀ a : ℝ<VAR>ha : a ≠ 0<GOAL>IsIntegralCurveAt γ v t₀ ↔ IsIntegralCurveAt (γ ∘ fun x => x * a) (a • v) (t₀ / a)
<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₀ a : ℝ<VAR>ha : a ≠ 0<VAR>hγ : IsIntegralCurveAt (γ ∘ fun x => x * a) (a • v) (t₀ / a)<GOAL>IsIntegralCurveAt γ v t₀
<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₀ a : ℝ<VAR>ha : a ≠ 0<VAR>hγ : IsIntegralCurveAt (γ ∘ fun x => x * a) (a • v) (t₀ / a)<GOAL>γ = (γ ∘ fun x => x * a) ∘ fun x => x * a⁻¹
<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₀ a : ℝ<VAR>ha : a ≠ 0<VAR>hγ : IsIntegralCurveAt (γ ∘ fun x => x * a) (a • v) (t₀ / a)<GOAL>v = a⁻¹ • a • v
<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₀ a : ℝ<VAR>ha : a ≠ 0<VAR>hγ : IsIntegralCurveAt (γ ∘ fun x => x * a) (a • v) (t₀ / a)<GOAL>t₀ = t₀ / a / a⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝¹ : CompleteLattice α<VAR>f✝ g s t : ι → α<VAR>a b : α<VAR>inst✝ : Unique ι<VAR>f : ι → α<GOAL>⨅ i, f i = f default
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Ring R<VAR>p : R[X]<GOAL>(-p).support.max = p.support.max
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u_4<VAR>h : IsEmpty ι<VAR>f : ι → Ordinal.{max u_5 u_4}<GOAL>lsub f = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u_4<VAR>h : IsEmpty ι<VAR>f : ι → Ordinal.{max u_5 u_4}<GOAL>∀ (i : ι), f i < 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDomain B<VAR>inst✝² : Algebra A B<VAR>K : Type u_6<VAR>inst✝¹ : Field K<VAR>inst✝ : Nontrivial R<VAR>x : S<VAR>hx : IsIntegral R x<VAR>f : R[X]<GOAL>(aeval x) f ∈ Submodule.span R (Set.range fun i => x ^ ↑i)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDomain B<VAR>inst✝² : Algebra A B<VAR>K : Type u_6<VAR>inst✝¹ : Field K<VAR>inst✝ : Nontrivial R<VAR>x : S<VAR>hx : IsIntegral R x<VAR>f : R[X]<GOAL>∃ f_1, f_1.degree < ↑(minpoly R x).natDegree ∧ (aeval x) f = (aeval x) f_1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDomain B<VAR>inst✝² : Algebra A B<VAR>K : Type u_6<VAR>inst✝¹ : Field K<VAR>inst✝ : Nontrivial R<VAR>x : S<VAR>hx : IsIntegral R x<VAR>f : R[X]<VAR>this : (minpoly R x).Monic<GOAL>∃ f_1, f_1.degree < ↑(minpoly R x).natDegree ∧ (aeval x) f = (aeval x) f_1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDomain B<VAR>inst✝² : Algebra A B<VAR>K : Type u_6<VAR>inst✝¹ : Field K<VAR>inst✝ : Nontrivial R<VAR>x : S<VAR>hx : IsIntegral R x<VAR>f : R[X]<VAR>this : (minpoly R x).Monic<GOAL>(aeval x) f = (aeval x) (f %ₘ minpoly R x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDomain B<VAR>inst✝² : Algebra A B<VAR>K : Type u_6<VAR>inst✝¹ : Field K<VAR>inst✝ : Nontrivial R<VAR>x : S<VAR>hx : IsIntegral R x<VAR>f : R[X]<VAR>this : (minpoly R x).Monic<GOAL>(aeval x) (f %ₘ minpoly R x + minpoly R x * (f /ₘ minpoly R x)) = (aeval x) (f %ₘ minpoly R x)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>s✝ : Finset ι<VAR>x✝ : (i : ↑↑s✝) → β ↑i<VAR>i✝ : ι<VAR>s : Finset ι<VAR>x y : (i : ↑↑s) → β ↑i<VAR>H : mk s x = mk s y<VAR>i : ι<VAR>hi : i ∈ s<VAR>h1 : (mk s x) ↑⟨i, hi⟩ = (mk s y) ↑⟨i, hi⟩<GOAL>x ⟨i, hi⟩ = y ⟨i, hi⟩
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>s✝ : Finset ι<VAR>x✝ : (i : ↑↑s✝) → β ↑i<VAR>i✝ : ι<VAR>s : Finset ι<VAR>x y : (i : ↑↑s) → β ↑i<VAR>H : mk s x = mk s y<VAR>i : ι<VAR>hi : i ∈ s<VAR>h1 : (if H : i ∈ s then x ⟨i, H⟩ else 0) = if H : i ∈ s then y ⟨i, H⟩ else 0<GOAL>x ⟨i, hi⟩ = y ⟨i, hi⟩
<VAR>α : Type u_1<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>γ✝ γ₁ γ₂ : Γ₀<VAR>l : Filter α<VAR>f : α → Γ₀<VAR>γ : Γ₀<VAR>h : γ ≠ 0<GOAL>Tendsto f l (𝓝 γ) ↔ ∀ᶠ (x : α) in l, f x = γ
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁹ : LinearOrderedField R<VAR>inst✝⁸ : LinearOrderedField R'<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : LinearOrderedAddCommGroup α<VAR>inst✝⁴ : Module R E<VAR>inst✝³ : Module R F<VAR>inst✝² : Module R α<VAR>inst✝¹ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t✝ : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>inst✝ : Fintype ι<VAR>f : ι → R<VAR>s t t₁ t₂ : Finset E<VAR>hs : AffineIndependent R Subtype.val<VAR>ht₁ : t₁ ⊆ s<VAR>ht₂ : t₂ ⊆ s<GOAL>(convexHull R) (↑t₁ ∩ ↑t₂) = (convexHull R) ↑t₁ ∩ (convexHull R) ↑t₂
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁹ : LinearOrderedField R<VAR>inst✝⁸ : LinearOrderedField R'<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : LinearOrderedAddCommGroup α<VAR>inst✝⁴ : Module R E<VAR>inst✝³ : Module R F<VAR>inst✝² : Module R α<VAR>inst✝¹ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t✝ : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>inst✝ : Fintype ι<VAR>f : ι → R<VAR>s t t₁ t₂ : Finset E<VAR>hs : AffineIndependent R Subtype.val<VAR>ht₁ : t₁ ⊆ s<VAR>ht₂ : t₂ ⊆ s<GOAL>(convexHull R) ↑t₁ ∩ (convexHull R) ↑t₂ ⊆ (convexHull R) (↑t₁ ⊓ ↑t₂)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁹ : LinearOrderedField R<VAR>inst✝⁸ : LinearOrderedField R'<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : LinearOrderedAddCommGroup α<VAR>inst✝⁴ : Module R E<VAR>inst✝³ : Module R F<VAR>inst✝² : Module R α<VAR>inst✝¹ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t✝ : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>inst✝ : Fintype ι<VAR>f : ι → R<VAR>s t t₁ t₂ : Finset E<VAR>hs : AffineIndependent R Subtype.val<VAR>ht₁ : t₁ ⊆ s<VAR>ht₂ : t₂ ⊆ s<GOAL>∀ (x : E), ((∃ w, (∀ y ∈ t₁, 0 ≤ w y) ∧ ∑ y ∈ t₁, w y = 1 ∧ ∑ y ∈ t₁, w y • y = x) ∧ ∃ w, (∀ y ∈ t₂, 0 ≤ w y) ∧ ∑ y ∈ t₂, w y = 1 ∧ ∑ y ∈ t₂, w y • y = x) → ∃ w, (∀ y ∈ t₁ ∩ t₂, 0 ≤ w y) ∧ ∑ y ∈ t₁ ∩ t₂, w y = 1 ∧ ∑ y ∈ t₁ ∩ t₂, w y • y = x
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁹ : LinearOrderedField R<VAR>inst✝⁸ : LinearOrderedField R'<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : LinearOrderedAddCommGroup α<VAR>inst✝⁴ : Module R E<VAR>inst✝³ : Module R F<VAR>inst✝² : Module R α<VAR>inst✝¹ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t✝ : Finset ι<VAR>w✝ : ι → R<VAR>z : ι → E<VAR>inst✝ : Fintype ι<VAR>f : ι → R<VAR>s t t₁ t₂ : Finset E<VAR>hs : AffineIndependent R Subtype.val<VAR>ht₁ : t₁ ⊆ s<VAR>ht₂ : t₂ ⊆ s<VAR>x : E<VAR>w₁ : E → R<VAR>h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y<VAR>h₂w₁ : ∑ y ∈ t₁, w₁ y = 1<VAR>h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x<VAR>w₂ : E → R<VAR>h₂w₂ : ∑ y ∈ t₂, w₂ y = 1<VAR>h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x<VAR>w : E → R := fun x => (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0<GOAL>∃ w, (∀ y ∈ t₁ ∩ t₂, 0 ≤ w y) ∧ ∑ y ∈ t₁ ∩ t₂, w y = 1 ∧ ∑ y ∈ t₁ ∩ t₂, w y • y = x
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁹ : LinearOrderedField R<VAR>inst✝⁸ : LinearOrderedField R'<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : LinearOrderedAddCommGroup α<VAR>inst✝⁴ : Module R E<VAR>inst✝³ : Module R F<VAR>inst✝² : Module R α<VAR>inst✝¹ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t✝ : Finset ι<VAR>w✝ : ι → R<VAR>z : ι → E<VAR>inst✝ : Fintype ι<VAR>f : ι → R<VAR>s t t₁ t₂ : Finset E<VAR>hs : AffineIndependent R Subtype.val<VAR>ht₁ : t₁ ⊆ s<VAR>ht₂ : t₂ ⊆ s<VAR>x : E<VAR>w₁ : E → R<VAR>h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y<VAR>h₂w₁ : ∑ y ∈ t₁, w₁ y = 1<VAR>h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x<VAR>w₂ : E → R<VAR>h₂w₂ : ∑ y ∈ t₂, w₂ y = 1<VAR>h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x<VAR>w : E → R := fun x => (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0<VAR>h₁w : ∑ i ∈ s, w i = 0<GOAL>∃ w, (∀ y ∈ t₁ ∩ t₂, 0 ≤ w y) ∧ ∑ y ∈ t₁ ∩ t₂, w y = 1 ∧ ∑ y ∈ t₁ ∩ t₂, w y • y = x
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁹ : LinearOrderedField R<VAR>inst✝⁸ : LinearOrderedField R'<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : LinearOrderedAddCommGroup α<VAR>inst✝⁴ : Module R E<VAR>inst✝³ : Module R F<VAR>inst✝² : Module R α<VAR>inst✝¹ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t✝ : Finset ι<VAR>w✝ : ι → R<VAR>z : ι → E<VAR>inst✝ : Fintype ι<VAR>f : ι → R<VAR>s t t₁ t₂ : Finset E<VAR>ht₁ : t₁ ⊆ s<VAR>ht₂ : t₂ ⊆ s<VAR>x : E<VAR>w₁ : E → R<VAR>h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y<VAR>h₂w₁ : ∑ y ∈ t₁, w₁ y = 1<VAR>h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x<VAR>w₂ : E → R<VAR>h₂w₂ : ∑ y ∈ t₂, w₂ y = 1<VAR>h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x<VAR>w : E → R := fun x => (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0<VAR>h₁w : ∑ i ∈ s, w i = 0<VAR>hs : ∀ x ∈ s, w x = 0<GOAL>∃ w, (∀ y ∈ t₁ ∩ t₂, 0 ≤ w y) ∧ ∑ y ∈ t₁ ∩ t₂, w y = 1 ∧ ∑ y ∈ t₁ ∩ t₂, w y • y = x
<VAR>x✝ y✝ x y : ℝ<GOAL>√x / x = 1 / √x
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<GOAL>Summable fun n => rexp (-↑n)
<VAR>M : Type u_1<VAR>inst✝ : NonAssocRing M<VAR>n : ℤ<VAR>x✝ : M<GOAL>↑n * x✝ = x✝ * ↑n
<VAR>M : Type u_1<VAR>inst✝ : NonAssocRing M<VAR>n✝ : ℤ<VAR>x✝¹ x✝ : M<VAR>n : ℕ<GOAL>↑↑n * (x✝¹ * x✝) = ↑↑n * x✝¹ * x✝
<VAR>M : Type u_1<VAR>inst✝ : NonAssocRing M<VAR>n✝ : ℤ<VAR>x✝¹ x✝ : M<VAR>n : ℕ<GOAL>↑(Int.negSucc n) * (x✝¹ * x✝) = ↑(Int.negSucc n) * x✝¹ * x✝
<VAR>M : Type u_1<VAR>inst✝ : NonAssocRing M<VAR>n✝ : ℤ<VAR>x✝¹ x✝ : M<VAR>n : ℕ<GOAL>x✝¹ * ↑↑n * x✝ = x✝¹ * (↑↑n * x✝)
<VAR>M : Type u_1<VAR>inst✝ : NonAssocRing M<VAR>n✝ : ℤ<VAR>x✝¹ x✝ : M<VAR>n : ℕ<GOAL>x✝¹ * ↑(Int.negSucc n) * x✝ = x✝¹ * (↑(Int.negSucc n) * x✝)
<VAR>M : Type u_1<VAR>inst✝ : NonAssocRing M<VAR>n✝ : ℤ<VAR>x✝¹ x✝ : M<VAR>n : ℕ<GOAL>x✝¹ * (-1 + -↑n) * x✝ = x✝¹ * ((-1 + -↑n) * x✝)
<VAR>M : Type u_1<VAR>inst✝ : NonAssocRing M<VAR>n✝ : ℤ<VAR>x✝¹ x✝ : M<VAR>n : ℕ<GOAL>x✝¹ * -1 * x✝ + x✝¹ * -↑n * x✝ = x✝¹ * -x✝ + x✝¹ * (-↑n * x✝)
<VAR>M : Type u_1<VAR>inst✝ : NonAssocRing M<VAR>n✝ : ℤ<VAR>x✝¹ x✝ : M<VAR>n : ℕ<GOAL>-(x✝¹ * x✝) + -(x✝¹ * ↑n * x✝) = x✝¹ * -x✝ + x✝¹ * -(↑n * x✝)
<VAR>M : Type u_1<VAR>inst✝ : NonAssocRing M<VAR>n✝ : ℤ<VAR>x✝¹ x✝ : M<VAR>n : ℕ<GOAL>-(x✝¹ * x✝) + -(x✝¹ * (↑n * x✝)) = x✝¹ * -x✝ + x✝¹ * -(↑n * x✝)
<VAR>M : Type u_1<VAR>inst✝ : NonAssocRing M<VAR>n✝ : ℤ<VAR>x✝¹ x✝ : M<VAR>n : ℕ<GOAL>x✝¹ * x✝ * ↑↑n = x✝¹ * (x✝ * ↑↑n)
<VAR>M : Type u_1<VAR>inst✝ : NonAssocRing M<VAR>n✝ : ℤ<VAR>x✝¹ x✝ : M<VAR>n : ℕ<GOAL>x✝¹ * x✝ * ↑(Int.negSucc n) = x✝¹ * (x✝ * ↑(Int.negSucc n))
<VAR>M : Type u_1<VAR>inst✝ : NonAssocRing M<VAR>n✝ : ℤ<VAR>x✝¹ x✝ : M<VAR>n : ℕ<GOAL>x✝¹ * x✝ * (-1 + -↑n) = x✝¹ * (x✝ * (-1 + -↑n))
<VAR>u : ℕ → ℕ<VAR>f : ℕ → ℝ≥0∞<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<GOAL>∑' (k : ℕ), f k ≤ f 0 + ∑' (k : ℕ), 2 ^ k * f (2 ^ k)
<VAR>u : ℕ → ℕ<VAR>f : ℕ → ℝ≥0∞<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<GOAL>⨆ i, ∑ a ∈ range (2 ^ i), f a ≤ f 0 + ∑' (k : ℕ), 2 ^ k * f (2 ^ k)
<VAR>u : ℕ → ℕ<VAR>f : ℕ → ℝ≥0∞<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>n : ℕ<GOAL>∑ k ∈ range n, 2 ^ k • f (2 ^ k) ≤ ∑' (k : ℕ), 2 ^ k * f (2 ^ k)
<VAR>u : ℕ → ℕ<VAR>f : ℕ → ℝ≥0∞<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>n : ℕ<GOAL>∑ x ∈ range n, 2 ^ x * f (2 ^ x) ≤ ∑' (k : ℕ), 2 ^ k * f (2 ^ k)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type w<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>ι : Type w<VAR>inst✝ : Projective R M<VAR>p : (ι →₀ R) →ₗ[R] M<VAR>hp : Surjective ⇑p<GOAL>Flat R M
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type w<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>ι : Type w<VAR>inst✝ : Projective R M<VAR>p : (ι →₀ R) →ₗ[R] M<VAR>hp : Surjective ⇑p<VAR>h : ∃ h, p ∘ₗ h = LinearMap.id<GOAL>Flat R M
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝² : Semiring R<VAR>r : R[X]<VAR>inst✝¹ : Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>inst✝ : Semiring T<VAR>p q : R[ℕ]<VAR>hf : ∀ (k : ℕ), Commute (f (q k)) x<GOAL>eval₂ f x ({ toFinsupp := p } * { toFinsupp := q }) = eval₂ f x { toFinsupp := p } * eval₂ f x { toFinsupp := q }
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝² : Semiring R<VAR>r : R[X]<VAR>inst✝¹ : Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>inst✝ : Semiring T<VAR>p q : R[ℕ]<VAR>hf : ∀ (k : ℕ), Commute (f (q k)) x<GOAL>(liftNC ↑f ⇑((powersHom S) x)) (p * q) = (liftNC ↑f ⇑((powersHom S) x)) p * (liftNC ↑f ⇑((powersHom S) x)) q
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>s✝ t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s : Set E<VAR>x : E<VAR>hx : x ∈ interior s<GOAL>x ∈ {x | gauge s x < 1}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>s✝ t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s : Set E<VAR>x : E<VAR>hx : x ∈ interior s<VAR>H₁ : Tendsto (fun r => r⁻¹ • x) (𝓝[<] 1) (𝓝 (1⁻¹ • x))<GOAL>x ∈ {x | gauge s x < 1}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>s✝ t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s : Set E<VAR>x : E<VAR>hx : x ∈ interior s<VAR>H₁ : Tendsto (fun r => r⁻¹ • x) (𝓝[<] 1) (𝓝 x)<GOAL>x ∈ {x | gauge s x < 1}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>s✝ t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s : Set E<VAR>x : E<VAR>hx : x ∈ interior s<VAR>H₁ : Tendsto (fun r => r⁻¹ • x) (𝓝[<] 1) (𝓝 x)<VAR>H₂ : ∀ᶠ (r : ℝ) in 𝓝[<] 1, x ∈ r • s ∧ 0 < r ∧ r < 1<GOAL>x ∈ {x | gauge s x < 1}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>s✝ t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s : Set E<VAR>x : E<VAR>hx : x ∈ interior s<VAR>H₁ : Tendsto (fun r => r⁻¹ • x) (𝓝[<] 1) (𝓝 x)<VAR>H₂ : ∀ᶠ (r : ℝ) in 𝓝[<] 1, x ∈ r • s ∧ 0 < r ∧ r < 1<VAR>r : ℝ<VAR>hxr : x ∈ r • s<VAR>hr₀ : 0 < r<VAR>hr₁ : r < 1<GOAL>x ∈ {x | gauge s x < 1}
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x✝ y : G<VAR>n m : ℕ<VAR>x : G<GOAL>IsPeriodicPt (fun x_1 => x * x_1) n 1 ↔ x ^ n = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x✝ y : G<VAR>n m : ℕ<VAR>x : G<GOAL>(fun x_1 => x ^ n * x_1) 1 = 1 ↔ x ^ n = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x✝ y : G<VAR>n m : ℕ<VAR>x : G<GOAL>x ^ n * 1 = 1 ↔ x ^ n = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : OrderTopology α<VAR>l : Filter β<VAR>f g : β → α<VAR>C : α<VAR>hf : Tendsto f l atBot<VAR>hg : Tendsto g l (𝓝 C)<GOAL>Tendsto (fun x => f x + g x) l atBot
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : OrderTopology α<VAR>l : Filter β<VAR>f g : β → α<VAR>C : α<VAR>hf : Tendsto f l atBot<VAR>hg : Tendsto g l (𝓝 C)<GOAL>Tendsto (fun x => g x + f x) l atBot
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>c : Cardinal.{u_3}<VAR>x : (Quotient.out c.ord).α<GOAL>(typein (fun x x_1 => x < x_1) x).card < c
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>c : Cardinal.{u_3}<VAR>x : (Quotient.out c.ord).α<GOAL>typein (fun x x_1 => x < x_1) x < c.ord