ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : FiniteDimensional F E<VAR>inst✝ : IsGalois F E<VAR>α : E<VAR>hα : F⟮α⟯ = ⊤<VAR>iso : ↥F⟮α⟯ ≃ₐ[F] E := { toFun := fun e => ↑e, invFun := fun e => ⟨e, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }<VAR>H : IsIntegral F α<VAR>h_sep : IsSeparable F α<GOAL>Fintype.card (E ≃ₐ[F] E) = finrank F E
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : FiniteDimensional F E<VAR>inst✝ : IsGalois F E<VAR>α : E<VAR>hα : F⟮α⟯ = ⊤<VAR>iso : ↥F⟮α⟯ ≃ₐ[F] E := { toFun := fun e => ↑e, invFun := fun e => ⟨e, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }<VAR>H : IsIntegral F α<VAR>h_sep : IsSeparable F α<VAR>h_splits : Polynomial.Splits (algebraMap F E) (minpoly F α)<GOAL>Fintype.card (E ≃ₐ[F] E) = finrank F E
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : FiniteDimensional F E<VAR>inst✝ : IsGalois F E<VAR>α : E<VAR>hα : F⟮α⟯ = ⊤<VAR>iso : ↥F⟮α⟯ ≃ₐ[F] E := { toFun := fun e => ↑e, invFun := fun e => ⟨e, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }<VAR>H : IsIntegral F α<VAR>h_sep : IsSeparable F α<VAR>h_splits : Polynomial.Splits (algebraMap F ↥F⟮α⟯) (minpoly F α)<GOAL>Fintype.card (E ≃ₐ[F] E) = finrank F E
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : FiniteDimensional F E<VAR>inst✝ : IsGalois F E<VAR>α : E<VAR>hα : F⟮α⟯ = ⊤<VAR>iso : ↥F⟮α⟯ ≃ₐ[F] E := { toFun := fun e => ↑e, invFun := fun e => ⟨e, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }<VAR>H : IsIntegral F α<VAR>h_sep : IsSeparable F α<VAR>h_splits : Polynomial.Splits (algebraMap F ↥F⟮α⟯) (minpoly F α)<GOAL>Fintype.card (E ≃ₐ[F] E) = finrank F ↥F⟮α⟯
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : FiniteDimensional F E<VAR>inst✝ : IsGalois F E<VAR>α : E<VAR>hα : F⟮α⟯ = ⊤<VAR>iso : ↥F⟮α⟯ ≃ₐ[F] E := { toFun := fun e => ↑e, invFun := fun e => ⟨e, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }<VAR>H : IsIntegral F α<VAR>h_sep : IsSeparable F α<VAR>h_splits : Polynomial.Splits (algebraMap F ↥F⟮α⟯) (minpoly F α)<GOAL>Fintype.card (E ≃ₐ[F] E) = Fintype.card (↥F⟮α⟯ ≃ₐ[F] ↥F⟮α⟯)
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : FiniteDimensional F E<VAR>inst✝ : IsGalois F E<VAR>α : E<VAR>hα : F⟮α⟯ = ⊤<VAR>iso : ↥F⟮α⟯ ≃ₐ[F] E := { toFun := fun e => ↑e, invFun := fun e => ⟨e, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }<VAR>H : IsIntegral F α<VAR>h_sep : IsSeparable F α<VAR>h_splits : Polynomial.Splits (algebraMap F ↥F⟮α⟯) (minpoly F α)<GOAL>(E ≃ₐ[F] E) ≃ ↥F⟮α⟯ ≃ₐ[F] ↥F⟮α⟯
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>P : Generators R S<VAR>r : R<VAR>inst✝ : IsLocalization.Away r S<VAR>s : S<GOAL>(aeval fun x => IsLocalization.Away.invSelf r) ((fun s => C (IsLocalization.Away.sec r s).1 * X () ^ (IsLocalization.Away.sec r s).2) s) = s
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>P : Generators R S<VAR>r : R<VAR>inst✝ : IsLocalization.Away r S<VAR>s : S<GOAL>(algebraMap R S) (IsLocalization.Away.sec r s).1 * IsLocalization.Away.invSelf r ^ (IsLocalization.Away.sec r s).2 = s
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>P : Generators R S<VAR>r : R<VAR>inst✝ : IsLocalization.Away r S<VAR>s : S<GOAL>s * (algebraMap R S) r ^ (IsLocalization.Away.sec r s).2 * IsLocalization.mk' S 1 ⟨r, ⋯⟩ ^ (IsLocalization.Away.sec r s).2 = s
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>P : Generators R S<VAR>r : R<VAR>inst✝ : IsLocalization.Away r S<VAR>s : S<GOAL>s * IsLocalization.mk' S r 1 ^ (IsLocalization.Away.sec r s).2 * IsLocalization.mk' S 1 (⟨r, ⋯⟩ ^ (IsLocalization.Away.sec r s).2) = s
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>P : Generators R S<VAR>r : R<VAR>inst✝ : IsLocalization.Away r S<VAR>s : S<GOAL>s * IsLocalization.mk' S (r ^ (IsLocalization.Away.sec r s).2 * 1) (1 * ⟨r, ⋯⟩ ^ (IsLocalization.Away.sec r s).2) = s
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>P : Generators R S<VAR>r : R<VAR>inst✝ : IsLocalization.Away r S<VAR>s : S<GOAL>s * IsLocalization.mk' S r ⟨r, ⋯⟩ ^ (IsLocalization.Away.sec r s).2 = s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>f : β → γ<VAR>g : α → β<VAR>x : Filter α<VAR>y : Filter γ<GOAL>Tendsto f (map g x) y ↔ Tendsto (f ∘ g) x y
<VAR>α : Type u_1<VAR>inst✝² : LinearOrderedAddCommGroup α<VAR>inst✝¹ : Module ℚ α<VAR>inst✝ : PosSMulMono ℚ α<VAR>q : ℚ<VAR>a : α<GOAL>|q • a| = |q| • |a|
<VAR>R✝ : Type u<VAR>inst✝¹ : CommRing R✝<VAR>W : Projective R✝<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>P : Fin 3 → R<VAR>u : Rˣ<GOAL>(u • P) 0 = ↑u * P 0 ∧ (u • P) 1 = ↑u * P 1 ∧ (u • P) 2 = ↑u * P 2
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>b : n → α<GOAL>A.cramer b = A.adjugate *ᵥ b
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>b : n → α<GOAL>A.cramer b = Aᵀᵀ.adjugate *ᵥ b
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>b : n → α<GOAL>A.cramer b = (of fun i => Aᵀᵀ.cramer (Pi.single i 1))ᵀ *ᵥ b
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>b : n → α<VAR>this : b = ∑ i : n, b i • Pi.single i 1<GOAL>A.cramer b = (of fun i => Aᵀᵀ.cramer (Pi.single i 1))ᵀ *ᵥ b
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>b : n → α<VAR>this : b = ∑ i : n, b i • Pi.single i 1<VAR>k : n<GOAL>A.cramer (∑ i : n, b i • Pi.single i 1) k = ((of fun i => Aᵀᵀ.cramer (Pi.single i 1))ᵀ *ᵥ b) k
<GOAL>riemannZeta 2 = ↑π ^ 2 / 6
<GOAL>riemannZeta 2 = ↑(∑' (b : ℕ), 1 / ↑b ^ 2)
<GOAL>↑π ^ 2 / 6 = ↑(π ^ 2 / 6)
<VAR>k : Type u<VAR>inst✝ : Field k<VAR>n : ℕ<VAR>x : Step k n<GOAL>((ofStep k (n + 1)).comp (toStepSucc k n)) x = (ofStep k n) x
<VAR>k : Type u<VAR>inst✝ : Field k<VAR>n : ℕ<VAR>x : Step k n<VAR>hx : AlgebraicClosure.toStepOfLE' k n (n + 1) ⋯ x = (toStepSucc k n) x<GOAL>((ofStep k (n + 1)).comp (toStepSucc k n)) x = (ofStep k n) x
<VAR>k : Type u<VAR>inst✝ : Field k<VAR>n : ℕ<VAR>x : Step k n<VAR>hx : AlgebraicClosure.toStepOfLE' k n (n + 1) ⋯ x = (toStepSucc k n) x<GOAL>((Ring.DirectLimit.of (Step k) (fun i j h => ⇑(toStepOfLE k i j h)) (n + 1)).comp (toStepSucc k n)) x = (Ring.DirectLimit.of (Step k) (fun i j h => ⇑(toStepOfLE k i j h)) n) x
<VAR>k : Type u<VAR>inst✝ : Field k<VAR>n : ℕ<VAR>x : Step k n<VAR>hx : AlgebraicClosure.toStepOfLE' k n (n + 1) ⋯ x = (toStepSucc k n) x<GOAL>(Ring.DirectLimit.of (Step k) (fun i j h => ⇑(toStepOfLE k i j h)) (n + 1)) ((toStepSucc k n) x) = (Ring.DirectLimit.of (Step k) (fun i j h => ⇑(toStepOfLE k i j h)) n) x
<VAR>k : Type u<VAR>inst✝ : Field k<VAR>n : ℕ<VAR>x : Step k n<VAR>hx : AlgebraicClosure.toStepOfLE' k n (n + 1) ⋯ x = (toStepSucc k n) x<GOAL>(Ring.DirectLimit.of (Step k) (AlgebraicClosure.toStepOfLE' k) (n + 1)) (AlgebraicClosure.toStepOfLE' k n (n + 1) ⋯ x) = (Ring.DirectLimit.of (Step k) (AlgebraicClosure.toStepOfLE' k) n) x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>x : P<GOAL>IsPreconnected {y | s.SOppSide x y}
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>x : P<VAR>h : ↑s = ∅<GOAL>IsPreconnected {y | s.SOppSide x y}
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>x : P<VAR>h : (↑s).Nonempty<GOAL>IsPreconnected {y | s.SOppSide x y}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousSMul 𝕜 E<VAR>U : Set E<VAR>inst✝ : RegularSpace E<GOAL>(𝓝 0).HasBasis (fun s => s ∈ 𝓝 0 ∧ IsClosed s ∧ Balanced 𝕜 s) id
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousSMul 𝕜 E<VAR>U : Set E<VAR>inst✝ : RegularSpace E<VAR>s : Set E<VAR>hs : s ∈ 𝓝 0 ∧ IsClosed s<GOAL>∃ i', (i' ∈ 𝓝 0 ∧ IsClosed i' ∧ Balanced 𝕜 i') ∧ id i' ⊆ id s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousSMul 𝕜 E<VAR>U : Set E<VAR>inst✝ : RegularSpace E<VAR>s : Set E<VAR>hs : s ∈ 𝓝 0 ∧ IsClosed s<GOAL>IsClosed (balancedCore 𝕜 s) ∧ Balanced 𝕜 (balancedCore 𝕜 s)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>x : S<VAR>h : adjoin R {x} = ⊤<GOAL>conductor R x = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f✝ : α ↪ β<VAR>s✝ : Finset α<VAR>f : α ↪ β<VAR>s : Finset α<GOAL>∀ (x : β), x ∈ ↑(map f s) ↔ x ∈ ⇑f '' ↑s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝ : Ring α<VAR>a b : α<VAR>n : ℕ<VAR>k : α<VAR>hk : a = 2 * k + 1<GOAL>Odd (-a)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝ : Ring α<VAR>a b : α<VAR>n : ℕ<VAR>k : α<VAR>hk : a = 2 * k + 1<GOAL>-a = 2 * -(k + 1) + 1
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → E<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f (verticalStrip 0 1)<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<VAR>hz : z ∈ verticalStrip 0 1<GOAL>‖f z‖ ≤ ‖interpStrip f z‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → E<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f (verticalStrip 0 1)<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<VAR>hz : z ∈ verticalStrip 0 1<GOAL>Tendsto (fun x => ‖f z‖) (𝓝[>] 0) (𝓝 ‖f z‖)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → E<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f (verticalStrip 0 1)<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<VAR>hz : z ∈ verticalStrip 0 1<GOAL>Tendsto (fun ε => ‖(↑ε + ↑(sSupNormIm f 0)) ^ (1 - z) * (↑ε + ↑(sSupNormIm f 1)) ^ z‖) (𝓝[>] 0) (𝓝 ‖interpStrip f z‖)
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>σ : Type u_1<VAR>inst✝⁶ : DecidableEq σ<VAR>S : Type u_2<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : CommSemiring N<VAR>inst✝² : Algebra R N<VAR>A : Type u_3<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>m : σ →₀ ℕ<VAR>a : A<GOAL>(algebraTensorAlgEquiv R A).symm ((monomial m) a) = a ⊗ₜ[R] (monomial m) 1
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>σ : Type u_1<VAR>inst✝⁶ : DecidableEq σ<VAR>S : Type u_2<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : CommSemiring N<VAR>inst✝² : Algebra R N<VAR>A : Type u_3<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>m : σ →₀ ℕ<VAR>a : A<GOAL>(algebraTensorAlgEquiv R A).symm ((monomial 0) a) = a ⊗ₜ[R] (monomial 0) 1
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>σ : Type u_1<VAR>inst✝⁶ : DecidableEq σ<VAR>S : Type u_2<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : CommSemiring N<VAR>inst✝² : Algebra R N<VAR>A : Type u_3<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>m : σ →₀ ℕ<VAR>a : A<GOAL>∀ (a_1 : σ) (b : ℕ) (f : σ →₀ ℕ), a_1 ∉ f.support → b ≠ 0 → (algebraTensorAlgEquiv R A).symm ((monomial f) a) = a ⊗ₜ[R] (monomial f) 1 → (algebraTensorAlgEquiv R A).symm ((monomial (Finsupp.single a_1 b + f)) a) = a ⊗ₜ[R] (monomial (Finsupp.single a_1 b + f)) 1
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>s : Set α<VAR>x✝ : α<VAR>X : Type u<VAR>inst✝ : PseudoMetricSpace X<VAR>E : Set X<VAR>x : X<GOAL>x ∈ thickening δ E ↔ ∃ z ∈ E, dist x z < δ
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>s : Set α<VAR>x✝ : α<VAR>X : Type u<VAR>inst✝ : PseudoMetricSpace X<VAR>E : Set X<VAR>x : X<VAR>key_iff : ∀ (z : X), edist x z < ENNReal.ofReal δ ↔ dist x z < δ<GOAL>x ∈ thickening δ E ↔ ∃ z ∈ E, dist x z < δ
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>U : TopCat<VAR>X : Scheme<VAR>f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace<VAR>h : OpenEmbedding ⇑f<VAR>V : X.Opens<VAR>W : (X.restrict h).Opens<VAR>e : W ≤ X.ofRestrict h ⁻¹ᵁ V<GOAL>X.ofRestrict h ''ᵁ unop (op W) ≤ V
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>U : TopCat<VAR>X : Scheme<VAR>f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace<VAR>h : OpenEmbedding ⇑f<VAR>V : X.Opens<VAR>W : (X.restrict h).Opens<VAR>e : W ≤ X.ofRestrict h ⁻¹ᵁ V<GOAL>X.presheaf.map (⋯.adjunction.counit.app V).op ≫ (X.restrict h).presheaf.map (homOfLE e).op = X.presheaf.map (homOfLE ⋯).op
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<GOAL>m.sqrt < n ↔ m < n ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<GOAL>IntegrableOn f ∅ μ
<VAR>p : ℕ<VAR>z : ℤ<VAR>hp : p ≠ 1<VAR>hz : z ≠ 0<GOAL>(multiplicity (↑p) z).Dom
<VAR>p : ℕ<VAR>z : ℤ<VAR>hp : p ≠ 1<VAR>hz : z ≠ 0<GOAL>(↑p).natAbs ≠ 1 ∧ z ≠ 0
<VAR>p : ℕ<VAR>z : ℤ<VAR>hp : p ≠ 1<VAR>hz : z ≠ 0<GOAL>padicValInt p z = (multiplicity (↑p) z).get ⋯
<VAR>p : ℕ<VAR>z : ℤ<VAR>hp : p ≠ 1<VAR>hz : z ≠ 0<GOAL>(multiplicity p z.natAbs).get ⋯ = (multiplicity (↑p) z).get ⋯
<VAR>ι✝ : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → PartialOrder (π i)<VAR>inst✝ : (i : ι) → OrderBot (π i)<VAR>f : (i : ι) → π i<GOAL>IsAtom f → ∃ i a, IsAtom a ∧ f = Function.update ⊥ i a
<VAR>ι✝ : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → PartialOrder (π i)<VAR>inst✝ : (i : ι) → OrderBot (π i)<VAR>f : (i : ι) → π i<GOAL>(∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) → IsAtom f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f✝ g : Filter α<VAR>s✝ t : Set α<VAR>f : ι → Filter α<VAR>s : Set α<VAR>hs : s ∈ iInf f<VAR>p : Set α → Prop<VAR>uni : p univ<VAR>ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)<GOAL>p s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f✝ g : Filter α<VAR>s✝ t : Set α<VAR>f : ι → Filter α<VAR>s : Set α<VAR>hs : ∃ t, s ∈ ⨅ i ∈ t, f i.down<VAR>p : Set α → Prop<VAR>uni : p univ<VAR>ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)<GOAL>p s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f✝ g : Filter α<VAR>s✝ t : Set α<VAR>f : ι → Filter α<VAR>s : Set α<VAR>p : Set α → Prop<VAR>uni : p univ<VAR>ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)<VAR>hs : ∃ t, s ∈ t.inf fun a => f a.down<GOAL>p s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f✝ g : Filter α<VAR>s✝ t : Set α<VAR>f : ι → Filter α<VAR>s : Set α<VAR>p : Set α → Prop<VAR>uni : p univ<VAR>ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)<VAR>is : Finset (PLift ι)<VAR>his : s ∈ is.inf fun a => f a.down<GOAL>p s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n : ℕ<GOAL>⌈1⌉₊ = 1
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<GOAL>W.ΨSq 4 = W.preΨ₄ ^ 2 * W.Ψ₂Sq
<VAR>p : ℕ<VAR>hp : Prime p<GOAL>φ p = p - 1
<VAR>x : ℝ*<VAR>h : x ≠ 0<GOAL>x.Infinitesimal ↔ x⁻¹⁻¹.Infinitesimal
<VAR>f g : CircleDeg1Lift<VAR>x : ℝ<VAR>n : ℤ<GOAL>translate (Multiplicative.ofAdd x) ^ n = translate (Multiplicative.ofAdd (↑n * x))
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x + a) ⁻¹' Ioo b c = Ioo (b - a) (c - a)
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>A B : Finset (Finset α)<VAR>hA : A ⊆ (chunk hP G ε hU).parts<VAR>hB : B ⊆ (chunk hP G ε hV).parts<GOAL>|(∑ ab ∈ A.product B, ↑(G.edgeDensity ab.1 ab.2)) / (↑A.card * ↑B.card) - ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))| ≤ ε ^ 5 / 49
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>A B : Finset (Finset α)<VAR>hA : A ⊆ (chunk hP G ε hU).parts<VAR>hB : B ⊆ (chunk hP G ε hV).parts<GOAL>(∑ ab ∈ A.product B, ↑(G.edgeDensity ab.1 ab.2)) / (↑A.card * ↑B.card) - ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤ ε ^ 5 / 49 ∧ ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - (∑ ab ∈ A.product B, ↑(G.edgeDensity ab.1 ab.2)) / (↑A.card * ↑B.card) ≤ ε ^ 5 / 49
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>A B : Finset (Finset α)<VAR>hA : A ⊆ (chunk hP G ε hU).parts<VAR>hB : B ⊆ (chunk hP G ε hV).parts<GOAL>↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - (∑ ab ∈ A.product B, ↑(G.edgeDensity ab.1 ab.2)) / (↑A.card * ↑B.card) ≤ ε ^ 5 / 49
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>A B : Finset (Finset α)<VAR>hA : A ⊆ (chunk hP G ε hU).parts<VAR>hB : B ⊆ (chunk hP G ε hV).parts<GOAL>↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - (∑ ab ∈ A.product B, ↑(G.edgeDensity ab.1 ab.2)) / (↑A.card * ↑B.card) ≤ ε ^ 5 / 50
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>A B : Finset (Finset α)<VAR>hA : A ⊆ (chunk hP G ε hU).parts<VAR>hB : B ⊆ (chunk hP G ε hV).parts<GOAL>↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤ (∑ ab ∈ A.product B, ↑(G.edgeDensity ab.1 ab.2)) / (↑A.card * ↑B.card)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : σ → τ<VAR>hf : Injective f<VAR>i : σ<GOAL>(killCompl hf) ((rename f) (X i)) = X i
<VAR>𝕜 : Type u_1<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedSpace 𝕜 G<VAR>R : Type u_5<VAR>𝕜₂ : Type u_6<VAR>𝕜' : Type u_7<VAR>inst✝⁶ : NontriviallyNormedField 𝕜'<VAR>inst✝⁵ : NontriviallyNormedField 𝕜₂<VAR>M : Type u_8<VAR>inst✝⁴ : TopologicalSpace M<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>G' : Type u_9<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace 𝕜₂ G'<VAR>inst✝¹ : NormedSpace 𝕜' G'<VAR>inst✝ : SMulCommClass 𝕜₂ 𝕜' G'<VAR>f : E →L[𝕜] F →L[𝕜] G<VAR>c : 𝕜<VAR>x : E<VAR>y : F<GOAL>(f (c • x)) y = c • (f x) y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<VAR>x : α<VAR>y : Set α<GOAL>y ∈ 𝒫{x} ↔ y ∈ {∅, {x}}
<VAR>f : ℕ → ℂ<VAR>l : ℂ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)<VAR>M : ℝ<GOAL>Tendsto (fun z => ∑' (n : ℕ), f n * z ^ n) (𝓝[stolzSet M] 1) (𝓝 l)
<VAR>f : ℕ → ℂ<VAR>l : ℂ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)<VAR>M : ℝ<VAR>hM : M ≤ 1<GOAL>Tendsto (fun z => ∑' (n : ℕ), f n * z ^ n) (𝓝[stolzSet M] 1) (𝓝 l)
<VAR>f : ℕ → ℂ<VAR>l : ℂ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)<VAR>M : ℝ<VAR>hM : 1 < M<GOAL>Tendsto (fun z => ∑' (n : ℕ), f n * z ^ n) (𝓝[stolzSet M] 1) (𝓝 l)
<VAR>f : ℕ → ℂ<VAR>l : ℂ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)<VAR>M : ℝ<VAR>hM : 1 < M<VAR>s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i<VAR>g : ℂ → ℂ := fun z => ∑' (n : ℕ), f n * z ^ n<GOAL>Tendsto (fun z => ∑' (n : ℕ), f n * z ^ n) (𝓝[stolzSet M] 1) (𝓝 l)
<VAR>f : ℕ → ℂ<VAR>l : ℂ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)<VAR>M : ℝ<VAR>hM : 1 < M<VAR>s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i<VAR>g : ℂ → ℂ := fun z => ∑' (n : ℕ), f n * z ^ n<VAR>hm : ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (∑ i ∈ range n, f i) l < ε<GOAL>Tendsto (fun z => ∑' (n : ℕ), f n * z ^ n) (𝓝[stolzSet M] 1) (𝓝 l)
<VAR>f : ℕ → ℂ<VAR>l : ℂ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)<VAR>M : ℝ<VAR>hM : 1 < M<VAR>s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i<VAR>g : ℂ → ℂ := fun z => ∑' (n : ℕ), f n * z ^ n<VAR>hm : ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (∑ i ∈ range n, f i) l < ε<GOAL>∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, x ∈ stolzSet M → dist x 1 < δ → dist (∑' (n : ℕ), f n * x ^ n) l < ε
<VAR>f : ℕ → ℂ<VAR>l : ℂ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)<VAR>M : ℝ<VAR>hM : 1 < M<VAR>s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i<VAR>g : ℂ → ℂ := fun z => ∑' (n : ℕ), f n * z ^ n<VAR>hm : ∀ ε > 0, ∃ N, ∀ n ≥ N, ‖∑ i ∈ range n, f i - l‖ < ε<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>B₁ : ℕ<VAR>hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M<VAR>F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖<GOAL>∃ δ > 0, ∀ {x : ℂ}, x ∈ stolzSet M → ‖x - 1‖ < δ → ‖∑' (n : ℕ), f n * x ^ n - l‖ < ε