ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>fp : Finpartition univ := h.finpartition<VAR>large : Finset V<VAR>hl : large ∈ fp.parts<VAR>small : Finset V<VAR>hs : small ∈ fp.parts<VAR>ineq : small.card + 1 < large.card<VAR>w : V<VAR>hw : w ∈ large<VAR>v : V<VAR>hv : v ∈ small<VAR>cf : G.CliqueFree (r + 1)<VAR>large_eq : fp.part w = large<VAR>small_eq : fp.part v = small<VAR>ha : G.Adj v w<GOAL>G.edgeFinset.card < G.edgeFinset.card + (Fintype.card V - small.card) - (Fintype.card V - large.card) - 1
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>fp : Finpartition univ := h.finpartition<VAR>large : Finset V<VAR>hl : large ∈ fp.parts<VAR>small : Finset V<VAR>hs : small ∈ fp.parts<VAR>ineq : small.card + 1 < large.card<VAR>w : V<VAR>hw : w ∈ large<VAR>v : V<VAR>hv : v ∈ small<VAR>cf : G.CliqueFree (r + 1)<VAR>large_eq : fp.part w = large<VAR>small_eq : fp.part v = small<VAR>ha : G.Adj v w<VAR>this : large.card ≤ Fintype.card V<GOAL>G.edgeFinset.card < G.edgeFinset.card + (Fintype.card V - small.card) - (Fintype.card V - large.card) - 1
<VAR>C : Type u<VAR>inst✝¹ : Groupoid C<VAR>S : Subgroupoid C<VAR>D : Type u_1<VAR>inst✝ : Groupoid D<VAR>φ : C ⥤ D<VAR>hφ : Function.Injective φ.obj<VAR>hφ' : im φ hφ = ⊤<VAR>d : D<GOAL>∃ a, φ.obj a = d
<VAR>C : Type u<VAR>inst✝¹ : Groupoid C<VAR>S : Subgroupoid C<VAR>D : Type u_1<VAR>inst✝ : Groupoid D<VAR>φ : C ⥤ D<VAR>hφ : Function.Injective φ.obj<VAR>hφ' : im φ hφ = ⊤<VAR>d : D<GOAL>d ∈ ⊤.objs
<VAR>α : Type u<VAR>n : ℕ<GOAL>finRange n.succ = (map Fin.castSucc (finRange n)).concat (Fin.last n)
<VAR>α : Type u<VAR>n : ℕ<GOAL>map Fin.val (finRange n.succ) = map Fin.val ((map Fin.castSucc (finRange n)).concat (Fin.last n))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c : α<GOAL>Iic a \ Iio a = {a}
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>h : p.support.card ≤ 1<GOAL>C p.leadingCoeff * X ^ p.natDegree = p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<GOAL>r * ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), r * f a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<GOAL>⨆ i, r * ⨆ (_ : ↑i ≤ fun a => f a), i.lintegral μ ≤ ∫⁻ (a : α), r * f a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>s : α →ₛ ℝ≥0∞<GOAL>r * ⨆ (_ : ↑s ≤ fun a => f a), s.lintegral μ ≤ ∫⁻ (a : α), r * f a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>s : α →ₛ ℝ≥0∞<GOAL>(↑s ≤ fun a => f a) → r * s.lintegral μ ≤ ∫⁻ (a : α), r * f a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>s : α →ₛ ℝ≥0∞<VAR>hs : ↑s ≤ fun a => f a<GOAL>r * s.lintegral μ ≤ ∫⁻ (a : α), r * f a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>s : α →ₛ ℝ≥0∞<VAR>hs : ↑s ≤ fun a => f a<GOAL>(const α r * s).lintegral μ ≤ ⨆ g, ⨆ (_ : ↑g ≤ fun a => r * f a), g.lintegral μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>s : α →ₛ ℝ≥0∞<VAR>hs : ↑s ≤ fun a => f a<VAR>x : α<GOAL>↑(const α r * s) x ≤ (fun a => r * f a) x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a✝ : α<VAR>b✝ : β<VAR>h₀ : ∀ (b : β), Antitone (swap f b)<VAR>h₁ : ∀ (a : α), Monotone (f a)<VAR>a : α<VAR>ha : a ∈ upperBounds s<VAR>b : β<VAR>hb : b ∈ lowerBounds t<GOAL>BddBelow (image2 f s t)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>b c d : R<GOAL>normEDS b c d 1 = 1
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>ι : Type ui<VAR>inst✝¹ : CommSemiring k<VAR>inst✝ : AddCommMonoid G<VAR>s✝ : Finset ι<VAR>a✝ : ι → G<VAR>b : ι → k<VAR>a : ι<VAR>s : Finset ι<VAR>has : a ∉ s<VAR>ih : ∏ i ∈ s, single (a✝ i) (b i) = single (∑ i ∈ s, a✝ i) (∏ i ∈ s, b i)<GOAL>∏ i ∈ Finset.cons a s has, single (a✝ i) (b i) = single (∑ i ∈ Finset.cons a s has, a✝ i) (∏ i ∈ Finset.cons a s has, b i)
<VAR>α β : Type u<VAR>ι : Type u_1<VAR>f g : ι → Cardinal.{u_2}<VAR>H : ∀ (i : ι), f i ≤ g i<VAR>i : ι<VAR>this : f i ≤ g i<GOAL>Nonempty (Quotient.out (f i) ↪ Quotient.out (g ((Embedding.refl ι) i)))
<VAR>α : Type u_1<VAR>s✝ t✝ : Finset α<VAR>a : α<VAR>x✝ : Set α<VAR>hx✝ : x✝ ∈ Set.range toSet<VAR>s : Finset α<VAR>t : Set α<VAR>ht : t ∈ Set.Icc x✝ ↑s<GOAL>t ∈ Set.range toSet
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>p : R[X]<VAR>hp : p ∈ degreeLT R n<VAR>x : R<GOAL>eval x p = ∑ i : Fin n, (degreeLTEquiv R n) ⟨p, hp⟩ i * x ^ ↑i
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>p : R[X]<VAR>hp : p ∈ degreeLT R n<VAR>x : R<GOAL>(p.sum fun e a => a * x ^ e) = ∑ i : Fin n, (degreeLTEquiv R n) ⟨p, hp⟩ i * x ^ ↑i
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_7<VAR>inst✝ : SeminormedAddCommGroup β<VAR>T T' : Set α → β<VAR>C C' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT' : DominatedFinMeasAdditive μ T' C'<GOAL>DominatedFinMeasAdditive μ (T + T') (C + C')
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_7<VAR>inst✝ : SeminormedAddCommGroup β<VAR>T T' : Set α → β<VAR>C C' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT' : DominatedFinMeasAdditive μ T' C'<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s < ⊤<GOAL>‖(T + T') s‖ ≤ (C + C') * (μ s).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_7<VAR>inst✝ : SeminormedAddCommGroup β<VAR>T T' : Set α → β<VAR>C C' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT' : DominatedFinMeasAdditive μ T' C'<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s < ⊤<GOAL>‖T s + T' s‖ ≤ C * (μ s).toReal + C' * (μ s).toReal
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<GOAL>x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hx : x % 2 = 0<VAR>hy : y % 2 = 0<GOAL>x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hx : x % 2 = 0<VAR>hy : y % 2 = 1<GOAL>x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hx : x % 2 = 1<VAR>hy : y % 2 = 0<GOAL>x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hx : x % 2 = 1<VAR>hy : y % 2 = 1<GOAL>x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I✝ I J : Ideal A<VAR>I_le_J : I ≤ J<GOAL>homogeneousHull 𝒜 I ≤ homogeneousHull 𝒜 J
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I✝ I J : Ideal A<VAR>I_le_J : I ≤ J<GOAL>{r | ∃ i x, ↑(((decompose 𝒜) ↑x) i) = r} ⊆ {r | ∃ i x, ↑(((decompose 𝒜) ↑x) i) = r}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M✝ : Matroid α<VAR>N : Matroid β<VAR>M : Matroid α<VAR>f : α → β<VAR>hf : InjOn f M.E<VAR>B : Set β<GOAL>(M.map f hf).Base B ↔ ∃ B₀, M.Base B₀ ∧ B = f '' B₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M✝ : Matroid α<VAR>N : Matroid β<VAR>M : Matroid α<VAR>f : α → β<VAR>hf : InjOn f M.E<VAR>B : Set β<GOAL>((M.map f hf).Indep B ∧ ∀ (I : Set β), (M.map f hf).Indep I → B ⊆ I → B = I) ↔ ∃ B₀, M.Base B₀ ∧ B = f '' B₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M✝ : Matroid α<VAR>N : Matroid β<VAR>M : Matroid α<VAR>f : α → β<VAR>hf : InjOn f M.E<VAR>B : Set α<VAR>hB : M.Base B<GOAL>(M.map f hf).Indep (f '' B) ∧ ∀ (I : Set β), (M.map f hf).Indep I → f '' B ⊆ I → f '' B = I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I✝ s : Set α<VAR>M✝ : Matroid α<VAR>N : Matroid β<VAR>M : Matroid α<VAR>f : α → β<VAR>hf : InjOn f M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>I : Set β<VAR>hI : (M.map f hf).Indep I<VAR>hBI : f '' B ⊆ I<GOAL>f '' B = I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I✝ s : Set α<VAR>M✝ : Matroid α<VAR>N : Matroid β<VAR>M : Matroid α<VAR>f : α → β<VAR>hf : InjOn f M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>I : Set β<VAR>hI : (M.map f hf).Indep I<VAR>hBI : f '' B ⊆ I<VAR>I₀ : Set α<VAR>hI₀ : M.Indep I₀<VAR>hbij : BijOn f I₀ I<GOAL>f '' B = I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I✝ s : Set α<VAR>M✝ : Matroid α<VAR>N : Matroid β<VAR>M : Matroid α<VAR>f : α → β<VAR>hf : InjOn f M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>I : Set β<VAR>hI : (M.map f hf).Indep I<VAR>I₀ : Set α<VAR>hBI : B ⊆ I₀<VAR>hI₀ : M.Indep I₀<VAR>hbij : BijOn f I₀ I<GOAL>f '' B = I
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>N✝ : Type u_5<VAR>inst✝¹ : Group N✝<VAR>f✝ : G →* N✝<VAR>N : Type u_6<VAR>inst✝ : Group N<VAR>H : Subgroup G<VAR>f : N →* G<VAR>hf : Injective ⇑f<VAR>h : H.normalizer ≤ f.range<GOAL>comap f H.normalizer = (comap f H).normalizer
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>N✝ : Type u_5<VAR>inst✝¹ : Group N✝<VAR>f✝ : G →* N✝<VAR>N : Type u_6<VAR>inst✝ : Group N<VAR>H : Subgroup G<VAR>f : N →* G<VAR>hf : Injective ⇑f<VAR>h : H.normalizer ≤ f.range<GOAL>map f (comap f H.normalizer) = map f (comap f H).normalizer
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>N✝ : Type u_5<VAR>inst✝¹ : Group N✝<VAR>f✝ : G →* N✝<VAR>N : Type u_6<VAR>inst✝ : Group N<VAR>H : Subgroup G<VAR>f : N →* G<VAR>hf : Injective ⇑f<VAR>h : H.normalizer ≤ f.range<GOAL>H.normalizer = map f (comap f H).normalizer
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>N✝ : Type u_5<VAR>inst✝¹ : Group N✝<VAR>f✝ : G →* N✝<VAR>N : Type u_6<VAR>inst✝ : Group N<VAR>H : Subgroup G<VAR>f : N →* G<VAR>hf : Injective ⇑f<VAR>h : H.normalizer ≤ f.range<GOAL>H.normalizer ≤ map f (comap f H).normalizer
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>N✝ : Type u_5<VAR>inst✝¹ : Group N✝<VAR>f✝ : G →* N✝<VAR>N : Type u_6<VAR>inst✝ : Group N<VAR>H : Subgroup G<VAR>f : N →* G<VAR>hf : Injective ⇑f<VAR>h : H.normalizer ≤ f.range<GOAL>map f (comap f H).normalizer ≤ H.normalizer
<VAR>V : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup V<VAR>inst✝⁶ : InnerProductSpace ℝ V<VAR>inst✝⁵ : MeasurableSpace V<VAR>inst✝⁴ : BorelSpace V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝ : CompleteSpace E<VAR>hf : Integrable f volume<VAR>v : V<VAR>h'f : ContinuousAt f v<VAR>φ : V → ℝ := fun w => π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)<VAR>A : Tendsto (fun c => ∫ (w : V), (c ^ finrank ℝ V * φ (c • (v - w))) • f w) atTop (𝓝 (f v))<GOAL>Tendsto (fun c => ∫ (w : V), ((↑π * ↑c) ^ (↑(finrank ℝ V) / 2) * cexp (-↑π ^ 2 * ↑c * ↑‖v - w‖ ^ 2)) • f w) atTop (𝓝 (f v))
<VAR>V : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup V<VAR>inst✝⁶ : InnerProductSpace ℝ V<VAR>inst✝⁵ : MeasurableSpace V<VAR>inst✝⁴ : BorelSpace V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝ : CompleteSpace E<VAR>hf : Integrable f volume<VAR>v : V<VAR>h'f : ContinuousAt f v<VAR>φ : V → ℝ := fun w => π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)<VAR>A : Tendsto (fun c => ∫ (w : V), (c ^ finrank ℝ V * φ (c • (v - w))) • f w) atTop (𝓝 (f v))<VAR>B : Tendsto (fun c => ∫ (w : V), ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w) atTop (𝓝 (f v))<GOAL>Tendsto (fun c => ∫ (w : V), ((↑π * ↑c) ^ (↑(finrank ℝ V) / 2) * cexp (-↑π ^ 2 * ↑c * ↑‖v - w‖ ^ 2)) • f w) atTop (𝓝 (f v))
<VAR>V : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup V<VAR>inst✝⁶ : InnerProductSpace ℝ V<VAR>inst✝⁵ : MeasurableSpace V<VAR>inst✝⁴ : BorelSpace V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝ : CompleteSpace E<VAR>hf : Integrable f volume<VAR>v : V<VAR>h'f : ContinuousAt f v<VAR>φ : V → ℝ := fun w => π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)<VAR>A : Tendsto (fun c => ∫ (w : V), (c ^ finrank ℝ V * φ (c • (v - w))) • f w) atTop (𝓝 (f v))<VAR>B : Tendsto (fun c => ∫ (w : V), ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w) atTop (𝓝 (f v))<GOAL>(fun c => ∫ (w : V), ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w) =ᶠ[atTop] fun c => ∫ (w : V), ((↑π * ↑c) ^ (↑(finrank ℝ V) / 2) * cexp (-↑π ^ 2 * ↑c * ↑‖v - w‖ ^ 2)) • f w
<VAR>V : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup V<VAR>inst✝⁶ : InnerProductSpace ℝ V<VAR>inst✝⁵ : MeasurableSpace V<VAR>inst✝⁴ : BorelSpace V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝ : CompleteSpace E<VAR>hf : Integrable f volume<VAR>v : V<VAR>h'f : ContinuousAt f v<VAR>φ : V → ℝ := fun w => π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)<VAR>A : Tendsto (fun c => ∫ (w : V), (c ^ finrank ℝ V * φ (c • (v - w))) • f w) atTop (𝓝 (f v))<VAR>B : Tendsto (fun c => ∫ (w : V), ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w) atTop (𝓝 (f v))<VAR>c : ℝ<VAR>hc : 0 < c<GOAL>∫ (w : V), ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w = ∫ (w : V), ((↑π * ↑c) ^ (↑(finrank ℝ V) / 2) * cexp (-↑π ^ 2 * ↑c * ↑‖v - w‖ ^ 2)) • f w
<VAR>V : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup V<VAR>inst✝⁶ : InnerProductSpace ℝ V<VAR>inst✝⁵ : MeasurableSpace V<VAR>inst✝⁴ : BorelSpace V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝ : CompleteSpace E<VAR>hf : Integrable f volume<VAR>v : V<VAR>h'f : ContinuousAt f v<VAR>φ : V → ℝ := fun w => π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)<VAR>A : Tendsto (fun c => ∫ (w : V), (c ^ finrank ℝ V * φ (c • (v - w))) • f w) atTop (𝓝 (f v))<VAR>B : Tendsto (fun c => ∫ (w : V), ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w) atTop (𝓝 (f v))<VAR>c : ℝ<VAR>hc : 0 < c<VAR>w : V<GOAL>((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w = ((↑π * ↑c) ^ (↑(finrank ℝ V) / 2) * cexp (-↑π ^ 2 * ↑c * ↑‖v - w‖ ^ 2)) • f w
<VAR>V : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup V<VAR>inst✝⁶ : InnerProductSpace ℝ V<VAR>inst✝⁵ : MeasurableSpace V<VAR>inst✝⁴ : BorelSpace V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝ : CompleteSpace E<VAR>hf : Integrable f volume<VAR>v : V<VAR>h'f : ContinuousAt f v<VAR>φ : V → ℝ := fun w => π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)<VAR>A : Tendsto (fun c => ∫ (w : V), (c ^ finrank ℝ V * φ (c • (v - w))) • f w) atTop (𝓝 (f v))<VAR>B : Tendsto (fun c => ∫ (w : V), ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w) atTop (𝓝 (f v))<VAR>c : ℝ<VAR>hc : 0 < c<VAR>w : V<GOAL>↑((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w = ((↑π * ↑c) ^ (↑(finrank ℝ V) / 2) * cexp (-↑π ^ 2 * ↑c * ↑‖v - w‖ ^ 2)) • f w
<VAR>V : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup V<VAR>inst✝⁶ : InnerProductSpace ℝ V<VAR>inst✝⁵ : MeasurableSpace V<VAR>inst✝⁴ : BorelSpace V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝ : CompleteSpace E<VAR>hf : Integrable f volume<VAR>v : V<VAR>h'f : ContinuousAt f v<VAR>φ : V → ℝ := fun w => π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)<VAR>A : Tendsto (fun c => ∫ (w : V), (c ^ finrank ℝ V * φ (c • (v - w))) • f w) atTop (𝓝 (f v))<VAR>B : Tendsto (fun c => ∫ (w : V), ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w) atTop (𝓝 (f v))<VAR>c : ℝ<VAR>hc : 0 < c<VAR>w : V<GOAL>↑((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) = (↑π * ↑c) ^ (↑(finrank ℝ V) / 2) * cexp (-↑π ^ 2 * ↑c * ↑‖v - w‖ ^ 2)
<VAR>V : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup V<VAR>inst✝⁶ : InnerProductSpace ℝ V<VAR>inst✝⁵ : MeasurableSpace V<VAR>inst✝⁴ : BorelSpace V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝ : CompleteSpace E<VAR>hf : Integrable f volume<VAR>v : V<VAR>h'f : ContinuousAt f v<VAR>φ : V → ℝ := fun w => π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)<VAR>A : Tendsto (fun c => ∫ (w : V), (c ^ finrank ℝ V * φ (c • (v - w))) • f w) atTop (𝓝 (f v))<VAR>B : Tendsto (fun c => ∫ (w : V), ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w) atTop (𝓝 (f v))<VAR>c : ℝ<VAR>hc : 0 < c<VAR>w : V<GOAL>↑((c ^ (1 / 2)) ^ finrank ℝ V) * ↑(π ^ (↑(finrank ℝ V) / 2)) * cexp ↑(-π ^ 2 * ‖c ^ (1 / 2) • (v - w)‖ ^ 2) = (↑π * ↑c) ^ (↑(finrank ℝ V) / 2) * cexp (-↑π ^ 2 * ↑c * ↑‖v - w‖ ^ 2)
<VAR>α : Type u_1<VAR>inst✝² : OrderedRing α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : DecidableEq α<VAR>n : ℕ<VAR>x : α<VAR>hx : x ∈ box n<VAR>hn : n = 0<GOAL>x = 0
<VAR>α : Type u<VAR>α' : Type w<VAR>β : Type v<VAR>β' : Type x<VAR>γ✝ : Type u_1<VAR>δ : Type u_2<VAR>γ : α ⊕ β → Sort u_3<VAR>p : ((ab : α ⊕ β) → γ ab) → Prop<GOAL>(∃ fab, p fab) ↔ ∃ fa fb, p fun t => rec fa fb t
<VAR>α : Type u<VAR>α' : Type w<VAR>β : Type v<VAR>β' : Type x<VAR>γ✝ : Type u_1<VAR>δ : Type u_2<VAR>γ : α ⊕ β → Sort u_3<VAR>p : ((ab : α ⊕ β) → γ ab) → Prop<GOAL>(¬∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), ¬p fun t => rec fa fb t) ↔ ∃ fa fb, p fun t => rec fa fb t
<VAR>a t : ℝ<VAR>ht : 0 < t<GOAL>HasSum (fun n => 2 * ↑n * Real.sin (2 * π * a * ↑n) * rexp (-π * ↑n ^ 2 * t)) (sinKernel (↑a) t)
<VAR>a t : ℝ<VAR>ht : 0 < t<GOAL>HasSum (fun x => ↑(2 * ↑x * Real.sin (2 * π * a * ↑x) * rexp (-π * ↑x ^ 2 * t))) ↑(sinKernel (↑a) t)
<VAR>a t : ℝ<VAR>ht : 0 < t<VAR>this : HasSum (fun n => -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) + -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t))) (↑(sinKernel (↑a) t) + -I * ↑0 * cexp (2 * ↑π * I * ↑a * ↑0) * ↑(rexp (-π * ↑0 ^ 2 * t)))<GOAL>HasSum (fun x => ↑(2 * ↑x * Real.sin (2 * π * a * ↑x) * rexp (-π * ↑x ^ 2 * t))) ↑(sinKernel (↑a) t)
<VAR>a t : ℝ<VAR>ht : 0 < t<VAR>this : HasSum (fun n => -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) + -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t))) ↑(sinKernel (↑a) t)<GOAL>HasSum (fun x => ↑(2 * ↑x * Real.sin (2 * π * a * ↑x) * rexp (-π * ↑x ^ 2 * t))) ↑(sinKernel (↑a) t)
<VAR>a t : ℝ<VAR>ht : 0 < t<VAR>this : HasSum (fun n => -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) + -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t))) ↑(sinKernel (↑a) t)<VAR>n : ℕ<GOAL>↑(2 * ↑n * Real.sin (2 * π * a * ↑n) * rexp (-π * ↑n ^ 2 * t)) = -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) + -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t))
<VAR>a t : ℝ<VAR>ht : 0 < t<VAR>this : HasSum (fun n => -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) + -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t))) ↑(sinKernel (↑a) t)<VAR>n : ℕ<GOAL>2 * ↑n * ((cexp (-↑(2 * π * a * ↑n) * I) - cexp (↑(2 * π * a * ↑n) * I)) * I / 2) * ↑(rexp (-π * ↑n ^ 2 * t)) = (-I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) + -(-I * ↑n) * cexp (-(2 * ↑π * I * ↑a * ↑n))) * ↑(rexp (-π * ↑n ^ 2 * t))
<VAR>a t : ℝ<VAR>ht : 0 < t<VAR>this : HasSum (fun n => -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) + -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t))) ↑(sinKernel (↑a) t)<VAR>n : ℕ<GOAL>2 * ↑n * ((cexp (-(2 * ↑π * ↑a * ↑n) * I) - cexp (2 * ↑π * ↑a * ↑n * I)) * I / 2) = -I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) + -(-I * ↑n) * cexp (-(2 * ↑π * I * ↑a * ↑n))
<VAR>a t : ℝ<VAR>ht : 0 < t<VAR>this : HasSum (fun n => -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) + -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t))) ↑(sinKernel (↑a) t)<VAR>n : ℕ<GOAL>I * ↑n * cexp (-(2 * ↑π * ↑a * ↑n * I)) - I * ↑n * cexp (2 * ↑π * ↑a * ↑n * I) = I * ↑n * cexp (-(2 * ↑π * I * ↑a * ↑n)) - I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n)
<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>s : Set (X ⊕ Y)<GOAL>IsClosed s ↔ IsClosed (inl ⁻¹' s) ∧ IsClosed (inr ⁻¹' s)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : NonAssocSemiring R<VAR>M : Submonoid R<VAR>inst✝¹ : NonAssocSemiring S<VAR>inst✝ : NonAssocSemiring T<VAR>s : Subsemiring S<VAR>x : R × S<GOAL>x ∈ ⊤.prod s ↔ x ∈ comap (RingHom.snd R S) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s t : Multiset α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>_l : List α<GOAL>Nodup (Quot.mk Setoid.r _l) ↔ ∀ a ∈ Quot.mk Setoid.r _l, count a (Quot.mk Setoid.r _l) = 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>k : ℕ<VAR>N✝ : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N : LieSubmodule R L M<GOAL>IsNilpotent R L ↥↑N ↔ ∃ k, LieSubmodule.lcs k N = ⊥