ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderTopology α<VAR>h' : 𝓝[<] x = ⊥<GOAL>ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderTopology α<VAR>h' : 𝓝[<] x ≠ ⊥<GOAL>ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderTopology α<VAR>h' : 𝓝[<] x ≠ ⊥<VAR>this : (𝓝[<] x).NeBot<GOAL>ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderTopology α<VAR>h' : 𝓝[<] x ≠ ⊥<VAR>this : (𝓝[<] x).NeBot<VAR>h : leftLim f x = f x<GOAL>ContinuousWithinAt f (Iio x) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderTopology α<VAR>h' : 𝓝[<] x ≠ ⊥<VAR>this✝ : (𝓝[<] x).NeBot<VAR>h : leftLim f x = f x<VAR>this : Tendsto f (𝓝[<] x) (𝓝 (leftLim f x))<GOAL>ContinuousWithinAt f (Iio x) x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q p : R[X]<VAR>a : R<VAR>hp0 : 0 < p.degree<GOAL>(p - C a).degree = p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q p : R[X]<VAR>a : R<VAR>hp0 : 0 < p.degree<GOAL>(p + C (-a)).degree = p.degree
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : NormedSpace ℝ V<VAR>inst✝² : StrictConvexSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c : P<GOAL>dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : NormedSpace ℝ V<VAR>inst✝² : StrictConvexSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c : P<VAR>this : dist (a -ᵥ a) (b -ᵥ a) + dist (b -ᵥ a) (c -ᵥ a) = dist (a -ᵥ a) (c -ᵥ a) ↔ b -ᵥ a ∈ [a -ᵥ a-[ℝ]c -ᵥ a]<GOAL>dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : NormedSpace ℝ V<VAR>inst✝² : StrictConvexSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c : P<VAR>this : dist a b + dist b c = dist a c ↔ b -ᵥ a ∈ (fun x => x -ᵥ a) '' affineSegment ℝ a c<GOAL>dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>f : ℕ → α<VAR>d : ℕ → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n<VAR>hd : tsum d ≠ ⊤<GOAL>CauchySeq f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>f : ℕ → α<VAR>d : ℕ → ℝ≥0<VAR>hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ (fun i => ↑(d i)) n<VAR>hd : ∑' (i : ℕ), ↑(d i) ≠ ⊤<GOAL>CauchySeq f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>f : ℕ → α<VAR>d : ℕ → ℝ≥0<VAR>hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ (fun i => ↑(d i)) n<VAR>hd : Summable d<GOAL>CauchySeq f
<VAR>m n : ℕ<VAR>i j : Fin (n + 1)<VAR>hi : i ≠ Fin.last n<VAR>hj : j ≠ i<GOAL>(finSuccEquiv' i) j = some ((i.castLT ⋯).predAbove j)
<VAR>m n : ℕ<VAR>i : Fin (n + 1)<VAR>hi : i ≠ Fin.last n<VAR>j : Fin n<VAR>hj : i.succAbove j ≠ i<GOAL>(finSuccEquiv' i) (i.succAbove j) = some ((i.castLT ⋯).predAbove (i.succAbove j))
<VAR>m n : ℕ<VAR>j i : Fin n<VAR>hi : i.castSucc ≠ Fin.last n<VAR>hj : i.castSucc.succAbove j ≠ i.castSucc<GOAL>(finSuccEquiv' i.castSucc) (i.castSucc.succAbove j) = some ((i.castSucc.castLT ⋯).predAbove (i.castSucc.succAbove j))
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I J : Submodule R P<VAR>aI : R<VAR>haI : aI ∈ S<VAR>hI : ∀ b ∈ I, IsInteger R (aI • b)<VAR>aJ : R<VAR>haJ : aJ ∈ S<VAR>hJ : ∀ b ∈ J, IsInteger R (aJ • b)<VAR>b : P<VAR>hb : b ∈ I ⊔ J<GOAL>IsInteger R ((aI * aJ) • b)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I J : Submodule R P<VAR>aI : R<VAR>haI : aI ∈ S<VAR>hI : ∀ b ∈ I, IsInteger R (aI • b)<VAR>aJ : R<VAR>haJ : aJ ∈ S<VAR>hJ : ∀ b ∈ J, IsInteger R (aJ • b)<VAR>bI : P<VAR>hbI : bI ∈ I<VAR>bJ : P<VAR>hbJ : bJ ∈ J<VAR>hb : bI + bJ ∈ I ⊔ J<GOAL>IsInteger R ((aI * aJ) • (bI + bJ))
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I J : Submodule R P<VAR>aI : R<VAR>haI : aI ∈ S<VAR>hI : ∀ b ∈ I, IsInteger R (aI • b)<VAR>aJ : R<VAR>haJ : aJ ∈ S<VAR>hJ : ∀ b ∈ J, IsInteger R (aJ • b)<VAR>bI : P<VAR>hbI : bI ∈ I<VAR>bJ : P<VAR>hbJ : bJ ∈ J<VAR>hb : bI + bJ ∈ I ⊔ J<GOAL>IsInteger R ((aI * aJ) • bI + (aI * aJ) • bJ)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I J : Submodule R P<VAR>aI : R<VAR>haI : aI ∈ S<VAR>hI : ∀ b ∈ I, IsInteger R (aI • b)<VAR>aJ : R<VAR>haJ : aJ ∈ S<VAR>hJ : ∀ b ∈ J, IsInteger R (aJ • b)<VAR>bI : P<VAR>hbI : bI ∈ I<VAR>bJ : P<VAR>hbJ : bJ ∈ J<VAR>hb : bI + bJ ∈ I ⊔ J<GOAL>IsInteger R ((aI * aJ) • bI)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I J : Submodule R P<VAR>aI : R<VAR>haI : aI ∈ S<VAR>hI : ∀ b ∈ I, IsInteger R (aI • b)<VAR>aJ : R<VAR>haJ : aJ ∈ S<VAR>hJ : ∀ b ∈ J, IsInteger R (aJ • b)<VAR>bI : P<VAR>hbI : bI ∈ I<VAR>bJ : P<VAR>hbJ : bJ ∈ J<VAR>hb : bI + bJ ∈ I ⊔ J<GOAL>IsInteger R ((aI * aJ) • bJ)
<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>inst✝ : ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>u : α → β<VAR>b : β<VAR>hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<GOAL>(∃ᶠ (x : α) in f, b ≤ u x) → b ≤ limsup u f
<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>inst✝ : ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>u : α → β<VAR>b : β<VAR>hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<GOAL>¬b ≤ limsup u f → ∀ᶠ (x : α) in f, ¬b ≤ u x
<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>inst✝ : ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>u : α → β<VAR>b : β<VAR>hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<GOAL>limsup u f < b → ∀ᶠ (x : α) in f, u x < b
<VAR>r r₁ r₂ : ℝ≥0<VAR>x y : ℝ<GOAL>↑r = 0 ↔ r = 0
<VAR>x : ZFSet<VAR>h : ∅ ∉ x<VAR>y : ZFSet<VAR>yx : y ∈ x<GOAL>↑(map (fun y => Classical.epsilon fun z => z ∈ y) x) ′ ↑y ∈ ↑y
<VAR>x : ZFSet<VAR>h : ∅ ∉ x<VAR>y : ZFSet<VAR>yx : y ∈ x<GOAL>(Classical.epsilon fun z => z ∈ y) ∈ y
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>p : ι → AddSubmonoid N<VAR>h : Function.Injective ⇑(sumAddHom fun i => (p i).subtype)<GOAL>Independent p
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>p : ι → AddSubmonoid N<VAR>h : Function.Injective ⇑(sumAddHom fun i => (p i).subtype)<GOAL>Independent (⇑AddSubmonoid.toNatSubmodule ∘ p)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a✝ b : α<VAR>s : Set α<VAR>a : α<VAR>h : (Ioi a).Nonempty<GOAL>closure (Ioi a) = Ici a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a✝ b : α<VAR>s : Set α<VAR>a : α<VAR>h : (Ioi a).Nonempty<GOAL>closure (Ioi a) ⊆ Ici a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a✝ b : α<VAR>s : Set α<VAR>a : α<VAR>h : (Ioi a).Nonempty<GOAL>Ici a ⊆ closure (Ioi a)
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝³ : Monoid N<VAR>hnontriv : Nontrivial ι<VAR>G : Type u_4<VAR>inst✝² : Group G<VAR>H : ι → Type u_5<VAR>inst✝¹ : (i : ι) → Group (H i)<VAR>f : (i : ι) → H i →* G<VAR>hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)<VAR>α : Type u_6<VAR>inst✝ : MulAction G α<VAR>X : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i<VAR>w : Word H<VAR>h : (lift f) w.prod = 1<GOAL>w = Word.empty
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝³ : Monoid N<VAR>hnontriv : Nontrivial ι<VAR>G : Type u_4<VAR>inst✝² : Group G<VAR>H : ι → Type u_5<VAR>inst✝¹ : (i : ι) → Group (H i)<VAR>f : (i : ι) → H i →* G<VAR>hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)<VAR>α : Type u_6<VAR>inst✝ : MulAction G α<VAR>X : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i<VAR>w : Word H<VAR>h : (lift f) w.prod = 1<VAR>hnotempty : ¬w = Word.empty<GOAL>False
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝³ : Monoid N<VAR>hnontriv : Nontrivial ι<VAR>G : Type u_4<VAR>inst✝² : Group G<VAR>H : ι → Type u_5<VAR>inst✝¹ : (i : ι) → Group (H i)<VAR>f : (i : ι) → H i →* G<VAR>hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)<VAR>α : Type u_6<VAR>inst✝ : MulAction G α<VAR>X : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i<VAR>i j : ι<VAR>w : NeWord H i j<VAR>h : (lift f) w.toWord.prod = 1<VAR>hnotempty : ¬w.toWord = Word.empty<GOAL>False
<VAR>a b c : ℕ<VAR>r : ℤ<VAR>ha : a % 2 = 0<VAR>hb : b % 8 = 7<VAR>hc : a / 2 = c<VAR>hr : jacobiSymNat c b = r<GOAL>jacobiSymNat a b = r
<VAR>a b c : ℕ<VAR>r : ℤ<VAR>ha : a % 2 = 0<VAR>hb : b % 8 = 7<VAR>hc : a / 2 = c<VAR>hr : jacobiSymNat c b = r<GOAL>jacobiSym (↑a) b = jacobiSym (↑a / 2) b
<VAR>a b c : ℕ<VAR>r : ℤ<VAR>ha : a % 2 = 0<VAR>hb : b % 8 = 7<VAR>hc : a / 2 = c<VAR>hr : jacobiSymNat c b = r<GOAL>b % 2 = 1
<VAR>a b c : ℕ<VAR>r : ℤ<VAR>ha : a % 2 = 0<VAR>hb : b % 8 = 7<VAR>hc : a / 2 = c<VAR>hr : jacobiSymNat c b = r<GOAL>2 ∣ 8
<VAR>R✝ : Type u_1<VAR>inst✝¹ : Semiring R✝<VAR>r✝ : R✝<VAR>f✝ : R✝[X]<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>f : R[X]<VAR>r : R<VAR>h : ∀ (k : ℕ), eval r ((hasseDeriv k) f) = 0<GOAL>f = 0
<VAR>R✝ : Type u_1<VAR>inst✝¹ : Semiring R✝<VAR>r✝ : R✝<VAR>f✝ : R✝[X]<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>f : R[X]<VAR>r : R<VAR>h : ∀ (k : ℕ), eval r ((hasseDeriv k) f) = 0<GOAL>(taylor r) f = (taylor r) 0
<VAR>R✝ : Type u_1<VAR>inst✝¹ : Semiring R✝<VAR>r✝ : R✝<VAR>f✝ : R✝[X]<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>f : R[X]<VAR>r : R<VAR>h : ∀ (k : ℕ), eval r ((hasseDeriv k) f) = 0<GOAL>(taylor r) f = 0
<VAR>R✝ : Type u_1<VAR>inst✝¹ : Semiring R✝<VAR>r✝ : R✝<VAR>f✝ : R✝[X]<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>f : R[X]<VAR>r : R<VAR>h : ∀ (k : ℕ), eval r ((hasseDeriv k) f) = 0<VAR>k : ℕ<GOAL>((taylor r) f).coeff k = coeff 0 k
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>p n : ℕ<VAR>inst✝¹ : ExpChar R p<VAR>f : R[X]<VAR>inst✝ : PerfectRing R p<VAR>y : R<GOAL>(X ^ p - C y).roots = p • {(frobeniusEquiv R p).symm y}
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>p n : ℕ<VAR>inst✝¹ : ExpChar R p<VAR>f : R[X]<VAR>inst✝ : PerfectRing R p<VAR>y : R<VAR>H : (X ^ p ^ 1 - C y).roots = p ^ 1 • {(iterateFrobeniusEquiv R p 1).symm y}<GOAL>(X ^ p - C y).roots = p • {(frobeniusEquiv R p).symm y}
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : CancelMonoidWithZero M₀<VAR>a b c : M₀<VAR>ha : a ≠ 0<GOAL>a * b = a ↔ b = 1
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>r : ℝ<VAR>hnr : ↑(finrank ℝ E) < r<GOAL>Integrable (fun x => (1 + ‖x‖ ^ 2) ^ (-r / 2)) μ
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>r : ℝ<VAR>hnr : ↑(finrank ℝ E) < r<VAR>hr : 0 < r<GOAL>Integrable (fun x => (1 + ‖x‖ ^ 2) ^ (-r / 2)) μ
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>r : ℝ<VAR>hnr : ↑(finrank ℝ E) < r<VAR>hr : 0 < r<GOAL>AEStronglyMeasurable (fun x => (1 + ‖x‖ ^ 2) ^ (-r / 2)) μ
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>r : ℝ<VAR>hnr : ↑(finrank ℝ E) < r<VAR>hr : 0 < r<VAR>x : E<GOAL>‖(1 + ‖x‖ ^ 2) ^ (-r / 2)‖ ≤ 2 ^ (r / 2) * (1 + ‖x‖) ^ (-r)
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>r : ℝ<VAR>hnr : ↑(finrank ℝ E) < r<VAR>hr : 0 < r<VAR>x : E<GOAL>0 < (1 + ‖x‖ ^ 2) ^ (-r / 2)
<VAR>a x y : ℂ<VAR>hx : ‖x‖ = 1<VAR>hy : ‖y‖ = 1<GOAL>angle x y ≤ π / 2 * ‖x - y‖
<VAR>a x y : ℂ<VAR>hx : ‖x‖ = 1<VAR>hy : ‖y‖ = 1<GOAL>2 / π * angle x y ≤ ‖x - y‖
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ η : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>s : Set γ<VAR>hsm : MeasurableSet s<VAR>hs : s ⊆ κ.mutuallySingularSetSlice η a<VAR>hs' : ∀ x ∈ s, 1 ≤ κ.rnDerivAux (κ + η) a x<GOAL>((κ.singularPart η) a) s = (κ a) s
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ η : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>s : Set γ<VAR>hsm : MeasurableSet s<VAR>hs : s ⊆ κ.mutuallySingularSetSlice η a<VAR>hs' : ∀ x ∈ s, 1 ≤ κ.rnDerivAux (κ + η) a x<GOAL>∫⁻ (b : γ) in s, ↑(κ.rnDerivAux (κ + η) a b).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal * κ.rnDeriv η a b ∂(κ + η) a = (κ a) s
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ η : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>s : Set γ<VAR>hsm : MeasurableSet s<VAR>hs : s ⊆ κ.mutuallySingularSetSlice η a<VAR>hs' : ∀ x ∈ s, 1 ≤ κ.rnDerivAux (κ + η) a x<GOAL>Measurable (Function.uncurry fun a x => ↑(κ.rnDerivAux (κ + η) a x).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>κ : ι → Sort u_3<VAR>inst✝ : SemilatticeSup α<VAR>c : ClosureOperator α<VAR>x y : α<GOAL>c (x ⊔ c y) = c (x ⊔ y)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>f : Function.End α<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hf : f ^ p ^ n = 1<GOAL>Fintype.card α ≡ Fintype.card ↑(fixedPoints f) [MOD p]
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>f : Function.End α<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hf : f ^ p ^ n = 1<VAR>σ : α ≃ α := { toFun := f, invFun := f ^ (p ^ n - 1), left_inv := ⋯, right_inv := ⋯ }<GOAL>Fintype.card α ≡ Fintype.card ↑(fixedPoints f) [MOD p]
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>f : Function.End α<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hf : f ^ p ^ n = 1<VAR>σ : α ≃ α := { toFun := f, invFun := f ^ (p ^ n - 1), left_inv := ⋯, right_inv := ⋯ }<VAR>hσ : σ ^ p ^ n = 1<GOAL>Fintype.card α ≡ Fintype.card ↑(fixedPoints f) [MOD p]
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>f : Function.End α<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hf : f ^ p ^ n = 1<VAR>σ : α ≃ α := { toFun := f, invFun := f ^ (p ^ n - 1), left_inv := ⋯, right_inv := ⋯ }<VAR>hσ : σ ^ p ^ n = 1<GOAL>Fintype.card ↑(fixedPoints f) = (support σ)ᶜ.card
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>f : Function.End α<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hf : f ^ p ^ n = 1<VAR>σ : α ≃ α := { toFun := f, invFun := f ^ (p ^ n - 1), left_inv := ⋯, right_inv := ⋯ }<VAR>hσ : σ ^ p ^ n = 1<GOAL>fixedPoints f = ↑(support σ)ᶜ
<VAR>x : ℂ<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>(x ^ (↑n)⁻¹) ^ n = x
<VAR>x : ℂ<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>↑n ≠ 0
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : IsLocalization M S<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>hM : Disjoint ↑M ↑I<GOAL>Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I) = I
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : IsLocalization M S<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>hM : Disjoint ↑M ↑I<GOAL>Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I) ≤ I
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : IsLocalization M S<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>hM : Disjoint ↑M ↑I<VAR>a : R<VAR>ha : a ∈ Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I)<GOAL>a ∈ I
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : IsLocalization M S<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>hM : Disjoint ↑M ↑I<VAR>a : R<VAR>ha : a ∈ Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I)<VAR>b : ↥I<VAR>s : ↥M<VAR>h : (algebraMap R S) a * (algebraMap R S) ↑(b, s).2 = (algebraMap R S) ↑(b, s).1<GOAL>a ∈ I
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : IsLocalization M S<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>hM : Disjoint ↑M ↑I<VAR>a : R<VAR>ha : a ∈ Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I)<VAR>b : ↥I<VAR>s : ↥M<VAR>h : (algebraMap R S) (↑s * a) = (algebraMap R S) ↑b<GOAL>a ∈ I
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : IsLocalization M S<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>hM : Disjoint ↑M ↑I<VAR>a : R<VAR>ha : a ∈ Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I)<VAR>b : ↥I<VAR>s : ↥M<VAR>h : (algebraMap R S) (↑s * a) = (algebraMap R S) ↑b<VAR>c : ↥M<VAR>hc : ↑c * (↑s * a) = ↑c * ↑b<GOAL>a ∈ I
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : IsLocalization M S<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>hM : Disjoint ↑M ↑I<VAR>a : R<VAR>ha : a ∈ Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I)<VAR>b : ↥I<VAR>s : ↥M<VAR>h : (algebraMap R S) (↑s * a) = (algebraMap R S) ↑b<VAR>c : ↥M<VAR>hc : ↑c * (↑s * a) = ↑c * ↑b<VAR>this : ↑c * ↑s * a ∈ I<GOAL>a ∈ I
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>hv : v ≠ 0<GOAL>∫ (x : ℝ), gaussianPDFReal μ v x = 1
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>hv : v ≠ 0<VAR>h : ∫⁻ (x : ℝ), ENNReal.ofReal (gaussianPDFReal μ v x) = 1<GOAL>∫ (x : ℝ), gaussianPDFReal μ v x = 1
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>hv : v ≠ 0<VAR>h : ENNReal.ofReal (∫ (x : ℝ), gaussianPDFReal μ v x) = ENNReal.ofReal 1<GOAL>∫ (x : ℝ), gaussianPDFReal μ v x = 1
<VAR>ι✝ : Type u_1<VAR>ι' : Type u_2<VAR>β : Type u_3<VAR>α : ι✝ → Type u<VAR>U : (i : ι✝) → UniformSpace (α i)<VAR>inst✝ : UniformSpace β<VAR>ι : Type u_4<VAR>X : Type u_5<VAR>u : ι → UniformSpace X<VAR>hu : ∀ (i : ι), CompleteSpace X<VAR>a✝ : Nontrivial X<VAR>t : TopologicalSpace X<VAR>ht : T2Space X<VAR>hut : ∀ (i : ι), toTopologicalSpace ≤ t<VAR>this : UniformInducing (const ι)<GOAL>CompleteSpace X
<VAR>ι✝ : Type u_1<VAR>ι' : Type u_2<VAR>β : Type u_3<VAR>α : ι✝ → Type u<VAR>U : (i : ι✝) → UniformSpace (α i)<VAR>inst✝ : UniformSpace β<VAR>ι : Type u_4<VAR>X : Type u_5<VAR>u : ι → UniformSpace X<VAR>hu : ∀ (i : ι), CompleteSpace X<VAR>a✝ : Nontrivial X<VAR>t : TopologicalSpace X<VAR>ht : T2Space X<VAR>hut : ∀ (i : ι), toTopologicalSpace ≤ t<VAR>this : UniformInducing (const ι)<GOAL>IsComplete (⋂ i, ⋂ i_1, {x | x i = x i_1})
<VAR>ι✝ : Type u_1<VAR>ι' : Type u_2<VAR>β : Type u_3<VAR>α : ι✝ → Type u<VAR>U : (i : ι✝) → UniformSpace (α i)<VAR>inst✝ : UniformSpace β<VAR>ι : Type u_4<VAR>X : Type u_5<VAR>u : ι → UniformSpace X<VAR>hu : ∀ (i : ι), CompleteSpace X<VAR>a✝ : Nontrivial X<VAR>t : TopologicalSpace X<VAR>ht : T2Space X<VAR>hut : ∀ (i : ι), toTopologicalSpace ≤ t<VAR>this✝ : UniformInducing (const ι)<VAR>this : Pi.topologicalSpace ≤ Pi.topologicalSpace<GOAL>IsComplete (⋂ i, ⋂ i_1, {x | x i = x i_1})
<VAR>ι✝ : Type u_1<VAR>ι' : Type u_2<VAR>β : Type u_3<VAR>α : ι✝ → Type u<VAR>U : (i : ι✝) → UniformSpace (α i)<VAR>inst✝ : UniformSpace β<VAR>ι : Type u_4<VAR>X : Type u_5<VAR>u : ι → UniformSpace X<VAR>hu : ∀ (i : ι), CompleteSpace X<VAR>a✝ : Nontrivial X<VAR>t : TopologicalSpace X<VAR>ht : T2Space X<VAR>hut : ∀ (i : ι), toTopologicalSpace ≤ t<VAR>this✝ : UniformInducing (const ι)<VAR>this : Pi.topologicalSpace ≤ Pi.topologicalSpace<GOAL>IsClosed (⋂ i, ⋂ i_1, {x | x i = x i_1})
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>x : R<VAR>k n : ℕ<GOAL>(coeff R n) ((C R) x * X ^ k) = if n = k then x else 0
<VAR>c : Cardinal.{u}<GOAL>lift.{v, u} c ≤ 𝔠 ↔ c ≤ 𝔠
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>b : K<VAR>nth_partDen_eq : (of v).partDens.get? n = some b<GOAL>1 ≤ b
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>gp_n : Pair K<VAR>nth_s_eq : (of v).s.get? n = some gp_n<VAR>nth_partDen_eq : (of v).partDens.get? n = some gp_n.b<GOAL>1 ≤ gp_n.b
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>gp_n : Pair K<VAR>nth_s_eq : (of v).s.get? n = some gp_n<VAR>nth_partDen_eq : (of v).partDens.get? n = some gp_n.b<VAR>ifp_n : IntFractPair K<VAR>succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_n<VAR>ifp_n_b_eq_gp_n_b : ↑ifp_n.b = gp_n.b<GOAL>1 ≤ gp_n.b
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>gp_n : Pair K<VAR>nth_s_eq : (of v).s.get? n = some gp_n<VAR>nth_partDen_eq : (of v).partDens.get? n = some gp_n.b<VAR>ifp_n : IntFractPair K<VAR>succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_n<VAR>ifp_n_b_eq_gp_n_b : ↑ifp_n.b = gp_n.b<GOAL>1 ≤ ↑ifp_n.b