ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>s✝ : Set E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜 E<VAR>inst✝⁴ : Module ℝ E<VAR>inst✝³ : SMulCommClass ℝ 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : LocallyConvexSpace ℝ E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>s : Set E<VAR>hs : s ∈ 𝓝 0 ∧ Convex ℝ s<GOAL>Balanced 𝕜 ((convexHull ℝ) (balancedCore 𝕜 s)) ∧ Convex ℝ ((convexHull ℝ) (balancedCore 𝕜 s))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>s✝ : Set E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜 E<VAR>inst✝⁴ : Module ℝ E<VAR>inst✝³ : SMulCommClass ℝ 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : LocallyConvexSpace ℝ E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>s : Set E<VAR>hs : s ∈ 𝓝 0 ∧ Convex ℝ s<GOAL>Convex ℝ ((convexHull ℝ) (balancedCore 𝕜 s))
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I✝ J : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>I : Box ι<VAR>π : Prepartition I<VAR>s : Finset (ι × ℝ)<GOAL>π ⊓ splitMany I s = π.biUnion fun J => splitMany J s
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I✝ J : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>I : Box ι<VAR>π : Prepartition I<GOAL>π ⊓ splitMany I ∅ = π.biUnion fun J => splitMany J ∅
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I✝ J : Box ι<VAR>i : ι<VAR>x : ℝ<VAR>I : Box ι<VAR>π : Prepartition I<VAR>p : ι × ℝ<VAR>s : Finset (ι × ℝ)<VAR>a✝ : p ∉ s<VAR>ihp : π ⊓ splitMany I s = π.biUnion fun J => splitMany J s<GOAL>π ⊓ splitMany I (insert p s) = π.biUnion fun J => splitMany J (insert p s)
<VAR>α : Type u_1<VAR>r : ℕ → ℕ → Prop<VAR>n : ℕ<GOAL>Chain r ↑(range n.succ) ↔ r n 0 ∧ ∀ m < n, r m m.succ
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n✝ : ℕ∞<VAR>n : ℕ<GOAL>ContMDiffAt I I' (↑n) f x ↔ ∃ u ∈ 𝓝 x, ContMDiffOn I I' (↑n) f u
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>e : F ≃L[𝕜] G<GOAL>ContDiffOn 𝕜 n (⇑e ∘ f) s ↔ ContDiffOn 𝕜 n f s
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>↑p ∈ nonunits ℤ_[p]
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>this : (↑p)⁻¹ < 1<GOAL>↑p ∈ nonunits ℤ_[p]
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : Semiring R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>f : R[X]<VAR>hf : IsUnit f.leadingCoeff<VAR>H : IsUnit (map φ f)<GOAL>IsUnit f
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : Semiring R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>f : R[X]<VAR>hf : IsUnit f.leadingCoeff<VAR>H : IsUnit (map φ f)<VAR>dz : (map φ f).degree = 0<GOAL>IsUnit f
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : Semiring R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>f : R[X]<VAR>hf : IsUnit f.leadingCoeff<VAR>H : IsUnit (map φ f)<VAR>dz : f.degree = 0<GOAL>IsUnit f
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : Semiring R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>f : R[X]<VAR>hf : IsUnit f.leadingCoeff<VAR>H : IsUnit (map φ f)<VAR>dz : (map φ f).degree = 0<GOAL>φ f.leadingCoeff ≠ 0
<VAR>c : Cardinal.{u}<GOAL>lift.{v, u} c < 𝔠 ↔ c < 𝔠
<VAR>x : ℝ<VAR>hl : -π ≤ x<VAR>hr : x ≤ π<GOAL>cos (x / 2) = √((1 + cos x) / 2)
<VAR>x : ℝ<VAR>hl : -π ≤ x<VAR>hr : x ≤ π<VAR>this : 0 ≤ cos (x / 2)<GOAL>cos (x / 2) = √((1 + cos x) / 2)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : OrderedRing 𝕜<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : Module 𝕜 E<VAR>l✝ : E →L[𝕜] 𝕜<VAR>A B : Set E<VAR>X : Finset E<VAR>x : E<VAR>hBA : B ⊆ A<VAR>w : E<VAR>l : E →L[𝕜] 𝕜<VAR>hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}<VAR>hCB : {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} ⊆ B<VAR>hw : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}<GOAL>∃ l_1, {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} = {x | x ∈ B ∧ ∀ y ∈ B, l_1 y ≤ l_1 x}
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsSplitMono f<GOAL>IsZero X ↔ f = 0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsSplitMono f<GOAL>𝟙 X = 0 ↔ f = 0
<VAR>b u w v : Ordinal.{u_1}<VAR>hw : w < b ^ u<GOAL>b ^ u * v + w < b ^ u * succ v
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>s : AffineSubspace ℝ P<VAR>p₁ p₂ p₃ p₄ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃p₄ : s.SOppSide p₃ p₄<GOAL>(∡ p₁ p₄ p₂).sign = -(∡ p₁ p₃ p₂).sign
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>s : AffineSubspace ℝ P<VAR>p₁ p₂ p₃ p₄ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃p₄ : s.SOppSide p₃ p₄<VAR>hp₁p₃ : p₁ ≠ p₃<GOAL>(∡ p₁ p₄ p₂).sign = -(∡ p₁ p₃ p₂).sign
<VAR>S : Type u<VAR>inst✝ : Semiring S<VAR>n : ℕ<GOAL>(ascPochhammer S (n + 1)).comp (X + 1) = ascPochhammer S (n + 1) + (n + 1) • (ascPochhammer S n).comp (X + 1)
<VAR>S : Type u<VAR>inst✝ : Semiring S<VAR>n : ℕ<GOAL>(ascPochhammer ℕ (n + 1)).comp (X + 1) = ascPochhammer ℕ (n + 1) + (↑n + 1) * (ascPochhammer ℕ n).comp (X + 1)
<VAR>S : Type u<VAR>inst✝ : Semiring S<VAR>n : ℕ<GOAL>(ascPochhammer ℕ (n + 1)).comp (X + 1) = X * (ascPochhammer ℕ n).comp (X + 1) + (↑n + 1) * (ascPochhammer ℕ n).comp (X + 1)
<VAR>S : Type u<VAR>inst✝ : Semiring S<VAR>n : ℕ<GOAL>(↑n + X + 1) * (ascPochhammer ℕ n).comp (X + 1) = (X + (↑n + 1)) * (ascPochhammer ℕ n).comp (X + 1)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝ : LinearOrderedField 𝕜<VAR>x y z : 𝕜<VAR>h : x < y<GOAL>z ∈ Ioo x y ↔ ∃ a b, 0 < a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivisionMonoid α<VAR>a✝ b c d a : α<VAR>m n : ℕ<GOAL>a ^ (↑m * ↑n) = (a ^ ↑m) ^ ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivisionMonoid α<VAR>a✝ b c d a : α<VAR>m n : ℕ<GOAL>a ^ (↑m * ↑n) = a ^ ↑(m * n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivisionMonoid α<VAR>a✝ b c d a : α<VAR>m n : ℕ<GOAL>a ^ (↑m * Int.negSucc n) = (a ^ ↑m) ^ Int.negSucc n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivisionMonoid α<VAR>a✝ b c d a : α<VAR>m n : ℕ<GOAL>a ^ (Int.negSucc m * ↑n) = (a ^ Int.negSucc m) ^ ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivisionMonoid α<VAR>a✝ b c d a : α<VAR>m n : ℕ<GOAL>a ^ (Int.negSucc m * Int.negSucc n) = (a ^ Int.negSucc m) ^ Int.negSucc n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivisionMonoid α<VAR>a✝ b c d a : α<VAR>m n : ℕ<GOAL>a ^ (↑m.succ * ↑n.succ) = a ^ ↑((m + 1) * (n + 1))
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Fintype K<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Fintype σ<VAR>inst✝² : DecidableEq σ<VAR>inst✝¹ : DecidableEq K<VAR>p : ℕ<VAR>inst✝ : CharP K p<VAR>f : MvPolynomial σ K<VAR>h : f.totalDegree < Fintype.card σ<VAR>F : Unit → MvPolynomial σ K := fun x => f<VAR>this : ∑ i : Unit, (F i).totalDegree < Fintype.card σ<GOAL>p ∣ Fintype.card { x // (eval x) f = 0 }
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Fintype K<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Fintype σ<VAR>inst✝² : DecidableEq σ<VAR>inst✝¹ : DecidableEq K<VAR>p : ℕ<VAR>inst✝ : CharP K p<VAR>f : MvPolynomial σ K<VAR>h : f.totalDegree < Fintype.card σ<VAR>F : Unit → MvPolynomial σ K := fun x => f<VAR>this : ∑ i : Unit, (F i).totalDegree < Fintype.card σ<VAR>x✝ : σ → K<GOAL>(eval x✝) f = 0 ↔ ∀ i ∈ univ, (eval x✝) (F i) = 0
<VAR>C : Type u_1<VAR>C' : Type ?u.14347<VAR>D : Type u_6<VAR>D' : Type ?u.14353<VAR>H : Type u_3<VAR>H' : Type ?u.14359<VAR>inst✝⁶ : Category.{u_4, u_1} C<VAR>inst✝⁵ : Category.{?u.14367, ?u.14347} C'<VAR>inst✝⁴ : Category.{u_5, u_6} D<VAR>inst✝³ : Category.{?u.14375, ?u.14353} D'<VAR>inst✝² : Category.{u_2, u_3} H<VAR>inst✝¹ : Category.{?u.14383, ?u.14359} H'<VAR>RF RF' RF'' : D ⥤ H<VAR>F F' F'' : C ⥤ H<VAR>e✝ : F ≅ F'<VAR>L : C ⥤ D<VAR>α : F ⟶ L ⋙ RF<VAR>α'✝ : F' ⟶ L ⋙ RF'<VAR>α'' : F'' ⟶ L ⋙ RF''<VAR>α'₂ : F ⟶ L ⋙ RF'<VAR>W✝ : MorphismProperty C<VAR>α' : F ⟶ L ⋙ RF'<VAR>W : MorphismProperty C<VAR>inst✝ : L.IsLocalization W<VAR>e : RF ≅ RF'<VAR>comm : α ≫ whiskerLeft L e.hom = α'<GOAL>RF.IsRightDerivedFunctor α W ↔ RF'.IsRightDerivedFunctor α' W
<VAR>C : Type u_1<VAR>C' : Type ?u.14347<VAR>D : Type u_6<VAR>D' : Type ?u.14353<VAR>H : Type u_3<VAR>H' : Type ?u.14359<VAR>inst✝⁶ : Category.{u_4, u_1} C<VAR>inst✝⁵ : Category.{?u.14367, ?u.14347} C'<VAR>inst✝⁴ : Category.{u_5, u_6} D<VAR>inst✝³ : Category.{?u.14375, ?u.14353} D'<VAR>inst✝² : Category.{u_2, u_3} H<VAR>inst✝¹ : Category.{?u.14383, ?u.14359} H'<VAR>RF RF' RF'' : D ⥤ H<VAR>F F' F'' : C ⥤ H<VAR>e✝ : F ≅ F'<VAR>L : C ⥤ D<VAR>α : F ⟶ L ⋙ RF<VAR>α'✝ : F' ⟶ L ⋙ RF'<VAR>α'' : F'' ⟶ L ⋙ RF''<VAR>α'₂ : F ⟶ L ⋙ RF'<VAR>W✝ : MorphismProperty C<VAR>α' : F ⟶ L ⋙ RF'<VAR>W : MorphismProperty C<VAR>inst✝ : L.IsLocalization W<VAR>e : RF ≅ RF'<VAR>comm : α ≫ whiskerLeft L e.hom = α'<GOAL>RF.IsLeftKanExtension α ↔ RF'.IsLeftKanExtension α'
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : Nontrivial α<GOAL>Disjoint atBot atTop
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : Nontrivial α<VAR>x y : α<VAR>hne : x ≠ y<GOAL>Disjoint atBot atTop
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝¹ : Field F<VAR>W : Jacobian F<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>P Q : Fin 3 → R<GOAL>dblY (map W' f) (⇑f ∘ P) = f (W'.dblY P)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>n : ℕ<GOAL>finRotate (2 * n + 1) ∈ alternatingGroup (Fin (2 * n + 1))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s : Finset ι<VAR>H : s.Nonempty<VAR>f✝ : ι → α<VAR>a : α<VAR>f : ι → α<GOAL>∃ i ∈ s, s.sup' H f = f i
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>hst : AEDisjoint μ s t<VAR>ht : NullMeasurableSet t μ<VAR>hfs : IntegrableOn f s μ<VAR>hft : IntegrableOn f t μ<GOAL>∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ + ∫ (x : X) in t, f x ∂μ
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hcf : ContinuousOn f (Ioc a b)<VAR>hcg : ContinuousOn g (Ioc a b)<VAR>hg' : ∀ x ∈ Ioo a b, g' x ≠ 0<VAR>hfb : f b = 0<VAR>hgb : g b = 0<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] b) l<GOAL>Tendsto (fun x => f x / g x) (𝓝[<] b) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hcf : ContinuousOn f (Ioc a b)<VAR>hcg : ContinuousOn g (Ioc a b)<VAR>hg' : ∀ x ∈ Ioo a b, g' x ≠ 0<VAR>hfb : f b = 0<VAR>hgb : g b = 0<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] b) l<GOAL>Tendsto f (𝓝[<] b) (𝓝 0)
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hcf : ContinuousOn f (Ioc a b)<VAR>hcg : ContinuousOn g (Ioc a b)<VAR>hg' : ∀ x ∈ Ioo a b, g' x ≠ 0<VAR>hfb : f b = 0<VAR>hgb : g b = 0<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] b) l<GOAL>Tendsto g (𝓝[<] b) (𝓝 0)
<VAR>K : Type u_1<VAR>inst✝ : LinearOrderedField K<VAR>f : ℤ[X]<VAR>a b : ℤ<VAR>b0 : 0 < b<VAR>fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0<GOAL>1 ≤ ↑b ^ f.natDegree * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|
<VAR>K : Type u_1<VAR>inst✝ : LinearOrderedField K<VAR>f : ℤ[X]<VAR>a b : ℤ<VAR>b0 : 0 < b<VAR>fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0<VAR>ev : ℤ<VAR>bi : K<VAR>bu : bi * (algebraMap ℤ K) b = 1<VAR>hF : (algebraMap ℤ K) ev = (algebraMap ℤ K) b ^ f.natDegree * eval ((algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)<GOAL>1 ≤ ↑b ^ f.natDegree * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|
<VAR>K : Type u_1<VAR>inst✝ : LinearOrderedField K<VAR>f : ℤ[X]<VAR>a b : ℤ<VAR>b0 : 0 < b<VAR>fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0<VAR>ev : ℤ<VAR>bi : K<VAR>bu : bi * (algebraMap ℤ K) b = 1<VAR>hF : (algebraMap ℤ K) ev = (algebraMap ℤ K) b ^ f.natDegree * eval ((algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)<VAR>Fa : |(algebraMap ℤ K) ev| = |(algebraMap ℤ K) b ^ f.natDegree * eval ((algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)|<GOAL>1 ≤ ↑b ^ f.natDegree * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|
<VAR>K : Type u_1<VAR>inst✝ : LinearOrderedField K<VAR>f : ℤ[X]<VAR>a b : ℤ<VAR>b0 : 0 < b<VAR>fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0<VAR>ev : ℤ<VAR>bi : K<VAR>bu : bi * (algebraMap ℤ K) b = 1<VAR>hF : (algebraMap ℤ K) ev = (algebraMap ℤ K) b ^ f.natDegree * eval ((algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)<VAR>Fa : |↑ev| = |↑b ^ f.natDegree| * |eval ((algebraMap ℤ K) a * (1 / ↑b)) (Polynomial.map (algebraMap ℤ K) f)|<GOAL>1 ≤ ↑b ^ f.natDegree * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|
<VAR>K : Type u_1<VAR>inst✝ : LinearOrderedField K<VAR>f : ℤ[X]<VAR>a b : ℤ<VAR>b0 : 0 < b<VAR>fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0<VAR>ev : ℤ<VAR>bi : K<VAR>bu : bi * (algebraMap ℤ K) b = 1<VAR>hF : (algebraMap ℤ K) ev = (algebraMap ℤ K) b ^ f.natDegree * eval ((algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)<VAR>Fa : |↑ev| = ↑b ^ f.natDegree * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|<GOAL>1 ≤ ↑b ^ f.natDegree * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|
<VAR>K : Type u_1<VAR>inst✝ : LinearOrderedField K<VAR>f : ℤ[X]<VAR>a b : ℤ<VAR>b0 : 0 < b<VAR>fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0<VAR>ev : ℤ<VAR>bi : K<VAR>bu : bi * (algebraMap ℤ K) b = 1<VAR>hF : (algebraMap ℤ K) ev = (algebraMap ℤ K) b ^ f.natDegree * eval ((algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)<VAR>Fa : |↑ev| = ↑b ^ f.natDegree * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|<GOAL>1 ≤ |ev|
<VAR>K : Type u_1<VAR>inst✝ : LinearOrderedField K<VAR>f : ℤ[X]<VAR>a b : ℤ<VAR>b0 : 0 < b<VAR>fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0<VAR>ev : ℤ<VAR>bi : K<VAR>bu : bi * (algebraMap ℤ K) b = 1<VAR>hF : (algebraMap ℤ K) ev = (algebraMap ℤ K) b ^ f.natDegree * eval ((algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)<VAR>Fa : |↑ev| = ↑b ^ f.natDegree * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|<VAR>F0 : ev = 0<GOAL>eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) = 0
<VAR>K : Type u_1<VAR>inst✝ : LinearOrderedField K<VAR>f : ℤ[X]<VAR>a b : ℤ<VAR>b0 : 0 < b<VAR>fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0<VAR>ev : ℤ<VAR>bi : K<VAR>bu : bi * (algebraMap ℤ K) b = 1<VAR>hF : (algebraMap ℤ K) b ^ f.natDegree = 0 ∨ eval ((algebraMap ℤ K) a * ((algebraMap ℤ K) b)⁻¹) (Polynomial.map (algebraMap ℤ K) f) = 0<VAR>Fa : |↑ev| = ↑b ^ f.natDegree * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|<VAR>F0 : ev = 0<GOAL>eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) = 0
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝² : DecidableRel r<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : IsRefl α r<VAR>x : α<VAR>xs : List α<GOAL>(orderedInsert r x xs).erase x = xs
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝² : DecidableRel r<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : IsRefl α r<VAR>x : α<VAR>xs : List α<GOAL>x ∉ takeWhile (fun b => decide ¬r x b) xs
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝² : DecidableRel r<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : IsRefl α r<VAR>x : α<VAR>xs : List α<VAR>h : x ∈ takeWhile (fun b => decide ¬r x b) xs<GOAL>False
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝² : DecidableRel r<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : IsRefl α r<VAR>x : α<VAR>xs : List α<VAR>h : (decide ¬r x x) = true<GOAL>False
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>α : K<GOAL>house α = ↑(univ.sup' ⋯ fun φ => ‖φ α‖₊)
<VAR>R : Type u_1<VAR>a b : R<VAR>inst✝ : Monoid R<VAR>n : ℕ<VAR>n0 : 0 < n<GOAL>IsRightRegular (a ^ n) ↔ IsRightRegular a
<VAR>R : Type u_1<VAR>a b : R<VAR>inst✝ : Monoid R<VAR>n : ℕ<VAR>n0 : 0 < n<GOAL>IsRightRegular (a ^ n) → IsRightRegular a
<VAR>R : Type u_1<VAR>a b : R<VAR>inst✝ : Monoid R<VAR>n : ℕ<VAR>n0 : 0 < n<GOAL>IsRightRegular (a * a ^ n.pred) → IsRightRegular a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Lattice α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>h : a ≤ b<GOAL>[[a, b]] = Icc a b
<VAR>α : Type u_1<VAR>inst✝⁵ : AddCommSemigroup α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>hab : b ≤ a<VAR>hcb : c ≤ b<GOAL>a - b + (b - c) = a - c
<VAR>α : Type u_1<VAR>inst✝⁵ : AddCommSemigroup α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>hab : b ≤ a<VAR>hcb : c ≤ b<GOAL>a - b = a - c - (b - c)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>m : M<GOAL>e0 Q * (v Q) m * e0 Q = (v Q) m
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : CategoryWithHomology C<VAR>inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization<VAR>K L : HomologicalComplex C c<VAR>f : K ⟶ L<GOAL>quasiIso C c ((quotient C c).map f) ↔ HomologicalComplex.quasiIso C c f
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : CategoryWithHomology C<VAR>inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization<VAR>K L : HomologicalComplex C c<VAR>f : K ⟶ L<VAR>eq : ∀ (i : ι), IsIso ((quotient C c ⋙ homologyFunctor C c i).map f) ↔ IsIso ((HomologicalComplex.homologyFunctor C c i).map f)<GOAL>quasiIso C c ((quotient C c).map f) ↔ HomologicalComplex.quasiIso C c f
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : CategoryWithHomology C<VAR>inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization<VAR>K L : HomologicalComplex C c<VAR>f : K ⟶ L<VAR>eq : ∀ (i : ι), IsIso ((homologyFunctor C c i).map ((quotient C c).map f)) ↔ IsIso (HomologicalComplex.homologyMap f i)<GOAL>quasiIso C c ((quotient C c).map f) ↔ HomologicalComplex.quasiIso C c f
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>b c d : R<VAR>m : ℕ<GOAL>preNormEDS' b c d (2 * (m + 2) + 1) = (preNormEDS' b c d (m + 4) * preNormEDS' b c d (m + 2) ^ 3 * if Even m then b else 1) - preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) ^ 3 * if Even m then 1 else b
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>b c d : R<VAR>m : ℕ<GOAL>((preNormEDS' b c d (2 * m / 2 + 4) * preNormEDS' b c d (2 * m / 2 + 2) ^ 3 * if Even (2 * m / 2) then b else 1) - preNormEDS' b c d (2 * m / 2 + 1) * preNormEDS' b c d (2 * m / 2 + 3) ^ 3 * if Even (2 * m / 2) then 1 else b) = (preNormEDS' b c d (m + 4) * preNormEDS' b c d (m + 2) ^ 3 * if Even m then b else 1) - preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) ^ 3 * if Even m then 1 else b
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(MaxProducts C ho)<VAR>q : Products I<VAR>hq : q < (↑l).Tail<VAR>this : Inhabited I<GOAL>List.Chain' (fun x x_1 => x > x_1) (term I ho :: ↑q)
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(MaxProducts C ho)<VAR>q : Products I<VAR>hq : q < (↑l).Tail<VAR>this : Inhabited I<GOAL>List.Pairwise (fun x x_1 => x > x_1) (term I ho :: ↑q)
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(MaxProducts C ho)<VAR>q : Products I<VAR>hq : q < (↑l).Tail<VAR>this : Inhabited I<GOAL>(∀ a' ∈ ↑q, a' < term I ho) ∧ List.Pairwise (fun x x_1 => x_1 < x) ↑q
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(MaxProducts C ho)<VAR>q : Products I<VAR>hq : q < (↑l).Tail<VAR>this : Inhabited I<VAR>a : I<VAR>ha : a ∈ ↑q<GOAL>(↑q).head! < term I ho