ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>a p : Associates α<VAR>hp : Irreducible p<VAR>inst✝ : (n : ℕ) → Decidable (a ∣ p ^ n)<VAR>n : ℕ<VAR>h : a ∣ p ^ n<GOAL>a ∣ p ^ ?m.494287
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>a p : Associates α<VAR>hp : Irreducible p<VAR>inst✝ : (n : ℕ) → Decidable (a ∣ p ^ n)<VAR>n : ℕ<VAR>h : a ∣ p ^ n<GOAL>ℕ
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>b : Basis ι ℝ E<VAR>inst✝ : Fintype ι<GOAL>fundamentalDomain b ⊆ parallelepiped ⇑b
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>b : Basis ι ℝ E<VAR>inst✝ : Fintype ι<GOAL>∀ (a : E), (∀ (i : ι), (b.repr a) i ∈ Set.Ico 0 1) → ∀ (i : ι), (b.repr a) i ∈ Set.Icc 0 1
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>inst✝ : LieModule.IsTrivial L M<GOAL>⁅I, N⁆ = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>inst✝ : LieModule.IsTrivial L M<GOAL>⁅I, N⁆ ≤ ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>inst✝ : LieModule.IsTrivial L M<GOAL>{m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>inst✝ : LieModule.IsTrivial L M<VAR>m : M<VAR>x : ↥I<VAR>n : ↥N<VAR>h : ⁅↑x, ↑n⁆ = m<GOAL>m ∈ ↑⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>inst✝ : LieModule.IsTrivial L M<VAR>m : M<VAR>x : ↥I<VAR>n : ↥N<VAR>h : 0 = m<GOAL>m ∈ ↑⊥
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>n : ℕ<VAR>h : 2 ≤ n<GOAL>dickson k a n = X * dickson k a (n - 1) - C a * dickson k a (n - 2)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>n : ℕ<VAR>h : 2 ≤ 2 + n<GOAL>dickson k a (2 + n) = X * dickson k a (2 + n - 1) - C a * dickson k a (2 + n - 2)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>n : ℕ<VAR>h : 2 ≤ 2 + n<GOAL>dickson k a (n + 2) = X * dickson k a (n + 2 - 1) - C a * dickson k a (n + 2 - 2)
<VAR>m n a✝ b✝ c d : ℤ<VAR>a b : ℕ<VAR>hab : a.Coprime b<VAR>hgcd : a.gcd b = 1<GOAL>↑a * a.gcdA b + ↑b * a.gcdB b ≡ 1 [ZMOD ↑b]
<VAR>m n a✝ b✝ c d : ℤ<VAR>a b : ℕ<VAR>hab : a.Coprime b<VAR>hgcd : a.gcd b = 1<GOAL>↑1 ≡ 1 [ZMOD ↑b]
<VAR>ι : Type u_1<VAR>inst✝¹⁴ : Fintype ι<VAR>A : ι → Type u_2<VAR>inst✝¹³ : (i : ι) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι) → Measure (A i)<VAR>inst✝¹² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : MeasurableSpace E<VAR>inst✝⁶ : BorelSpace E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝⁴ : μ.IsAddHaarMeasure<VAR>F' : Type u_5<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : CompleteSpace F'<VAR>inst✝ : FiniteDimensional ℝ F<VAR>u : E → F<VAR>s : Set E<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : support u ⊆ s<VAR>p : ℝ≥0<VAR>hp : 1 ≤ p<VAR>h2p : p < ↑(finrank ℝ E)<VAR>hs : Bornology.IsBounded s<GOAL>eLpNorm u (↑p) μ ≤ ↑(eLpNormLESNormFDerivOfLeConst F μ s p p) * eLpNorm (fderiv ℝ u) (↑p) μ
<VAR>ι : Type u_1<VAR>inst✝¹⁴ : Fintype ι<VAR>A : ι → Type u_2<VAR>inst✝¹³ : (i : ι) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι) → Measure (A i)<VAR>inst✝¹² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : MeasurableSpace E<VAR>inst✝⁶ : BorelSpace E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝⁴ : μ.IsAddHaarMeasure<VAR>F' : Type u_5<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : CompleteSpace F'<VAR>inst✝ : FiniteDimensional ℝ F<VAR>u : E → F<VAR>s : Set E<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : support u ⊆ s<VAR>p : ℝ≥0<VAR>hp : 1 ≤ p<VAR>h2p : p < ↑(finrank ℝ E)<VAR>hs : Bornology.IsBounded s<GOAL>↑p⁻¹ - (↑(finrank ℝ E))⁻¹ ≤ (↑p)⁻¹
<VAR>ι : Type u_1<VAR>inst✝¹⁴ : Fintype ι<VAR>A : ι → Type u_2<VAR>inst✝¹³ : (i : ι) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι) → Measure (A i)<VAR>inst✝¹² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : MeasurableSpace E<VAR>inst✝⁶ : BorelSpace E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝⁴ : μ.IsAddHaarMeasure<VAR>F' : Type u_5<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : CompleteSpace F'<VAR>inst✝ : FiniteDimensional ℝ F<VAR>u : E → F<VAR>s : Set E<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : support u ⊆ s<VAR>p : ℝ≥0<VAR>hp : 1 ≤ p<VAR>h2p : p < ↑(finrank ℝ E)<VAR>hs : Bornology.IsBounded s<GOAL>↑p⁻¹ - (↑(finrank ℝ E))⁻¹ ≤ ↑p⁻¹
<VAR>ι : Type u_1<VAR>inst✝¹⁴ : Fintype ι<VAR>A : ι → Type u_2<VAR>inst✝¹³ : (i : ι) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι) → Measure (A i)<VAR>inst✝¹² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : MeasurableSpace E<VAR>inst✝⁶ : BorelSpace E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝⁴ : μ.IsAddHaarMeasure<VAR>F' : Type u_5<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : CompleteSpace F'<VAR>inst✝ : FiniteDimensional ℝ F<VAR>u : E → F<VAR>s : Set E<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : support u ⊆ s<VAR>p : ℝ≥0<VAR>hp : 1 ≤ p<VAR>h2p : p < ↑(finrank ℝ E)<VAR>hs : Bornology.IsBounded s<GOAL>0 ≤ (↑(finrank ℝ E))⁻¹
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>w : InfinitePlace K<VAR>x : K<GOAL>(normAtPlace w) ((mixedEmbedding K) x) = w x
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>f : α → ℝ<GOAL>((fun x => rexp (f x)) =O[l] fun x => 1) ↔ IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>inst✝ : DecidableEq α<VAR>x : FreeGroup α<GOAL>x⁻¹.norm = x.norm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>r : ℚ<VAR>inst✝ : IsFiniteMeasure ρ<GOAL>∫ (x : α), (preCDF ρ r x).toReal ∂ρ.fst = ((ρ.IicSnd ↑r) univ).toReal
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : Preorder α<VAR>t : OrderTopology α<VAR>s : Set α<GOAL>IsOpen s ↔ GenerateOpen {s | ∃ a, s = Ioi a ∨ s = Iio a} s
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : Ω → ℝ<VAR>hint : Integrable X ℙ<VAR>hnonneg : 0 ≤ X<GOAL>∑' (j : ℕ), ℙ {ω | X ω ∈ Set.Ioi ↑j} < ⊤
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : Ω → ℝ<VAR>hint : Integrable X ℙ<VAR>hnonneg : 0 ≤ X<GOAL>∀ (K : ℕ), ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioi ↑j} ≤ ENNReal.ofReal ((∫ (a : Ω), X a) + 1)
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : Ω → ℝ<VAR>hint : Integrable X ℙ<VAR>hnonneg : 0 ≤ X<VAR>K : ℕ<VAR>A : Tendsto (fun N => ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N}) atTop (𝓝 (∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioi ↑j}))<GOAL>∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioi ↑j} ≤ ENNReal.ofReal ((∫ (a : Ω), X a) + 1)
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : Ω → ℝ<VAR>hint : Integrable X ℙ<VAR>hnonneg : 0 ≤ X<VAR>K : ℕ<VAR>A : Tendsto (fun N => ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N}) atTop (𝓝 (∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioi ↑j}))<GOAL>(fun N => ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N}) ≤ᶠ[atTop] fun x => ENNReal.ofReal ((∫ (a : Ω), X a) + 1)
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : Ω → ℝ<VAR>hint : Integrable X ℙ<VAR>hnonneg : 0 ≤ X<VAR>K : ℕ<VAR>A : Tendsto (fun N => ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N}) atTop (𝓝 (∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioi ↑j}))<VAR>N : ℕ<VAR>hN : N ∈ Set.Ici K<GOAL>∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N} ≤ ENNReal.ofReal ((∫ (a : Ω), X a) + 1)
<VAR>p : ℕ<VAR>hp : 1 < p<GOAL>padicNorm p ↑p < 1
<VAR>p : ℕ<VAR>hp : 1 < p<GOAL>↑p ≤ 0 ∨ 1 < ↑p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>f : α → β → ℝ≥0∞<VAR>κ : Kernel α β<VAR>inst✝ : IsFiniteKernel κ<VAR>hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤<VAR>hf : Measurable (Function.uncurry f)<VAR>fs : ℕ → α → β → ℝ≥0∞ := fun n a b => min (f a b) (↑n + 1) - min (f a b) ↑n<VAR>h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n<GOAL>IsSFiniteKernel (κ.withDensity f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>f : α → β → ℝ≥0∞<VAR>κ : Kernel α β<VAR>inst✝ : IsFiniteKernel κ<VAR>hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤<VAR>hf : Measurable (Function.uncurry f)<VAR>fs : ℕ → α → β → ℝ≥0∞ := fun n a b => min (f a b) (↑n + 1) - min (f a b) ↑n<VAR>h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n<VAR>h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0<GOAL>IsSFiniteKernel (κ.withDensity f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>f : α → β → ℝ≥0∞<VAR>κ : Kernel α β<VAR>inst✝ : IsFiniteKernel κ<VAR>hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤<VAR>hf : Measurable (Function.uncurry f)<VAR>fs : ℕ → α → β → ℝ≥0∞ := fun n a b => min (f a b) (↑n + 1) - min (f a b) ↑n<VAR>h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n<VAR>h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0<VAR>hf_eq_tsum : f = ∑' (n : ℕ), fs n<GOAL>IsSFiniteKernel (κ.withDensity f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>f : α → β → ℝ≥0∞<VAR>κ : Kernel α β<VAR>inst✝ : IsFiniteKernel κ<VAR>hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤<VAR>hf : Measurable (Function.uncurry f)<VAR>fs : ℕ → α → β → ℝ≥0∞ := fun n a b => min (f a b) (↑n + 1) - min (f a b) ↑n<VAR>h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n<VAR>h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0<VAR>hf_eq_tsum : f = ∑' (n : ℕ), fs n<GOAL>IsSFiniteKernel (Kernel.sum fun n => κ.withDensity (fs n))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>f : α → β → ℝ≥0∞<VAR>κ : Kernel α β<VAR>inst✝ : IsFiniteKernel κ<VAR>hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤<VAR>hf : Measurable (Function.uncurry f)<VAR>fs : ℕ → α → β → ℝ≥0∞ := fun n a b => min (f a b) (↑n + 1) - min (f a b) ↑n<VAR>h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n<VAR>h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0<VAR>hf_eq_tsum : f = ∑' (n : ℕ), fs n<GOAL>∀ (n : ℕ), Measurable (Function.uncurry (fs n))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>f : α → β → ℝ≥0∞<VAR>κ : Kernel α β<VAR>inst✝ : IsFiniteKernel κ<VAR>hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤<VAR>hf : Measurable (Function.uncurry f)<VAR>fs : ℕ → α → β → ℝ≥0∞ := fun n a b => min (f a b) (↑n + 1) - min (f a b) ↑n<VAR>h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n<VAR>h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0<VAR>hf_eq_tsum : f = ∑' (n : ℕ), fs n<VAR>n : ℕ<GOAL>IsSFiniteKernel (κ.withDensity (fs n))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>f : α → β → ℝ≥0∞<VAR>κ : Kernel α β<VAR>inst✝ : IsFiniteKernel κ<VAR>hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤<VAR>hf : Measurable (Function.uncurry f)<VAR>fs : ℕ → α → β → ℝ≥0∞ := fun n a b => min (f a b) (↑n + 1) - min (f a b) ↑n<VAR>h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n<VAR>h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0<VAR>hf_eq_tsum : f = ∑' (n : ℕ), fs n<VAR>n : ℕ<GOAL>IsFiniteKernel (κ.withDensity (fs n))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>f : α → β → ℝ≥0∞<VAR>κ : Kernel α β<VAR>inst✝ : IsFiniteKernel κ<VAR>hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤<VAR>hf : Measurable (Function.uncurry f)<VAR>fs : ℕ → α → β → ℝ≥0∞ := fun n a b => min (f a b) (↑n + 1) - min (f a b) ↑n<VAR>h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n<VAR>h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0<VAR>hf_eq_tsum : f = ∑' (n : ℕ), fs n<VAR>n : ℕ<VAR>a : α<VAR>b : β<GOAL>fs n a b ≤ ↑((fun x x_1 => x + x_1) (↑n) 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>f : α → β → ℝ≥0∞<VAR>κ : Kernel α β<VAR>inst✝ : IsFiniteKernel κ<VAR>hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤<VAR>hf : Measurable (Function.uncurry f)<VAR>fs : ℕ → α → β → ℝ≥0∞ := fun n a b => min (f a b) (↑n + 1) - min (f a b) ↑n<VAR>h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n<VAR>h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0<VAR>hf_eq_tsum : f = ∑' (n : ℕ), fs n<VAR>n : ℕ<VAR>a : α<VAR>b : β<GOAL>fs n a b ≤ ↑(n + 1)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : MvPolynomial σ R<GOAL>(expand 1) f = f
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : LinearOrderedSemifield α<VAR>l : Filter β<VAR>f : β → α<VAR>r c : α<VAR>n : ℕ<VAR>hr : 0 < r<VAR>h : Tendsto f l atTop<GOAL>Tendsto (fun x => r⁻¹ * (r * f x)) l atTop
<VAR>n m l : ℕ<VAR>hnm : n ≤ m<VAR>hml : m ≤ l<GOAL>range' n (m - n) ++ range' m (l - m) = range' n (l - n)
<VAR>n m l : ℕ<VAR>hnm : n ≤ m<VAR>hml : m ≤ l<GOAL>range' m (l - m) = range' (n + 1 * (m - n)) (l - m)
<VAR>n m l : ℕ<VAR>hnm : n ≤ m<VAR>hml : m ≤ l<GOAL>l - n = l - m + (m - n)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : Distrib R<VAR>a b x y : R<VAR>ha : SemiconjBy a x y<VAR>hb : SemiconjBy b x y<GOAL>SemiconjBy (a + b) x y
<VAR>t t' : Type u → Type u<VAR>eqv : (α : Type u) → t α ≃ t' α<VAR>inst✝⁵ : Traversable t<VAR>inst✝⁴ : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : Applicative G<VAR>inst✝¹ : LawfulApplicative F<VAR>inst✝ : LawfulApplicative G<VAR>η : ApplicativeTransformation F G<VAR>α β γ : Type u<VAR>f : β → F γ<VAR>g : α → G β<VAR>x : t' α<GOAL>Equiv.traverse eqv (Comp.mk ∘ map f ∘ g) x = Comp.mk (Equiv.traverse eqv f <$> Equiv.traverse eqv g x)
<VAR>t t' : Type u → Type u<VAR>eqv : (α : Type u) → t α ≃ t' α<VAR>inst✝⁵ : Traversable t<VAR>inst✝⁴ : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : Applicative G<VAR>inst✝¹ : LawfulApplicative F<VAR>inst✝ : LawfulApplicative G<VAR>η : ApplicativeTransformation F G<VAR>α β γ : Type u<VAR>f : β → F γ<VAR>g : α → G β<VAR>x : t' α<GOAL>Comp.mk ((fun x => ⇑(eqv γ) <$> x) <$> traverse f <$> traverse g ((eqv α).symm x)) = Comp.mk (Equiv.traverse eqv f <$> Equiv.traverse eqv g x)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁴ : SeminormedGroup E<VAR>inst✝³ : SeminormedGroup F<VAR>inst✝² : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : SemilatticeSup α<VAR>u : α → E<GOAL>CauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ (m : α), N ≤ m → ∀ (n : α), N ≤ n → ‖u m / u n‖ < ε
<VAR>α : Type u<VAR>a : α<VAR>inst✝¹ : Group α<VAR>inst✝ : Fintype α<VAR>x : α<VAR>hx : orderOf x = Fintype.card α<GOAL>IsCyclic α
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝ : Monoid M<VAR>c : Con M<VAR>f : M → M<VAR>hf : ∀ (x : M), c (f x * x) 1<VAR>x y : M<VAR>h : c x y<GOAL>c (f x) (f y)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝ : Monoid M<VAR>c : Con M<VAR>f : M → M<VAR>x y : M<VAR>hf : ∀ (x : M), ↑(f x) * ↑x = 1<VAR>h : ↑x = ↑y<GOAL>↑(f x) = ↑(f y)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝ : Monoid M<VAR>c : Con M<VAR>f : M → M<VAR>x y : M<VAR>hf : ∀ (x : M), ↑(f x) * ↑x = 1<VAR>h : ↑x = ↑y<VAR>hf' : ∀ (x : M), ↑x * ↑(f x) = 1<GOAL>↑(f x) = ↑(f y)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝ : Monoid M<VAR>c : Con M<VAR>f : M → M<VAR>x y : M<VAR>hf : ∀ (x : M), ↑(f x) * ↑x = 1<VAR>h : ↑x = ↑y<VAR>hf' : ∀ (x : M), ↑x * ↑(f x) = 1<VAR>this : { val := ↑x, inv := ↑(f x), val_inv := ⋯, inv_val := ⋯ } = { val := ↑y, inv := ↑(f y), val_inv := ⋯, inv_val := ⋯ }<GOAL>↑(f x) = ↑(f y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → ℕ<GOAL>s.EquitableOn f ↔ ∃ b, ∀ a ∈ s, f a = b ∨ f a = b + 1
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<VAR>h_odd : Odd n<VAR>hlt : 1 < n<VAR>B : ℚ⟦X⟧ := PowerSeries.mk fun n => bernoulli' n / ↑n !<GOAL>(B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<VAR>h_odd : Odd n<VAR>hlt : 1 < n<VAR>B : ℚ⟦X⟧ := PowerSeries.mk fun n => bernoulli' n / ↑n !<VAR>h : B * (exp ℚ - 1) = X * exp ℚ<GOAL>(B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<VAR>h_odd : Odd n<VAR>hlt : 1 < n<VAR>B : ℚ⟦X⟧ := PowerSeries.mk fun n => bernoulli' n / ↑n !<VAR>h : B * (exp ℚ - 1) = X * exp ℚ<GOAL>evalNegHom B * (1 - exp ℚ) = -(X * 1)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<VAR>h_odd : Odd n<VAR>hlt : 1 < n<VAR>B : ℚ⟦X⟧ := PowerSeries.mk fun n => bernoulli' n / ↑n !<VAR>h : B * (exp ℚ - 1) = X * exp ℚ<GOAL>evalNegHom (B * (exp ℚ - 1)) * exp ℚ = evalNegHom (X * exp ℚ) * exp ℚ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h : min c d < b<GOAL>Iio b ∪ Ioo c d = Iio (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>hcd : c ≤ d<VAR>h : c < b<GOAL>Iio b ∪ Ioo c d = Iio (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>hcd : d ≤ c<VAR>h : d < b<GOAL>Iio b ∪ Ioo c d = Iio (max b d)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : BorelSpace X<VAR>inst✝¹ : MeasurableSpace Y<VAR>inst✝ : BorelSpace Y<VAR>K : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>h : LipschitzOnWith K f s<VAR>d : ℝ<VAR>hd : 0 ≤ d<GOAL>μH[d] (f '' s) ≤ ↑K ^ d * μH[d] s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g s t : ι → α<VAR>a b : α<VAR>f : Bool → α<GOAL>⨆ b, f b = f true ⊔ f false
<VAR>J : Type u'<VAR>inst✝² : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimitsOfShape J TopCat<VAR>F : J ⥤ PresheafedSpace C<VAR>j : J<GOAL>{ obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.map (𝟙 j) = 𝟙 ({ obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.obj j)
<VAR>J : Type u'<VAR>inst✝² : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimitsOfShape J TopCat<VAR>F : J ⥤ PresheafedSpace C<VAR>j : J<GOAL>(opEquiv ({ obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.obj j) ({ obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.obj j)) ({ obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.map (𝟙 j)) = (opEquiv ({ obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.obj j) ({ obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.obj j)) (𝟙 ({ obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.obj j))