ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : IsPurelyInseparable F K<VAR>x : E<VAR>h : (minpoly F ((algebraMap E K) x)).Separable<GOAL>x ∈ (algebraMap F E).range
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : IsPurelyInseparable F K<VAR>x : E<VAR>h✝ : (minpoly F ((algebraMap E K) x)).Separable<VAR>y : F<VAR>h : (algebraMap F K) y = (algebraMap E K) x<GOAL>x ∈ (algebraMap F E).range
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>hσ : σ ^ 2 = 1<VAR>n : ℕ<VAR>hn : n ∈ σ.cycleType<GOAL>2 ∣ n
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<VAR>H : IsClosed (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))<GOAL>IsClosed (range ((⋃₀ 𝔖).restrict ∘ F))
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<VAR>H : IsClosed (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))<VAR>h✝ : IsEmpty α<GOAL>IsClosed (range ((⋃₀ 𝔖).restrict ∘ F))
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<VAR>H : IsClosed (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))<VAR>h✝ : Nonempty α<GOAL>IsClosed (range ((⋃₀ 𝔖).restrict ∘ F))
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<VAR>H : IsClosed (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))<VAR>h✝ : Nonempty α<GOAL>∀ (x : X → α), (∃ U, ↑U ≤ ⊤ ∧ Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) (↑U) (𝓝 ((UniformOnFun.ofFun 𝔖) x))) → (⋃₀ 𝔖).restrict x ∈ (⋃₀ 𝔖).restrict '' range F
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<GOAL>degrees 0 = 0
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<GOAL>(C 0).degrees = 0
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝² : (i : ι) → Module R (M₁ i)<VAR>inst✝¹ : Module R M₂<VAR>f f' : MultilinearMap R M₁ M₂<VAR>inst✝ : DecidableEq ι<VAR>c : ι → R<VAR>m : (i : ι) → M₁ i<VAR>s : Finset ι<GOAL>f (s.piecewise (fun i => c i • m i) m) = (∏ i ∈ s, c i) • f m
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝² : (i : ι) → Module R (M₁ i)<VAR>inst✝¹ : Module R M₂<VAR>f f' : MultilinearMap R M₁ M₂<VAR>inst✝ : DecidableEq ι<VAR>c : ι → R<VAR>m : (i : ι) → M₁ i<VAR>s : Finset ι<GOAL>∀ ⦃a : ι⦄ {s : Finset ι}, a ∉ s → f (s.piecewise (fun i => c i • m i) m) = (∏ i ∈ s, c i) • f m → f ((insert a s).piecewise (fun i => c i • m i) m) = (∏ i ∈ insert a s, c i) • f m
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝² : (i : ι) → Module R (M₁ i)<VAR>inst✝¹ : Module R M₂<VAR>f f' : MultilinearMap R M₁ M₂<VAR>inst✝ : DecidableEq ι<VAR>c : ι → R<VAR>m : (i : ι) → M₁ i<VAR>s✝ : Finset ι<VAR>j : ι<VAR>s : Finset ι<VAR>j_not_mem_s : j ∉ s<VAR>Hrec : f (s.piecewise (fun i => c i • m i) m) = (∏ i ∈ s, c i) • f m<VAR>A : update (s.piecewise (fun i => c i • m i) m) j (m j) = s.piecewise (fun i => c i • m i) m<GOAL>f ((insert j s).piecewise (fun i => c i • m i) m) = (∏ i ∈ insert j s, c i) • f m
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝² : (i : ι) → Module R (M₁ i)<VAR>inst✝¹ : Module R M₂<VAR>f f' : MultilinearMap R M₁ M₂<VAR>inst✝ : DecidableEq ι<VAR>c : ι → R<VAR>m : (i : ι) → M₁ i<VAR>s✝ : Finset ι<VAR>j : ι<VAR>s : Finset ι<VAR>j_not_mem_s : j ∉ s<VAR>Hrec : f (s.piecewise (fun i => c i • m i) m) = (∏ i ∈ s, c i) • f m<VAR>A : update (s.piecewise (fun i => c i • m i) m) j (m j) = s.piecewise (fun i => c i • m i) m<GOAL>c j • (∏ i ∈ s, c i) • f m = (∏ i ∈ insert j s, c i) • f m
<VAR>i : ℤ<GOAL>i.natAbs.lcm (natAbs 0) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : KleeneAlgebra α<VAR>a b c : α<VAR>h : a ≤ 1<GOAL>1 * a ≤ 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>s : Set E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module ℝ E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : LocallyConvexSpace ℝ E<VAR>inst✝² : ContinuousSMul 𝕜 E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>inst✝ : TopologicalAddGroup E<GOAL>(𝓝 0).HasBasis (fun s => 0 ∈ s ∧ IsOpen s ∧ Balanced 𝕜 s ∧ Convex ℝ s) id
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>s : Set E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module ℝ E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : LocallyConvexSpace ℝ E<VAR>inst✝² : ContinuousSMul 𝕜 E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>inst✝ : TopologicalAddGroup E<GOAL>∀ (i : Set E), i ∈ 𝓝 0 ∧ Balanced 𝕜 i ∧ Convex ℝ i → ∃ i', (0 ∈ i' ∧ IsOpen i' ∧ Balanced 𝕜 i' ∧ Convex ℝ i') ∧ id i' ⊆ id i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>s : Set E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module ℝ E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : LocallyConvexSpace ℝ E<VAR>inst✝² : ContinuousSMul 𝕜 E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>inst✝ : TopologicalAddGroup E<GOAL>∀ (i' : Set E), 0 ∈ i' ∧ IsOpen i' ∧ Balanced 𝕜 i' ∧ Convex ℝ i' → ∃ i, (i ∈ 𝓝 0 ∧ Balanced 𝕜 i ∧ Convex ℝ i) ∧ id i ⊆ id i'
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>s✝ : Set E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module ℝ E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : LocallyConvexSpace ℝ E<VAR>inst✝² : ContinuousSMul 𝕜 E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>inst✝ : TopologicalAddGroup E<VAR>s : Set E<VAR>hs_zero : 0 ∈ s<VAR>hs_open : IsOpen s<VAR>hs_balanced : Balanced 𝕜 s<VAR>hs_convex : Convex ℝ s<GOAL>∃ i, (i ∈ 𝓝 0 ∧ Balanced 𝕜 i ∧ Convex ℝ i) ∧ id i ⊆ id s
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<GOAL>(Spec Γ(X, U)).basicOpen ((Scheme.Hom.app hU.fromSpec U) f) = PrimeSpectrum.basicOpen f
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.147899, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<VAR>ψ : S₃ ⟶ S₁<GOAL>S₃.g ≫ ψ.τ₃ ≫ h.h₃ = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.147899, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<VAR>ψ : S₃ ⟶ S₁<GOAL>(ψ ≫ φ₁).τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + (ψ ≫ φ₂).τ₁
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.147899, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<VAR>ψ : S₃ ⟶ S₁<GOAL>(ψ ≫ φ₁).τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + (ψ ≫ φ₂).τ₂
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.147899, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<VAR>ψ : S₃ ⟶ S₁<GOAL>(ψ ≫ φ₁).τ₃ = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + (ψ ≫ φ₂).τ₃
<VAR>α : Type u<VAR>β✝ : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>β : Type u_2<VAR>p : β → Prop<VAR>f : β → ℝ≥0∞<VAR>hf₀ : ∀ (x : β), p x → 0 < f x<VAR>hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε<GOAL>(𝓤 α).HasBasis p fun x => {p | edist p.1 p.2 < f x}
<VAR>α : Type u<VAR>β✝ : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>β : Type u_2<VAR>p : β → Prop<VAR>f : β → ℝ≥0∞<VAR>hf₀ : ∀ (x : β), p x → 0 < f x<VAR>hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε<VAR>s : Set (α × α)<GOAL>(∃ i, 0 < i ∧ {p | edist p.1 p.2 < i} ⊆ s) ↔ ∃ i, p i ∧ {p | edist p.1 p.2 < f i} ⊆ s
<VAR>b : Bool<VAR>n : ℕ<GOAL>bit b -[n+1] = -[Nat.bit (!b) n+1]
<VAR>b : Bool<VAR>n : ℕ<GOAL>(2 * -[n+1] + bif b then 1 else 0) = -[2 * n + bif !b then 1 else 0+1]
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m✝ m : Multiset α<VAR>x : α<VAR>i : ℕ<GOAL>(x, i) ∈ Finset.map m.coeEmbedding Finset.univ ↔ (x, i) ∈ m.toEnumFinset
<VAR>E : Type u_1<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>x y : F<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>SameRay ℝ x y ↔ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<GOAL>AntilipschitzWith K f ↔ ∀ (x y : α), dist x y ≤ ↑K * dist (f x) (f y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<GOAL>(∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)) ↔ ∀ (x y : α), ↑(nndist x y) ≤ ↑K * ↑(nndist (f x) (f y))
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>n : Type w<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Invertible 2<VAR>Q : QuadraticMap R (n → R) R<VAR>i j : n<GOAL>Q.toMatrix'.transpose i j = Q.toMatrix' i j
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>h : ⊤ ≤ (span 𝕜 (Set.range v)).topologicalClosure<VAR>i : ι<GOAL>⋯.linearIsometryEquiv.symm (lp.single 2 i 1) = v i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>inst✝⁷ : InnerProductSpace 𝕜 F<VAR>inst✝⁶ : InnerProductSpace 𝕜 G<VAR>m : Type u_5<VAR>n : Type u_6<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : FiniteDimensional 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 F<VAR>v₁ : OrthonormalBasis n 𝕜 E<VAR>v₂ : OrthonormalBasis m 𝕜 F<VAR>f : E →ₗ[𝕜] F<GOAL>(toLin v₂.toBasis v₁.toBasis) ((toMatrix v₂.toBasis v₁.toBasis) (adjoint f)) = (toLin v₂.toBasis v₁.toBasis) ((toMatrix v₁.toBasis v₂.toBasis) f)ᴴ
<VAR>α : Type u<VAR>inst✝ : TopologicalSpace α<VAR>x : α<VAR>g : Ultrafilter α<VAR>gx : ↑g ≤ 𝓝 x<GOAL>Tendsto preStoneCechUnit (↑g) (𝓝 (preStoneCechUnit x))
<VAR>α : Type u<VAR>inst✝ : TopologicalSpace α<VAR>x : α<VAR>g : Ultrafilter α<VAR>gx : ↑g ≤ 𝓝 x<VAR>this : ↑(Ultrafilter.map pure g) ≤ 𝓝 g<GOAL>Tendsto preStoneCechUnit (↑g) (𝓝 (preStoneCechUnit x))
<VAR>α : Type u<VAR>inst✝ : TopologicalSpace α<VAR>x : α<VAR>g : Ultrafilter α<VAR>gx : ↑g ≤ 𝓝 x<VAR>this✝ : ↑(Ultrafilter.map pure g) ≤ 𝓝 g<VAR>this : map preStoneCechUnit ↑g ≤ 𝓝 (Quot.mk (fun F G => ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) g)<GOAL>Tendsto preStoneCechUnit (↑g) (𝓝 (preStoneCechUnit x))
<VAR>α : Type u<VAR>inst✝ : TopologicalSpace α<VAR>x : α<VAR>g : Ultrafilter α<VAR>gx : ↑g ≤ 𝓝 x<VAR>this✝ : ↑(Ultrafilter.map pure g) ≤ 𝓝 g<VAR>this : map preStoneCechUnit ↑g ≤ 𝓝 (Quot.mk (fun F G => ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) g)<VAR>e_1✝ : PreStoneCech α = Quot fun F G => ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x<GOAL>preStoneCechUnit x = Quot.mk (fun F G => ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) g
<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>H✝ K✝ : Subgroup G<VAR>k : Set G<VAR>N : Type u_5<VAR>inst✝¹ : Group N<VAR>P : Type u_6<VAR>inst✝ : Group P<VAR>H K : Subgroup G<GOAL>(K ⊓ H).subgroupOf K = H.subgroupOf K
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>v : ι → M<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : CommRing R₂<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M''<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R₂ M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>c d : R<VAR>x y : M<VAR>b : Basis ι R M<VAR>hli : LinearIndependent R v<VAR>hsp : ⊤ ≤ span R (Set.range v)<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<GOAL>((Basis.mk hli hsp).coord i) (v j) = if j = i then 1 else 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>v : ι → M<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : CommRing R₂<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M''<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R₂ M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>c d : R<VAR>x y : M<VAR>b : Basis ι R M<VAR>hli : LinearIndependent R v<VAR>hsp : ⊤ ≤ span R (Set.range v)<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>h : j = i<GOAL>((Basis.mk hli hsp).coord i) (v j) = if j = i then 1 else 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>v : ι → M<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : CommRing R₂<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M''<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R₂ M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>c d : R<VAR>x y : M<VAR>b : Basis ι R M<VAR>hli : LinearIndependent R v<VAR>hsp : ⊤ ≤ span R (Set.range v)<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>h : j ≠ i<GOAL>((Basis.mk hli hsp).coord i) (v j) = if j = i then 1 else 0
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝³ : SeminormedGroup E<VAR>inst✝² : SeminormedGroup F<VAR>inst✝¹ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>inst✝ : TopologicalSpace α<VAR>f : α → E<VAR>hf : HasCompactMulSupport f<VAR>h'f : Continuous f<GOAL>∃ C, ∀ (x : α), ‖f x‖ ≤ C
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝⁴ : LinearOrder ι<VAR>inst✝³ : LocallyFiniteOrderBot ι<VAR>inst✝² : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>h : finrank 𝕜 E = Fintype.card ι<VAR>f✝ f : ι → E<VAR>hf : Pairwise fun i j => ⟪f i, f j⟫_𝕜 = 0<VAR>i : ι<VAR>hi : f i ≠ 0<GOAL>(gramSchmidtOrthonormalBasis h f) i = (↑‖f i‖)⁻¹ • f i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝⁴ : LinearOrder ι<VAR>inst✝³ : LocallyFiniteOrderBot ι<VAR>inst✝² : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>h : finrank 𝕜 E = Fintype.card ι<VAR>f✝ f : ι → E<VAR>hf : Pairwise fun i j => ⟪f i, f j⟫_𝕜 = 0<VAR>i : ι<VAR>hi : f i ≠ 0<VAR>H : gramSchmidtNormed 𝕜 f i = (↑‖f i‖)⁻¹ • f i<GOAL>(gramSchmidtOrthonormalBasis h f) i = (↑‖f i‖)⁻¹ • f i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝⁴ : LinearOrder ι<VAR>inst✝³ : LocallyFiniteOrderBot ι<VAR>inst✝² : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>h : finrank 𝕜 E = Fintype.card ι<VAR>f✝ f : ι → E<VAR>hf : Pairwise fun i j => ⟪f i, f j⟫_𝕜 = 0<VAR>i : ι<VAR>hi : f i ≠ 0<VAR>H : gramSchmidtNormed 𝕜 f i = (↑‖f i‖)⁻¹ • f i<GOAL>gramSchmidtNormed 𝕜 f i ≠ 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : LinearOrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f✝ : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>x✝ y✝ z✝ : E<VAR>f : 𝕜 → β<VAR>x y z : 𝕜<VAR>hf : ConcaveOn 𝕜 (Set.Icc x y) f<VAR>hz : z ∈ Set.Icc x y<GOAL>min (f x) (f y) ≤ f z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : LinearOrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f✝ : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>x✝ y✝ z✝ : E<VAR>f : 𝕜 → β<VAR>x y z : 𝕜<VAR>hf : ConcaveOn 𝕜 [x-[𝕜]y] f<VAR>hz : z ∈ [x-[𝕜]y]<GOAL>min (f x) (f y) ≤ f z
<VAR>c : Code<VAR>n x : ℕ<GOAL>x ∈ c.eval n ↔ ∃ k, x ∈ evaln k c n
<VAR>c : Code<VAR>n x : ℕ<VAR>h : x ∈ c.eval n<GOAL>∃ k, x ∈ evaln k c n
<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 : R[X]<VAR>inst✝³ : CommRing T<VAR>p : T[X]<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>inst✝ : Algebra T S<VAR>a : S<VAR>h : a ∈ p.rootSet S<VAR>hf : p = 0<GOAL>False
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[T;T⁻¹]<VAR>m n : ℤ<GOAL>f * T m * T n = f * T (m + n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>s t : Finset α<VAR>inst✝ : DecidableEq α<VAR>a✝ a : α<GOAL>{a}ᶜ = univ.erase a
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>a : R<VAR>f : R[X]<VAR>n✝ : ℕ<GOAL>(C a * f).coeff n✝ = (a • f).coeff n✝
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x : ℝ<VAR>n : ℕ<GOAL>ENNReal.ofReal (n • x) = n • ENNReal.ofReal x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : G<GOAL>IsPrimitiveRoot ζ⁻¹ k ↔ IsPrimitiveRoot ζ k
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : G<GOAL>IsPrimitiveRoot ζ⁻¹ k → IsPrimitiveRoot ζ k
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : G<VAR>h : IsPrimitiveRoot ζ⁻¹ k<GOAL>IsPrimitiveRoot ζ k
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : G<VAR>h : IsPrimitiveRoot ζ⁻¹ k<GOAL>IsPrimitiveRoot ζ⁻¹⁻¹ k
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℂ<VAR>ha : 0 < a.re<VAR>b : ℂ<VAR>f : ℝ → ℂ := fun x => cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)<VAR>hCf : Continuous f<GOAL>∑' (n : ℤ), cexp (-↑π * a * ↑n ^ 2 + 2 * ↑π * b * ↑n) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / a * (↑n + I * b) ^ 2)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℂ<VAR>ha : 0 < a.re<VAR>b : ℂ<VAR>f : ℝ → ℂ := fun x => cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)<VAR>hCf : Continuous f<VAR>hFf : 𝓕 f = fun x => 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)<GOAL>∑' (n : ℤ), cexp (-↑π * a * ↑n ^ 2 + 2 * ↑π * b * ↑n) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / a * (↑n + I * b) ^ 2)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℂ<VAR>ha : 0 < a.re<VAR>b : ℂ<VAR>f : ℝ → ℂ := fun x => cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)<VAR>hCf : Continuous f<VAR>hFf : 𝓕 f = fun x => 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)<VAR>h1 : 0 < (↑π * a).re<GOAL>∑' (n : ℤ), cexp (-↑π * a * ↑n ^ 2 + 2 * ↑π * b * ↑n) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / a * (↑n + I * b) ^ 2)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℂ<VAR>ha : 0 < a.re<VAR>b : ℂ<VAR>f : ℝ → ℂ := fun x => cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)<VAR>hCf : Continuous f<VAR>hFf : 𝓕 f = fun x => 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)<VAR>h1 : 0 < (↑π * a).re<VAR>h2 : 0 < (↑π / a).re<GOAL>∑' (n : ℤ), cexp (-↑π * a * ↑n ^ 2 + 2 * ↑π * b * ↑n) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / a * (↑n + I * b) ^ 2)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℂ<VAR>ha : 0 < a.re<VAR>b : ℂ<VAR>f : ℝ → ℂ := fun x => cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)<VAR>hCf : Continuous f<VAR>hFf : 𝓕 f = fun x => 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)<VAR>h1 : 0 < (↑π * a).re<VAR>h2 : 0 < (↑π / a).re<VAR>f_bd : f =O[cocompact ℝ] fun x => |x| ^ (-2)<GOAL>∑' (n : ℤ), cexp (-↑π * a * ↑n ^ 2 + 2 * ↑π * b * ↑n) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / a * (↑n + I * b) ^ 2)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℂ<VAR>ha : 0 < a.re<VAR>b : ℂ<VAR>f : ℝ → ℂ := fun x => cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)<VAR>hCf : Continuous f<VAR>hFf : 𝓕 f = fun x => 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)<VAR>h1 : 0 < (↑π * a).re<VAR>h2 : 0 < (↑π / a).re<VAR>f_bd : f =O[cocompact ℝ] fun x => |x| ^ (-2)<VAR>Ff_bd : 𝓕 f =O[cocompact ℝ] fun x => |x| ^ (-2)<GOAL>∑' (n : ℤ), cexp (-↑π * a * ↑n ^ 2 + 2 * ↑π * b * ↑n) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / a * (↑n + I * b) ^ 2)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℂ<VAR>ha : 0 < a.re<VAR>b : ℂ<VAR>f : ℝ → ℂ := fun x => cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)<VAR>hCf : Continuous f<VAR>hFf : 𝓕 f = fun x => 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)<VAR>h1 : 0 < (↑π * a).re<VAR>h2 : 0 < (↑π / a).re<VAR>f_bd : f =O[cocompact ℝ] fun x => |x| ^ (-2)<VAR>Ff_bd : 𝓕 f =O[cocompact ℝ] fun x => |x| ^ (-2)<GOAL>∑' (n : ℤ), cexp (-↑π * a * ↑n ^ 2 + 2 * ↑π * b * ↑n) = ∑' (n : ℤ), f (0 + ↑n)