ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g✝ : E → G<VAR>C : ℝ<VAR>s : Set E<VAR>x y : E<VAR>f' g' : E → E →L[𝕜] G<VAR>φ : E →L[𝕜] G<VAR>hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>bound : ∀ x ∈ s, ‖f' x‖ ≤ C<VAR>hs : Convex ℝ s<VAR>xs : x ∈ s<VAR>ys : y ∈ s<VAR>this : NormedSpace ℝ G := RestrictScalars.normedSpace ℝ 𝕜 G<VAR>g : ℝ → E := ⇑(AffineMap.lineMap x y)<VAR>segm : MapsTo g (Icc 0 1) s<VAR>hD : ∀ t ∈ Icc 0 1, HasDerivWithinAt (f ∘ g) ((f' (g t)) (y - x)) (Icc 0 1) t<GOAL>‖f y - f x‖ ≤ C * ‖y - x‖
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g✝ : E → G<VAR>C : ℝ<VAR>s : Set E<VAR>x y : E<VAR>f' g' : E → E →L[𝕜] G<VAR>φ : E →L[𝕜] G<VAR>hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>bound✝ : ∀ x ∈ s, ‖f' x‖ ≤ C<VAR>hs : Convex ℝ s<VAR>xs : x ∈ s<VAR>ys : y ∈ s<VAR>this : NormedSpace ℝ G := RestrictScalars.normedSpace ℝ 𝕜 G<VAR>g : ℝ → E := ⇑(AffineMap.lineMap x y)<VAR>segm : MapsTo g (Icc 0 1) s<VAR>hD : ∀ t ∈ Icc 0 1, HasDerivWithinAt (f ∘ g) ((f' (g t)) (y - x)) (Icc 0 1) t<VAR>bound : ∀ t ∈ Ico 0 1, ‖(f' (g t)) (y - x)‖ ≤ C * ‖y - x‖<GOAL>‖f y - f x‖ ≤ C * ‖y - x‖
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hf : ClosedEmbedding f<VAR>s : Set Y<VAR>hs : s ⊆ range f<GOAL>IsClosed s ↔ IsClosed (f ⁻¹' s)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℤ<GOAL>‖↑p ^ n‖ = ↑p ^ (-n)
<VAR>α : Type u_2<VAR>β : Type u_1<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>l₁.product l₂ = l₁.productTR l₂
<VAR>α : Type u_2<VAR>β : Type u_1<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>(l₁.bind fun a => map (Prod.mk a) l₂) = (foldl (fun acc a => foldl (fun acc b => acc.push (a, b)) acc l₂) #[] l₁).data
<VAR>α : Type u_2<VAR>β : Type u_1<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>(l₁.bind fun a => map (Prod.mk a) l₂) = #[].data ++ l₁.bind ?h.h.h.h.G
<VAR>α : Type u_2<VAR>β : Type u_1<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>α → List (α × β)
<VAR>α : Type u_2<VAR>β : Type u_1<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>∀ (acc : Array (α × β)) (a : α), (foldl (fun acc b => acc.push (a, b)) acc l₂).data = acc.data ++ ?h.h.h.h.G a
<VAR>α : Type u_2<VAR>β : Type u_1<VAR>l₁ : List α<VAR>l₂ : List β<VAR>acc✝ : Array (α × β)<VAR>a✝ : α<GOAL>(foldl (fun acc b => acc.push (a✝, b)) acc✝ l₂).data = acc✝.data ++ map (Prod.mk a✝) l₂
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>W : Submodule R M<GOAL>⊤.dualAnnihilator = ⊥
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>W : Submodule R M<GOAL>⊤.dualAnnihilator ≤ ⊥
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>W : Submodule R M<VAR>v : Module.Dual R M<GOAL>v ∈ ⊤.dualAnnihilator → v ∈ ⊥
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>W : Submodule R M<VAR>v : Module.Dual R M<GOAL>(∀ (w : M), v w = 0) → v = 0
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>m : ℝ≥0∞ → ℝ≥0∞<GOAL>(mkMetric m).trim = mkMetric m
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>m : ℝ≥0∞ → ℝ≥0∞<GOAL>⨆ i, (mkMetric'.pre (fun s => m (diam s)) (↑i)⁻¹).trim = ⨆ n, mkMetric'.pre (fun s => m (diam s)) (↑n)⁻¹
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>n : ℕ<GOAL>(mkMetric'.pre (fun s => m (diam s)) (↑n)⁻¹).trim = mkMetric'.pre (fun s => m (diam s)) (↑n)⁻¹
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>n : ℕ<VAR>s : Set X<GOAL>m (diam (closure s)) = m (diam s)
<VAR>α : Type u_1<VAR>m n : ℕ<VAR>f : Vector3 α 0 → Prop<VAR>x✝ : Exists f<VAR>v : Vector3 α 0<VAR>fv : f v<GOAL>f []
<VAR>α : Type u_1<VAR>m n : ℕ<VAR>f : Vector3 α 0 → Prop<VAR>x✝ : Exists f<VAR>v : Vector3 α 0<VAR>fv : f v<GOAL>f v
<VAR>C : Type u_1<VAR>inst✝² : Category.{v, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteBiproducts C<VAR>n : ℕ<VAR>F : Fin n → Karoubi C<GOAL>HasBiproduct F
<VAR>C : Type u_1<VAR>inst✝² : Category.{v, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteBiproducts C<VAR>n : ℕ<VAR>F : Fin n → Karoubi C<GOAL>∑ j : Fin n, (Biproducts.bicone F).π j ≫ (Biproducts.bicone F).ι j = 𝟙 (Biproducts.bicone F).pt
<VAR>C : Type u_1<VAR>inst✝² : Category.{v, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteBiproducts C<VAR>n : ℕ<VAR>F : Fin n → Karoubi C<GOAL>(∑ j : Fin n, (Biproducts.bicone F).π j ≫ (Biproducts.bicone F).ι j).f = (𝟙 (Biproducts.bicone F).pt).f
<VAR>C : Type u_1<VAR>inst✝² : Category.{v, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteBiproducts C<VAR>n : ℕ<VAR>F : Fin n → Karoubi C<VAR>j : Fin n<GOAL>biproduct.ι (fun j => (F j).X) j ≫ (∑ j : Fin n, (Biproducts.bicone F).π j ≫ (Biproducts.bicone F).ι j).f = biproduct.ι (fun j => (F j).X) j ≫ (𝟙 (Biproducts.bicone F).pt).f
<VAR>C : Type u_1<VAR>inst✝² : Category.{v, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteBiproducts C<VAR>n : ℕ<VAR>F : Fin n → Karoubi C<VAR>j : Fin n<GOAL>∑ j_1 : Fin n, biproduct.ι (fun j => (F j).X) j ≫ biproduct.π (fun j => (F j).X) j_1 ≫ (F j_1).p ≫ biproduct.ι (fun j => (F j).X) j_1 = (F j).p ≫ biproduct.ι (fun j => (F j).X) j
<VAR>C : Type u_1<VAR>inst✝² : Category.{v, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteBiproducts C<VAR>n : ℕ<VAR>F : Fin n → Karoubi C<VAR>j : Fin n<GOAL>biproduct.ι (fun j => (F j).X) j ≫ biproduct.π (fun j => (F j).X) j ≫ (F j).p ≫ biproduct.ι (fun j => (F j).X) j = (F j).p ≫ biproduct.ι (fun j => (F j).X) j
<VAR>C : Type u_1<VAR>inst✝² : Category.{v, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteBiproducts C<VAR>n : ℕ<VAR>F : Fin n → Karoubi C<VAR>j : Fin n<GOAL>∀ b ∈ Finset.univ, b ≠ j → biproduct.ι (fun j => (F j).X) j ≫ biproduct.π (fun j => (F j).X) b ≫ (F b).p ≫ biproduct.ι (fun j => (F j).X) b = 0
<VAR>C : Type u_1<VAR>inst✝² : Category.{v, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteBiproducts C<VAR>n : ℕ<VAR>F : Fin n → Karoubi C<VAR>j : Fin n<GOAL>j ∉ Finset.univ → biproduct.ι (fun j => (F j).X) j ≫ biproduct.π (fun j => (F j).X) j ≫ (F j).p ≫ biproduct.ι (fun j => (F j).X) j = 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁸ : Semiring α<VAR>inst✝⁷ : LinearOrder α<VAR>a b c d : α<VAR>inst✝⁶ : IsRightCancelAdd α<VAR>inst✝⁵ : NoZeroDivisors α<VAR>inst✝⁴ : ZeroLEOneClass α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : PosMulMono α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<GOAL>a * a + b * b = 0 ↔ a = 0 ∧ b = 0
<VAR>x : ℝ<VAR>hx : x ∈ Ioo (-(π / 2)) (π / 2)<VAR>y : ℝ<VAR>hy : y ∈ Ioo (-(π / 2)) (π / 2)<VAR>hlt : x < y<GOAL>tan x < tan y
<VAR>x : ℝ<VAR>hx : x ∈ Ioo (-(π / 2)) (π / 2)<VAR>y : ℝ<VAR>hy : y ∈ Ioo (-(π / 2)) (π / 2)<VAR>hlt : x < y<GOAL>0 < sin (y - x)
<VAR>s : ℂ<GOAL>completedRiemannZeta (1 - s) = completedRiemannZeta s
<VAR>X✝¹ : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝³ : TopologicalSpace X✝¹<VAR>inst✝² : TopologicalSpace Y<VAR>s t : Set X✝¹<VAR>X✝ : ι → Type u_2<VAR>inst✝¹ : (i : ι) → TopologicalSpace (X✝ i)<VAR>X : ι → Type u_3<VAR>inst✝ : (d : ι) → TopologicalSpace (X d)<GOAL>(Filter.coprodᵢ fun d => cocompact (X d)) = cocompact ((d : ι) → X d)
<VAR>X✝¹ : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝³ : TopologicalSpace X✝¹<VAR>inst✝² : TopologicalSpace Y<VAR>s t : Set X✝¹<VAR>X✝ : ι → Type u_2<VAR>inst✝¹ : (i : ι) → TopologicalSpace (X✝ i)<VAR>X : ι → Type u_3<VAR>inst✝ : (d : ι) → TopologicalSpace (X d)<GOAL>cocompact ((d : ι) → X d) ≤ Filter.coprodᵢ fun d => cocompact (X d)
<VAR>X✝¹ : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝³ : TopologicalSpace X✝¹<VAR>inst✝² : TopologicalSpace Y<VAR>s✝ t : Set X✝¹<VAR>X✝ : ι → Type u_2<VAR>inst✝¹ : (i : ι) → TopologicalSpace (X✝ i)<VAR>X : ι → Type u_3<VAR>inst✝ : (d : ι) → TopologicalSpace (X d)<VAR>s : Set ((i : ι) → X i)<VAR>H : sᶜ ∈ Filter.coprodᵢ fun d => cocompact (X d)<GOAL>sᶜ ∈ cocompact ((d : ι) → X d)
<VAR>X✝¹ : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝³ : TopologicalSpace X✝¹<VAR>inst✝² : TopologicalSpace Y<VAR>s✝ t : Set X✝¹<VAR>X✝ : ι → Type u_2<VAR>inst✝¹ : (i : ι) → TopologicalSpace (X✝ i)<VAR>X : ι → Type u_3<VAR>inst✝ : (d : ι) → TopologicalSpace (X d)<VAR>s : Set ((i : ι) → X i)<VAR>H : ∀ (i : ι), ∃ t, IsCompact t ∧ s ⊆ eval i ⁻¹' t<GOAL>∃ t, IsCompact t ∧ s ⊆ t
<VAR>X✝¹ : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝³ : TopologicalSpace X✝¹<VAR>inst✝² : TopologicalSpace Y<VAR>s✝ t : Set X✝¹<VAR>X✝ : ι → Type u_2<VAR>inst✝¹ : (i : ι) → TopologicalSpace (X✝ i)<VAR>X : ι → Type u_3<VAR>inst✝ : (d : ι) → TopologicalSpace (X d)<VAR>s : Set ((i : ι) → X i)<VAR>K : (i : ι) → Set (X i)<VAR>hKc : ∀ (i : ι), IsCompact (K i)<VAR>htK : ∀ (i : ι), s ⊆ eval i ⁻¹' K i<GOAL>∃ t, IsCompact t ∧ s ⊆ t
<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>p p₀ p₁✝ p₂✝ p₁ p₂ p₃ : P<VAR>h : Wbtw ℝ p₁ p₂ p₃<VAR>hp₂p₁ : p₂ ≠ p₁<GOAL>∠ p₃ p₁ p₂ = 0
<VAR>α : Type u_1<VAR>a : α<VAR>n : Nat<VAR>l : List α<VAR>h : n < l.length<GOAL>l.set n a = take n l ++ a :: drop (n + 1) l
<VAR>n : Nat<VAR>α : Sort u_1<VAR>m : Nat<VAR>f : Fin (n + 1) → α → α<VAR>x : α<VAR>h : m + 1 ≤ n + 1<GOAL>foldr.loop (n + 1) f ⟨m + 1, h⟩ x = f 0 (foldr.loop n (fun i => f i.succ) ⟨m, ⋯⟩ x)
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>h : ↑n ≠ 0<GOAL>0 ^ ↑n = 0
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>h : ↑n ≠ 0<GOAL>n ≠ 0
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>x✝ : -[n+1] ≠ 0<GOAL>0 ^ -[n+1] = 0
<VAR>R : Type u_1<VAR>inst✝¹⁰ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommMonoid N<VAR>inst✝⁶ : Module R N<VAR>ι : Type u_4<VAR>inst✝⁵ : DecidableEq ι<VAR>x y z : M<VAR>S : Type u_5<VAR>inst✝⁴ : OrderedCommSemiring S<VAR>inst✝³ : Algebra S R<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMulPosMono S R<VAR>inst✝ : IsScalarTower S R M<VAR>a : S<VAR>v : M<VAR>h : 0 ≤ a<GOAL>SameRay R v (a • v)
<VAR>R : Type u_1<VAR>inst✝¹⁰ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommMonoid N<VAR>inst✝⁶ : Module R N<VAR>ι : Type u_4<VAR>inst✝⁵ : DecidableEq ι<VAR>x y z : M<VAR>S : Type u_5<VAR>inst✝⁴ : OrderedCommSemiring S<VAR>inst✝³ : Algebra S R<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMulPosMono S R<VAR>inst✝ : IsScalarTower S R M<VAR>a : S<VAR>v : M<VAR>h✝ : 0 ≤ a<VAR>h : (algebraMap S R) a = 0<GOAL>SameRay R v (a • v)
<VAR>R : Type u_1<VAR>inst✝¹⁰ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommMonoid N<VAR>inst✝⁶ : Module R N<VAR>ι : Type u_4<VAR>inst✝⁵ : DecidableEq ι<VAR>x y z : M<VAR>S : Type u_5<VAR>inst✝⁴ : OrderedCommSemiring S<VAR>inst✝³ : Algebra S R<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMulPosMono S R<VAR>inst✝ : IsScalarTower S R M<VAR>a : S<VAR>v : M<VAR>h✝ : 0 ≤ a<VAR>h : 0 < (algebraMap S R) a<GOAL>SameRay R v (a • v)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsAtomistic α<VAR>a b : α<VAR>h : ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)<GOAL>a = b
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝³ : SeminormedGroup E<VAR>inst✝² : SeminormedGroup F<VAR>inst✝¹ : SeminormedGroup G<VAR>s : Set E<VAR>a✝ a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>inst✝ : Subsingleton E<VAR>a : E<GOAL>‖a‖ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Append α<VAR>a b : Part α<VAR>hab : (a ++ b).Dom<GOAL>(a ++ b).get hab = a.get ⋯ ++ b.get ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Append α<VAR>a b : Part α<VAR>hab : (a ++ b).Dom<GOAL>(a.bind fun y => map (fun x => y ++ x) b).get ⋯ = a.get ⋯ ++ b.get ⋯
<VAR>α : Type<VAR>d : ℕ<VAR>ds ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝ : Ring α<VAR>x : Holor α (d :: ds)<GOAL>∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯ = x
<VAR>α : Type<VAR>d : ℕ<VAR>ds ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝ : Ring α<VAR>x : Holor α (d :: ds)<GOAL>(∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯).slice = x.slice
<VAR>α : Type<VAR>d : ℕ<VAR>ds ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝ : Ring α<VAR>x : Holor α (d :: ds)<VAR>i : ℕ<VAR>hid : i < d<GOAL>(∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯).slice i hid = x.slice i hid
<VAR>α : Type<VAR>d : ℕ<VAR>ds ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝ : Ring α<VAR>x : Holor α (d :: ds)<VAR>i : ℕ<VAR>hid : i < d<GOAL>∑ x_1 ∈ (Finset.range d).attach, (unitVec d ↑x_1 ⊗ x.slice ↑x_1 ⋯).slice i hid = x.slice i hid
<VAR>α : Type<VAR>d : ℕ<VAR>ds ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝ : Ring α<VAR>x : Holor α (d :: ds)<VAR>i : ℕ<VAR>hid : i < d<GOAL>(∑ x_1 ∈ (Finset.range d).attach, if i = ↑x_1 then x.slice ↑x_1 ⋯ else 0) = x.slice i hid
<VAR>α : Type<VAR>d : ℕ<VAR>ds ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝ : Ring α<VAR>x : Holor α (d :: ds)<VAR>i : ℕ<VAR>hid : i < d<GOAL>(if i = ↑⟨i, ⋯⟩ then x.slice ↑⟨i, ⋯⟩ ⋯ else 0) = x.slice i hid
<VAR>α : Type<VAR>d : ℕ<VAR>ds ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝ : Ring α<VAR>x : Holor α (d :: ds)<VAR>i : ℕ<VAR>hid : i < d<GOAL>∀ b ∈ (Finset.range d).attach, b ≠ ⟨i, ⋯⟩ → (if i = ↑b then x.slice ↑b ⋯ else 0) = 0
<VAR>α : Type<VAR>d : ℕ<VAR>ds ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝ : Ring α<VAR>x : Holor α (d :: ds)<VAR>i : ℕ<VAR>hid : i < d<GOAL>⟨i, ⋯⟩ ∉ (Finset.range d).attach → (if i = ↑⟨i, ⋯⟩ then x.slice ↑⟨i, ⋯⟩ ⋯ else 0) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : LinearOrderedField R<VAR>inst✝¹ : OrderTopology R<VAR>inst✝ : FloorRing R<GOAL>Tendsto (fun x => ↑⌈x⌉₊ / x) atTop (𝓝 1)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>p : ι → E<VAR>hc : ConvexIndependent 𝕜 p<GOAL>ConvexIndependent 𝕜 Subtype.val
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>p : ι → E<VAR>hc : ConvexIndependent 𝕜 p<VAR>f : ↑(Set.range p) → ι := fun x => Exists.choose ⋯<GOAL>ConvexIndependent 𝕜 Subtype.val
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>p : ι → E<VAR>hc : ConvexIndependent 𝕜 p<VAR>f : ↑(Set.range p) → ι := fun x => Exists.choose ⋯<VAR>hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x<GOAL>ConvexIndependent 𝕜 Subtype.val
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>p : ι → E<VAR>hc : ConvexIndependent 𝕜 p<VAR>f : ↑(Set.range p) → ι := fun x => Exists.choose ⋯<VAR>hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x<VAR>fe : ↑(Set.range p) ↪ ι := { toFun := f, inj' := ⋯ }<GOAL>ConvexIndependent 𝕜 Subtype.val
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>p : ι → E<VAR>hc : ConvexIndependent 𝕜 p<VAR>f : ↑(Set.range p) → ι := fun x => Exists.choose ⋯<VAR>hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x<VAR>fe : ↑(Set.range p) ↪ ι := { toFun := f, inj' := ⋯ }<GOAL>Subtype.val = p ∘ ⇑fe
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>p : ι → E<VAR>hc : ConvexIndependent 𝕜 p<VAR>f : ↑(Set.range p) → ι := fun x => Exists.choose ⋯<VAR>hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x<VAR>fe : ↑(Set.range p) ↪ ι := { toFun := f, inj' := ⋯ }<VAR>x✝ : { x // x ∈ Set.range p }<GOAL>↑x✝ = (p ∘ ⇑fe) x✝
<VAR>α : Type u<VAR>β : Type v<VAR>l l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>L : List (List α)<GOAL>L.join.Nodup ↔ (∀ l ∈ L, l.Nodup) ∧ Pairwise Disjoint L
<VAR>n : ℕ+<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>ce : IsCyclotomicExtension {n} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑n<GOAL>discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis = discr ℚ ⇑(subOnePowerBasis ℚ hζ).basis
<VAR>n : ℕ+<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>ce : IsCyclotomicExtension {n} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>this : NumberField K<GOAL>discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis = discr ℚ ⇑(subOnePowerBasis ℚ hζ).basis
<VAR>n : ℕ+<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>ce : IsCyclotomicExtension {n} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>this : NumberField K<VAR>H₁ : (aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen<VAR>H₂ : (aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen<GOAL>discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis = discr ℚ ⇑(subOnePowerBasis ℚ hζ).basis
<VAR>n : ℕ+<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>ce : IsCyclotomicExtension {n} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>this : NumberField K<VAR>H₁ : (aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen<VAR>H₂ : (aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen<VAR>i : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim<VAR>j : Fin (subOnePowerBasis ℚ hζ).dim<GOAL>IsIntegral ℤ (IsPrimitiveRoot.powerBasis ℚ hζ).gen
<VAR>n : ℕ+<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>ce : IsCyclotomicExtension {n} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>this : NumberField K<VAR>H₁ : (aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen<VAR>H₂ : (aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen<VAR>i : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim<VAR>j : Fin (subOnePowerBasis ℚ hζ).dim<GOAL>minpoly ℚ (IsPrimitiveRoot.powerBasis ℚ hζ).gen = Polynomial.map (algebraMap ℤ ℚ) (minpoly ℤ (IsPrimitiveRoot.powerBasis ℚ hζ).gen)
<VAR>n : ℕ+<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>ce : IsCyclotomicExtension {n} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>this : NumberField K<VAR>H₁ : (aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen<VAR>H₂ : (aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen<VAR>i : Fin (subOnePowerBasis ℚ hζ).dim<VAR>j : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim<GOAL>IsIntegral ℤ (subOnePowerBasis ℚ hζ).gen
<VAR>n : ℕ+<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>ce : IsCyclotomicExtension {n} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>this : NumberField K<VAR>H₁ : (aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen<VAR>H₂ : (aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen<VAR>i : Fin (subOnePowerBasis ℚ hζ).dim<VAR>j : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim<GOAL>minpoly ℚ (subOnePowerBasis ℚ hζ).gen = Polynomial.map (algebraMap ℤ ℚ) (minpoly ℤ (subOnePowerBasis ℚ hζ).gen)
<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>ps : Set P<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ V<VAR>hd : finrank ℝ V = n<VAR>hc : Cospherical ps<VAR>sx₁ sx₂ : Simplex ℝ P n<VAR>hsx₁ : Set.range sx₁.points ⊆ ps<VAR>hsx₂ : Set.range sx₂.points ⊆ ps<GOAL>sx₁.circumsphere = sx₂.circumsphere
<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>ps : Set P<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ V<VAR>hd : finrank ℝ V = n<VAR>hc : Cospherical ps<VAR>sx₁ sx₂ : Simplex ℝ P n<VAR>hsx₁ : Set.range sx₁.points ⊆ ps<VAR>hsx₂ : Set.range sx₂.points ⊆ ps<VAR>r : Sphere P<VAR>hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = r<GOAL>sx₁.circumsphere = sx₂.circumsphere
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : PreconnectedSpace X<VAR>inst✝ : DiscreteTopology X<GOAL>Subsingleton X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : PreconnectedSpace X<VAR>inst✝ : DiscreteTopology X<GOAL>¬Nontrivial X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : PreconnectedSpace X<VAR>inst✝ : DiscreteTopology X<VAR>x y : X<VAR>hxy : x ≠ y<GOAL>False
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : PreconnectedSpace X<VAR>inst✝ : DiscreteTopology X<VAR>x y : X<VAR>hxy : x ∉ univ<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>inst✝¹ : MeasurableSpace α<VAR>p : α → ℕ → Prop<VAR>inst✝ : (x : α) → DecidablePred (p x)<VAR>hp : ∀ (x : α), ∃ N, p x N<VAR>hm : ∀ (k : ℕ), MeasurableSet {x | p x k}<GOAL>Measurable fun x => Nat.find ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>inst✝¹ : MeasurableSpace α<VAR>p : α → ℕ → Prop<VAR>inst✝ : (x : α) → DecidablePred (p x)<VAR>hp : ∀ (x : α), ∃ N, p x N<VAR>hm : ∀ (k : ℕ), MeasurableSet {x | p x k}<VAR>x : α<GOAL>MeasurableSet ((fun x => Nat.find ⋯) ⁻¹' {Nat.find ⋯})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>inst✝¹ : MeasurableSpace α<VAR>p : α → ℕ → Prop<VAR>inst✝ : (x : α) → DecidablePred (p x)<VAR>hp : ∀ (x : α), ∃ N, p x N<VAR>hm : ∀ (k : ℕ), MeasurableSet {x | p x k}<VAR>x : α<GOAL>MeasurableSet (disjointed (fun k => {x | p x k}) (Nat.find ⋯))
<VAR>α : Type u<VAR>a : α<VAR>inst✝¹ : Group α<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>x✝ : Fintype G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : Fintype.card G = p<VAR>g : G<VAR>hg : g ≠ 1<VAR>x : G<GOAL>x ∈ Submonoid.powers g ↔ x ∈ ⊤
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>C U : Set α<VAR>hC : Preperfect C<VAR>hU : IsOpen U<VAR>x : α<VAR>xU : x ∈ U<VAR>xC : x ∈ C<GOAL>AccPt x (𝓟 (U ∩ C))
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>C U : Set α<VAR>hC : Preperfect C<VAR>hU : IsOpen U<VAR>x : α<VAR>xU : x ∈ U<VAR>xC : x ∈ C<GOAL>U ∈ 𝓝 x
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : HasForget₂ C Ab<VAR>inst✝² : Abelian C<VAR>inst✝¹ : (forget₂ C Ab).Additive<VAR>inst✝ : (forget₂ C Ab).PreservesHomology<VAR>D : SnakeInput C<VAR>x₃ : ↑((forget₂ C Ab).obj D.L₀.X₃)<VAR>x₂ : ↑((forget₂ C Ab).obj D.L₁.X₂)<VAR>x₁ : ↑((forget₂ C Ab).obj D.L₂.X₁)<VAR>h₂ : ((forget₂ C Ab).map D.L₁.g) x₂ = ((forget₂ C Ab).map D.v₀₁.τ₃) x₃<VAR>h₁ : ((forget₂ C Ab).map D.L₂.f) x₁ = ((forget₂ C Ab).map D.v₁₂.τ₂) x₂<GOAL>((forget₂ C Ab).map D.δ) x₃ = ((forget₂ C Ab).map D.v₂₃.τ₁) x₁