ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u'<VAR>inst✝⁴ : Category.{v', u'} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝³ : Presheaf.IsLocallyInjective J α<VAR>inst✝² : Presheaf.IsLocallySurjective J α<VAR>inst✝¹ : J.WEqualsLocallyBijective AddCommGrp<VAR>inst✝ : HasWeakSheafify J AddCommGrp<VAR>X✝ Y✝ Z✝ : PresheafOfModules R₀<VAR>x✝¹ : X✝ ⟶ Y✝<VAR>x✝ : Y✝ ⟶ Z✝<GOAL>(toPresheaf R.val).map ({ obj := fun M₀ => sheafify α (CategoryTheory.toSheafify J M₀.presheaf), map := fun {X Y} f => sheafifyMap α (CategoryTheory.toSheafify J X.presheaf) (CategoryTheory.toSheafify J Y.presheaf) f ((presheafToSheaf J AddCommGrp).map f.hom) ⋯ }.map (x✝¹ ≫ x✝)).val = (toPresheaf R.val).map ({ obj := fun M₀ => sheafify α (CategoryTheory.toSheafify J M₀.presheaf), map := fun {X Y} f => sheafifyMap α (CategoryTheory.toSheafify J X.presheaf) (CategoryTheory.toSheafify J Y.presheaf) f ((presheafToSheaf J AddCommGrp).map f.hom) ⋯ }.map x✝¹ ≫ { obj := fun M₀ => sheafify α (CategoryTheory.toSheafify J M₀.presheaf), map := fun {X Y} f => sheafifyMap α (CategoryTheory.toSheafify J X.presheaf) (CategoryTheory.toSheafify J Y.presheaf) f ((presheafToSheaf J AddCommGrp).map f.hom) ⋯ }.map x✝).val
<VAR>p x : ℝ<VAR>hp : p ≠ 0<GOAL>‖↑x‖ = |x| ↔ |x| ≤ |p| / 2
<VAR>p x : ℝ<VAR>hp : p ≠ 0<VAR>hx : |x| ≤ |p| / 2<GOAL>‖↑x‖ = |x|
<VAR>p✝ x : ℝ<VAR>hp✝ : p✝ ≠ 0<VAR>p : ℝ<VAR>hp : 0 < p<VAR>hx : |x| ≤ p / 2<GOAL>‖↑x‖ = |x|
<VAR>p✝ : ℝ<VAR>hp✝ : p✝ ≠ 0<VAR>p : ℝ<VAR>hp : 0 < p<VAR>hx : |p / 2| ≤ p / 2<GOAL>‖↑(p / 2)‖ = |p / 2|
<VAR>p✝ x : ℝ<VAR>hp✝ : p✝ ≠ 0<VAR>p : ℝ<VAR>hp : 0 < p<VAR>hx : |x| ≤ p / 2<VAR>hx' : x ≠ p / 2<GOAL>‖↑x‖ = |x|
<VAR>p✝ x : ℝ<VAR>hp✝ : p✝ ≠ 0<VAR>p : ℝ<VAR>hp : 0 < p<VAR>hx : |x| ≤ p / 2<VAR>hx' : x ≠ p / 2<GOAL>round (p⁻¹ * x) = 0
<VAR>p✝ x : ℝ<VAR>hp✝ : p✝ ≠ 0<VAR>p : ℝ<VAR>hp : 0 < p<VAR>hx : |x| ≤ p / 2<VAR>hx' : x ≠ p / 2<GOAL>p⁻¹ * x ∈ Ico (-(1 / 2)) (1 / 2)
<VAR>p✝ x : ℝ<VAR>hp✝ : p✝ ≠ 0<VAR>p : ℝ<VAR>hp : 0 < p<VAR>hx : |x| ≤ p / 2<VAR>hx' : x ≠ p / 2<VAR>hx₁ : -(p / 2) ≤ x<VAR>hx₂ : x ≤ p / 2<GOAL>p⁻¹ * x ∈ Ico (-(1 / 2)) (1 / 2)
<VAR>p✝ x : ℝ<VAR>hp✝ : p✝ ≠ 0<VAR>p : ℝ<VAR>hp : 0 < p<VAR>hx : |x| ≤ p / 2<VAR>hx' : x ≠ p / 2<VAR>hx₁ : -(p / 2) ≤ x<VAR>hx₂ : x < p / 2<GOAL>p⁻¹ * x ∈ Ico (-(1 / 2)) (1 / 2)
<VAR>s : List Char<GOAL>go₂ s { byteIdx := 0 } { byteIdx := utf8Len s } = s
<VAR>p : ℕ → Prop<VAR>h : p 0<GOAL>nth p 0 = 0
<VAR>σ : Type u_1<VAR>f : σ → Option σ<VAR>a b : σ<VAR>h : b ∈ eval f a<VAR>c : σ<VAR>x✝ : Reaches₁ f b c<VAR>bc : Reaches₁ f b c := x✝<GOAL>False
<VAR>σ : Type u_1<VAR>f : σ → Option σ<VAR>a b : σ<VAR>h : b ∈ eval f a<VAR>c : σ<VAR>x✝ : Reaches₁ f b c<VAR>bc : Reaches₁ f b c := x✝<VAR>left✝ : Reaches f a b<VAR>b0 : f b = none<GOAL>False
<VAR>σ : Type u_1<VAR>f : σ → Option σ<VAR>a b : σ<VAR>h : b ∈ eval f a<VAR>c : σ<VAR>x✝ : Reaches₁ f b c<VAR>bc : Reaches₁ f b c := x✝<VAR>left✝ : Reaches f a b<VAR>b0 : f b = none<VAR>b' : σ<VAR>h' : b' ∈ f b<VAR>right✝ : ReflTransGen (fun a b => b ∈ f a) b' c<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>h : (ball x ε₁ ∩ closedBall y ε₂).Nonempty<GOAL>dist x y < ε₁ + ε₂
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>h : (closedBall y ε₂ ∩ ball x ε₁).Nonempty<GOAL>dist x y < ε₁ + ε₂
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>h : (closedBall y ε₂ ∩ ball x ε₁).Nonempty<GOAL>dist y x < ε₂ + ε₁
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<VAR>x✝ : hs.Quotient<VAR>x y : α<GOAL>y ∈ hs.proj ⁻¹' {Quotient.mk'' x} ↔ y ∈ s (hs.equivQuotient.symm (Quotient.mk'' x))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<VAR>x✝ : hs.Quotient<VAR>x y : α<GOAL>hs.proj y = Quotient.mk'' x ↔ hs.index y = hs.equivQuotient.symm (Quotient.mk'' x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Module A M<VAR>inst✝ : IsScalarTower R A M<VAR>x : PrimeSpectrum A<VAR>hx : x ∈ support A M<GOAL>x ∈ ⇑(PrimeSpectrum.comap (algebraMap R A)) ⁻¹' support R M
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Module A M<VAR>inst✝ : IsScalarTower R A M<VAR>x : PrimeSpectrum A<VAR>hx : ∃ m, ∀ (r : A), r • m = 0 → r ∈ x.asIdeal<GOAL>∃ m, ∀ (r : R), r • m = 0 → (algebraMap R A) r ∈ x.asIdeal
<VAR>α : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>b : FactorSet α<VAR>h : ⊤ ≤ b<GOAL>⊤.prod ≤ b.prod
<VAR>α : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>b : FactorSet α<VAR>h : ⊤ ≤ b<VAR>this : b = ⊤<GOAL>⊤.prod ≤ b.prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : CountableOrCountablyGenerated α β<VAR>κ : Kernel α (β × Ω)<VAR>inst✝² : IsFiniteKernel κ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>a : α<VAR>hf : Integrable f (κ a)<GOAL>∫ (b : β), ∫ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω), f x ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : CountableOrCountablyGenerated α β<VAR>κ : Kernel α (β × Ω)<VAR>inst✝² : IsFiniteKernel κ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>a : α<VAR>hf : Integrable f (κ a)<GOAL>∫ (b : β), ∫ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω), f x ∂(κ.fst ⊗ₖ κ.condKernel) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : CountableOrCountablyGenerated α β<VAR>κ : Kernel α (β × Ω)<VAR>inst✝² : IsFiniteKernel κ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>a : α<VAR>hf : Integrable f ((κ.fst ⊗ₖ κ.condKernel) a)<GOAL>∫ (b : β), ∫ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω), f x ∂(κ.fst ⊗ₖ κ.condKernel) a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>B : ModuleFilterBasis R M<VAR>ι : Type u_3<VAR>inst✝² : TopologicalRing R<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : TopologicalAddGroup M<VAR>p : ι → Prop<VAR>b : ι → Set M<VAR>h : (𝓝 0).HasBasis p b<VAR>hsmul : ∀ {i : ι}, p i → ∃ V ∈ 𝓝 0, ∃ j, p j ∧ V • b j ⊆ b i<VAR>hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ MapsTo (fun x => x₀ • x) (b j) (b i)<VAR>hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i<GOAL>ContinuousSMul R M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>B : ModuleFilterBasis R M<VAR>ι : Type u_3<VAR>inst✝² : TopologicalRing R<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : TopologicalAddGroup M<VAR>p : ι → Prop<VAR>b : ι → Set M<VAR>h : (𝓝 0).HasBasis p b<VAR>hsmul : ∀ {i : ι}, p i → ∃ V ∈ 𝓝 0, ∃ j, p j ∧ V • b j ⊆ b i<VAR>hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ MapsTo (fun x => x₀ • x) (b j) (b i)<VAR>hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i<GOAL>Tendsto (fun p => p.1 • p.2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>B : ModuleFilterBasis R M<VAR>ι : Type u_3<VAR>inst✝² : TopologicalRing R<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : TopologicalAddGroup M<VAR>p : ι → Prop<VAR>b : ι → Set M<VAR>h : (𝓝 0).HasBasis p b<VAR>hsmul : ∀ {i : ι}, p i → ∃ V ∈ 𝓝 0, ∃ j, p j ∧ V • b j ⊆ b i<VAR>hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ MapsTo (fun x => x₀ • x) (b j) (b i)<VAR>hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i<GOAL>∀ (m : M), Tendsto (fun a => a • m) (𝓝 0) (𝓝 0)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>B : ModuleFilterBasis R M<VAR>ι : Type u_3<VAR>inst✝² : TopologicalRing R<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : TopologicalAddGroup M<VAR>p : ι → Prop<VAR>b : ι → Set M<VAR>h : (𝓝 0).HasBasis p b<VAR>hsmul : ∀ {i : ι}, p i → ∃ V ∈ 𝓝 0, ∃ j, p j ∧ V • b j ⊆ b i<VAR>hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ j, p j ∧ MapsTo (fun x => x₀ • x) (b j) (b i)<VAR>hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i<GOAL>∀ (a : R), Tendsto (fun m => a • m) (𝓝 0) (𝓝 0)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>inst✝² : Category.{u_4, u_3} C<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>K : HomologicalComplex C c<VAR>e : c.Embedding c'<VAR>i' j' : ι'<VAR>i : ι<VAR>hi : e.f i = i'<VAR>hi' : ¬c.Rel i (c.next i)<GOAL>(K.extend e).d i' j' = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>inst✝² : Category.{u_4, u_3} C<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>K : HomologicalComplex C c<VAR>e : c.Embedding c'<VAR>i' j' : ι'<VAR>i : ι<VAR>hi : e.f i = i'<VAR>hi' : ¬c.Rel i (c.next i)<VAR>hj' : e.r j' = none<GOAL>(K.extend e).d i' j' = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>inst✝² : Category.{u_4, u_3} C<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>K : HomologicalComplex C c<VAR>e : c.Embedding c'<VAR>i' j' : ι'<VAR>i : ι<VAR>hi : e.f i = i'<VAR>hi' : ¬c.Rel i (c.next i)<VAR>j : ι<VAR>hj : e.r j' = some j<GOAL>(K.extend e).d i' j' = 0
<VAR>R : Type u<VAR>σ : Type v<VAR>a a' a₁ a₂ : R<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>S : Type u_1<VAR>inst✝ : CommSemiring S<VAR>φ : R →+* S<VAR>f : MvPolynomial σ R<VAR>i : σ<GOAL>(pderiv i) ((map φ) f) = (map φ) ((pderiv i) f)
<VAR>R : Type u<VAR>σ : Type v<VAR>a a' a₁ a₂ : R<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>S : Type u_1<VAR>inst✝ : CommSemiring S<VAR>φ : R →+* S<VAR>f : MvPolynomial σ R<VAR>i : σ<VAR>p : MvPolynomial σ R<VAR>j : σ<VAR>eq : (pderiv i) ((map φ) p) = (map φ) ((pderiv i) p)<GOAL>(pderiv i) ((map φ) (p * X j)) = (map φ) ((pderiv i) (p * X j))
<VAR>R : Type u<VAR>σ : Type v<VAR>a a' a₁ a₂ : R<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>S : Type u_1<VAR>inst✝ : CommSemiring S<VAR>φ : R →+* S<VAR>f p : MvPolynomial σ R<VAR>j : σ<VAR>eq : (pderiv j) ((map φ) p) = (map φ) ((pderiv j) p)<GOAL>(pderiv j) ((map φ) (p * X j)) = (map φ) ((pderiv j) (p * X j))
<VAR>R : Type u<VAR>σ : Type v<VAR>a a' a₁ a₂ : R<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>S : Type u_1<VAR>inst✝ : CommSemiring S<VAR>φ : R →+* S<VAR>f : MvPolynomial σ R<VAR>i : σ<VAR>p : MvPolynomial σ R<VAR>j : σ<VAR>eq : (pderiv i) ((map φ) p) = (map φ) ((pderiv i) p)<VAR>h : j ≠ i<GOAL>(pderiv i) ((map φ) (p * X j)) = (map φ) ((pderiv i) (p * X j))
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁹ : DecidableEq α'<VAR>inst✝⁸ : DecidableEq β'<VAR>inst✝⁷ : DecidableEq γ<VAR>inst✝⁶ : DecidableEq γ'<VAR>inst✝⁵ : DecidableEq δ<VAR>inst✝⁴ : DecidableEq δ'<VAR>inst✝³ : DecidableEq ε<VAR>inst✝² : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g✝ g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a✝ a' : α<VAR>b b' : β<VAR>c : γ<VAR>inst✝¹ : SemilatticeSup δ<VAR>inst✝ : OrderBot δ<VAR>g : γ → δ<VAR>a : δ<GOAL>(image₂ f s t).sup g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<GOAL>IsBlock G B ↔ ∀ {g : G} {b : X}, b ∈ B → b ∈ g • B → g • B ⊆ B
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<GOAL>(∀ (g : G), (g • B ∩ B).Nonempty → g • B = B) ↔ ∀ {g : G} {b : X}, b ∈ B → b ∈ g • B → g • B ⊆ B
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>inst✝² : Zero β<VAR>inst✝¹ : Zero γ<VAR>μ : Measure α<VAR>f✝ : α →ₛ β<VAR>inst✝ : MeasurableSpace α<VAR>f : α →ₛ β<GOAL>MeasurableSet (support ↑f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>inst✝² : Zero β<VAR>inst✝¹ : Zero γ<VAR>μ : Measure α<VAR>f✝ : α →ₛ β<VAR>inst✝ : MeasurableSpace α<VAR>f : α →ₛ β<GOAL>MeasurableSet (⋃ y ∈ filter (fun y => y ≠ 0) f.range, ↑f ⁻¹' {y})
<VAR>ι : Type u_1<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : Group α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : GroupNormClass F α β<VAR>f : F<GOAL>f 1 = 0
<VAR>c : ℝ<VAR>f✝ g : ℕ → Bool<VAR>n✝ : ℕ<VAR>f : ℕ → Bool<VAR>n : ℕ<GOAL>cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun n => f (n + 1)) n
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>M✝ : Type u_2<VAR>inst✝¹⁰ : AddCommGroup M✝<VAR>inst✝⁹ : Module R M✝<VAR>M'✝ : Type u_3<VAR>inst✝⁸ : AddCommGroup M'✝<VAR>inst✝⁷ : Module R M'✝<VAR>ι : Type u_4<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : Fintype ι<VAR>e✝ : Basis ι R M✝<VAR>A : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>m : Type u_6<VAR>n : Type u_7<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : DecidableEq n<VAR>M : Matrix n m A<VAR>N M' : Matrix m n A<VAR>hMM' : M * M' = 1<VAR>hM'M : M' * M = 1<VAR>a✝ : Nontrivial A<VAR>e : n ≃ m := indexEquivOfInv hMM' hM'M<GOAL>(M * N).det = (N * M).det
<VAR>n m : ℕ<VAR>inst✝ : NeZero n<VAR>j : Fin (n + 1)<VAR>h : j ≠ 0<GOAL>(predAbove 0 j).succ = j
<VAR>n m : ℕ<VAR>inst✝ : NeZero n<VAR>k : Fin n<VAR>h : k.succ ≠ 0<GOAL>(predAbove 0 k.succ).succ = k.succ
<VAR>n : ℕ<GOAL>properDivisors 1 = ∅
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R⟦X⟧<VAR>hf : f ≠ 0<VAR>hg : g ≠ 0<GOAL>divided_by_X_pow_order hf * divided_by_X_pow_order hg = divided_by_X_pow_order ⋯
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R⟦X⟧<VAR>hf : f ≠ 0<VAR>hg : g ≠ 0<VAR>df : ℕ := f.order.get ⋯<GOAL>divided_by_X_pow_order hf * divided_by_X_pow_order hg = divided_by_X_pow_order ⋯
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R⟦X⟧<VAR>hf : f ≠ 0<VAR>hg : g ≠ 0<VAR>df : ℕ := f.order.get ⋯<VAR>dg : ℕ := g.order.get ⋯<GOAL>divided_by_X_pow_order hf * divided_by_X_pow_order hg = divided_by_X_pow_order ⋯
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R⟦X⟧<VAR>hf : f ≠ 0<VAR>hg : g ≠ 0<VAR>df : ℕ := f.order.get ⋯<VAR>dg : ℕ := g.order.get ⋯<VAR>dfg : ℕ := (f * g).order.get ⋯<VAR>hdfg : dfg = (f * g).order.get ⋯<GOAL>divided_by_X_pow_order hf * divided_by_X_pow_order hg = divided_by_X_pow_order ⋯
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R⟦X⟧<VAR>hf : f ≠ 0<VAR>hg : g ≠ 0<VAR>df : ℕ := f.order.get ⋯<VAR>dg : ℕ := g.order.get ⋯<VAR>dfg : ℕ := (f * g).order.get ⋯<VAR>hdfg : dfg = (f * g).order.get ⋯<VAR>H_add_d : df + dg = dfg<GOAL>divided_by_X_pow_order hf * divided_by_X_pow_order hg = divided_by_X_pow_order ⋯
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R⟦X⟧<VAR>hf : f ≠ 0<VAR>hg : g ≠ 0<VAR>df : ℕ := f.order.get ⋯<VAR>dg : ℕ := g.order.get ⋯<VAR>dfg : ℕ := (f * g).order.get ⋯<VAR>hdfg : dfg = (f * g).order.get ⋯<VAR>H_add_d : df + dg = dfg<VAR>H : X ^ (f * g).order.get ⋯ * divided_by_X_pow_order ⋯ = f * g<GOAL>divided_by_X_pow_order hf * divided_by_X_pow_order hg = divided_by_X_pow_order ⋯
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R⟦X⟧<VAR>hf : f ≠ 0<VAR>hg : g ≠ 0<VAR>df : ℕ := f.order.get ⋯<VAR>dg : ℕ := g.order.get ⋯<VAR>dfg : ℕ := (f * g).order.get ⋯<VAR>hdfg : dfg = (f * g).order.get ⋯<VAR>H_add_d : df + dg = dfg<VAR>H : X ^ (f * g).order.get ⋯ * divided_by_X_pow_order ⋯ = f * g<VAR>this : f * g = X ^ dfg * (divided_by_X_pow_order hf * divided_by_X_pow_order hg)<GOAL>divided_by_X_pow_order hf * divided_by_X_pow_order hg = divided_by_X_pow_order ⋯
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R⟦X⟧<VAR>hf : f ≠ 0<VAR>hg : g ≠ 0<VAR>df : ℕ := f.order.get ⋯<VAR>dg : ℕ := g.order.get ⋯<VAR>dfg : ℕ := (f * g).order.get ⋯<VAR>hdfg : dfg = (f * g).order.get ⋯<VAR>H_add_d : df + dg = dfg<VAR>this : f * g = X ^ dfg * (divided_by_X_pow_order hf * divided_by_X_pow_order hg)<VAR>H : X ^ (X ^ dfg * (divided_by_X_pow_order hf * divided_by_X_pow_order hg)).order.get ⋯ * divided_by_X_pow_order ⋯ = X ^ dfg * (divided_by_X_pow_order hf * divided_by_X_pow_order hg)<GOAL>divided_by_X_pow_order hf * divided_by_X_pow_order hg = divided_by_X_pow_order ⋯
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R⟦X⟧<VAR>hf : f ≠ 0<VAR>hg : g ≠ 0<VAR>df : ℕ := f.order.get ⋯<VAR>dg : ℕ := g.order.get ⋯<VAR>dfg : ℕ := (f * g).order.get ⋯<VAR>hdfg : dfg = (f * g).order.get ⋯<VAR>H_add_d : df + dg = dfg<VAR>this : f * g = X ^ dfg * (divided_by_X_pow_order hf * divided_by_X_pow_order hg)<VAR>H : X ^ (X ^ dfg * (divided_by_X_pow_order hf * divided_by_X_pow_order hg)).order.get ⋯ * divided_by_X_pow_order ⋯ = X ^ dfg * (divided_by_X_pow_order hf * divided_by_X_pow_order hg)<GOAL>X ^ dfg * divided_by_X_pow_order ⋯ = X ^ dfg * (divided_by_X_pow_order hf * divided_by_X_pow_order hg)
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : Fintype l<VAR>inst✝ : CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<VAR>h : A ∈ symplecticGroup l R<GOAL>-A ∈ symplecticGroup l R
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : Fintype l<VAR>inst✝ : CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<VAR>h : A * J l R * Aᵀ = J l R<GOAL>-A * J l R * (-A)ᵀ = J l R
<VAR>R : Type u_1<VAR>inst✝⁴ : StrictOrderedCommRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>x y : M<VAR>u : Rˣ<VAR>hu : ↑u < 0<VAR>v : Ray R M<GOAL>u • v = -v
<VAR>R : Type u_1<VAR>inst✝⁴ : StrictOrderedCommRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>x y : M<VAR>u : Rˣ<VAR>hu : ↑u < 0<VAR>v : Ray R M<GOAL>0 < ↑(-u)
<VAR>R : Type u<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q p : R[X]<VAR>n : ℕ<GOAL>(p.update n 0).support = p.support.erase n
<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>f : R →+* S₁<VAR>g : σ → S₁<VAR>q : S₂ → MvPolynomial σ R<VAR>p : MvPolynomial S₂ R<GOAL>eval₂ f (fun t => eval₂ f g (q t)) p = (eval₂Hom f g) (eval₂ C q p)
<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>f : R →+* S₁<VAR>g : σ → S₁<VAR>q : S₂ → MvPolynomial σ R<VAR>p : MvPolynomial S₂ R<GOAL>eval₂ f (fun t => eval₂ f g (q t)) p = eval₂ ((eval₂Hom f g).comp C) (⇑(eval₂Hom f g) ∘ q) p
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>P : RootPairing ι R M N<VAR>i j : ι<GOAL>P.IsOrthogonal i j ↔ P.IsOrthogonal j i
<VAR>a b p q : ℝ≥0<VAR>h : p.IsConjExponent q<GOAL>p * q = p + q
<VAR>θ : Angle<GOAL>(-θ).expMapCircle = θ.expMapCircle⁻¹
<VAR>x✝ : ℝ<GOAL>(-↑x✝).expMapCircle = (↑x✝).expMapCircle⁻¹
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝¹⁰ : AddCommGroup V<VAR>inst✝⁹ : TopologicalSpace V<VAR>inst✝⁸ : TopologicalAddGroup V<VAR>inst✝⁷ : T2Space V<VAR>inst✝⁶ : MeasurableSpace V<VAR>inst✝⁵ : BorelSpace V<VAR>inst✝⁴ : Module ℝ V<VAR>inst✝³ : ContinuousSMul ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))<VAR>A : V ≃L[ℝ] V'<VAR>this✝¹ : MeasurableSpace V' := borel V'<VAR>this✝ : BorelSpace V'<VAR>Aₘ : V ≃ᵐ V' := A.toHomeomorph.toMeasurableEquiv<GOAL>Tendsto (fun w => ∫ (v : V), 𝐞 (-w v) • f v ∂μ) (cocompact (V →L[ℝ] ℝ)) (𝓝 0)
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝¹⁰ : AddCommGroup V<VAR>inst✝⁹ : TopologicalSpace V<VAR>inst✝⁸ : TopologicalAddGroup V<VAR>inst✝⁷ : T2Space V<VAR>inst✝⁶ : MeasurableSpace V<VAR>inst✝⁵ : BorelSpace V<VAR>inst✝⁴ : Module ℝ V<VAR>inst✝³ : ContinuousSMul ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))<VAR>A : V ≃L[ℝ] V'<VAR>this✝¹ : MeasurableSpace V' := borel V'<VAR>this✝ : BorelSpace V'<VAR>Aₘ : V ≃ᵐ V' := A.toHomeomorph.toMeasurableEquiv<VAR>Adualₗ : (V →L[ℝ] ℝ) ≃ₗ[ℝ] V' →L[ℝ] ℝ := { toFun := fun t => t.comp ↑A.symm, map_add' := ⋯, map_smul' := ⋯, invFun := fun t => t.comp ↑A, left_inv := ⋯, right_inv := ⋯ }<GOAL>Tendsto (fun w => ∫ (v : V), 𝐞 (-w v) • f v ∂μ) (cocompact (V →L[ℝ] ℝ)) (𝓝 0)
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝¹⁰ : AddCommGroup V<VAR>inst✝⁹ : TopologicalSpace V<VAR>inst✝⁸ : TopologicalAddGroup V<VAR>inst✝⁷ : T2Space V<VAR>inst✝⁶ : MeasurableSpace V<VAR>inst✝⁵ : BorelSpace V<VAR>inst✝⁴ : Module ℝ V<VAR>inst✝³ : ContinuousSMul ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))<VAR>A : V ≃L[ℝ] V'<VAR>this✝¹ : MeasurableSpace V' := borel V'<VAR>this✝ : BorelSpace V'<VAR>Aₘ : V ≃ᵐ V' := A.toHomeomorph.toMeasurableEquiv<VAR>Adualₗ : (V →L[ℝ] ℝ) ≃ₗ[ℝ] V' →L[ℝ] ℝ := { toFun := fun t => t.comp ↑A.symm, map_add' := ⋯, map_smul' := ⋯, invFun := fun t => t.comp ↑A, left_inv := ⋯, right_inv := ⋯ }<VAR>Adual : (V →L[ℝ] ℝ) ≃L[ℝ] V' →L[ℝ] ℝ := { toLinearEquiv := Adualₗ, continuous_toFun := ⋯, continuous_invFun := ⋯ }<GOAL>Tendsto (fun w => ∫ (v : V), 𝐞 (-w v) • f v ∂μ) (cocompact (V →L[ℝ] ℝ)) (𝓝 0)
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝¹⁰ : AddCommGroup V<VAR>inst✝⁹ : TopologicalSpace V<VAR>inst✝⁸ : TopologicalAddGroup V<VAR>inst✝⁷ : T2Space V<VAR>inst✝⁶ : MeasurableSpace V<VAR>inst✝⁵ : BorelSpace V<VAR>inst✝⁴ : Module ℝ V<VAR>inst✝³ : ContinuousSMul ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : CompleteSpace E<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))<VAR>A : V ≃L[ℝ] V'<VAR>this✝¹ : MeasurableSpace V' := borel V'<VAR>this✝ : BorelSpace V'<VAR>Aₘ : V ≃ᵐ V' := A.toHomeomorph.toMeasurableEquiv<VAR>Adualₗ : (V →L[ℝ] ℝ) ≃ₗ[ℝ] V' →L[ℝ] ℝ := { toFun := fun t => t.comp ↑A.symm, map_add' := ⋯, map_smul' := ⋯, invFun := fun t => t.comp ↑A, left_inv := ⋯, right_inv := ⋯ }<VAR>Adual : (V →L[ℝ] ℝ) ≃L[ℝ] V' →L[ℝ] ℝ := { toLinearEquiv := Adualₗ, continuous_toFun := ⋯, continuous_invFun := ⋯ }<VAR>this : (Measure.map (⇑Aₘ) μ).IsAddHaarMeasure<GOAL>Tendsto (fun w => ∫ (v : V), 𝐞 (-w v) • f v ∂μ) (cocompact (V →L[ℝ] ℝ)) (𝓝 0)