ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>X : ℝ<VAR>hX : 0 ≤ X<VAR>F_der_I : ∀ x ∈ Ioo 0 X, HasDerivAt (fun x => ↑(rexp (-x)) * ↑x ^ s) (-(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) x<VAR>cont : Continuous fun x => (ofReal' ∘ fun y => rexp (-y)) x * ↑x ^ s<VAR>der_ible : IntervalIntegrable (fun x => -(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 X<VAR>int_eval : (∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ s) + -∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * (s * ↑x ^ (s - 1)) = -((ofReal' ∘ fun y => rexp (-y)) X * ↑X ^ s - (ofReal' ∘ fun y => rexp (-y)) 0 * ↑0 ^ s)<VAR>this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * ↑(rexp (-x)) * ↑x ^ (s - 1)<VAR>t : ∫ (x : ℝ) in 0 ..X, s * (↑(rexp (-x)) * ↑x ^ (s - 1)) = s * ∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ (s - 1)<GOAL>(∫ (x : ℝ) in 0 ..X, s * ↑(rexp (-x)) * ↑x ^ (s - 1)) + (ofReal' ∘ fun y => rexp (-y)) 0 * 0 - (ofReal' ∘ fun y => rexp (-y)) X * ↑X ^ s = (∫ (x : ℝ) in 0 ..X, s * (↑(rexp (-x)) * ↑x ^ (s - 1))) - ↑(rexp (-X)) * ↑X ^ s
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>X : ℝ<VAR>hX : 0 ≤ X<VAR>F_der_I : ∀ x ∈ Ioo 0 X, HasDerivAt (fun x => ↑(rexp (-x)) * ↑x ^ s) (-(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) x<VAR>cont : Continuous fun x => (ofReal' ∘ fun y => rexp (-y)) x * ↑x ^ s<VAR>der_ible : IntervalIntegrable (fun x => -(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 X<VAR>int_eval : (∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ s) + -∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * (s * ↑x ^ (s - 1)) = -((ofReal' ∘ fun y => rexp (-y)) X * ↑X ^ s - (ofReal' ∘ fun y => rexp (-y)) 0 * ↑0 ^ s)<VAR>this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * ↑(rexp (-x)) * ↑x ^ (s - 1)<VAR>t : ∫ (x : ℝ) in 0 ..X, s * (↑(rexp (-x)) * ↑x ^ (s - 1)) = s * ∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ (s - 1)<GOAL>s ≠ 0
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁴ : CommSemiring K<VAR>inst✝³ : CommSemiring L<VAR>inst✝² : Algebra K L<VAR>E1 E2 : Subalgebra K L<VAR>inst✝¹ : Module.Finite K ↥E1<VAR>inst✝ : Module.Finite K ↥E2<GOAL>Module.Finite K ↥(E1 ⊔ E2)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁴ : CommSemiring K<VAR>inst✝³ : CommSemiring L<VAR>inst✝² : Algebra K L<VAR>E1 E2 : Subalgebra K L<VAR>inst✝¹ : Module.Finite K ↥E1<VAR>inst✝ : Module.Finite K ↥E2<GOAL>Module.Finite K ↥(Algebra.TensorProduct.productMap E1.val E2.val).range
<VAR>a b : ℝ<VAR>n : ℕ<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>∫ (x : ℝ) in a..b, 1 / x = Real.log (b / a)
<VAR>m✝ n a b c d m : ℕ<VAR>h : a ≡ b [MOD n]<GOAL>a ^ m ≡ b ^ m [MOD n]
<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>P : Fin 3 → R<VAR>u : R<GOAL>W'.dblXYZ (u • P) = u ^ 4 • W'.dblXYZ P
<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>P : Fin 3 → R<VAR>u : R<GOAL>![(u ^ 4) ^ 2 * W'.dblX P, (u ^ 4) ^ 3 * W'.dblY P, u ^ 4 * W'.dblZ P] = u ^ 4 • W'.dblXYZ P
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace T<VAR>K : Set X<VAR>U : Set Y<VAR>f g : C(X, Y)<GOAL>⇑f ⤳ ⇑g ↔ f ⤳ g
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace T<VAR>K : Set X<VAR>U : Set Y<VAR>f g : C(X, Y)<VAR>h : ⇑f ⤳ ⇑g<GOAL>f ⤳ g
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace T<VAR>K : Set X<VAR>U : Set Y<VAR>f g : C(X, Y)<VAR>h : ⇑f ⤳ ⇑g<GOAL>∀ (K : Set X), IsCompact K → ∀ (U : Set Y), IsOpen U → MapsTo (⇑g) K U → MapsTo (⇑f) K U
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>S : Set (Set X)<VAR>t : Set X<VAR>x : X<VAR>inst✝ : SequentialSpace X<VAR>h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S<GOAL>RestrictGenTopology S
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>S : Set (Set X)<VAR>t✝ : Set X<VAR>x✝ : X<VAR>inst✝ : SequentialSpace X<VAR>h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S<VAR>t : Set X<VAR>ht : ∀ s ∈ S, IsClosed (Subtype.val ⁻¹' t)<VAR>u : ℕ → X<VAR>x : X<VAR>hut : ∀ (n : ℕ), u n ∈ t<VAR>hux : Tendsto u atTop (𝓝 x)<GOAL>x ∈ t
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>S : Set (Set X)<VAR>t✝ : Set X<VAR>x✝ : X<VAR>inst✝ : SequentialSpace X<VAR>h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S<VAR>t : Set X<VAR>ht : ∀ s ∈ S, IsClosed (Subtype.val ⁻¹' t)<VAR>u : ℕ → X<VAR>x : X<VAR>hut : ∀ (n : ℕ), u n ∈ t<VAR>hux : Tendsto u atTop (𝓝 x)<VAR>s : Set X<VAR>hsc : IsClosed s<VAR>hst : Subtype.val ⁻¹' s = Subtype.val ⁻¹' t<GOAL>x ∈ t
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>S : Set (Set X)<VAR>t✝ : Set X<VAR>x✝ : X<VAR>inst✝ : SequentialSpace X<VAR>h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S<VAR>t : Set X<VAR>ht : ∀ s ∈ S, IsClosed (Subtype.val ⁻¹' t)<VAR>u : ℕ → X<VAR>x : X<VAR>hut : ∀ (n : ℕ), u n ∈ t<VAR>hux : Tendsto u atTop (𝓝 x)<VAR>s : Set X<VAR>hsc : IsClosed s<VAR>hst : ∀ (x_1 : X), x_1 ∈ insert x (range u) ∩ s ↔ x_1 ∈ insert x (range u) ∩ t<GOAL>x ∈ t
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>S : Set (Set X)<VAR>t✝ : Set X<VAR>x✝ : X<VAR>inst✝ : SequentialSpace X<VAR>h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S<VAR>t : Set X<VAR>ht : ∀ s ∈ S, IsClosed (Subtype.val ⁻¹' t)<VAR>u : ℕ → X<VAR>x : X<VAR>hut : ∀ (n : ℕ), u n ∈ t<VAR>hux : Tendsto u atTop (𝓝 x)<VAR>s : Set X<VAR>hsc : IsClosed s<VAR>hst : ∀ (x_1 : X), x_1 ∈ insert x (range u) ∩ s ↔ x_1 ∈ insert x (range u) ∩ t<GOAL>x ∈ s
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>S : Set (Set X)<VAR>t✝ : Set X<VAR>x✝ : X<VAR>inst✝ : SequentialSpace X<VAR>h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S<VAR>t : Set X<VAR>ht : ∀ s ∈ S, IsClosed (Subtype.val ⁻¹' t)<VAR>u : ℕ → X<VAR>x : X<VAR>hut : ∀ (n : ℕ), u n ∈ t<VAR>hux : Tendsto u atTop (𝓝 x)<VAR>s : Set X<VAR>hsc : IsClosed s<VAR>hst : ∀ (x_1 : X), x_1 ∈ insert x (range u) ∩ s ↔ x_1 ∈ insert x (range u) ∩ t<VAR>k : ℕ<GOAL>u k ∈ s
<VAR>G✝ : Type u<VAR>inst✝² : Monoid G✝<VAR>G : Type u_1<VAR>inst✝¹ : Monoid G<VAR>inst✝ : Nontrivial G<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>exponent G = p ↔ ∀ (g : G), g ≠ 1 → orderOf g = p
<VAR>G✝ : Type u<VAR>inst✝² : Monoid G✝<VAR>G : Type u_1<VAR>inst✝¹ : Monoid G<VAR>inst✝ : Nontrivial G<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hG : exponent G = p<VAR>g : G<VAR>hg : g ≠ 1<GOAL>orderOf g = p
<VAR>G✝ : Type u<VAR>inst✝² : Monoid G✝<VAR>G : Type u_1<VAR>inst✝¹ : Monoid G<VAR>inst✝ : Nontrivial G<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>h : ∀ (g : G), g ≠ 1 → orderOf g = p<GOAL>exponent G ∣ p
<VAR>G✝ : Type u<VAR>inst✝² : Monoid G✝<VAR>G : Type u_1<VAR>inst✝¹ : Monoid G<VAR>inst✝ : Nontrivial G<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>h : ∀ (g : G), g ≠ 1 → orderOf g = p<GOAL>p ∣ exponent G
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>h : LinearIndependent R v<VAR>f : ι' → ι<VAR>hf : Injective f<GOAL>LinearIndependent R (v ∘ f)
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>h : LinearIndependent R v<VAR>f : ι' → ι<VAR>hf : Injective f<GOAL>∀ (l : ι' →₀ R), (Finsupp.total ι M R v ∘ₗ Finsupp.lmapDomain R R f) l = 0 → l = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>h : LinearIndependent R v<VAR>f : ι' → ι<VAR>hf : Injective f<VAR>l : ι' →₀ R<VAR>hl : (Finsupp.total ι M R v ∘ₗ Finsupp.lmapDomain R R f) l = 0<GOAL>l = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>h : LinearIndependent R v<VAR>f : ι' → ι<VAR>hf : Injective f<VAR>l : ι' →₀ R<VAR>hl : (Finsupp.total ι M R v ∘ₗ Finsupp.lmapDomain R R f) l = 0<VAR>h_map_domain : ∀ (x : ι'), (Finsupp.mapDomain f l) (f x) = 0<GOAL>l = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x✝ y : M<VAR>h : LinearIndependent R v<VAR>f : ι' → ι<VAR>hf : Injective f<VAR>l : ι' →₀ R<VAR>hl : (Finsupp.total ι M R v ∘ₗ Finsupp.lmapDomain R R f) l = 0<VAR>h_map_domain : ∀ (x : ι'), (Finsupp.mapDomain f l) (f x) = 0<VAR>x : ι'<GOAL>l x = (Finsupp.mapDomain f l) (f x)
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f g : Perm α<VAR>x : α<GOAL>f x ∈ f.support ↔ x ∈ f.support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : ℕ →. ℕ<GOAL>Partrec f ↔ Nat.Partrec f
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s t : Set G<VAR>ht : IsOpen t<GOAL>IsOpen (s / t)
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s t : Set G<VAR>ht : IsOpen t<GOAL>IsOpen (⋃ a ∈ s, (fun x => a / x) '' t)
<VAR>u v : ℂ<GOAL>∫ (x : ℝ) in 0 ..1, ↑x ^ (v - 1) * (1 - ↑x) ^ (u - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)
<VAR>u v : ℂ<VAR>this : ∫ (x : ℝ) in 0 ..1, ↑(-1 * x + 1) ^ (u - 1) * (1 - ↑(-1 * x + 1)) ^ (v - 1) = (-1)⁻¹ • ∫ (x : ℝ) in -1 * 0 + 1 ..-1 * 1 + 1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)<GOAL>∫ (x : ℝ) in 0 ..1, ↑x ^ (v - 1) * (1 - ↑x) ^ (u - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)
<VAR>u v : ℂ<VAR>this : ∫ (x : ℝ) in 0 ..1, ↑(-1 * x + 1) ^ (u - 1) * (1 - ↑(-1 * x + 1)) ^ (v - 1) = ∫ (x : ℝ) in -1 * 1 + 1 ..-1 * 0 + 1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)<GOAL>∫ (x : ℝ) in 0 ..1, ↑x ^ (v - 1) * (1 - ↑x) ^ (u - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)
<VAR>u v : ℂ<VAR>this : ∫ (x : ℝ) in 0 ..1, (-↑x + 1) ^ (u - 1) * ↑x ^ (v - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)<GOAL>∫ (x : ℝ) in 0 ..1, ↑x ^ (v - 1) * (1 - ↑x) ^ (u - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)
<VAR>u v : ℂ<VAR>this : ∫ (x : ℝ) in 0 ..1, ↑x ^ (v - 1) * (1 - ↑x) ^ (u - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)<GOAL>∫ (x : ℝ) in 0 ..1, ↑x ^ (v - 1) * (1 - ↑x) ^ (u - 1) = ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R M₁<VAR>inst✝² : StrongRankCondition R<VAR>inst✝¹ : Finite R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>t : Finset M<VAR>h : finrank R M < t.card<GOAL>∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∃ x ∈ t, f x ≠ 0
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R M₁<VAR>inst✝² : StrongRankCondition R<VAR>inst✝¹ : Finite R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>t : Finset M<VAR>h : finrank R M < t.card<VAR>g : { x // x ∈ t } → R<VAR>sum : ∑ i : { x // x ∈ t }, g i • ↑i = 0<VAR>z : { x // x ∈ t }<VAR>nonzero : g z ≠ 0<GOAL>∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∃ x ∈ t, f x ≠ 0
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R M₁<VAR>inst✝² : StrongRankCondition R<VAR>inst✝¹ : Finite R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>t : Finset M<VAR>h : finrank R M < t.card<VAR>g : { x // x ∈ t } → R<VAR>sum : ∑ i : { x // x ∈ t }, g i • ↑i = 0<VAR>z : { x // x ∈ t }<VAR>nonzero : g z ≠ 0<GOAL>∑ e ∈ t, Function.extend Subtype.val g 0 e • e = 0
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R M₁<VAR>inst✝² : StrongRankCondition R<VAR>inst✝¹ : Finite R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>t : Finset M<VAR>h : finrank R M < t.card<VAR>g : { x // x ∈ t } → R<VAR>sum : ∑ i : { x // x ∈ t }, g i • ↑i = 0<VAR>z : { x // x ∈ t }<VAR>nonzero : g z ≠ 0<GOAL>∑ i : ↑↑t, Function.extend Subtype.val g 0 ↑i • ↑i = 0
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R M₁<VAR>inst✝² : StrongRankCondition R<VAR>inst✝¹ : Finite R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>t : Finset M<VAR>h : finrank R M < t.card<VAR>g : { x // x ∈ t } → R<VAR>sum : ∑ i : { x // x ∈ t }, g i • ↑i = 0<VAR>z : { x // x ∈ t }<VAR>nonzero : g z ≠ 0<VAR>x✝ : ↑↑t<VAR>a✝ : x✝ ∈ Finset.univ<GOAL>Function.extend Subtype.val g 0 ↑x✝ = g x✝
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>r : R<VAR>hb : 1 < b<VAR>hr : 0 < r<GOAL>↑b ^ log b r ≤ r
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>r : R<VAR>hb : 1 < b<VAR>hr : 0 < r<VAR>hr1 : 1 ≤ r<GOAL>↑b ^ log b r ≤ r
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>r : R<VAR>hb : 1 < b<VAR>hr : 0 < r<VAR>hr1 : r ≤ 1<GOAL>↑b ^ log b r ≤ r
<VAR>G : Type u_1<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : MeasurableSpace G<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : PolishSpace G<VAR>ν : Measure G<VAR>Γ : Subgroup G<VAR>inst✝⁴ : Countable ↥Γ<VAR>inst✝³ : T2Space (G ⧸ Γ)<VAR>inst✝² : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ<VAR>inst✝ : ν.IsMulLeftInvariant<VAR>hasFun : HasFundamentalDomain (↥Γ.op) G ν<VAR>g : G<VAR>A : Set (G ⧸ Γ)<VAR>hA : MeasurableSet A<GOAL>μ ((fun x => g • x) ⁻¹' A) = μ A
<VAR>G : Type u_1<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : MeasurableSpace G<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : PolishSpace G<VAR>ν : Measure G<VAR>Γ : Subgroup G<VAR>inst✝⁴ : Countable ↥Γ<VAR>inst✝³ : T2Space (G ⧸ Γ)<VAR>inst✝² : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ<VAR>inst✝ : ν.IsMulLeftInvariant<VAR>hasFun : HasFundamentalDomain (↥Γ.op) G ν<VAR>g : G<VAR>A : Set (G ⧸ Γ)<VAR>hA : MeasurableSet A<VAR>meas_π : Measurable QuotientGroup.mk<GOAL>μ ((fun x => g • x) ⁻¹' A) = μ A
<VAR>G : Type u_1<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : MeasurableSpace G<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : PolishSpace G<VAR>ν : Measure G<VAR>Γ : Subgroup G<VAR>inst✝⁴ : Countable ↥Γ<VAR>inst✝³ : T2Space (G ⧸ Γ)<VAR>inst✝² : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ<VAR>inst✝ : ν.IsMulLeftInvariant<VAR>hasFun : HasFundamentalDomain (↥Γ.op) G ν<VAR>g : G<VAR>A : Set (G ⧸ Γ)<VAR>hA : MeasurableSet A<VAR>meas_π : Measurable QuotientGroup.mk<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν<GOAL>μ ((fun x => g • x) ⁻¹' A) = μ A
<VAR>G : Type u_1<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : MeasurableSpace G<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : PolishSpace G<VAR>ν : Measure G<VAR>Γ : Subgroup G<VAR>inst✝⁴ : Countable ↥Γ<VAR>inst✝³ : T2Space (G ⧸ Γ)<VAR>inst✝² : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ<VAR>inst✝ : ν.IsMulLeftInvariant<VAR>hasFun : HasFundamentalDomain (↥Γ.op) G ν<VAR>g : G<VAR>A : Set (G ⧸ Γ)<VAR>hA : MeasurableSet A<VAR>meas_π : Measurable QuotientGroup.mk<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν<VAR>h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν<GOAL>μ ((fun x => g • x) ⁻¹' A) = μ A
<VAR>G : Type u_1<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : MeasurableSpace G<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : PolishSpace G<VAR>ν : Measure G<VAR>Γ : Subgroup G<VAR>inst✝⁴ : Countable ↥Γ<VAR>inst✝³ : T2Space (G ⧸ Γ)<VAR>inst✝² : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ<VAR>inst✝ : ν.IsMulLeftInvariant<VAR>hasFun : HasFundamentalDomain (↥Γ.op) G ν<VAR>g : G<VAR>A : Set (G ⧸ Γ)<VAR>hA : MeasurableSet A<VAR>meas_π : Measurable QuotientGroup.mk<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν<VAR>h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν<GOAL>ν (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' ((fun x => g • x) ⁻¹' A) ∩ 𝓕) = ν (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' A ∩ g • 𝓕)
<VAR>G : Type u_1<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : MeasurableSpace G<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : PolishSpace G<VAR>ν : Measure G<VAR>Γ : Subgroup G<VAR>inst✝⁴ : Countable ↥Γ<VAR>inst✝³ : T2Space (G ⧸ Γ)<VAR>inst✝² : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ<VAR>inst✝ : ν.IsMulLeftInvariant<VAR>hasFun : HasFundamentalDomain (↥Γ.op) G ν<VAR>g : G<VAR>A : Set (G ⧸ Γ)<VAR>hA : MeasurableSet A<VAR>meas_π : Measurable QuotientGroup.mk<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν<VAR>h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν<VAR>π_preA : Set G := QuotientGroup.mk ⁻¹' A<VAR>this✝ : QuotientGroup.mk ⁻¹' ((fun x => g • x) ⁻¹' A) = (fun x => g * x) ⁻¹' π_preA<VAR>this : ν ((fun x => g * x) ⁻¹' π_preA ∩ 𝓕) = ν (π_preA ∩ (fun x => g⁻¹ * x) ⁻¹' 𝓕)<GOAL>ν ((fun x => g * x) ⁻¹' π_preA ∩ 𝓕) = ν (π_preA ∩ g • 𝓕)
<VAR>G : Type u_1<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : MeasurableSpace G<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : PolishSpace G<VAR>ν : Measure G<VAR>Γ : Subgroup G<VAR>inst✝⁴ : Countable ↥Γ<VAR>inst✝³ : T2Space (G ⧸ Γ)<VAR>inst✝² : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ<VAR>inst✝ : ν.IsMulLeftInvariant<VAR>hasFun : HasFundamentalDomain (↥Γ.op) G ν<VAR>g : G<VAR>A : Set (G ⧸ Γ)<VAR>hA : MeasurableSet A<VAR>meas_π : Measurable QuotientGroup.mk<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν<VAR>h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν<VAR>π_preA : Set G := QuotientGroup.mk ⁻¹' A<VAR>this✝ : QuotientGroup.mk ⁻¹' ((fun x => g • x) ⁻¹' A) = (fun x => g * x) ⁻¹' π_preA<VAR>this : ν ((fun x => g * x) ⁻¹' π_preA ∩ 𝓕) = ν (π_preA ∩ (fun x => g⁻¹ * x) ⁻¹' 𝓕)<GOAL>ν (π_preA ∩ (fun x => g⁻¹ * x) ⁻¹' 𝓕) = ν (π_preA ∩ (fun x => g⁻¹ • x) ⁻¹' 𝓕)
<VAR>α : Type u<VAR>α' : Type u_1<VAR>β : Type v<VAR>β' : Type u_2<VAR>γ : Type u_3<VAR>φ : Type u_4<VAR>inst✝⁵ : OmegaCompletePartialOrder α<VAR>inst✝⁴ : OmegaCompletePartialOrder β<VAR>inst✝³ : OmegaCompletePartialOrder γ<VAR>inst✝² : OmegaCompletePartialOrder φ<VAR>inst✝¹ : OmegaCompletePartialOrder α'<VAR>inst✝ : OmegaCompletePartialOrder β'<VAR>c₀ : Chain (α →𝒄 β)<VAR>c₁ : Chain α<GOAL>(ωSup c₀) (ωSup c₁) = Prod.apply (ωSup (c₀.zip c₁))
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>s : ℂ<VAR>hs : 0 < s.re<GOAL>HasMellin ((Ioc 0 1).indicator fun x => 1) s (1 / s)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>aux1 : -1 < (s - 1).re<GOAL>HasMellin ((Ioc 0 1).indicator fun x => 1) s (1 / s)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>aux1 : -1 < (s - 1).re<VAR>aux2 : s ≠ 0<GOAL>HasMellin ((Ioc 0 1).indicator fun x => 1) s (1 / s)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>aux1 : -1 < (s - 1).re<VAR>aux2 : s ≠ 0<VAR>aux3 : MeasurableSet (Ioc 0 1)<GOAL>HasMellin ((Ioc 0 1).indicator fun x => 1) s (1 / s)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>aux1 : -1 < (s - 1).re<VAR>aux2 : s ≠ 0<VAR>aux3 : MeasurableSet (Ioc 0 1)<GOAL>Integrable (fun a => ↑a ^ (s - 1)) (volume.restrict (Ioc 0 1)) ∧ ∫ (a : ℝ) in Ioc 0 1, ↑a ^ (s - 1) ∂volume = 1 / s
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>aux1 : -1 < (s - 1).re<VAR>aux2 : s ≠ 0<VAR>aux3 : MeasurableSet (Ioc 0 1)<GOAL>IntervalIntegrable (fun a => ↑a ^ (s - 1)) volume 0 1 ∧ ∫ (a : ℝ) in Ioc 0 1, ↑a ^ (s - 1) ∂volume = 1 / s
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>aux1 : -1 < (s - 1).re<VAR>aux2 : s ≠ 0<VAR>aux3 : MeasurableSet (Ioc 0 1)<GOAL>∫ (a : ℝ) in Ioc 0 1, ↑a ^ (s - 1) ∂volume = 1 / s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Preorder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>a ∈ Ioc a b ↔ False
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>H : LieSubalgebra R L<VAR>α χ : ↥H → R<VAR>p q : ℤ<VAR>inst✝ : LieAlgebra.IsNilpotent R ↥H<VAR>hp : weightSpace M (p • α + χ) = ⊥<VAR>x : L<VAR>hx : x ∈ rootSpace H (-α)<VAR>y : M<VAR>hy : y ∈ weightSpaceChain M α χ p q<GOAL>⁅x, y⁆ ∈ weightSpaceChain M α χ p q
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>H : LieSubalgebra R L<VAR>α χ : ↥H → R<VAR>p q : ℤ<VAR>inst✝ : LieAlgebra.IsNilpotent R ↥H<VAR>x : L<VAR>hx : x ∈ rootSpace H (-α)<VAR>y : M<VAR>hy : y ∈ weightSpaceChain M α χ p q<VAR>hp : weightSpace M (-p • -α + χ) = ⊥<GOAL>⁅x, y⁆ ∈ weightSpaceChain M α χ p q
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>H : LieSubalgebra R L<VAR>α χ : ↥H → R<VAR>p q : ℤ<VAR>inst✝ : LieAlgebra.IsNilpotent R ↥H<VAR>x : L<VAR>hx : x ∈ rootSpace H (-α)<VAR>y : M<VAR>hy : y ∈ weightSpaceChain M (-α) χ (-q) (-p)<VAR>hp : weightSpace M (-p • -α + χ) = ⊥<GOAL>⁅x, y⁆ ∈ weightSpaceChain M (-α) χ (-q) (-p)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F G : (Cᵒᵖ ⥤ D)ᵒᵖ<VAR>η : F ⟶ G<GOAL>η ≫ (unop G).rightOpLeftOpIso.hom.op = (unop F).rightOpLeftOpIso.hom.op ≫ (NatTrans.leftOp (NatTrans.rightOp η.unop)).op