ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Γ✝ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁷ : PartialOrder Γ✝<VAR>inst✝⁶ : PartialOrder Γ'<VAR>inst✝⁵ : VAdd Γ✝ Γ'<VAR>inst✝⁴ : IsOrderedCancelVAdd Γ✝ Γ'<VAR>inst✝³ : AddCommMonoid V<VAR>Γ : Type u_5<VAR>inst✝² : LinearOrderedCancelAddCommMonoid Γ<VAR>inst✝¹ : Zero R<VAR>inst✝ : SMulWithZero R V<VAR>x : HahnSeries Γ R<VAR>y : HahnModule Γ R V<VAR>hx : ¬x = 0<VAR>hy : ¬(of R).symm y = 0<GOAL>∑ ij ∈ VAddAntidiagonal ⋯ ⋯ (⋯.min ⋯ + ⋯.min ⋯), x.coeff ij.1 • ((of R).symm y).coeff ij.2 = x.coeff (⋯.min ⋯) • ((of R).symm y).coeff (⋯.min ⋯)
<VAR>F : Type u_1<VAR>inst✝⁷ : Field F<VAR>E : Type u_2<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>L✝ : Type u_3<VAR>inst✝² : Field L✝<VAR>inst✝¹ : Algebra K L✝<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>hnfd : ¬FiniteDimensional F E<VAR>n : ℕ<VAR>L : IntermediateField F E<VAR>fin : FiniteDimensional F ↥L<VAR>hn : n < finrank F ↥L<GOAL>∃ L, FiniteDimensional F ↥L ∧ n + 1 < finrank F ↥L
<VAR>F : Type u_1<VAR>inst✝⁷ : Field F<VAR>E : Type u_2<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>L✝ : Type u_3<VAR>inst✝² : Field L✝<VAR>inst✝¹ : Algebra K L✝<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>hnfd : ¬FiniteDimensional F E<VAR>n : ℕ<VAR>L : IntermediateField F E<VAR>fin : FiniteDimensional F ↥L<VAR>hn : n < finrank F ↥L<VAR>x : E<VAR>hx : x ∉ L<GOAL>∃ L, FiniteDimensional F ↥L ∧ n + 1 < finrank F ↥L
<VAR>F : Type u_1<VAR>inst✝⁷ : Field F<VAR>E : Type u_2<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>L✝ : Type u_3<VAR>inst✝² : Field L✝<VAR>inst✝¹ : Algebra K L✝<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>hnfd : ¬FiniteDimensional F E<VAR>n : ℕ<VAR>L : IntermediateField F E<VAR>fin : FiniteDimensional F ↥L<VAR>hn : n < finrank F ↥L<VAR>x : E<VAR>hx : x ∉ L<VAR>L' : IntermediateField F E := L ⊔ F⟮x⟯<GOAL>∃ L, FiniteDimensional F ↥L ∧ n + 1 < finrank F ↥L
<VAR>F : Type u_1<VAR>inst✝⁷ : Field F<VAR>E : Type u_2<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>L✝ : Type u_3<VAR>inst✝² : Field L✝<VAR>inst✝¹ : Algebra K L✝<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>hnfd : ¬FiniteDimensional F E<VAR>n : ℕ<VAR>L : IntermediateField F E<VAR>fin : FiniteDimensional F ↥L<VAR>hn : n < finrank F ↥L<VAR>x : E<VAR>hx : x ∉ L<VAR>L' : IntermediateField F E := L ⊔ F⟮x⟯<VAR>this : FiniteDimensional F ↥F⟮x⟯<GOAL>∃ L, FiniteDimensional F ↥L ∧ n + 1 < finrank F ↥L
<VAR>F : Type u_1<VAR>inst✝⁷ : Field F<VAR>E : Type u_2<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>L✝ : Type u_3<VAR>inst✝² : Field L✝<VAR>inst✝¹ : Algebra K L✝<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>hnfd : ¬FiniteDimensional F E<VAR>n : ℕ<VAR>L : IntermediateField F E<VAR>fin : FiniteDimensional F ↥L<VAR>hn : n < finrank F ↥L<VAR>x : E<VAR>hx : x ∉ L<VAR>L' : IntermediateField F E := L ⊔ F⟮x⟯<VAR>this : FiniteDimensional F ↥F⟮x⟯<VAR>h : ¬n + 1 < finrank F ↥L'<GOAL>False
<VAR>F : Type u_1<VAR>inst✝⁷ : Field F<VAR>E : Type u_2<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>L✝ : Type u_3<VAR>inst✝² : Field L✝<VAR>inst✝¹ : Algebra K L✝<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>hnfd : ¬FiniteDimensional F E<VAR>n : ℕ<VAR>L : IntermediateField F E<VAR>fin : FiniteDimensional F ↥L<VAR>hn : n < finrank F ↥L<VAR>x : E<VAR>hx : x ∉ L<VAR>L' : IntermediateField F E := L ⊔ F⟮x⟯<VAR>this : FiniteDimensional F ↥F⟮x⟯<VAR>h : ¬n + 1 < finrank F ↥L'<VAR>h1 : L = L'<GOAL>False
<VAR>F : Type u_1<VAR>inst✝⁷ : Field F<VAR>E : Type u_2<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>L✝ : Type u_3<VAR>inst✝² : Field L✝<VAR>inst✝¹ : Algebra K L✝<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>hnfd : ¬FiniteDimensional F E<VAR>n : ℕ<VAR>L : IntermediateField F E<VAR>fin : FiniteDimensional F ↥L<VAR>hn : n < finrank F ↥L<VAR>x : E<VAR>hx : x ∉ L<VAR>L' : IntermediateField F E := L ⊔ F⟮x⟯<VAR>this : FiniteDimensional F ↥F⟮x⟯<VAR>h : ¬n + 1 < finrank F ↥L'<VAR>h1 : L = L'<VAR>h2 : F⟮x⟯ ≤ L'<GOAL>False
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>Y : D<GOAL>e.inverse.map (e.counit.app Y) = e.unitInv.app (e.inverse.obj Y)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>Y : D<GOAL>𝟙 (e.inverse.obj Y) = 𝟙 ((𝟭 C).obj (e.inverse.obj Y))
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>A : Type u_5<VAR>B : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>δ : Type u_10<VAR>inst✝² : DivInvMonoid β<VAR>inst✝¹ : SMul α β<VAR>inst✝ : IsScalarTower α β β<VAR>r : α<VAR>x y : β<GOAL>r • x / y = r • (x / y)
<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>j : ι<VAR>hj : ¬c.Rel j (c.next j)<VAR>k : ι<VAR>hk' : c.Rel j k<GOAL>c.Rel j (c.next j)
<VAR>f✝ g : CircleDeg1Lift<VAR>f : CircleDeg1Liftˣ<VAR>x : ℝ<GOAL>↑f⁻¹ (↑f x) = x
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>yn a1 n * yn a1 n ∣ yn a1 n ^ 3
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>yn a1 n * yn a1 n ∣ yn a1 n * xn a1 n ^ (yn a1 n - 1) * yn a1 n
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>a : α<VAR>b : Bool<GOAL>¬Step [(a, b)] L
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t : Set α<VAR>f g : α → ℝ≥0∞<GOAL>⨍⁻ (_x : α), 0 ∂μ = 0
<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>m : M<GOAL>star ((ι Q) m) = -(ι Q) m
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>pb : PowerBasis K L<VAR>f : K[X]<GOAL>pb.equivAdjoinSimple.symm ((aeval pb.gen) f) = (aeval (AdjoinSimple.gen K pb.gen)) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b b₁✝ b₂✝ : β<VAR>γ : Type u_3<VAR>inst✝⁸ : Zero α<VAR>inst✝⁷ : Preorder α<VAR>inst✝⁶ : Zero β<VAR>inst✝⁵ : Preorder β<VAR>inst✝⁴ : Zero γ<VAR>inst✝³ : Preorder γ<VAR>inst✝² : SMul α β<VAR>inst✝¹ : SMul α γ<VAR>f : β → γ<VAR>inst✝ : PosSMulStrictMono α γ<VAR>hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂<VAR>smul : ∀ (a : α) (b : β), f (a • b) = a • f b<VAR>a : α<VAR>ha : 0 < a<VAR>b₁ b₂ : β<VAR>hb : b₁ < b₂<GOAL>a • b₁ < a • b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b b₁✝ b₂✝ : β<VAR>γ : Type u_3<VAR>inst✝⁸ : Zero α<VAR>inst✝⁷ : Preorder α<VAR>inst✝⁶ : Zero β<VAR>inst✝⁵ : Preorder β<VAR>inst✝⁴ : Zero γ<VAR>inst✝³ : Preorder γ<VAR>inst✝² : SMul α β<VAR>inst✝¹ : SMul α γ<VAR>f : β → γ<VAR>inst✝ : PosSMulStrictMono α γ<VAR>hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂<VAR>a : α<VAR>ha : 0 < a<VAR>b₁ b₂ : β<VAR>smul : α → β → True<VAR>hb : f b₁ < f b₂<GOAL>a • f b₁ < a • f b₂
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>κ : Type u_3<VAR>κ' : Type u_4<VAR>R : Type u_5<VAR>M : Type u_6<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>R₂ : Type u_7<VAR>M₂ : Type u_8<VAR>inst✝⁸ : CommRing R₂<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : Module R₂ M₂<VAR>e : Basis ι R M<VAR>v : ι' → M<VAR>i : ι<VAR>j : ι'<VAR>N : Type u_9<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>b : Basis ι R M<VAR>b' : Basis ι' R M<VAR>c : Basis κ R N<VAR>c' : Basis κ' R N<VAR>f : M →ₗ[R] N<VAR>inst✝³ : Fintype ι'<VAR>inst✝² : Finite κ<VAR>inst✝¹ : Fintype κ'<VAR>inst✝ : DecidableEq ι'<VAR>this : DecidableEq κ'<GOAL>(toLin b' c) (c.toMatrix ⇑c' * (toMatrix b' c') f) = (toLin b' c) ((toMatrix b' c) f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : Monoid α<VAR>p n : α<VAR>hp : Irreducible p<GOAL>IsRelPrime p n ↔ ¬p ∣ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : Monoid α<VAR>p n : α<VAR>hp : Irreducible p<VAR>hpn : ¬p ∣ n<VAR>d : α<VAR>hdp : d ∣ p<VAR>hdn : d ∣ n<GOAL>IsUnit d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : Monoid α<VAR>p n : α<VAR>hp : Irreducible p<VAR>d : α<VAR>hdp : d ∣ p<VAR>hdn : d ∣ n<VAR>hpn : ¬IsUnit d<GOAL>p ∣ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : Monoid α<VAR>p n : α<VAR>hp : Irreducible p<VAR>d : α<VAR>hdp : d ∣ p<VAR>hdn : d ∣ n<VAR>hpn : ¬IsUnit d<GOAL>p ~ᵤ d
<GOAL>HasSum (fun n => term (n + 1) 1) (1 - γ)
<GOAL>Tendsto (fun n => ∑ i ∈ Finset.range n, term (i + 1) 1) atTop (𝓝 (1 - γ))
<GOAL>Tendsto (fun N => term_sum 1 N) atTop (𝓝 (1 - γ))
<GOAL>Tendsto (fun N => -↑(harmonic (N + 1)) + log (↑N + 1) + 1) atTop (𝓝 (-γ + 1))
<GOAL>Tendsto (fun N => -↑(harmonic (N + 1)) + log (↑N + 1)) atTop (𝓝 (-γ))
<VAR>this : Tendsto (fun x => -(eulerMascheroniSeq' ∘ fun a => a + 1) x) atTop (𝓝 (-γ))<GOAL>Tendsto (fun N => -↑(harmonic (N + 1)) + log (↑N + 1)) atTop (𝓝 (-γ))
<VAR>this : Tendsto (fun x => -(eulerMascheroniSeq' ∘ fun a => a + 1) x) atTop (𝓝 (-γ))<VAR>n : ℕ<GOAL>-(eulerMascheroniSeq' ∘ fun a => a + 1) n = (fun N => -↑(harmonic (N + 1)) + log (↑N + 1)) n
<VAR>this : Tendsto (fun x => -(eulerMascheroniSeq' ∘ fun a => a + 1) x) atTop (𝓝 (-γ))<VAR>n : ℕ<GOAL>-(↑(harmonic (n + 1)) - log ↑(n + 1)) = -↑(harmonic (n + 1)) + log (↑n + 1)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain S<VAR>inst✝³ : Algebra R S<VAR>N : Type u_4<VAR>inst✝² : Semiring N<VAR>inst✝¹ : Module N S<VAR>inst✝ : SMulCommClass R N S<VAR>b : Basis ι R S<VAR>x : S<VAR>hx : x ≠ 0<VAR>i : ι<GOAL>((↑(b.constr N)).toFun (Subtype.val ∘ ⇑(basisSpanSingleton b hx))) (b i) = ((Algebra.lmul R S) x) (b i)
<VAR>G : PGame<GOAL>G.ImpartialAux ↔ G ≈ -G ∧ (∀ (i : G.LeftMoves), (G.moveLeft i).ImpartialAux) ∧ ∀ (j : G.RightMoves), (G.moveRight j).ImpartialAux
<VAR>a b c : SignType<VAR>x✝¹ : a ≤ b<VAR>x✝ : b ≤ c<GOAL>a ≤ c
<VAR>p q : ℤ[X]<VAR>hp : p.IsUnitTrinomial<VAR>h : IsRelPrime p p.mirror<GOAL>Irreducible p
<VAR>p q✝ : ℤ[X]<VAR>hp : p.IsUnitTrinomial<VAR>h : IsRelPrime p p.mirror<VAR>q : ℤ[X]<VAR>hpq : p * p.mirror = q * q.mirror<GOAL>q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
<VAR>p q✝ : ℤ[X]<VAR>hp : p.IsUnitTrinomial<VAR>h : IsRelPrime p p.mirror<VAR>q : ℤ[X]<VAR>hpq : p * p.mirror = q * q.mirror<VAR>hq : q.IsUnitTrinomial<GOAL>q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
<VAR>p q✝ : ℤ[X]<VAR>h : IsRelPrime p p.mirror<VAR>q : ℤ[X]<VAR>hpq : p * p.mirror = q * q.mirror<VAR>k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>u v w : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>k' m' n' : ℕ<VAR>hkm' : k' < m'<VAR>hmn' : m' < n'<VAR>x y z : ℤˣ<VAR>hq : q = trinomial k' m' n' ↑x ↑y ↑z<GOAL>q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
<VAR>p q✝ : ℤ[X]<VAR>h : IsRelPrime p p.mirror<VAR>q : ℤ[X]<VAR>hpq : p * p.mirror = q * q.mirror<VAR>k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>u v w : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>k' m' n' : ℕ<VAR>hkm' : k' < m'<VAR>hmn' : m' < n'<VAR>x y z : ℤˣ<VAR>hq : q = trinomial k' m' n' ↑x ↑y ↑z<VAR>hk : k = k'<GOAL>q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
<VAR>p q✝ : ℤ[X]<VAR>h : IsRelPrime p p.mirror<VAR>q : ℤ[X]<VAR>hpq : p * p.mirror = q * q.mirror<VAR>k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>u v w : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>k' m' n' : ℕ<VAR>hkm' : k' < m'<VAR>hmn' : m' < n'<VAR>x y z : ℤˣ<VAR>hq : q = trinomial k' m' n' ↑x ↑y ↑z<VAR>hk : k = k'<VAR>hn : n = n'<GOAL>q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
<VAR>p q✝ : ℤ[X]<VAR>h : IsRelPrime p p.mirror<VAR>q : ℤ[X]<VAR>hpq : p * p.mirror = q * q.mirror<VAR>k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>u v w : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>m' : ℕ<VAR>x y z : ℤˣ<VAR>hkm' : k < m'<VAR>hmn' : m' < n<VAR>hq : q = trinomial k m' n ↑x ↑y ↑z<GOAL>q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
<VAR>p q✝ : ℤ[X]<VAR>h : IsRelPrime p p.mirror<VAR>q : ℤ[X]<VAR>hpq : p * p.mirror = q * q.mirror<VAR>k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>u v w : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>m' : ℕ<VAR>x y z : ℤˣ<VAR>hkm' : k < m'<VAR>hmn' : m' < n<VAR>hq : q = trinomial k m' n ↑x ↑y ↑z<VAR>h1 : ↑y = ↑v<GOAL>q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
<VAR>p q✝ : ℤ[X]<VAR>h : IsRelPrime p p.mirror<VAR>q : ℤ[X]<VAR>hpq : p * p.mirror = q * q.mirror<VAR>k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>u v w : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>m' : ℕ<VAR>x y z : ℤˣ<VAR>hkm' : k < m'<VAR>hmn' : m' < n<VAR>hq : q = trinomial k m' n ↑x ↑y ↑z<VAR>h1 : ↑y = -↑v<GOAL>q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>f : α → β<VAR>s : Set β<VAR>hf : InjOn f (f ⁻¹' s)<VAR>hsf : s ⊆ range f<GOAL>Nat.card ↑(f ⁻¹' s) = Nat.card ↑s
<VAR>G : Type u_1<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁷ : SFinite ν<VAR>inst✝⁶ : SFinite μ<VAR>s✝ : Set G<VAR>inst✝⁵ : MeasurableInv G<VAR>inst✝⁴ : μ.IsMulLeftInvariant<VAR>μ' ν' : Measure G<VAR>inst✝³ : SigmaFinite μ'<VAR>inst✝² : SigmaFinite ν'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : ν'.IsMulLeftInvariant<VAR>s : Set G<VAR>hμs : μ' s ≠ ⊤<VAR>sm : MeasurableSet s<GOAL>∀ᵐ (x : G) ∂μ', ν' ((fun x_1 => x_1 * x) ⁻¹' s) < ⊤
<VAR>G : Type u_1<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁷ : SFinite ν<VAR>inst✝⁶ : SFinite μ<VAR>s✝ : Set G<VAR>inst✝⁵ : MeasurableInv G<VAR>inst✝⁴ : μ.IsMulLeftInvariant<VAR>μ' ν' : Measure G<VAR>inst✝³ : SigmaFinite μ'<VAR>inst✝² : SigmaFinite ν'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : ν'.IsMulLeftInvariant<VAR>s : Set G<VAR>hμs : μ' s ≠ ⊤<VAR>sm : MeasurableSet s<GOAL>∀ (s_1 : Set G), MeasurableSet s_1 → μ' s_1 < ⊤ → ν'.inv s_1 < ⊤ → ∀ᵐ (x : G) ∂μ'.restrict s_1, ν' ((fun x_1 => x_1 * x) ⁻¹' s) < ⊤
<VAR>G : Type u_1<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁷ : SFinite ν<VAR>inst✝⁶ : SFinite μ<VAR>s✝ : Set G<VAR>inst✝⁵ : MeasurableInv G<VAR>inst✝⁴ : μ.IsMulLeftInvariant<VAR>μ' ν' : Measure G<VAR>inst✝³ : SigmaFinite μ'<VAR>inst✝² : SigmaFinite ν'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : ν'.IsMulLeftInvariant<VAR>s : Set G<VAR>hμs : μ' s ≠ ⊤<VAR>sm : MeasurableSet s<VAR>A : Set G<VAR>hA : MeasurableSet A<VAR>a✝ : μ' A < ⊤<VAR>h3A : ν'.inv A < ⊤<GOAL>∀ᵐ (x : G) ∂μ'.restrict A, ν' ((fun x_1 => x_1 * x) ⁻¹' s) < ⊤
<VAR>G : Type u_1<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁷ : SFinite ν<VAR>inst✝⁶ : SFinite μ<VAR>s✝ : Set G<VAR>inst✝⁵ : MeasurableInv G<VAR>inst✝⁴ : μ.IsMulLeftInvariant<VAR>μ' ν' : Measure G<VAR>inst✝³ : SigmaFinite μ'<VAR>inst✝² : SigmaFinite ν'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : ν'.IsMulLeftInvariant<VAR>s : Set G<VAR>hμs : μ' s ≠ ⊤<VAR>sm : MeasurableSet s<VAR>A : Set G<VAR>hA : MeasurableSet A<VAR>a✝ : μ' A < ⊤<VAR>h3A : ν' A⁻¹ < ⊤<GOAL>∀ᵐ (x : G) ∂μ'.restrict A, ν' ((fun x_1 => x_1 * x) ⁻¹' s) < ⊤
<VAR>G : Type u_1<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁷ : SFinite ν<VAR>inst✝⁶ : SFinite μ<VAR>s✝ : Set G<VAR>inst✝⁵ : MeasurableInv G<VAR>inst✝⁴ : μ.IsMulLeftInvariant<VAR>μ' ν' : Measure G<VAR>inst✝³ : SigmaFinite μ'<VAR>inst✝² : SigmaFinite ν'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : ν'.IsMulLeftInvariant<VAR>s : Set G<VAR>hμs : μ' s ≠ ⊤<VAR>sm : MeasurableSet s<VAR>A : Set G<VAR>hA : MeasurableSet A<VAR>a✝ : μ' A < ⊤<VAR>h3A : ν' A⁻¹ < ⊤<GOAL>∫⁻ (x : G) in A, ν' ((fun y => y * x) ⁻¹' s) ∂μ' ≠ ⊤
<VAR>G : Type u_1<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁷ : SFinite ν<VAR>inst✝⁶ : SFinite μ<VAR>s✝ : Set G<VAR>inst✝⁵ : MeasurableInv G<VAR>inst✝⁴ : μ.IsMulLeftInvariant<VAR>μ' ν' : Measure G<VAR>inst✝³ : SigmaFinite μ'<VAR>inst✝² : SigmaFinite ν'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : ν'.IsMulLeftInvariant<VAR>s : Set G<VAR>hμs : μ' s ≠ ⊤<VAR>sm : MeasurableSet s<VAR>A : Set G<VAR>hA : MeasurableSet A<VAR>a✝ : μ' A < ⊤<VAR>h3A : ν' A⁻¹ < ⊤<VAR>h1 : μ' s * ∫⁻ (y : G), A⁻¹.indicator 1 y ∂ν' = ∫⁻ (x : G), ν' ((fun z => z * x) ⁻¹' s) * A⁻¹.indicator 1 x⁻¹ ∂μ'<GOAL>∫⁻ (x : G) in A, ν' ((fun y => y * x) ⁻¹' s) ∂μ' ≠ ⊤
<VAR>G : Type u_1<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁷ : SFinite ν<VAR>inst✝⁶ : SFinite μ<VAR>s✝ : Set G<VAR>inst✝⁵ : MeasurableInv G<VAR>inst✝⁴ : μ.IsMulLeftInvariant<VAR>μ' ν' : Measure G<VAR>inst✝³ : SigmaFinite μ'<VAR>inst✝² : SigmaFinite ν'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : ν'.IsMulLeftInvariant<VAR>s : Set G<VAR>hμs : μ' s ≠ ⊤<VAR>sm : MeasurableSet s<VAR>A : Set G<VAR>hA : MeasurableSet A<VAR>a✝ : μ' A < ⊤<VAR>h3A : ν' A⁻¹ < ⊤<VAR>h1 : μ' s * ∫⁻ (a : G) in A⁻¹, 1 a ∂ν' = ∫⁻ (x : G), ν' ((fun z => z * x) ⁻¹' s) * A⁻¹.indicator 1 x⁻¹ ∂μ'<GOAL>∫⁻ (x : G) in A, ν' ((fun y => y * x) ⁻¹' s) ∂μ' ≠ ⊤
<VAR>G : Type u_1<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁷ : SFinite ν<VAR>inst✝⁶ : SFinite μ<VAR>s✝ : Set G<VAR>inst✝⁵ : MeasurableInv G<VAR>inst✝⁴ : μ.IsMulLeftInvariant<VAR>μ' ν' : Measure G<VAR>inst✝³ : SigmaFinite μ'<VAR>inst✝² : SigmaFinite ν'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : ν'.IsMulLeftInvariant<VAR>s : Set G<VAR>hμs : μ' s ≠ ⊤<VAR>sm : MeasurableSet s<VAR>A : Set G<VAR>hA : MeasurableSet A<VAR>a✝ : μ' A < ⊤<VAR>h3A : ν' A⁻¹ < ⊤<VAR>h1 : μ' s * ν' A⁻¹ = ∫⁻ (x : G), A.indicator (fun j => ν' ((fun y => y * j) ⁻¹' s)) x ∂μ'<GOAL>∫⁻ (x : G) in A, ν' ((fun y => y * x) ⁻¹' s) ∂μ' ≠ ⊤
<VAR>G : Type u_1<VAR>inst✝¹⁰ : MeasurableSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁷ : SFinite ν<VAR>inst✝⁶ : SFinite μ<VAR>s✝ : Set G<VAR>inst✝⁵ : MeasurableInv G<VAR>inst✝⁴ : μ.IsMulLeftInvariant<VAR>μ' ν' : Measure G<VAR>inst✝³ : SigmaFinite μ'<VAR>inst✝² : SigmaFinite ν'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : ν'.IsMulLeftInvariant<VAR>s : Set G<VAR>hμs : μ' s ≠ ⊤<VAR>sm : MeasurableSet s<VAR>A : Set G<VAR>hA : MeasurableSet A<VAR>a✝ : μ' A < ⊤<VAR>h3A : ν' A⁻¹ < ⊤<VAR>h1 : μ' s * ν' A⁻¹ = ∫⁻ (x : G), A.indicator (fun j => ν' ((fun y => y * j) ⁻¹' s)) x ∂μ'<GOAL>μ' s * ν' A⁻¹ ≠ ⊤
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_2<VAR>inst✝¹ : NontriviallyNormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>c d✝ : 𝕜 → 𝕜'<VAR>c' d' : 𝕜'<VAR>hc : HasStrictDerivAt c c' x<VAR>d : 𝕜'<GOAL>HasStrictDerivAt (fun x => c x / d) (c' / d) x
<VAR>α : Type u_1<VAR>inst✝³ : Mul α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (Function.swap HMul.hMul) LE.le<VAR>a b y : α<VAR>hya : y ∈ Iic a<VAR>z : α<VAR>hzb : z ∈ Iic b<GOAL>(fun x x_1 => x * x_1) y z ∈ Iic (a * b)
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticMap R M N<VAR>x : M<GOAL>polar (⇑Q) x x = 2 • Q x
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticMap R M N<VAR>x : M<GOAL>4 • Q x = (2 * 2) • Q x
<VAR>α : Type v<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>exp_pos : 0 < Monoid.exponent M<VAR>m : M<GOAL>BddAbove (Set.range fun a => period m a)
<VAR>α : Type v<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>exp_pos : 0 < Monoid.exponent M<VAR>m : M<GOAL>Monoid.exponent M ∈ upperBounds (Set.range fun a => period m a)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m✝ : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>inst✝ : DecidableEq σ<VAR>i : σ<VAR>m : σ →₀ ℕ<VAR>k : ℕ<GOAL>coeff m (X i ^ k) = if Finsupp.single i k = m then 1 else 0
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m✝ : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>inst✝ : DecidableEq σ<VAR>i : σ<VAR>m : σ →₀ ℕ<VAR>k : ℕ<VAR>this : coeff m ((monomial (Finsupp.single i k)) 1) = if Finsupp.single i k = m then 1 else 0<GOAL>coeff m (X i ^ k) = if Finsupp.single i k = m then 1 else 0
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m✝ : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>inst✝ : DecidableEq σ<VAR>i : σ<VAR>m : σ →₀ ℕ<VAR>k : ℕ<VAR>this : coeff m ((Finsupp.single i k).prod fun n e => X n ^ e) = if Finsupp.single i k = m then 1 else 0<GOAL>X i ^ 0 = 1
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝⁷ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P : Cᵒᵖ ⥤ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>x✝ : Cᵒᵖ<GOAL>F.map (⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P (unop x✝)) (op ⊤)) ≫ (J.plusCompIso F P).hom.app x✝ = ⊤.toMultiequalizer (P ⋙ F) ≫ colimit.ι (J.diagram (P ⋙ F) (unop x✝)) (op ⊤)
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝⁷ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P : Cᵒᵖ ⥤ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>x✝ : Cᵒᵖ<GOAL>F.map (⊤.toMultiequalizer P) ≫ (J.diagramCompIso F P (unop x✝)).hom.app (op ⊤) ≫ colimit.ι (J.diagram (P ⋙ F) (unop x✝)) (op ⊤) = ⊤.toMultiequalizer (P ⋙ F) ≫ colimit.ι (J.diagram (P ⋙ F) (unop x✝)) (op ⊤)