ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u_1<VAR>inst✝ : Monoid M<VAR>S : Submonoid M<VAR>x y : M<VAR>z : ↥S<VAR>h₁ : y * ↑z = 1<VAR>h₂ : x * y = 1<GOAL>x = ↑z
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasDerivedCategory C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<GOAL>triangleOfSES hS ∈ distinguishedTriangles
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasDerivedCategory C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<GOAL>∃ X Y f, Nonempty (triangleOfSES hS ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle f))
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<GOAL>ofFn f = map f (finRange n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β<VAR>U : ι → Set β<VAR>hU : iUnion U = univ<GOAL>Injective f ↔ ∀ (i : ι), Injective ((U i).restrictPreimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β<VAR>U : ι → Set β<VAR>hU : iUnion U = univ<VAR>H : ∀ (i : ι), Injective ((U i).restrictPreimage f)<VAR>x y : α<VAR>e : f x = f y<GOAL>x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β<VAR>U : ι → Set β<VAR>hU : iUnion U = univ<VAR>H : ∀ (i : ι), Injective ((U i).restrictPreimage f)<VAR>x y : α<VAR>e : f x = f y<VAR>i : ι<VAR>hi : f x ∈ U i<GOAL>x = y
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a : α<GOAL>⌈0⌉ = 0
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>Real.cos (angle x (x - y)) * ‖x - y‖ = ‖x‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, -y⟫_ℝ = 0<GOAL>Real.cos (angle x (x - y)) * ‖x - y‖ = ‖x‖
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : OplaxMonoidalFunctor C D<VAR>X Y Z : C<GOAL>F.δ X (Y ⊗ Z) ≫ F.obj X ◁ F.δ Y Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv = F.map (α_ X Y Z).inv ≫ F.δ (X ⊗ Y) Z ≫ F.δ X Y ▷ F.obj Z
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a✝ : α<VAR>f✝ g : α → β<VAR>inst✝ : DecidableEq α<VAR>s : Finset β<VAR>a : α<VAR>f : β → Multiset α<GOAL>count a (map (fun x => f x) s.val).sum = (map (fun x => count a (f x)) s.val).sum
<VAR>a t : ℝ<VAR>ht : 0 < t<GOAL>HasSum (fun n => 2 * Real.cos (2 * π * a * (↑n + 1)) * rexp (-π * (↑n + 1) ^ 2 * t)) (cosKernel (↑a) t - 1)
<VAR>a t : ℝ<VAR>ht : 0 < t<GOAL>HasSum (fun x => ↑(2 * Real.cos (2 * π * a * (↑x + 1)) * rexp (-π * (↑x + 1) ^ 2 * t))) (↑(cosKernel (↑a) t) - 1)
<VAR>a t : ℝ<VAR>ht : 0 < t<VAR>this : HasSum (fun n => cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) + cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t))) (↑(cosKernel (↑a) t) + cexp (2 * ↑π * I * ↑a * ↑0) * ↑(rexp (-π * ↑0 ^ 2 * t)))<GOAL>HasSum (fun x => ↑(2 * Real.cos (2 * π * a * (↑x + 1)) * rexp (-π * (↑x + 1) ^ 2 * t))) (↑(cosKernel (↑a) t) - 1)
<VAR>a t : ℝ<VAR>ht : 0 < t<VAR>this : HasSum (fun n => cexp (2 * ↑π * I * ↑a * ↑↑(n + 1)) * ↑(rexp (-π * ↑↑(n + 1) ^ 2 * t)) + cexp (2 * ↑π * I * ↑a * ↑(-↑(n + 1))) * ↑(rexp (-π * ↑(-↑(n + 1)) ^ 2 * t))) (↑(cosKernel (↑a) t) + cexp (2 * ↑π * I * ↑a * ↑0) * ↑(rexp (-π * ↑0 ^ 2 * t)) - ∑ i ∈ Finset.range 1, (cexp (2 * ↑π * I * ↑a * ↑↑i) * ↑(rexp (-π * ↑↑i ^ 2 * t)) + cexp (2 * ↑π * I * ↑a * ↑(-↑i)) * ↑(rexp (-π * ↑(-↑i) ^ 2 * t))))<GOAL>HasSum (fun x => ↑(2 * Real.cos (2 * π * a * (↑x + 1)) * rexp (-π * (↑x + 1) ^ 2 * t))) (↑(cosKernel (↑a) t) - 1)
<VAR>a t : ℝ<VAR>ht : 0 < t<VAR>this : HasSum (fun n => (cexp (2 * ↑π * I * ↑a * ↑(n + 1)) + cexp (-(2 * ↑π * I * ↑a * ↑(n + 1)))) * ↑(rexp (-π * ↑(n + 1) ^ 2 * t))) (↑(cosKernel (↑a) t) - 1)<GOAL>HasSum (fun x => ↑(2 * Real.cos (2 * π * a * (↑x + 1)) * rexp (-π * (↑x + 1) ^ 2 * t))) (↑(cosKernel (↑a) t) - 1)
<VAR>a t : ℝ<VAR>ht : 0 < t<VAR>this : HasSum (fun n => (cexp (2 * ↑π * I * ↑a * ↑(n + 1)) + cexp (-(2 * ↑π * I * ↑a * ↑(n + 1)))) * ↑(rexp (-π * ↑(n + 1) ^ 2 * t))) (↑(cosKernel (↑a) t) - 1)<VAR>n : ℕ<GOAL>↑(2 * Real.cos (2 * π * a * (↑n + 1)) * rexp (-π * (↑n + 1) ^ 2 * t)) = (cexp (2 * ↑π * I * ↑a * ↑(n + 1)) + cexp (-(2 * ↑π * I * ↑a * ↑(n + 1)))) * ↑(rexp (-π * ↑(n + 1) ^ 2 * t))
<VAR>a t : ℝ<VAR>ht : 0 < t<VAR>this : HasSum (fun n => (cexp (2 * ↑π * I * ↑a * ↑(n + 1)) + cexp (-(2 * ↑π * I * ↑a * ↑(n + 1)))) * ↑(rexp (-π * ↑(n + 1) ^ 2 * t))) (↑(cosKernel (↑a) t) - 1)<VAR>n : ℕ<GOAL>2 * Complex.cos (2 * ↑π * ↑a * (↑n + 1)) * cexp (-↑π * (↑n + 1) ^ 2 * ↑t) = (cexp (2 * ↑π * I * ↑a * (↑n + 1)) + cexp (-(2 * ↑π * I * ↑a * (↑n + 1)))) * cexp (-↑π * (↑n + 1) ^ 2 * ↑t)
<VAR>a t : ℝ<VAR>ht : 0 < t<VAR>this : HasSum (fun n => (cexp (2 * ↑π * I * ↑a * ↑(n + 1)) + cexp (-(2 * ↑π * I * ↑a * ↑(n + 1)))) * ↑(rexp (-π * ↑(n + 1) ^ 2 * t))) (↑(cosKernel (↑a) t) - 1)<VAR>n : ℕ<GOAL>(cexp (2 * ↑π * ↑a * (↑n + 1) * I) + cexp (-(2 * ↑π * ↑a * (↑n + 1)) * I)) * cexp (-↑π * (↑n + 1) ^ 2 * ↑t) = (cexp (2 * ↑π * I * ↑a * (↑n + 1)) + cexp (-(2 * ↑π * I * ↑a * (↑n + 1)))) * cexp (-↑π * (↑n + 1) ^ 2 * ↑t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → ℝ<VAR>hf : Summable f<GOAL>Summable fun n => (f n).toNNReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → ℝ<VAR>hf : Summable f<GOAL>Summable fun a => ↑(f a).toNNReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → ℝ<VAR>hf : Summable f<VAR>n : α<GOAL>↑(f n).toNNReal ≤ |f n|
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Multiset α<GOAL>(Finset.Ioc s t).card = ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s) - 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f fab : α → β<VAR>fbc : β → γ<VAR>ga ga' : α → α<VAR>gb gb' : β → β<VAR>gc gc' : γ → γ<VAR>h : Semiconj f ga gb<VAR>ha : RightInverse ga' ga<VAR>hb : LeftInverse gb' gb<VAR>x : α<GOAL>f (ga' x) = gb' (f x)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>fin : hausdorffEdist s t ≠ ⊤<GOAL>infDist x t ≤ infDist x s + hausdorffDist s t
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>fin : hausdorffEdist s t ≠ ⊤<VAR>h : infEdist x s = ⊤<GOAL>infEdist x t = ⊤
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>fin : hausdorffEdist s t ≠ ⊤<VAR>h : ¬s.Nonempty<GOAL>¬t.Nonempty
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>fin : hausdorffEdist t s ≠ ⊤<VAR>h : ¬s.Nonempty<GOAL>¬t.Nonempty
<VAR>a x y : ℂ<VAR>hy : y ≠ 0<GOAL>angle 1 y = |y.arg|
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f : (a : Ordinal.{u_4}) → a < 1 → Ordinal.{max u_4 u_5}<GOAL>bsup 1 f = f 0 ⋯
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : LinearOrderedField k<VAR>inst✝² : OrderedAddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : OrderedSMul k E<VAR>f : k → E<VAR>a b r : k<VAR>h : 0 < r * (b - a)<GOAL>f ((lineMap a b) r) ≤ (lineMap (f a) (f b)) r ↔ slope f a ((lineMap a b) r) ≤ slope f a b
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>K : Set α<VAR>p : ι → Prop<VAR>s : ι → Set (α × α)<VAR>hU : (𝓤 α).HasBasis p s<VAR>A B : Set α<VAR>hA : IsCompact A<VAR>hB : IsClosed B<VAR>h : Disjoint A B<GOAL>∃ i, p i ∧ Disjoint (⋃ x ∈ A, ball x (s i)) (⋃ x ∈ B, ball x (s i))
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>K : Set α<VAR>p : ι → Prop<VAR>s : ι → Set (α × α)<VAR>hU : (𝓤 α).HasBasis p s<VAR>A B : Set α<VAR>hA : IsCompact A<VAR>hB : IsClosed B<VAR>h : Disjoint A B<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>hVAB : Disjoint (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)<GOAL>∃ i, p i ∧ Disjoint (⋃ x ∈ A, ball x (s i)) (⋃ x ∈ B, ball x (s i))
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>K : Set α<VAR>p : ι → Prop<VAR>s : ι → Set (α × α)<VAR>hU : (𝓤 α).HasBasis p s<VAR>A B : Set α<VAR>hA : IsCompact A<VAR>hB : IsClosed B<VAR>h : Disjoint A B<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>hVAB : Disjoint (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)<VAR>i : ι<VAR>hi : p i<VAR>hiV : s i ⊆ V<GOAL>∃ i, p i ∧ Disjoint (⋃ x ∈ A, ball x (s i)) (⋃ x ∈ B, ball x (s i))
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>A : Type u_1<VAR>inst✝¹ : Category.{?u.11500, u_1} A<VAR>S : C<VAR>E : PreOneHypercover S<VAR>i₁ i₂ : E.I₀<VAR>inst✝ : HasPullback (E.f i₁) (E.f i₂)<GOAL>E.sieve₁' i₁ i₂ = E.sieve₁ (pullback.fst (E.f i₁) (E.f i₂)) (pullback.snd (E.f i₁) (E.f i₂))
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>A : Type u_1<VAR>inst✝¹ : Category.{?u.11500, u_1} A<VAR>S : C<VAR>E : PreOneHypercover S<VAR>i₁ i₂ : E.I₀<VAR>inst✝ : HasPullback (E.f i₁) (E.f i₂)<GOAL>Sieve.pullback (𝟙 (pullback (E.f i₁) (E.f i₂))) (E.sieve₁' i₁ i₂) = Sieve.pullback (pullback.lift (pullback.fst (E.f i₁) (E.f i₂)) (pullback.snd (E.f i₁) (E.f i₂)) ⋯) (E.sieve₁' i₁ i₂)
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n : A<GOAL>1 ≤ P ↔ 1 ∈ P
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι✝ : Type uι<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : DecidableEq ι✝<VAR>b✝ : Basis ι✝ R M<VAR>ι : Type u_1<VAR>inst✝ : _root_.Finite ι<VAR>b : Basis ι R M<GOAL>range (Dual.eval R M) = ⊤
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>a b : α<GOAL>some ⁻¹' Icc ↑a ↑b = Icc a b
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type w<VAR>inst✝¹ : Category.{z, w} D<VAR>inst✝ : Abelian D<VAR>F G : C ⥤ D<VAR>α : F ⟶ G<VAR>X : C<GOAL>(kernel.ι α).app X ≫ 𝟙 (F.obj X) = (PreservesKernel.iso ((evaluation C D).obj X) α).hom ≫ kernel.ι (α.app X)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type w<VAR>inst✝¹ : Category.{z, w} D<VAR>inst✝ : Abelian D<VAR>F G : C ⥤ D<VAR>α : F ⟶ G<VAR>X : C<GOAL>(kernel.ι α).app X = kernelComparison α ((evaluation C D).obj X) ≫ kernel.ι (α.app X)
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>ι : Type u_2<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι ℤ (𝓞 K)<VAR>b₀ : Basis ι ℤ (𝓞 K) := (RingOfIntegers.basis K).reindex ((RingOfIntegers.basis K).indexEquiv b)<GOAL>Algebra.discr ℤ ⇑b = discr K
<VAR>b : ℂ<VAR>hb : 0 < b.re<GOAL>Integrable (fun x => cexp (-b * ↑x ^ 2)) volume
<VAR>b : ℂ<VAR>hb : 0 < b.re<GOAL>HasFiniteIntegral (fun x => cexp (-b * ↑x ^ 2)) volume
<VAR>b : ℂ<VAR>hb : 0 < b.re<GOAL>HasFiniteIntegral (fun a => ‖cexp (-b * ↑a ^ 2)‖) volume
<VAR>b : ℂ<VAR>hb : 0 < b.re<GOAL>HasFiniteIntegral (fun a => rexp (-b.re * a ^ 2)) volume
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>f : K[X]<VAR>hf : Splits i f<VAR>n : ℕ<GOAL>Splits i (f ^ n)
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>f : K[X]<VAR>hf : Splits i f<VAR>n : ℕ<GOAL>Splits i (∏ _x ∈ Finset.range n, f)
<VAR>k : Type u<VAR>inst✝ : Field k<VAR>f : k[X]<VAR>hfm : f.Monic<VAR>hfi : Irreducible f<GOAL>Polynomial.eval₂ (toAdjoinMonic k) ((Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X ⟨f, ⋯⟩)) f = 0
<VAR>k : Type u<VAR>inst✝ : Field k<VAR>f : k[X]<VAR>hfm : f.Monic<VAR>hfi : Irreducible f<GOAL>Polynomial.eval₂ MvPolynomial.C (MvPolynomial.X ⟨f, ⋯⟩) f ∈ maxIdeal k
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ<VAR>inst✝¹ : Zero R<VAR>a b : Γ<VAR>r : R<VAR>inst✝ : Zero Γ<VAR>x : HahnSeries Γ R<VAR>hx : x ≠ 0<GOAL>0 < x.orderTop ↔ 0 < x.order
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s : Multiset α<VAR>a : α<GOAL>{a} ⊆ s ↔ a ∈ s
<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>inst✝ : TopologicalSpace ι<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_ind : Inducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F)<VAR>F_cl : IsClosed (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<VAR>F_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q<GOAL>CompactSpace ι
<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>inst✝ : TopologicalSpace ι<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_ind : Inducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F)<VAR>F_cl : IsClosed (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<VAR>F_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q<VAR>this : Inducing ((⋃₀ 𝔖).restrict ∘ F)<GOAL>CompactSpace ι
<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>inst✝ : TopologicalSpace ι<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_ind : Inducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F)<VAR>F_cl : IsClosed (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<VAR>F_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q<VAR>this : Inducing ((⋃₀ 𝔖).restrict ∘ F)<GOAL>IsCompact (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>inst✝ : TopologicalSpace ι<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_ind : Inducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F)<VAR>F_cl : IsClosed (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<VAR>F_pointwiseCompact : ∀ x ∈ ⋃₀ 𝔖, ∃ Q, IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q<VAR>this : Inducing ((⋃₀ 𝔖).restrict ∘ F)<GOAL>IsCompact (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>inst✝ : TopologicalSpace ι<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_ind : Inducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F)<VAR>F_cl : IsClosed (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<VAR>this : Inducing ((⋃₀ 𝔖).restrict ∘ F)<VAR>Q : X → Set α<VAR>Q_compact : ∀ x ∈ ⋃₀ 𝔖, IsCompact (Q x)<VAR>F_in_Q : ∀ x ∈ ⋃₀ 𝔖, ∀ (i : ι), F i x ∈ Q x<GOAL>IsCompact (range ((⋃₀ 𝔖).restrict ∘ F))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x : F<GOAL>⟪0, x⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x : F<GOAL>(starRingEnd 𝕜) 0 * ⟪0, x⟫_𝕜 = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<GOAL>indicatorConstLp p ⋯ ⋯ c = 0
<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.degree < q.degree<GOAL>(p + q).degree = q.degree
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>α : Type u_3<VAR>inst✝² : NormedRing E<VAR>inst✝¹ : StarRing E<VAR>inst✝ : CstarRing E<VAR>U : ↥(unitary E)<VAR>A : E<VAR>a✝ : Nontrivial E<GOAL>‖↑U * A‖ = ‖A‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>α : Type u_3<VAR>inst✝² : NormedRing E<VAR>inst✝¹ : StarRing E<VAR>inst✝ : CstarRing E<VAR>U : ↥(unitary E)<VAR>A : E<VAR>a✝ : Nontrivial E<GOAL>‖↑U * A‖ ≤ ‖A‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>α : Type u_3<VAR>inst✝² : NormedRing E<VAR>inst✝¹ : StarRing E<VAR>inst✝ : CstarRing E<VAR>U : ↥(unitary E)<VAR>A : E<VAR>a✝ : Nontrivial E<GOAL>‖A‖ ≤ ‖↑U * A‖
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>m n : ℕ<VAR>h : Odd n<GOAL>n / 2 * 2 + 1 = n
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<GOAL>W.Ψ 4 = C W.preΨ₄ * W.ψ₂
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x✝ y : E<VAR>hs : IsCompact s<VAR>hδ : 0 ≤ δ<VAR>x : E<GOAL>s * closedBall x δ = x • cthickening δ s
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝⁵ : AddCommMonoid M₁<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M₁<VAR>inst✝² : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>M₃ : Type u_7<VAR>inst✝¹ : AddCommMonoid M₃<VAR>inst✝ : Module R M₃<VAR>v₃ : Basis l R M₃<VAR>f g : M₁ →ₗ[R] M₁<GOAL>(toMatrixAlgEquiv v₁) (f * g) = (toMatrixAlgEquiv v₁) f * (toMatrixAlgEquiv v₁) g
<VAR>R : Type u<VAR>inst✝ : LinearOrder R<VAR>x y : Tropical R<GOAL>x + y = x ↔ x ≤ y
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<GOAL>⊥ ∥ s ↔ s = ⊥
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>f g : WithLp ⊤ (α × β)<GOAL>edist f.1 g.1 ⊔ edist f.2 g.2 < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t u v : Finset α<VAR>a b x y : α<VAR>s : Finset α<VAR>hx : x ∈ s<GOAL>s.erase x = s.erase y ↔ x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t u v : Finset α<VAR>a b x y : α<VAR>s : Finset α<VAR>hx : x ∈ s<VAR>h : s.erase x = s.erase y<GOAL>x ∉ s.erase y
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : CommMonoid M<VAR>a : M<GOAL>IsUnit a ↔ ∃ b, b * a = 1
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : UniformSpace β<VAR>K : Set α<VAR>V : Set (β × β)<VAR>f : C(α, β)<VAR>ι : Type u₃<VAR>p : Filter ι<VAR>F : ι → C(α, β)<VAR>δ : ι → Type u_1<VAR>inst✝ : (i : ι) → TopologicalSpace (δ i)<VAR>φ : (i : ι) → C(δ i, α)<VAR>h_proper : ∀ (i : ι), IsProperMap ⇑(φ i)<VAR>h_lf : LocallyFinite fun i => range ⇑(φ i)<VAR>h_cover : ⋃ i, range ⇑(φ i) = univ<VAR>𝔖 : Set (Set α) := {K | IsCompact K}<VAR>𝔗 : (i : ι) → Set (Set (δ i)) := fun i => {K | IsCompact K}<VAR>h_image : ∀ (i : ι), MapsTo (fun x => ⇑(φ i) '' x) (𝔗 i) 𝔖<VAR>h_preimage : ∀ (i : ι), MapsTo (fun x => ⇑(φ i) ⁻¹' x) 𝔖 (𝔗 i)<GOAL>inferInstanceAs (UniformSpace C(α, β)) = ⨅ i, UniformSpace.comap (fun x => x.comp (φ i)) inferInstance
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : UniformSpace β<VAR>K : Set α<VAR>V : Set (β × β)<VAR>f : C(α, β)<VAR>ι : Type u₃<VAR>p : Filter ι<VAR>F : ι → C(α, β)<VAR>δ : ι → Type u_1<VAR>inst✝ : (i : ι) → TopologicalSpace (δ i)<VAR>φ : (i : ι) → C(δ i, α)<VAR>h_proper : ∀ (i : ι), IsProperMap ⇑(φ i)<VAR>h_lf : LocallyFinite fun i => range ⇑(φ i)<VAR>h_cover : ⋃ i, range ⇑(φ i) = univ<VAR>𝔖 : Set (Set α) := {K | IsCompact K}<VAR>𝔗 : (i : ι) → Set (Set (δ i)) := fun i => {K | IsCompact K}<VAR>h_image : ∀ (i : ι), MapsTo (fun x => ⇑(φ i) '' x) (𝔗 i) 𝔖<VAR>h_preimage : ∀ (i : ι), MapsTo (fun x => ⇑(φ i) ⁻¹' x) 𝔖 (𝔗 i)<VAR>h_cover' : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range ⇑(φ i)<GOAL>inferInstanceAs (UniformSpace C(α, β)) = ⨅ i, UniformSpace.comap (fun x => x.comp (φ i)) inferInstance
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : UniformSpace β<VAR>K : Set α<VAR>V : Set (β × β)<VAR>f : C(α, β)<VAR>ι : Type u₃<VAR>p : Filter ι<VAR>F : ι → C(α, β)<VAR>δ : ι → Type u_1<VAR>inst✝ : (i : ι) → TopologicalSpace (δ i)<VAR>φ : (i : ι) → C(δ i, α)<VAR>h_proper : ∀ (i : ι), IsProperMap ⇑(φ i)<VAR>h_lf : LocallyFinite fun i => range ⇑(φ i)<VAR>h_cover : ⋃ i, range ⇑(φ i) = univ<VAR>𝔖 : Set (Set α) := {K | IsCompact K}<VAR>𝔗 : (i : ι) → Set (Set (δ i)) := fun i => {K | IsCompact K}<VAR>h_image : ∀ (i : ι), MapsTo (fun x => ⇑(φ i) '' x) (𝔗 i) 𝔖<VAR>h_preimage : ∀ (i : ι), MapsTo (fun x => ⇑(φ i) ⁻¹' x) 𝔖 (𝔗 i)<VAR>h_cover' : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range ⇑(φ i)<GOAL>⨅ i, ⨅ i_1 ∈ 𝔗 i, UniformSpace.comap (((⇑UniformFun.ofFun ∘ i_1.restrict ∘ ⇑(UniformOnFun.toFun (𝔗 i))) ∘ ⇑(UniformOnFun.ofFun (𝔗 i)) ∘ (fun x => x ∘ ⇑(φ i)) ∘ ⇑(UniformOnFun.toFun 𝔖)) ∘ toUniformOnFunIsCompact) (UniformFun.uniformSpace (↑i_1) β) = ⨅ i, ⨅ i_1 ∈ {K | IsCompact K}, UniformSpace.comap (((⇑UniformFun.ofFun ∘ i_1.restrict ∘ ⇑(UniformOnFun.toFun {K | IsCompact K})) ∘ toUniformOnFunIsCompact) ∘ fun x => x.comp (φ i)) (UniformFun.uniformSpace (↑i_1) β)
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hX : AEStronglyMeasurable X μ<GOAL>evariance X μ < ⊤ ↔ Memℒp X 2 μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hX : AEStronglyMeasurable X μ<GOAL>evariance X μ < ⊤ → Memℒp X 2 μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hX : AEStronglyMeasurable X μ<GOAL>¬Memℒp X 2 μ → ¬evariance X μ < ⊤
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hX : AEStronglyMeasurable X μ<GOAL>¬Memℒp X 2 μ → evariance X μ = ⊤
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : Mul A<VAR>inst✝² : SMulWithZero R A<VAR>inst✝¹ : StarAddMonoid R<VAR>inst✝ : Star A<VAR>a : A<GOAL>IsStarNormal ↑a ↔ IsStarNormal a
<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>f : F[X]<VAR>hf : f ≠ 0<GOAL>f.natSepDegree = f.natDegree ↔ f.Separable
<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>f : F[X]<VAR>hf : f ≠ 0<GOAL>f.natSepDegree = f.natDegree ↔ (f.aroots f.SplittingField).toFinset.card = f.natDegree
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>ha : IsUnit A.det<VAR>m n : ℤ<GOAL>A ^ (m + n) = A ^ m * A ^ n
<VAR>α : Type u<VAR>α' : Type w<VAR>β : Type v<VAR>β' : Type x<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>r : α → γ → Prop<VAR>s : β → δ → Prop<VAR>x : α ⊕ β<VAR>y : γ ⊕ δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>d : δ<VAR>h₁ : LiftRel r s x y<VAR>h₂ : x.isLeft = true<GOAL>∃ a c, r a c ∧ x = inl a ∧ y = inl c
<VAR>α : Type u<VAR>α' : Type w<VAR>β : Type v<VAR>β' : Type x<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>r : α → γ → Prop<VAR>s : β → δ → Prop<VAR>y : γ ⊕ δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>d : δ<VAR>w✝ : α<VAR>h₁ : LiftRel r s (inl w✝) y<VAR>h₂ : (inl w✝).isLeft = true<GOAL>∃ a c, r a c ∧ inl w✝ = inl a ∧ y = inl c