ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁵ : RCLike 𝕜<VAR>inst✝¹⁴ : NormedAddCommGroup F<VAR>inst✝¹³ : NormedSpace 𝕜 F<VAR>inst✝¹² : NormedAddCommGroup F'<VAR>inst✝¹¹ : NormedSpace 𝕜 F'<VAR>inst✝¹⁰ : NormedSpace ℝ F'<VAR>inst✝⁹ : CompleteSpace F'<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedAddCommGroup G'<VAR>inst✝⁶ : NormedSpace ℝ G'<VAR>inst✝⁵ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝⁴ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝³ : SigmaFinite (μ.trim hm)<VAR>E : Type u_8<VAR>inst✝² : NormedLatticeAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : OrderedSMul ℝ E<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E<VAR>hx : 0 ≤ x<GOAL>↑↑0 ≤ᶠ[ae μ] ↑↑(condexpIndSMul hm hs hμs x)
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>f : Perm (Fin n)<VAR>x✝ : (_ : Fin n) × Fin n<VAR>a b : Fin n<VAR>hab : ⟨a, b⟩ ∈ finPairsLT n<VAR>h : f⁻¹ b < f⁻¹ a<GOAL>(if f⁻¹ ⟨a, b⟩.fst ≤ f⁻¹ ⟨a, b⟩.snd then -1 else 1) = if f (f⁻¹.signBijAux ⟨a, b⟩).fst ≤ f (f⁻¹.signBijAux ⟨a, b⟩).snd then -1 else 1
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>f : Perm (Fin n)<VAR>x✝ : (_ : Fin n) × Fin n<VAR>a b : Fin n<VAR>hab : ⟨a, b⟩ ∈ finPairsLT n<VAR>h : ¬f⁻¹ b < f⁻¹ a<GOAL>(if f⁻¹ ⟨a, b⟩.fst ≤ f⁻¹ ⟨a, b⟩.snd then -1 else 1) = if f (f⁻¹.signBijAux ⟨a, b⟩).fst ≤ f (f⁻¹.signBijAux ⟨a, b⟩).snd then -1 else 1
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<VAR>s t : Set ((i : ι) → α i)<VAR>hs : s ∈ measurableCylinders α<GOAL>sᶜ ∈ measurableCylinders α
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<VAR>s t : Set ((i : ι) → α i)<VAR>hs : ∃ s_1 S, MeasurableSet S ∧ s = cylinder s_1 S<GOAL>∃ s_1 S, MeasurableSet S ∧ sᶜ = cylinder s_1 S
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<VAR>t : Set ((i : ι) → α i)<VAR>s : Finset ι<VAR>S : Set ((i : { x // x ∈ s }) → α ↑i)<VAR>hS : MeasurableSet S<GOAL>∃ s_1 S_1, MeasurableSet S_1 ∧ (cylinder s S)ᶜ = cylinder s_1 S_1
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<VAR>t : Set ((i : ι) → α i)<VAR>s : Finset ι<VAR>S : Set ((i : { x // x ∈ s }) → α ↑i)<VAR>hS : MeasurableSet S<GOAL>(cylinder s S)ᶜ = cylinder s Sᶜ
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>n : ℕ<VAR>M : Fin n → Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>inst✝⁴ : (i : Fin n) → AddCommMonoid (M i)<VAR>inst✝³ : (i : Fin n) → Module R (M i)<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module R M₃<VAR>inst✝ : Finite ι<VAR>f g : MultilinearMap R (fun x => M₂) M₃<VAR>ι₁ : Type u_6<VAR>e : Basis ι₁ R M₂<VAR>h : ∀ (v : ι → ι₁), (f fun i => e (v i)) = g fun i => e (v i)<GOAL>f = g
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>n : ℕ<VAR>M : Fin n → Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>inst✝⁴ : (i : Fin n) → AddCommMonoid (M i)<VAR>inst✝³ : (i : Fin n) → Module R (M i)<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module R M₃<VAR>inst✝ : Finite ι<VAR>f g : MultilinearMap R (fun x => M₂) M₃<VAR>ι₁ : Type u_6<VAR>e : Basis ι₁ R M₂<VAR>h : ∀ (v : ι → ι₁), (f fun i => e (v i)) = g fun i => e (v i)<VAR>val✝ : Fintype ι<GOAL>f = g
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝ : CommMonoid β<VAR>u : ℕ → β<VAR>N : ℕ<VAR>hu : ∀ n ≥ N, u n = 1<VAR>n : ℕ<VAR>hn : N ≤ n<GOAL>∏ k ∈ range n, u k = ∏ k ∈ range N, u k
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝ : CommMonoid β<VAR>u : ℕ → β<VAR>N : ℕ<VAR>hu : ∀ n ≥ N, u n = 1<VAR>m : ℕ<VAR>hn : N ≤ N + m<GOAL>∏ k ∈ range (N + m), u k = ∏ k ∈ range N, u k
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : LocalRing R<VAR>T : Type u<VAR>inst✝¹ : CommRing T<VAR>inst✝ : LocalRing T<VAR>x : PrimeSpectrum (ResidueField T)<GOAL>(PrimeSpectrum.comap (residue T)) x = closedPoint T
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : LocalRing R<VAR>T : Type u<VAR>inst✝¹ : CommRing T<VAR>inst✝ : LocalRing T<VAR>x : PrimeSpectrum (ResidueField T)<GOAL>(PrimeSpectrum.comap (residue T)) ⊥ = closedPoint T
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : LocalRing R<VAR>T : Type u<VAR>inst✝¹ : CommRing T<VAR>inst✝ : LocalRing T<VAR>x : PrimeSpectrum (ResidueField T)<GOAL>((PrimeSpectrum.comap (residue T)) ⊥).asIdeal = (closedPoint T).asIdeal
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>p : X × Y → Prop<VAR>x : X<VAR>y : Y<VAR>h : ∀ᶠ (x : X × Y) in 𝓝 (x, y), p x<GOAL>∀ᶠ (x' : X) in 𝓝 x, ∀ᶠ (y' : Y) in 𝓝 y, p (x', y')
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>p : X × Y → Prop<VAR>x : X<VAR>y : Y<VAR>h : ∀ᶠ (x : X × Y) in 𝓝 x ×ˢ 𝓝 y, p x<GOAL>∀ᶠ (x' : X) in 𝓝 x, ∀ᶠ (y' : Y) in 𝓝 y, p (x', y')
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s✝ t : Set α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>s : Set α<VAR>h : (f '' s).Finite<VAR>hs : s.Nonempty<GOAL>∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s✝ t : Set α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>s : Set α<VAR>h : (f '' s).Finite<VAR>hs : s.Nonempty<VAR>a : α<VAR>ha : a ∈ s<VAR>hmax : ∀ a' ∈ f '' s, id (f a) ≤ id a' → id (f a) = id a'<GOAL>∃ a ∈ s, ∀ a' ∈ s, f a ≤ f a' → f a = f a'
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<VAR>e : E<GOAL>∫ (x : X), ↑↑(indicatorConstLp p ht hμt e) x ∂μ = ∫ (x : X) in univ, ↑↑(indicatorConstLp p ht hμt e) x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<VAR>e : E<GOAL>(μ (t ∩ univ)).toReal • e = (μ t).toReal • e
<VAR>G : Type u_1<VAR>inst✝¹⁰ : TopologicalSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : TopologicalGroup G<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝⁴ : μ.IsHaarMeasure<VAR>inst✝³ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝² : μ'.IsMulLeftInvariant<VAR>inst✝¹ : μ.InnerRegular<VAR>inst✝ : μ'.InnerRegular<VAR>s : Set G<VAR>hs : MeasurableSet s<GOAL>μ' s = (μ'.haarScalarFactor μ • μ) s
<VAR>G : Type u_1<VAR>inst✝¹⁰ : TopologicalSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : TopologicalGroup G<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝⁴ : μ.IsHaarMeasure<VAR>inst✝³ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝² : μ'.IsMulLeftInvariant<VAR>inst✝¹ : μ.InnerRegular<VAR>inst✝ : μ'.InnerRegular<VAR>s : Set G<VAR>hs : MeasurableSet s<GOAL>⨆ K, ⨆ (_ : K ⊆ s), ⨆ (_ : IsCompact K), μ' K = ⨆ K, ⨆ (_ : K ⊆ s), ⨆ (_ : IsCompact K), (μ'.haarScalarFactor μ • μ) K
<VAR>G : Type u_1<VAR>inst✝¹⁰ : TopologicalSpace G<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : TopologicalGroup G<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝⁴ : μ.IsHaarMeasure<VAR>inst✝³ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝² : μ'.IsMulLeftInvariant<VAR>inst✝¹ : μ.InnerRegular<VAR>inst✝ : μ'.InnerRegular<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>K : Set G<VAR>_Ks : K ⊆ s<VAR>K_comp : IsCompact K<GOAL>μ' K = (μ'.haarScalarFactor μ • μ) K
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>x : α<GOAL>𝓝 (pure x) = 𝓟 {⊥, pure x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → α<VAR>g : β → β<VAR>n : ℕ<GOAL>(map f g)^[n] = map f^[n] g^[n]
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f g : Filter α<VAR>s✝ t✝ s t : Set α<GOAL>𝓟 s ⊓ 𝓟 t ≤ 𝓟 (s ∩ t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f g : Filter α<VAR>s✝ t✝ s t : Set α<GOAL>∃ t₁ ∈ 𝓟 s, ∃ t₂ ∈ 𝓟 t, s ∩ t = t₁ ∩ t₂
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f g : Filter α<VAR>s✝ t✝ s t : Set α<GOAL>𝓟 (s ∩ t) ≤ 𝓟 s ⊓ 𝓟 t
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<VAR>n : ℤ<GOAL>QuasiIsoAt (descShortComplex S) n
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<VAR>n : ℤ<GOAL>IsIso (HomologicalComplex.homologyMap (descShortComplex S) n)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<VAR>n : ℤ<VAR>φ : ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅ (triangleh S.f) n (n + 1) ⋯).δlast ⟶ (composableArrows₅ hS n (n + 1) ⋯).δlast := homMk₄ ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₁) ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₂) ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₃ ≫ HomologicalComplex.homologyMap (descShortComplex S) n) ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app (triangle S.f).obj₁) ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app (triangle S.f).obj₂) ⋯ ⋯ ⋯ ⋯<GOAL>IsIso (HomologicalComplex.homologyMap (descShortComplex S) n)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<VAR>n : ℤ<VAR>φ : ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅ (triangleh S.f) n (n + 1) ⋯).δlast ⟶ (composableArrows₅ hS n (n + 1) ⋯).δlast := homMk₄ ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₁) ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₂) ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₃ ≫ HomologicalComplex.homologyMap (descShortComplex S) n) ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app (triangle S.f).obj₁) ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app (triangle S.f).obj₂) ⋯ ⋯ ⋯ ⋯<VAR>this : IsIso ((homologyFunctorFactors C (up ℤ) n).hom.app (mappingCone S.f) ≫ HomologicalComplex.homologyMap (descShortComplex S) n)<GOAL>IsIso (HomologicalComplex.homologyMap (descShortComplex S) n)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : Filter X<VAR>s t s₁ s₂ t₁ t₂ : Set X<VAR>x : X<GOAL>s ⊆ interior t ↔ t ∈ 𝓝ˢ s
<VAR>α : Type u<VAR>inst✝ : MetricSpace α<GOAL>LipschitzWith 2 fun p => infDist p.1 ↑p.2
<VAR>α : Type u<VAR>inst✝ : MetricSpace α<GOAL>2 = 1 + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : DistribLattice α<VAR>inst✝² : LinearOrderedCommSemiring β<VAR>inst✝¹ : ExistsAddOfLE β<VAR>f f₁ f₂ f₃ f₄ g μ : α → β<VAR>inst✝ : Fintype α<VAR>hμ₀ : 0 ≤ μ<VAR>hf₀ : 0 ≤ f<VAR>hg₀ : 0 ≤ g<VAR>hf : Monotone f<VAR>hg : Monotone g<VAR>hμ : ∀ (a b : α), μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)<GOAL>(∑ a : α, μ a * f a) * ∑ a : α, μ a * g a ≤ (∑ a : α, μ a) * ∑ a : α, μ a * (f a * g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : DistribLattice α<VAR>inst✝² : LinearOrderedCommSemiring β<VAR>inst✝¹ : ExistsAddOfLE β<VAR>f f₁ f₂ f₃ f₄ g μ : α → β<VAR>inst✝ : Fintype α<VAR>hμ₀ : 0 ≤ μ<VAR>hf₀ : 0 ≤ f<VAR>hg₀ : 0 ≤ g<VAR>hf : Monotone f<VAR>hg : Monotone g<VAR>hμ : ∀ (a b : α), μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)<VAR>a b : α<GOAL>(μ * f) a * (μ * g) b ≤ μ (a ⊓ b) * (μ (a ⊔ b) * (f (a ⊔ b) * g (a ⊔ b)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : DistribLattice α<VAR>inst✝² : LinearOrderedCommSemiring β<VAR>inst✝¹ : ExistsAddOfLE β<VAR>f f₁ f₂ f₃ f₄ g μ : α → β<VAR>inst✝ : Fintype α<VAR>hμ₀ : 0 ≤ μ<VAR>hf₀ : 0 ≤ f<VAR>hg₀ : 0 ≤ g<VAR>hf : Monotone f<VAR>hg : Monotone g<VAR>hμ : ∀ (a b : α), μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)<VAR>a b : α<GOAL>μ a * f a * (μ b * g b) ≤ μ (a ⊓ b) * (μ (a ⊔ b) * (f (a ⊔ b) * g (a ⊔ b)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : DistribLattice α<VAR>inst✝² : LinearOrderedCommSemiring β<VAR>inst✝¹ : ExistsAddOfLE β<VAR>f f₁ f₂ f₃ f₄ g μ : α → β<VAR>inst✝ : Fintype α<VAR>hμ₀ : 0 ≤ μ<VAR>hf₀ : 0 ≤ f<VAR>hg₀ : 0 ≤ g<VAR>hf : Monotone f<VAR>hg : Monotone g<VAR>hμ : ∀ (a b : α), μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)<VAR>a b : α<GOAL>μ a * μ b * (f a * g b) ≤ μ (a ⊓ b) * μ (a ⊔ b) * (f (a ⊔ b) * g (a ⊔ b))
<VAR>a b : ℕ<VAR>ha : Odd a<VAR>hb : Odd b<GOAL>J(↑a | b) = qrSign b a * J(↑b | a)
<VAR>a b : ℕ<VAR>ha : Odd a<VAR>hb : Odd b<VAR>rhs : ℕ → ℕ →* ℤ := fun a => { toFun := fun x => qrSign x a * J(↑x | a), map_one' := ⋯, map_mul' := ⋯ }<GOAL>J(↑a | b) = qrSign b a * J(↑b | a)
<VAR>a b : ℕ<VAR>ha : Odd a<VAR>hb : Odd b<VAR>rhs : ℕ → ℕ →* ℤ := fun a => { toFun := fun x => qrSign x a * J(↑x | a), map_one' := ⋯, map_mul' := ⋯ }<VAR>rhs_apply : ∀ (a b : ℕ), (rhs a) b = qrSign b a * J(↑b | a)<GOAL>J(↑a | b) = qrSign b a * J(↑b | a)
<VAR>a b : ℕ<VAR>ha : Odd a<VAR>hb : Odd b<VAR>rhs : ℕ → ℕ →* ℤ := fun a => { toFun := fun x => qrSign x a * J(↑x | a), map_one' := ⋯, map_mul' := ⋯ }<VAR>rhs_apply : ∀ (a b : ℕ), (rhs a) b = qrSign b a * J(↑b | a)<VAR>p : ℕ<VAR>pp : Nat.Prime p<VAR>hp : p ≠ 2<GOAL>(rhs a) ↑p = legendreSym p ↑a
<VAR>a b : ℕ<VAR>ha : Odd a<VAR>hb : Odd b<VAR>rhs : ℕ → ℕ →* ℤ := fun a => { toFun := fun x => qrSign x a * J(↑x | a), map_one' := ⋯, map_mul' := ⋯ }<VAR>rhs_apply : ∀ (a b : ℕ), (rhs a) b = qrSign b a * J(↑b | a)<VAR>p : ℕ<VAR>pp : Nat.Prime p<VAR>hp : p ≠ 2<VAR>hpo : Odd p<GOAL>(rhs a) ↑p = legendreSym p ↑a
<VAR>a b : ℕ<VAR>ha : Odd a<VAR>hb : Odd b<VAR>rhs : ℕ → ℕ →* ℤ := fun a => { toFun := fun x => qrSign x a * J(↑x | a), map_one' := ⋯, map_mul' := ⋯ }<VAR>rhs_apply : ∀ (a b : ℕ), (rhs a) b = qrSign b a * J(↑b | a)<VAR>p : ℕ<VAR>pp : Nat.Prime p<VAR>hp : p ≠ 2<VAR>hpo : Odd p<GOAL>J(↑p | a) = qrSign a p * J(↑a | p)
<VAR>a b : ℕ<VAR>ha : Odd a<VAR>hb : Odd b<VAR>rhs : ℕ → ℕ →* ℤ := fun a => { toFun := fun x => qrSign x a * J(↑x | a), map_one' := ⋯, map_mul' := ⋯ }<VAR>rhs_apply : ∀ (a b : ℕ), (rhs a) b = qrSign b a * J(↑b | a)<VAR>p : ℕ<VAR>pp : Nat.Prime p<VAR>hp : p ≠ 2<VAR>hpo : Odd p<VAR>q : ℕ<VAR>pq : Nat.Prime q<VAR>hq : q ≠ 2<GOAL>legendreSym q ↑p = (rhs p) ↑q
<VAR>a b : ℕ<VAR>ha : Odd a<VAR>hb : Odd b<VAR>rhs : ℕ → ℕ →* ℤ := fun a => { toFun := fun x => qrSign x a * J(↑x | a), map_one' := ⋯, map_mul' := ⋯ }<VAR>rhs_apply : ∀ (a b : ℕ), (rhs a) b = qrSign b a * J(↑b | a)<VAR>p : ℕ<VAR>pp : Nat.Prime p<VAR>hp : p ≠ 2<VAR>hpo : Odd p<VAR>q : ℕ<VAR>pq : Nat.Prime q<VAR>hq : q ≠ 2<VAR>hqo : Odd q<GOAL>legendreSym q ↑p = (rhs p) ↑q
<VAR>ι✝ : Type u_1<VAR>κ✝ : Type u_2<VAR>α✝ : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝¹ s₁ s₂ : Finset α✝<VAR>a : α✝<VAR>f✝¹ g✝¹ : α✝ → β<VAR>inst✝² : CommMonoid β<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>inst✝¹ : CommMonoid α<VAR>s✝ : Finset ι<VAR>t✝ : Finset κ<VAR>f✝ : ι → α<VAR>g✝ : κ → α<VAR>inst✝ : DecidableEq κ<VAR>s : Finset ι<VAR>t : Finset κ<VAR>g : ι → κ<VAR>f : κ → α<GOAL>∏ j ∈ t, ∏ _i ∈ filter (fun i => g i = j) s, f j = ∏ i ∈ filter (fun i => g i ∈ t) s, f (g i)
<VAR>n : ℕ<VAR>hn : 0 < n<VAR>s : ℝ<VAR>hs : 0 < s<GOAL>IntervalIntegrable (fun x => (x - ↑n) / x ^ (s + 1)) volume (↑n) (↑n + 1)
<VAR>n : ℕ<VAR>hn : 0 < n<VAR>s : ℝ<VAR>hs : 0 < s<GOAL>IntegrableOn (fun x => (x - ↑n) / x ^ (s + 1)) (Icc (↑n) (↑n + 1)) volume
<VAR>n : ℕ<VAR>hn : 0 < n<VAR>s : ℝ<VAR>hs : 0 < s<VAR>x : ℝ<VAR>hx : x ∈ Icc (↑n) (↑n + 1)<GOAL>ContinuousAt (fun x => x - ↑n) x
<VAR>n : ℕ<VAR>hn : 0 < n<VAR>s : ℝ<VAR>hs : 0 < s<VAR>x : ℝ<VAR>hx : x ∈ Icc (↑n) (↑n + 1)<GOAL>ContinuousAt (fun x => x ^ (s + 1)) x
<VAR>n : ℕ<VAR>hn : 0 < n<VAR>s : ℝ<VAR>hs : 0 < s<VAR>x : ℝ<VAR>hx : x ∈ Icc (↑n) (↑n + 1)<GOAL>x ^ (s + 1) ≠ 0
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : HasLimits C<VAR>X : TopCat<VAR>F : J ⥤ Presheaf C X<VAR>H : ∀ (j : J), (F.obj j).IsSheaf<VAR>c : Cone F<VAR>hc : IsLimit c<VAR>F' : J ⥤ Sheaf C X := { obj := fun j => { val := F.obj j, cond := ⋯ }, map := fun {X_1 Y} f => { val := F.map f }, map_id := ⋯, map_comp := ⋯ }<VAR>e : F' ⋙ Sheaf.forget C X ≅ F := NatIso.ofComponents (fun x => Iso.refl ((F' ⋙ Sheaf.forget C X).obj x)) ⋯<GOAL>c.pt.IsSheaf
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<GOAL>T_gen p F a < 1
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>h : ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2 < 1<GOAL>T_gen p F a < 1
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>h : ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2 < 1<GOAL>‖Polynomial.eval a F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2 < 1
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n x y : A<GOAL>x ∈ map ((LinearMap.mul R A).flip y) P ↔ ∃ z ∈ P, Mul.mul z y = x
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝⁴ : DecidableEq o<VAR>inst✝³ : Zero α<VAR>inst✝² : Zero β<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : One α<GOAL>(blockDiagonal fun x => diagonal fun x => 1) = diagonal fun x => 1
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t : Set α<VAR>h : 0 < ε<GOAL>x ∈ ball x ε
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>a : S<GOAL>1 ⊗ₜ[R] a - a ⊗ₜ[R] 1 ∈ ideal R S
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n : ℕ<GOAL>∃ q, (of v).convs n = ↑q
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n : ℕ<VAR>Aₙ : ℚ<VAR>nth_num_eq : (of v).nums n = ↑Aₙ<GOAL>∃ q, (of v).convs n = ↑q
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n : ℕ<VAR>Aₙ : ℚ<VAR>nth_num_eq : (of v).nums n = ↑Aₙ<VAR>Bₙ : ℚ<VAR>nth_den_eq : (of v).dens n = ↑Bₙ<GOAL>∃ q, (of v).convs n = ↑q
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n : ℕ<VAR>Aₙ : ℚ<VAR>nth_num_eq : (of v).nums n = ↑Aₙ<VAR>Bₙ : ℚ<VAR>nth_den_eq : (of v).dens n = ↑Bₙ<GOAL>(of v).convs n = ↑(Aₙ / Bₙ)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>h's : μ s ≠ ⊤<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<GOAL>∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ μ (f '' s)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>h's : μ s ≠ ⊤<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>this : Tendsto (fun ε => μ (f '' s) + 2 * ↑ε * μ s) (𝓝[>] 0) (𝓝 (μ (f '' s) + 2 * ↑0 * μ s))<GOAL>∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ μ (f '' s)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>h's : μ s ≠ ⊤<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>this : Tendsto (fun ε => μ (f '' s) + 2 * ↑ε * μ s) (𝓝[>] 0) (𝓝 (μ (f '' s)))<GOAL>∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ μ (f '' s)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>h's : μ s ≠ ⊤<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>this : Tendsto (fun ε => μ (f '' s) + 2 * ↑ε * μ s) (𝓝[>] 0) (𝓝 (μ (f '' s)))<GOAL>∀ᶠ (c : ℝ≥0) in 𝓝[>] 0, ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ μ (f '' s) + 2 * ↑c * μ s
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>h's : μ s ≠ ⊤<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>this : Tendsto (fun ε => μ (f '' s) + 2 * ↑ε * μ s) (𝓝[>] 0) (𝓝 (μ (f '' s)))<GOAL>∀ a ∈ Ioi 0, ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ μ (f '' s) + 2 * ↑a * μ s
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>h's : μ s ≠ ⊤<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>this : Tendsto (fun ε => μ (f '' s) + 2 * ↑ε * μ s) (𝓝[>] 0) (𝓝 (μ (f '' s)))<VAR>ε : ℝ≥0<VAR>εpos : ε ∈ Ioi 0<GOAL>∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ μ (f '' s) + 2 * ↑ε * μ s
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>h's : μ s ≠ ⊤<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>hf : InjOn f s<VAR>this : Tendsto (fun ε => μ (f '' s) + 2 * ↑ε * μ s) (𝓝[>] 0) (𝓝 (μ (f '' s)))<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<GOAL>∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ μ (f '' s) + 2 * ↑ε * μ s