ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>N : Subgroup G<VAR>n : N.Normal<VAR>inst✝ : FirstCountableTopology G<VAR>u : ℕ → Set G<VAR>hu : (𝓝 1).HasBasis (fun x => True) u<VAR>u_anti : Antitone u<VAR>this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib<VAR>event_mul : ∀ (n : ℕ), ∀ᶠ (m : ℕ) in atTop, u m * u m ⊆ u n<VAR>φ : ℕ → ℕ<VAR>hφ : ∀ ⦃m n : ℕ⦄, m < n → u (φ n) * u (φ n) ⊆ u (φ m)<VAR>φ_anti_basis : (𝓝 1).HasAntitoneBasis (u ∘ φ)<GOAL>∃ u, (𝓝 1).HasAntitoneBasis u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hdf : DifferentiableOn ℝ f (Ioi a)<VAR>hg' : ∀ x ∈ Ioi a, deriv g x ≠ 0<VAR>hftop : Tendsto f atTop (𝓝 0)<VAR>hgtop : Tendsto g atTop (𝓝 0)<VAR>hdiv : Tendsto (fun x => deriv f x / deriv g x) atTop l<GOAL>Tendsto (fun x => f x / g x) atTop l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hdf✝ : DifferentiableOn ℝ f (Ioi a)<VAR>hg' : ∀ x ∈ Ioi a, deriv g x ≠ 0<VAR>hftop : Tendsto f atTop (𝓝 0)<VAR>hgtop : Tendsto g atTop (𝓝 0)<VAR>hdiv : Tendsto (fun x => deriv f x / deriv g x) atTop l<VAR>hdf : ∀ x ∈ Ioi a, DifferentiableAt ℝ f x<GOAL>Tendsto (fun x => f x / g x) atTop l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hdf✝ : DifferentiableOn ℝ f (Ioi a)<VAR>hg' : ∀ x ∈ Ioi a, deriv g x ≠ 0<VAR>hftop : Tendsto f atTop (𝓝 0)<VAR>hgtop : Tendsto g atTop (𝓝 0)<VAR>hdiv : Tendsto (fun x => deriv f x / deriv g x) atTop l<VAR>hdf : ∀ x ∈ Ioi a, DifferentiableAt ℝ f x<VAR>hdg : ∀ x ∈ Ioi a, DifferentiableAt ℝ g x<GOAL>Tendsto (fun x => f x / g x) atTop l
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁶ : Semiring α<VAR>inst✝⁵ : LinearOrder α<VAR>a✝ b c d : α<VAR>inst✝⁴ : IsRightCancelAdd α<VAR>inst✝³ : ZeroLEOneClass α<VAR>inst✝² : ExistsAddOfLE α<VAR>inst✝¹ : PosMulMono α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<GOAL>0 ≤ a * a
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hodd : p ≠ 2<GOAL>Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hodd : p ≠ 2<VAR>this : (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑↑p<GOAL>Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hodd : p ≠ 2<VAR>this : (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑↑p<GOAL>Prime ↑↑p
<VAR>n : ℕ<GOAL>a 1 ^ (2 * n) = 1
<VAR>n : ℕ<GOAL>a ↑(2 * n) = a 0
<VAR>n : ℕ<GOAL>↑(2 * n) = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SMulCommClass ℝ 𝕜 E<VAR>F' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup F'<VAR>inst✝ : NormedSpace ℝ F'<VAR>f : ↥(simpleFunc ℝ 1 μ)<VAR>h_pos : 0 ≤ᶠ[ae μ] ↑(toSimpleFunc f)<GOAL>integral f = (∫⁻ (a : α), ENNReal.ofReal (↑(toSimpleFunc f) a) ∂μ).toReal
<VAR>k : Type u_1<VAR>inst✝⁸ : Field k<VAR>K : Type u_2<VAR>inst✝⁷ : Field K<VAR>F : Type u_3<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : NumberField K<VAR>inst✝⁴ : Algebra k K<VAR>inst✝³ : Algebra k F<VAR>inst✝² : Algebra K F<VAR>inst✝¹ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>inst✝ : IsGalois k K<GOAL>IsUnramified k w ↔ Stab w = ⊥
<VAR>k : Type u_1<VAR>inst✝⁸ : Field k<VAR>K : Type u_2<VAR>inst✝⁷ : Field K<VAR>F : Type u_3<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : NumberField K<VAR>inst✝⁴ : Algebra k K<VAR>inst✝³ : Algebra k F<VAR>inst✝² : Algebra K F<VAR>inst✝¹ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>inst✝ : IsGalois k K<GOAL>(∀ (σ : K ≃ₐ[k] K), ComplexEmbedding.IsConj w.embedding σ → σ = 1) ↔ Stab (mk w.embedding) = ⊥
<VAR>x y : ℝ<GOAL>cos (-x) = cos x
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x ≠ 0<GOAL>angle x (x - y) = Real.arctan (‖y‖ / ‖x‖)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, -y⟫_ℝ = 0<VAR>h0 : x ≠ 0<GOAL>angle x (x - y) = Real.arctan (‖y‖ / ‖x‖)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : LinearOrderedCommRing S<VAR>abv : AbsoluteValue ℤ S<VAR>x : ℤˣ<GOAL>abv ↑x = 1
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>h : f.nextCoeff ≠ 0<GOAL>f.eraseLead.natDegree + 1 = f.natDegree
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>h : f.nextCoeff ≠ 0<GOAL>1 ≤ f.natDegree
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>C₂₃ : Type u_6<VAR>inst✝⁵ : Category.{?u.4909, u_1} C₁<VAR>inst✝⁴ : Category.{?u.4913, u_2} C₂<VAR>inst✝³ : Category.{?u.4917, u_3} C₃<VAR>inst✝² : Category.{?u.4921, u_4} C₄<VAR>inst✝¹ : Category.{?u.4925, u_5} C₁₂<VAR>inst✝ : Category.{?u.4929, u_6} C₂₃<VAR>F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂<VAR>G : C₁₂ ⥤ C₃ ⥤ C₄<VAR>X₁ Y₁ : C₁<VAR>φ : X₁ ⟶ Y₁<VAR>X₂ Y₂ : C₂<VAR>ψ : X₂ ⟶ Y₂<VAR>X₃ : C₃<GOAL>(G.map ((F₁₂.obj X₁).map ψ)).app X₃ ≫ (G.map ((F₁₂.map φ).app Y₂)).app X₃ = (G.map ((F₁₂.map φ).app X₂)).app X₃ ≫ (G.map ((F₁₂.obj Y₁).map ψ)).app X₃
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝² : EMetricSpace X<VAR>inst✝¹ : EMetricSpace Y<VAR>C K r✝ : ℝ≥0<VAR>f✝ : X → Y<VAR>s t : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>r : ℝ≥0<VAR>f : X → Y<VAR>hr : 0 < r<VAR>hf : ∀ (x : X), ∃ C, ∃ s ∈ 𝓝 x, HolderOnWith C r f s<GOAL>dimH (range f) ≤ dimH univ / ↑r
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝² : EMetricSpace X<VAR>inst✝¹ : EMetricSpace Y<VAR>C K r✝ : ℝ≥0<VAR>f✝ : X → Y<VAR>s t : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>r : ℝ≥0<VAR>f : X → Y<VAR>hr : 0 < r<VAR>hf : ∀ (x : X), ∃ C, ∃ s ∈ 𝓝 x, HolderOnWith C r f s<GOAL>dimH (f '' univ) ≤ dimH univ / ↑r
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝² : EMetricSpace X<VAR>inst✝¹ : EMetricSpace Y<VAR>C K r✝ : ℝ≥0<VAR>f✝ : X → Y<VAR>s t : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>r : ℝ≥0<VAR>f : X → Y<VAR>hr : 0 < r<VAR>hf : ∀ (x : X), ∃ C, ∃ s ∈ 𝓝 x, HolderOnWith C r f s<VAR>x : X<VAR>x✝ : x ∈ univ<GOAL>∃ C, ∃ t ∈ 𝓝[univ] x, HolderOnWith C r f t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a a' : α<VAR>s✝ : Set α<VAR>inst✝ : MeasurableSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(pure a).toMeasure s = (Measure.dirac a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a a' : α<VAR>s✝ : Set α<VAR>inst✝ : MeasurableSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(if a ∈ s then 1 else 0) = s.indicator 1 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>μ : Measure X<VAR>𝕜 : Type u_5<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>f : X → 𝕜<VAR>hf : Integrable f μ<GOAL>∫ (x : X), ↑(re (f x)) ∂μ + (∫ (x : X), ↑(im (f x)) ∂μ) * I = ∫ (x : X), f 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>μ : Measure X<VAR>𝕜 : Type u_5<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>f : X → 𝕜<VAR>hf : Integrable f μ<GOAL>∫ (a : X), ↑(re (f a)) + I • ↑(im (f a)) ∂μ = ∫ (x : X), f 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>μ : Measure X<VAR>𝕜 : Type u_5<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>f : X → 𝕜<VAR>hf : Integrable f μ<GOAL>Integrable (fun x => ↑(re (f 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>μ : Measure X<VAR>𝕜 : Type u_5<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>f : X → 𝕜<VAR>hf : Integrable f μ<GOAL>Integrable (fun a => I • ↑(im (f a))) μ
<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>H : SimpleGraph V<VAR>hr : 0 < r<GOAL>(turanGraph n r).CliqueFree (r + 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>H : SimpleGraph V<VAR>hr : 0 < r<GOAL>IsEmpty (⊤ ↪g turanGraph n r)
<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>H : SimpleGraph V<VAR>hr : 0 < r<VAR>h : ¬IsEmpty (⊤ ↪g turanGraph n r)<GOAL>False
<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>H : SimpleGraph V<VAR>hr : 0 < r<VAR>h : Nonempty (⊤ ↪g turanGraph n r)<GOAL>False
<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>H : SimpleGraph V<VAR>hr : 0 < r<VAR>f : Fin (r + 1) ↪ Fin n<VAR>ha : ∀ {a b : Fin (r + 1)}, (turanGraph n r).Adj (f a) (f b) ↔ ⊤.Adj a b<GOAL>False
<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>H : SimpleGraph V<VAR>hr : 0 < r<VAR>f : Fin (r + 1) ↪ Fin n<VAR>ha : ∀ {a b : Fin (r + 1)}, ↑(f a) % r ≠ ↑(f b) % r ↔ a ≠ b<GOAL>False
<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>H : SimpleGraph V<VAR>hr : 0 < r<VAR>f : Fin (r + 1) ↪ Fin n<VAR>ha : ∀ {a b : Fin (r + 1)}, ↑(f a) % r ≠ ↑(f b) % r ↔ a ≠ b<VAR>x y : Fin (r + 1)<VAR>d : x ≠ y<VAR>c : ⟨↑(f x) % r, ⋯⟩ = ⟨↑(f y) % r, ⋯⟩<GOAL>False
<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>H : SimpleGraph V<VAR>hr : 0 < r<VAR>f : Fin (r + 1) ↪ Fin n<VAR>ha : ∀ {a b : Fin (r + 1)}, ↑(f a) % r ≠ ↑(f b) % r ↔ a ≠ b<VAR>x y : Fin (r + 1)<VAR>d : x ≠ y<VAR>c : ↑(f x) % r = ↑(f y) % r<GOAL>False
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝¹ : AddCommMonoid R<VAR>inst✝ : StarAddMonoid R<VAR>x : R<GOAL>IsSelfAdjoint (x + star x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : F<GOAL>⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = -1 ↔ x ≠ 0 ∧ ∃ r < 0, y = r • x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : F<GOAL>(x ≠ 0 ∧ ∃ x_1, 0 < -x_1 ∧ -y = -x_1 • x) ↔ x ≠ 0 ∧ ∃ r < 0, y = r • x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : F<VAR>r : ℝ<GOAL>0 < -r ∧ -y = -r • x ↔ r < 0 ∧ y = r • x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>x : E<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<GOAL>∑' (i : ι), ‖⟪v i, x⟫_𝕜‖ ^ 2 ≤ ‖x‖ ^ 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>x : E<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<GOAL>0 ≤ ‖x‖ ^ 2
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIcoDiv hp (-a) b = -(toIocDiv hp a (-b) + 1)
<VAR>n : ℕ<GOAL>(hermite (2 * (n + 1) + 0)).coeff 0 = (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑((2 * (n + 1) + 0).choose 0)
<VAR>n : ℕ<GOAL>(-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑((2 * (n + 1) + 0).choose 0) = -(hermite (2 * n + 1)).coeff 1
<VAR>n : ℕ<GOAL>(-1) ^ n * -1 * ↑((2 * n + 1) * (2 * n - 1)‼) * ↑1 = -((-1) ^ n * ↑(2 * n - 1)‼ * ↑(2 * n + 1))
<VAR>n k : ℕ<VAR>hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)<GOAL>(hermite (2 * (n + 1) + (k + 1))).coeff (k + 1) = (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑((2 * (n + 1) + (k + 1)).choose (k + 1))
<VAR>n k : ℕ<VAR>hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)<VAR>hermite_explicit_recur : ∀ (n k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)<GOAL>(hermite (2 * (n + 1) + (k + 1))).coeff (k + 1) = (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑((2 * (n + 1) + (k + 1)).choose (k + 1))
<VAR>n k : ℕ<VAR>hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)<VAR>hermite_explicit_recur : ∀ (n k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)<GOAL>(hermite (2 * (n + 1) + (k + 1))).coeff (k + 1) = hermite_explicit (n + 1) (k + 1)
<VAR>n k : ℕ<VAR>hermite_explicit : ℕ → ℕ → ℤ := fun n k => (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)<VAR>hermite_explicit_recur : ∀ (n k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)<GOAL>(hermite (2 * (n + 1) + k)).coeff k - (↑k + 2) * (hermite (2 * (n + 1) + k)).coeff (k + 2) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
<VAR>V : Type u_1<VAR>inst✝ : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>h : G.Adj s t<GOAL>G ⊔ edge s t = G
<VAR>ι✝ : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>p : Type u_4<VAR>α : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype p<VAR>ι : Type u_8<VAR>inst✝¹ : Unique ι<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>a b : n → R<GOAL>(col ι a * row ι b).trace = a ⬝ᵥ b
<VAR>ι✝ : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>p : Type u_4<VAR>α : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype p<VAR>ι : Type u_8<VAR>inst✝¹ : Unique ι<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>a b : n → R<GOAL>∀ x ∈ Finset.univ, (col ι a * row ι b).diag x = a x * b x
<VAR>ι : Type u_4<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁵ : LinearOrder ι<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticMap R M N<VAR>bm : Basis ι R M<VAR>x : M<GOAL>(Q.toBilin bm).toQuadraticMap x = Q x
<VAR>ι : Type u_4<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁵ : LinearOrder ι<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticMap R M N<VAR>bm : Basis ι R M<VAR>x : M<GOAL>((Q.toBilin bm) (∑ a ∈ (bm.repr x).support, (bm.repr x) a • bm a)) (∑ a ∈ (bm.repr x).support, (bm.repr x) a • bm a) = Q (∑ a ∈ (bm.repr x).support, (bm.repr x) a • bm a)
<VAR>ι : Type u_4<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁵ : LinearOrder ι<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticMap R M N<VAR>bm : Basis ι R M<VAR>x : M<GOAL>(∑ x_1 ∈ (bm.repr x).support, (bm.repr x) x_1 • (bm.repr x) x_1 • Q (bm x_1) + ∑ x_1 ∈ (bm.repr x).support.offDiag, if x_1.1 = x_1.2 then (bm.repr x) x_1.1 • (bm.repr x) x_1.2 • Q (bm x_1.1) else if x_1.1 < x_1.2 then (bm.repr x) x_1.1 • (bm.repr x) x_1.2 • polar (⇑Q) (bm x_1.1) (bm x_1.2) else 0) = Q (∑ a ∈ (bm.repr x).support, (bm.repr x) a • bm a)
<VAR>ι : Type u_4<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁵ : LinearOrder ι<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticMap R M N<VAR>bm : Basis ι R M<VAR>x : M<GOAL>∑ x_1 ∈ (bm.repr x).support, (bm.repr x) x_1 • (bm.repr x) x_1 • Q (bm x_1) + ∑ a ∈ Finset.filter (fun x => x.1 < x.2) (bm.repr x).support.offDiag, (bm.repr x) a.1 • (bm.repr x) a.2 • polar (⇑Q) (bm a.1) (bm a.2) = ∑ i ∈ (bm.repr x).support, Q ((bm.repr x) i • bm i) + ∑ ij ∈ Finset.filter (fun x => ¬x.IsDiag) (bm.repr x).support.sym2, Sym2.lift ⟨fun i j => polar (⇑Q) ((bm.repr x) i • bm i) ((bm.repr x) j • bm j), ⋯⟩ ij
<VAR>ι : Type u_4<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁵ : LinearOrder ι<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticMap R M N<VAR>bm : Basis ι R M<VAR>x : M<GOAL>∀ x_1 ∈ (bm.repr x).support.offDiag, ¬x_1.1 = x_1.2
<VAR>m k p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>hp : Fact (Nat.Prime p)<VAR>hchar : CharP R p<VAR>μ : R<VAR>inst✝ : NeZero ↑m<GOAL>(cyclotomic (p ^ k * m) R).IsRoot μ ↔ IsPrimitiveRoot μ m
<VAR>m p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>hp : Fact (Nat.Prime p)<VAR>hchar : CharP R p<VAR>μ : R<VAR>inst✝ : NeZero ↑m<GOAL>(cyclotomic (p ^ 0 * m) R).IsRoot μ ↔ IsPrimitiveRoot μ m
<VAR>m k p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>hp : Fact (Nat.Prime p)<VAR>hchar : CharP R p<VAR>μ : R<VAR>inst✝ : NeZero ↑m<VAR>hk : k > 0<GOAL>(cyclotomic (p ^ k * m) R).IsRoot μ ↔ IsPrimitiveRoot μ m
<VAR>x : ℝ<VAR>n : ℕ<GOAL>sin (π / 2 ^ (n + 2)) = √(2 - sqrtTwoAddSeries 0 n) / 2
<VAR>x : ℝ<VAR>n : ℕ<GOAL>1 / 2 * 2 ^ 2 - sqrtTwoAddSeries 0 n / 4 * 2 ^ 2 = 2 - sqrtTwoAddSeries 0 n
<VAR>x : ℝ<VAR>n : ℕ<GOAL>0 ≤ 2 - sqrtTwoAddSeries 0 n
<VAR>x : ℝ<VAR>n : ℕ<GOAL>0 ≤ sin (π / 2 ^ (n + 2)) * 2
<VAR>x : ℝ<VAR>n : ℕ<GOAL>0 ≤ π / 2 ^ (n + 2)
<VAR>x : ℝ<VAR>n : ℕ<GOAL>π / 2 ^ (n + 2) ≤ π
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r : R[X]<VAR>x : R<VAR>p : R[X]<GOAL>eval 0 p = p.coeff 0 * 0 ^ 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r : R[X]<VAR>x : R<VAR>p : R[X]<GOAL>(p.sum fun e a => a * 0 ^ e) = p.coeff 0 * 0 ^ 0
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<GOAL>IsCompact ↑U
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<GOAL>↑U = ⇑hU.fromSpec.val.base '' Set.univ
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<GOAL>⇑hU.fromSpec.val.base '' Set.univ = Set.range ⇑hU.fromSpec.val.base
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v s t : Finset α<VAR>hε : 0 < ε<VAR>hP : P.IsEquipartition<VAR>hP' : 4 / ε ≤ ↑P.parts.card<GOAL>↑(P.parts.biUnion offDiag).card ≤ ε / 2 * ↑A.card ^ 2
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v s t : Finset α<VAR>hε : 0 < ε<VAR>P : Finpartition ⊥<VAR>hP : P.IsEquipartition<VAR>hP' : 4 / ε ≤ ↑P.parts.card<GOAL>↑(P.parts.biUnion offDiag).card ≤ ε / 2 * ↑⊥.card ^ 2
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v s t : Finset α<VAR>hε : 0 < ε<VAR>hP : P.IsEquipartition<VAR>hP' : 4 / ε ≤ ↑P.parts.card<VAR>hA : A.Nonempty<GOAL>↑(P.parts.biUnion offDiag).card ≤ ε / 2 * ↑A.card ^ 2
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v s t : Finset α<VAR>hε : 0 < ε<VAR>hP : P.IsEquipartition<VAR>hP' : 4 / ε ≤ ↑P.parts.card<VAR>hA : A.Nonempty<GOAL>↑A.card * (↑A.card + ↑P.parts.card) / ↑P.parts.card ≤ ε / 2 * ↑A.card ^ 2
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v s t : Finset α<VAR>hε : 0 < ε<VAR>hP : P.IsEquipartition<VAR>hP' : 4 / ε ≤ ↑P.parts.card<VAR>hA : A.Nonempty<GOAL>↑A.card * (↑A.card + ↑P.parts.card) ≤ ε / 2 * ↑A.card ^ 2 * ↑P.parts.card
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v s t : Finset α<VAR>hε : 0 < ε<VAR>hP : P.IsEquipartition<VAR>hP' : 4 / ε ≤ ↑P.parts.card<VAR>hA : A.Nonempty<VAR>this : ↑A.card + ↑P.parts.card ≤ 2 * ↑A.card<GOAL>↑A.card * (↑A.card + ↑P.parts.card) ≤ ε / 2 * ↑A.card ^ 2 * ↑P.parts.card
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v s t : Finset α<VAR>hε : 0 < ε<VAR>hP : P.IsEquipartition<VAR>hP' : 4 / ε ≤ ↑P.parts.card<VAR>hA : A.Nonempty<VAR>this : ↑A.card + ↑P.parts.card ≤ 2 * ↑A.card<GOAL>↑A.card * (2 * ↑A.card) ≤ ε / 2 * ↑A.card ^ 2 * ↑P.parts.card
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v s t : Finset α<VAR>hε : 0 < ε<VAR>hP : P.IsEquipartition<VAR>hP' : 4 / ε ≤ ↑P.parts.card<VAR>hA : A.Nonempty<VAR>this : ↑A.card + ↑P.parts.card ≤ 2 * ↑A.card<GOAL>1 ≤ ε / 4 * ↑P.parts.card
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v s t : Finset α<VAR>hε : 0 < ε<VAR>hP : P.IsEquipartition<VAR>hP' : 4 / ε ≤ ↑P.parts.card<VAR>hA : A.Nonempty<VAR>this : ↑A.card + ↑P.parts.card ≤ 2 * ↑A.card<GOAL>0 < ε / 4
<VAR>x✝ y✝ x y : ℝ<VAR>hx : 0 ≤ x<GOAL>x < √y ↔ x ^ 2 < y
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q p : ℕ<VAR>f : R[X]<GOAL>((expand R p) f).natDegree = f.natDegree * p
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q p : ℕ<VAR>f : R[X]<VAR>hp : p = 0<GOAL>((expand R p) f).natDegree = f.natDegree * p
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q p : ℕ<VAR>f : R[X]<VAR>hp : p > 0<GOAL>((expand R p) f).natDegree = f.natDegree * p
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q p : ℕ<VAR>f : R[X]<VAR>hp : p > 0<VAR>hf : ¬f = 0<GOAL>((expand R p) f).natDegree = f.natDegree * p
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q p : ℕ<VAR>f : R[X]<VAR>hp : p > 0<VAR>hf : ¬f = 0<VAR>hf1 : (expand R p) f ≠ 0<GOAL>((expand R p) f).natDegree = f.natDegree * p
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q p : ℕ<VAR>f : R[X]<VAR>hp : p > 0<VAR>hf : ¬f = 0<VAR>hf1 : (expand R p) f ≠ 0<GOAL>↑((expand R p) f).natDegree = ↑(f.natDegree * p)