ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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<VAR>h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫_ℝ = 0<VAR>h0 : p₃ ≠ p₂<GOAL>∠ p₂ p₃ p₁ < π / 2
<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<VAR>h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫_ℝ = 0<VAR>h0 : p₂ -ᵥ p₃ ≠ 0<GOAL>∠ p₂ p₃ p₁ < π / 2
<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<VAR>h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫_ℝ = 0<VAR>h0 : p₂ -ᵥ p₃ ≠ 0<GOAL>InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)) < π / 2
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n j : ℕ<VAR>h : j ≤ 2 * n<VAR>jn : n ≤ j<GOAL>xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n j : ℕ<VAR>h : j ≤ 2 * n<VAR>jn : n ≤ j<VAR>this : 2 * n - j + j ≤ n + j<GOAL>xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n j : ℕ<VAR>h : j ≤ 2 * n<VAR>jn : n ≤ j<VAR>this : 2 * n - j + j ≤ n + j<VAR>t : xn a1 (2 * n - (2 * n - j)) + xn a1 (2 * n - j) ≡ 0 [MOD xn a1 n] := xn_modEq_x2n_sub_lem a1 (Nat.le_of_add_le_add_right this)<GOAL>xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : Group α<VAR>inst✝² : MulAction α β<VAR>inst✝¹ : ContinuousInv α<VAR>inst✝ : ContinuousSMul α β<VAR>s : Set α<VAR>t : Set β<VAR>ht : IsClosed t<VAR>hs : IsCompact s<GOAL>IsClosed (s • t)
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : Group α<VAR>inst✝² : MulAction α β<VAR>inst✝¹ : ContinuousInv α<VAR>inst✝ : ContinuousSMul α β<VAR>s : Set α<VAR>t : Set β<VAR>ht : IsClosed t<VAR>hs : IsCompact s<VAR>this : ∀ x ∈ s • t, ∃ g ∈ s, g⁻¹ • x ∈ t<GOAL>IsClosed (s • t)
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : Group α<VAR>inst✝² : MulAction α β<VAR>inst✝¹ : ContinuousInv α<VAR>inst✝ : ContinuousSMul α β<VAR>s : Set α<VAR>t : Set β<VAR>ht : IsClosed t<VAR>hs : IsCompact s<VAR>f : β → α<VAR>hf : ∀ x ∈ s • t, f x ∈ s ∧ (f x)⁻¹ • x ∈ t<GOAL>IsClosed (s • t)
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : Group α<VAR>inst✝² : MulAction α β<VAR>inst✝¹ : ContinuousInv α<VAR>inst✝ : ContinuousSMul α β<VAR>s : Set α<VAR>t : Set β<VAR>ht : IsClosed t<VAR>hs : IsCompact s<VAR>f : β → α<VAR>hf : ∀ x ∈ s • t, f x ∈ s ∧ (f x)⁻¹ • x ∈ t<VAR>x : β<VAR>hx : x ∈ closure (s • t)<GOAL>x ∈ s • t
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : Group α<VAR>inst✝² : MulAction α β<VAR>inst✝¹ : ContinuousInv α<VAR>inst✝ : ContinuousSMul α β<VAR>s : Set α<VAR>t : Set β<VAR>ht : IsClosed t<VAR>hs : IsCompact s<VAR>f : β → α<VAR>hf : ∀ x ∈ s • t, f x ∈ s ∧ (f x)⁻¹ • x ∈ t<VAR>x : β<VAR>hx : x ∈ closure (s • t)<VAR>u : Ultrafilter β<VAR>hust : s • t ∈ u<VAR>hux : ↑u ≤ 𝓝 x<GOAL>x ∈ s • t
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : Group α<VAR>inst✝² : MulAction α β<VAR>inst✝¹ : ContinuousInv α<VAR>inst✝ : ContinuousSMul α β<VAR>s : Set α<VAR>t : Set β<VAR>ht : IsClosed t<VAR>hs : IsCompact s<VAR>f : β → α<VAR>hf : ∀ x ∈ s • t, f x ∈ s ∧ (f x)⁻¹ • x ∈ t<VAR>x : β<VAR>hx : x ∈ closure (s • t)<VAR>u : Ultrafilter β<VAR>hust : s • t ∈ u<VAR>hux : ↑u ≤ 𝓝 x<VAR>this : ↑(Ultrafilter.map f u) ≤ 𝓟 s<GOAL>x ∈ s • t
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : Group α<VAR>inst✝² : MulAction α β<VAR>inst✝¹ : ContinuousInv α<VAR>inst✝ : ContinuousSMul α β<VAR>s : Set α<VAR>t : Set β<VAR>ht : IsClosed t<VAR>hs : IsCompact s<VAR>f : β → α<VAR>hf : ∀ x ∈ s • t, f x ∈ s ∧ (f x)⁻¹ • x ∈ t<VAR>x : β<VAR>hx : x ∈ closure (s • t)<VAR>u : Ultrafilter β<VAR>hust : s • t ∈ u<VAR>hux : ↑u ≤ 𝓝 x<VAR>this : ↑(Ultrafilter.map f u) ≤ 𝓟 s<VAR>g : α<VAR>hg : g ∈ s<VAR>hug : ↑(Ultrafilter.map f u) ≤ 𝓝 g<GOAL>x ∈ s • t
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : Group α<VAR>inst✝² : MulAction α β<VAR>inst✝¹ : ContinuousInv α<VAR>inst✝ : ContinuousSMul α β<VAR>s : Set α<VAR>t : Set β<VAR>ht : IsClosed t<VAR>hs : IsCompact s<VAR>f : β → α<VAR>hf : ∀ x ∈ s • t, f x ∈ s ∧ (f x)⁻¹ • x ∈ t<VAR>x : β<VAR>hx : x ∈ closure (s • t)<VAR>u : Ultrafilter β<VAR>hust : s • t ∈ u<VAR>hux : ↑u ≤ 𝓝 x<VAR>this : ↑(Ultrafilter.map f u) ≤ 𝓟 s<VAR>g : α<VAR>hg : g ∈ s<VAR>hug : ↑(Ultrafilter.map f u) ≤ 𝓝 g<GOAL>g⁻¹ • x ∈ t
<VAR>x : ℝ<GOAL>Real.toEReal '' Ici x = Ico ↑x ⊤
<VAR>x : ℝ<GOAL>WithBot.some '' (WithTop.some '' Ici x) = Ico ↑x ⊤
<VAR>x : ℝ<GOAL>Ico ↑↑x ↑⊤ = Ico ↑x ⊤
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : 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✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>N N₁ N₂ : LieSubmodule R L M<VAR>m✝ : M<GOAL>m✝ ∈ (N₁ ⊓ N₂).normalizer ↔ m✝ ∈ N₁.normalizer ⊓ N₂.normalizer
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>m : MeasurableSpace α<VAR>f : α → ℝ≥0∞<VAR>μ : Measure α<GOAL>∫⁻ (a : α), f a ∂μ = ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(↑φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>m : MeasurableSpace α<VAR>f : α → ℝ≥0∞<VAR>μ : Measure α<GOAL>⨆ g, ⨆ (_ : ↑g ≤ fun a => f a), g.lintegral μ = ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(↑φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>m : MeasurableSpace α<VAR>f : α → ℝ≥0∞<VAR>μ : Measure α<VAR>φ : α →ₛ ℝ≥0∞<VAR>hφ : ↑φ ≤ fun a => f a<GOAL>φ.lintegral μ ≤ ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(↑φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>f : X → Y<VAR>hf : Inducing f<GOAL>IsPathConnected F ↔ IsPathConnected (f '' F)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>f : X → Y<VAR>hf : Inducing f<VAR>hF : IsPathConnected (f '' F)<GOAL>IsPathConnected F
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>f : X → Y<VAR>hf : Inducing f<VAR>hF : F.Nonempty ∧ ∀ a ∈ F, ∀ a_2 ∈ F, JoinedIn (f '' F) (f a) (f a_2)<GOAL>F.Nonempty ∧ ∀ x ∈ F, ∀ y ∈ F, JoinedIn F x y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x✝ y✝ z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>f : X → Y<VAR>hf : Inducing f<VAR>hF : F.Nonempty ∧ ∀ a ∈ F, ∀ a_2 ∈ F, JoinedIn (f '' F) (f a) (f a_2)<VAR>x : X<VAR>hx : x ∈ F<VAR>y : X<VAR>hy : y ∈ F<GOAL>JoinedIn F x y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x✝ y✝ z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>f : X → Y<VAR>hf : Inducing f<VAR>hF : F.Nonempty ∧ ∀ a ∈ F, ∀ a_2 ∈ F, JoinedIn (f '' F) (f a) (f a_2)<VAR>x : X<VAR>hx : x ∈ F<VAR>y : X<VAR>hy : y ∈ F<VAR>γ : Path (f x) (f y)<VAR>hγ : ∀ (t : ↑I), γ t ∈ f '' F<GOAL>JoinedIn F x y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x✝ y✝ z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>f : X → Y<VAR>hf : Inducing f<VAR>hF : F.Nonempty ∧ ∀ a ∈ F, ∀ a_2 ∈ F, JoinedIn (f '' F) (f a) (f a_2)<VAR>x : X<VAR>hx : x ∈ F<VAR>y : X<VAR>hy : y ∈ F<VAR>γ : Path (f x) (f y)<VAR>γ' : ↑I → X<VAR>hγ' : ∀ (t : ↑I), γ' t ∈ F<VAR>hγγ' : ∀ (t : ↑I), f (γ' t) = γ t<GOAL>JoinedIn F x y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x✝ y✝ z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>f : X → Y<VAR>hf : Inducing f<VAR>hF : F.Nonempty ∧ ∀ a ∈ F, ∀ a_2 ∈ F, JoinedIn (f '' F) (f a) (f a_2)<VAR>x : X<VAR>hx : x ∈ F<VAR>y : X<VAR>hy : y ∈ F<VAR>γ : Path (f x) (f y)<VAR>γ' : ↑I → X<VAR>hγ' : ∀ (t : ↑I), γ' t ∈ F<VAR>hγγ' : ∀ (t : ↑I), f (γ' t) = γ t<VAR>key₁ : Inseparable x (γ' 0)<GOAL>JoinedIn F x y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x✝ y✝ z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>f : X → Y<VAR>hf : Inducing f<VAR>hF : F.Nonempty ∧ ∀ a ∈ F, ∀ a_2 ∈ F, JoinedIn (f '' F) (f a) (f a_2)<VAR>x : X<VAR>hx : x ∈ F<VAR>y : X<VAR>hy : y ∈ F<VAR>γ : Path (f x) (f y)<VAR>γ' : ↑I → X<VAR>hγ' : ∀ (t : ↑I), γ' t ∈ F<VAR>hγγ' : ∀ (t : ↑I), f (γ' t) = γ t<VAR>key₁ : Inseparable x (γ' 0)<VAR>key₂ : Inseparable (γ' 1) y<GOAL>JoinedIn F x y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x✝ y✝ z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>f : X → Y<VAR>hf : Inducing f<VAR>hF : F.Nonempty ∧ ∀ a ∈ F, ∀ a_2 ∈ F, JoinedIn (f '' F) (f a) (f a_2)<VAR>x : X<VAR>hx : x ∈ F<VAR>y : X<VAR>hy : y ∈ F<VAR>γ : Path (f x) (f y)<VAR>γ' : ↑I → X<VAR>hγ' : ∀ (t : ↑I), γ' t ∈ F<VAR>hγγ' : ∀ (t : ↑I), f (γ' t) = γ t<VAR>key₁ : Inseparable x (γ' 0)<VAR>key₂ : Inseparable (γ' 1) y<GOAL>Continuous γ'
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : MulOneClass M<VAR>S T : Submonoid M<GOAL>∀ {x : M}, x ∈ T → x ∈ S ⊔ T
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : MulOneClass M<VAR>S T : Submonoid M<GOAL>T ≤ S ⊔ T
<VAR>ι✝ : Type u_1<VAR>κ : Type u_2<VAR>α✝ : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α✝<VAR>a : α✝<VAR>f g : α✝ → β<VAR>ι : Type u_6<VAR>α : Type u_7<VAR>inst✝¹ : LinearOrder ι<VAR>inst✝ : AddCommMonoid α<VAR>s : Finset ι<VAR>p : Sym2 ι → α<GOAL>∑ i ∈ filter (fun x => ¬x.IsDiag) s.sym2, p i = ∑ i ∈ filter (fun i => i.1 < i.2) s.offDiag, p s(i.1, i.2)
<VAR>ι✝ : Type u_1<VAR>κ : Type u_2<VAR>α✝ : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α✝<VAR>a : α✝<VAR>f g : α✝ → β<VAR>ι : Type u_6<VAR>α : Type u_7<VAR>inst✝¹ : LinearOrder ι<VAR>inst✝ : AddCommMonoid α<VAR>s : Finset ι<VAR>p : Sym2 ι → α<GOAL>∑ i ∈ filter (fun x => ¬x.IsDiag) s.sym2, p i = ∑ i ∈ filter (fun i => i.1 ≤ i.2) s.offDiag, p s(i.1, i.2)
<VAR>ι✝ : Type u_1<VAR>κ : Type u_2<VAR>α✝ : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α✝<VAR>a : α✝<VAR>f g : α✝ → β<VAR>ι : Type u_6<VAR>α : Type u_7<VAR>inst✝¹ : LinearOrder ι<VAR>inst✝ : AddCommMonoid α<VAR>s : Finset ι<VAR>p : Sym2 ι → α<GOAL>∑ i ∈ filter (fun x => ¬x.IsDiag) s.sym2, p i = ∑ x ∈ Finset.subtype (fun i => i.1 ≤ i.2) s.offDiag, p s((↑x).1, (↑x).2)
<VAR>ι✝ : Type u_1<VAR>κ : Type u_2<VAR>α✝ : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α✝<VAR>a : α✝<VAR>f g : α✝ → β<VAR>ι : Type u_6<VAR>α : Type u_7<VAR>inst✝¹ : LinearOrder ι<VAR>inst✝ : AddCommMonoid α<VAR>s : Finset ι<VAR>p : Sym2 ι → α<GOAL>∀ (i : { p // p.1 ≤ p.2 }), i ∈ Finset.subtype (fun i => i.1 ≤ i.2) s.offDiag ↔ Sym2.sortEquiv.symm i ∈ filter (fun x => ¬x.IsDiag) s.sym2
<VAR>ι✝ : Type u_1<VAR>κ : Type u_2<VAR>α✝ : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α✝<VAR>a : α✝<VAR>f g : α✝ → β<VAR>ι : Type u_6<VAR>α : Type u_7<VAR>inst✝¹ : LinearOrder ι<VAR>inst✝ : AddCommMonoid α<VAR>s : Finset ι<VAR>p : Sym2 ι → α<GOAL>∀ i ∈ Finset.subtype (fun i => i.1 ≤ i.2) s.offDiag, p s((↑i).1, (↑i).2) = p (Sym2.sortEquiv.symm i)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>nd : l.Nodup<VAR>h : ∀ (x : α), x ∈ l<VAR>i : Fin l.length<GOAL>(fun a => ⟨indexOf a l, ⋯⟩) ((fun i => l.get i) i) = i
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : DecidableEq E<VAR>t : Finset E<VAR>h : ¬AffineIndependent 𝕜 Subtype.val<VAR>x : E<VAR>m : x ∈ (convexHull 𝕜) ↑t<GOAL>∃ y, x ∈ (convexHull 𝕜) ↑(t.erase ↑y)
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : DecidableEq E<VAR>t : Finset E<VAR>h : ¬AffineIndependent 𝕜 Subtype.val<VAR>x : E<VAR>m : ∃ w, (∀ y ∈ t, 0 ≤ w y) ∧ ∑ y ∈ t, w y = 1 ∧ t.centerMass w id = x<GOAL>∃ y w, (∀ y_1 ∈ t.erase ↑y, 0 ≤ w y_1) ∧ ∑ y ∈ t.erase ↑y, w y = 1 ∧ (t.erase ↑y).centerMass w id = x
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : DecidableEq E<VAR>t : Finset E<VAR>h : ¬AffineIndependent 𝕜 Subtype.val<VAR>f : E → 𝕜<VAR>fpos : ∀ y ∈ t, 0 ≤ f y<VAR>fsum : ∑ y ∈ t, f y = 1<GOAL>∃ y w, (∀ y_1 ∈ t.erase ↑y, 0 ≤ w y_1) ∧ ∑ y ∈ t.erase ↑y, w y = 1 ∧ (t.erase ↑y).centerMass w id = t.centerMass f id
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : DecidableEq E<VAR>t : Finset E<VAR>h : ¬AffineIndependent 𝕜 Subtype.val<VAR>f : E → 𝕜<VAR>fpos : ∀ y ∈ t, 0 ≤ f y<VAR>fsum : ∑ y ∈ t, f y = 1<VAR>g : E → 𝕜<VAR>gcombo : ∑ e ∈ t, g e • e = 0<VAR>gsum : ∑ e ∈ t, g e = 0<VAR>gpos : ∃ x ∈ t, g x ≠ 0<GOAL>∃ y w, (∀ y_1 ∈ t.erase ↑y, 0 ≤ w y_1) ∧ ∑ y ∈ t.erase ↑y, w y = 1 ∧ (t.erase ↑y).centerMass w id = t.centerMass f id
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : DecidableEq E<VAR>t : Finset E<VAR>h : ¬AffineIndependent 𝕜 Subtype.val<VAR>f : E → 𝕜<VAR>fpos : ∀ y ∈ t, 0 ≤ f y<VAR>fsum : ∑ y ∈ t, f y = 1<VAR>g : E → 𝕜<VAR>gcombo : ∑ e ∈ t, g e • e = 0<VAR>gsum : ∑ e ∈ t, g e = 0<VAR>gpos : ∃ i ∈ t, 0 < g i<GOAL>∃ y w, (∀ y_1 ∈ t.erase ↑y, 0 ≤ w y_1) ∧ ∑ y ∈ t.erase ↑y, w y = 1 ∧ (t.erase ↑y).centerMass w id = t.centerMass f id
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : DecidableEq E<VAR>t : Finset E<VAR>f : E → 𝕜<VAR>fpos : ∀ y ∈ t, 0 ≤ f y<VAR>fsum : ∑ y ∈ t, f y = 1<VAR>g : E → 𝕜<VAR>gcombo : ∑ e ∈ t, g e • e = 0<VAR>gsum : ∑ e ∈ t, g e = 0<VAR>gpos : ∃ i ∈ t, 0 < g i<VAR>s : Finset E := filter (fun z => 0 < g z) t<GOAL>∃ y w, (∀ y_1 ∈ t.erase ↑y, 0 ≤ w y_1) ∧ ∑ y ∈ t.erase ↑y, w y = 1 ∧ (t.erase ↑y).centerMass w id = t.centerMass f id
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : DecidableEq E<VAR>t : Finset E<VAR>f : E → 𝕜<VAR>fpos : ∀ y ∈ t, 0 ≤ f y<VAR>fsum : ∑ y ∈ t, f y = 1<VAR>g : E → 𝕜<VAR>gcombo : ∑ e ∈ t, g e • e = 0<VAR>gsum : ∑ e ∈ t, g e = 0<VAR>gpos : ∃ i ∈ t, 0 < g i<VAR>s : Finset E := filter (fun z => 0 < g z) t<VAR>i₀ : E<VAR>mem : i₀ ∈ s<VAR>w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i<GOAL>∃ y w, (∀ y_1 ∈ t.erase ↑y, 0 ≤ w y_1) ∧ ∑ y ∈ t.erase ↑y, w y = 1 ∧ (t.erase ↑y).centerMass w id = t.centerMass f id
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : DecidableEq E<VAR>t : Finset E<VAR>f : E → 𝕜<VAR>fpos : ∀ y ∈ t, 0 ≤ f y<VAR>fsum : ∑ y ∈ t, f y = 1<VAR>g : E → 𝕜<VAR>gcombo : ∑ e ∈ t, g e • e = 0<VAR>gsum : ∑ e ∈ t, g e = 0<VAR>gpos : ∃ i ∈ t, 0 < g i<VAR>s : Finset E := filter (fun z => 0 < g z) t<VAR>i₀ : E<VAR>mem : i₀ ∈ s<VAR>w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i<VAR>hg : 0 < g i₀<GOAL>∃ y w, (∀ y_1 ∈ t.erase ↑y, 0 ≤ w y_1) ∧ ∑ y ∈ t.erase ↑y, w y = 1 ∧ (t.erase ↑y).centerMass w id = t.centerMass f id
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : DecidableEq E<VAR>t : Finset E<VAR>f : E → 𝕜<VAR>fpos : ∀ y ∈ t, 0 ≤ f y<VAR>fsum : ∑ y ∈ t, f y = 1<VAR>g : E → 𝕜<VAR>gcombo : ∑ e ∈ t, g e • e = 0<VAR>gsum : ∑ e ∈ t, g e = 0<VAR>gpos : ∃ i ∈ t, 0 < g i<VAR>s : Finset E := filter (fun z => 0 < g z) t<VAR>i₀ : E<VAR>mem : i₀ ∈ s<VAR>w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i<VAR>hg : 0 < g i₀<VAR>hi₀ : i₀ ∈ t<GOAL>∃ y w, (∀ y_1 ∈ t.erase ↑y, 0 ≤ w y_1) ∧ ∑ y ∈ t.erase ↑y, w y = 1 ∧ (t.erase ↑y).centerMass w id = t.centerMass f id
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : DecidableEq E<VAR>t : Finset E<VAR>f : E → 𝕜<VAR>fpos : ∀ y ∈ t, 0 ≤ f y<VAR>fsum : ∑ y ∈ t, f y = 1<VAR>g : E → 𝕜<VAR>gcombo : ∑ e ∈ t, g e • e = 0<VAR>gsum : ∑ e ∈ t, g e = 0<VAR>gpos : ∃ i ∈ t, 0 < g i<VAR>s : Finset E := filter (fun z => 0 < g z) t<VAR>i₀ : E<VAR>mem : i₀ ∈ s<VAR>w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i<VAR>hg : 0 < g i₀<VAR>hi₀ : i₀ ∈ t<VAR>k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z<GOAL>∃ y w, (∀ y_1 ∈ t.erase ↑y, 0 ≤ w y_1) ∧ ∑ y ∈ t.erase ↑y, w y = 1 ∧ (t.erase ↑y).centerMass w id = t.centerMass f id
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : DecidableEq E<VAR>t : Finset E<VAR>f : E → 𝕜<VAR>fpos : ∀ y ∈ t, 0 ≤ f y<VAR>fsum : ∑ y ∈ t, f y = 1<VAR>g : E → 𝕜<VAR>gcombo : ∑ e ∈ t, g e • e = 0<VAR>gsum : ∑ e ∈ t, g e = 0<VAR>gpos : ∃ i ∈ t, 0 < g i<VAR>s : Finset E := filter (fun z => 0 < g z) t<VAR>i₀ : E<VAR>mem : i₀ ∈ s<VAR>w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i<VAR>hg : 0 < g i₀<VAR>hi₀ : i₀ ∈ t<VAR>k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z<VAR>hk : k i₀ = 0<GOAL>∃ y w, (∀ y_1 ∈ t.erase ↑y, 0 ≤ w y_1) ∧ ∑ y ∈ t.erase ↑y, w y = 1 ∧ (t.erase ↑y).centerMass w id = t.centerMass f id
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : DecidableEq E<VAR>t : Finset E<VAR>f : E → 𝕜<VAR>fpos : ∀ y ∈ t, 0 ≤ f y<VAR>fsum : ∑ y ∈ t, f y = 1<VAR>g : E → 𝕜<VAR>gcombo : ∑ e ∈ t, g e • e = 0<VAR>gsum : ∑ e ∈ t, g e = 0<VAR>gpos : ∃ i ∈ t, 0 < g i<VAR>s : Finset E := filter (fun z => 0 < g z) t<VAR>i₀ : E<VAR>mem : i₀ ∈ s<VAR>w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i<VAR>hg : 0 < g i₀<VAR>hi₀ : i₀ ∈ t<VAR>k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z<VAR>hk : k i₀ = 0<VAR>ksum : ∑ e ∈ t.erase i₀, k e = 1<GOAL>∃ y w, (∀ y_1 ∈ t.erase ↑y, 0 ≤ w y_1) ∧ ∑ y ∈ t.erase ↑y, w y = 1 ∧ (t.erase ↑y).centerMass w id = t.centerMass f id
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>A : Cᵒᵖ ⥤ Type v<VAR>F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v<VAR>X : C<VAR>G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v<VAR>η : F ⟶ G<VAR>p : YonedaCollection F X<GOAL>op (CostructuredArrow.mk p.fst) = op (CostructuredArrow.mk (map₁ η p).fst)
<VAR>n : ℤ<VAR>z τ : ℂ<VAR>f : ℂ × ℂ → ℂ := fun p => 2 * ↑π * I * ↑n * p.1 + ↑π * I * ↑n ^ 2 * p.2<GOAL>HasFDerivAt (fun p => jacobiTheta₂_term n p.1 p.2) (jacobiTheta₂_term_fderiv n z τ) (z, τ)
<VAR>n : ℤ<VAR>z τ : ℂ<VAR>f : ℂ × ℂ → ℂ := fun p => 2 * ↑π * I * ↑n * p.1 + ↑π * I * ↑n ^ 2 * p.2<GOAL>HasFDerivAt f ((2 * ↑π * I * ↑n) • ContinuousLinearMap.fst ℂ ℂ ℂ + (↑π * I * ↑n ^ 2) • ContinuousLinearMap.snd ℂ ℂ ℂ) (z, τ)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIcoMod hp a (p + b) = toIcoMod hp a b
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F✝ : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f✝ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f f' : ℝ → E<VAR>hab : a < b<VAR>fa fb : E<VAR>hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hint : IntervalIntegrable f' volume a b<VAR>ha : Tendsto f (𝓝[>] a) (𝓝 fa)<VAR>hb : Tendsto f (𝓝[<] b) (𝓝 fb)<VAR>F : ℝ → E := update (update f a fa) b fb<GOAL>∫ (y : ℝ) in a..b, f' y = fb - fa
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F✝ : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f✝ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f f' : ℝ → E<VAR>hab : a < b<VAR>fa fb : E<VAR>hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hint : IntervalIntegrable f' volume a b<VAR>ha : Tendsto f (𝓝[>] a) (𝓝 fa)<VAR>hb : Tendsto f (𝓝[<] b) (𝓝 fb)<VAR>F : ℝ → E := update (update f a fa) b fb<VAR>Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x<GOAL>∫ (y : ℝ) in a..b, f' y = fb - fa
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F✝ : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f✝ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f f' : ℝ → E<VAR>hab : a < b<VAR>fa fb : E<VAR>hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hint : IntervalIntegrable f' volume a b<VAR>ha : Tendsto f (𝓝[>] a) (𝓝 fa)<VAR>hb : Tendsto f (𝓝[<] b) (𝓝 fb)<VAR>F : ℝ → E := update (update f a fa) b fb<VAR>Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x<VAR>hcont : ContinuousOn F (Icc a b)<GOAL>∫ (y : ℝ) in a..b, f' y = fb - fa
<VAR>R✝ : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>A₃ : Type uA₃<VAR>A₁' : Type uA₁'<VAR>A₂' : Type uA₂'<VAR>A₃' : Type uA₃'<VAR>inst✝¹⁵ : CommSemiring R✝<VAR>inst✝¹⁴ : Semiring A₁<VAR>inst✝¹³ : Semiring A₂<VAR>inst✝¹² : Semiring A₃<VAR>inst✝¹¹ : Semiring A₁'<VAR>inst✝¹⁰ : Semiring A₂'<VAR>inst✝⁹ : Semiring A₃'<VAR>inst✝⁸ : Algebra R✝ A₁<VAR>inst✝⁷ : Algebra R✝ A₂<VAR>inst✝⁶ : Algebra R✝ A₃<VAR>inst✝⁵ : Algebra R✝ A₁'<VAR>inst✝⁴ : Algebra R✝ A₂'<VAR>inst✝³ : Algebra R✝ A₃'<VAR>e : A₁ ≃ₐ[R✝] A₂<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>f : (S →ₐ[R] S)ˣ<VAR>x : S<GOAL>↑(f⁻¹ * f) x = x
<VAR>R✝ : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>A₃ : Type uA₃<VAR>A₁' : Type uA₁'<VAR>A₂' : Type uA₂'<VAR>A₃' : Type uA₃'<VAR>inst✝¹⁵ : CommSemiring R✝<VAR>inst✝¹⁴ : Semiring A₁<VAR>inst✝¹³ : Semiring A₂<VAR>inst✝¹² : Semiring A₃<VAR>inst✝¹¹ : Semiring A₁'<VAR>inst✝¹⁰ : Semiring A₂'<VAR>inst✝⁹ : Semiring A₃'<VAR>inst✝⁸ : Algebra R✝ A₁<VAR>inst✝⁷ : Algebra R✝ A₂<VAR>inst✝⁶ : Algebra R✝ A₃<VAR>inst✝⁵ : Algebra R✝ A₁'<VAR>inst✝⁴ : Algebra R✝ A₂'<VAR>inst✝³ : Algebra R✝ A₃'<VAR>e : A₁ ≃ₐ[R✝] A₂<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>f : (S →ₐ[R] S)ˣ<VAR>x : S<GOAL>↑1 x = x
<VAR>R✝ : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>A₃ : Type uA₃<VAR>A₁' : Type uA₁'<VAR>A₂' : Type uA₂'<VAR>A₃' : Type uA₃'<VAR>inst✝¹⁵ : CommSemiring R✝<VAR>inst✝¹⁴ : Semiring A₁<VAR>inst✝¹³ : Semiring A₂<VAR>inst✝¹² : Semiring A₃<VAR>inst✝¹¹ : Semiring A₁'<VAR>inst✝¹⁰ : Semiring A₂'<VAR>inst✝⁹ : Semiring A₃'<VAR>inst✝⁸ : Algebra R✝ A₁<VAR>inst✝⁷ : Algebra R✝ A₂<VAR>inst✝⁶ : Algebra R✝ A₃<VAR>inst✝⁵ : Algebra R✝ A₁'<VAR>inst✝⁴ : Algebra R✝ A₂'<VAR>inst✝³ : Algebra R✝ A₃'<VAR>e : A₁ ≃ₐ[R✝] A₂<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>f : (S →ₐ[R] S)ˣ<VAR>x : S<GOAL>↑(f * f⁻¹) x = x
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ Z✝ X Y Z : C<VAR>f f' : X ⟶ Y<VAR>g : Z ≅ Y<GOAL>f ≫ g.inv = f' ≫ g.inv ↔ f = f'
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : Field R<VAR>p q : R[X]<VAR>inst✝¹ : CommSemiring k<VAR>inst✝ : DecidableEq R<VAR>ϕ : R →+* k<VAR>f g : R[X]<VAR>α : k<VAR>hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0<GOAL>eval₂ ϕ α f = 0
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : Field R<VAR>p✝ q : R[X]<VAR>inst✝¹ : CommSemiring k<VAR>inst✝ : DecidableEq R<VAR>ϕ : R →+* k<VAR>f g : R[X]<VAR>α : k<VAR>hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0<VAR>p : R[X]<VAR>hp : f = EuclideanDomain.gcd f g * p<GOAL>eval₂ ϕ α f = 0