ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>n : ℕ<VAR>hζ✝ : (primitiveRoots n K).Nonempty<VAR>hn✝ : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>this✝ : Fact (Irreducible (X ^ n - C a)) := { out := H }<VAR>this : Algebra K K[n√a] := inferInstance<VAR>hn : 0 < n<VAR>hn' : ¬n = 1<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ n<GOAL>(X ^ n - C a).Separable
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>n : ℕ<VAR>hζ✝ : (primitiveRoots n K).Nonempty<VAR>hn✝ : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>this✝ : Fact (Irreducible (X ^ n - C a)) := { out := H }<VAR>this : Algebra K K[n√a] := inferInstance<VAR>hn : 0 < n<VAR>hn' : ¬n = 1<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ n<GOAL>∀ x ∈ Finset.range n, ∀ y ∈ Finset.range n, (algebraMap K K[n√a]) ζ ^ x * root (X ^ n - C a) = (algebraMap K K[n√a]) ζ ^ y * root (X ^ n - C a) → x = y
<VAR>M : Type u_1<VAR>inst✝³ : Monoid M<VAR>R : Type u_2<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : NatPowAssoc R<VAR>n : ℤ<GOAL>↑(n ^ 0) = ↑n ^ 0
<VAR>M : Type u_1<VAR>inst✝³ : Monoid M<VAR>R : Type u_2<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : NatPowAssoc R<VAR>n : ℤ<VAR>m : ℕ<GOAL>↑(n ^ (m + 1)) = ↑n ^ (m + 1)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<GOAL>Submodule.map reverse (LinearMap.range (ι Q)) = LinearMap.range (ι Q)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<GOAL>Submodule.map (↑(MulOpposite.opLinearEquiv R).symm ∘ₗ ↑(MulOpposite.opLinearEquiv R)) (LinearMap.range (ι Q)) = LinearMap.range (ι Q)
<VAR>x : PartENat<VAR>x✝ : Decidable x.Dom<GOAL>↑x.toWithTop = x
<VAR>α : Type u_1<VAR>t : Ordnode α<VAR>hl : t.Sized<VAR>C : Ordnode α → Prop<VAR>H0 : C nil<VAR>H1 : ∀ (l : Ordnode α) (x : α) (r : Ordnode α), C l → C r → C (l.node' x r)<GOAL>C t
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁸ : NontriviallyNormedField R<VAR>inst✝⁷ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁶ : (x : B) → Module R (E x)<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace R F<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹ : (x : B) → TopologicalSpace (E x)<VAR>inst✝ : FiberBundle F E<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<VAR>i j k : ι<VAR>x : B<VAR>hx : x ∈ Z.baseSet i ∩ Z.baseSet j ∩ Z.baseSet k<VAR>v : F<GOAL>((Z.coordChange j k x).comp (Z.coordChange i j x)) v = (Z.coordChange i k x) v
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>J : Type u<VAR>inst✝² : Category.{v, u} J<VAR>D : J ⥤ T.Algebra<VAR>c : Cocone (D ⋙ T.forget)<VAR>t : IsColimit c<VAR>inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor<VAR>inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>A B : J<VAR>f : A ⟶ B<GOAL>(D.map f).f ≫ c.ι.app B = c.ι.app A ≫ 𝟙 c.pt
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>J : Type u<VAR>inst✝² : Category.{v, u} J<VAR>D : J ⥤ T.Algebra<VAR>c : Cocone (D ⋙ T.forget)<VAR>t : IsColimit c<VAR>inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor<VAR>inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor<VAR>A B : J<VAR>f : A ⟶ B<GOAL>(D.map f).f ≫ c.ι.app B = c.ι.app A
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharP R p<GOAL>(↑p).coeff 1 = 1
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>p : K[X]<VAR>m : p.Monic<VAR>hsplit : Splits (RingHom.id K) p<GOAL>p = (Multiset.map (fun a => X - C a) p.roots).prod
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>p : K[X]<VAR>m : p.Monic<VAR>hsplit : Splits (RingHom.id K) p<GOAL>(Multiset.map (fun a => X - C a) p.roots).prod = C p.leadingCoeff * (Multiset.map (fun a => X - C a) p.roots).prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : CommGroup G<VAR>a✝ b✝ c✝ d a b c : G<GOAL>a / b * (c / a) = c / b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : CommGroup G<VAR>a✝ b✝ c✝ d a b c : G<GOAL>c / a * (a / b) = c / b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteDistribLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<VAR>a : α<GOAL>a ⊔ liminf u f = liminf (fun x => a ⊔ u x) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteDistribLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<VAR>a : α<GOAL>a ⊔ ⨆ s ∈ f, ⨅ a ∈ s, u a = ⨆ s ∈ f, ⨅ a_1 ∈ s, a ⊔ u a_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteDistribLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<VAR>a : α<GOAL>⨆ i ∈ f, (⨅ a ∈ i, u a) ⊔ a = ⨆ s ∈ f, ⨅ a_1 ∈ s, a ⊔ u a_1
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>a b : M<GOAL>(ι Q) a * (ι Q) b * (ι Q) a = (ι Q) (QuadraticMap.polar (⇑Q) a b • a - Q a • b)
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i✝ : K →+* L<VAR>p : K[X]<VAR>i : K →+* L<VAR>p_ne_zero : map i p ≠ 0<VAR>hsplit : Splits i p<GOAL>(map i p).degree = ↑(Multiset.card (map i p).roots)
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>χ : LieCharacter R L<VAR>x y : L<GOAL>χ ⁅x, y⁆ = 0
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β ↑i<VAR>i✝ : ι<VAR>inst✝ : Fintype ι<VAR>i : ι<VAR>m : β i<VAR>i' : ι<GOAL>(equivFunOnFintype.symm (Pi.single i m)) i' = (single i m) i'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : LinearOrder β<VAR>inst✝³ : OrderTopology α<VAR>inst✝² : OrderTopology β<VAR>inst✝¹ : DenselyOrdered α<VAR>inst✝ : FirstCountableTopology α<VAR>x y : α<VAR>hy : x < y<GOAL>∃ u, StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Ioo x y) ∧ Tendsto u atTop (𝓝 x)
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝⁹ : Fact (1 ≤ p)<VAR>inst✝⁸ : Fintype ι<VAR>inst✝⁷ : Semiring 𝕜<VAR>inst✝⁶ : (i : ι) → SeminormedAddCommGroup (α i)<VAR>inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β i)<VAR>inst✝⁴ : (i : ι) → Module 𝕜 (α i)<VAR>inst✝³ : (i : ι) → Module 𝕜 (β i)<VAR>c : 𝕜<VAR>ι' : Type u_5<VAR>inst✝² : Fintype ι'<VAR>E : Type u_6<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>e : ι ≃ ι'<VAR>z : PiLp p fun x => E<GOAL>(LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e).symm z = (LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e.symm) z
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝⁹ : Fact (1 ≤ p)<VAR>inst✝⁸ : Fintype ι<VAR>inst✝⁷ : Semiring 𝕜<VAR>inst✝⁶ : (i : ι) → SeminormedAddCommGroup (α i)<VAR>inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β i)<VAR>inst✝⁴ : (i : ι) → Module 𝕜 (α i)<VAR>inst✝³ : (i : ι) → Module 𝕜 (β i)<VAR>c : 𝕜<VAR>ι' : Type u_5<VAR>inst✝² : Fintype ι'<VAR>E : Type u_6<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>e : ι ≃ ι'<VAR>z : PiLp p fun x => E<GOAL>(LinearEquiv.piCongrLeft' 𝕜 (fun x => E) e).symm z = (LinearEquiv.piCongrLeft' 𝕜 (fun x => E) e.symm) z
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝⁹ : Fact (1 ≤ p)<VAR>inst✝⁸ : Fintype ι<VAR>inst✝⁷ : Semiring 𝕜<VAR>inst✝⁶ : (i : ι) → SeminormedAddCommGroup (α i)<VAR>inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β i)<VAR>inst✝⁴ : (i : ι) → Module 𝕜 (α i)<VAR>inst✝³ : (i : ι) → Module 𝕜 (β i)<VAR>c : 𝕜<VAR>ι' : Type u_5<VAR>inst✝² : Fintype ι'<VAR>E : Type u_6<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>e : ι ≃ ι'<VAR>z : PiLp p fun x => E<VAR>x✝ : ι<GOAL>(LinearEquiv.piCongrLeft' 𝕜 (fun x => E) e).symm z x✝ = (LinearEquiv.piCongrLeft' 𝕜 (fun x => E) e.symm) z x✝
<VAR>R✝ : Type u<VAR>inst✝³ : CommRing R✝<VAR>R' : Type v<VAR>inst✝² : CommMonoid R'<VAR>N : ℕ<VAR>inst✝¹ : NeZero N<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>e : AddChar (ZMod N) R<VAR>he : ¬e.IsPrimitive<GOAL>∃ d, d ∣ N ∧ d < N ∧ e.mulShift ↑d = 1
<VAR>R✝ : Type u<VAR>inst✝³ : CommRing R✝<VAR>R' : Type v<VAR>inst✝² : CommMonoid R'<VAR>N : ℕ<VAR>inst✝¹ : NeZero N<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>e : AddChar (ZMod N) R<VAR>he : ∃ x, ∃ (_ : x ≠ 0), e.mulShift x = 1<GOAL>∃ d, d ∣ N ∧ d < N ∧ e.mulShift ↑d = 1
<VAR>R✝ : Type u<VAR>inst✝³ : CommRing R✝<VAR>R' : Type v<VAR>inst✝² : CommMonoid R'<VAR>N : ℕ<VAR>inst✝¹ : NeZero N<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>e : AddChar (ZMod N) R<VAR>b : ZMod N<VAR>hb_ne : b ≠ 0<VAR>hb : e.mulShift b = 1<GOAL>∃ d, d ∣ N ∧ d < N ∧ e.mulShift ↑d = 1
<VAR>R✝ : Type u<VAR>inst✝³ : CommRing R✝<VAR>R' : Type v<VAR>inst✝² : CommMonoid R'<VAR>N : ℕ<VAR>inst✝¹ : NeZero N<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>e : AddChar (ZMod N) R<VAR>d : ℕ<VAR>hd : d ∣ N<VAR>u : ZMod N<VAR>hu : IsUnit u<VAR>hb_ne : u * ↑d ≠ 0<VAR>hb : e.mulShift (u * ↑d) = 1<GOAL>∃ d, d ∣ N ∧ d < N ∧ e.mulShift ↑d = 1
<VAR>R✝ : Type u<VAR>inst✝³ : CommRing R✝<VAR>R' : Type v<VAR>inst✝² : CommMonoid R'<VAR>N : ℕ<VAR>inst✝¹ : NeZero N<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>e : AddChar (ZMod N) R<VAR>d : ℕ<VAR>hd : d ∣ N<VAR>u : ZMod N<VAR>hu : IsUnit u<VAR>hb_ne : u * ↑d ≠ 0<VAR>hb : e.mulShift (u * ↑d) = 1<GOAL>d ≠ N
<VAR>R✝ : Type u<VAR>inst✝³ : CommRing R✝<VAR>R' : Type v<VAR>inst✝² : CommMonoid R'<VAR>N : ℕ<VAR>inst✝¹ : NeZero N<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>e : AddChar (ZMod N) R<VAR>d : ℕ<VAR>hd : d ∣ N<VAR>u : ZMod N<VAR>hu : IsUnit u<VAR>hb_ne : u * ↑d ≠ 0<VAR>hb : e.mulShift (u * ↑d) = 1<GOAL>e.mulShift ↑d = 1
<VAR>a b c p q : ℚ<GOAL>p < q ↔ p.num * ↑q.den < q.num * ↑p.den
<VAR>a b c p q : ℚ<GOAL>p.num * ↑q.den ≤ q.num * ↑p.den ∧ p ≠ q ↔ p.num * ↑q.den < q.num * ↑p.den
<VAR>a b c p q : ℚ<GOAL>p ≠ q ↔ p.num * ↑q.den ≠ q.num * ↑p.den
<VAR>n : ℕ<VAR>hn : 2 ≤ n<GOAL>fib n < fib (n + 1)
<VAR>n : ℕ<VAR>hn : 2 ≤ 2 + n<GOAL>fib (2 + n) < fib (2 + n + 1)
<VAR>n : ℕ<VAR>hn : 2 ≤ 2 + n<GOAL>0 < n + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set α)<GOAL>UniformContinuous ((⋃₀ 𝔖).restrict ∘ ⇑(toFun 𝔖))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set α)<GOAL>∀ (i : ↑(⋃₀ 𝔖)), UniformContinuous fun x => ((⋃₀ 𝔖).restrict ∘ ⇑(toFun 𝔖)) x i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>x : α<VAR>hx : x ∈ ⋃₀ 𝔖<GOAL>UniformContinuous fun x_1 => ((⋃₀ 𝔖).restrict ∘ ⇑(toFun 𝔖)) x_1 ⟨x, hx⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s✝ s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>x : α<VAR>hx : x ∈ ⋃₀ 𝔖<VAR>s : Set α<VAR>hs : s ∈ 𝔖<VAR>hxs : x ∈ s<GOAL>UniformContinuous fun x_1 => ((⋃₀ 𝔖).restrict ∘ ⇑(toFun 𝔖)) x_1 ⟨x, hx⟩
<GOAL>StableUnderBaseChange fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f
<GOAL>∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S] [inst_4 : Algebra R T], Function.Surjective ⇑(algebraMap R T) → Function.Surjective ⇑includeLeftRingHom
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Multiset α<GOAL>(Finset.Icc s t).card = ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Group G<VAR>inst✝ : Fintype G<VAR>x : G<VAR>n : ℕ<VAR>s : Submonoid G<VAR>hs : (↑s).Finite<VAR>hx : x ∈ s<GOAL>orderOf x ≤ Nat.card ↥s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Group G<VAR>inst✝ : Fintype G<VAR>x : G<VAR>n : ℕ<VAR>s : Submonoid G<VAR>hs : (↑s).Finite<VAR>hx : x ∈ s<GOAL>Nat.card ↥(powers x) ≤ Nat.card ↥s
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_1<VAR>I : Set ι<VAR>s : ι → Set α<VAR>H : ∀ i ∈ I, IsOpen (s i)<GOAL>∃ T ⊆ I, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i ∈ I, s i
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_1<VAR>I : Set ι<VAR>s : ι → Set α<VAR>H : ∀ i ∈ I, IsOpen (s i)<GOAL>∃ s_1, (Subtype.val '' s_1).Countable ∧ ⋃ y ∈ s_1, s ↑y = ⋃ i ∈ I, s i
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_1<VAR>I : Set ι<VAR>s : ι → Set α<VAR>H : ∀ i ∈ I, IsOpen (s i)<VAR>T : Set ↑I<VAR>hTc : T.Countable<VAR>hU : ⋃ i ∈ T, s ↑i = ⋃ i, s ↑i<GOAL>∃ s_1, (Subtype.val '' s_1).Countable ∧ ⋃ y ∈ s_1, s ↑y = ⋃ i ∈ I, s i
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>U : Set E<VAR>hU' : U ∈ p.basisSets<GOAL>∃ V ∈ p.basisSets, V ⊆ (fun x => -x) ⁻¹' U
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>U : Set E<VAR>hU' : U ∈ p.basisSets<VAR>s : Finset ι<VAR>r : ℝ<VAR>left✝ : 0 < r<VAR>hU : U = (s.sup p).ball 0 r<GOAL>∃ V ∈ p.basisSets, V ⊆ (fun x => -x) ⁻¹' U
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>U : Set E<VAR>hU' : U ∈ p.basisSets<VAR>s : Finset ι<VAR>r : ℝ<VAR>left✝ : 0 < r<VAR>hU : U = (s.sup p).ball 0 r<GOAL>∃ V ∈ p.basisSets, V ⊆ (s.sup p).ball 0 r
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>a : A<VAR>x✝ : C<GOAL>(eqToHom ⋯).app x✝ ≫ (shiftFunctorAdd C a 0).hom.app x✝ = 𝟙 (((shiftMonoidalFunctor C A).obj { as := a }).obj x✝) ≫ (shiftMonoidalFunctor C A).ε.app (((shiftMonoidalFunctor C A).obj { as := a }).obj x✝)
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>a : A<VAR>x✝ : C<GOAL>eqToHom ⋯ ≫ (shiftFunctorAdd C a 0).hom.app x✝ = eqToHom ⋯ ≫ ((shiftMonoidalFunctor C A).μIso { as := a } (𝟙_ (Discrete A))).inv.app x✝
<VAR>α : Type u_1<GOAL>Filter.map Real.toNNReal atTop = atTop
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<GOAL>(-o).volumeForm = -o.volumeForm
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o<GOAL>(-o).volumeForm = -o.volumeForm
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o<VAR>h₁ : e.toBasis.orientation = o<GOAL>(-o).volumeForm = -o.volumeForm
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o<VAR>h₁ : e.toBasis.orientation = o<VAR>h₂ : e.toBasis.orientation ≠ -o<GOAL>(-o).volumeForm = -o.volumeForm
<VAR>R : Type u_1<VAR>inst✝²⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝²⁶ : AddCommMonoid M<VAR>inst✝²⁵ : AddCommMonoid M'<VAR>inst✝²⁴ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝²³ : CommSemiring A<VAR>inst✝²² : Algebra R A<VAR>inst✝²¹ : Module A M'<VAR>inst✝²⁰ : IsLocalization S A<VAR>inst✝¹⁹ : Module R M<VAR>inst✝¹⁸ : Module R M'<VAR>inst✝¹⁷ : Module R M''<VAR>inst✝¹⁶ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝¹ : M →ₗ[R] M''<VAR>inst✝¹⁵ : IsLocalizedModule S f<VAR>N : Type ?u.1089083<VAR>N' : Type ?u.1089086<VAR>inst✝¹⁴ : AddCommGroup N<VAR>inst✝¹³ : AddCommGroup N'<VAR>inst✝¹² : Module R N<VAR>inst✝¹¹ : Module R N'<VAR>g✝ : N →ₗ[R] N'<VAR>inst✝¹⁰ : IsLocalizedModule S g✝<VAR>M₀ : Type u_6<VAR>M₀' : Type ?u.1091157<VAR>inst✝⁹ : AddCommGroup M₀<VAR>inst✝⁸ : AddCommGroup M₀'<VAR>inst✝⁷ : Module R M₀<VAR>inst✝⁶ : Module R M₀'<VAR>f₀ : M₀ →ₗ[R] M₀'<VAR>inst✝⁵ : IsLocalizedModule S f₀<VAR>M₁ : Type u_7<VAR>M₁' : Type ?u.1093228<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : AddCommGroup M₁'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R M₁'<VAR>f₁ : M₁ →ₗ[R] M₁'<VAR>inst✝ : IsLocalizedModule S f₁<VAR>g : M₀ →ₗ[R] M₁<VAR>m : M₀<VAR>s : ↥S<GOAL>((map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m s) = LocalizedModule.mk (g m) s
<VAR>R : Type u_1<VAR>inst✝²⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝²⁶ : AddCommMonoid M<VAR>inst✝²⁵ : AddCommMonoid M'<VAR>inst✝²⁴ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝²³ : CommSemiring A<VAR>inst✝²² : Algebra R A<VAR>inst✝²¹ : Module A M'<VAR>inst✝²⁰ : IsLocalization S A<VAR>inst✝¹⁹ : Module R M<VAR>inst✝¹⁸ : Module R M'<VAR>inst✝¹⁷ : Module R M''<VAR>inst✝¹⁶ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝¹ : M →ₗ[R] M''<VAR>inst✝¹⁵ : IsLocalizedModule S f<VAR>N : Type ?u.1089083<VAR>N' : Type ?u.1089086<VAR>inst✝¹⁴ : AddCommGroup N<VAR>inst✝¹³ : AddCommGroup N'<VAR>inst✝¹² : Module R N<VAR>inst✝¹¹ : Module R N'<VAR>g✝ : N →ₗ[R] N'<VAR>inst✝¹⁰ : IsLocalizedModule S g✝<VAR>M₀ : Type u_6<VAR>M₀' : Type ?u.1091157<VAR>inst✝⁹ : AddCommGroup M₀<VAR>inst✝⁸ : AddCommGroup M₀'<VAR>inst✝⁷ : Module R M₀<VAR>inst✝⁶ : Module R M₀'<VAR>f₀ : M₀ →ₗ[R] M₀'<VAR>inst✝⁵ : IsLocalizedModule S f₀<VAR>M₁ : Type u_7<VAR>M₁' : Type ?u.1093228<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : AddCommGroup M₁'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R M₁'<VAR>f₁ : M₁ →ₗ[R] M₁'<VAR>inst✝ : IsLocalizedModule S f₁<VAR>g : M₀ →ₗ[R] M₁<VAR>m : M₀<VAR>s : ↥S<VAR>this : ↑⋯.unit⁻¹ ((mkLinearMap S M₁) (g m)) = (iso S (mkLinearMap S M₁)) (LocalizedModule.mk (g m) s)<GOAL>((map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m s) = LocalizedModule.mk (g m) s
<VAR>R : Type u_1<VAR>inst✝²⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝²⁶ : AddCommMonoid M<VAR>inst✝²⁵ : AddCommMonoid M'<VAR>inst✝²⁴ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝²³ : CommSemiring A<VAR>inst✝²² : Algebra R A<VAR>inst✝²¹ : Module A M'<VAR>inst✝²⁰ : IsLocalization S A<VAR>inst✝¹⁹ : Module R M<VAR>inst✝¹⁸ : Module R M'<VAR>inst✝¹⁷ : Module R M''<VAR>inst✝¹⁶ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝¹ : M →ₗ[R] M''<VAR>inst✝¹⁵ : IsLocalizedModule S f<VAR>N : Type ?u.1089083<VAR>N' : Type ?u.1089086<VAR>inst✝¹⁴ : AddCommGroup N<VAR>inst✝¹³ : AddCommGroup N'<VAR>inst✝¹² : Module R N<VAR>inst✝¹¹ : Module R N'<VAR>g✝ : N →ₗ[R] N'<VAR>inst✝¹⁰ : IsLocalizedModule S g✝<VAR>M₀ : Type u_6<VAR>M₀' : Type ?u.1091157<VAR>inst✝⁹ : AddCommGroup M₀<VAR>inst✝⁸ : AddCommGroup M₀'<VAR>inst✝⁷ : Module R M₀<VAR>inst✝⁶ : Module R M₀'<VAR>f₀ : M₀ →ₗ[R] M₀'<VAR>inst✝⁵ : IsLocalizedModule S f₀<VAR>M₁ : Type u_7<VAR>M₁' : Type ?u.1093228<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : AddCommGroup M₁'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R M₁'<VAR>f₁ : M₁ →ₗ[R] M₁'<VAR>inst✝ : IsLocalizedModule S f₁<VAR>g : M₀ →ₗ[R] M₁<VAR>m : M₀<VAR>s : ↥S<VAR>this : ↑⋯.unit⁻¹ ((mkLinearMap S M₁) (g m)) = LocalizedModule.mk (g m) s<GOAL>((map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m s) = LocalizedModule.mk (g m) s
<VAR>a : ℝ<VAR>ha : a ∈ Icc 0 1<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => (1 / (↑n + ↑a) ^ s - 1 / (↑n + 1 - ↑a) ^ s) / 2) (hurwitzZetaOdd (↑a) s)
<VAR>a : ℝ<VAR>ha : a ∈ Icc 0 1<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>n : ℕ<GOAL>(1 / (↑n + ↑a) ^ s - 1 / (↑n + 1 - ↑a) ^ s) / 2 = (↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s - ↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s) / 2
<VAR>a : ℝ<VAR>ha : a ∈ Icc 0 1<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>n : ℕ<GOAL>∀ (b : ℝ), 0 ≤ b → ↑(SignType.sign (↑n + b)) / ↑|↑n + b| ^ s = 1 / (↑n + ↑b) ^ s
<VAR>a : ℝ<VAR>ha : a ∈ Icc 0 1<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>n : ℕ<VAR>b : ℝ<VAR>hb : 0 ≤ b<GOAL>↑(SignType.sign (↑n + b)) / ↑|↑n + b| ^ s = 1 / (↑n + ↑b) ^ s
<VAR>a : ℝ<VAR>ha : a ∈ Icc 0 1<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>n : ℕ<VAR>b : ℝ<VAR>hb : 0 ≤ b<GOAL>↑(SignType.sign (↑n + b)) / ↑(↑n + b) ^ s = 1 / ↑(↑n + b) ^ s
<VAR>a : ℝ<VAR>ha : a ∈ Icc 0 1<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>n : ℕ<VAR>b : ℝ<VAR>hb✝ : 0 ≤ b<VAR>hb : 0 < ↑n + b<GOAL>↑(SignType.sign (↑n + b)) / ↑(↑n + b) ^ s = 1 / ↑(↑n + b) ^ s
<VAR>a : ℝ<VAR>ha : a ∈ Icc 0 1<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>n : ℕ<VAR>b : ℝ<VAR>hb✝ : 0 ≤ b<VAR>hb : 0 = ↑n + b<GOAL>↑(SignType.sign (↑n + b)) / ↑(↑n + b) ^ s = 1 / ↑(↑n + b) ^ s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X₁ X₂ Y₁ Y₂ : ModuleCat R<VAR>f : X₁ ⟶ Y₁<VAR>g : X₂ ⟶ Y₂<GOAL>(f ⊗ g) ≫ (Y₁.braiding Y₂).hom = (X₁.braiding X₂).hom ≫ (g ⊗ f)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X₁ X₂ Y₁ Y₂ : ModuleCat R<VAR>f : X₁ ⟶ Y₁<VAR>g : X₂ ⟶ Y₂<GOAL>∀ (x : ↑X₁) (y : ↑X₂), ((f ⊗ g) ≫ (Y₁.braiding Y₂).hom) (x ⊗ₜ[R] y) = ((X₁.braiding X₂).hom ≫ (g ⊗ f)) (x ⊗ₜ[R] y)
<VAR>L : Language<VAR>α : Type w<VAR>V : Type w'<VAR>n : ℕ<VAR>S : Language.graph.Structure V<VAR>inst✝ : V ⊨ Theory.simpleGraph<VAR>x✝² : ℕ<VAR>x✝¹ : Language.graph.Functions x✝²<VAR>x✝ : Fin x✝² → V<GOAL>funMap x✝¹ x✝ = funMap x✝¹ x✝
<VAR>L : Language<VAR>α : Type w<VAR>V : Type w'<VAR>n : ℕ<VAR>S : Language.graph.Structure V<VAR>inst✝ : V ⊨ Theory.simpleGraph<VAR>x✝² : ℕ<VAR>x✝¹ : Language.graph.Relations x✝²<VAR>x✝ : Fin x✝² → V<GOAL>RelMap x✝¹ x✝ ↔ RelMap x✝¹ x✝
<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>Γ : Subgroup G<VAR>inst✝⁸ : Countable ↥Γ<VAR>inst✝⁷ : Γ.Normal<VAR>inst✝⁶ : T2Space (G ⧸ Γ)<VAR>inst✝⁵ : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝⁴ : ν.IsMulLeftInvariant<VAR>inst✝³ : ν.IsMulRightInvariant<VAR>inst✝² : SigmaFinite ν<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : SigmaFinite μ<VAR>s : Set G<VAR>fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν<VAR>V : Set (G ⧸ Γ)<VAR>meas_V : MeasurableSet V<VAR>neZeroV : μ V ≠ 0<VAR>hV : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s)<VAR>neTopV : μ V ≠ ⊤<GOAL>QuotientMeasureEqMeasurePreimage ν μ
<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>Γ : Subgroup G<VAR>inst✝⁸ : Countable ↥Γ<VAR>inst✝⁷ : Γ.Normal<VAR>inst✝⁶ : T2Space (G ⧸ Γ)<VAR>inst✝⁵ : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝⁴ : ν.IsMulLeftInvariant<VAR>inst✝³ : ν.IsMulRightInvariant<VAR>inst✝² : SigmaFinite ν<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : SigmaFinite μ<VAR>s : Set G<VAR>fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν<VAR>V : Set (G ⧸ Γ)<VAR>meas_V : MeasurableSet V<VAR>neZeroV : μ V ≠ 0<VAR>hV : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s)<VAR>neTopV : μ V ≠ ⊤<GOAL>μ = map (Quotient.mk (MulAction.orbitRel (↥Γ.op) G)) (ν.restrict s)